I have seen a lot of Coq tactics that are overlapping each other in function.
For example, when you have the exact conclusion in the hypothesis, you can use assumption
, apply
, exact
, trivial
, and maybe others. Other examples include destruct
and induction
for non-inductive types(??).
My question is:
Is there a minimal set of basic tactics (that excludes auto
, and its like) that is complete, in the sense that this set can be used to prove any Coq-provable theorems about functions of natural numbers?
The tactics in this minimal complete set would be ideally basic, so that each perform one (or two) function only and one can easily understand what it does.
A proof in Coq is just a term of the correct type. Tactics help you build these term by combining smaller sub-terms into more complex ones. Therefore, the minimal set of basic tactics would only contain the exact
tactic, as Konstantin mentioned.
The refine
tactics allows you to directly give proof terms, but with holes that will generated sub-goals. Basically any tactic is just an instance of the refine
tactic.
However, if you want to first consider only a minimal set of tactics, I would consider intro{s}
, exists
, reflexivity
, symmetry
, apply
, rewrite
, revert
, destruct
and induction
. inversion
might come in handy rather quickly too.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With