Commit e1e81667 by Jean-Christophe Filliâtre

### bitvectors: removed some Coq proofs

parent 5f0df6ba
 ... ... @@ -10,12 +10,13 @@ Parameter pow2: Z -> Z. Axiom Power_0 : ((pow2 0%Z) = 1%Z). Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z). Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z). Axiom Power_1 : ((pow2 1%Z) = 2%Z). Axiom Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%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. ... ... @@ -148,24 +149,29 @@ Axiom pow2_62 : ((pow2 62%Z) = 4611686018427387904%Z). Axiom pow2_63 : ((pow2 63%Z) = 9223372036854775808%Z). Axiom Div_mult_inst : forall (x:Z) (z:Z), (0%Z < x)%Z -> ((int.EuclideanDivision.div ((x * 1%Z)%Z + z)%Z x) = (1%Z + (int.EuclideanDivision.div z x))%Z). Axiom Div_mult_inst : forall (x:Z) (z:Z), (0%Z < x)%Z -> ((int.EuclideanDivision.div ((x * 1%Z)%Z + z)%Z x) = (1%Z + (int.EuclideanDivision.div z x))%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_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_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_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 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). Open Scope Z_scope. ... ... @@ -174,11 +180,11 @@ Ltac ae := why3 "alt-ergo" timelimit 3; admit. (* Why3 goal *) Theorem 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)). Theorem 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)). (* Why3 intros x i k (h1,h2). *) (* intros x i k (h1,h2). *) intros x i k (h1,h2). ... ...
 ... ... @@ -8,8 +8,8 @@ Parameter pow2: Z -> Z. Axiom Power_0 : ((pow2 0%Z) = 1%Z). Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z). Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%Z * (pow2 n))%Z). Axiom Power_1 : ((pow2 1%Z) = 2%Z). ... ... @@ -17,7 +17,8 @@ Open Scope Z_scope. Require Import Why3. (* Why3 goal *) Theorem Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) -> Theorem Power_sum : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) -> ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%Z). (* Why3 intros n m (h1,h2). *) intros n m (Hn & Hm). ... ...
 (* 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 int.Int. Require int.Abs. Require int.EuclideanDivision. Require real.Real. Require real.RealInfix. Require real.FromInt. ... ... @@ -11,18 +13,19 @@ Parameter pow2: Z -> R. Axiom Power_0 : ((pow2 0%Z) = 1%R). Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R). Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R). Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z -> Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z -> ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R). Axiom Power_s_all : forall (n:Z), ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R). Axiom Power_p_all : forall (n:Z), ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R). Axiom Power_p_all : forall (n:Z), ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R). Axiom Power_1_2 : ((05 / 10)%R = (Rdiv 1%R 2%R)%R). Axiom Power_1_2 : ((05 / 10)%R = (1%R / 2%R)%R). Axiom Power_1 : ((pow2 1%Z) = 2%R). ... ... @@ -30,31 +33,35 @@ Axiom Power_neg1 : ((pow2 (-1%Z)%Z) = (05 / 10)%R). Axiom Power_non_null_aux : forall (n:Z), (0%Z <= n)%Z -> ~ ((pow2 n) = 0%R). Axiom Power_neg_aux : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (-n)%Z) = (Rdiv 1%R (pow2 n))%R). Axiom Power_neg_aux : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (-n)%Z) = (1%R / (pow2 n))%R). Axiom Power_non_null : forall (n:Z), ~ ((pow2 n) = 0%R). Axiom Power_neg : forall (n:Z), ((pow2 (-n)%Z) = (Rdiv 1%R (pow2 n))%R). Axiom Power_neg : forall (n:Z), ((pow2 (-n)%Z) = (1%R / (pow2 n))%R). Axiom Power_sum_aux : forall (n:Z) (m:Z), (0%Z <= m)%Z -> Axiom Power_sum_aux : forall (n:Z) (m:Z), (0%Z <= m)%Z -> ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R). Axiom Power_sum : forall (n:Z) (m:Z), ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R). Axiom Power_sum : forall (n:Z) (m:Z), ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R). Parameter pow21: Z -> Z. Axiom Power_01 : ((pow21 0%Z) = 1%Z). Axiom Power_s1 : forall (n:Z), (0%Z <= n)%Z -> ((pow21 (n + 1%Z)%Z) = (2%Z * (pow21 n))%Z). Axiom Power_s1 : forall (n:Z), (0%Z <= n)%Z -> ((pow21 (n + 1%Z)%Z) = (2%Z * (pow21 n))%Z). Axiom Power_11 : ((pow21 1%Z) = 2%Z). Axiom Power_sum1 : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) -> Axiom Power_sum1 : forall (n:Z) (m:Z), ((0%Z <= n)%Z /\ (0%Z <= m)%Z) -> ((pow21 (n + m)%Z) = ((pow21 n) * (pow21 m))%Z). Axiom pow2pos : forall (i:Z), (0%Z <= i)%Z -> (0%Z < (pow21 i))%Z. Axiom pow2_0 : ((pow21 0%Z) = 1%Z). Axiom pow2_1 : ((pow21 1%Z) = 2%Z). ... ... @@ -183,13 +190,45 @@ Axiom pow2_62 : ((pow21 62%Z) = 4611686018427387904%Z). Axiom pow2_63 : ((pow21 63%Z) = 9223372036854775808%Z). Axiom Div_mult_inst : forall (x:Z) (z:Z), (0%Z < x)%Z -> ((int.EuclideanDivision.div ((x * 1%Z)%Z + z)%Z x) = (1%Z + (int.EuclideanDivision.div z x))%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 -> (((pow21 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow21 i))%Z) -> ((int.EuclideanDivision.div x (pow21 (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 -> (((-(pow21 i))%Z <= x)%Z /\ (x < (-(pow21 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x (pow21 (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 + (pow21 i))%Z (pow21 k)) 2%Z) = (int.EuclideanDivision.mod1 (int.EuclideanDivision.div x (pow21 k)) 2%Z)). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 2. Open Scope Z_scope. (* Why3 goal *) Theorem Pow2_int_real : forall (x:Z), (0%Z <= x)%Z -> ((pow2 x) = (IZR (pow21 x))). Theorem Pow2_int_real : forall (x:Z), (0%Z <= x)%Z -> ((pow2 x) = (BuiltIn.IZR (pow21 x))). (* Why3 intros x h1. *) intros x Hx. generalize Hx. pattern x; apply Z_lt_induction; auto. ... ... @@ -209,4 +248,3 @@ rewrite mult_IZR. rewrite Hind; auto with zarith. Qed.
 ... ... @@ -10,16 +10,17 @@ Parameter pow2: Z -> R. Axiom Power_0 : ((pow2 0%Z) = 1%R). Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R). Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R). Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z -> Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z -> ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R). Axiom Power_s_all : forall (n:Z), ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R). Axiom Power_p_all : forall (n:Z), ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R). Axiom Power_p_all : forall (n:Z), ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R). Axiom Power_1_2 : ((05 / 10)%R = (1%R / 2%R)%R). ... ... @@ -34,8 +35,8 @@ Ltac ae := why3 "alt-ergo" timelimit 2; admit. Open Scope Z_scope. (* Why3 goal *) Theorem Power_neg_aux : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (-n)%Z) = (1%R / (pow2 n))%R). Theorem Power_neg_aux : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (-n)%Z) = (1%R / (pow2 n))%R). (* Why3 intros n h1. *) intros n Hn. generalize Hn. ... ...
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require real.Real. Require real.RealInfix. Parameter pow2: Z -> R. Axiom Power_0 : ((pow2 0%Z) = 1%R). Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R). Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z -> ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R). Axiom Power_s_all : forall (n:Z), ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R). Axiom Power_p_all : forall (n:Z), ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R). Axiom Power_1_2 : ((05 / 10)%R = (1%R / 2%R)%R). Axiom Power_1 : ((pow2 1%Z) = 2%R). Axiom Power_neg1 : ((pow2 (-1%Z)%Z) = (05 / 10)%R). Axiom Power_non_null_aux : forall (n:Z), (0%Z <= n)%Z -> ~ ((pow2 n) = 0%R). Axiom Power_neg_aux : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (-n)%Z) = (1%R / (pow2 n))%R). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 2; admit. Open Scope Z_scope. (* Why3 goal *) Theorem Power_non_null : forall (n:Z), ~ ((pow2 n) = 0%R). (* Why3 intros n. *) intro n. assert (h:n>=0 \/ n<0) by omega. destruct h. ae. pose (n':=-n). assert (Hn': n' > 0) by (subst n'; omega). replace n with (-n') by (subst n'; omega). rewrite Power_neg_aux; auto with zarith. unfold Rdiv. rewrite Rmult_1_l. apply Rinv_neq_0_compat. ae. Admitted.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require real.Real. Require real.RealInfix. Parameter pow2: Z -> R. Axiom Power_0 : ((pow2 0%Z) = 1%R). Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R). Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z -> ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R). Axiom Power_s_all : forall (n:Z), ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R). Axiom Power_p_all : forall (n:Z), ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R). Axiom Power_1_2 : ((05 / 10)%R = (1%R / 2%R)%R). Axiom Power_1 : ((pow2 1%Z) = 2%R). Axiom Power_neg1 : ((pow2 (-1%Z)%Z) = (05 / 10)%R). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 2; admit. (* Why3 goal *) Theorem Power_non_null_aux : forall (n:Z), (0%Z <= n)%Z -> ~ ((pow2 n) = 0%R). (* Why3 intros n h1. *) intros n Hn. generalize Hn. pattern n; apply Z_lt_induction; auto. ae. Admitted.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require real.Real. Require real.RealInfix. Parameter pow2: Z -> R. Axiom Power_0 : ((pow2 0%Z) = 1%R). Axiom Power_s : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R). Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z -> ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R). Axiom Power_s_all : forall (n:Z), ((pow2 (n + 1%Z)%Z) = (2%R * (pow2 n))%R). Axiom Power_p_all : forall (n:Z), ((pow2 (n - 1%Z)%Z) = ((05 / 10)%R * (pow2 n))%R). Axiom Power_1_2 : ((05 / 10)%R = (1%R / 2%R)%R). Axiom Power_1 : ((pow2 1%Z) = 2%R). Axiom Power_neg1 : ((pow2 (-1%Z)%Z) = (05 / 10)%R). Axiom Power_non_null_aux : forall (n:Z), (0%Z <= n)%Z -> ~ ((pow2 n) = 0%R). Axiom Power_neg_aux : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (-n)%Z) = (1%R / (pow2 n))%R). Axiom Power_non_null : forall (n:Z), ~ ((pow2 n) = 0%R). Axiom Power_neg : forall (n:Z), ((pow2 (-n)%Z) = (1%R / (pow2 n))%R). Axiom Power_sum_aux : forall (n:Z) (m:Z), (0%Z <= m)%Z -> ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 2; admit. Open Scope Z_scope. (* Why3 goal *) Theorem Power_sum : forall (n:Z) (m:Z), ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R). (* Why3 intros n m. *) intros n m. assert (h:m>=0 \/ m <=0) by omega; destruct h. apply Power_sum_aux; auto with zarith. pose (m' := -m). assert (0 <= m') by (subst m'; omega). replace m with (-m') by (subst m'; omega). replace (n+ - m') with (- ((-n) + m')) by omega. repeat rewrite Power_neg; auto. rewrite Power_sum_aux; auto. ae. Admitted.
 ... ... @@ -3,9 +3,11 @@ "http://why3.lri.fr/why3session.dtd"> ... ... @@ -244,7 +246,7 @@ ... ... @@ -303,7 +305,7 @@ ... ... @@ -467,13 +469,24 @@ ... ... @@ -482,10 +495,10 @@ ... ...
No preview for this file type
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!