The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Dear Hugo,

yes. This I needed.

Thank you very much for help and especially for explanation of practical
work of apply tactic.

Greetings,

Marko Malikovi�

> 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
>> -----------------------------
>>
>


-----------------------
Dr. Sc. Marko Malikovi�
Filozofski fakultet
Sveu�ili�te u Rijeci
---------------------
Ph.D. Marko Malikovi�
Faculty of Arts and Sciences
University of Rijeka, Croatia
-----------------------------