Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Instantiations with apply - impossible to unify

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Instantiations with apply - impossible to unify


chronological Thread 
  • From: Michael<michaelschausten AT googlemail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Instantiations with apply - impossible to unify
  • Date: Sun, 4 Jul 2010 14:59:18 +0200

Hello,

I started out trying to prove the following Lemma:
1 <= asr 1000 5 (* arithmetic right shift of 1000 by 5 bits *)

I created to Lemmas which I assume:

Lemma asr_1:
 forall (x: Z),
 x >= 1 -> asr x 1 = x/2.
Admitted.

Lemma asr_2:
 forall (x y z: Z),
 x >= 1 -> asr x (y + z) = asr (asr x y) z.
Admitted.

Now I would like to prove the first Lemma using asr_1 and asr_2. I started out
with:

Lemma test1:
 1 <= asr 1000 5.
Proof.
 apply asr_2 with (x:=1000) (y:=1) (z:=4).
Save.

This, however, gives me the error:
Impossible to unify "asr 1000 (1+4) = asr (asr 1000 1) 4" with "1 <= asr 10000
5)". How can I apply the Lemmas to solve "test1"?

Sincerely,
Michael



Archive powered by MhonArc 2.6.16.

Top of Page