-
Equality in Coq
For the first meeting we said that one could prove "associativity of append for vectors (i.e. lists of a certain length)" as a warm-up exercise. This is, however, much more difficult than the analogous theorem for lists because we get different types on the two sides of the equality. (Daniel managed to prove this using JMeq.)
-
Proof by reflection and SSReflect
-
Writing tactics (proof automation)
-
Ltac (“not the most beautiful part of Coq”)
http://adam.chlipala.net/cpdt/cpdt.pdf#chapter.14
Nisse recommended going deep into Ltac with Chlipala's book if we have the time. (Which we should, getting the proof of normalization of the simply-typed lambda calculus using logical relations should be easy).
-
Mtac (typed tactic programming)
-
-
Generic programming
-
Beyond PLT, handling traditional mathematics in Coq
- Irrationality of the square root of two (Cocorico!)
- GeoCoq - "A formalization of foundations of geometry in Coq"
- Elementary real analysis? Work in e.g. topology and related has been done in HOL Light at least.
- The Mathematical Components project? E.g. infinitude of primes (proof).
-
Program extraction
- Covered in one chapter in SF, but more info in Extraction in VFA
- Examples with simple programs?
- Efficiency of extracted programs?
- Coq.io
- Any formal guarantees on extracted programs or are they simply pretty-printed?
-
Large proof projects
- CompCert
- Formalized mathematics (four color theorem often mentioned)
-
Abus de notation: Type classes/Canonical structures/Coercions/Unification hints/Mooooooonads
- TODO: Good documentation for this? Exercises?
-
Matthieu Sozeau's Program tactics and Equations plugin
- TODO: Good documentation for this? Exercises?
-
See also the links/books/references in the README