Bitvector: improved lemmas

examples/bitvectors/bitvector/bitvector_BitVector_nth_from_int2c_plus_pow2_1.v

-(* This file is generated by Why3's Coq driver *)
+(* This file is generated by Why3's Coq 8.4 driver *)
 (* Beware! Only edit allowed sections below    *)
-Require Import ZArith.
-Require Import Rbase.
+Require Import BuiltIn.
+Require Import ZOdiv.
+Require BuiltIn.
+Require bool.Bool.
 Require int.Int.
 Require int.Abs.
-Require int.EuclideanDivision.
-
-(* Why3 assumption *)
-Definition implb(x:bool) (y:bool): bool := match (x,
-  y) with
-  | (true, false) => false
-  | (_, _) => true
-  end.
+Require int.ComputerDivision.
 
 Parameter pow2: Z -> Z.
 
@@ -156,27 +151,22 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z).
 Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z).
 
 Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\
-  (x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x
-  (pow2 (i - 1%Z)%Z)) = 1%Z).
+  (x < (pow2 i))%Z) -> ((ZOdiv x (pow2 (i - 1%Z)%Z)) = 1%Z).
 
 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)).
+  (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) ->
+  ((ZOdiv x (pow2 (i - 1%Z)%Z)) = (-2%Z)%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)).
+  ((ZOmod (ZOdiv (x + (pow2 i))%Z (pow2 k)) 2%Z) = (ZOmod (ZOdiv x (pow2 k)) 2%Z)).
 
 Parameter size: Z.
 
 Axiom size_positive : (1%Z < size)%Z.
 
-Parameter bv : Type.
+Axiom bv : Type.
+Parameter bv_WhyType : WhyType bv.
+Existing Instance bv_WhyType.
 
 Parameter nth: bv -> Z -> bool.
 
@@ -191,7 +181,7 @@ Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone
   n) = true).
 
 (* Why3 assumption *)
-Definition eq(v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
+Definition eq (v1:bv) (v2:bv): Prop := forall (n:Z), ((0%Z <= n)%Z /\
   (n < size)%Z) -> ((nth v1 n) = (nth v2 n)).
 
 Axiom extensionality : forall (v1:bv) (v2:bv), (eq v1 v2) -> (v1 = v2).
@@ -297,19 +287,18 @@ Axiom to_nat_sub_footprint : forall (b1:bv) (b2:bv) (j:Z) (i:Z),
 Parameter from_int: Z -> bv.
 
 Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i < size)%Z /\
-  (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n
-  (pow2 i)) 2%Z) = 0%Z)) -> ((nth (from_int n) i) = false).
+  (0%Z <= i)%Z) /\ ((ZOmod (ZOdiv n (pow2 i)) 2%Z) = 0%Z)) ->
+  ((nth (from_int n) i) = false).
 
 Axiom nth_from_int_high_odd : forall (n:Z) (i:Z), (((i < size)%Z /\
-  (0%Z <= i)%Z) /\
-  ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
-  2%Z) = 0%Z)) -> ((nth (from_int n) i) = true).
+  (0%Z <= i)%Z) /\ ~ ((ZOmod (ZOdiv n (pow2 i)) 2%Z) = 0%Z)) ->
+  ((nth (from_int n) i) = true).
 
-Axiom nth_from_int_low_even : forall (n:Z), ((int.EuclideanDivision.mod1 n
-  2%Z) = 0%Z) -> ((nth (from_int n) 0%Z) = false).
+Axiom nth_from_int_low_even : forall (n:Z), ((ZOmod n 2%Z) = 0%Z) ->
+  ((nth (from_int n) 0%Z) = false).
 
-Axiom nth_from_int_low_odd : forall (n:Z), (~ ((int.EuclideanDivision.mod1 n
-  2%Z) = 0%Z)) -> ((nth (from_int n) 0%Z) = true).
+Axiom nth_from_int_low_odd : forall (n:Z), (~ ((ZOmod n 2%Z) = 0%Z)) ->
+  ((nth (from_int n) 0%Z) = true).
 
 Axiom nth_from_int_0 : forall (i:Z), ((i < size)%Z /\ (0%Z <= i)%Z) ->
   ((nth (from_int 0%Z) i) = false).
