Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
List of other pages stored on this Wiki.
- QuickSort: an implementation of quicksort in Coq.
- Another QuickSort: an implementation of quicksort in Coq using Program and definitions from the standard library.
- InductiveFiniteTypes or alternatively FixpointFiniteTypes.
- An other version of InductiveFiniteTypes not using nat.
- ListOfPredecessors for binary numbers.
- 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
- 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
- How do I change the Proof General Error Color?
- I'm using Proof General. Where did my proof state go?
- 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 update/remove
High-Level Advice and Guidance
- Beginners Video Tutorials by Andrej Bauer
- How do I do mutual induction?
- How do I do induction over a type containing pairs?
- 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 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?
Language Constructs and Built-In Tactics
- How can I avoid non-instantiated existential variables with eauto?
- How does the pattern match syntax work?
- How does dependent inversion work?
- 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?
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)