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:

  • by David Pichardie
  • by Pierre Letouzey
  • by Assia Mahboubi

• 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.

• ITP'15 tutorial on Coq

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 ?
• Tips on code extraction
• Tips on improving performance
• Tips on notation (Haskell-style list comprehension)

Ltac tactics

• 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)

OCaml tactics

• A simple example of a tactic written in OCaml
• Unfold a fixpoint once (in OCaml)