The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

Hello list,

I'm trying to define (using Ltac) a tactic that would be to "eapply"
what "lapply" is to "apply", or in other terms a tactic for forward
reasoning that can guess subexpressions involved, "eapply"-style.

Consider for instance the goal:

         H: forall x y, A x y -> B x y -> C x y -> D x y
         H1: A foo bar
         H2: B foo bar
         --------------------------------------------------
         G

The tactic I'm looking for, say, "elapply H", should produce the four goals

         A ?1 ?2
         B ?1 ?2
         C ?1 ?2
         D ?1 ?2 -> G

so that "elapply H; eauto" would leave the two goals

         C foo bar
         D foo bar -> G

That would be very useful in the kind of proofs (simulation arguments)
that I'm currently doing.

My first attempt was to define

   Ltac elapply x := eapply modusponens; [eapply x | idtac]

where

   Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q.

The "eapply modusponens" part generates the two expected goals

         ?3
         ?3 -> G

and for some simple theorems T, the "eapply T" succeeds in instantiating ?3
to the conclusion of T and generate fresh ? variables for the
parameters.  So, it sometimes works.

However, for more complex theorems T -- e.g. those I'm interested in :-( --
the "eapply T" fails with the mysterious error message:

         User error: execute: found a non-instanciated goal

So, I'm stuck.  Any suggestions on how to define a tactic like "elapply" ?

Cheers,

- Xavier Leroy