diff options
| author | Reynald Affeldt | 2020-04-09 16:51:27 +0900 |
|---|---|---|
| committer | Reynald Affeldt | 2020-04-09 23:05:09 +0900 |
| commit | 533dd3525b67278e770bbdb848a2568466cc3a65 (patch) | |
| tree | 3b90a2b8da01a8c5b148d2f7dab472e6ef2d3258 | |
| parent | 504a34ba48a29a252c40cfc0467f6b192243b6bc (diff) | |
move the contents of
https://github.com/math-comp/math-comp/wiki/good-practices
to
CONTRIBUTING.md
| -rw-r--r-- | CONTRIBUTING.md | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 85ee5a9..9e904ad 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -9,7 +9,11 @@ This file is not comprehensive yet and might still contain mistakes or unclear indications, please consider contributing. ## Proof style + ### General guidelines +- One important guideline is to structure proofs in blocks, i.e., + forward steps, to limit the scope of errors. + + See [G. Gonthier, A. Mahboubi, "An introduction to small scale reflection in Coq", p.103](https://doi.org/10.6092/issn.1972-5787/1979) for an illustration - **A line should have no more than 80 characters**. If a line is longer than that, it should be cut semantically. If there is no way to make a semantic cut (e.g. the user provides an explicit term that is @@ -19,6 +23,10 @@ make it readable. - Lines that close a goal must start with a terminator (`by` or `exact`). You should consider using an editor that highlight those terminators in a specific color (e.g. red). +- Chaining too many optional rewrites makes error detection hard. The idiom is + ``` + rewrite conditional_rule ?simplify_side_condition // next_rule. + ``` ### Spaces We write @@ -66,6 +74,14 @@ We write - Operators are surrounded by space, for example `n*m` should be written `n * m`. This particular example can be problematic if matrix.v is imported because then, `M *m N` is matrix product. +### Statement-macros + +- There is a number of "macros" that are available to state lemmas, like `commutative`, `associative`,... + (see [`ssrfun.v`](https://github.com/coq/coq/blob/master/theories/ssr/ssrfun.v)) + +- There are also macros that are available to to localize a statement, like `{in A, P}`,... + (see [`ssrbool.v`](https://github.com/coq/coq/blob/master/theories/ssr/ssrbool.v)) + ### Naming of variables - Variable names follow the following conventions. + Hypothesis should not be named `H`, `H'`,... (these collide with @@ -76,6 +92,7 @@ This particular example can be problematic if matrix.v is imported because then, + Elements of another ring should be named `x`, `y`, `z`, `u`, `v`, `w`, ... + Polynomials should be named by lower case letter `p`, `q`, `r` ... (to avoid collision with properties named `P`, `Q`, ...) + Matrices should be named `A`, `B`, ..., `M`, `N`, ... + + Polymorphic variables should be named `x`, ... ### Naming conventions for lemmas (non exhaustive) #### Names in the library usually obey one of the following conventions |