feature request: applying tactics to multiple subgoals

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#1805
From: @amccreight
Reported version: trunk
CC: @silene, @pirbo

[coqbot]

Comment author: @amccreight

Currently, the grammar rule for tactic invocations is this (from the manual):

tactic_invocation ::=
| num : tactic .
| tactic .

It would be nice if there could be a slightly more general form of the first case that allows multiple numbers. So for instance you could do something like:
1, 3, 7: auto.
or maybe
1 3 7: auto.

and then it would invoke auto on the 1st, 3rd and 7th subgoals.

Something like that would be handy, especially if the order the numbers are presented it is the order that the tactic is applied to the various subgoals. This can be very useful when solving a particular subgoal instantiates existential variables, which in turn allows other cases to be solved.

[coqbot]

Comment author: @pirbo

It is in the plan of Arnaud but the release date is not for now...

[coqbot]

Comment author: @aspiwack

In the current trunk (since r16967-r17038), we have
all: tactic
which can apply a tactic to all the focused subgoals. There is no fine-grain selection yet. But it can certainly be done.

The exact semantics is not entirely clear, though: for tactic which do not solve the goal, where should the new subgoals be in the goal list? If the tactic manipulates the goals separately, we can imagine having each goal replaced by the corresponding list of subgoals. But that would preclude having multiple goal tactics called this way.

[coqbot]

Comment author: @JasonGross

In trunk, you can do things like:

Goal True /\ True.
split.
1,2:constructor.

Goal True /\ True.
split.
1-2:constructor.

Though the syntax might change soon. I'm considering this wish granted.