... | ... | @@ -27,13 +27,15 @@ Always use Unicode variants of forall, exists, ->, <=, >= |
|
|
|
|
|
Use `Context`, never `Variable`
|
|
|
|
|
|
**TODO::** Use `Implicit Types`, never `Implicit Type`
|
|
|
**TODO:** Use `Implicit Types`, never `Implicit Type`
|
|
|
|
|
|
Use `Lemma`, not `Theorem` (or the other variants: `Fact`, `Corollary`,
|
|
|
`Remark`)
|
|
|
|
|
|
Tests may use `Example` for theorems.
|
|
|
|
|
|
*RJ*: Why this? In Iris itself, they use `Lemma` as well.
|
|
|
|
|
|
### Uncategorized
|
|
|
|
|
|
Indent the body of a match by one space:
|
... | ... | @@ -45,6 +47,8 @@ match foo with |
|
|
long line here using
|
|
|
```
|
|
|
|
|
|
*RJ*: This is odd, usually everything is in (multiples of) 2 spaces, I think.
|
|
|
|
|
|
Avoid using the extra square brackets around an Ltac match:
|
|
|
|
|
|
**Good:**
|
... | ... | @@ -61,7 +65,7 @@ match goal with |
|
|
|
|
|
```
|
|
|
|
|
|
Use coqdoc syntax in comments for Coq identifiers and inline code, eg `[cmraT]`
|
|
|
Use coqdoc syntax in comments for Coq identifiers and inline code, e.g. `[cmraT]`
|
|
|
|
|
|
Put proofs either all on one line (`Proof. reflexivity. Qed.`) or split up the usual way with indentation.
|
|
|
|
... | ... | @@ -100,11 +104,13 @@ Lemma foo x y z : |
|
|
x < z.
|
|
|
```
|
|
|
|
|
|
**TODO:** Use `"[H1 H2]"` when possible otherwise do `"(H1&H2&H3)"`
|
|
|
**TODO:** Use `"[H1 H2]"` when possible otherwise do `"(H1 & H2 & H3)"`
|
|
|
|
|
|
*RJ*: I added spaces around the `&`.
|
|
|
|
|
|
For tests with output put `Check "theorem name in a string"` before it so that the output from different tests is separated.
|
|
|
|
|
|
For long `t; [t1 | t2 | t3]` split them like this:
|
|
|
For long `t; [t1 | t2 | t3]` split them like this, and indent by 2 spaces:
|
|
|
|
|
|
**Good:**
|
|
|
```coq
|
... | ... | @@ -124,15 +130,15 @@ theories/base_logic/lib is for constructions in the base logic (using own) |
|
|
* `*_ctx` for persistent facts (often an invariant) needed by everything in a library
|
|
|
* `*_interp` for a function from some representation to iProp
|
|
|
* If you have lemma `foo` which is an iff and you want single direction versions, name them `foo_1` (forward) and `foo_2` (backward)
|
|
|
* If you have a lemma `foo` parametrized by a relation, you might want a version specialized to Leibniz equality for better rewrite support; name that version `foo_L` and state it with plain equality (eg, `dom_empty_L` in stdpp). You might take an assumption `LeibnizEquiv A` if the original version took an equivalence (say the OFE equivalence) to assume that the provided equivalence is plain equality.
|
|
|
* If you have a lemma `foo` parametrized by an equivalence relation, you might want a version specialized to Leibniz equality for better rewrite support; name that version `foo_L` and state it with plain equality (e.g., `dom_empty_L` in stdpp). You might take an assumption `LeibnizEquiv A` if the original version took an equivalence (say the OFE equivalence) to assume that the provided equivalence is plain equality.
|
|
|
* Lower-case theorem names, lower-case types, upper-case constructors
|
|
|
* **TODO:** how should `f (g x) = f' (g' x)` be named?
|
|
|
* `list_lookup_insert` is named by context (the type involved), then the two functions outside-in on the left-hand-side, so it has the type `lookup (insert …) = …` where the `insert` is on a list. Notations mean it doesn’t actually look like this and the insert is textually first.
|
|
|
* Injectivity theorems are instances of `Inj` and then are used with `inj`
|
|
|
* Suffixes `_l` and `_r` when we have binary `op x y` and a theorem related to the left or right. For example, `sep_mono_l` says bi_sep is monotonic in its left argument (holding the right constant)
|
|
|
* Suffixes `_l` and `_r` when we have binary `op x y` and a theorem related to the left or right. For example, `sep_mono_l` says bi_sep is monotonic in its left argument (holding the right constant).
|
|
|
* Entailments at the top level are typically written `P -* Q`, which is notation
|
|
|
for P ⊢ Q. If you have a theorem which has no premises you have to write ⊢ P
|
|
|
explicitly (for example, common to have `⊢ |==> ∃ γ, …` for an allocation
|
|
|
for `P ⊢ Q`. If you have a theorem which has no premises you have to write ⊢ P
|
|
|
explicitly (for example, it is common to have `⊢ |==> ∃ γ, …` for an allocation
|
|
|
theorem)
|
|
|
* Suffix `'` (prime) is used when `foo'` is a corollary of `foo`. Try to avoid
|
|
|
these since the name doesn't convey how `foo'` is related to `foo`.
|
... | ... | |