From d6ebd62341fd6bbe2b7d4e5309d8e13f786a9462 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 2 Nov 2010 15:10:43 +0000
Subject: 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
---
 theories/Numbers/Natural/Abstract/NAxioms.v     |  9 ++++-----
 theories/Numbers/Natural/Abstract/NLog.v        | 22 ++++++++++++++++++++++
 theories/Numbers/Natural/Abstract/NPow.v        |  2 +-
 theories/Numbers/Natural/Abstract/NProperties.v |  5 +++--
 4 files changed, 30 insertions(+), 8 deletions(-)
 create mode 100644 theories/Numbers/Natural/Abstract/NLog.v

(limited to 'theories/Numbers/Natural/Abstract')

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.
-- 
cgit v1.2.3