From c114c99ac237c34e2a24aeec2344efbcd7f1e34d Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 18 Jan 2002 14:46:04 +0000 Subject: ajouts provenant de Chinese dans ZArith + deplacements de 3 fichiers de contrib/omega vers theories/ZArith git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2406 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/omega/Zcomplements.v | 306 ---------------------------------- contrib/omega/Zlogarithm.v | 264 ----------------------------- contrib/omega/Zpower.v | 386 ------------------------------------------- 3 files changed, 956 deletions(-) delete mode 100644 contrib/omega/Zcomplements.v delete mode 100644 contrib/omega/Zlogarithm.v delete mode 100644 contrib/omega/Zpower.v (limited to 'contrib/omega') diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v deleted file mode 100644 index 90d1f5940..000000000 --- a/contrib/omega/Zcomplements.v +++ /dev/null @@ -1,306 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 0 preserves Zcompare. It also perserves - Zle, Zlt, Zge, Zgt *) - -Implicit Arguments On. - -Lemma Zmult_zero : (x,y:Z)`x*y=0` -> `x=0` \/ `y=0`. -NewDestruct x; NewDestruct y; Auto. -Simpl; Intros; Discriminate H. -Simpl; Intros; Discriminate H. -Simpl; Intros; Discriminate H. -Simpl; Intros; Discriminate H. -Save. - -Lemma Zeq_Zminus : (x,y:Z)x=y -> `x-y = 0`. -Intros; Omega. -Save. - -Lemma Zminus_Zeq : (x,y:Z)`x-y=0` -> x=y. -Intros; Omega. -Save. - -Lemma Zmult_Zminus_distr_l : (x,y,z:Z)`(x-y)*z = x*z - y*z`. -Intros; Unfold Zminus. -Rewrite <- Zopp_Zmult. -Apply Zmult_plus_distr_l. -Save. - -Lemma Zmult_Zminus_distr_r : (x,y,z:Z)`z*(x-y) = z*x - z*y`. -Intros; Rewrite (Zmult_sym z `x-y`). -Rewrite (Zmult_sym z x). -Rewrite (Zmult_sym z y). -Apply Zmult_Zminus_distr_l. -Save. - -Lemma Zmult_reg_left : (x,y,z:Z)`z>0` -> `z*x=z*y` -> x=y. -Intros. -Generalize (Zeq_Zminus H0). -Intro. -Apply Zminus_Zeq. -Rewrite <- (Zmult_Zminus_distr_r x y z) in H1. -Elim (Zmult_zero H1). -Omega. -Trivial. -Save. - -Lemma Zmult_reg_right : (x,y,z:Z)`z>0` -> `x*z=y*z` -> x=y. -Intros x y z Hz. -Rewrite (Zmult_sym x z). -Rewrite (Zmult_sym y z). -Intro; Apply Zmult_reg_left with z; Assumption. -Save. - -Lemma Zgt0_le_pred : (y:Z) `y > 0` -> `0 <= (Zpred y)`. -Intro; Unfold Zpred; Omega. -Save. - -Lemma Zlt_Zplus : - (x1,x2,y1,y2:Z)`x1 < x2` -> `y1 < y2` -> `x1 + y1 < x2 + y2`. -Intros; Omega. -Save. - -Lemma Zlt_Zmult_right : (x,y,z:Z)`z>0` -> `x < y` -> `x*z < y*z`. - -Intros; Rewrite (Zs_pred z); Generalize (Zgt0_le_pred H); Intro; -Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`; -[ Simpl; Do 2 (Rewrite Zmult_n_1); Assumption -| Unfold Zs; Intros x0 Hx0; Do 6 (Rewrite Zmult_plus_distr_r); - Repeat Rewrite Zmult_n_1; - Intro; Apply Zlt_Zplus; Assumption -| Assumption ]. -Save. - -Lemma Zlt_Zmult_right2 : (x,y,z:Z)`z>0` -> `x*z < y*z` -> `x < y`. -Intros x y z H; Rewrite (Zs_pred z). -Apply natlike_ind with P:=[z:Z]`x*(Zs z) < y*(Zs z)`->`x < y`. -Simpl; Do 2 Rewrite Zmult_n_1; Auto 1. -Unfold Zs. -Intros x0 Hx0; Repeat Rewrite Zmult_plus_distr_r. -Repeat Rewrite Zmult_n_1. -Omega. (* Auto with zarith. *) -Unfold Zpred; Omega. -Save. - -Lemma Zle_Zmult_right : (x,y,z:Z)`z>0` -> `x <= y` -> `x*z <= y*z`. -Intros x y z Hz Hxy. -Elim (Zle_lt_or_eq x y Hxy). -Intros; Apply Zlt_le_weak. -Apply Zlt_Zmult_right; Trivial. -Intros; Apply Zle_refl. -Rewrite H; Trivial. -Save. - -Lemma Zle_Zmult_right2 : (x,y,z:Z)`z>0` -> `x*z <= y*z` -> `x <= y`. -Intros x y z Hz Hxy. -Elim (Zle_lt_or_eq `x*z` `y*z` Hxy). -Intros; Apply Zlt_le_weak. -Apply Zlt_Zmult_right2 with z; Trivial. -Intros; Apply Zle_refl. -Apply Zmult_reg_right with z; Trivial. -Save. - -Lemma Zgt_Zmult_right : (x,y,z:Z)`z>0` -> `x > y` -> `x*z > y*z`. - -Intros; Apply Zlt_gt; Apply Zlt_Zmult_right; -[ Assumption | Apply Zgt_lt ; Assumption ]. -Save. - -Lemma Zlt_Zmult_left : (x,y,z:Z)`z>0` -> `x < y` -> `z*x < z*y`. - -Intros; -Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y); -Apply Zlt_Zmult_right; Assumption. -Save. - -Lemma Zgt_Zmult_left : (x,y,z:Z)`z>0` -> `x > y` -> `z*x > z*y`. -Intros; -Rewrite (Zmult_sym z x); Rewrite (Zmult_sym z y); -Apply Zgt_Zmult_right; Assumption. -Save. - -Theorem Zcompare_Zmult_right : (x,y,z:Z)` z>0` -> `x ?= y`=`x*z ?= y*z`. - -Intros; Apply Zcompare_egal_dec; -[ Intros; Apply Zlt_Zmult_right; Trivial -| Intro Hxy; Apply [a,b:Z](let (t1,t2)=(Zcompare_EGAL a b) in t2); - Rewrite ((let (t1,t2)=(Zcompare_EGAL x y) in t1) Hxy); Trivial -| Intros; Apply Zgt_Zmult_right; Trivial -]. -Save. - -Theorem Zcompare_Zmult_left : (x,y,z:Z)`z>0` -> `x ?= y`=`z*x ?= z*y`. -Intros; -Rewrite (Zmult_sym z x); -Rewrite (Zmult_sym z y); -Apply Zcompare_Zmult_right; Assumption. -Save. - - -Section diveucl. - -Lemma two_or_two_plus_one : (x:Z) { y:Z | `x = 2*y`}+{ y:Z | `x = 2*y+1`}. -NewDestruct x. -Left ; Split with ZERO; Reflexivity. - -NewDestruct p. -Right ; Split with (POS p); Reflexivity. - -Left ; Split with (POS p); Reflexivity. - -Right ; Split with ZERO; Reflexivity. - -NewDestruct p. -Right ; Split with (NEG (add xH p)). -Rewrite NEG_xI. -Rewrite NEG_add. -Omega. - -Left ; Split with (NEG p); Reflexivity. - -Right ; Split with `-1`; Reflexivity. -Save. - -(* The biggest power of 2 that is stricly less than a *) -(* Easy to compute : replace all "1" of the binary representation by - "0", except the first "1" (or the first one :-) *) -Fixpoint floor_pos [a : positive] : positive := - Cases a of - | xH => xH - | (xO a') => (xO (floor_pos a')) - | (xI b') => (xO (floor_pos b')) - end. - -Definition floor := [a:positive](POS (floor_pos a)). - -Lemma floor_gt0 : (x:positive) `(floor x) > 0`. -Intro. -Compute. -Trivial. -Save. - -Lemma floor_ok : (a:positive) - `(floor a) <= (POS a) < 2*(floor a)`. -Unfold floor. -Induction a. - -Intro p; Simpl. -Repeat Rewrite POS_xI. -Rewrite (POS_xO (xO (floor_pos p))). -Rewrite (POS_xO (floor_pos p)). -Omega. - -Intro p; Simpl. -Repeat Rewrite POS_xI. -Rewrite (POS_xO (xO (floor_pos p))). -Rewrite (POS_xO (floor_pos p)). -Rewrite (POS_xO p). -Omega. - -Simpl; Omega. -Save. - -Lemma Zdiv_eucl_POS : (b:Z)`b > 0` -> (p:positive) - { qr:Z*Z | let (q,r)=qr in `(POS p)=b*q+r` /\ `0 <= r < b` }. - -Induction p. - -(* p => (xI p) *) -(* Notez l'utilisation des nouveaux patterns Intro *) -Intros p' ((q,r), (Hrec1, Hrec2)). -Elim (Z_lt_ge_dec `2*r+1` b); -[ Exists `(2*q, 2*r+1)`; - Rewrite POS_xI; - Rewrite Hrec1; - Split; - [ Rewrite Zmult_Zplus_distr; - Rewrite Zplus_assoc_l; - Rewrite (Zmult_permute b `2`); - Reflexivity - | Omega ] -| Exists `(2*q+1, 2*r+1-b)`; - Rewrite POS_xI; - Rewrite Hrec1; - Split; - [ Do 2 Rewrite Zmult_Zplus_distr; - Unfold Zminus; - Do 2 Rewrite Zplus_assoc_l; - Rewrite <- (Zmult_permute `2` b); - Generalize `b*q`; Intros; Omega - | Omega ] -]. - -(* p => (xO p) *) -Intros p' ((q,r), (Hrec1, Hrec2)). -Elim (Z_lt_ge_dec `2*r` b); -[ Exists `(2*q,2*r)`; - Rewrite POS_xO; - Rewrite Hrec1; - Split; - [ Rewrite Zmult_Zplus_distr; - Rewrite (Zmult_permute b `2`); - Reflexivity - | Omega ] -| Exists `(2*q+1, 2*r-b)`; - Rewrite POS_xO; - Rewrite Hrec1; - Split; - [ Do 2 Rewrite Zmult_Zplus_distr; - Unfold Zminus; - Rewrite <- (Zmult_permute `2` b); - Generalize `b*q`; Intros; Omega - | Omega ] -]. -(* xH *) -Elim (Z_le_gt_dec `2` b); -[ Exists `(0,1)`; Omega -| Exists `(1,0)`; Omega -]. -Save. - -Theorem Zdiv_eucl : (b:Z)`b > 0` -> (a:Z) - { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < b` }. -NewDestruct a; - -[ (* a=0 *) Exists `(0,0)`; Omega -| (* a = (POS p) *) Intros; Apply Zdiv_eucl_POS; Auto -| (* a = (NEG p) *) Intros; Elim (Zdiv_eucl_POS H p); - Intros (q,r) (Hp1, Hp2); - Elim (Z_le_gt_dec r `0`); - [ Exists `(-q,0)`; Split; - [ Apply Zopp_intro; Simpl; Rewrite Hp1; - Rewrite Zero_right; - Rewrite <- Zopp_Zmult; - Rewrite Zmult_Zopp_Zopp; - Generalize `b*q`; Intro; Omega - | Omega - ] - | Exists `(-(q+1),b-r)`; Split; - [ Apply Zopp_intro; - Unfold Zminus; Simpl; Rewrite Hp1; - Repeat Rewrite Zopp_Zplus; - Repeat Rewrite <- Zopp_Zmult; - Rewrite Zmult_Zplus_distr; - Rewrite Zmult_Zopp_Zopp; - Rewrite Zplus_assoc_r; - Apply f_equal with f:=[c:Z]`b*q+c`; - Omega - | Omega ] - ] -]. -Save. - -End diveucl. diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v deleted file mode 100644 index 45ad93aba..000000000 --- a/contrib/omega/Zlogarithm.v +++ /dev/null @@ -1,264 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* `0` (* 1 *) - | (xO q) => (Zs (log_inf q)) (* 2n *) - | (xI q) => (Zs (log_inf q)) (* 2n+1 *) - end. -Fixpoint log_sup [p:positive] : Z := - Cases p of - xH => `0` (* 1 *) - | (xO n) => (Zs (log_sup n)) (* 2n *) - | (xI n) => (Zs (Zs (log_inf n))) (* 2n+1 *) - end. - -Hints Unfold log_inf log_sup. - -(* Then we give the specifications of log_inf and log_sup - and prove their validity *) - -(* Hints Resolve ZERO_le_S : zarith. *) -Hints Resolve Zle_trans : zarith. - -Theorem log_inf_correct : (x:positive) ` 0 <= (log_inf x)` /\ - ` (two_p (log_inf x)) <= (POS x) < (two_p (Zs (log_inf x)))`. -Induction x; Intros; Simpl; -[ Elim H; Intros Hp HR; Clear H; Split; - [ Auto with zarith - | Rewrite (two_p_S (Zs (log_inf p)) (Zle_le_S `0` (log_inf p) Hp)); - Rewrite (two_p_S (log_inf p) Hp); - Rewrite (two_p_S (log_inf p) Hp) in HR; - Rewrite (POS_xI p); Omega ] -| Elim H; Intros Hp HR; Clear H; Split; - [ Auto with zarith - | Rewrite (two_p_S (Zs (log_inf p)) (Zle_le_S `0` (log_inf p) Hp)); - Rewrite (two_p_S (log_inf p) Hp); - Rewrite (two_p_S (log_inf p) Hp) in HR; - Rewrite (POS_xO p); Omega ] -| Unfold two_power_pos; Unfold shift_pos; Simpl; Omega -]. -Save. - -Definition log_inf_correct1 := - [p:positive](proj1 ? ? (log_inf_correct p)). -Definition log_inf_correct2 := - [p:positive](proj2 ? ? (log_inf_correct p)). - -Opaque log_inf_correct1 log_inf_correct2. - -Hints Resolve log_inf_correct1 log_inf_correct2 : zarith. - -Lemma log_sup_correct1 : (p:positive)` 0 <= (log_sup p)`. -Induction p; Intros; Simpl; Auto with zarith. -Save. - -(* For every p, either p is a power of two and (log_inf p)=(log_sup p) - either (log_sup p)=(log_inf p)+1 *) - -Theorem log_sup_log_inf : (p:positive) - either (POS p)=(two_p (log_inf p)) - and_then (POS p)=(two_p (log_sup p)) - or_else ` (log_sup p)=(Zs (log_inf p))`. - -Induction p; Intros; -[ Elim H; Right; Simpl; - Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); - Rewrite POS_xI; Unfold Zs; Omega -| Elim H; Clear H; Intro Hif; - [ Left; Simpl; - Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); - Rewrite (two_p_S (log_sup p0) (log_sup_correct1 p0)); - Rewrite <- (proj1 ? ? Hif); Rewrite <- (proj2 ? ? Hif); - Auto - | Right; Simpl; - Rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); - Rewrite POS_xO; Unfold Zs; Omega ] -| Left; Auto ]. -Save. - -Theorem log_sup_correct2 : (x:positive) - ` (two_p (Zpred (log_sup x))) < (POS x) <= (two_p (log_sup x))`. - -Intro. -Elim (log_sup_log_inf x). -(* x is a power of two and log_sup = log_inf *) -Intros (E1,E2); Rewrite E2. -Split ; [ Apply two_p_pred; Apply log_sup_correct1 | Apply Zle_n ]. -Intros (E1,E2); Rewrite E2. -Rewrite <- (Zpred_Sn (log_inf x)). -Generalize (log_inf_correct2 x); Omega. -Save. - -Lemma log_inf_le_log_sup : - (p:positive) `(log_inf p) <= (log_sup p)`. -Induction p; Simpl; Intros; Omega. -Save. - -Lemma log_sup_le_Slog_inf : - (p:positive) `(log_sup p) <= (Zs (log_inf p))`. -Induction p; Simpl; Intros; Omega. -Save. - -(* Now it's possible to specify and build the Log rounded to the nearest *) - -Fixpoint log_near[x:positive] : Z := - Cases x of - xH => `0` - | (xO xH) => `1` - | (xI xH) => `2` - | (xO y) => (Zs (log_near y)) - | (xI y) => (Zs (log_near y)) - end. - -Theorem log_near_correct1 : (p:positive)` 0 <= (log_near p)`. -Induction p; Simpl; Intros; -[Elim p0; Auto with zarith | Elim p0; Auto with zarith | Trivial with zarith ]. -Intros; Apply Zle_le_S. -Generalize H0; Elim p1; Intros; Simpl; - [ Assumption | Assumption | Apply ZERO_le_POS ]. -Intros; Apply Zle_le_S. -Generalize H0; Elim p1; Intros; Simpl; - [ Assumption | Assumption | Apply ZERO_le_POS ]. -Save. - -Theorem log_near_correct2: (p:positive) - (log_near p)=(log_inf p) -\/(log_near p)=(log_sup p). -Induction p. -Intros p0 [Einf|Esup]. -Simpl. Rewrite Einf. -Case p0; [Left | Left | Right]; Reflexivity. -Simpl; Rewrite Esup. -Elim (log_sup_log_inf p0). -Generalize (log_inf_le_log_sup p0). -Generalize (log_sup_le_Slog_inf p0). -Case p0; Auto with zarith. -Intros; Omega. -Case p0; Intros; Auto with zarith. -Intros p0 [Einf|Esup]. -Simpl. -Repeat Rewrite Einf. -Case p0; Intros; Auto with zarith. -Simpl. -Repeat Rewrite Esup. -Case p0; Intros; Auto with zarith. -Auto. -Save. - -(******************* -Theorem log_near_correct: (p:positive) - `| (two_p (log_near p)) - (POS p) | <= (POS p)-(two_p (log_inf p))` - /\`| (two_p (log_near p)) - (POS p) | <= (two_p (log_sup p))-(POS p)`. -Intro. -Induction p. -Intros p0 [(Einf1,Einf2)|(Esup1,Esup2)]. -Unfold log_near log_inf log_sup. Fold log_near log_inf log_sup. -Rewrite Einf1. -Repeat Rewrite two_p_S. -Case p0; [Left | Left | Right]. - -Split. -Simpl. -Rewrite E1; Case p0; Try Reflexivity. -Compute. -Unfold log_near; Fold log_near. -Unfold log_inf; Fold log_inf. -Repeat Rewrite E1. -Split. -***********************************) - -End Log_pos. - -Section divers. - -(* Number of significative digits. *) - -Definition N_digits := - [x:Z]Cases x of - (POS p) => (log_inf p) - | (NEG p) => (log_inf p) - | ZERO => `0` - end. - -Lemma ZERO_le_N_digits : (x:Z) ` 0 <= (N_digits x)`. -Induction x; Simpl; -[ Apply Zle_n -| Exact log_inf_correct1 -| Exact log_inf_correct1]. -Save. - -Lemma log_inf_shift_nat : - (n:nat)(log_inf (shift_nat n xH))=(inject_nat n). -Induction n; Intros; -[ Try Trivial -| Rewrite -> inj_S; Rewrite <- H; Reflexivity]. -Save. - -Lemma log_sup_shift_nat : - (n:nat)(log_sup (shift_nat n xH))=(inject_nat n). -Induction n; Intros; -[ Try Trivial -| Rewrite -> inj_S; Rewrite <- H; Reflexivity]. -Save. - -(* (Is_power p) means that p is a power of two *) -Fixpoint Is_power[p:positive] : Prop := - Cases p of - xH => True - | (xO q) => (Is_power q) - | (xI q) => False - end. - -Lemma Is_power_correct : - (p:positive) (Is_power p) <-> (Ex [y:nat](p=(shift_nat y xH))). - -Split; -[ Elim p; - [ Simpl; Tauto - | Simpl; Intros; Generalize (H H0); Intro H1; Elim H1; Intros y0 Hy0; - Exists (S y0); Rewrite Hy0; Reflexivity - | Intro; Exists O; Reflexivity] -| Intros; Elim H; Intros; Rewrite -> H0; Elim x; Intros; Simpl; Trivial]. -Save. - -Lemma Is_power_or : (p:positive) (Is_power p)\/~(Is_power p). -Induction p; -[ Intros; Right; Simpl; Tauto -| Intros; Elim H; - [ Intros; Left; Simpl; Exact H0 - | Intros; Right; Simpl; Exact H0] -| Left; Simpl; Trivial]. -Save. - -End divers. diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v deleted file mode 100644 index 1d9727573..000000000 --- a/contrib/omega/Zpower.v +++ /dev/null @@ -1,386 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* nat and Zmult : Z->Z *) - -Lemma Zpower_nat_is_exp : - (n,m:nat)(z:Z) - `(Zpower_nat z (plus n m)) = (Zpower_nat z n)*(Zpower_nat z m)`. - -Intros; Elim n; -[ Simpl; Elim (Zpower_nat z m); Auto with zarith -| Unfold Zpower_nat; Intros; Simpl; Rewrite H; - Apply Zmult_assoc]. -Save. - -(* (Zpower_nat z n) is the n-th power of x when n is an binary - integer (type positive) and z an signed integer (type Z) *) - -Definition Zpower_pos := - [z:Z][n:positive] (iter_pos n Z ([x:Z]`z * x`) `1`). - -(* This theorem shows that powers of unary and binary integers - are the same thing, modulo the function convert : positive -> nat *) - -Theorem Zpower_pos_nat : - (z:Z)(p:positive)(Zpower_pos z p) = (Zpower_nat z (convert p)). - -Intros; Unfold Zpower_pos; Unfold Zpower_nat; Apply iter_convert. -Save. - -(* Using the theorem Zpower_pos_nat and the lemma Zpower_nat_is_exp we - deduce that the function [n:positive](Zpower_pos z n) is a morphism - for add : positive->positive and Zmult : Z->Z *) - -Theorem Zpower_pos_is_exp : - (n,m:positive)(z:Z) - ` (Zpower_pos z (add n m)) = (Zpower_pos z n)*(Zpower_pos z m)`. - -Intros. -Rewrite -> (Zpower_pos_nat z n). -Rewrite -> (Zpower_pos_nat z m). -Rewrite -> (Zpower_pos_nat z (add n m)). -Rewrite -> (convert_add n m). -Apply Zpower_nat_is_exp. -Save. - -Definition Zpower := - [x,y:Z]Cases y of - (POS p) => (Zpower_pos x p) - | ZERO => `1` - | (NEG p) => `0` - end. - -Hints Immediate Zpower_nat_is_exp : zarith. -Hints Immediate Zpower_pos_is_exp : zarith. -Hints Unfold Zpower_pos : zarith. -Hints Unfold Zpower_nat : zarith. - -Lemma Zpower_exp : (x:Z)(n,m:Z) - `n >= 0` -> `m >= 0` -> `(Zpower x (n+m))=(Zpower x n)*(Zpower x m)`. -NewDestruct n; NewDestruct m; Auto with zarith. -Simpl; Intros; Apply Zred_factor0. -Simpl; Auto with zarith. -Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith. -Intros; Compute in H0; Absurd INFERIEUR=INFERIEUR; Auto with zarith. -Save. - -End section1. - -Hints Immediate Zpower_nat_is_exp : zarith. -Hints Immediate Zpower_pos_is_exp : zarith. -Hints Unfold Zpower_pos : zarith. -Hints Unfold Zpower_nat : zarith. - -Section Powers_of_2. - -(* For the powers of two, that will be widely used, a more direct - calculus is possible. We will also prove some properties such - as (x:positive) x < 2^x that are true for all integers bigger - than 2 but more difficult to prove and useless. *) - -(* shift n m computes 2^n * m, or m shifted by n positions *) - -Definition shift_nat := - [n:nat][z:positive](iter_nat n positive xO z). -Definition shift_pos := - [n:positive][z:positive](iter_pos n positive xO z). -Definition shift := - [n:Z][z:positive] - Cases n of - ZERO => z - | (POS p) => (iter_pos p positive xO z) - | (NEG p) => z - end. - -Definition two_power_nat := [n:nat] (POS (shift_nat n xH)). -Definition two_power_pos := [x:positive] (POS (shift_pos x xH)). - -Lemma two_power_nat_S : - (n:nat)` (two_power_nat (S n)) = 2*(two_power_nat n)`. -Intro; Simpl; Apply refl_equal. -Save. - -Lemma shift_nat_plus : - (n,m:nat)(x:positive) - (shift_nat (plus n m) x)=(shift_nat n (shift_nat m x)). - -Intros; Unfold shift_nat; Apply iter_nat_plus. -Save. - -Theorem shift_nat_correct : - (n:nat)(x:positive)(POS (shift_nat n x))=`(Zpower_nat 2 n)*(POS x)`. - -Unfold shift_nat; Induction n; -[ Simpl; Trivial with zarith -| Intros; Replace (Zpower_nat `2` (S n0)) with `2 * (Zpower_nat 2 n0)`; -[ Rewrite <- Zmult_assoc; Rewrite <- (H x); Simpl; Reflexivity -| Auto with zarith ] -]. -Save. - -Theorem two_power_nat_correct : - (n:nat)(two_power_nat n)=(Zpower_nat `2` n). - -Intro n. -Unfold two_power_nat. -Rewrite -> (shift_nat_correct n). -Omega. -Save. - -(* Second we show that two_power_pos and two_power_nat are the same *) -Lemma shift_pos_nat : (p:positive)(x:positive) - (shift_pos p x)=(shift_nat (convert p) x). - -Unfold shift_pos. -Unfold shift_nat. -Intros; Apply iter_convert. -Save. - -Lemma two_power_pos_nat : - (p:positive) (two_power_pos p)=(two_power_nat (convert p)). - -Intro; Unfold two_power_pos; Unfold two_power_nat. -Apply f_equal with f:=POS. -Apply shift_pos_nat. -Save. - -(* Then we deduce that two_power_pos is also correct *) - -Theorem shift_pos_correct : - (p,x:positive) ` (POS (shift_pos p x)) = (Zpower_pos 2 p) * (POS x)`. - -Intros. -Rewrite -> (shift_pos_nat p x). -Rewrite -> (Zpower_pos_nat `2` p). -Apply shift_nat_correct. -Save. - -Theorem two_power_pos_correct : - (x:positive) (two_power_pos x)=(Zpower_pos `2` x). - -Intro. -Rewrite -> two_power_pos_nat. -Rewrite -> Zpower_pos_nat. -Apply two_power_nat_correct. -Save. - -(* Some consequences *) - -Theorem two_power_pos_is_exp : - (x,y:positive) (two_power_pos (add x y)) - =(Zmult (two_power_pos x) (two_power_pos y)). -Intros. -Rewrite -> (two_power_pos_correct (add x y)). -Rewrite -> (two_power_pos_correct x). -Rewrite -> (two_power_pos_correct y). -Apply Zpower_pos_is_exp. -Save. - -(* The exponentiation z -> 2^z for z a signed integer. *) -(* For convenience, we assume that 2^z = 0 for all z <0 *) -(* We could also define a inductive type Log_result with *) -(* 3 contructors Zero | Pos positive -> | minus_infty *) -(* but it's more complexe and not so useful. *) - -Definition two_p := - [x:Z]Cases x of - ZERO => `1` - | (POS y) => (two_power_pos y) - | (NEG y) => `0` - end. - -Theorem two_p_is_exp : - (x,y:Z) ` 0 <= x` -> ` 0 <= y` -> - ` (two_p (x+y)) = (two_p x)*(two_p y)`. -Induction x; -[ Induction y; Simpl; Auto with zarith -| Induction y; - [ Unfold two_p; Rewrite -> (Zmult_sym (two_power_pos p) `1`); - Rewrite -> (Zmult_one (two_power_pos p)); Auto with zarith - | Unfold Zplus; Unfold two_p; - Intros; Apply two_power_pos_is_exp - | Intros; Unfold Zle in H0; Unfold Zcompare in H0; - Absurd SUPERIEUR=SUPERIEUR; Trivial with zarith - ] -| Induction y; - [ Simpl; Auto with zarith - | Intros; Unfold Zle in H; Unfold Zcompare in H; - Absurd (SUPERIEUR=SUPERIEUR); Trivial with zarith - | Intros; Unfold Zle in H; Unfold Zcompare in H; - Absurd (SUPERIEUR=SUPERIEUR); Trivial with zarith - ] -]. -Save. - -Lemma two_p_gt_ZERO : (x:Z) ` 0 <= x` -> ` (two_p x) > 0`. -Induction x; Intros; -[ Simpl; Omega -| Simpl; Unfold two_power_pos; Apply POS_gt_ZERO -| Absurd ` 0 <= (NEG p)`; - [ Simpl; Unfold Zle; Unfold Zcompare; - Do 2 Unfold not; Auto with zarith - | Assumption ] -]. -Save. - -Lemma two_p_S : (x:Z) ` 0 <= x` -> - `(two_p (Zs x)) = 2 * (two_p x)`. -Intros; Unfold Zs. -Rewrite (two_p_is_exp x `1` H (ZERO_le_POS xH)). -Apply Zmult_sym. -Save. - -Lemma two_p_pred : - (x:Z)` 0 <= x` -> ` (two_p (Zpred x)) < (two_p x)`. -Intros; Apply natlike_ind -with P:=[x:Z]` (two_p (Zpred x)) < (two_p x)`; -[ Simpl; Unfold Zlt; Auto with zarith -| Intros; Elim (Zle_lt_or_eq `0` x0 H0); - [ Intros; - Replace (two_p (Zpred (Zs x0))) - with (two_p (Zs (Zpred x0))); - [ Rewrite -> (two_p_S (Zpred x0)); - [ Rewrite -> (two_p_S x0); - [ Omega - | Assumption] - | Apply Zlt_ZERO_pred_le_ZERO; Assumption] - | Rewrite <- (Zs_pred x0); Rewrite <- (Zpred_Sn x0); Trivial with zarith] - | Intro Hx0; Rewrite <- Hx0; Simpl; Unfold Zlt; Auto with zarith] -| Assumption]. -Save. - -Lemma Zlt_lt_double : (x,y:Z) ` 0 <= x < y` -> ` x < 2*y`. -Intros; Omega. Save. - -End Powers_of_2. - -Hints Resolve two_p_gt_ZERO : zarith. -Hints Immediate two_p_pred two_p_S : zarith. - -Section power_div_with_rest. - -(* Division by a power of two - To n:Z and p:positive q,r are associated such that - n = 2^p.q + r and 0 <= r < 2^p *) - -(* Invariant : d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d' *) -Definition Zdiv_rest_aux := - [qrd:(Z*Z)*Z] - let (qr,d)=qrd in let (q,r)=qr in - (Cases q of - ZERO => ` (0, r)` - | (POS xH) => ` (0, d + r)` - | (POS (xI n)) => ` ((POS n), d + r)` - | (POS (xO n)) => ` ((POS n), r)` - | (NEG xH) => ` (-1, d + r)` - | (NEG (xI n)) => ` ((NEG n) - 1, d + r)` - | (NEG (xO n)) => ` ((NEG n), r)` - end, ` 2*d`). - -Definition Zdiv_rest := - [x:Z][p:positive]let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in qr. - -Lemma Zdiv_rest_correct1 : - (x:Z)(p:positive) - let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in d=(two_power_pos p). - -Intros x p; -Rewrite (iter_convert p ? Zdiv_rest_aux ((x,`0`),`1`)); -Rewrite (two_power_pos_nat p); -Elim (convert p); Simpl; -[ Trivial with zarith -| Intro n; Rewrite (two_power_nat_S n); - Unfold 2 Zdiv_rest_aux; - Elim (iter_nat n (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)); - NewDestruct a; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. -Save. - -Lemma Zdiv_rest_correct2 : - (x:Z)(p:positive) - let (qr,d)=(iter_pos p ? Zdiv_rest_aux ((x,`0`),`1`)) in - let (q,r)=qr in - ` x=q*d + r` /\ ` 0 <= r < d`. - -Intros; Apply iter_pos_invariant with - f:=Zdiv_rest_aux - Inv:=[qrd:(Z*Z)*Z]let (qr,d)=qrd in let (q,r)=qr in - ` x=q*d + r` /\ ` 0 <= r < d`; -[ Intro x0; Elim x0; Intro y0; Elim y0; - Intros q r d; Unfold Zdiv_rest_aux; - Elim q; - [ Omega - | NewDestruct p0; - [ Rewrite POS_xI; Intro; Elim H; Intros; Split; - [ Rewrite H0; Rewrite Zplus_assoc; - Rewrite Zmult_plus_distr_l; - Rewrite Zmult_1_n; Rewrite Zmult_assoc; - Rewrite (Zmult_sym (POS p0) `2`); Apply refl_equal - | Omega ] - | Rewrite POS_xO; Intro; Elim H; Intros; Split; - [ Rewrite H0; - Rewrite Zmult_assoc; Rewrite (Zmult_sym (POS p0) `2`); - Apply refl_equal - | Omega ] - | Omega ] - | NewDestruct p0; - [ Rewrite NEG_xI; Unfold Zminus; Intro; Elim H; Intros; Split; - [ Rewrite H0; Rewrite Zplus_assoc; - Apply f_equal with f:=[z:Z]`z+r`; - Do 2 (Rewrite Zmult_plus_distr_l); - Rewrite Zmult_assoc; - Rewrite (Zmult_sym (NEG p0) `2`); - Rewrite <- Zplus_assoc; - Apply f_equal with f:=[z:Z]`2 * (NEG p0) * d + z`; - Omega - | Omega ] - | Rewrite NEG_xO; Unfold Zminus; Intro; Elim H; Intros; Split; - [ Rewrite H0; - Rewrite Zmult_assoc; Rewrite (Zmult_sym (NEG p0) `2`); - Apply refl_equal - | Omega ] - | Omega ] ] -| Omega]. -Save. - -Inductive Set Zdiv_rest_proofs[x:Z; p:positive] := - Zdiv_rest_proof : (q:Z)(r:Z) - `x = q * (two_power_pos p) + r` - -> `0 <= r` - -> `r < (two_power_pos p)` - -> (Zdiv_rest_proofs x p). - -Lemma Zdiv_rest_correct : - (x:Z)(p:positive)(Zdiv_rest_proofs x p). -Intros x p. -Generalize (Zdiv_rest_correct1 x p); Generalize (Zdiv_rest_correct2 x p). -Elim (iter_pos p (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)). -Induction a. -Intros. -Elim H; Intros H1 H2; Clear H. -Rewrite -> H0 in H1; Rewrite -> H0 in H2; -Elim H2; Intros; -Apply Zdiv_rest_proof with q:=a0 r:=b; Assumption. -Save. - -End power_div_with_rest. -- cgit v1.2.3