@@ -324,20 +313,19 @@ Axiom nth_sign_negative : forall (n:Z), (n < 0%Z)%Z -> ((nth (from_int2c n)
 
 Axiom nth_from_int2c_high_even : forall (n:Z) (i:Z),
   (((i < (size - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
-  ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
-  2%Z) = 0%Z)) -> ((nth (from_int2c n) i) = false).
+  ((ZOmod (ZOdiv n (pow2 i)) 2%Z) = 0%Z)) -> ((nth (from_int2c n)
+  i) = false).
 
 Axiom nth_from_int2c_high_odd : forall (n:Z) (i:Z),
   (((i < (size - 1%Z)%Z)%Z /\ (0%Z <= i)%Z) /\
-  ~ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n (pow2 i))
-  2%Z) = 0%Z)) -> ((nth (from_int2c n) i) = true).
+  ~ ((ZOmod (ZOdiv n (pow2 i)) 2%Z) = 0%Z)) -> ((nth (from_int2c n)
+  i) = true).
 
-Axiom nth_from_int2c_low_even : forall (n:Z), ((int.EuclideanDivision.mod1 n
-  2%Z) = 0%Z) -> ((nth (from_int2c n) 0%Z) = false).
+Axiom nth_from_int2c_low_even : forall (n:Z), ((ZOmod n 2%Z) = 0%Z) ->
+  ((nth (from_int2c n) 0%Z) = false).
 
-Axiom nth_from_int2c_low_odd : forall (n:Z),
-  (~ ((int.EuclideanDivision.mod1 n 2%Z) = 0%Z)) -> ((nth (from_int2c n)
-  0%Z) = true).
+Axiom nth_from_int2c_low_odd : forall (n:Z), (~ ((ZOmod n 2%Z) = 0%Z)) ->
+  ((nth (from_int2c n) 0%Z) = true).
 
 Axiom nth_from_int2c_0 : forall (i:Z), ((i < size)%Z /\ (0%Z <= i)%Z) ->
   ((nth (from_int2c 0%Z) i) = false).
@@ -350,12 +338,12 @@ Ltac ae := why3 "alt-ergo" timelimit 3.
 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)).
+(* intros x k i ((h1,h2),h3). *)
 
 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.
+assert (h: ZOmod (ZOdiv x (pow2 k)) 2 = 0 \/
+           ZOmod (ZOdiv x (pow2 k)) 2 <> 0) 
+  by omega.
 destruct h.
 rewrite nth_from_int2c_high_even; intuition.
 rewrite nth_from_int2c_high_even; intuition.

examples/bitvectors/double/why3session.xml

@@ -20,7 +20,7 @@
  <prover
   id="4"
   name="Coq"
-  version="8.3pl4"/>
+  version="8.4"/>
  <prover
   id="5"
   name="Z3"
@@ -50,7 +50,7 @@
     name="nth_one1"
     locfile="../double.why"
     loclnum="73" loccnumb="8" loccnume="16"
-    sum="68b26f6bd21633cb2cb9250019b673f2"
+    sum="64b742f26230c95a6f017247e361064e"
     proved="true"
     expanded="true"
     shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c51Aainfix &lt;=c0V0F">
@@ -75,7 +75,7 @@
     name="nth_one2"
     locfile="../double.why"
     loclnum="74" loccnumb="8" loccnume="16"
-    sum="f08cb866a3ab9529aea096452c0c2aba"
+    sum="84a85185c5147202068cebe22848d18f"
     proved="true"
     expanded="true"
     shape="ainfix =anthaoneV0aTrueIainfix &lt;=V0c61Aainfix &lt;=c52V0F">
