Numbers: new functions pow, even, odd + many reorganisations

 - Simplification of functor names, e.g. ZFooProp instead of ZFooPropFunct
 - The axiomatisations of the different fonctions are now in {N,Z}Axioms.v
   apart for Z division (three separate flavours in there own files).
   Content of {N,Z}AxiomsSig is extended, old version is {N,Z}AxiomsMiniSig.
 - In NAxioms, the recursion field isn't that useful, since we axiomatize
   other functions and not define them (apart in the toy NDefOps.v).
   We leave recursion there, but in a separate NAxiomsFullSig.
 - On Z, the pow function is specified to behave as Zpower : a^(-1)=0
 - In BigN/BigZ, (power:t->N->t) is now pow_N, while pow is t->t->t
   These pow could be more clever (we convert 2nd arg to N and use pow_N).
   Default "^" is now (pow:t->t->t). BigN/BigZ ring is adapted accordingly
 - In BigN, is_even is now even, its spec is changed to use Zeven_bool.
   We add an odd. In BigZ, we add even and odd.
 - In ZBinary (implem of ZAxioms by ZArith), we create an efficient Zpow
   to implement pow. This Zpow should replace the current linear Zpower
   someday.
 - In NPeano (implem of NAxioms by Arith), we create pow, even, odd functions,
   and we modify the div and mod functions for them to be linear, structural,
   tail-recursive.

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

1 files changed, 21 insertions, 27 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v
index 5407496325..6d90bc0fd8 100644
--- a/theories/Numbers/Integer/Abstract/ZSgnAbs.v
+++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v
@@ -6,20 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Export ZMulOrder.
+(** Properties of [abs] and [sgn] *)
 
-(** An axiomatization of [abs]. *)
-
-Module Type HasAbs(Import Z : ZAxiomsSig').
- Parameter Inline abs : t -> t.
- Axiom abs_eq : forall n, 0<=n -> abs n == n.
- Axiom abs_neq : forall n, n<=0 -> abs n == -n.
-End HasAbs.
+Require Import ZMulOrder.
 
 (** Since we already have [max], we could have defined [abs]. *)
 
-Module GenericAbs (Import Z : ZAxiomsSig')
-                  (Import ZP : ZMulOrderPropFunct Z) <: HasAbs Z.
+Module GenericAbs (Import Z : ZAxiomsMiniSig')
+                  (Import ZP : ZMulOrderProp Z) <: HasAbs Z.
  Definition abs n := max n (-n).
  Lemma abs_eq : forall n, 0<=n -> abs n == n.
  Proof.
@@ -35,22 +29,13 @@ Module GenericAbs (Import Z : ZAxiomsSig')
  Qed.
 End GenericAbs.
 
-(** An Axiomatization of [sgn]. *)
-
-Module Type HasSgn (Import Z : ZAxiomsSig').
- Parameter Inline sgn : t -> t.
- Axiom sgn_null : forall n, n==0 -> sgn n == 0.
- Axiom sgn_pos : forall n, 0<n -> sgn n == 1.
- Axiom sgn_neg : forall n, n<0 -> sgn n == -(1).
-End HasSgn.
-
 (** We can deduce a [sgn] function from a [compare] function *)
 
-Module Type ZDecAxiomsSig := ZAxiomsSig <+ HasCompare.
-Module Type ZDecAxiomsSig' := ZAxiomsSig' <+ HasCompare.
+Module Type ZDecAxiomsSig := ZAxiomsMiniSig <+ HasCompare.
+Module Type ZDecAxiomsSig' := ZAxiomsMiniSig' <+ HasCompare.
 
 Module Type GenericSgn (Import Z : ZDecAxiomsSig')
-                       (Import ZP : ZMulOrderPropFunct Z) <: HasSgn Z.
+                       (Import ZP : ZMulOrderProp Z) <: HasSgn Z.
  Definition sgn n :=
   match compare 0 n with Eq => 0 | Lt => 1 | Gt => -(1) end.
  Lemma sgn_null : forall n, n==0 -> sgn n == 0.
@@ -61,11 +46,11 @@ Module Type GenericSgn (Import Z : ZDecAxiomsSig')
  Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed.
 End GenericSgn.
 
-Module Type ZAxiomsExtSig := ZAxiomsSig <+ HasAbs <+ HasSgn.
-Module Type ZAxiomsExtSig' := ZAxiomsSig' <+ HasAbs <+ HasSgn.
 
-Module Type ZSgnAbsPropSig (Import Z : ZAxiomsExtSig')
-                           (Import ZP : ZMulOrderPropFunct Z).
+(** Derived properties of [abs] and [sgn] *)
+
+Module Type ZSgnAbsProp (Import Z : ZAxiomsSig')
+                        (Import ZP : ZMulOrderProp Z).
 
 Ltac destruct_max n :=
  destruct (le_ge_cases 0 n);
@@ -343,6 +328,15 @@ Proof.
  rewrite eq_opp_l. apply abs_neq. now apply lt_le_incl.
 Qed.
 
-End ZSgnAbsPropSig.
+Lemma sgn_sgn : forall x, sgn (sgn x) == sgn x.
+Proof.
+ intros.
+ destruct (sgn_spec x) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ.
+ apply sgn_pos, lt_0_1.
+ now apply sgn_null.
+ apply sgn_neg. rewrite opp_neg_pos. apply lt_0_1.
+Qed.
+
+End ZSgnAbsProp.