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

7 files changed, 57 insertions, 42 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.