If you’re like me, one of the biggest shortcomings of the Coq ecosystem is the fairly complicated tactic reference documentation. It is exhaustive (which is better than lacking), but I have a few specific issues with it:
- Entries are too verbose. I usually don’t need an exhaustive explanation of what a tactic does.
- BNF grammar is not that easy to read. This one might be more controversial, but I would rather have examples of syntax.
- There are not enough examples of tactics being used, and the examples that do exist are too often not representative of what a beginner might see.
For these reasons, I’ve decided to compile a reference document of every tactic that I’ve ever used, addressing the problems above via the following solutions.
- Entries will be written at an undergraduate level, assuming a basic understanding of the Coq system. Sometimes, this will require reading the pages for other tactics before the one you really want to know about, but I think that’s a fair compromise. Explanations will focus on what configurations of goal states the tactic is useful or not useful for.
- Entries will start general and become more specific as one reads on. This will ensure minimal maintenance is necessary as tactics change over time.
- Entries will include syntax examples rather than BNF grammars.
- Entries will contain multiple examples, including goal states before and after executing the tactics. Small MRE Coq scripts may be included.
- As a fallback, links to other resources, at minimum the official documentation, will be included in each entry.
This guide doesn’t aim to replace the reference documentation, it aims to be a stepping stone into the reference documentation that reduces the apprehension of those new to Coq.
There are many other guides to Coq tactics, you should check them out too if I don’t have what you need: