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 course Semantic of Proofs and Certified Mathematics
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)