coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Instantiations with apply - impossible to unify, Michael
- <Possible follow-ups>
- Re: Re: [Coq-Club] Instantiations with apply - impossible to unify, Michael
Archive powered by MhonArc 2.6.16.