Contributing to Seymour

Thank you for your interest in contributing to Seymour! We welcome all contributions from the community and appreciate your efforts to improve the project.

Code style

If you contribute to the project, do not worry about code style too much; none of the style rules is enforced by a linter; we will accept your PR regardless of style; Martin will eventually adjust it. The guideline below is written primarily to assist you in reading the code.

Global variables

Implicit and typeclass arguments may be put after variable but explicit arguments may not be. Example and a non-example:

variable {R : Type} [R : Ring] (a : R)

While {R : Type} [R : Ring] in encouraged, the explicit argument (a : R) is not allowed to be a global variable. As a result, when you call a function or a lemma, you can be sure that all required arguments are visible at the lines of given function or lemma, which is very important.
We use global variables sparingly — usually for arguments that are used by the entire file or section.

Lines

Lines should not be longer than 128 characters (see the vertical ruler in VS Code) unless the line contains a long URL.
Starting a proof on a new line is recommended even in cases where the entire proof fits into the same line with the statement.
When the header of a declaration does not fit into one line, it is recommended to start the part after : on a new line.
Make 2 empty lines between imports and the content of the file (unless it has /-! a top-level comment section -/ in which case 1 empty line goes above and 1 empty line goes below).
Make 1 empty line between the start of a section and a declaration.
Make 1 empty line between declarations of any kind.
Make 1 empty line between a declaration and the end of a section.
Make 2 empty lines between the end of a section and what follows.
Each file ends with a linebreak.

Indentation

We use the same indentation as Mathlib.
- Subitem: 2 spaces
- Continuation of the same item after a linebreak: 4 spaces
Deviations from the style are welcome if they hint some metaïnformation.

Spaces

There is always a space before a bracket (of any kind) opens and after it closes. Example:

foo {R : Type} [R : Ring] (a b : R) : ⟨a, b⟩ ∈ S
Space after a brace opens and before a brace closes is written only in the Set builder and in Subtype declarations. Examples:

{ x : X | ∃ y : Y, Bar x y }

