update guidelines
All threads resolved!
All threads resolved!
Compare changes
+ 79
− 37
@@ -16,11 +16,7 @@ This project targets Coq *non*-experts. Accordingly, great emphasis is placed on
@@ -134,7 +130,6 @@ Note: We employ an automatic proof-length checker that runs as part of continuou
@@ -149,58 +144,105 @@ Guideline: do not name proof terms in type classes to prevent explicit dependenc
Some tactics, like `intros.` (without arguments) can introduce hypotheses with automatically generated names (typically `H`, `H0`, `H1`, `H2`). The use of such tactic should be avoided as they make the proofs less robust (any change can easily shift the naming). Note that ssreflect offers `move=> ?` that can be used when naming is not needed, while still being robust, because it ensures the automatically named hypotheses cannot be explicitly mentioned in the proof script. The fact that no automatically generated name is explicitly referred to is checked in the CI with the `-mangle-names` option of Coq.
Although the primary focus of Prosa is on the quality of the overall structure and the specifications, good proofs are short and readable. Since Coq tends to favor backward reasoning, try to adhere to it. Forward reasoning tends to be more verbose and to generate needlessly convoluted proof trees. To get an idea, read the following snippet:
- Instead of writing `exists x, P x /\ Q x`, prefer `exists2 x, P x & Q x` ([see documentation](https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/merge_requests/276#note_89874)). The latter saves a destruct making the intro patterns less cluttered in the proofs (i.e., one would write `=> [x Px Qx]` instead of having to write `=> [x [Px Qx]]`).
- It can be initially difficult to find lemmas applicable to `int` (in)equalities (e.g., when working with the GEL or ELF policies). The key is to note that `int` is just a particular instance of `ringType` or `numDomainType` and generic lemmas for these algebraic structures do apply (a lot of them are in [`ssralg`](https://math-comp.github.io/htmldoc/mathcomp.algebra.ssralg.html) or [`ssrnum`](https://math-comp.github.io/htmldoc/mathcomp.algebra.ssrnum.html)). To find applicable lemmas with `Search`, make sure to specify the appropriate notation scope `%R`. For example, `Search (_ + _)%R.` will find lemmas about addition that are applicable to `int`. As another example, `Search +%R -%R "K".` will find relevant cancellation lemmas (which by ssreflect convention include the letter "K" in their names).