Other Coq Resources
-
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.
- 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 ?
- 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
- 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)
- A simple example of a tactic written in OCaml
- Unfold a fixpoint once (in OCaml)
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.