Numbers: misc improvements

 - Add alternate specifications of pow and sqrt
 - Slightly more general pow_lt_mono_r
 - More explicit equivalence of Plog2_Z and log_inf
 - Nicer proofs in Zpower

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13607 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 11 deletions

diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index 7d5b41121..7bb23db62 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -18,22 +18,16 @@
     - [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.
+Require Import ZArith_base Omega Zcomplements Zlog_def Zpower.
+Local Open 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.
+  (** [log_inf] is exactly the same as the new [Plog2_Z] *)
+
+  Definition log_inf : positive -> Z := Eval red in Plog2_Z.
 
   Fixpoint log_sup (p:positive) : Z :=
     match p with
@@ -44,6 +38,9 @@ Section Log_pos. (* Log of positive integers *)
 
   Hint Unfold log_inf log_sup.
 
+  Lemma Zlog2_log_inf : forall p, Zlog2 (Zpos p) = log_inf p.
+  Proof. reflexivity. Qed.
+
   (** Then we give the specifications of [log_inf] and [log_sup]
     and prove their validity *)