Is there a minimal complete set of tactics in Coq?

问题:

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.

回答1:

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.