- Try to have proofs that are automated but not too long to execute.
- The LTac scripts are useful to write down proofs techniques that are domain-specific. This helps to save time but also serves as documentation. An example of LTac script where we were doing always the same things is for the data-encodings: /docs/environment/proofs/data_encoding
- We use Coq Hammer https://coqhammer.github.io/ to automate things, especially the
besttactic. We can use
bestwith parameters such as
best use: lemmaor
best solve: lia. Once this tactic succeeds we replace it with the specialized tactic given on the terminal.
- When possible, use standard tactics (
easy, ...) rather than Coq Hammer. It is generally faster for the execution time, and more standard.
- To measure the execution time of a tactic there is the command
introscommand has many variations;
intros ? choose a variable name for the first parameter and does a
destructfor the second.
destruct (_ && _) eqn:?will destruct an expression matching
_ && _and generate a name for the associated equation.
- Avoiding generated names when possible helps automation.
- Automation helps to go faster, have more maintainable proofs and adapt to code changes in OCaml.