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

10 files changed, 76 insertions, 25 deletions

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.