what's the correct usage for Coq "local application of tactics"?

Question

I'm reading Coq reference manual (8.5p1) about

Local application of tactics

Different tactics can be applied to the different goals using the following form:

[ > expr1 | ::: | exprn ]

The expressions expri are evaluated to vi, for i = 0; ...; n and all have to be tactics. The vi is applied to the i-th goal, for = 1; ...; n. It fails if the number of focused goals is not exactly n.

So I did a little test with two goals trying to apply two trivial idtac tactics to each, as follows:

Goal forall P Q: Prop, P \/ Q -> Q \/ P.
intros. destruct H. [ >  idtac | idtac  ].

However, I got an error telling me that only one tactic is expected:

Error: Incorrect number of goals (expected 1 tactic).

I'm confused. Can some one explain what I did wrong, and what's the correct usage?

Answer 1

The key part here is

It fails if the number of focused goals is not exactly n.

You need 2 focused goals. The number of focused goals can be checked like this:

Ltac print_numgoals := let n := numgoals in idtac "# of goals:" n.

Goal forall P Q: Prop, P \/ Q -> Q \/ P.
  intros. destruct H.
  print_numgoals.  (* prints 1 *)

There is a number of ways of getting several focused goals:

(1) Using sequencing: destruct H; [> idtac | idtac].

(2) Or slightly shorter: destruct H; [> idtac ..].

(3) Using the all selector (see the manual, §8.1):

destruct H. all: [ > id_tac | id_tac ].

In this last case, destruct H. all: print_numgoals. prints 2.

In conclusion, the following should be mentioned -- it seems that local application of tactics in that exact form ([ > ...]) is not very useful, because it is never used in the standard library (and several other libraries) and there are no mentions of it in the manual, except for the section devoted to this feature. Its version of the form expr; [ expr_1 | ... | expr_n] seems to be the most useful.