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?