 parent fc2bc72c
 ... ... @@ -95,12 +95,16 @@ theory Pow2real lemma Power_p_all : forall n:int. pow2 (n-1) = 0.5 *. pow2 n lemma Power_1_2: 0.5 = 1.0 /. 2.0 lemma Power_1 : pow2 1 = 2.0 lemma Power_neg1 : pow2 (-1) = 0.5 lemma Power_non_null_aux: forall n:int.n>=0 -> pow2 n <> 0.0 lemma Power_non_null: forall n:int. pow2 n <> 0.0 lemma Power_neg_aux : forall n:int. n>=0 ->pow2 (-n) = 1.0 /. pow2 n 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 ... ...
 ... ... @@ -343,6 +343,19 @@ rewrite Power_0;auto with zarith. replace (x) with (x-1+1) by omega. rewrite Power_s;auto with *. Require Export ZArith Classical_Prop. Open Scope Z_scope. Lemma Zmult_neq_0_compat : forall (x y : Z), x <> 0 -> y <> 0 -> x * y <> 0. Proof. intros x y Hx Hy Hxy. apply (@absurd (x = 0 \/ y = 0)). apply Zmult_integral, Hxy. apply and_not_or ; intuition. Qed. apply Zmult_neq_0_compat. auto with zarith. apply Hind;auto with zarith. Qed. (* DO NOT EDIT BELOW *) ... ...
 (* 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_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 : forall (n:Z), ~ ((pow2 n) = 0%R). (* YOU MAY EDIT THE CONTEXT BELOW *) Open Scope R_scope. Open Scope Z_scope. (* DO NOT EDIT BELOW *) Theorem Power_neg_aux : forall (n:Z), (0%Z <= n)%Z -> ((pow2 (-n)%Z) = (Rdiv 1%R (pow2 n))%R). (* YOU MAY EDIT THE PROOF BELOW *) intros n H. cut (0 <=n);auto. apply Z_lt_induction with (P:= fun n => 0 <= n -> pow2 (- n) = (1 / pow2 n)%R); auto with zarith. intros x Hind Hxpos. assert (hx:x>0\/x=0) by omega. destruct hx. replace (x) with (x-1+1) by omega. replace (- (x - 1 + 1)) with (-(x-1) -1) by omega. rewrite Power_p;auto with zarith. rewrite Power_s;auto with zarith. rewrite Hind;auto with *. rewrite Power_1_2. unfold Rdiv in |-*. repeat rewrite Rmult_1_l. rewrite<-Rinv_mult_distr;auto. apply Rgt_not_eq;auto with *. apply Power_non_null. (*x = 0*) subst x. replace (-0) with 0 by omega. rewrite Power_0. unfold Rdiv in |-*. rewrite Rinv_r;auto with *. Qed. (* DO NOT EDIT BELOW *)
 (* 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). (* YOU MAY EDIT THE CONTEXT BELOW *) Open Scope Z_scope. (* DO NOT EDIT BELOW *) Theorem Power_non_null : forall (n:Z), ~ ((pow2 n) = 0%R). (* YOU MAY EDIT THE PROOF BELOW *) intro n. assert (h:n>=0 \/ n<=0) by omega. destruct h. cut (0 <= n); auto with zarith. apply Z_lt_induction with (P:= fun n => 0 <= n -> pow2 n <> 0%R);auto with zarith. intros x Hind Hxpos. assert (hx:x = 0 \/ x >0) by omega. destruct hx. subst x. rewrite Power_0;auto with *. replace (x) with (x-1+1) by omega. rewrite Power_s;auto with *. rewrite Rmult_neq_0_reg with (r1:=2%R) (r2:=pow2 (x - 1)). apply Hind. Qed. (* DO NOT EDIT BELOW *)
 (* 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_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). (* YOU MAY EDIT THE CONTEXT BELOW *) Open Scope Z_scope. (* DO NOT EDIT BELOW *) Theorem Power_non_null : forall (n:Z), ~ ((pow2 n) = 0%R). (* YOU MAY EDIT THE PROOF BELOW *) intro n. assert (h:n>=0 \/ n<0) by omega. destruct h. apply Power_non_null_aux;auto with zarith. pose (n':=-n). replace n with (-n') by (subst n';omega). replace (n') with (n'-1+1) by omega. replace (- (n' - 1 + 1)) with (-(n'-1)-1) by omega. rewrite Power_p. apply Rmult_integral_contrapositive. split. rewrite Power_1_2. unfold Rdiv in |-*. rewrite Rmult_1_l. apply Rinv_neq_0_compat. apply Rgt_not_eq;auto with *. cut(n'>0);auto with zarith. apply Z_lt_induction with (P:= fun n' => n' > 0 -> pow2 (- n') <> 0%R);auto with zarith. intros x Hind Hnxpos. replace (x) with (x-1+1) by omega. replace (- (x - 1 + 1)) with (-(x-1)-1) by omega. rewrite Power_p_all;auto with zarith. apply Rmult_integral_contrapositive. split. rewrite Power_1_2. unfold Rdiv in |-*. rewrite Rmult_1_l. apply Rinv_neq_0_compat. apply Rgt_not_eq;auto with *. apply Hind;auto with zarith. Qed. (* DO NOT EDIT BELOW *)
 (* 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_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). (* YOU MAY EDIT THE CONTEXT BELOW *) Open Scope Z_scope. (* DO NOT EDIT BELOW *) Theorem Power_non_null_aux : forall (n:Z), (0%Z <= n)%Z -> ~ ((pow2 n) = 0%R). (* YOU MAY EDIT THE PROOF BELOW *) intros n H. cut (0 <= n); auto with zarith. apply Z_lt_induction with (P:= fun n => 0 <= n -> (pow2 n <> 0)%R);auto with zarith. intros x Hind Hxpos. assert (hx:x = 0 \/ x >0) by omega. destruct hx. subst x. rewrite Power_0;auto with *. (*x>0*) replace (x) with (x-1+1) by omega. rewrite Power_s;auto with *. apply Rmult_integral_contrapositive. split. apply Rgt_not_eq;auto with *. apply Hind;auto with *. Qed. (* DO NOT EDIT BELOW *)
 ... ... @@ -22,6 +22,8 @@ Axiom Power_1 : ((pow2 1%Z) = 2%R). Axiom Power_neg1 : ((pow2 (-1%Z)%Z) = (05 / 10)%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 -> ... ... @@ -45,7 +47,11 @@ repeat rewrite Power_neg. rewrite Power_sum_aux. rewrite Power_neg. field. split. apply Power_non_null. apply Power_non_null. subst m'. auto with zarith. Qed. (* DO NOT EDIT BELOW *) ... ...
This diff is collapsed.
 ... ... @@ -585,10 +585,30 @@ Axiom Power_s1 : forall (n:Z), (0%Z <= n)%Z -> Axiom Power_p : forall (n:Z), (n <= 0%Z)%Z -> ((pow21 (n - 1%Z)%Z) = ((05 / 10)%R * (pow21 n))%R). Axiom Power_s_all : forall (n:Z), ((pow21 (n + 1%Z)%Z) = (2%R * (pow21 n))%R). Axiom Power_p_all : forall (n:Z), ((pow21 (n - 1%Z)%Z) = ((05 / 10)%R * (pow21 n))%R). Axiom Power_1_2 : ((05 / 10)%R = (Rdiv 1%R 2%R)%R). Axiom Power_11 : ((pow21 1%Z) = 2%R). Axiom Power_neg1 : ((pow21 (-1%Z)%Z) = (05 / 10)%R). Axiom Power_non_null_aux : forall (n:Z), (0%Z <= n)%Z -> ~ ((pow21 n) = 0%R). Axiom Power_non_null : forall (n:Z), ~ ((pow21 n) = 0%R). Axiom Power_neg_aux : forall (n:Z), (0%Z <= n)%Z -> ((pow21 (-n)%Z) = (Rdiv 1%R (pow21 n))%R). Axiom Power_neg : forall (n:Z), ((pow21 (-n)%Z) = (Rdiv 1%R (pow21 n))%R). Axiom Power_sum_aux : forall (n:Z) (m:Z), (0%Z <= m)%Z -> ((pow21 (n + m)%Z) = ((pow21 n) * (pow21 m))%R). Axiom Power_sum1 : forall (n:Z) (m:Z), ((pow21 (n + m)%Z) = ((pow21 n) * (pow21 m))%R). ... ... @@ -746,7 +766,8 @@ Open Scope Z_scope. Theorem sign_of_x : forall (x:Z), ((nth (from_int2c x) 31%Z) = false) -> (0%Z < x)%Z. (* YOU MAY EDIT THE PROOF BELOW *) intro x. intros x H. Qed. ... ...
This diff is collapsed.
This diff is collapsed.
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!