Skip to content
Snippets Groups Projects
GUIDE.md 2.22 KiB
Newer Older
Michael Sammler's avatar
Michael Sammler committed
# WIP: Guide for RefinedC developers

This guide has two parts: First, a guide for writing typing rules.
Second, a style guide for RefinedC development.

## Rule guide

1. `SimplifyHyp` and `SimplifyGoal` rules should match: The
   information learned by the `SimplifyHyp` rule should be enough to
   prove the `SimplifyGoal`. Said another way, applying the
   `SimplifyHyp` instance and then proving `SimplifyGoal` should be
   equivalent to not using any of the two (except for learning more
   information).
Michael Sammler's avatar
Michael Sammler committed
2. If there are multiple `SimplifyHyp` or `SimplifyGoal` rules for the
   same proposition, one must ensure that the ones with the smaller
   number also have the smaller priority on the typeclass.
Michael Sammler's avatar
Michael Sammler committed

## Style guide

Michael Sammler's avatar
Michael Sammler committed
1. Follow the std++/Iris style except when noted otherwise below. In
   particular, do the following:
  - Only use `Lemma`, not any of the other variants like `Fact` or
    similar.
  - Specify all types in Definitions, both for arguments and for the
    Definition itself.
  - Use std++'s typeclasses to overload existing notations (e.g.
    `ElemOf` for `∈`).
  - Type parameters should use captial latin letters, starting from A
    and should usually be implicit.
  - Use `done` or `by ...` to solve trivial goals. It replaces
    `reflexivity`, `trivial`, `assumption`, ...
Michael Sammler's avatar
Michael Sammler committed
  - Don't use generated names of hypothesis.
Michael Sammler's avatar
Michael Sammler committed
2. Prefer the ssreflect tactics to the Coq tactics. I.e. use `move =>
   ...` instead of `intros ...`, `have ... : ...` instead of `assert`,
   `have ... := ...` instead of `pose proof`, `move Heq: (...) => ?`
   instead of `remember` and so on. See
   https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html
   for documentation on ssreflect.
3. Use std++ where possible. E.g. use `f <$> l` instead of `map f l`.
Michael Sammler's avatar
Michael Sammler committed
   Also use `naive_solver` instead of `intuition` or `tauto`.
Michael Sammler's avatar
Michael Sammler committed
4. If there is a typeclass to restrict when a typing rule applies, but
Michael Sammler's avatar
Michael Sammler committed
   it does not contain useful information for proving the typing rule,
   it should only be on the instance, not the lemma.
Michael Sammler's avatar
Michael Sammler committed
5. Use `if bool_decide P then ...` instead of `if decide P then ...`.
   This works better for automation since one can rewrite with
   `bool_decide P = true` in the first version, but not in the second
   version.