diff options
Diffstat (limited to 'theories/ZArith/Zlogarithm.v')
| -rw-r--r-- | theories/ZArith/Zlogarithm.v | 37 |
1 files changed, 18 insertions, 19 deletions
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index d8f4f236..70a959c2 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zlogarithm.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id$ i*) (**********************************************************************) -(** The integer logarithms with base 2. +(** The integer logarithms with base 2. There are three logarithms, depending on the rounding of the real 2-based logarithm: @@ -27,7 +27,7 @@ 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 := @@ -43,31 +43,30 @@ Section Log_pos. (* Log of positive integers *) | 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] + + (** Then we give the specifications of [log_inf] and [log_sup] and prove their validity *) - + 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)). + Proof. 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); + | rewrite two_p_S with (x := Zsucc (log_inf p)) by (apply Zle_le_succ; trivial); + rewrite two_p_S by trivial; + rewrite two_p_S in HR by trivial; 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); + | rewrite two_p_S with (x := Zsucc (log_inf p)) by (apply Zle_le_succ; trivial); + rewrite two_p_S by trivial; + rewrite two_p_S in HR by trivial; rewrite (BinInt.Zpos_xO p); omega ] | unfold two_power_pos in |- *; unfold shift_pos in |- *; simpl in |- *; omega ]. @@ -101,11 +100,11 @@ Section Log_pos. (* Log of positive integers *) [ 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); + 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 |- *; + rewrite BinInt.Zpos_xO; unfold Zsucc in |- *; omega ] | left; auto ]. Qed. @@ -142,7 +141,7 @@ Section Log_pos. (* Log of positive integers *) | xI xH => 2 | xO y => Zsucc (log_near y) | xI y => Zsucc (log_near y) - end. + end. Theorem log_near_correct1 : forall p:positive, 0 <= log_near p. Proof. @@ -187,7 +186,7 @@ End Log_pos. Section divers. (** Number of significative digits. *) - + Definition N_digits (x:Z) := match x with | Zpos p => log_inf p |