The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

I see what you mean. You would have expected that (P->Q) unifies with
(x=1->y=2) and Coq infers both P and Q.

In practise, "apply in" treats arguments right-to-left. So it first
tries to unify P and (x=1->y=2) which works. Then, because it is
"apply" and not "eapply" which is used, Coq detects that Q cannot be
inferred and fails ("eapply" would have set instead an existential
variables).

If you want your lemma to be used so that it gives |- P and Q |- R
from P -> Q |- R, you should instead use the following statement:

Axiom A : forall P Q : Prop, P -> (P -> Q) -> Q.

Hope it helps better,

Hugo

On Mon, May 10, 2010 at 01:07:22PM +0200, Marko Maliković wrote:
> OK, "apply A with (Q := (y=3)) in H" also work. But result of this tactic
> is confusing me. What seems unnatural for me is that in the same (second)
> subgoal Coq once replaced Q by y = 2, and the other with y = 3:
> 
> H : x = 1 -> y = 2
> ============================
>  (x = 1 -> y = 2) -> y = 3
> 
> Marko Maliković
> 
> > You could have said as well "apply A with (Q := (y=3)) in H" and it
> > would have worked, what shows that there is indeed no instance for Q
> > that Coq could infer.
> >
> > Hope it helps.
> >
> > Hugo Herbelin
> >
> 
> -----------------------
> Dr. Sc. Marko Maliković
> Filozofski fakultet
> Sveučilište u Rijeci
> ---------------------
> Ph.D. Marko Maliković
> Faculty of Arts and Sciences
> University of Rijeka, Croatia
> -----------------------------
>