Commit 6b0839fa by MARCHE Claude

### Continued proofs in bitvectors example. Only 3 basic lemmas on

`pow2, div and mod missing`
parent 773f4802
 ... ... @@ -345,9 +345,8 @@ theory BitVector lemma nth_from_int2c_0: forall i:int. size > i >= 0 -> nth (from_int2c 0) i = False lemma nth_from_int2c_plus_pow2: forall x k i:int. 0 <= k < i -> forall x k i:int. 0 <= k < i /\ k < size-1 -> nth (from_int2c (x+pow2 i)) k = nth (from_int2c x) k end ... ...
 ... ... @@ -163,6 +163,15 @@ Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z). Axiom Mod_pow2 : forall (x:Z) (i:Z), ((int.EuclideanDivision.mod1 (x + (pow2 i))%Z 2%Z) = (int.EuclideanDivision.mod1 x 2%Z)). Axiom Mod_pow2_gen : forall (x:Z) (i:Z) (k:Z), ((0%Z <= k)%Z /\ (k < i)%Z) -> ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div (x + (pow2 i))%Z (pow2 k)) 2%Z) = (int.EuclideanDivision.mod1 (int.EuclideanDivision.div x (pow2 k)) 2%Z)). Parameter size: Z. Axiom size_positive : (1%Z < size)%Z. ... ... @@ -338,31 +347,23 @@ Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. (* Why3 goal *) Theorem nth_from_int2c_plus_pow2 : forall (x:Z) (k:Z) (i:Z), ((0%Z <= k)%Z /\ (k < i)%Z) -> ((nth (from_int2c (x + (pow2 i))%Z) k) = (nth (from_int2c x) k)). intros x k i (h1 & h2). generalize i h1 h2. pattern k; apply Z_lt_induction; auto. clear k i h1 h2. intros k Hind i Hk Hki. assert (h: k = 0 \/ k > 0) by omega. destruct h. Theorem nth_from_int2c_plus_pow2 : forall (x:Z) (k:Z) (i:Z), (((0%Z <= k)%Z /\ (k < i)%Z) /\ (k < (size - 1%Z)%Z)%Z) -> ((nth (from_int2c (x + (pow2 i))%Z) k) = (nth (from_int2c x) k)). (*case k = 0*) subst k. assert (h: nth (from_int2c (x)) 0 = true \/ nth (from_int2c (x)) 0 = false). destruct (nth (from_int2c (x)) 0);auto. intros x k i (h1 & h2). assert (h: int.EuclideanDivision.mod1 (int.EuclideanDivision.div x (pow2 k)) 2 = 0 \/ int.EuclideanDivision.mod1 (int.EuclideanDivision.div x (pow2 k)) 2 <> 0) by omega. destruct h. rewrite H. apply nth_from_int2c_low_odd. rewrite Mod_pow2. (*case k >0*) rewrite nth_from_int2c_high_even; intuition. rewrite nth_from_int2c_high_even; intuition. rewrite Mod_pow2_gen; auto. rewrite nth_from_int2c_high_odd. rewrite nth_from_int2c_high_odd; intuition. split; auto with zarith. rewrite Mod_pow2_gen; auto. Qed.
This diff is collapsed.
 ... ... @@ -47,7 +47,7 @@ name="nth_one1" locfile="bitvectors/double/../double.why" loclnum="73" loccnumb="8" loccnume="16" sum="3848d3fd3fbc40c879e047aaab4a85a2" sum="1de7d115c0c2e47b0f7c904ae25676bb" proved="true" expanded="false" shape="ainfix =anthaoneV0aFalseIainfix <=V0c51Aainfix <=c0V0F"> ... ... @@ -57,14 +57,14 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -74,14 +74,14 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -91,14 +91,14 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -124,7 +124,7 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -157,7 +157,7 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -183,7 +183,7 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -224,7 +224,7 @@ memlimit="1000" obsolete="false" archived="false">
This diff is collapsed.
This diff is collapsed.
 ... ... @@ -32,7 +32,7 @@ name="Nth_j" locfile="bitvectors/neg_as_xor/../neg_as_xor.why" loclnum="13" loccnumb="8" loccnume="13" sum="313f7cfd9cb238cefe6b30a61ef11c31" sum="d3063104903bdd668679f74cb5f68a13" proved="true" expanded="false" shape="ainfix =anthajV0aFalseIainfix <=V0c62Aainfix <=c0V0F"> ... ... @@ -42,14 +42,14 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -59,14 +59,14 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -76,7 +76,7 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -109,7 +109,7 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -158,14 +158,14 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -175,14 +175,14 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -199,7 +199,7 @@ name="Sign_of_xor_j" locfile="bitvectors/neg_as_xor/../neg_as_xor.why" loclnum="25" loccnumb="8" loccnume="21" sum="5c22f51afd72897f2722925bdf3ca2b0" sum="9174061a363d9c2b808fff999dd1c00d" proved="true" expanded="false" shape="ainfix =asignabw_xorV0ajanotbasignV0F"> ... ... @@ -232,7 +232,7 @@ name="Exp_of_xor_j" locfile="bitvectors/neg_as_xor/../neg_as_xor.why" loclnum="27" loccnumb="8" loccnume="20" sum="ccbeb8d697184227f9f75d9bacb2a039" sum="f86ab36765de5476dc2c4e7364803681" proved="true" expanded="false" shape="ainfix =aexpabw_xorV0ajaexpV0F"> ... ... @@ -242,7 +242,7 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -275,7 +275,7 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -308,7 +308,7 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -341,14 +341,14 @@ memlimit="1000" obsolete="false" archived="false"> ... ... @@ -359,7 +359,7 @@ edited="neg_as_xor_TestNegAsXOR_MainResult_1.v" obsolete="false" archived="false"> ... ...
 ... ... @@ -89,6 +89,11 @@ theory Pow2int lemma Div_pow2: forall x i:int. -pow2 i <= x < -pow2 (i-1) -> div x (pow2 (i-1)) = -2 (* lemma Mod_pow2: forall x i:int. mod (x + pow2 i) 2 = mod x 2 *) lemma Mod_pow2_gen: forall x i k :int. 0 <= k < i -> mod (div (x + pow2 i) (pow2 k)) 2 = mod (div x (pow2 k)) 2 end ... ...
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!