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

21 files changed, 785 insertions, 200 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index b2324d9718..96d60c9979 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -10,8 +10,8 @@
 
 Require Export NBase.
 
-Module NAddPropFunct (Import N : NAxiomsSig').
-Include NBasePropFunct N.
+Module NAddProp (Import N : NAxiomsMiniSig').
+Include NBaseProp N.
 
 (** For theorems about [add] that are both valid for [N] and [Z], see [NZAdd] *)
 (** Now comes theorems valid for natural numbers but not for Z *)
@@ -75,5 +75,5 @@ intros n m H; rewrite (add_comm n (P m));
 rewrite (add_comm n m); now apply add_pred_l.
 Qed.
 
-End NAddPropFunct.
+End NAddProp.
 
diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v
index fe7a491dd9..da41886f05 100644
--- a/theories/Numbers/Natural/Abstract/NAddOrder.v
+++ b/theories/Numbers/Natural/Abstract/NAddOrder.v
@@ -10,8 +10,8 @@
 
 Require Export NOrder.
 
-Module NAddOrderPropFunct (Import N : NAxiomsSig').
-Include NOrderPropFunct N.
+Module NAddOrderProp (Import N : NAxiomsMiniSig').
+Include NOrderProp N.
 
 (** Theorems true for natural numbers, not for integers *)
 
@@ -43,4 +43,4 @@ Proof.
 intros; apply add_nonneg_pos. apply le_0_l. assumption.
 Qed.
 
-End NAddOrderPropFunct.
+End NAddOrderProp.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index fd5a353918..66ff2ded54 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -8,30 +8,67 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-Require Export NZAxioms.
+Require Export NZAxioms NZPow NZDiv.
 
-Set Implicit Arguments.
+(** From [NZ], we obtain natural numbers just by stating that [pred 0] == 0 *)
 
-Module Type NAxioms (Import NZ : NZDomainSig').
+Module Type NAxiom (Import NZ : NZDomainSig').
+ Axiom pred_0 : P 0 == 0.
+End NAxiom.
 
-Axiom pred_0 : P 0 == 0.
+Module Type NAxiomsMiniSig := NZOrdAxiomsSig <+ NAxiom.
+Module Type NAxiomsMiniSig' := NZOrdAxiomsSig' <+ NAxiom.
 
-Parameter Inline recursion : forall A : Type, A -> (t -> A -> A) -> t -> A.
-Implicit Arguments recursion [A].
 
-Declare Instance recursion_wd (A : Type) (Aeq : relation A) :
- Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
+(** Let's now add some more functions and their specification *)
+
+(** Parity functions *)
+
+Module Type Parity (Import N : NAxiomsMiniSig').
+ Parameter Inline even odd : t -> bool.
+ Definition Even n := exists m, n == 2*m.
+ Definition Odd n := exists m, n == 2*m+1.
+ Axiom even_spec : forall n, even n = true <-> Even n.
+ Axiom odd_spec : forall n, odd n = true <-> Odd n.
+End Parity.
+
+(** Power function : NZPow is enough *)
+
+(** Division Function : we reuse NZDiv.DivMod and NZDiv.NZDivCommon,
+    and add to that a N-specific constraint. *)
+
+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.
+
+
+(** We now group everything together. *)
+
+Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ Parity
+  <+ NZPow.NZPow <+ DivMod <+ NZDivCommon <+ NDivSpecific.
+
+Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ Parity
+  <+ NZPow.NZPow' <+ DivMod' <+ NZDivCommon <+ NDivSpecific.
+
+
+(** It could also be interesting to have a constructive recursor function. *)
+
+Module Type NAxiomsRec (Import NZ : NZDomainSig').
+
+Parameter Inline recursion : forall {A : Type}, A -> (t -> A -> A) -> t -> A.
+
+Declare Instance recursion_wd {A : Type} (Aeq : relation A) :
+ Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion.
 
 Axiom recursion_0 :
-  forall (A : Type) (a : A) (f : t -> A -> A), recursion a f 0 = a.
+  forall {A} (a : A) (f : t -> A -> A), recursion a f 0 = a.
 
 Axiom recursion_succ :
-  forall (A : Type) (Aeq : relation A) (a : A) (f : t -> A -> A),
+  forall {A} (Aeq : relation A) (a : A) (f : t -> A -> A),
     Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
       forall n, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 
-End NAxioms.
-
-Module Type NAxiomsSig := NZOrdAxiomsSig <+ NAxioms.
-Module Type NAxiomsSig' := NZOrdAxiomsSig' <+ NAxioms.
+End NAxiomsRec.
 
+Module Type NAxiomsFullSig := NAxiomsSig <+ NAxiomsRec.
+Module Type NAxiomsFullSig' := NAxiomsSig' <+ NAxiomsRec.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 911be68b07..e9ec6a823e 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -12,42 +12,19 @@ Require Export Decidable.
 Require Export NAxioms.
 Require Import NZProperties.
 
-Module NBasePropFunct (Import N : NAxiomsSig').
+Module NBaseProp (Import N : NAxiomsMiniSig').
 (** First, we import all known facts about both natural numbers and integers. *)
-Include NZPropFunct N.
+Include NZProp N.
 
-(** We prove that the successor of a number is not zero by defining a
-function (by recursion) that maps 0 to false and the successor to true *)
-
-Definition if_zero (A : Type) (a b : A) (n : N.t) : A :=
-  recursion a (fun _ _ => b) n.
-
-Implicit Arguments if_zero [A].
-
-Instance if_zero_wd (A : Type) :
- Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A).
-Proof.
-intros; unfold if_zero.
-repeat red; intros. apply recursion_wd; auto. repeat red; auto.
-Qed.
-
-Theorem if_zero_0 : forall (A : Type) (a b : A), if_zero a b 0 = a.
-Proof.
-unfold if_zero; intros; now rewrite recursion_0.
-Qed.
-
-Theorem if_zero_succ :
- forall (A : Type) (a b : A) (n : N.t), if_zero a b (S n) = b.
-Proof.
-intros; unfold if_zero.
-now rewrite recursion_succ.
-Qed.
+(** From [pred_0] and order facts, we can prove that 0 isn't a successor. *)
 
 Theorem neq_succ_0 : forall n, S n ~= 0.
 Proof.
-intros n H.
-generalize (Logic.eq_refl (if_zero false true 0)).
-rewrite <- H at 1. rewrite if_zero_0, if_zero_succ; discriminate.
+ intros n EQ.
+ assert (EQ' := pred_succ n).
+ rewrite EQ, pred_0 in EQ'.
+ rewrite <- EQ' in EQ.
+ now apply (neq_succ_diag_l 0).
 Qed.
 
 Theorem neq_0_succ : forall n, 0 ~= S n.
@@ -204,5 +181,5 @@ Ltac double_induct n m :=
   pattern n, m; apply double_induction; clear n m;
   [solve_relation_wd | | | ].
 
-End NBasePropFunct.
+End NBaseProp.
 
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 308a24f790..c1bac7165a 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -12,8 +12,37 @@ Require Import Bool. (* To get the orb and negb function *)
 Require Import RelationPairs.
 Require Export NStrongRec.
 
-Module NdefOpsPropFunct (Import N : NAxiomsSig').
-Include NStrongRecPropFunct N.
+(** In this module, we derive generic implementations of usual operators
+   just via the use of a [recursion] function. *)
+
+Module NdefOpsProp (Import N : NAxiomsFullSig').
+Include NStrongRecProp N.
+
+(** Nullity Test *)
+
+Definition if_zero (A : Type) (a b : A) (n : N.t) : A :=
+  recursion a (fun _ _ => b) n.
+
+Implicit Arguments if_zero [A].
+
+Instance if_zero_wd (A : Type) :
+ Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A).
+Proof.
+intros; unfold if_zero.
+repeat red; intros. apply recursion_wd; auto. repeat red; auto.
+Qed.
+
+Theorem if_zero_0 : forall (A : Type) (a b : A), if_zero a b 0 = a.
+Proof.
+unfold if_zero; intros; now rewrite recursion_0.
+Qed.
+
+Theorem if_zero_succ :
+ forall (A : Type) (a b : A) (n : N.t), if_zero a b (S n) = b.
+Proof.
+intros; unfold if_zero.
+now rewrite recursion_succ.
+Qed.
 
 (*****************************************************)
 (**                   Addition                       *)
@@ -473,5 +502,5 @@ Theorem log_pow2 : forall n, log (2^^n) = n.
 
 *)
 
-End NdefOpsPropFunct.
+End NdefOpsProp.
 
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index 773b9ad616..be56c8b032 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.v
@@ -6,18 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** Euclidean Division *)
+(** Properties of Euclidean Division *)
 
-Require Import NAxioms NProperties NZDiv.
+Require Import NAxioms NSub NZDiv.
 
-Module Type NDivSpecific (Import N : NAxiomsSig')(Import DM : DivMod' N).
- Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b.
-End NDivSpecific.
-
-Module Type NDivSig := NAxiomsSig <+ DivMod <+ NZDivCommon <+ NDivSpecific.
-Module Type NDivSig' := NAxiomsSig' <+ DivMod' <+ NZDivCommon <+ NDivSpecific.
-
-Module NDivPropFunct (Import N : NDivSig')(Import NP : NPropSig N).
+Module NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N).
 
 (** We benefit from what already exists for NZ *)
 
@@ -30,7 +23,7 @@ Module NDivPropFunct (Import N : NDivSig')(Import NP : NPropSig N).
   Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
   Proof. split. apply le_0_l. apply mod_upper_bound. order. Qed.
  End ND.
- Module Import NZDivP := NZDivPropFunct N NP ND.
+ Module Import NZDivP := NZDivProp N NP ND.
 
  Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l.
 
@@ -235,5 +228,5 @@ Lemma mod_divides : forall a b, b~=0 ->
  (a mod b == 0 <-> exists c, a == b*c).
 Proof. intros. apply mod_divides; auto'. Qed.
 
-End NDivPropFunct.
+End NDivProp.
 
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 19e5a318ae..3a48b79972 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -10,7 +10,7 @@
 
 Require Import NBase.
 
-Module Homomorphism (N1 N2 : NAxiomsSig).
+Module Homomorphism (N1 N2 : NAxiomsFullSig).
 
 Local Notation "n == m" := (N2.eq n m) (at level 70, no associativity).
 
@@ -51,9 +51,9 @@ Qed.
 
 End Homomorphism.
 
-Module Inverse (N1 N2 : NAxiomsSig).
+Module Inverse (N1 N2 : NAxiomsFullSig).
 
-Module Import NBasePropMod1 := NBasePropFunct N1.
+Module Import NBasePropMod1 := NBaseProp N1.
 (* This makes the tactic induct available. Since it is taken from
 (NBasePropFunct NAxiomsMod1), it refers to induction on N1. *)
 
@@ -74,7 +74,7 @@ Qed.
 
 End Inverse.
 
-Module Isomorphism (N1 N2 : NAxiomsSig).
+Module Isomorphism (N1 N2 : NAxiomsFullSig).
 
 Module Hom12 := Homomorphism N1 N2.
 Module Hom21 := Homomorphism N2 N1.
diff --git a/theories/Numbers/Natural/Abstract/NMaxMin.v b/theories/Numbers/Natural/Abstract/NMaxMin.v
index f8276c1602..cdff6dbc8c 100644
--- a/theories/Numbers/Natural/Abstract/NMaxMin.v
+++ b/theories/Numbers/Natural/Abstract/NMaxMin.v
@@ -10,8 +10,8 @@ Require Import NAxioms NSub GenericMinMax.
 
 (** * Properties of minimum and maximum specific to natural numbers *)
 
-Module Type NMaxMinProp (Import N : NAxiomsSig').
-Include NSubPropFunct N.
+Module Type NMaxMinProp (Import N : NAxiomsMiniSig').
+Include NSubProp N.
 
 (** Zero *)
 
diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v
index 3eb6f3698c..f6c6ad5428 100644
--- a/theories/Numbers/Natural/Abstract/NMulOrder.v
+++ b/theories/Numbers/Natural/Abstract/NMulOrder.v
@@ -10,8 +10,8 @@
 
 Require Export NAddOrder.
 
-Module NMulOrderPropFunct (Import N : NAxiomsSig').
-Include NAddOrderPropFunct N.
+Module NMulOrderProp (Import N : NAxiomsMiniSig').
+Include NAddOrderProp N.
 
 (** Theorems that are either not valid on Z or have different proofs
     on N and Z *)
@@ -74,5 +74,5 @@ assert (H3 : 1 < n * m) by now apply (lt_1_l m).
 rewrite H in H3; false_hyp H3 lt_irrefl.
 Qed.
 
-End NMulOrderPropFunct.
+End NMulOrderProp.
 
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index faa78b30cd..fa855f2105 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -10,8 +10,8 @@
 
 Require Export NAdd.
 
-Module NOrderPropFunct (Import N : NAxiomsSig').
-Include NAddPropFunct N.
+Module NOrderProp (Import N : NAxiomsMiniSig').
+Include NAddProp N.
 
 (* Theorems that are true for natural numbers but not for integers *)
 
@@ -238,5 +238,5 @@ rewrite pred_0. split; intro H; apply le_0_l.
 intro n. rewrite pred_succ. apply succ_le_mono.
 Qed.
 
-End NOrderPropFunct.
+End NOrderProp.
 
diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v
new file mode 100644
index 0000000000..e815f9ee6a
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NParity.v
@@ -0,0 +1,206 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+Require Import Bool NSub.
+
+(** Properties of [even], [odd]. *)
+
+(** NB: most parts of [NParity] and [ZParity] are common,
+    but it is difficult to share them in NZ, since
+    initial proofs [Even_or_Odd] and [Even_Odd_False] must
+    be proved differently *)
+
+Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N).
+
+Instance Even_wd : Proper (eq==>iff) Even.
+Proof. unfold Even. solve_predicate_wd. Qed.
+
+Instance Odd_wd : Proper (eq==>iff) Odd.
+Proof. unfold Odd. solve_predicate_wd. Qed.
+
+Instance even_wd : Proper (eq==>Logic.eq) even.
+Proof.
+ intros x x' EQ. rewrite eq_iff_eq_true, 2 even_spec. now apply Even_wd.
+Qed.
+
+Instance odd_wd : Proper (eq==>Logic.eq) odd.
+Proof.
+ intros x x' EQ. rewrite eq_iff_eq_true, 2 odd_spec. now apply Odd_wd.
+Qed.
+
+Lemma Even_or_Odd : forall x, Even x \/ Odd x.
+Proof.
+ induct x.
+ left. exists 0. now nzsimpl.
+ intros x.
+ intros [(y,H)|(y,H)].
+ right. exists y. rewrite H. now nzsimpl.
+ left. exists (S y). rewrite H. now nzsimpl.
+Qed.
+
+Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1.
+Proof.
+ intros. nzsimpl. apply lt_succ_r. now apply add_le_mono.
+Qed.
+
+Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m.
+Proof.
+ intros. nzsimpl.
+ rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r.
+ apply add_le_mono; now apply le_succ_l.
+Qed.
+
+Lemma Even_Odd_False : forall x, Even x -> Odd x -> False.
+Proof.
+intros x (y,E) (z,O). rewrite O in E; clear O.
+destruct (le_gt_cases y z) as [LE|GT].
+generalize (double_below _ _ LE); order.
+generalize (double_above _ _ GT); order.
+Qed.
+
+Lemma orb_even_odd : forall n, orb (even n) (odd n) = true.
+Proof.
+ intros.
+ destruct (Even_or_Odd n) as [H|H].
+ rewrite <- even_spec in H. now rewrite H.
+ rewrite <- odd_spec in H. now rewrite H, orb_true_r.
+Qed.
+
+Lemma negb_odd_even : forall n, negb (odd n) = even n.
+Proof.
+ intros.
+ generalize (Even_or_Odd n) (Even_Odd_False n).
+ rewrite <- even_spec, <- odd_spec.
+ destruct (odd n), (even n); simpl; intuition.
+Qed.
+
+Lemma negb_even_odd : forall n, negb (even n) = odd n.
+Proof.
+ intros. rewrite <- negb_odd_even. apply negb_involutive.
+Qed.
+
+Lemma even_0 : even 0 = true.
+Proof.
+ rewrite even_spec. exists 0. now nzsimpl.
+Qed.
+
+Lemma odd_1 : odd 1 = true.
+Proof.
+ rewrite odd_spec. exists 0. now nzsimpl.
+Qed.
+
+Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n.
+Proof.
+ split; intros (m,H).
+ exists m. apply succ_inj. now rewrite add_1_r in H.
+ exists m. rewrite add_1_r. now apply succ_wd.
+Qed.
+
+Lemma odd_succ_even : forall n, odd (S n) = even n.
+Proof.
+ intros. apply eq_iff_eq_true. rewrite even_spec, odd_spec.
+ apply Odd_succ_Even.
+Qed.
+
+Lemma even_succ_odd : forall n, even (S n) = odd n.
+Proof.
+ intros. now rewrite <- negb_odd_even, odd_succ_even, negb_even_odd.
+Qed.
+
+Lemma Even_succ_Odd : forall n, Even (S n) <-> Odd n.
+Proof.
+ intros. now rewrite <- even_spec, even_succ_odd, odd_spec.
+Qed.
+
+Lemma odd_pred_even : forall n, n~=0 -> odd (P n) = even n.
+Proof.
+ intros. rewrite <- (succ_pred n) at 2 by trivial.
+ symmetry. apply even_succ_odd.
+Qed.
+
+Lemma even_pred_odd : forall n, n~=0 -> even (P n) = odd n.
+Proof.
+ intros. rewrite <- (succ_pred n) at 2 by trivial.
+ symmetry. apply odd_succ_even.
+Qed.
+
+Lemma even_add : forall n m, even (n+m) = Bool.eqb (even n) (even m).
+Proof.
+ intros.
+ case_eq (even n); case_eq (even m);
+  rewrite <- ?negb_true_iff, ?negb_even_odd, ?odd_spec, ?even_spec;
+  intros (m',Hm) (n',Hn).
+ exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm.
+ exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc.
+ exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.
+ exists (n'+m'+1). rewrite Hm,Hn. nzsimpl. now rewrite add_shuffle1.
+Qed.
+
+Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m).
+Proof.
+ intros. rewrite <- !negb_even_odd. rewrite even_add.
+ now destruct (even n), (even m).
+Qed.
+
+Lemma even_mul : forall n m, even (mul n m) = even n || even m.
+Proof.
+ intros.
+ case_eq (even n); simpl; rewrite ?even_spec.
+ intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc.
+ case_eq (even m); simpl; rewrite ?even_spec.
+ intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2).
+ (* odd / odd *)
+ rewrite <- !negb_true_iff, !negb_even_odd, !odd_spec.
+ intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m').
+ rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r.
+ now rewrite add_shuffle1, add_assoc, !mul_assoc.
+Qed.
+
+Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m.
+Proof.
+ intros. rewrite <- !negb_even_odd. rewrite even_mul.
+ now destruct (even n), (even m).
+Qed.
+
+Lemma even_sub : forall n m, m<=n -> even (n-m) = Bool.eqb (even n) (even m).
+Proof.
+ intros.
+ case_eq (even n); case_eq (even m);
+  rewrite <- ?negb_true_iff, ?negb_even_odd, ?odd_spec, ?even_spec;
+  intros (m',Hm) (n',Hn).
+ exists (n'-m'). now rewrite mul_sub_distr_l, Hn, Hm.
+ exists (n'-m'-1).
+  rewrite !mul_sub_distr_l, Hn, Hm, sub_add_distr, mul_1_r.
+  rewrite <- (add_1_l 1) at 5. rewrite sub_add_distr.
+  symmetry. apply sub_add.
+  apply le_add_le_sub_l.
+  rewrite add_1_l, <- (mul_1_r 2) at 1.
+  rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l.
+  rewrite le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r.
+  destruct (le_gt_cases n' m') as [LE|GT]; trivial.
+  generalize (double_below _ _ LE). order.
+  apply lt_succ_r, le_0_1.
+ exists (n'-m'). rewrite mul_sub_distr_l, Hn, Hm.
+  apply add_sub_swap.
+  apply mul_le_mono_pos_l.
+  apply lt_succ_r, le_0_1.
+  destruct (le_gt_cases m' n') as [LE|GT]; trivial.
+  generalize (double_above _ _ GT). order.
+ exists (n'-m'). rewrite Hm,Hn, mul_sub_distr_l.
+  rewrite sub_add_distr. rewrite add_sub_swap. apply add_sub.
+  apply succ_le_mono.
+  rewrite add_1_r in Hm,Hn. order.
+Qed.
+
+Lemma odd_sub : forall n m, m<=n -> odd (n-m) = xorb (odd n) (odd m).
+Proof.
+ intros. rewrite <- !negb_even_odd. rewrite even_sub by trivial.
+ now destruct (even n), (even m).
+Qed.
+
+End NParityProp.
diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v
new file mode 100644
index 0000000000..0039a1e2c8
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NPow.v
@@ -0,0 +1,147 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Properties of the power function *)
+
+Require Import Bool NAxioms NSub NParity NZPow.
+
+(** Derived properties of power, specialized on natural numbers *)
+
+Module NPowProp
+ (Import N : NAxiomsSig')(Import NS : NSubProp N)(Import NP : NParityProp N NS).
+
+ Module Import NZPowP := NZPowProp N NS N.
+
+ Ltac auto' := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l.
+ Ltac wrap l := intros; apply l; auto'.
+
+Lemma pow_succ_r' : forall a b, a^(S b) == a * a^b.
+Proof. wrap pow_succ_r. Qed.
+
+(** Power and basic constants *)
+
+Lemma pow_0_l : forall a, a~=0 -> 0^a == 0.
+Proof. wrap pow_0_l. Qed.
+
+Definition pow_1_r : forall a, a^1 == a
+ := pow_1_r.
+
+Lemma pow_1_l : forall a, 1^a == 1.
+Proof. wrap pow_1_l. Qed.
+
+Definition pow_2_r : forall a, a^2 == a*a
+ := pow_2_r.
+
+(** Power and addition, multiplication *)
+
+Lemma pow_add_r : forall a b c, a^(b+c) == a^b * a^c.
+Proof. wrap pow_add_r. Qed.
+
+Lemma pow_mul_l : forall a b c, (a*b)^c == a^c * b^c.
+Proof. wrap pow_mul_l. Qed.
+
+Lemma pow_mul_r : forall a b c, a^(b*c) == (a^b)^c.
+Proof. wrap pow_mul_r. Qed.
+
+(** Positivity *)
+
+Lemma pow_nonzero : forall a b, a~=0 -> a^b~=0.
+Proof. intros. rewrite neq_0_lt_0. wrap pow_pos_nonneg. Qed.
+
+(** Monotonicity *)
+
+Lemma pow_lt_mono_l : forall a b c, c~=0 -> a<b -> a^c < b^c.
+Proof. wrap pow_lt_mono_l. Qed.
+
+Lemma pow_le_mono_l : forall a b c, a<=b -> a^c <= b^c.
+Proof. wrap pow_le_mono_l. Qed.
+
+Lemma pow_gt_1 : forall a b, 1<a -> b~=0 -> 1<a^b.
+Proof. wrap pow_gt_1. Qed.
+
+Lemma pow_lt_mono_r : forall a b c, 1<a -> b<c -> a^b < a^c.
+Proof. wrap pow_lt_mono_r. Qed.
+
+(** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *)
+
+Lemma pow_le_mono_r : forall a b c, a~=0 -> b<=c -> a^b <= a^c.
+Proof. wrap pow_le_mono_r. Qed.
+
+Lemma pow_le_mono : forall a b c d, a~=0 -> a<=c -> b<=d ->
+ a^b <= c^d.
+Proof. wrap pow_le_mono. Qed.
+
+Definition pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d ->
+ a^b < c^d
+ := pow_lt_mono.
+
+(** Injectivity *)
+
+Lemma pow_inj_l : forall a b c, c~=0 -> a^c == b^c -> a == b.
+Proof. intros; eapply pow_inj_l; eauto; auto'. auto'. Qed.
+
+Lemma pow_inj_r : forall a b c, 1<a -> a^b == a^c -> b == c.
+Proof. intros; eapply pow_inj_r; eauto; auto'. Qed.
+
+(** Monotonicity results, both ways *)
+
+Lemma pow_lt_mono_l_iff : forall a b c, c~=0 ->
+  (a<b <-> a^c < b^c).
+Proof. wrap pow_lt_mono_l_iff. Qed.
+
+Lemma pow_le_mono_l_iff : forall a b c, c~=0 ->
+  (a<=b <-> a^c <= b^c).
+Proof. wrap pow_le_mono_l_iff. Qed.
+
+Lemma pow_lt_mono_r_iff : forall a b c, 1<a ->
+  (b<c <-> a^b < a^c).
+Proof. wrap pow_lt_mono_r_iff. Qed.
+
+Lemma pow_le_mono_r_iff : forall a b c, 1<a ->
+  (b<=c <-> a^b <= a^c).
+Proof. wrap pow_le_mono_r_iff. Qed.
+
+(** For any a>1, the a^x function is above the identity function *)
+
+Lemma pow_gt_lin_r : forall a b, 1<a -> b < a^b.
+Proof. wrap pow_gt_lin_r. Qed.
+
+(** Someday, we should say something about the full Newton formula.
+    In the meantime, we can at least provide some inequalities about
+    (a+b)^c.
+*)
+
+Lemma pow_add_lower : forall a b c, c~=0 ->
+  a^c + b^c <= (a+b)^c.
+Proof. wrap pow_add_lower. Qed.
+
+(** This upper bound can also be seen as a convexity proof for x^c :
+    image of (a+b)/2 is below the middle of the images of a and b
+*)
+
+Lemma pow_add_upper : forall a b c, c~=0 ->
+  (a+b)^c <= 2^(pred c) * (a^c + b^c).
+Proof. wrap pow_add_upper. Qed.
+
+(** Power and parity *)
+
+Lemma even_pow : forall a b, b~=0 -> even (a^b) = even a.
+Proof.
+ intros a b Hb. rewrite neq_0_lt_0 in Hb.
+ apply lt_ind with (4:=Hb). solve_predicate_wd.
+ now nzsimpl.
+ clear b Hb. intros b Hb IH.
+ rewrite pow_succ_r', even_mul, IH. now destruct (even a).
+Qed.
+
+Lemma odd_pow : forall a b, b~=0 -> odd (a^b) = odd a.
+Proof.
+ intros. now rewrite <- !negb_even_odd, even_pow.
+Qed.
+
+End NPowProp.
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index 46117b25b6..c1977f3533 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -6,15 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Export NAxioms NMaxMin.
+Require Export NAxioms.
+Require Import NMaxMin NParity NPow NDiv.
 
-(** This functor summarizes all known facts about N.
-    For the moment it is only an alias to the last functor which
-    subsumes all others.
-*)
+(** This functor summarizes all known facts about N. *)
 
-Module Type NPropSig := NMaxMinProp.
-
-Module NPropFunct (N:NAxiomsSig) <: NPropSig N.
- Include NPropSig N.
-End NPropFunct.
+Module Type NProp (N:NAxiomsSig) :=
+ NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NDivProp N.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index f1ff87a8f1..26cf2d64a6 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -13,8 +13,8 @@ and proves its properties *)
 
 Require Export NSub.
 
-Module NStrongRecPropFunct (Import N : NAxiomsSig').
-Include NSubPropFunct N.
+Module NStrongRecProp (Import N : NAxiomsFullSig').
+Include NSubProp N.
 
 Section StrongRecursion.
 
@@ -204,5 +204,5 @@ End StrongRecursion.
 
 Implicit Arguments strong_rec [A].
 
-End NStrongRecPropFunct.
+End NStrongRecProp.
 
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v
index 4cf8d62f11..4232ecbfad 100644
--- a/theories/Numbers/Natural/Abstract/NSub.v
+++ b/theories/Numbers/Natural/Abstract/NSub.v
@@ -10,8 +10,8 @@
 
 Require Export NMulOrder.
 
-Module Type NSubPropFunct (Import N : NAxiomsSig').
-Include NMulOrderPropFunct N.
+Module Type NSubProp (Import N : NAxiomsMiniSig').
+Include NMulOrderProp N.
 
 Theorem sub_0_l : forall n, 0 - n == 0.
 Proof.
@@ -316,5 +316,5 @@ Theorem add_dichotomy :
   forall n m, (exists p, p + n == m) \/ (exists p, p + m == n).
 Proof. exact le_alt_dichotomy. Qed.
 
-End NSubPropFunct.
+End NSubProp.
 
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 2bb79280c9..ef4ac7c457 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -29,7 +29,7 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
 
 Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
  NMake.Make Int31Cyclic <+ NTypeIsNAxioms
- <+ !NPropSig <+ !NDivPropFunct <+ HasEqBool2Dec
+ <+ !NProp <+ HasEqBool2Dec
  <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
 
 
@@ -58,8 +58,9 @@ Arguments Scope BigN.compare [bigN_scope bigN_scope].
 Arguments Scope BigN.min [bigN_scope bigN_scope].
 Arguments Scope BigN.max [bigN_scope bigN_scope].
 Arguments Scope BigN.eq_bool [bigN_scope bigN_scope].
-Arguments Scope BigN.power_pos [bigN_scope positive_scope].
-Arguments Scope BigN.power [bigN_scope N_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.sqrt [bigN_scope].
 Arguments Scope BigN.div_eucl [bigN_scope bigN_scope].
 Arguments Scope BigN.modulo [bigN_scope bigN_scope].
@@ -71,7 +72,7 @@ Infix "+" := BigN.add : bigN_scope.
 Infix "-" := BigN.sub : bigN_scope.
 Infix "*" := BigN.mul : bigN_scope.
 Infix "/" := BigN.div : bigN_scope.
-Infix "^" := BigN.power : bigN_scope.
+Infix "^" := BigN.pow : bigN_scope.
 Infix "?=" := BigN.compare : bigN_scope.
 Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
 Notation "x != y" := (~x==y)%bigN (at level 70, no associativity) : bigN_scope.
@@ -110,11 +111,11 @@ Qed.
 Lemma BigNeqb_correct : forall x y, BigN.eq_bool x y = true -> x==y.
 Proof. now apply BigN.eqb_eq. Qed.
 
-Lemma BigNpower : power_theory 1 BigN.mul BigN.eq (@id N) BigN.power.
+Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow.
 Proof.
 constructor.
-intros. red. rewrite BigN.spec_power. unfold id.
-destruct Zpower_theory as [EQ]. rewrite EQ.
+intros. red. rewrite BigN.spec_pow, BigN.spec_of_N.
+rewrite Zpower_theory.(rpow_pow_N).
 destruct n; simpl. reflexivity.
 induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto.
 Qed.
@@ -172,6 +173,12 @@ Ltac BigNcst t :=
  | false => constr:NotConstant
  end.
 
+Ltac BigN_to_N t :=
+ match isBigNcst t with
+ | true => eval vm_compute in (BigN.to_N t)
+ | false => constr:NotConstant
+ end.
+
 Ltac Ncst t :=
  match isNcst t with
  | true => constr:t
@@ -183,11 +190,12 @@ Ltac Ncst t :=
 Add Ring BigNr : BigNring
  (decidable BigNeqb_correct,
   constants [BigNcst],
-  power_tac BigNpower [Ncst],
+  power_tac BigNpower [BigN_to_N],
   div BigNdiv).
 
 Section TestRing.
-Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
+Local Notation "2" := (BigN.N0 2%int31) : bigN_scope. (* temporary notation *)
+Let test : forall x y, 1 + x*y^1 + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
 intros. ring_simplify. reflexivity.
 Qed.
 End TestRing.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index cea2e3195f..6697d59c3b 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -16,7 +16,7 @@
     representation. The representation-dependent (and macro-generated) part
     is now in [NMake_gen]. *)
 
-Require Import BigNumPrelude ZArith CyclicAxioms DoubleType
+Require Import Bool BigNumPrelude ZArith Nnat CyclicAxioms DoubleType
   Nbasic Wf_nat StreamMemo NSig NMake_gen.
 
 Module Make (W0:CyclicType) <: NType.
@@ -69,6 +69,8 @@ Module Make (W0:CyclicType) <: NType.
  apply Zpower_le_monotone2; auto with zarith.
  Qed.
 
+ Definition to_N (x : t) := Zabs_N (to_Z x).
+
  (** * Zero and One *)
 
  Definition zero := mk_t O ZnZ.zero.
@@ -731,16 +733,16 @@ Module Make (W0:CyclicType) <: NType.
 
  (** * Power *)
 
- Fixpoint power_pos (x:t)(p:positive) : t :=
+ Fixpoint pow_pos (x:t)(p:positive) : t :=
   match p with
   | xH => x
-  | xO p => square (power_pos x p)
-  | xI p => mul (square (power_pos x p)) x
+  | xO p => square (pow_pos x p)
+  | xI p => mul (square (pow_pos x p)) x
   end.
 
- Theorem spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.
+ Theorem spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
  Proof.
- intros x n; generalize x; elim n; clear n x; simpl power_pos.
+ intros x n; generalize x; elim n; clear n x; simpl pow_pos.
  intros; rewrite spec_mul; rewrite spec_square; rewrite H.
  rewrite Zpos_xI; rewrite Zpower_exp; auto with zarith.
  rewrite (Zmult_comm 2); rewrite Zpower_mult; auto with zarith.
@@ -752,15 +754,23 @@ Module Make (W0:CyclicType) <: NType.
  intros; rewrite Zpower_1_r; auto.
  Qed.
 
- Definition power (x:t)(n:N) : t := match n with
+ Definition pow_N (x:t)(n:N) : t := match n with
   | BinNat.N0 => one
-  | BinNat.Npos p => power_pos x p
+  | BinNat.Npos p => pow_pos x p
  end.
 
- Theorem spec_power: forall x n, [power x n] = [x] ^ Z_of_N n.
+ Theorem spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
  Proof.
  destruct n; simpl. apply spec_1.
- apply spec_power_pos.
+ apply spec_pow_pos.
+ Qed.
+
+ Definition pow (x y:t) : t := pow_N x (to_N y).
+
+ Theorem spec_pow : forall x y, [pow x y] = [x] ^ [y].
+ Proof.
+ intros. unfold pow, to_N.
+ now rewrite spec_pow_N, Z_of_N_abs, Zabs_eq by apply spec_pos.
  Qed.
 
 
@@ -1000,8 +1010,6 @@ Module Make (W0:CyclicType) <: NType.
  intros p; exact (spec_of_pos p).
  Qed.
 
- Definition to_N (x : t) := Zabs_N (to_Z x).
-
  (** * [head0] and [tail0]
 
      Number of zero at the beginning and at the end of
@@ -1497,17 +1505,40 @@ Module Make (W0:CyclicType) <: NType.
 
  (** * Parity test *)
 
- Definition is_even : t -> bool := Eval red_t in
+ Definition even : t -> bool := Eval red_t in
    iter_t (fun n x => ZnZ.is_even x).
 
- Lemma is_even_fold : is_even = iter_t (fun n x => ZnZ.is_even x).
+ Definition odd x := negb (even x).
+
+ Lemma even_fold : even = iter_t (fun n x => ZnZ.is_even x).
  Proof. red_t; reflexivity. Qed.
 
- Theorem spec_is_even: forall x,
-   if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1.
+ Theorem spec_even_aux: forall x,
+   if even x then [x] mod 2 = 0 else [x] mod 2 = 1.
  Proof.
- intros x. rewrite is_even_fold. destr_t x as (n,x).
+ intros x. rewrite even_fold. destr_t x as (n,x).
  exact (ZnZ.spec_is_even x).
  Qed.
 
+ Theorem spec_even: forall x, even x = Zeven_bool [x].
+ Proof.
+ intros x. assert (H := spec_even_aux x). symmetry.
+ rewrite (Z_div_mod_eq_full [x] 2); auto with zarith.
+ destruct (even x); rewrite H, ?Zplus_0_r.
+ rewrite Zeven_bool_iff. apply Zeven_2p.
+ apply not_true_is_false. rewrite Zeven_bool_iff.
+ apply Zodd_not_Zeven. apply Zodd_2p_plus_1.
+ Qed.
+
+ Theorem spec_odd: forall x, odd x = Zodd_bool [x].
+ Proof.
+ intros x. unfold odd.
+ assert (H := spec_even_aux x). symmetry.
+ rewrite (Z_div_mod_eq_full [x] 2); auto with zarith.
+ destruct (even x); rewrite H, ?Zplus_0_r; simpl negb.
+ apply not_true_is_false. rewrite Zodd_bool_iff.
+ apply Zeven_not_Zodd. apply Zeven_2p.
+ apply Zodd_bool_iff. apply Zodd_2p_plus_1.
+ Qed.
+
 End Make.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 0d6c379e05..65b166df60 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -10,14 +10,14 @@
 
 Require Import BinPos Ndiv_def.
 Require Export BinNat.
-Require Import NAxioms NProperties NDiv.
+Require Import NAxioms NProperties.
 
 Local Open Scope N_scope.
 
 (** * Implementation of [NAxiomsSig] module type via [BinNat.N] *)
 
 Module Type N
- <: NAxiomsSig <: UsualOrderedTypeFull <: TotalOrder <: DecidableTypeFull.
+ <: NAxiomsMiniSig <: UsualOrderedTypeFull <: TotalOrder <: DecidableTypeFull.
 
 (** Bi-directional induction. *)
 
@@ -144,6 +144,19 @@ Program Instance mod_wd : Proper (eq==>eq==>eq) Nmod.
 Definition div_mod := fun x y (_:y<>0) => Ndiv_mod_eq x y.
 Definition mod_upper_bound := Nmod_lt.
 
+(** Odd and Even *)
+
+Definition Even n := exists m, n = 2*m.
+Definition Odd n := exists m, n = 2*m+1.
+Definition even_spec := Neven_spec.
+Definition odd_spec := Nodd_spec.
+
+(** Power *)
+
+Definition pow_0_r := Npow_0_r.
+Definition pow_succ_r n p (H:0 <= p) := Npow_succ_r n p.
+Program Instance pow_wd : Proper (eq==>eq==>eq) Npow.
+
 (** The instantiation of operations.
     Placing them at the very end avoids having indirections in above lemmas. *)
 
@@ -164,14 +177,13 @@ Definition min := Nmin.
 Definition max := Nmax.
 Definition div := Ndiv.
 Definition modulo := Nmod.
+Definition pow := Npow.
+Definition even := Neven.
+Definition odd := Nodd.
 
-Include NPropFunct
+Include NProp
  <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
-(** Generic properties of [div] and [mod] *)
-
-Include NDivPropFunct.
-
 End N.
 
 (*
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 182b9b8dd6..5bb26d04f2 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -8,25 +8,131 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-Require Import Peano Peano_dec Compare_dec EqNat NAxioms NProperties NDiv.
+Require Import
+ Bool Peano Peano_dec Compare_dec Plus Minus Le EqNat NAxioms NProperties.
 
-(** Functions not already defined: div mod *)
+(** Functions not already defined *)
 
-Definition divF div x y := if leb y x then S (div (x-y) y) else 0.
-Definition modF mod x y := if leb y x then mod (x-y) y else x.
-Definition initF (_ _ : nat) := 0.
+Fixpoint pow n m :=
+  match m with
+    | O => 1
+    | S m => n * (pow n m)
+  end.
 
-Fixpoint loop {A} (F:A->A)(i:A) (n:nat) : A :=
- match n with
-  | 0 => i
-  | S n => F (loop F i n)
- end.
+Infix "^" := pow : nat_scope.
+
+Lemma pow_0_r : forall a, a^0 = 1.
+Proof. reflexivity. Qed.
+
+Lemma pow_succ_r : forall a b, 0<=b -> a^(S b) = a * a^b.
+Proof. reflexivity. Qed.
+
+Definition Even n := exists m, n = 2*m.
+Definition Odd n := exists m, n = 2*m+1.
+
+Fixpoint even n :=
+  match n with
+    | O => true
+    | 1 => false
+    | S (S n') => even n'
+  end.
+
+Definition odd n := negb (even n).
+
+Lemma even_spec : forall n, even n = true <-> Even n.
+Proof.
+ fix 1.
+  destruct n as [|[|n]]; simpl; try rewrite even_spec; split.
+  now exists 0.
+  trivial.
+  discriminate.
+  intros (m,H). destruct m. discriminate.
+   simpl in H. rewrite <- plus_n_Sm in H. discriminate.
+  intros (m,H). exists (S m). rewrite H. simpl. now rewrite plus_n_Sm.
+  intros (m,H). destruct m. discriminate. exists m.
+   simpl in H. rewrite <- plus_n_Sm in H. inversion H. reflexivity.
+Qed.
+
+Lemma odd_spec : forall n, odd n = true <-> Odd n.
+Proof.
+ unfold odd.
+ fix 1.
+  destruct n as [|[|n]]; simpl; try rewrite odd_spec; split.
+  discriminate.
+  intros (m,H). rewrite <- plus_n_Sm in H; discriminate.
+  now exists 0.
+  trivial.
+  intros (m,H). exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m).
+  intros (m,H). destruct m. discriminate. exists m.
+   simpl in H. rewrite <- plus_n_Sm in H. inversion H. simpl.
+   now rewrite <- !plus_n_Sm, <- !plus_n_O.
+Qed.
+
+(* A linear, tail-recursive, division for nat.
+
+   In [divmod], [y] is the predecessor of the actual divisor,
+   and [u] is [y] minus the real remainder
+*)
+
+Fixpoint divmod x y q u :=
+  match x with
+    | 0 => (q,u)
+    | S x' => match u with
+                | 0 => divmod x' y (S q) y
+                | S u' => divmod x' y q u'
+              end
+  end.
+
+Definition div x y :=
+  match y with
+    | 0 => 0
+    | S y' => fst (divmod x y' 0 y')
+  end.
+
+Definition modulo x y :=
+  match y with
+    | 0 => 0
+    | S y' => y' - snd (divmod x y' 0 y')
+  end.
 
-Definition div x y := loop divF initF x x y.
-Definition modulo x y := loop modF initF x x y.
 Infix "/" := div : nat_scope.
 Infix "mod" := modulo (at level 40, no associativity) : nat_scope.
 
+Lemma divmod_spec : forall x y q u, u <= y ->
+ let (q',u') := divmod x y q u in
+ x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y.
+Proof.
+ induction x. simpl. intuition.
+ intros y q u H. destruct u; simpl divmod.
+ generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u').
+ intros (EQ,LE); split; trivial.
+ rewrite <- EQ, <- minus_n_O, minus_diag, <- plus_n_O.
+ now rewrite !plus_Sn_m, plus_n_Sm, <- plus_assoc, mult_n_Sm.
+ generalize (IHx y q u (le_Sn_le _ _ H)). destruct divmod as (q',u').
+ intros (EQ,LE); split; trivial.
+ rewrite <- EQ.
+ rewrite !plus_Sn_m, plus_n_Sm. f_equal. now apply minus_Sn_m.
+Qed.
+
+Lemma div_mod : forall x y, y<>0 -> x = y*(x/y) + x mod y.
+Proof.
+ intros x y Hy.
+ destruct y; [ now elim Hy | clear Hy ].
+ unfold div, modulo.
+ generalize (divmod_spec x y 0 y (le_n y)).
+ destruct divmod as (q,u).
+ intros (U,V).
+ simpl in *.
+ now rewrite <- mult_n_O, minus_diag, <- !plus_n_O in U.
+Qed.
+
+Lemma mod_upper_bound : forall x y, y<>0 -> x mod y < y.
+Proof.
+ intros x y Hy.
+ destruct y; [ now elim Hy | clear Hy ].
+ unfold modulo.
+ apply le_n_S, le_minus.
+Qed.
 
 (** * Implementation of [NAxiomsSig] by [nat] *)
 
@@ -119,25 +225,26 @@ Proof.
 reflexivity.
 Qed.
 
-Definition recursion (A : Type) : A -> (nat -> A -> A) -> nat -> A :=
+(** Recursion fonction *)
+
+Definition recursion {A} : A -> (nat -> A -> A) -> nat -> A :=
   nat_rect (fun _ => A).
-Implicit Arguments recursion [A].
 
-Instance recursion_wd (A : Type) (Aeq : relation A) :
- Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
+Instance recursion_wd {A} (Aeq : relation A) :
+ Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion.
 Proof.
 intros a a' Ha f f' Hf n n' Hn. subst n'.
 induction n; simpl; auto. apply Hf; auto.
 Qed.
 
 Theorem recursion_0 :
-  forall (A : Type) (a : A) (f : nat -> A -> A), recursion a f 0 = a.
+  forall {A} (a : A) (f : nat -> A -> A), recursion a f 0 = a.
 Proof.
 reflexivity.
 Qed.
 
 Theorem recursion_succ :
-  forall (A : Type) (Aeq : relation A) (a : A) (f : nat -> A -> A),
+  forall {A} (Aeq : relation A) (a : A) (f : nat -> A -> A),
     Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
       forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).
 Proof.
@@ -171,56 +278,29 @@ Definition eqb_eq := beq_nat_true_iff.
 Definition compare_spec := nat_compare_spec.
 Definition eq_dec := eq_nat_dec.
 
-(** Generic Properties *)
-
-Include NPropFunct
- <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
-
-(** Proofs of specification for [div] and [mod]. *)
+Definition Even := Even.
+Definition Odd := Odd.
+Definition even := even.
+Definition odd := odd.
+Definition even_spec := even_spec.
+Definition odd_spec := odd_spec.
 
-Lemma div_mod : forall x y, y<>0 -> x = y*(x/y) + x mod y.
-Proof.
- cut (forall n x y, y<>0 -> x<=n ->
-       x = y*(loop divF initF n x y) + (loop modF initF n x y)).
- intros H x y Hy. apply H; auto.
- induction n.
- simpl; unfold initF; simpl. intros. nzsimpl. auto with arith.
- simpl; unfold divF at 1, modF at 1.
- intros.
- destruct (leb y x) as [ ]_eqn:L;
-  [apply leb_complete in L | apply leb_complete_conv in L; now nzsimpl].
- rewrite mul_succ_r, <- add_assoc, (add_comm y), add_assoc.
- rewrite <- IHn; auto.
- symmetry; apply sub_add; auto.
- rewrite <- lt_succ_r.
- apply lt_le_trans with x; auto.
- apply sub_lt; auto. rewrite <- neq_0_lt_0; auto.
-Qed.
-
-Lemma mod_upper_bound : forall x y, y<>0 -> x mod y < y.
-Proof.
- cut (forall n x y, y<>0 -> x<=n -> loop modF initF n x y < y).
- intros H x y Hy. apply H; auto.
- induction n.
- simpl; unfold initF. intros. rewrite <- neq_0_lt_0; auto.
- simpl; unfold modF at 1.
- intros.
- destruct (leb y x) as [ ]_eqn:L;
-  [apply leb_complete in L | apply leb_complete_conv in L]; auto.
- apply IHn; auto.
- rewrite <- lt_succ_r.
- apply lt_le_trans with x; auto.
- apply sub_lt; auto. rewrite <- neq_0_lt_0; auto.
-Qed.
+Definition pow := pow.
+Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
+Definition pow_0_r := pow_0_r.
+Definition pow_succ_r := pow_succ_r.
 
 Definition div := div.
 Definition modulo := modulo.
 Program Instance div_wd : Proper (eq==>eq==>eq) div.
 Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+Definition div_mod := div_mod.
+Definition mod_upper_bound := mod_upper_bound.
 
-(** Generic properties of [div] and [mod] *)
+(** Generic Properties *)
 
-Include NDivPropFunct.
+Include NProp
+ <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 End Nat.
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index ba28647605..3ff2ded62d 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -46,8 +46,9 @@ Module Type NType.
  Parameter sub : t -> t -> t.
  Parameter mul : t -> t -> t.
  Parameter square : t -> t.
- Parameter power_pos : t -> positive -> t.
- Parameter power : t -> N -> t.
+ Parameter pow_pos : t -> positive -> t.
+ 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.
@@ -56,7 +57,8 @@ Module Type NType.
  Parameter gcd : t -> t -> t.
  Parameter shiftr : t -> t -> t.
  Parameter shiftl : t -> t -> t.
- Parameter is_even : t -> bool.
+ Parameter even : t -> bool.
+ Parameter odd : t -> bool.
 
  Parameter spec_compare: forall x y, compare x y = Zcompare [x] [y].
  Parameter spec_eq_bool: forall x y, eq_bool x y = Zeq_bool [x] [y].
@@ -70,8 +72,9 @@ Module Type NType.
  Parameter spec_sub: forall x y, [sub x y] = Zmax 0 ([x] - [y]).
  Parameter spec_mul: forall x y, [mul x y] = [x] * [y].
  Parameter spec_square: forall x, [square x] = [x] *  [x].
- Parameter spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.
- Parameter spec_power: forall x n, [power x n] = [x] ^ Z_of_N n.
+ Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
+ 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] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.
  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).
@@ -82,8 +85,8 @@ Module Type NType.
  Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
  Parameter spec_shiftr: forall p x, [shiftr p x] = [x] / 2^[p].
  Parameter spec_shiftl: forall p x, [shiftl p x] = [x] * 2^[p].
- Parameter spec_is_even: forall x,
-  if is_even x then [x] mod 2 = 0 else [x] mod 2 = 1.
+ Parameter spec_even: forall x, even x = Zeven_bool [x].
+ Parameter spec_odd: forall x, odd x = Zodd_bool [x].
 
 End NType.
 
@@ -94,6 +97,7 @@ Module Type NType_Notation (Import N:NType).
  Infix "+" := add.
  Infix "-" := sub.
  Infix "*" := mul.
+ Infix "^" := pow.
  Infix "<=" := le.
  Infix "<" := lt.
 End NType_Notation.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 90dd162498..568ebeae86 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -13,13 +13,13 @@ Require Import ZArith Nnat NAxioms NDiv NSig.
 Module NTypeIsNAxioms (Import N : NType').
 
 Hint Rewrite
- spec_0 spec_succ spec_add spec_mul spec_pred spec_sub
+ spec_0 spec_1 spec_succ spec_add spec_mul spec_pred spec_sub
  spec_div spec_modulo spec_gcd spec_compare spec_eq_bool
- spec_max spec_min spec_power_pos spec_power
+ 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; repeat red; intros; nsimpl; congruence.
-Ltac zify := unfold eq, lt, le in *; nsimpl.
+Ltac ncongruence := unfold eq, to_N; repeat red; intros; nsimpl; congruence.
+Ltac zify := unfold eq, lt, le, to_N in *; nsimpl.
 
 Local Obligation Tactic := ncongruence.
 
@@ -177,6 +177,70 @@ Proof.
 zify. auto.
 Qed.
 
+(** Power *)
+
+Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
+
+Local Notation "1" := (succ 0).
+Local Notation "2" := (succ 1).
+
+Lemma pow_0_r : forall a, a^0 == 1.
+Proof.
+ intros. now zify.
+Qed.
+
+Lemma pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b.
+Proof.
+ intros a b. zify. intro Hb.
+ rewrite Zpower_exp; auto with zarith.
+ simpl. unfold Zpower_pos; simpl. ring.
+Qed.
+
+Lemma pow_pow_N : forall a b, a^b == pow_N a (to_N b).
+Proof.
+ intros. zify. f_equal.
+ now rewrite Z_of_N_abs, Zabs_eq by apply spec_pos.
+Qed.
+
+Lemma pow_N_pow : forall a b, pow_N a b == a^(of_N b).
+Proof.
+ intros. zify. f_equal. symmetry. apply spec_of_N.
+Qed.
+
+Lemma pow_pos_N : forall a p, pow_pos a p == pow_N a (Npos p).
+Proof.
+ intros. now zify.
+Qed.
+
+(** Even / Odd *)
+
+Definition Even n := exists m, n == 2*m.
+Definition Odd n := exists m, n == 2*m+1.
+
+Lemma even_spec : forall n, even n = true <-> Even n.
+Proof.
+ intros n. unfold Even. zify.
+ rewrite Zeven_bool_iff, Zeven_ex_iff.
+ split; intros (m,Hm).
+ exists (of_N (Zabs_N m)).
+ zify. rewrite spec_of_N, Z_of_N_abs, Zabs_eq; auto.
+ generalize (spec_pos n); auto with zarith.
+ exists [m]. revert Hm. now zify.
+Qed.
+
+Lemma odd_spec : forall n, odd n = true <-> Odd n.
+Proof.
+ intros n. unfold Odd. zify.
+ rewrite Zodd_bool_iff, Zodd_ex_iff.
+ split; intros (m,Hm).
+ exists (of_N (Zabs_N m)).
+ zify. rewrite spec_of_N, Z_of_N_abs, Zabs_eq; auto.
+ generalize (spec_pos n); auto with zarith.
+ exists [m]. revert Hm. now zify.
+Qed.
+
+(** Div / Mod *)
+
 Program Instance div_wd : Proper (eq==>eq==>eq) div.
 Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 
@@ -192,6 +256,8 @@ destruct (Z_mod_lt [a] [b]); auto.
 generalize (spec_pos b); auto with zarith.
 Qed.
 
+(** Recursion *)
+
 Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) :=
   Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n).
 Implicit Arguments recursion [A].
@@ -250,5 +316,5 @@ Qed.
 End NTypeIsNAxioms.
 
 Module NType_NAxioms (N : NType)
- <: NAxiomsSig <: NDivSig <: HasCompare N <: HasEqBool N <: HasMinMax N
+ <: NAxiomsSig <: HasCompare N <: HasEqBool N <: HasMinMax N
  := N <+ NTypeIsNAxioms.