8

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.

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
thor
  • 21,418
  • 31
  • 87
  • 173
  • 4
    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. – Konstantin Weitz Sep 20 '15 at 19:08

1 Answers1

8

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.

Vinz
  • 5,997
  • 1
  • 31
  • 52
  • `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. – Clément Oct 10 '15 at 00:29
  • 2
    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. – Vinz Oct 11 '15 at 09:05
  • 2
    Ah, dependent types would use a lot of `revert`ing, indeed :) `rewrite` is indeed often just an application of an inductive principle, but I virtually never use that. – Clément Oct 13 '15 at 03:28
  • @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`. – Anton Trunov Sep 24 '17 at 08:12
  • @AntonTrunov Indeed. I did mention setoids in my original comment; thanks for adding the note about one_constructor! – Clément Sep 24 '17 at 13:46