The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

In trunk, as it happens, I've implemented the "+" tactical which does precisely what you want (instead of using (t1 || t2) you can use (t1+t2).

If trunk is not an option for you, in the meantime, you can encode backtracking by continuation passing style, as suggested by Justus Matthiesen (though match is not necessary for that, first or || would be quite fine too). Or, indeed, use eauto whenever it's practical.

On 9 February 2014 15:35, Jonas Oberhauser <s9joober AT gmail.com> wrote:

I'm trying to automatize the following (ugly) lemma in the attached proof:


Goal (MCDC (fun s => s = s1 \/ s = s2 \/ s = s3 \/ s = s4 \/ s = s5 \/ s = s6) (fun g => g = f)).
hnf.
simpl.
intros [] g eq ; subst.
 exists s1 ; exists s6 ;
      simpl ; intuition ; try discriminate ;
      destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
 exists s1 ; exists s6 ;
      simpl ; intuition ; try discriminate ;
      destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
 exists s1 ; exists s5 ;
      simpl ; intuition ; try discriminate ;
      destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
 exists s1 ; exists s5 ;
      simpl ; intuition ; try discriminate ;
      destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
 exists s1 ; exists s4 ;
      simpl ; intuition ; try discriminate ;
      destruct y ; try (exfalso ; now apply H) ; compute ; intuition.
Qed.


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.
How can I automatize the script such that I don't have to find the instances for the exists by hand?

Kind regards, Jonas