Clone this wiki locally
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
- 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?
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
- 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
ExistsFromPropToSet: Existential implies Sigma for decidable properties on
- 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!
- 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.