The Coq mailing list

[Justus Matthiesen <justus.matthiesen AT cl.cam.ac.uk>]

> I was trying something along the lines of
> (exists s1 || exists s2 || exists s3) ; (exists s4 || exists s5 ||
> exists s6) ; (simpl ; .... ; intuition).
> 
> However, since all the exist commands on their own will go through and
> the "stuckedness" is only discovered much later in the tactic, || does
> not work.

You need backtracking to implement the above. Fortunately(?), Ltac's pattern 
matching has a backtracking semantics (c.f. [1]).

So here's one approach:

  Ltac explode tac :=
    match goal with
    | _ => exists s1; now tac
    | _ => exists s2; now tac
    | _ => exists s3; now tac
    | _ => exists s4; now tac
    | _ => exists s5; now tac
    | _ => exists s6; now tac
    end.

  Ltac n_explode n tac :=
    match n with
    | O    => now tac
    | S ?n => explode ltac:(idtac; n_explode n tac)
    end.

Later, you can invoke the tactic via

  n_explode 2 ltac:(simpl; ... ; intuition).


Best wishes,
Justus


[1] http://coq.inria.fr/refman/Reference-Manual011.html#sec459