Commit e5b01dea by Jean-Christophe Filliâtre

fixed Coq proofs (Claude and Guillaume)

parent 59cecc21
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require Import BuiltIn. Require BuiltIn. Require bool.Bool. Require int.Int. (* Why3 assumption *) Definition implb(x:bool) (y:bool): bool := match (x, y) with | (true, false) => false | (_, _) => true end. Require int.Abs. Require int.EuclideanDivision. Parameter pow2: Z -> Z. ... ... @@ -23,6 +19,8 @@ Axiom Power_1 : ((pow2 1%Z) = 2%Z). Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) -> ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z). Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow2 i))%Z. Axiom pow2_0 : ((pow2 0%Z) = 1%Z). Axiom pow2_1 : ((pow2 1%Z) = 2%Z). ... ... @@ -151,129 +149,151 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z). Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z). Axiom Div_double : forall (x:Z) (y:Z), (((0%Z < y)%Z /\ (y <= x)%Z) /\ (x < (2%Z * y)%Z)%Z) -> ((int.EuclideanDivision.div x y) = 1%Z). Axiom Div_pow : forall (x:Z) (i:Z), (0%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)). Axiom Div_double_neg : forall (x:Z) (y:Z), (((((-2%Z)%Z * y)%Z <= x)%Z /\ (x < (-y)%Z)%Z) /\ ((-y)%Z < 0%Z)%Z) -> ((int.EuclideanDivision.div x y) = (-2%Z)%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), (0%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_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. 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. Parameter bvzero: bv. Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvzero n) = false). Axiom Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvzero n) = false). Parameter bvone: bv. Axiom Nth_one : forall (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth bvone 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 /\ (n < size)%Z) -> ((nth v1 n) = (nth v2 n)). 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). Parameter bw_and: bv -> bv -> bv. Axiom Nth_bw_and : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))). (n < size)%Z) -> ((nth (bw_and v1 v2) n) = (andb (nth v1 n) (nth v2 n))). Parameter bw_or: bv -> bv -> bv. Axiom Nth_bw_or : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))). (n < size)%Z) -> ((nth (bw_or v1 v2) n) = (orb (nth v1 n) (nth v2 n))). Parameter bw_xor: bv -> bv -> bv. Axiom Nth_bw_xor : forall (v1:bv) (v2:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))). (n < size)%Z) -> ((nth (bw_xor v1 v2) n) = (xorb (nth v1 n) (nth v2 n))). Axiom Nth_bw_xor_v1true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ (n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2) (n < size)%Z) /\ ((nth v1 n) = true)) -> ((nth (bw_xor v1 v2) n) = (negb (nth v2 n))). Axiom Nth_bw_xor_v1false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ (n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2 n)). (n < size)%Z) /\ ((nth v1 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v2 n)). Axiom Nth_bw_xor_v2true : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ (n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2) (n < size)%Z) /\ ((nth v2 n) = true)) -> ((nth (bw_xor v1 v2) n) = (negb (nth v1 n))). Axiom Nth_bw_xor_v2false : forall (v1:bv) (v2:bv) (n:Z), (((0%Z <= n)%Z /\ (n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1 n)). (n < size)%Z) /\ ((nth v2 n) = false)) -> ((nth (bw_xor v1 v2) n) = (nth v1 n)). Parameter bw_not: bv -> bv. Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> Axiom Nth_bw_not : forall (v:bv) (n:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((nth (bw_not v) n) = (negb (nth v n))). Parameter lsr: bv -> Z -> bv. Axiom lsr_nth_low : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\ (n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\ ((n + s)%Z < size)%Z)) -> ((nth (lsr b s) n) = (nth b (n + s)%Z)). (n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\ ((n + s)%Z < size)%Z)) -> ((nth (lsr b s) n) = (nth b (n + s)%Z)). Axiom lsr_nth_high : forall (b:bv) (n:Z) (s:Z), (((0%Z <= n)%Z /\ (n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\ (n < size)%Z) /\ (((0%Z <= s)%Z /\ (s < size)%Z) /\ (size <= (n + s)%Z)%Z)) -> ((nth (lsr b s) n) = false). Parameter asr: bv -> Z -> bv. Axiom asr_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < size)%Z -> ((nth (asr b s) n) = (nth b (n + s)%Z)))). (n < size)%Z) -> ((0%Z <= s)%Z -> (((n + s)%Z < size)%Z -> ((nth (asr b s) n) = (nth b (n + s)%Z)))). Axiom asr_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((0%Z <= s)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (asr b s) n) = (nth b (size - 1%Z)%Z)))). (n < size)%Z) -> ((0%Z <= s)%Z -> ((size <= (n + s)%Z)%Z -> ((nth (asr b s) n) = (nth b (size - 1%Z)%Z)))). Parameter lsl: bv -> Z -> bv. Axiom lsl_nth_high : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s) (n < size)%Z) -> ((0%Z <= s)%Z -> ((0%Z <= (n - s)%Z)%Z -> ((nth (lsl b s) n) = (nth b (n - s)%Z)))). Axiom lsl_nth_low : forall (b:bv) (n:Z) (s:Z), ((0%Z <= n)%Z /\ (n < size)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s) (n < size)%Z) -> ((0%Z <= s)%Z -> (((n - s)%Z < 0%Z)%Z -> ((nth (lsl b s) n) = false))). Parameter to_nat_sub: bv -> Z -> Z -> Z. Axiom to_nat_sub_zero : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\ (i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j (i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = false) -> ((to_nat_sub b j i) = (to_nat_sub b (j - 1%Z)%Z i))). Axiom to_nat_sub_one : forall (b:bv) (j:Z) (i:Z), (((0%Z <= i)%Z /\ (i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j (i <= j)%Z) /\ (j < size)%Z) -> (((nth b j) = true) -> ((to_nat_sub b j i) = ((pow2 (j - i)%Z) + (to_nat_sub b (j - 1%Z)%Z i))%Z)). Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j < i)%Z -> Axiom to_nat_sub_high : forall (b:bv) (j:Z) (i:Z), (j < i)%Z -> ((to_nat_sub b j i) = 0%Z). Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\ Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\ (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i < k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j 0%Z) = (to_nat_sub b i 0%Z))). (i < k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j 0%Z) = (to_nat_sub b i 0%Z))). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 2. Open Scope Z_scope. (* Why3 goal *) Theorem to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\ Theorem to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j i) = 0%Z)). (* intros b i j (h1,h2) h3. *) intros b i j (Hj & Hi). assert (h:(i>j)\/(i<=j)) by omega; destruct h. ae. why3 "Alt-Ergo,0.95.1," timelimit 2. generalize Hj. pattern j. apply Zlt_lower_bound_ind with (z:=i); auto. ae. why3 "CVC3,2.4.1,". Qed.
This diff is collapsed.
 (* This file is generated by Why3's Coq 8.4 driver *) (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. ... ... @@ -152,13 +152,20 @@ 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). Axiom Div_double : forall (x:Z) (y:Z), (((0%Z < y)%Z /\ (y <= x)%Z) /\ (x < (2%Z * y)%Z)%Z) -> ((int.EuclideanDivision.div x y) = 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 Div_pow : forall (x:Z) (i:Z), (0%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)). Axiom Div_double_neg : forall (x:Z) (y:Z), (((((-2%Z)%Z * y)%Z <= x)%Z /\ (x < (-y)%Z)%Z) /\ ((-y)%Z < 0%Z)%Z) -> ((int.EuclideanDivision.div x y) = (-2%Z)%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), (0%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_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 ... ... @@ -586,6 +593,25 @@ Axiom double_of_bv64_value : forall (b:bv1), ((0%Z < (to_nat_sub1 b 62%Z 62%Z 52%Z) - 1023%Z)%Z))%R * (1%R + ((IZR (to_nat_sub1 b 51%Z 0%Z)) * (pow21 (-52%Z)%Z))%R)%R)%R). Axiom nth_j1 : forall (i:Z), ((0%Z <= i)%Z /\ (i <= 19%Z)%Z) -> ((nth (from_int 1127219200%Z) i) = false). Axiom nth_j2 : forall (i:Z), ((20%Z <= i)%Z /\ (i <= 21%Z)%Z) -> ((nth (from_int 1127219200%Z) i) = true). Axiom nth_j3 : forall (i:Z), ((22%Z <= i)%Z /\ (i <= 23%Z)%Z) -> ((nth (from_int 1127219200%Z) i) = false). Axiom nth_j4 : forall (i:Z), ((24%Z <= i)%Z /\ (i <= 25%Z)%Z) -> ((nth (from_int 1127219200%Z) i) = true). Axiom nth_j5 : forall (i:Z), ((26%Z <= i)%Z /\ (i <= 29%Z)%Z) -> ((nth (from_int 1127219200%Z) i) = false). Axiom nth_j6 : ((nth (from_int 1127219200%Z) 30%Z) = true). Axiom nth_j7 : ((nth (from_int 1127219200%Z) 31%Z) = false). Axiom jp0_30 : forall (i:Z), ((0%Z <= i)%Z /\ (i < 30%Z)%Z) -> ((nth (from_int 2147483648%Z) i) = false). ... ... @@ -743,7 +769,7 @@ Axiom nth_var8 : forall (x:Z), (is_int32 x) -> ((nth1 (var x) 62%Z) = true). Open Scope Z_scope. Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. Ltac ae := why3 "Alt-Ergo,0.95.1," timelimit 3. (* Why3 goal *) ... ... @@ -753,7 +779,7 @@ Theorem lemma3 : forall (x:Z), (is_int32 x) -> ((to_nat_sub1 (var x) 62%Z intros x H. rewrite to_nat_sub_one1; auto with zarith. 2: apply nth_var8; auto with zarith. replace (62 - 52) with 10 by omega. change (62 - 52) with 10. rewrite pow2_10. rewrite to_nat_sub_zero1; auto with zarith. 2: apply nth_var7; auto with zarith. ... ... @@ -765,11 +791,11 @@ rewrite to_nat_sub_zero1; auto with zarith. 2: apply nth_var7; auto with zarith. rewrite to_nat_sub_one1; auto with zarith. 2: apply nth_var6; auto with zarith. replace (62 - 1 - 1 - 1 - 1 - 1 - 52) with 5 by omega. change (62 - 1 - 1 - 1 - 1 - 1 - 52) with 5. rewrite pow2_5. rewrite to_nat_sub_one1; auto with zarith. 2: apply nth_var6; auto with zarith. replace (62 - 1 - 1 - 1 - 1 - 1 - 1 - 52) with 4 by omega. change (62 - 1 - 1 - 1 - 1 - 1 - 1 - 52) with 4. rewrite pow2_4. rewrite to_nat_sub_zero1; auto with zarith. 2: apply nth_var5; auto with zarith. ... ... @@ -777,6 +803,11 @@ rewrite to_nat_sub_zero1; auto with zarith. 2: apply nth_var5; auto with zarith. rewrite to_nat_sub_one1; auto with zarith. 2: ae. change (62 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 52) with 1. rewrite pow2_1. change (62 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1 - 1) with 52. rewrite to_nat_sub_one1 ; auto with zarith. 2: ae. ae. Qed. ... ...
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!