List of other pages stored on this Wiki.
Coq Pearls
QuickSort: an implementation of quicksort in Coq.
InductiveFiniteTypes or alternatively FixpointFiniteTypes.
An other version of InductiveFiniteTypes not using nat.
ListOfPredecessors for binary numbers.
A proof of Lagrange's Theorem.
A proof that there are not finitely many primes.
SquareRootTwo: A very short proof that the square root of 2 is non rational.
UntypedLambdaTerms: various data structures for implementing the untyped lambda calculus in Coq.
ExistsFromPropToSet: Existential implies Sigma for decidable properties on nat.
HandMul: A fun way of doing multiplication by hand
Math Classes: Mathematics using TypeClasses
Discussion
A discussion about Coq Style.
A discussion suggesting preferring Set to Prop.
What is the difference between Require Import and Require Export?
Do objects living in Prop ever need to be evaluated? See PropsGuardingIotaReduction.
A discussion about intensional equality.
How should I organize large inductive proofs?
How can use the module system effectively?
Threads to remove
Another QuickSort: an implementation of quicksort in Coq using Program and definitions from the standard library.
Information about Coq's source code.
How do TypeClasses work?
How can I input unicode characters for Coq independently of my editor using XCompose (X graphical servers only) or the TeX input method (Unix systems).
How can I avoid non-instantiated existential variables with eauto?
What exactly does simpl do?
How can I make Coq always print universes?
Threads to update/remove
How does the pattern match syntax work?
How does dependent inversion work?
When using eapply, how can I instantiate the question marks?
Why doesn't Coq support extension equality? (Why can't I prove forall x, f x = g x) -> f = g?)
Why can I eliminate False (a Prop) when constructing a member of Set?
How does the fix tactic work?
Why do I get "Error: Abstracting over the term ... leads to a term which is ill-typed" when rewriting with equalities?
Where can I see other examples of formalization and verification?