Other Coq Resources
Clone this wiki locally
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.
- Tips on code extraction
- Tips on improving performance
- Tips on notation (Haskell-style list comprehension)
- Marking cases and subcases in proofs
- Folding definitions in multiple places
- A conditional tactical
- An aggressive version of subst
- Decomposing all record-like structures
- Solving a goal by inversion on an unspecified hypothesis
- Solve goals about list inclusion
- Apply <-> forwards and backwards
- Manipulate equalities in the goal
- Automatically cleaning your hypothesis like in linear programming (contains also an example of a way to have list of hypothesis in a custom tactic)