OtherContents - rocq-prover/rocq GitHub Wiki
List of other pages stored on this Wiki.
Coq Pearls
- 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.
- 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
Proof-General tips
- How do I change the Proof General Error Color?
- I'm using Proof General. Where did my proof state go?
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 update/remove
- Where can I see other examples of formalization and verification?
- Project ideas
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
Community
- Who is using Coq in their programming languages research?
- Who is using Coq for the formalization of mathematics?
- HowToContributeToTheStandardLibrary?
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
- 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)