• OldFront

Cocorico Main Page (V2)

High-Level Advice and Guidance

• Beginners Video Tutorials by Andrej Bauer

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

• How can I get better Performance out of Coq?

• What hints can you give me about Extraction of OCaml/Haskell/Scheme code?

• How can I do induction with self defined cases ?

• How do TypeClasses work?

• How do ImplicitArguments 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 build the CoqIDE under Mac OS X without X11

Community

• Who is using Coq in their programming languages research?

• Who is using Coq for the formalization of mathematics?

• How is Coq being taught and used to teach?

• HowToContributeToTheStandardLibrary?

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?

• Why do I get "Error: Abstracting over the term ... leads to a term which is ill-typed" when rewriting with equalities?

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

• Automatically cleaning your hypothesis like in linear programming (contains also an example of a way to have list of hypothesis in a custom tactic)

• A simple example of a tactic written in OCaml

• Unfold a fixpoint once (in OCaml)

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

• Monads in Coq

• A short tutorial on extraction

• Math Classes: Mathematics using TypeClasses

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

• How to deal with multiple coq binaries and path settings

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

Cocorico Main Page (V1)

This site is a WikiWikiWeb dedicated to the Coq proof assistant.