The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

In fact, this is basically what is done in Agda (for example), where you build all the proof terms without tactics.

Kris

On Mon, Oct 7, 2013 at 2:13 AM, t x <txrev319 AT gmail.com> wrote:

Ah, that's right, all the tactics are just to help me build an _expression_ of a certain type.

Thanks! :-)

On Sun, Oct 6, 2013 at 9:50 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

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!