The Coq mailing list

[Rodrigo Ribeiro <rodrigo AT decsi.ufop.br>]

Hi Marcus,

I have not tested your code, but it seems that using destruct (foo1 _ _ H) as [H1 | H2], should work.

Regards.

Rodrigo

On Thu, Jun 26, 2014 at 7:18 AM, Marcus Ramos <marcus.ramos AT univasf.edu.br> wrote:

Hi,

This should be obvious, but still I can´t see why it doesn´t work. In the script:

Lemma foo1:

forall (i j: nat), i=j -> (forall p q: nat, p <= q \/ p > q).

Proof.

Admitted.

Lemma foo2:

forall (m n: nat),

m = n -> n = m.

Proof.

intros m n H.

apply foo1 in H.

Why does the "apply foo1 in H" above causes the folowing error message to be displayed?

"Error: Unable to find an instance for the variables p, q."

Shouldn´t it just place (forall p q: nat, p <= q \/ p > q) in the context as a new hypothesis? If I execute, for example, apply foo1 with (p:=0)(q:=1) in H, I get H : 0 <= 1 \/ 0 > 1, but this is not what I want.

Thanks,

Marcus.