Skip to main content

Automation

Gitlab

  • 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 best tactic. We can use best with parameters such as best use: lemma or best solve: lia. Once this tactic succeeds we replace it with the specialized tactic given on the terminal.
  • When possible, use standard tactics (tauto, 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 Time tactic.
  • The intros command has many variations; intros ? [] choose a variable name for the first parameter and does a destruct for the second.
  • Similarly, 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.