{ x₁ : α × β₁ // f x₁.fst = ◩x₁.snd }
With a comma, a space is written only after it, not before.
With a colon, a space is written from both sides.

Naming

Constants

Use camelCase and PascalCase and snake_case the same way Mathlib uses them.
- Constants that live in Sort (i.e., new Type and Prop declarations) are written in PascalCase
- All other constants that live in Type (e.g. functions that return real numbers) are written in camelCase
- Constants that live in Prop (i.e., theorems and lemmas) are written in snake_case whose constituents are other constants converted to camelCase and other standard tokens like ext or cancel
We like to write . in the name of a constant if it facilitates the use of dot notation when calling it. Usually it means that the part of the name that comes before the last . is identical to the type of the first explicit argument.
- In such a case, the parts before the last . are not converted to camelCase

Variables

Data variables (both in arguments and local variables) are always denoted by a single letter, possibly with other stuff after it like lower index or apostrophe.
Prop variables (both in arguments and local variables) are always denoted by multiple letters, possibly with other stuff after them like lower index or apostrophe.
- Prefix h means "the statement is anything about the following variables"
- Not starting with h means that the actual statement (or its substantial part) is spelled out, not only the variables that appear in it
- We sometimes use the digit 9 to refer to the number -1 in the names of Prop variables (only there; write neg_one in names of constants)
Examples:

intro a b a_lt_b hab
- a carries data (e.g. an integer)
- b carries data (e.g. an integer)
- a_lt_b carries a proof of a < b
- hab carries any information about a and b
intro x y x_eq_y h1 h1'
- x carries data (e.g. an integer)
- y carries data (e.g. an integer)
- x_eq_y carries a proof of x = y
- h1 carries any information involving the number 1
- h1' carries another information involving the number 1
intro M hM hM'
- M carries data (e.g. a matroid)
- hM carries any information about M
- hM' carries another information about M
intro M M' hM hM'
- M carries data (e.g. a matroid)
- M' carries data (e.g. a matroid)
- hM carries any information about M
- hM' carries any information about M'
intro M₁ M₂ hM₁ hM₂ hMM
- M₁ carries data (e.g. a matroid)
- M₂ carries data (e.g. a matroid)
- hM₁ carries any information about M₁
- hM₂ carries any information about M₂
- hMM carries any information about both M₁ and M₂ (indices after hMM are not needed)
Never name anything this or standalone h (these names are acceptable neither for data nor for propositions), but leaving automatically named stuff with this or h is encouraged if the term is not explicitly referred to later.
- Writing names like h₁ or h' or this' or this_ is strongly discouraged regardless of the purpose

Real-life example (focus on the third line of each version – explicit arguments of the lemma):

Unacceptable argument names:

lemma Multiset.sum_lt_sum {ι α : Type} [OrderedCancelAddCommMonoid α]
    {s : Multiset ι} {f g : ι → α}
    (h : ∀ i ∈ s, f i ≤ g i) (h' : ∃ i ∈ s, f i < g i) :
    (s.map f).sum < (s.map g).sum := by
  obtain ⟨l⟩ := s
  simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
  exact l.sum_lt_sum f g h h'

Bad argument names:

lemma Multiset.sum_lt_sum {ι α : Type} [OrderedCancelAddCommMonoid α]
    {s : Multiset ι} {f g : ι → α}
    (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
    (s.map f).sum < (s.map g).sum := by
  obtain ⟨l⟩ := s
  simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
  exact l.sum_lt_sum f g hle hlt

Acceptable argument names:

lemma Multiset.sum_lt_sum {ι α : Type} [OrderedCancelAddCommMonoid α]
    {s : Multiset ι} {f g : ι → α}
    (hfg : ∀ i ∈ s, f i ≤ g i) (hfg' : ∃ i ∈ s, f i < g i) :
    (s.map f).sum < (s.map g).sum := by
  obtain ⟨l⟩ := s
  simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
  exact l.sum_lt_sum f g hfg hfg'

Better argument names:

lemma Multiset.sum_lt_sum {ι α : Type} [OrderedCancelAddCommMonoid α]
    {s : Multiset ι} {f g : ι → α}
    (all_f_le_g : ∀ i ∈ s, f i ≤ g i) (exists_f_lt_g : ∃ i ∈ s, f i < g i) :
    (s.map f).sum < (s.map g).sum := by
  obtain ⟨l⟩ := s
  simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
  exact l.sum_lt_sum f g all_f_le_g exists_f_lt_g

Best argument names:

lemma Multiset.sum_lt_sum {ι α : Type} [OrderedCancelAddCommMonoid α]
    {s : Multiset ι} {f g : ι → α}
    (all_le : ∀ i ∈ s, f i ≤ g i) (exists_lt : ∃ i ∈ s, f i < g i) :
    (s.map f).sum < (s.map g).sum := by
  obtain ⟨l⟩ := s
  simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
  exact l.sum_lt_sum f g all_le exists_lt

Default single-capital-letter names

A ... matrix
B ... standard representation matrix
C ... circuit
D ... dependent set
E ... ground set
F ... field
G ... base
I ... independent set
J ... independent set
M ... matroid
O ... module
P ... proposition
Q ... proposition
R ... (semi)ring
S ... standard representation of a matroid
X ... set of row indices
Y ... set of col indices
Z ... subset of indices

Stability and readability

Do not open namespaces (but open scoped is fine).
Do not utilize automatic opening of a namespace for the declaration's name prefix.

For example, do not write:
```
def List.uppcaseLetters (l : List Char) := map Char.toUpper l
```
Either write down the full name of the function:
```
def List.uppcaseLetters (l : List Char) := List.map Char.toUpper l
```
Or, even better, utilize the dot notation:
```
def List.uppcaseLetters (l : List Char) := l.map Char.toUpper
```
This way:
- Reading the code is immediately clear without reading ahead and performing unification inside the reader's mind.
- The effect of the function will not change when you rename it (and the same applies to proofs).
Since deviation from the recommended style can be hard to spot here, we use the implicitNamespace linter by Damiano Testa to check that the automatically opened namespace hasn't been exploited.
Annotate types even in situations where they can be inferred automatically, for example:
```
def List.uppcaseLetters (l : List Char) : List Char := l.map Char.toUpper
```
The only exception is decidability assumptions such as [∀ a, Decidable (a ∈ Z)] where Z : Set _ because it appears all the time (we do not annotate the type of a),

Other

We currently prefer Type over universe-polymorphic types. Generalization to Type* will probably be done at the end of the project.
We prefer Unit over Fin 1 and we prefer ⟨⟩ over () for its only value.
We prefer not to write parentheses after quantifiers.
We do not write a space after ¬ but we write redundant parentheses around the negated expression when it contains any infix operator.
Orphaning parentheses is allowed.
We like to use our custom notation declared at the beginning of the Basic file.
We do not write .1 and .2 to access fields; write their names instead (with the exception for Iff.mp and Iff.mpr where we prefer our notation .→ and .← respectively).
We prefer Mathlib's have over Std's have inside tactic-block proofs.
We prefer Mathlib's congr_arg and congr_fun over Std's congrArg and congrFun respectively.
We prefer exfalso over absurd to discharge "impossible" proof branches.
When a variable name refers to exactly 2 out of 3 objects, we often refer to the missing object (instead of the two present objects) (analogical to naming parts of a triangle).
We do not write a space after ← in the rw syntax.
We do not write ↦ as this syntax does not work everywhere. Write => instead.
When passing arguments to simp and other tactics that don't care about in which order they come, pass variables first, constants later.
Ordering of cases when eliminating SignType is: first zero (0), then pos (1), then neg (-1).

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Contributing to Seymour

Code style

Global variables

Lines

Indentation

Spaces

Naming

Constants

Variables

Default single-capital-letter names

Stability and readability

Other

FilesExpand file tree

CONTRIBUTING.md

Latest commit

History

CONTRIBUTING.md

File metadata and controls

Contributing to Seymour

Code style

Global variables

Lines

Indentation

Spaces

Naming

Constants

Variables

Default single-capital-letter names

Stability and readability

Other