summaryrefslogtreecommitdiff
path: root/theories/ZArith/Zlogarithm.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /theories/ZArith/Zlogarithm.v
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/ZArith/Zlogarithm.v')
-rw-r--r--theories/ZArith/Zlogarithm.v265
1 files changed, 265 insertions, 0 deletions
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
new file mode 100644
index 00000000..b575de88
--- /dev/null
+++ b/theories/ZArith/Zlogarithm.v
@@ -0,0 +1,265 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: Zlogarithm.v,v 1.14.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
+
+(**********************************************************************)
+(** 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)]
+ i.e. [Log_inf x] is the biggest integer that is smaller than [Log x]
+ - [Log_sup]: [y = (Log_sup x) iff 2^(y-1) < x <= 2^y]
+ i.e. [Log_inf x] is the smallest integer that is bigger than [Log x]
+ - [Log_nearest]: [y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)]
+ i.e. [Log_nearest x] is the integer nearest from [Log x] *)
+
+Require Import ZArith_base.
+Require Import Omega.
+Require Import Zcomplements.
+Require Import Zpower.
+Open Local Scope Z_scope.
+
+Section Log_pos. (* Log of positive integers *)
+
+(** First we build [log_inf] and [log_sup] *)
+
+Fixpoint log_inf (p:positive) : Z :=
+ match p with
+ | xH => 0 (* 1 *)
+ | xO q => Zsucc (log_inf q) (* 2n *)
+ | xI q => Zsucc (log_inf q) (* 2n+1 *)
+ end.
+Fixpoint log_sup (p:positive) : Z :=
+ match p with
+ | xH => 0 (* 1 *)
+ | xO n => Zsucc (log_sup n) (* 2n *)
+ | xI n => Zsucc (Zsucc (log_inf n)) (* 2n+1 *)
+ end.
+
+Hint Unfold log_inf log_sup.
+
+(** Then we give the specifications of [log_inf] and [log_sup]
+ and prove their validity *)
+
+(*i Hints Resolve ZERO_le_S : zarith. i*)
+Hint Resolve Zle_trans: zarith.
+
+Theorem log_inf_correct :
+ forall x:positive,
+ 0 <= log_inf x /\ two_p (log_inf x) <= Zpos x < two_p (Zsucc (log_inf x)).
+simple induction x; intros; simpl in |- *;
+ [ elim H; intros Hp HR; clear H; split;
+ [ auto with zarith
+ | conditional apply Zle_le_succ; trivial rewrite
+ two_p_S with (x := Zsucc (log_inf p));
+ conditional trivial rewrite two_p_S;
+ conditional trivial rewrite two_p_S in HR; rewrite (BinInt.Zpos_xI p);
+ omega ]
+ | elim H; intros Hp HR; clear H; split;
+ [ auto with zarith
+ | conditional apply Zle_le_succ; trivial rewrite
+ two_p_S with (x := Zsucc (log_inf p));
+ conditional trivial rewrite two_p_S;
+ conditional trivial rewrite two_p_S in HR; rewrite (BinInt.Zpos_xO p);
+ omega ]
+ | unfold two_power_pos in |- *; unfold shift_pos in |- *; simpl in |- *;
+ omega ].
+Qed.
+
+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.
+
+Hint Resolve log_inf_correct1 log_inf_correct2: zarith.
+
+Lemma log_sup_correct1 : forall p:positive, 0 <= log_sup p.
+simple induction p; intros; simpl in |- *; auto with zarith.
+Qed.
+
+(** 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 :
+ forall p:positive,
+ IF Zpos p = two_p (log_inf p) then Zpos p = two_p (log_sup p)
+ else log_sup p = Zsucc (log_inf p).
+
+simple induction p; intros;
+ [ elim H; right; simpl in |- *;
+ rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
+ rewrite BinInt.Zpos_xI; unfold Zsucc in |- *; omega
+ | elim H; clear H; intro Hif;
+ [ left; simpl in |- *;
+ 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 in |- *;
+ rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
+ rewrite BinInt.Zpos_xO; unfold Zsucc in |- *;
+ omega ]
+ | left; auto ].
+Qed.
+
+Theorem log_sup_correct2 :
+ forall x:positive, two_p (Zpred (log_sup x)) < Zpos 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_refl ].
+intros [E1 E2]; rewrite E2.
+rewrite <- (Zpred_succ (log_inf x)).
+generalize (log_inf_correct2 x); omega.
+Qed.
+
+Lemma log_inf_le_log_sup : forall p:positive, log_inf p <= log_sup p.
+simple induction p; simpl in |- *; intros; omega.
+Qed.
+
+Lemma log_sup_le_Slog_inf : forall p:positive, log_sup p <= Zsucc (log_inf p).
+simple induction p; simpl in |- *; intros; omega.
+Qed.
+
+(** Now it's possible to specify and build the [Log] rounded to the nearest *)
+
+Fixpoint log_near (x:positive) : Z :=
+ match x with
+ | xH => 0
+ | xO xH => 1
+ | xI xH => 2
+ | xO y => Zsucc (log_near y)
+ | xI y => Zsucc (log_near y)
+ end.
+
+Theorem log_near_correct1 : forall p:positive, 0 <= log_near p.
+simple induction p; simpl in |- *; intros;
+ [ elim p0; auto with zarith
+ | elim p0; auto with zarith
+ | trivial with zarith ].
+intros; apply Zle_le_succ.
+generalize H0; elim p1; intros; simpl in |- *;
+ [ assumption | assumption | apply Zorder.Zle_0_pos ].
+intros; apply Zle_le_succ.
+generalize H0; elim p1; intros; simpl in |- *;
+ [ assumption | assumption | apply Zorder.Zle_0_pos ].
+Qed.
+
+Theorem log_near_correct2 :
+ forall p:positive, log_near p = log_inf p \/ log_near p = log_sup p.
+simple induction p.
+intros p0 [Einf| Esup].
+simpl in |- *. rewrite Einf.
+case p0; [ left | left | right ]; reflexivity.
+simpl in |- *; 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 in |- *.
+repeat rewrite Einf.
+case p0; intros; auto with zarith.
+simpl in |- *.
+repeat rewrite Esup.
+case p0; intros; auto with zarith.
+auto.
+Qed.
+
+(*i******************
+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.
+**********************************i*)
+
+End Log_pos.
+
+Section divers.
+
+(** Number of significative digits. *)
+
+Definition N_digits (x:Z) :=
+ match x with
+ | Zpos p => log_inf p
+ | Zneg p => log_inf p
+ | Z0 => 0
+ end.
+
+Lemma ZERO_le_N_digits : forall x:Z, 0 <= N_digits x.
+simple induction x; simpl in |- *;
+ [ apply Zle_refl | exact log_inf_correct1 | exact log_inf_correct1 ].
+Qed.
+
+Lemma log_inf_shift_nat : forall n:nat, log_inf (shift_nat n 1) = Z_of_nat n.
+simple induction n; intros;
+ [ try trivial | rewrite Znat.inj_S; rewrite <- H; reflexivity ].
+Qed.
+
+Lemma log_sup_shift_nat : forall n:nat, log_sup (shift_nat n 1) = Z_of_nat n.
+simple induction n; intros;
+ [ try trivial | rewrite Znat.inj_S; rewrite <- H; reflexivity ].
+Qed.
+
+(** [Is_power p] means that p is a power of two *)
+Fixpoint Is_power (p:positive) : Prop :=
+ match p with
+ | xH => True
+ | xO q => Is_power q
+ | xI q => False
+ end.
+
+Lemma Is_power_correct :
+ forall p:positive, Is_power p <-> (exists y : nat, p = shift_nat y 1).
+
+split;
+ [ elim p;
+ [ simpl in |- *; tauto
+ | simpl in |- *; intros; generalize (H H0); intro H1; elim H1;
+ intros y0 Hy0; exists (S y0); rewrite Hy0; reflexivity
+ | intro; exists 0%nat; reflexivity ]
+ | intros; elim H; intros; rewrite H0; elim x; intros; simpl in |- *; trivial ].
+Qed.
+
+Lemma Is_power_or : forall p:positive, Is_power p \/ ~ Is_power p.
+simple induction p;
+ [ intros; right; simpl in |- *; tauto
+ | intros; elim H;
+ [ intros; left; simpl in |- *; exact H0
+ | intros; right; simpl in |- *; exact H0 ]
+ | left; simpl in |- *; trivial ].
+Qed.
+
+End divers.
+
+
+
+
+
+