Commit 9d3e04c4 by MARCHE Claude

### finished proof of examples/bitvectors/power2

parent bea0483f
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require int.Int. Require real.Real. Require real.RealInfix. Require real.FromInt. 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 = (Rdiv 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) = (Rdiv 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_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). 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_11 : ((pow21 1%Z) = 2%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 pow2_0 : ((pow21 0%Z) = 1%Z). Axiom pow2_1 : ((pow21 1%Z) = 2%Z). Axiom pow2_2 : ((pow21 2%Z) = 4%Z). Axiom pow2_3 : ((pow21 3%Z) = 8%Z). Axiom pow2_4 : ((pow21 4%Z) = 16%Z). Axiom pow2_5 : ((pow21 5%Z) = 32%Z). Axiom pow2_6 : ((pow21 6%Z) = 64%Z). Axiom pow2_7 : ((pow21 7%Z) = 128%Z). Axiom pow2_8 : ((pow21 8%Z) = 256%Z). Axiom pow2_9 : ((pow21 9%Z) = 512%Z). Axiom pow2_10 : ((pow21 10%Z) = 1024%Z). Axiom pow2_11 : ((pow21 11%Z) = 2048%Z). Axiom pow2_12 : ((pow21 12%Z) = 4096%Z). Axiom pow2_13 : ((pow21 13%Z) = 8192%Z). Axiom pow2_14 : ((pow21 14%Z) = 16384%Z). Axiom pow2_15 : ((pow21 15%Z) = 32768%Z). Axiom pow2_16 : ((pow21 16%Z) = 65536%Z). Axiom pow2_17 : ((pow21 17%Z) = 131072%Z). Axiom pow2_18 : ((pow21 18%Z) = 262144%Z). Axiom pow2_19 : ((pow21 19%Z) = 524288%Z). Axiom pow2_20 : ((pow21 20%Z) = 1048576%Z). Axiom pow2_21 : ((pow21 21%Z) = 2097152%Z). Axiom pow2_22 : ((pow21 22%Z) = 4194304%Z). Axiom pow2_23 : ((pow21 23%Z) = 8388608%Z). Axiom pow2_24 : ((pow21 24%Z) = 16777216%Z). Axiom pow2_25 : ((pow21 25%Z) = 33554432%Z). Axiom pow2_26 : ((pow21 26%Z) = 67108864%Z). Axiom pow2_27 : ((pow21 27%Z) = 134217728%Z). Axiom pow2_28 : ((pow21 28%Z) = 268435456%Z). Axiom pow2_29 : ((pow21 29%Z) = 536870912%Z). Axiom pow2_30 : ((pow21 30%Z) = 1073741824%Z). Axiom pow2_31 : ((pow21 31%Z) = 2147483648%Z). Axiom pow2_32 : ((pow21 32%Z) = 4294967296%Z). Axiom pow2_33 : ((pow21 33%Z) = 8589934592%Z). Axiom pow2_34 : ((pow21 34%Z) = 17179869184%Z). Axiom pow2_35 : ((pow21 35%Z) = 34359738368%Z). Axiom pow2_36 : ((pow21 36%Z) = 68719476736%Z). Axiom pow2_37 : ((pow21 37%Z) = 137438953472%Z). Axiom pow2_38 : ((pow21 38%Z) = 274877906944%Z). Axiom pow2_39 : ((pow21 39%Z) = 549755813888%Z). Axiom pow2_40 : ((pow21 40%Z) = 1099511627776%Z). Axiom pow2_41 : ((pow21 41%Z) = 2199023255552%Z). Axiom pow2_42 : ((pow21 42%Z) = 4398046511104%Z). Axiom pow2_43 : ((pow21 43%Z) = 8796093022208%Z). Axiom pow2_44 : ((pow21 44%Z) = 17592186044416%Z). Axiom pow2_45 : ((pow21 45%Z) = 35184372088832%Z). Axiom pow2_46 : ((pow21 46%Z) = 70368744177664%Z). Axiom pow2_47 : ((pow21 47%Z) = 140737488355328%Z). Axiom pow2_48 : ((pow21 48%Z) = 281474976710656%Z). Axiom pow2_49 : ((pow21 49%Z) = 562949953421312%Z). Axiom pow2_50 : ((pow21 50%Z) = 1125899906842624%Z). Axiom pow2_51 : ((pow21 51%Z) = 2251799813685248%Z). Axiom pow2_52 : ((pow21 52%Z) = 4503599627370496%Z). Axiom pow2_53 : ((pow21 53%Z) = 9007199254740992%Z). Axiom pow2_54 : ((pow21 54%Z) = 18014398509481984%Z). Axiom pow2_55 : ((pow21 55%Z) = 36028797018963968%Z). Axiom pow2_56 : ((pow21 56%Z) = 72057594037927936%Z). Axiom pow2_57 : ((pow21 57%Z) = 144115188075855872%Z). Axiom pow2_58 : ((pow21 58%Z) = 288230376151711744%Z). Axiom pow2_59 : ((pow21 59%Z) = 576460752303423488%Z). Axiom pow2_60 : ((pow21 60%Z) = 1152921504606846976%Z). Axiom pow2_61 : ((pow21 61%Z) = 2305843009213693952%Z). Axiom pow2_62 : ((pow21 62%Z) = 4611686018427387904%Z). Axiom pow2_63 : ((pow21 63%Z) = 9223372036854775808%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))). intros x Hx. generalize Hx. pattern x; apply Z_lt_induction; auto. clear x Hx. intros x Hind Hx. assert (h:x = 0 \/ x > 0) by omega; destruct h. subst x. rewrite Power_0. rewrite pow2_0. auto with zarith. replace x with (x-1+1) by omega. rewrite Power_s; auto with zarith. rewrite Power_sum1; auto with zarith. rewrite pow2_1. rewrite Zmult_comm. rewrite mult_IZR. rewrite Hind; auto with zarith. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. 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 = (Rdiv 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). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 2. Open Scope Z_scope. (* Why3 goal *) Theorem Power_neg_aux : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (-n)%Z) = (Rdiv 1%R (pow2 n))%R). intros n Hn. generalize Hn. pattern n; apply Z_lt_induction; auto. clear n Hn. intros n Hind Hn. assert (h:n=0\/n>0) by omega; destruct h. ae. replace n with (n-1+1) by omega. replace (- (n - 1 + 1)) with (-(n-1) -1) by omega. rewrite Power_p;auto with zarith. rewrite Power_s;auto with zarith. ae. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. 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 = (Rdiv 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) = (Rdiv 1%R (pow2 n))%R). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 2. Open Scope Z_scope. (* Why3 goal *) Theorem Power_non_null : forall (n:Z), ~ ((pow2 n) = 0%R). 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. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. 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 = (Rdiv 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. (* Why3 goal *) Theorem Power_non_null_aux : forall (n:Z), (0%Z <= n)%Z -> ~ ((pow2 n) = 0%R). intros n Hn. generalize Hn. pattern n; apply Z_lt_induction; auto. ae. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. 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 = (Rdiv 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) = (Rdiv 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_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. Open Scope Z_scope. (* Why3 goal *) Theorem Power_sum : forall (n:Z) (m:Z), ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R). 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. Qed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. 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 = (Rdiv 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) = (Rdiv 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). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 2. Open Scope Z_scope. (* Why3 goal *) Theorem Power_sum_aux : forall (n:Z) (m:Z), (0%Z <= m)%Z -> ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R). intros n m Hm. generalize Hm. pattern m; apply Z_lt_induction; auto. clear m Hm. intros m Hind Hm. assert (h:(m = 0 \/ m > 0)) by omega. destruct h. ae. replace m with ((m-1)+1) by omega. rewrite Power_s_all;auto with zarith. ae. Qed.
 ... ... @@ -32,8 +32,8 @@ version="3.2"/> verified="true" expanded="false"> verified="true" expanded="false">