Other tutorials
Introduction to Coq
Beginners video tutorials, by Andrej Bauer
Coq in a Hurry, tutorial by Yves Bertot
Material from the Coq summer school Modelling and verifying algorithms in Coq: an introduction.
- Material from courses in French:
Material from the Using Proof Assistants for Programming Language Research tutorial.
See also the page Technique for formalization of variable binding.
Specific techniques
Warning: the rest of this page may contain deprecated information.
Tips
- Induction
How do I do mutual induction?
How do I do induction over a type containing pairs?
How can I do induction with self defined cases ?
Ltac tactics
Automatically cleaning your hypothesis like in linear programming (contains also an example of a way to have list of hypothesis in a custom tactic)
OCaml tactics
A simple example of a tactic written in OCaml
Unfold a fixpoint once (in OCaml)