High-Level Advice and Guidance

• How do I do mutual induction?

• How should I organize large inductive proofs?

• How do I do induction over a type containing pairs?

• Where else can I learn about Coq?

• Where can I read research papers about Coq's theoretical foundations?

• How can use the module system effectively?

• What tools and tactic packages are available for Coq?

• Where can I learn about proofs for languages with variable binding?

Community

• Who is using Coq in their programming languages research?

• How is Coq being taught and used to teach?

Language Constructs and Built-In Tactics

• What exactly does simpl do?

• How can I avoid non-instantiated existential variables with eauto?

• How does the pattern match syntax work?

• How does dependent inversion work?

• When using eapply, how can I instantiate the question marks?

• How can I make Coq always print universes?

• Why doesn't Coq support extension equality? (Why can't I prove forall x, f x = g x) -> f = g?)

• Why does Coq use inductive types and not W-Types?

• Why can I eliminate False (a Prop) when constructing a member of Set?

• How does the fix tactic work?

Some Useful Custom Tactics and Notation

• 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

• Haskell-like notation for list comprehension

Formal Developments and Coq Pearls

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

• QuickSort: an implementation of quicksort in Coq using Program.

• ExistsFromPropToSet: Existential implies Sigma for decidable properties on nat.

• HandMul: A fun way of doing multiplication by hand

• Where can I see other examples of formalization and verification?

Proof-General and CoqIDE Tips

• How do I change the Proof General Error Color?

• I'm using Proof General. Where did my proof state go?

• CoqIDE crashes in KDE. Help!

Meta

• Where is the old front page?

• Where can I learn about this wiki?

• How do I edit this wiki?

• Where did that old article go?