Is there a minimal complete set of tactics in Coq?

Question

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.

Taxexempt

Because of the Curry-Howard Isomorphism, every proof that you can construct with a tactic corresponds to some term. Thus, the exact tactic is sufficient to prove any goal. If you don't want to construct the term all at once, you can use refine instead. – Owe

Answer 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.

Unmeant

reflexivity is just apply eq_refl if you don't use setoids, and symmetry is an application too; exists is constructor, which in turn is just apply too. Do you often use revert? On the other hand, rewrite and simpl would probably be nice additions to this list. – Momentous

You could say the say about rewrite, it is just applying a lemma with the correct shape. As I said everything tumble down to refine (directly writing the proof term). But I admit, rewrite should be in the list. I use revert often, because I do a lot of induction with dependent types, where it helps a lot. – Unmeant

Ah, dependent types would use a lot of reverting, indeed :) rewrite is indeed often just an application of an inductive principle, but I virtually never use that. – Momentous

@Clément reflexivity works kind of like apply eq_refl only at first, if does not succeed it has several fall backs, like setoid_rewrite and one_constructor (a non-exposed tactic, which tries to find a proof term if the goal is a one-constructor inductive type). E.g. reflexivity solves a goal like True. – Steiger

@AntonTrunov Indeed. I did mention setoids in my original comment; thanks for adding the note about one_constructor! – Momentous