Commit 12121e6a authored by MARCHE Claude's avatar MARCHE Claude

bitvecotrs, power_sum

parent b6331a81
......@@ -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
......
......@@ -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 *)
......
(* 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 *)
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!
Please register or to comment