The Coq mailing list

[t x <txrev319 AT gmail.com>]

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!