Ltac: do something different in each goal

Question

I've got a proof script where I'm exploring multiple cases, and it's currently quite slow, since I have a number of strategies for solving the goals, and I'm trying each one in each case.

I know that I need to apply certain tactics in certain cases, but I'm unsure of how to do this.

Here's what I have now:

induction e;
    intros;
    pose (bool_dec (is_v_of_expr e1)) as ve1; destruct ve1;
    [> thing1 | thing 2].

which gives the error Incorrect number of goals (expected 26 tactics, was given 2).

I'm trying to do thing1 in the first goal from destruct and thing2 in the second goal from destruct, for each case generated by induction.

The problem is, induction generates 13 subgoals, each of which gets split into 2 by destruct. The local selector [> thing1 | thing2 ] is trying to match all subgoals, not just the ones produced by the particular destruct.

How can I sequence the tactics, so that destruct is run on each case generated by induction, then thing1 is run on the first destruct-generated goal, and thing2 is run on the second generated goal, for each induction case.

Answer 1

You have two problems: (1) semicolons are left-associative by default, and (2) the [> ] syntax applies to all focused goals, rather than only the ones produced by the previous tactic. (As pointed out by Jason, this explanation isn't right, but the answer still works :)

You can solve these problems by changing [> ] to [ ] and right-associating the semicolons with parentheses:

Goal ((True /\ True) /\ (True /\ True) /\ (True /\ True)).
  Fail (split; [|split]); split; [> exact I | exact I].
  (split; [|split]); (split; [exact I | exact I]).
Qed.

In your example:

induction e; intros;
  pose (bool_dec (is_v_of_expr e1)) as ve1;
  (destruct ve1; [thing1 | thing 2]).