The Coq FAQ
This FAQ is the sum of the questions that came to mind as we developed proofs in Coq. Since we are singularly short-minded, we wrote the answers we found on bits of papers to have them at hand whenever the situation occurs again. This is pretty much the result of that: a collection of tips one can refer to when proofs become intricate. Yes, this means we won't take the blame for the shortcomings of this FAQ. But if you want to contribute and send in your own question and answers, feel free to add your own contributions to this wiki.
- Presentation
- Documentation
- Installation
- Getting started
- The Logic of Coq
- Talkin' with the Rooster
- Inductive and Co-Inductive Types
- Syntax and Notations
- Ltac
- Typeclasses and Canonical Structures
- Case Studies
- Publishing Tools
- CoqIde
- Extraction
- Anti-patterns
- Setting up a development environment for working on Coq
- Tactics Written in OCaml
- Glossary
- Troubleshooting
- More questions
Use the dpdusage tool which comes with the coq-dpdgraph plugin.
- Should I put my type in Prop_or_Set?
- How does the MatchAsInReturn syntax work?
- Why can't I prove
(forall x, f x = g x) -> f = g? See extensional_equality. - Isn't IntensionalEquality useless?
- How do I get DependentInversion to work in my case?
- Why not WTypeInsteadOfInductiveTypes?
- Do objects living in
Propever need to be evaluated? See PropsGuardingIotaReduction. - When using
eapply, how can I instantiate the question marks i.e. the ExistentialVariablesInEapply? - CoqNewbieQuestions
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq 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.