The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 02/09/2014 12:07 PM, Justus Matthiesen wrote:
> > 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]).
>    

There's no need to implement the backtracking afresh with Ltac.  [eauto] 
already does everything you need.


Hint Extern 1 False => discriminate.

Hint Extern 1 (_ \/ _) => progress unfold update;
  repeat match goal with
           | [ |- context[if ?E then _ else _] ] => destruct E; subst; 
try discriminate; try tauto
         end.

Goal (MCDC (fun s => s = s1 \/ s = s2 \/ s = s3 \/ s = s4 \/ s = s5 \/ s 
= s6) (fun g => g = f)).
  hnf; destruct x; intros; subst; simpl; eauto 20.
Qed.