Numbers : log2. Abstraction, properties and implementations.

 Btw, we finally declare the original Zpower as the power on Z.
 We should switch to a more efficient one someday, but in the
 meantime BigN is proved with respect to the old one.

 TODO: reform Zlogarithm with respect to Zlog_def

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

19 files changed, 432 insertions, 67 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 6e6cd7f0fc..47286c729e 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 Require Export NZAxioms.
-Require Import NZPow NZSqrt.
+Require Import NZPow NZSqrt NZLog.
 
 (** We obtain integers by postulating that successor of predecessor
     is identity. *)
@@ -70,16 +70,16 @@ Module Type Parity (Import Z : ZAxiomsMiniSig').
  Axiom odd_spec : forall n, odd n = true <-> Odd n.
 End Parity.
 
-(** For the power and sqrt functions, the NZ axiomatizations are enough. *)
+(** For pow sqrt log2, the NZ axiomatizations are enough. *)
 
 (** Let's group everything *)
 
 Module Type ZAxiomsSig :=
   ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
-   <+ NZPow.NZPow <+ NZSqrt.NZSqrt.
+   <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2.
 Module Type ZAxiomsSig' :=
   ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
-   <+ NZPow.NZPow' <+ NZSqrt.NZSqrt'.
+   <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2.
 
 
 (** Division is left apart, since many different flavours are available *)
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 8b34e5b2db..d2e9626737 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -12,4 +12,4 @@ Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow.
 
 Module Type ZProp (Z:ZAxiomsSig) :=
  ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z
- <+ NZSqrt.NZSqrtProp Z Z.
+ <+ NZSqrt.NZSqrtProp Z Z <+ NZLog.NZLog2Prop Z Z Z.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 92be49bdaf..b2bf8703ea 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -63,10 +63,13 @@ Arguments Scope BigZ.eq_bool [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.pow_pos [bigZ_scope positive_scope].
 Arguments Scope BigZ.pow_N [bigZ_scope N_scope].
 Arguments Scope BigZ.pow [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.log2 [bigZ_scope].
 Arguments Scope BigZ.sqrt [bigZ_scope].
 Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.even [bigZ_scope].
+Arguments Scope BigZ.odd [bigZ_scope].
 
 Local Notation "0" := BigZ.zero : bigZ_scope.
 Local Notation "1" := BigZ.one : bigZ_scope.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 099554cd0b..b341b32095 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -332,6 +332,21 @@ Module Make (N:NType) <: ZType.
  apply N.spec_0.
  Qed.
 
+ Definition log2 x :=
+  match x with
+  | Pos nx => Pos (N.log2 nx)
+  | Neg nx => zero
+  end.
+
+ Theorem spec_log2: forall x, to_Z (log2 x) = Zlog2 (to_Z x).
+ Proof.
+  intros. destruct x as [p|p]; simpl. apply N.spec_log2.
+  rewrite N.spec_0.
+  destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ].
+  rewrite Zlog2_nonpos; auto with zarith.
+  now rewrite <- EQ.
+ Qed.
+
  Definition sqrt x :=
   match x with
   | Pos nx => Pos (N.sqrt nx)
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 48d166c0ab..bdaa748e4a 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -9,40 +9,12 @@
 (************************************************************************)
 
 
-Require Import ZAxioms ZProperties.
-Require Import BinInt Zcompare Zorder ZArith_dec Zbool Zeven Zsqrt_def.
+Require Import ZAxioms ZProperties BinInt Zcompare Zorder ZArith_dec
+ Zbool Zeven Zsqrt_def Zpow_def Zlog_def.
 
 Local Open Scope Z_scope.
 
-(** An alternative Zpow *)
-
-(** The Zpow is extensionnaly equal to Zpower in ZArith, but not
-    convertible with it. This Zpow uses a logarithmic number of
-    multiplications instead of a linear one. We should try someday to
-    replace Zpower with this Zpow.
-*)
-
-Definition Zpow n m :=
-  match m with
-    | Z0 => 1
-    | Zpos p => Piter_op Zmult p n
-    | Zneg p => 0
-  end.
-
-Lemma Zpow_0_r : forall n, Zpow n 0 = 1.
-Proof. reflexivity. Qed.
-
-Lemma Zpow_succ_r : forall a b, 0<=b -> Zpow a (Zsucc b) = a * Zpow a b.
-Proof.
- intros a [|b|b] Hb; [ | |now elim Hb]; simpl.
- now rewrite Zmult_1_r.
- rewrite <- Pplus_one_succ_r. apply Piter_op_succ. apply Zmult_assoc.
-Qed.
-
-Lemma Zpow_neg_r : forall a b, b<0 -> Zpow a b = 0.
-Proof.
- now destruct b.
-Qed.
+(** Bi-directional induction for Z. *)
 
 Theorem Z_bi_induction :
   forall A : Z -> Prop, Proper (eq ==> iff) A ->
@@ -167,12 +139,12 @@ Definition odd := Zodd_bool.
 
 (** Power *)
 
-Program Instance pow_wd : Proper (eq==>eq==>eq) Zpow.
+Program Instance pow_wd : Proper (eq==>eq==>eq) Zpower.
 
-Definition pow_0_r := Zpow_0_r.
-Definition pow_succ_r := Zpow_succ_r.
-Definition pow_neg_r := Zpow_neg_r.
-Definition pow := Zpow.
+Definition pow_0_r := Zpower_0_r.
+Definition pow_succ_r := Zpower_succ_r.
+Definition pow_neg_r := Zpower_neg_r.
+Definition pow := Zpower.
 
 (** Sqrt *)
 
@@ -185,6 +157,14 @@ Definition sqrt_spec := Zsqrt_spec.
 Definition sqrt_neg := Zsqrt_neg.
 Definition sqrt := Zsqrt.
 
+(** Log2 *)
+
+Program Instance log2_wd : Proper (eq==>eq) Zlog2.
+
+Definition log2_spec := Zlog2_spec.
+Definition log2_nonpos := Zlog2_nonpos.
+Definition log2 := Zlog2.
+
 (** We define [eq] only here to avoid refering to this [eq] above. *)
 
 Definition eq := (@eq Z).
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index 37f5b294e1..b5c761a6f2 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -51,6 +51,7 @@ Module Type ZType.
  Parameter pow_N : t -> N -> t.
  Parameter pow : t -> t -> t.
  Parameter sqrt : t -> t.
+ Parameter log2 : t -> t.
  Parameter div_eucl : t -> t -> t * t.
  Parameter div : t -> t -> t.
  Parameter modulo : t -> t -> t.
@@ -79,6 +80,7 @@ Module Type ZType.
  Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
  Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
  Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
+ Parameter spec_log2: forall x, [log2 x] = Zlog2 [x].
  Parameter spec_div_eucl: forall x y,
    let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index c2965016ad..96f243fa62 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -20,7 +20,7 @@ Hint Rewrite
  spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
  spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
- spec_pow spec_even spec_odd
+ spec_pow spec_log2 spec_even spec_odd
  : zsimpl.
 
 Ltac zsimpl := autorewrite with zsimpl.
@@ -293,6 +293,21 @@ Proof.
  intros n. zify. apply Zsqrt_neg.
 Qed.
 
+(** Log2 *)
+
+Program Instance log2_wd : Proper (eq==>eq) log2.
+
+Lemma log2_spec : forall n, 0<n ->
+ 2^(log2 n) <= n /\ n < 2^(succ (log2 n)).
+Proof.
+ intros n. zify. apply Zlog2_spec.
+Qed.
+
+Lemma log2_nonpos : forall n, n<=0 -> log2 n == 0.
+Proof.
+ intros n. zify. apply Zlog2_nonpos.
+Qed.
+
 (** Even / Odd *)
 
 Definition Even n := exists m, n == 2*m.
diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v
new file mode 100644
index 0000000000..4742cc6991
--- /dev/null
+++ b/theories/Numbers/NatInt/NZLog.v
@@ -0,0 +1,297 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Base-2 Logarithm *)
+
+Require Import NZAxioms NZMulOrder NZPow.
+
+(** Interface of a log2 function, then its specification on naturals *)
+
+Module Type Log2 (Import A : Typ).
+ Parameters Inline log2 : t -> t.
+End Log2.
+
+Module Type NZLog2Spec (A : NZOrdAxiomsSig')(B : Pow' A)(C : Log2 A).
+ Import A B C.
+ Declare Instance log2_wd : Proper (eq==>eq) log2.
+ Axiom log2_spec : forall a, 0<a -> 2^(log2 a) <= a < 2^(S (log2 a)).
+ Axiom log2_nonpos : forall a, a<=0 -> log2 a == 0.
+End NZLog2Spec.
+
+Module Type NZLog2 (A : NZOrdAxiomsSig)(B : Pow A) := Log2 A <+ NZLog2Spec A B.
+
+(** Derived properties of logarithm *)
+
+Module NZLog2Prop
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZPow' A)
+ (Import C : NZLog2 A B)
+ (Import D : NZMulOrderProp A)
+ (Import E : NZPowProp A B D).
+
+(** log2 is always non-negative *)
+
+Lemma log2_nonneg : forall a, 0 <= log2 a.
+Proof.
+ intros a. destruct (le_gt_cases a 0) as [Ha|Ha].
+ now rewrite log2_nonpos.
+ destruct (log2_spec a Ha) as (_,LT).
+ apply lt_succ_r, (pow_gt_1 2). order'.
+ rewrite <- le_succ_l, <- one_succ in Ha. order.
+Qed.
+
+(** A tactic for proving positivity and non-negativity *)
+
+Ltac order_pos :=
+((apply add_pos_pos || apply add_nonneg_nonneg ||
+  apply mul_pos_pos || apply mul_nonneg_nonneg ||
+  apply pow_nonneg || apply log2_nonneg ||
+  apply (le_le_succ_r 0));
+ order_pos) (* in case of success of an apply, we recurse *)
+|| order'.  (* otherwise *)
+
+(** The spec of log2 indeed determines it *)
+
+Lemma log2_unique : forall a b, 0<=b -> 2^b<=a<2^(S b) -> log2 a == b.
+Proof.
+ intros a b Hb (LEb,LTb).
+ assert (Ha : 0 < a).
+  apply lt_le_trans with (2^b); trivial.
+  apply pow_pos_nonneg; order'.
+ assert (Hc := log2_nonneg a).
+ destruct (log2_spec a Ha) as (LEc,LTc).
+ assert (log2 a <= b).
+  apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'.
+  now apply le_le_succ_r.
+ assert (b <= log2 a).
+  apply lt_succ_r, (pow_lt_mono_r_iff 2); try order'.
+  now apply le_le_succ_r.
+ order.
+Qed.
+
+(** log2 is exact on powers of 2 *)
+
+Lemma log2_pow2 : forall a, 0<=a -> log2 (2^a) == a.
+Proof.
+ intros a Ha.
+ apply log2_unique; trivial.
+ split. order. apply pow_lt_mono_r. order'. split; trivial.
+  apply lt_succ_diag_r.
+Qed.
+
+(** log2 and basic constants *)
+
+Lemma log2_1 : log2 1 == 0.
+Proof.
+ rewrite <- (pow_0_r 2). now apply log2_pow2.
+Qed.
+
+Lemma log2_2 : log2 2 == 1.
+Proof.
+ rewrite <- (pow_1_r 2). apply log2_pow2; order'.
+Qed.
+
+(** log2 n is strictly positive for 1<n *)
+
+Lemma log2_pos : forall a, 1<a -> 0 < log2 a.
+Proof.
+ intros a Ha.
+ assert (Ha' : 0 < a) by order'.
+ assert (H := log2_nonneg a). apply le_lteq in H.
+  destruct H; trivial.
+ generalize (log2_spec a Ha'). rewrite <- H in *. nzsimpl; try order.
+ intros (_,H'). rewrite two_succ in H'. apply lt_succ_r in H'; order.
+Qed.
+
+(** Said otherwise, log2 is null only below 1 *)
+
+Lemma log2_null : forall a, log2 a == 0 <-> a <= 1.
+Proof.
+ intros a. split; intros H.
+ destruct (le_gt_cases a 1) as [Ha|Ha]; trivial.
+ generalize (log2_pos a Ha); order.
+ apply le_lteq in H; destruct H.
+ apply log2_nonpos. apply lt_succ_r. now rewrite <- one_succ.
+ rewrite H. apply log2_1.
+Qed.
+
+(** log2 is a monotone function (but not a strict one) *)
+
+Lemma log2_le_mono : forall a b, a<=b -> log2 a <= log2 b.
+Proof.
+ intros a b H.
+ destruct (le_gt_cases a 0) as [Ha|Ha].
+ rewrite log2_nonpos; order_pos.
+ assert (Hb : 0 < b) by order.
+ destruct (log2_spec a Ha) as (LEa,_).
+ destruct (log2_spec b Hb) as (_,LTb).
+ apply lt_succ_r, (pow_lt_mono_r_iff 2); order_pos.
+Qed.
+
+(** No reverse result for <=, consider for instance log2 3 <= log2 2 *)
+
+Lemma log2_lt_cancel : forall a b, log2 a < log2 b -> a < b.
+Proof.
+ intros a b H.
+ destruct (le_gt_cases b 0) as [Hb|Hb].
+  rewrite (log2_nonpos b) in H; trivial.
+  generalize (log2_nonneg a); order.
+ destruct (le_gt_cases a 0) as [Ha|Ha]. order.
+ destruct (log2_spec a Ha) as (_,LTa).
+ destruct (log2_spec b Hb) as (LEb,_).
+ apply le_succ_l in H.
+ apply (pow_le_mono_r_iff 2) in H; order_pos.
+Qed.
+
+(** When left side is a power of 2, we have an equivalence for <= *)
+
+Lemma log2_le_pow2 : forall a b, 0<a -> 0<=b -> (2^b<=a <-> b <= log2 a).
+Proof.
+ intros a b Ha Hb.
+ split; intros H.
+ rewrite <- (log2_pow2 b); trivial. now apply log2_le_mono.
+ transitivity (2^(log2 a)).
+ apply pow_le_mono_r; order'.
+ now destruct (log2_spec a Ha).
+Qed.
+
+(** When right side is a square, we have an equivalence for < *)
+
+Lemma log2_lt_pow2 : forall a b, 0<a -> 0<=b -> (a<2^b <-> log2 a < b).
+Proof.
+ intros a b Ha Hb.
+ split; intros H.
+ apply (pow_lt_mono_r_iff 2); try order_pos.
+ apply le_lt_trans with a; trivial.
+ now destruct (log2_spec a Ha).
+ apply log2_lt_cancel; try order.
+ now rewrite log2_pow2.
+Qed.
+
+(** Comparing log2 and identity *)
+
+Lemma log2_lt_lin : forall a, 0<a -> log2 a < a.
+Proof.
+ intros a Ha.
+ apply (pow_lt_mono_r_iff 2); try order_pos.
+ apply le_lt_trans with a.
+ now destruct (log2_spec a Ha).
+ apply pow_gt_lin_r; order'.
+Qed.
+
+Lemma log2_le_lin : forall a, 0<=a -> log2 a <= a.
+Proof.
+ intros a Ha.
+ apply le_lteq in Ha; destruct Ha as [Ha|Ha].
+ now apply lt_le_incl, log2_lt_lin.
+ rewrite <- Ha, log2_nonpos; order.
+Qed.
+
+(** Log2 and multiplication. *)
+
+(** Due to rounding error, we don't have the usual
+    [log2 (a*b) = log2 a + log2 b] but we may be off by 1 at most *)
+
+Lemma log2_mul_below : forall a b, 0<a -> 0<b ->
+ log2 a + log2 b <= log2 (a*b).
+Proof.
+ intros a b Ha Hb.
+ apply log2_le_pow2; try order_pos.
+ rewrite pow_add_r by order_pos.
+ apply mul_le_mono_nonneg; try apply log2_spec; order_pos.
+Qed.
+
+Lemma log2_mul_above : forall a b, 0<=a -> 0<=b ->
+ log2 (a*b) <= log2 a + log2 b + 1.
+Proof.
+ intros a b Ha Hb.
+ apply le_lteq in Ha. destruct Ha as [Ha|Ha].
+ apply le_lteq in Hb. destruct Hb as [Hb|Hb].
+ apply lt_succ_r.
+ rewrite add_1_r, <- add_succ_r, <- add_succ_l.
+ apply log2_lt_pow2; try order_pos.
+ rewrite pow_add_r by order_pos.
+ apply mul_lt_mono_nonneg; try order; now apply log2_spec.
+ rewrite <- Hb. nzsimpl. rewrite log2_nonpos; order_pos.
+ rewrite <- Ha. nzsimpl. rewrite log2_nonpos; order_pos.
+Qed.
+
+(** And we can't find better approximations in general.
+    - The lower bound is exact for powers of 2.
+    - Concerning the upper bound, for any c>0, take a=b=2^c-1,
+      then log2 (a*b) = c+c -1 while (log2 a) = (log2 b) = c-1
+*)
+
+(** Log2 and addition *)
+
+Lemma log2_add_le : forall a b, a~=1 -> b~=1 -> log2 (a+b) <= log2 a + log2 b.
+Proof.
+ intros a b Ha Hb.
+ destruct (lt_trichotomy a 1) as [Ha'|[Ha'|Ha']]; [|order|].
+ rewrite one_succ, lt_succ_r in Ha'.
+ rewrite (log2_nonpos a); trivial. nzsimpl. apply log2_le_mono.
+ rewrite <- (add_0_l b) at 2. now apply add_le_mono.
+ destruct (lt_trichotomy b 1) as [Hb'|[Hb'|Hb']]; [|order|].
+ rewrite one_succ, lt_succ_r in Hb'.
+ rewrite (log2_nonpos b); trivial. nzsimpl. apply log2_le_mono.
+ rewrite <- (add_0_r a) at 2. now apply add_le_mono.
+ clear Ha Hb.
+ apply lt_succ_r.
+ apply log2_lt_pow2; try order_pos.
+ rewrite pow_succ_r by order_pos.
+ rewrite two_succ, one_succ at 1. nzsimpl.
+ apply add_lt_mono.
+ apply lt_le_trans with (2^(S (log2 a))). apply log2_spec; order'.
+ apply pow_le_mono_r. order'. rewrite <- add_1_r. apply add_le_mono_l.
+  rewrite one_succ; now apply le_succ_l, log2_pos.
+ apply lt_le_trans with (2^(S (log2 b))). apply log2_spec; order'.
+ apply pow_le_mono_r. order'. rewrite <- add_1_l. apply add_le_mono_r.
+  rewrite one_succ; now apply le_succ_l, log2_pos.
+Qed.
+
+(** The sum of two log2 is less than twice the log2 of the sum.
+    This can almost be seen as a convexity inequality. *)
+
+Lemma quadmul_le_squareadd : forall a b, 0<=a -> 0<=b ->
+ 2*2*a*b <= (a+b)*(a+b).
+Proof.
+ intros.
+ nzsimpl'.
+ rewrite !mul_add_distr_l, !mul_add_distr_r.
+ rewrite (add_comm _ (b*b)), add_assoc.
+ apply add_le_mono_r.
+ rewrite (add_shuffle0 (a*a)), (mul_comm b a).
+ apply add_le_mono_r.
+ rewrite (mul_comm a b) at 1.
+ now apply crossmul_le_addsquare.
+Qed.
+
+Lemma add_log2_lt : forall a b, 0<a -> 0<b ->
+ log2 a + log2 b < 2 * log2 (a+b).
+Proof.
+ intros a b Ha Hb.
+ apply (pow_lt_mono_r_iff 2); try order_pos.
+ rewrite !pow_add_r by order_pos.
+ apply le_lt_trans with (a*b).
+  apply mul_le_mono_nonneg; try order_pos; now apply log2_spec.
+ apply (mul_lt_mono_pos_r (2^2)).
+ apply pow_pos_nonneg; order'.
+ rewrite (mul_comm 2).
+ rewrite <- pow_add_r by order_pos.
+ rewrite <- mul_succ_l.
+ rewrite pow_mul_r by order_pos.
+ apply le_lt_trans with ((a+b)^2).
+ rewrite !pow_2_r, (mul_comm (a*b)), mul_assoc.
+ apply quadmul_le_squareadd; order.
+ apply pow_lt_mono_l. order'. split. order_pos.
+ apply log2_spec; order_pos.
+Qed.
+
+(** We can't be more precise : consider for instance a=2 b=4, then 1+2<2*2 *)
+
+End NZLog2Prop.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 78e38b3cf3..2fbfb04c24 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-Require Export NZAxioms NZPow NZSqrt NZDiv.
+Require Export NZAxioms NZPow NZSqrt NZLog NZDiv.
 
 (** From [NZ], we obtain natural numbers just by stating that [pred 0] == 0 *)
 
@@ -32,8 +32,6 @@ Module Type Parity (Import N : NAxiomsMiniSig').
  Axiom odd_spec : forall n, odd n = true <-> Odd n.
 End Parity.
 
-(** For Power and Sqrt functions : NZPow and NZSqrt are enough *)
-
 (** Division Function : we reuse NZDiv.DivMod and NZDiv.NZDivCommon,
     and add to that a N-specific constraint. *)
 
@@ -41,15 +39,16 @@ Module Type NDivSpecific (Import N : NAxiomsMiniSig')(Import DM : DivMod' N).
  Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b.
 End NDivSpecific.
 
+(** For pow sqrt log2, the NZ axiomatizations are enough. *)
 
 (** We now group everything together. *)
 
 Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ Parity
-  <+ NZPow.NZPow <+ NZSqrt.NZSqrt
+  <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2
   <+ DivMod <+ NZDivCommon <+ NDivSpecific.
 
 Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ Parity
-  <+ NZPow.NZPow' <+ NZSqrt.NZSqrt'
+  <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2
   <+ DivMod' <+ NZDivCommon <+ NDivSpecific.
 
 
diff --git a/theories/Numbers/Natural/Abstract/NLog.v b/theories/Numbers/Natural/Abstract/NLog.v
new file mode 100644
index 0000000000..7fbf4280a3
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NLog.v
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Base-2 Logarithm Properties *)
+
+Require Import NAxioms NSub NPow NParity NZLog.
+
+Module Type NLog2Prop
+ (A : NAxiomsSig)
+ (B : NSubProp A)
+ (C : NParityProp A B)
+ (D : NPowProp A B C).
+
+ (** For the moment we simply reuse NZ properties *)
+
+ Include NZLog2Prop A A A B D.NZPowP.
+End NLog2Prop.
diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v
index 8ab460a2f8..275a5c4f5e 100644
--- a/theories/Numbers/Natural/Abstract/NPow.v
+++ b/theories/Numbers/Natural/Abstract/NPow.v
@@ -12,7 +12,7 @@ Require Import Bool NAxioms NSub NParity NZPow.
 
 (** Derived properties of power, specialized on natural numbers *)
 
-Module NPowProp
+Module Type NPowProp
  (Import A : NAxiomsSig')
  (Import B : NSubProp A)
  (Import C : NParityProp A B).
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index fc8f27ddc9..35b6af8342 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -7,9 +7,10 @@
 (************************************************************************)
 
 Require Export NAxioms.
-Require Import NMaxMin NParity NPow NSqrt NDiv.
+Require Import NMaxMin NParity NPow NSqrt NLog NDiv.
 
 (** This functor summarizes all known facts about N. *)
 
 Module Type NProp (N:NAxiomsSig) :=
- NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N <+ NDivProp N.
+ NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N
+  <+ NLog2Prop N <+ NDivProp N.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 0f04869c09..209bee8c16 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -61,10 +61,13 @@ Arguments Scope BigN.eq_bool [bigN_scope bigN_scope].
 Arguments Scope BigN.pow_pos [bigN_scope positive_scope].
 Arguments Scope BigN.pow_N [bigN_scope N_scope].
 Arguments Scope BigN.pow [bigN_scope bigN_scope].
+Arguments Scope BigN.log2 [bigN_scope].
 Arguments Scope BigN.sqrt [bigN_scope].
 Arguments Scope BigN.div_eucl [bigN_scope bigN_scope].
 Arguments Scope BigN.modulo [bigN_scope bigN_scope].
 Arguments Scope BigN.gcd [bigN_scope bigN_scope].
+Arguments Scope BigN.even [bigN_scope].
+Arguments Scope BigN.odd [bigN_scope].
 
 Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
 Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 60a836d416..306efc19ca 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -1151,7 +1151,7 @@ Module Make (W0:CyclicType) <: NType.
  rewrite Zmult_comm in H0. auto with zarith.
  Qed.
 
- Lemma spec_log2 : forall x, [x]<>0 ->
+ Lemma spec_log2_pos : forall x, [x]<>0 ->
    2^[log2 x] <= [x] < 2^([log2 x]+1).
  Proof.
  intros x H. rewrite log2_fold.
@@ -1178,6 +1178,15 @@ Module Make (W0:CyclicType) <: NType.
  apply ZnZ.spec_head0; auto with zarith.
  Qed.
 
+ Lemma spec_log2 : forall x, [log2 x] = Zlog2 [x].
+ Proof.
+  intros. destruct (Z_lt_ge_dec 0 [x]).
+  symmetry. apply Z.log2_unique. apply spec_pos.
+  apply spec_log2_pos. intro EQ; rewrite EQ in *; auto with zarith.
+  rewrite spec_log2_0. rewrite Z.log2_nonpos; auto with zarith.
+  generalize (spec_pos x); auto with zarith.
+ Qed.
+
  Lemma log2_digits_head0 : forall x, 0 < [x] ->
    [log2 x] = Zpos (digits x) - [head0 x] - 1.
  Proof.
@@ -1311,7 +1320,7 @@ Module Make (W0:CyclicType) <: NType.
  (* [x] <> 0 *)
  apply spec_unsafe_shiftl_aux with ([log2 x] + 1); auto with zarith.
  generalize (spec_pos (log2 x)); auto with zarith.
- destruct (spec_log2 x); auto with zarith.
+ destruct (spec_log2_pos x); auto with zarith.
  rewrite log2_digits_head0; auto with zarith.
  generalize (spec_pos x); auto with zarith.
  Qed.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 8b7b06966f..97e7b36784 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -62,18 +62,7 @@ Program Instance lt_wd : Proper (eq==>eq==>iff) Nlt.
 
 Definition lt_eq_cases := Nle_lteq.
 Definition lt_irrefl := Nlt_irrefl.
-
-Theorem lt_succ_r : forall n m, n < (Nsucc m) <-> n <= m.
-Proof.
-intros n m; unfold Nlt, Nle; destruct n as [| p]; destruct m as [| q]; simpl;
-split; intro H; try reflexivity; try discriminate.
-destruct p; simpl; intros; discriminate. exfalso; now apply H.
-apply -> Pcompare_p_Sq in H. destruct H as [H | H].
-now rewrite H. now rewrite H, Pcompare_refl.
-apply <- Pcompare_p_Sq. case_eq ((p ?= q)%positive Eq); intro H1.
-right; now apply Pcompare_Eq_eq. now left. exfalso; now apply H.
-Qed.
-
+Definition lt_succ_r := Nlt_succ_r.
 Definition eqb_eq := Neqb_eq.
 
 Definition compare_spec := Ncompare_spec.
@@ -169,6 +158,12 @@ Definition pow_succ_r n p (H:0 <= p) := Npow_succ_r n p.
 Lemma pow_neg_r : forall a b, b<0 -> a^b = 0.
 Proof. destruct b; discriminate. Qed.
 
+(** Log2 *)
+
+Program Instance log2_wd : Proper (eq==>eq) Nlog2.
+Definition log2_spec := Nlog2_spec.
+Definition log2_nonpos := Nlog2_nonpos.
+
 (** Sqrt *)
 
 Program Instance sqrt_wd : Proper (eq==>eq) Nsqrt.
@@ -202,6 +197,7 @@ Definition pow := Npow.
 Definition even := Neven.
 Definition odd := Nodd.
 Definition sqrt := Nsqrt.
+Definition log2 := Nlog2.
 
 Include NProp
  <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index a3203948a4..3255fda683 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -444,6 +444,11 @@ Definition pow_succ_r := pow_succ_r.
 Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed.
 Definition pow := pow.
 
+Program Instance log2_wd : Proper (eq==>eq) log2.
+Definition log2_spec := log2_spec.
+Definition log2_nonpos := log2_nonpos.
+Definition log2 := log2.
+
 Program Instance sqrt_wd : Proper (eq==>eq) sqrt.
 Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a.
 Lemma sqrt_neg : forall a, a<0 -> sqrt a = 0. inversion 1. Qed.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 703897eba5..dc2d27fa44 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -78,8 +78,7 @@ Module Type NType.
  Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
  Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
  Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
- Parameter spec_log2_0: forall x, [x] = 0 -> [log2 x] = 0.
- Parameter spec_log2: forall x, [x]<>0 -> 2^[log2 x] <= [x] < 2^([log2 x]+1).
+ Parameter spec_log2: forall x, [log2 x] = Zlog2 [x].
  Parameter spec_div_eucl: forall x y,
   let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index f242951e54..64dcd1967e 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -16,7 +16,8 @@ Module NTypeIsNAxioms (Import N : NType').
 Hint Rewrite
  spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
  spec_div spec_modulo spec_gcd spec_compare spec_eq_bool spec_sqrt
- spec_max spec_min spec_pow_pos spec_pow_N spec_pow spec_even spec_odd
+ spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow
+ spec_even spec_odd
  : nsimpl.
 Ltac nsimpl := autorewrite with nsimpl.
 Ltac ncongruence := unfold eq, to_N; repeat red; intros; nsimpl; congruence.
@@ -242,6 +243,22 @@ Proof.
  generalize (spec_pos n); omega.
 Qed.
 
+(** Log2 *)
+
+Program Instance log2_wd : Proper (eq==>eq) log2.
+
+Lemma log2_spec : forall n, 0<n ->
+ 2^(log2 n) <= n /\ n < 2^(succ (log2 n)).
+Proof.
+ intros n. zify. change (Zlog2 [n]+1)%Z with (Zsucc (Zlog2 [n])).
+ apply Zlog2_spec.
+Qed.
+
+Lemma log2_nonpos : forall n, n<=0 -> log2 n == 0.
+Proof.
+ intros n. zify. apply Zlog2_nonpos.
+Qed.
+
 (** Even / Odd *)
 
 Definition Even n := exists m, n == 2*m.
diff --git a/theories/Numbers/vo.itarget b/theories/Numbers/vo.itarget
index 7867b8caa0..fbfaa80075 100644
--- a/theories/Numbers/vo.itarget
+++ b/theories/Numbers/vo.itarget
@@ -49,6 +49,7 @@ NatInt/NZDomain.vo
 NatInt/NZDiv.vo
 NatInt/NZPow.vo
 NatInt/NZSqrt.vo
+NatInt/NZLog.vo
 Natural/Abstract/NAddOrder.vo
 Natural/Abstract/NAdd.vo
 Natural/Abstract/NAxioms.vo
@@ -65,6 +66,7 @@ Natural/Abstract/NMaxMin.vo
 Natural/Abstract/NParity.vo
 Natural/Abstract/NPow.vo
 Natural/Abstract/NSqrt.vo
+Natural/Abstract/NLog.vo
 Natural/BigN/BigN.vo
 Natural/BigN/Nbasic.vo
 Natural/BigN/NMake_gen.vo