The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

The "<num>:<tactic>" syntax makes it possible to apply a tactic to a
specific subgoal; for example:

  3:simpl.

Is there a version of this which applies a tactic to all subgoals?  I
tried the obvious

  *:simpl.

But that's not valid syntax.

The case where this matters most (to me, at least) is when an [Instance]
declaration using the { ; ; } syntax generates a large number of
subgoals which can all be discharged with the same tactic; for example

  Instance foo : bar :=
  { baz := blah
  }.
  (* many obligations remain here *)

In the past I've rewritten this sort of thing as

  Instance foo : bar.
    apply Build_bar with (baz:=blah)
    ; magical_tactic.
    Defined.

But that's probably not the ideal way to go about this and is a bit less
pleasant for people reading the proof.

I suppose I could also use [Program Instance] and [Solve All Obligations
using]; I'm just wondering if there's another solution.

Thanks,

  - a