@@ -85,7 +85,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.56"/>
+     <result status="valid" time="0.75"/>
     </proof>
     <proof
      prover="1"
@@ -100,7 +100,7 @@
     name="nth_one3"
     locfile="../double.why"
     loclnum="75" loccnumb="8" loccnume="16"
-    sum="45f916af66fcd9ac376a27c68412cbea"
+    sum="3fa54a156946495d247aa0b4e5d2308b"
     proved="true"
     expanded="false"
     shape="ainfix =anthaoneV0aFalseIainfix &lt;=V0c63Aainfix &lt;=c62V0F">
@@ -110,14 +110,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.22"/>
+     <result status="valid" time="1.62"/>
     </proof>
    </goal>
    <goal
     name="sign_one"
     locfile="../double.why"
     loclnum="77" loccnumb="8" loccnume="16"
-    sum="ae26ebd49d4971fd05324b0e13322dd7"
+    sum="be9ca7041b727df4ca7493d2af0cd4c6"
     proved="true"
     expanded="false"
     shape="ainfix =asignaoneaFalse">
@@ -166,7 +166,7 @@
     name="exp_one"
     locfile="../double.why"
     loclnum="78" loccnumb="8" loccnume="15"
-    sum="df76b3cb3a441260a89d05f9f45d59fb"
+    sum="a95859f4aee7c4d050a5a4db5dd9c1fd"
     proved="true"
     expanded="false"
     shape="ainfix =aexpaonec1023">
@@ -176,7 +176,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.09"/>
+     <result status="valid" time="2.77"/>
     </proof>
     <proof
      prover="4"
@@ -185,14 +185,14 @@
      edited="double_TestDouble_exp_one_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="0.67"/>
+     <result status="valid" time="1.19"/>
     </proof>
    </goal>
    <goal
     name="mantissa_one"
     locfile="../double.why"
     loclnum="79" loccnumb="8" loccnume="20"
-    sum="fea308f93f031eb47ac1cca53b50bafd"
+    sum="1e2b71c93f02723b910f5b0520c73873"
     proved="true"
     expanded="false"
     shape="ainfix =amantissaaonec0">
@@ -225,7 +225,7 @@
     name="double_value_of_1"
     locfile="../double.why"
     loclnum="81" loccnumb="8" loccnume="25"
-    sum="5c567bd886a7249af1b84ee36fa83a02"
+    sum="ad540400343cee2ffb0b8a07d70165cf"
     proved="true"
     expanded="false"
     shape="ainfix =adouble_of_bv64aonec1.0">

examples/bitvectors/neg_as_xor/why3session.xml

@@ -12,7 +12,7 @@
  <prover
   id="2"
   name="Coq"
-  version="8.3pl4"/>
+  version="8.4"/>
  <prover
   id="3"
   name="Z3"
@@ -35,7 +35,7 @@
     name="Nth_j"
     locfile="../neg_as_xor.why"
     loclnum="13" loccnumb="8" loccnume="13"
-    sum="ffa7aadc98c7c81aa8afa142b455755d"
+    sum="34b383120a6c9582c26cf0005c710a92"
     proved="true"
     expanded="true"
     shape="ainfix =anthajV0aFalseIainfix &lt;=V0c62Aainfix &lt;=c0V0F">
@@ -45,7 +45,7 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.47"/>
+     <result status="valid" time="1.74"/>
     </proof>
     <proof
      prover="1"
@@ -60,7 +60,7 @@
     name="sign_of_j"
     locfile="../neg_as_xor.why"
     loclnum="15" loccnumb="8" loccnume="17"
-    sum="eff4aeb7674767da11cced006af36114"
+    sum="8874135905e94507fde3c62c691db581"
     proved="true"
     expanded="false"
     shape="ainfix =asignajaTrue">
@@ -70,14 +70,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="2.33"/>
+     <result status="valid" time="0.25"/>
     </proof>
    </goal>
    <goal
     name="mantissa_of_j"
     locfile="../neg_as_xor.why"
     loclnum="16" loccnumb="8" loccnume="21"
