diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-18 14:46:04 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-18 14:46:04 +0000 |
commit | c114c99ac237c34e2a24aeec2344efbcd7f1e34d (patch) | |
tree | 2648ed1b6fd72099c11cfaa55fdaa3641756d5aa /theories/ZArith/Zlogarithm.v | |
parent | a4c788c1492a85f7dcf2f61af218ce5d9a762e1a (diff) |
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
Diffstat (limited to 'theories/ZArith/Zlogarithm.v')
-rw-r--r-- | theories/ZArith/Zlogarithm.v | 264 |
1 files changed, 264 insertions, 0 deletions
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v new file mode 100644 index 000000000..45ad93aba --- /dev/null +++ b/theories/ZArith/Zlogarithm.v @@ -0,0 +1,264 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* $Id$ *) + +(****************************************************************************) +(* The integer logarithms with base 2. There are three logarithms, *) +(* depending on the rounding of the real 2-based logarithm : *) +(* *) +(* Log_inf : y = (Log_inf x) iff 2^y <= x < 2^(y+1) *) +(* Log_sup : y = (Log_sup x) iff 2^(y-1) < x <= 2^y *) +(* Log_nearest : y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2) *) +(* *) +(* (Log_inf x) is the biggest integer that is smaller than (Log x) *) +(* (Log_inf x) is the smallest integer that is bigger than (Log x) *) +(* (Log_nearest x) is the integer nearest from (Log x). *) +(****************************************************************************) + +Require ZArith. +Require Omega. +Require Zcomplements. +Require Zpower. + +Section Log_pos. (* Log of positive integers *) + +(* First we build log_inf and log_sup *) + +Fixpoint log_inf [p:positive] : Z := + Cases p of + xH => `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. |