OtherContents
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.
- 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
- 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?
- Where can I see other examples of formalization and verification?
- Project ideas
- 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?
- HowToContributeToTheStandardLibrary?
- 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?
- 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)
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.