The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You don't actually need any tactics; you can do anything with only [Definition.]  Alternatively, your minimal set of tactics is {[exact]}.

-Jason

On Monday, October 7, 2013, t x wrote:

Hi,

  Let $S$ be a "minimal" set of tactics, if (1) any proposition provable in Coq can be proved using only $S$ and (2) removing a tactic from $S$ makes (1) false.

  My question: is "pattern at, apply, cbv, inversion, assert, f_equal, unfold, fold" enough?

  For example:

    replace _ with _ ==> assert( _ = _ ) + rewrite ...

    rewrite ==> pattern at ....  + f_equal

    simpl ==> cbv ...

    destruct ==> inversion

  This leads me to believe that the above is sufficient. However, is it "minimal", or we can remove some more from it?

Thanks!