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 --- .depend.coq | 8 +- Makefile | 7 +- contrib/omega/Zcomplements.v | 306 -------------------------------- contrib/omega/Zlogarithm.v | 264 ---------------------------- contrib/omega/Zpower.v | 386 ----------------------------------------- theories/ZArith/Wf_Z.v | 50 ++++++ theories/ZArith/Zcomplements.v | 359 ++++++++++++++++++++++++++++++++++++++ theories/ZArith/Zhints.v | 1 + theories/ZArith/Zlogarithm.v | 264 ++++++++++++++++++++++++++++ theories/ZArith/Zpower.v | 386 +++++++++++++++++++++++++++++++++++++++++ theories/ZArith/zarith_aux.v | 33 ++++ 11 files changed, 1100 insertions(+), 964 deletions(-) delete mode 100644 contrib/omega/Zcomplements.v delete mode 100644 contrib/omega/Zlogarithm.v delete mode 100644 contrib/omega/Zpower.v create mode 100644 theories/ZArith/Zcomplements.v create mode 100644 theories/ZArith/Zlogarithm.v create mode 100644 theories/ZArith/Zpower.v diff --git a/.depend.coq b/.depend.coq index eb774f7956..e9f6c7de7c 100644 --- a/.depend.coq +++ b/.depend.coq @@ -28,10 +28,7 @@ contrib/ring/Ring_normalize.vo: contrib/ring/Ring_normalize.v contrib/ring/Ring_ contrib/ring/ArithRing.vo: contrib/ring/ArithRing.v contrib/ring/Ring.vo theories/Arith/Arith.vo theories/Logic/Eqdep_dec.vo contrib/romega/ROmega.vo: contrib/romega/ROmega.v contrib/omega/Omega.vo contrib/romega/ReflOmegaCore.vo contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/PolyList.vo theories/Bool/Bool.vo theories/ZArith/ZArith.vo -contrib/omega/Zcomplements.vo: contrib/omega/Zcomplements.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo -contrib/omega/Zpower.vo: contrib/omega/Zpower.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/OmegaSyntax.vo: contrib/omega/OmegaSyntax.v -contrib/omega/Zlogarithm.vo: contrib/omega/Zlogarithm.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo contrib/omega/Zcomplements.vo contrib/omega/Zpower.vo contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith.vo theories/Arith/Minus.vo contrib/omega/OmegaSyntax.vo theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/PolyList.vo theories/Sets/Multiset.vo @@ -46,7 +43,7 @@ theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rseries theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rderiv.vo theories/Logic/Classical.vo theories/Arith/Compare.vo theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rfunctions.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Logic/Classical_Prop.vo theories/Reals/DiscrR.vo contrib/fourier/Fourier.vo theories/Reals/SplitAbsolu.vo -theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo contrib/omega/Omega.vo contrib/omega/Zpower.vo +theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rlimit.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/DiscrR.vo theories/Reals/Rbasic_fun.vo @@ -117,6 +114,9 @@ theories/Lists/Streams.vo: theories/Lists/Streams.v theories/Lists/ListSet.vo: theories/Lists/ListSet.v theories/Lists/PolyList.vo theories/Lists/PolyListSyntax.vo: theories/Lists/PolyListSyntax.v theories/Lists/PolyList.vo theories/Lists/List.vo: theories/Lists/List.v theories/Arith/Le.vo +theories/ZArith/Zcomplements.vo: theories/ZArith/Zcomplements.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/Arith/Wf_nat.vo +theories/ZArith/Zpower.vo: theories/ZArith/Zpower.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo +theories/ZArith/Zlogarithm.vo: theories/ZArith/Zlogarithm.v theories/ZArith/ZArith.vo contrib/omega/Omega.vo theories/ZArith/Zcomplements.vo theories/ZArith/Zpower.vo theories/ZArith/Zhints.vo: theories/ZArith/Zhints.v theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/ZArith/Zmisc.vo theories/ZArith/Wf_Z.vo theories/ZArith/zarith_aux.vo: theories/ZArith/zarith_aux.v theories/Arith/Arith.vo theories/ZArith/fast_integer.vo theories/ZArith/Zmisc.vo: theories/ZArith/Zmisc.v theories/ZArith/fast_integer.vo theories/ZArith/zarith_aux.vo theories/ZArith/auxiliary.vo theories/ZArith/Zsyntax.vo theories/Bool/Bool.vo diff --git a/Makefile b/Makefile index 65046fa90a..8117134042 100644 --- a/Makefile +++ b/Makefile @@ -396,7 +396,8 @@ ZARITHVO=theories/ZArith/Wf_Z.vo theories/ZArith/Zsyntax.vo \ theories/ZArith/ZArith.vo theories/ZArith/auxiliary.vo \ theories/ZArith/ZArith_dec.vo theories/ZArith/fast_integer.vo \ theories/ZArith/Zmisc.vo theories/ZArith/zarith_aux.vo \ - theories/ZArith/Zhints.vo + theories/ZArith/Zhints.vo theories/ZArith/Zlogarithm.vo \ + theories/ZArith/Zpower.vo theories/ZArith/Zcomplements.vo LISTSVO=theories/Lists/List.vo theories/Lists/PolyListSyntax.vo \ theories/Lists/ListSet.vo theories/Lists/Streams.vo \ @@ -493,9 +494,7 @@ CORRECTNESSVO=contrib/correctness/Arrays.vo \ contrib/correctness/Tuples.vo # contrib/correctness/ProgramsExtraction.vo -OMEGAVO = contrib/omega/Omega.vo contrib/omega/Zlogarithm.vo \ - contrib/omega/OmegaSyntax.vo contrib/omega/Zpower.vo \ - contrib/omega/Zcomplements.vo +OMEGAVO = contrib/omega/Omega.vo contrib/omega/OmegaSyntax.vo ROMEGAVO = contrib/romega/ReflOmegaCore.vo contrib/romega/ROmega.vo diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v deleted file mode 100644 index 90d1f59408..0000000000 --- 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 45ad93aba0..0000000000 --- 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 1d97275736..0000000000 --- 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. diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 65571855e1..5935555869 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -84,6 +84,15 @@ Intros Hn; Elim Hn; Intros. Rewrite -> H1; Apply H. Save. +Lemma inject_nat_set : + (P:Z->Set)((n:nat)(P (inject_nat n))) -> + (x:Z) `0 <= x` -> (P x). +Intros. +Specialize (inject_nat_complete_inf x H0). +Intros Hn; Elim Hn; Intros. +Rewrite -> p; Apply H. +Save. + Lemma ZERO_le_inj : (n:nat) `0 <= (inject_nat n)`. Induction n; Simpl; Intros; @@ -102,6 +111,17 @@ Intros; Apply inject_nat_prop; | Assumption]. Save. +Lemma natlike_rec : (P:Z->Set) (P `0`) -> + ((x:Z)(`0 <= x` -> (P x) -> (P (Zs x)))) -> + (x:Z) `0 <= x` -> (P x). +Intros; Apply inject_nat_set; +[ Induction n; + [ Simpl; Assumption + | Intros; Rewrite -> (inj_S n0); + Exact (H0 (inject_nat n0) (ZERO_le_inj n0) H2) ] +| Assumption]. +Save. + Lemma Z_lt_induction : (P:Z->Prop) ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x)) @@ -131,3 +151,33 @@ Apply Zgt_S_le. Apply Zlt_gt. Intuition. Assumption. Save. + +Lemma Z_lt_rec : + (P:Z->Set) + ((x:Z)((y:Z)`0 <= y < x`->(P y))->(P x)) + -> (x:Z)`0 <= x`->(P x). +Proof. +Intros P H x Hx. +Cut (x:Z)`0 <= x`->(y:Z)`0 <= y < x`->(P y). +Intro. +Apply (H0 (Zs x)). +Auto with zarith. + +Split; [ Assumption | Exact (Zlt_n_Sn x) ]. + +Intros x0 Hx0; Generalize Hx0; Pattern x0; Apply natlike_rec. +Intros. +Absurd `0 <= 0`; Try Assumption. +Apply Zgt_not_le. +Apply Zgt_le_trans with m:=y. +Apply Zlt_gt. +Intuition. Intuition. + +Intros. Apply H. Intros. +Apply (H1 H0). +Split; [ Intuition | Idtac ]. +Apply Zlt_le_trans with y. Intuition. +Apply Zgt_S_le. Apply Zlt_gt. Intuition. + +Assumption. +Save. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v new file mode 100644 index 0000000000..69ce3b6f89 --- /dev/null +++ b/theories/ZArith/Zcomplements.v @@ -0,0 +1,359 @@ +(***********************************************************************) +(* 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. + +Theorem Zdiv_eucl_extended : (b:Z)`b <> 0` -> (a:Z) + { qr:Z*Z | let (q,r)=qr in `a=b*q+r` /\ `0 <= r < |b|` }. +Proof. +Intros b Hb a. +Elim (Z_le_gt_dec `0` b);Intro Hb'. +Cut `b>0`;[Intro Hb''|Omega]. +Rewrite Zabs_eq;[Apply Zdiv_eucl;Assumption|Assumption]. +Cut `-b>0`;[Intro Hb''|Omega]. +Elim (Zdiv_eucl Hb'' a);Intros qr. +Elim qr;Intros q r Hqr. +Exists (pair ? ? `-q` r). +Elim Hqr;Intros. +Split. +Rewrite <- Zmult_Zopp_left;Assumption. +Rewrite Zabs_non_eq;[Assumption|Omega]. +Save. + +End diveucl. + +(* Two more induction principles upon Z. *) + +Theorem Z_lt_abs_rec : (P: Z -> Set) + ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p). +Intros P HP p. +LetTac Q:=[z]`0<=z`->(P z)*(P `-z`). +Cut (Q `|p|`);[Intros|Apply (Z_lt_rec Q);Auto with zarith]. +Elim (Zabs_dec p);Intro eq;Rewrite eq;Elim H;Auto with zarith. +Unfold Q;Clear Q;Intros. +Apply pair;Apply HP. +Rewrite Zabs_eq;Auto;Intros. +Elim (H `|m|`);Intros;Auto with zarith. +Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial. +Rewrite Zabs_non_eq;Auto with zarith. +Rewrite Zopp_Zopp;Intros. +Elim (H `|m|`);Intros;Auto with zarith. +Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial. +Qed. + +Theorem Z_lt_abs_induction : (P: Z -> Prop) + ((n: Z) ((m: Z) `|m|<|n|` -> (P m)) -> (P n)) -> (p: Z) (P p). +Intros P HP p. +LetTac Q:=[z]`0<=z`->(P z) /\ (P `-z`). +Cut (Q `|p|`);[Intros|Apply (Z_lt_induction Q);Auto with zarith]. +Elim (Zabs_dec p);Intro eq;Rewrite eq;Elim H;Auto with zarith. +Unfold Q;Clear Q;Intros. +Split;Apply HP. +Rewrite Zabs_eq;Auto;Intros. +Elim (H `|m|`);Intros;Auto with zarith. +Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial. +Rewrite Zabs_non_eq;Auto with zarith. +Rewrite Zopp_Zopp;Intros. +Elim (H `|m|`);Intros;Auto with zarith. +Elim (Zabs_dec m);Intro eq;Rewrite eq;Trivial. +Qed. diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v index d54d1a0a26..19f71b3221 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.v @@ -69,6 +69,7 @@ Hints Resolve Zle_min_r (* :(n,m:Z)`(Zmin n m) <= m` *) Zle_reg_l (* :(n,m,p:Z)`n <= m`->`p+n <= p+m` *) Zle_reg_r (* :(a,b,c:Z)`a <= b`->`a+c <= b+c` *) + Zabs_pos (* :(x:Z)`0 <= |x|` *) (* B) Irreversible simplification lemmas : Probably to be declared as *) (* hints, when no other simplification is possible *) diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v new file mode 100644 index 0000000000..45ad93aba0 --- /dev/null +++ b/theories/ZArith/Zlogarithm.v @@ -0,0 +1,264 @@ +(***********************************************************************) +(* 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/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v new file mode 100644 index 0000000000..1d97275736 --- /dev/null +++ b/theories/ZArith/Zpower.v @@ -0,0 +1,386 @@ +(***********************************************************************) +(* 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. diff --git a/theories/ZArith/zarith_aux.v b/theories/ZArith/zarith_aux.v index 7eb1e37c23..bdb56fb910 100644 --- a/theories/ZArith/zarith_aux.v +++ b/theories/ZArith/zarith_aux.v @@ -28,6 +28,14 @@ Definition Zgt := [x,y:Z](Zcompare x y) = SUPERIEUR. Definition Zle := [x,y:Z]~(Zcompare x y) = SUPERIEUR. Definition Zge := [x,y:Z]~(Zcompare x y) = INFERIEUR. +(* Sign function *) +Definition Zsgn [z:Z] : Z := + Cases z of + ZERO => ZERO + | (POS p) => (POS xH) + | (NEG p) => (NEG xH) + end. + (*s Absolu function *) Definition absolu [x:Z] : nat := Cases x of @@ -50,6 +58,31 @@ NewDestruct x; Auto with arith. Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith. Save. +Lemma Zabs_non_eq : (x:Z) (Zle x ZERO) -> (Zabs x)=(Zopp x). +Proof. +NewDestruct x; Auto with arith. +Compute; Intros; Absurd SUPERIEUR=SUPERIEUR; Trivial with arith. +Save. + +Lemma Zabs_dec : (x:Z){x=(Zabs x)}+{x=(Zopp (Zabs x))}. +Proof. +NewDestruct x;Auto with arith. +Save. + +Lemma Zabs_pos : (x:Z)(Zle ZERO (Zabs x)). +NewDestruct x;Auto with arith; Compute; Intros H;Inversion H. +Save. + +Lemma Zsgn_Zabs: (x:Z)(Zmult x (Zsgn x))=(Zabs x). +Proof. +Destruct x;Intros;Rewrite Zmult_sym;Auto with arith. +Save. + +Lemma Zabs_Zsgn: (x:Z)(Zabs x)=(Zmult (Zsgn x) x). +Proof. +Destruct x;Intros;Auto with arith. +Qed. + (*s From nat to Z *) Definition inject_nat := [x:nat]Cases x of -- cgit v1.2.3