-    sum="2efb10e521eba776b7ece640f4473a5f"
+    sum="7a9b27b0536d17d854cf27f8234d761b"
     proved="true"
     expanded="false"
     shape="ainfix =amantissaajc0">
@@ -110,7 +110,7 @@
     name="exp_of_j"
     locfile="../neg_as_xor.why"
     loclnum="17" loccnumb="8" loccnume="16"
-    sum="fc87a20dea9a71534d543df10bf7ab7f"
+    sum="d30d723f5c789d43e3644685e0f09ad3"
     proved="true"
     expanded="false"
     shape="ainfix =aexpajc0">
@@ -136,14 +136,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="3.44"/>
+     <result status="valid" time="2.68"/>
     </proof>
    </goal>
    <goal
     name="int_of_bv"
     locfile="../neg_as_xor.why"
     loclnum="18" loccnumb="8" loccnume="17"
-    sum="23ea5b39ea99f819456d1b2e7e0344f2"
+    sum="a5352ad948c731bc7e1b1d044870bb95"
     proved="true"
     expanded="false"
     shape="ainfix =adouble_of_bv64ajc0.0">
@@ -176,7 +176,7 @@
     name="MainResultBits"
     locfile="../neg_as_xor.why"
     loclnum="20" loccnumb="8" loccnume="22"
-    sum="4707f538b9d68b3fa116ca0ad59aa071"
+    sum="52f645e44bf665a7bc0953d0ab22cbec"
     proved="true"
     expanded="false"
     shape="ainfix =anthabw_xorV0ajV1anthV0V1Iainfix &lt;V1c63Aainfix &lt;=c0V1FF">
@@ -193,7 +193,7 @@
     name="MainResultSign"
     locfile="../neg_as_xor.why"
     loclnum="23" loccnumb="8" loccnume="22"
-    sum="6352e7cd945029c87d1ea3a6482d4683"
+    sum="84408f58ca669e966ac3dd0e8e26c501"
     proved="true"
     expanded="false"
     shape="ainfix =anthabw_xorV0ajc63anotbanthV0c63F">
@@ -210,7 +210,7 @@
     name="Sign_of_xor_j"
     locfile="../neg_as_xor.why"
     loclnum="25" loccnumb="8" loccnume="21"
-    sum="44f96c656d009bca0b5dabe0f3343dd7"
+    sum="8e35e7b3978720fcffa4654f4d40a8bb"
     proved="true"
     expanded="false"
     shape="ainfix =asignabw_xorV0ajanotbasignV0F">
@@ -243,7 +243,7 @@
     name="Exp_of_xor_j"
     locfile="../neg_as_xor.why"
     loclnum="27" loccnumb="8" loccnume="20"
-    sum="4836861f99a9dc39ab00265e89154d00"
+    sum="bd2a20ad78883a9b246d819dfc050046"
     proved="true"
     expanded="false"
     shape="ainfix =aexpabw_xorV0ajaexpV0F">
@@ -276,7 +276,7 @@
     name="Mantissa_of_xor_j"
     locfile="../neg_as_xor.why"
     loclnum="29" loccnumb="8" loccnume="25"
-    sum="5662f7f7ef7b6f8e2d958c949cdb6b93"
+    sum="ce1ceaaaf0b5d079ac350e484e3a5051"
     proved="true"
     expanded="false"
     shape="ainfix =amantissaabw_xorV0ajamantissaV0F">
@@ -302,14 +302,14 @@
      memlimit="1000"
      obsolete="false"
      archived="false">
-     <result status="valid" time="3.43"/>
+     <result status="valid" time="2.92"/>
     </proof>
    </goal>
    <goal
     name="MainResultZero"
     locfile="../neg_as_xor.why"
     loclnum="31" loccnumb="8" loccnume="22"
