diff --git a/tests/bitvector1.why b/tests/bitvector1.why index 0c4d0fb282f105cec051adef4e1c71ac334419f9..b3b3adcf056acb63a221a9a00f440923765a7803 100644 --- a/tests/bitvector1.why +++ b/tests/bitvector1.why @@ -87,21 +87,24 @@ 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 -(* axiom Power_s : forall n:int. pow2 (n+1) = 2.0 *. pow2 n + lemma Power_s_all : forall n:int. pow2 (n+1) = 2.0 *. pow2 n + + lemma Power_p_all : forall n:int. pow2 (n-1) = 0.5 *. pow2 n - axiom Power_p : forall n:int. pow2 (n-1) = 0.5 *. pow2 n -*) lemma Power_1 : pow2 1 = 2.0 lemma Power_neg1 : pow2 (-1) = 0.5 + lemma Power_non_null: forall n:int. pow2 n <> 0.0 + + lemma Power_neg : forall n:int. pow2 (-n) = 1.0 /. pow2 n + + lemma Power_sum_aux : forall n m: int. m >= 0 -> pow2 (n+m) = pow2 n *. pow2 m + lemma Power_sum : forall n m: int. pow2 (n+m) = pow2 n *. pow2 m use Pow2int diff --git a/tests/bitvector1/bitvector1_Pow2real_Power_sum_1.v b/tests/bitvector1/bitvector1_Pow2real_Power_sum_1.v index 9249b8acc9767111028e82ed6608024a39dde069..4d91cdab2d74545d822ec6db6f519612ef0cfc93 100644 --- a/tests/bitvector1/bitvector1_Pow2real_Power_sum_1.v +++ b/tests/bitvector1/bitvector1_Pow2real_Power_sum_1.v @@ -7,15 +7,26 @@ Parameter pow2: Z -> R. Axiom Power_0 : ((pow2 0%Z) = 1%R). -Axiom Power_s : forall (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), +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 : ((pow2 1%Z) = 2%R). Axiom Power_neg1 : ((pow2 (-1%Z)%Z) = (05 / 10)%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). + (* YOU MAY EDIT THE CONTEXT BELOW *) Open Scope Z_scope. (* DO NOT EDIT BELOW *) @@ -24,32 +35,16 @@ Theorem Power_sum : forall (n:Z) (m:Z), ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R). (* YOU MAY EDIT THE PROOF BELOW *) intros n m. - assert (hm:m>=0 \/ m <=0) by omega. destruct hm. -cut (0 <= m); auto with zarith. -apply Z_lt_induction with - (P:= fun m => - 0 <= m ->pow2 (n + m) = (pow2 n * pow2 m)%R); - auto with zarith. -intros x Hind Hxpos. -assert (h:(x = 0 \/ x > 0)) by omega. -destruct h. -subst x. -rewrite Power_0. -replace (n+0) with n by omega. -rewrite Rmult_1_r. -auto. -replace (x) with ((x-1)+1) by omega. -rewrite Power_s;auto with zarith. -replace (n + (x-1+1)) with (n+(x-1)+1) by omega. -rewrite Power_s;auto with zarith. -rewrite Hind;auto with zarith. -rewrite <-Rmult_assoc. -rewrite <-Rmult_assoc. -rewrite Rmult_comm with (r1:=pow2 n)(r2:=2%R). -auto with zarith. - +apply Power_sum_aux; auto with zarith. +pose (m' := -m). +replace m with (-m') by (subst m'; omega). +replace (n+ - m') with (- ((-n) + m')) by omega. +repeat rewrite Power_neg. +rewrite Power_sum_aux. +rewrite Power_neg. +field. Qed. (* DO NOT EDIT BELOW *) diff --git a/tests/bitvector1/bitvector1_Pow2real_Power_sum_aux_1.v b/tests/bitvector1/bitvector1_Pow2real_Power_sum_aux_1.v new file mode 100644 index 0000000000000000000000000000000000000000..7d4a67386491e78c4847bd96e5f6200e86b6d7bd --- /dev/null +++ b/tests/bitvector1/bitvector1_Pow2real_Power_sum_aux_1.v @@ -0,0 +1,61 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import ZArith. +Require Import Rbase. +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 : ((pow2 1%Z) = 2%R). + +Axiom Power_neg1 : ((pow2 (-1%Z)%Z) = (05 / 10)%R). + +Axiom Power_neg : forall (n:Z), ((pow2 (-n)%Z) = (Rdiv 1%R (pow2 n))%R). + +(* YOU MAY EDIT THE CONTEXT BELOW *) +Open Scope Z_scope. +(* DO NOT EDIT BELOW *) + +Theorem Power_sum_aux : forall (n:Z) (m:Z), (0%Z <= m)%Z -> + ((pow2 (n + m)%Z) = ((pow2 n) * (pow2 m))%R). +(* YOU MAY EDIT THE PROOF BELOW *) +intros n m Hmpos. +cut (0 <= m); auto with zarith. +apply Z_lt_induction with + (P:= fun m => + 0 <= m ->pow2 (n + m) = (pow2 n * pow2 m)%R); + auto with zarith. +intros x Hind Hxpos. +assert (h:(x = 0 \/ x > 0)) by omega. +destruct h. +subst x. +rewrite Power_0. +replace (n+0) with n by omega. +rewrite Rmult_1_r. +auto. +replace (x) with ((x-1)+1) by omega. +rewrite Power_s_all;auto with zarith. +replace (n + (x-1+1)) with (n+(x-1)+1) by omega. +rewrite Power_s_all;auto with zarith. +rewrite Hind;auto with zarith. +rewrite <-Rmult_assoc. +rewrite <-Rmult_assoc. +rewrite Rmult_comm with (r1:=pow2 n)(r2:=2%R). +auto with zarith. + +Qed. +(* DO NOT EDIT BELOW *) + + diff --git a/tests/bitvector1/why3session.xml b/tests/bitvector1/why3session.xml index 80dba153de4c879257750fc909802d5bfe4de6cc..46e12954641cd3295c46562a3ff82e964ead284b 100644 --- a/tests/bitvector1/why3session.xml +++ b/tests/bitvector1/why3session.xml @@ -64,7 +64,7 @@ expanded="true"> + obsolete="false"> - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + @@ -1053,7 +1109,7 @@ @@ -1066,51 +1122,135 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + - + - + + + + + obsolete="true"> @@ -1483,332 +1623,332 @@ + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> @@ -1819,826 +1959,826 @@ expanded="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> @@ -2646,126 +2786,126 @@ prover="coq" timelimit="5" edited="bitvector1_TestDoubleOfInt_sign_of_x_1.v" - obsolete="false"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> @@ -2848,106 +2988,106 @@ + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> @@ -2986,15 +3126,15 @@ + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true"> + obsolete="true">