The Coq FAQ

Siddharth edited this page Jun 12, 2018 · 8 revisions

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.

  1. Presentation
  2. Documentation
  3. Installation
  4. The Logic of Coq
  5. Talkin' with the Rooster
  6. Inductive and Co-Inductive Types
  7. Syntax and Notations
  8. Ltac
  9. Tactics Written in OCaml
  10. Typeclasses and Canonical Structures
  11. Case Studies
  12. Publishing Tools
  13. CoqIde
  14. Extraction
  15. Glossary
  16. Troubleshooting
  17. More questions

More questions

How to find unused lemmas in a large development?

Use the dpdusage tool which comes with the coq-dpdgraph plugin.

Questions to move to the section they belong to

  1. Should I put my type in Prop_or_Set?
  2. How does the MatchAsInReturn syntax work?
  3. Why can't I prove (forall x, f x = g x) -> f = g? (see extensional_equality)
  4. Isn't IntensionalEquality useless?
  5. How do I get DependentInversion to work in my case?
  6. Why not WTypeInsteadOfInductiveTypes?
  7. Do objects living in Prop ever need to be evaluated? See PropsGuardingIotaReduction.
  8. When using eapply, how can I instantiate the question marks i.e. the ExistentialVariablesInEapply?
  9. CoqNewbieQuestions
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.