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.
Warning: the rest of this page may contain deprecated information.
Automatically cleaning your hypothesis like in linear programming (contains also an example of a way to have list of hypothesis in a custom tactic)