GUIDE.md

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).
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.

Style guide

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, ...
• Don't use generated names of hypothesis.

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. Also use naive_solver instead of intuition or tauto.
4. If there is a typeclass to restrict when a typing rule applies, but it does not contain useful information for proving the typing rule, it should only be on the instance, not the lemma.
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.