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

2 files changed, 18 insertions, 1 deletions

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.