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: