OtherContents

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.
• ExcludedMiddleOnNegativeFormulasFromCoqRealAxioms
• A proof of Lagrange's Theorem.
• 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
• Monads in Coq
• A short tutorial on extraction
• Math Classes: Mathematics using Type Classes
• Tactic pearls

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 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.
• How can I build the CoqIDE under Mac OS X without X11
• 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).
• HowToContributeToTheStandardLibrary?
• How can I avoid non-instantiated existential variables with eauto?

Threads to update/remove

• Resources for Coq Newbies
• 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?)
• Where can I see other examples of formalization and verification?
• Project ideas