-    sum="3218b62d0748383b9d38e4f71ffd6cb1"
+    sum="e71da47a4d26e5f9bb78680af2110e9d"
     proved="true"
     expanded="false"
     shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix =amantissaV0c0Aainfix =c0aexpV0F">
@@ -342,7 +342,7 @@
     name="sign_neg"
     locfile="../neg_as_xor.why"
     loclnum="34" loccnumb="8" loccnume="16"
-    sum="eb021a51368e1a70d9d38dcc3ade5616"
+    sum="1a8d522bc703c9be8a1629374fd9d762"
     proved="true"
     expanded="false"
     shape="ainfix =asign_valueanotbasignV0aprefix -.asign_valueasignV0F">
@@ -359,7 +359,7 @@
     name="MainResult"
     locfile="../neg_as_xor.why"
     loclnum="36" loccnumb="8" loccnume="18"
-    sum="3c4e973663d5b160e10c91d79275f1a9"
+    sum="172f68d15ea46e505257c40efb1e8b07"
     proved="true"
     expanded="true"
     shape="ainfix =adouble_of_bv64abw_xorV0ajaprefix -.adouble_of_bv64V0Iainfix &lt;aexpV0c2047Aainfix &lt;c0aexpV0F">
@@ -370,7 +370,7 @@
      edited="neg_as_xor_TestNegAsXOR_MainResult_1.v"
      obsolete="false"
      archived="false">
-     <result status="valid" time="1.04"/>
+     <result status="valid" time="1.70"/>
     </proof>
    </goal>
   </theory>

examples/bitvectors/power2.why

@@ -83,16 +83,51 @@ theory Pow2int
 
   use import int.EuclideanDivision
 
-  lemma Div_pow: forall x i:int. pow2 (i-1) <= x < pow2 i ->
-		 div x (pow2 (i-1)) = 1
+(*
+  lemma div_uniq:
+    forall x y q:int.
+      y > 0 /\ (exists r:int. x = q*y + r /\ 0 <= r < y) -> div x y = q
+
+  lemma mod_uniq:
+    forall x y r:int.
+      y > 0 /\ (exists q:int. x = q*y + r /\ 0 <= r < y) -> mod x y = r
+
+  lemma Div_double_aux:
+    forall x y:int. 0 < y <= x < 2*y -> 
+      x = 1*y+(x-y) /\ 0 <= x-y < y
+
+  lemma Div_double_aux2:
+    forall x y:int. 0 < y <= x < 2*y -> mod x y = x - y
+*)
+
+(*
+  lemma Div_mult :
+    forall x y q:int. q > 0 -> 
+      0 < q*y <= x < (q+1)*y -> div x y = q
 
-  lemma Div_pow2: forall x i:int. -pow2 i <= x < -pow2 (i-1) ->
-  		 div x (pow2 (i-1)) = -2
+  lemma Div_mult_neg :
+    forall x y q:int. q > 0 ->
+      -(q+1)*y <= x < -q*y < 0 -> div x y = -(q+1)
+*)
+
+  lemma Div_double:
+    forall x y:int. 0 < y <= x < 2*y -> div x y = 1 
+
+  lemma Div_pow: forall x i:int. 
+    i > 0 -> pow2 (i-1) <= x < pow2 i -> div x (pow2 (i-1)) = 1
+
+  lemma Div_double_neg:
+    forall x y:int. -2*y <= x < -y < 0 -> div x y = -2 
+
+  lemma Div_pow2: forall x i:int. 
+    i > 0 -> -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
+
+  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
 
@@ -104,6 +139,7 @@ theory Pow2real
   use import real.RealInfix
 
   function pow2 (i:int) : real
+
   axiom Power_0 : pow2 0 = 1.0
   axiom Power_s : forall n: int. n >= 0 -> pow2 (n+1) = 2.0 *. pow2 n
   axiom Power_p : forall n: int. n <= 0 -> pow2 (n-1) = 0.5 *. pow2 n