Numbers abstract layer: more Module Type, used especially for divisions.

 Properties are now rather passed as functor arg instead of via Include or
 some inner modules.

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

20 files changed, 50 insertions, 57 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 3429a4fa3..64a122c71 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -15,7 +15,7 @@ Require Export ZAxioms.
 Require Import NZProperties.
 
 Module ZBasePropFunct (Import Z : ZAxiomsSig).
-Include NZPropFunct Z.
+Include Type NZPropFunct Z.
 Local Open Scope NumScope.
 
 (* Theorems that are true for integers but not for natural numbers *)
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index ad8e24cfb..a853395a6 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -33,9 +33,7 @@ End ZDiv.
 
 Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
 
-Module ZDivPropFunct (Import Z : ZDivSig).
- (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *)
- Module Import ZP := ZPropFunct Z.
+Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
@@ -48,7 +46,7 @@ Module ZDivPropFunct (Import Z : ZDivSig).
   apply le_trans with 0; [ rewrite opp_nonpos_nonneg |]; order.
   Qed.
  End Z'.
- Module Import NZDivP := NZDivPropFunct Z'.
+ Module Import NZDivP := NZDivPropFunct Z' ZP.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index fe695907d..551ce6b41 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -36,9 +36,7 @@ End ZDiv.
 
 Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
 
-Module ZDivPropFunct (Import Z : ZDivSig).
- (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *)
- Module Import ZP := ZPropFunct Z.
+Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
@@ -47,7 +45,7 @@ Module ZDivPropFunct (Import Z : ZDivSig).
   Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
   Proof. intros. now apply mod_pos_bound. Qed.
  End Z'.
- Module Import NZDivP := NZDivPropFunct Z'.
+ Module Import NZDivP := NZDivPropFunct Z' ZP.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index b57f8e27f..c60bf7c6a 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -37,13 +37,11 @@ End ZDiv.
 
 Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
 
-Module ZDivPropFunct (Import Z : ZDivSig).
- (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *)
- Module Import ZP := ZPropFunct Z.
+Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
- Module Import NZDivP := NZDivPropFunct Z.
+ Module Import NZDivP := NZDivPropFunct Z ZP.
 
 Ltac pos_or_neg a :=
  let LT := fresh "LT" in
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index a9cf0dc4d..bd9a85714 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -12,7 +12,7 @@
 
 Require Export ZAddOrder.
 
-Module ZMulOrderPropFunct (Import Z : ZAxiomsSig).
+Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig).
 Include ZAddOrderPropFunct Z.
 Local Open Scope NumScope.
 
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index eee5b0273..7f2253205 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -15,4 +15,9 @@ Require Export ZAxioms ZMulOrder.
     subsumes all others.
 *)
 
-Module ZPropFunct := ZMulOrderPropFunct.
+Module Type ZPropSig := ZMulOrderPropFunct.
+
+Module ZPropFunct (Z:ZAxiomsSig) <: ZPropSig Z.
+ Include Type ZPropSig Z.
+End ZPropFunct.
+
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 785abb5c7..bca7c3682 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -13,7 +13,8 @@
 Require Import NZAxioms.
 Require Import NZBase.
 
-Module NZAddProp (Import NZ : NZAxiomsSig)(Import NZBase : NZBaseProp NZ).
+Module Type NZAddPropSig
+ (Import NZ : NZAxiomsSig)(Import NZBase : NZBasePropSig NZ).
 Local Open Scope NumScope.
 
 Hint Rewrite
@@ -88,6 +89,4 @@ Proof.
 intro n; now nzsimpl.
 Qed.
 
-End NZAddProp.
-
-Module NZAddPropFunct (NZ : NZAxiomsSig) := NZBasePropFunct NZ <+ NZAddProp NZ.
+End NZAddPropSig.
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index b51216fd2..56982c616 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -12,10 +12,8 @@
 
 Require Import NZAxioms NZBase NZMul NZOrder.
 
-Module NZAddOrderProp
- (Import NZ : NZOrdAxiomsSig)(Import NZBase : NZBaseProp NZ).
-Include NZMulProp NZ NZBase.
-Include NZOrderProp NZ NZBase.
+Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig).
+Include Type NZBasePropSig NZ <+ NZMulPropSig NZ <+ NZOrderPropSig NZ.
 Local Open Scope NumScope.
 
 Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
@@ -152,8 +150,5 @@ Proof.
 intros n m H; apply add_le_cases; now nzsimpl.
 Qed.
 
-End NZAddOrderProp.
-
-Module NZAddOrderPropFunct (NZ:NZOrdAxiomsSig) :=
- NZBasePropFunct NZ <+ NZAddOrderProp NZ.
+End NZAddOrderPropSig.
 
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 1215bfba2..04955b3b3 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -12,7 +12,7 @@
 
 Require Import NZAxioms.
 
-Module Type NZBaseProp (Import NZ : NZDomainSig).
+Module Type NZBasePropSig (Import NZ : NZDomainSig).
 Local Open Scope NumScope.
 
 Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *)
@@ -86,9 +86,5 @@ Tactic Notation "nzinduct" ident(n) :=
 Tactic Notation "nzinduct" ident(n) constr(u) :=
   induction_maker n ltac:(apply central_induction with (z := u)).
 
-End NZBaseProp.
-
-Module NZBasePropFunct (NZ : NZDomainSig).
- Include Type NZBaseProp NZ.
-End NZBasePropFunct.
+End NZBasePropSig.
 
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 5b81cadd2..db64a7963 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -38,9 +38,8 @@ End NZDiv.
 
 Module Type NZDivSig := NZOrdAxiomsSig <+ NZDiv.
 
-Module NZDivPropFunct (Import NZ : NZDivSig).
- (* TODO: a transformer un jour en arg funct puis include *)
- Module Import P := NZMulOrderPropFunct NZ.
+Module NZDivPropFunct
+ (Import NZ : NZDivSig)(Import NZP : NZMulOrderPropSig NZ).
 
 (** Uniqueness theorems *)
 
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 0daca2b87..e7c9b05e0 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -12,8 +12,9 @@
 
 Require Import NZAxioms NZBase NZAdd.
 
-Module NZMulProp (Import NZ : NZAxiomsSig)(Import NZBase : NZBaseProp NZ).
-Include NZAddProp NZ NZBase.
+Module Type NZMulPropSig
+ (Import NZ : NZAxiomsSig)(Import NZBase : NZBasePropSig NZ).
+Include Type NZAddPropSig NZ NZBase.
 Local Open Scope NumScope.
 
 Theorem mul_0_r : forall n, n * 0 == 0.
@@ -67,6 +68,4 @@ Proof.
 intro n. now nzsimpl.
 Qed.
 
-End NZMulProp.
-
-Module NZMulPropFunct (NZ : NZAxiomsSig) := NZBasePropFunct NZ <+ NZMulProp NZ.
+End NZMulPropSig.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index b6e4849f5..a4d8a3972 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -13,8 +13,8 @@
 Require Import NZAxioms.
 Require Import NZAddOrder.
 
-Module NZMulOrderPropFunct (Import NZ : NZOrdAxiomsSig).
-Include NZAddOrderPropFunct NZ.
+Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig).
+Include Type NZAddOrderPropSig NZ.
 Local Open Scope NumScope.
 
 Theorem mul_lt_pred :
@@ -305,4 +305,4 @@ rewrite !mul_add_distr_r; nzsimpl; now rewrite le_succ_l.
 apply add_pos_pos; now apply lt_0_1.
 Qed.
 
-End NZMulOrderPropFunct.
+End NZMulOrderPropSig.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index c6815ebf5..a95de8df7 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -12,7 +12,8 @@
 
 Require Import NZAxioms NZBase Decidable OrderTac.
 
-Module NZOrderProp (Import NZ : NZOrdSig)(Import NZBase : NZBaseProp NZ).
+Module Type NZOrderPropSig
+ (Import NZ : NZOrdSig)(Import NZBase : NZBasePropSig NZ).
 Local Open Scope NumScope.
 
 Instance le_wd : Proper (eq==>eq==>iff) le.
@@ -613,9 +614,11 @@ Qed.
 
 End WF.
 
-End NZOrderProp.
+End NZOrderPropSig.
 
-Module NZOrderPropFunct (NZ : NZOrdSig) := NZBasePropFunct NZ <+ NZOrderProp NZ.
+Module NZOrderPropFunct (Import NZ : NZOrdSig).
+ Include Type NZBasePropSig NZ <+ NZOrderPropSig NZ.
+End NZOrderPropFunct.
 
 
 (** To Merge with GenericMinMax ... *)
diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v
index 781d06594..125b4f62c 100644
--- a/theories/Numbers/NatInt/NZProperties.v
+++ b/theories/Numbers/NatInt/NZProperties.v
@@ -17,4 +17,4 @@ Require Export NZAxioms NZMulOrder.
     subsumes all others.
 *)
 
-Module NZPropFunct := NZMulOrderPropFunct.
+Module Type NZPropFunct := NZMulOrderPropSig.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 6bf12ee5e..4095fbb50 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -16,7 +16,7 @@ Require Import NZProperties.
 
 Module NBasePropFunct (Import N : NAxiomsSig).
 (** First, we import all known facts about both natural numbers and integers. *)
-Include NZPropFunct N.
+Include Type NZPropFunct N.
 Local Open Scope NumScope.
 
 (** We prove that the successor of a number is not zero by defining a
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index 6c417868a..9e446dc69 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.v
@@ -19,8 +19,7 @@ End NDiv.
 
 Module Type NDivSig := NAxiomsSig <+ NDiv.
 
-Module NDivPropFunct (Import N : NDivSig).
- Module Import NP := NPropFunct N.
+Module NDivPropFunct (Import N : NDivSig)(Import NP : NPropSig N).
 
 (** We benefit from what already exists for NZ *)
 
@@ -29,7 +28,7 @@ Module NDivPropFunct (Import N : NDivSig).
   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 N'.
- Module Import NZDivP := NZDivPropFunct N'.
+ Module Import NZDivP := NZDivPropFunct N' NP.
 
  Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l.
 
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index 29bda136a..f59d5b1e7 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -15,4 +15,8 @@ Require Export NAxioms NSub.
     subsumes all others.
 *)
 
-Module NPropFunct := NSubPropFunct.
+Module Type NPropSig := NSubPropFunct.
+
+Module NPropFunct (N:NAxiomsSig). (* <: NPropSig N.  BUG !! *)
+ Include Type NPropSig N.
+End NPropFunct.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index fee9b4372..7629aa11b 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -16,7 +16,7 @@ and proves its properties *)
 Require Export NSub.
 
 Module NStrongRecPropFunct (Import N : NAxiomsSig).
-Include NSubPropFunct N.
+Include Type NSubPropFunct N.
 Local Open Scope NumScope.
 
 Section StrongRecursion.
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v
index 62d1c731c..e027c0be2 100644
--- a/theories/Numbers/Natural/Abstract/NSub.v
+++ b/theories/Numbers/Natural/Abstract/NSub.v
@@ -12,7 +12,7 @@
 
 Require Export NMulOrder.
 
-Module NSubPropFunct (Import N : NAxiomsSig).
+Module Type NSubPropFunct (Import N : NAxiomsSig).
 Include NMulOrderPropFunct N.
 Local Open Scope NumScope.
 
@@ -220,7 +220,7 @@ Qed.
 
 Theorem add_dichotomy :
   forall n m, (exists p, p + n == m) \/ (exists p, p + m == n).
-Proof le_alt_dichotomy.
+Proof. exact le_alt_dichotomy. Qed.
 
 End NSubPropFunct.
 
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 97ac9f872..73affd90d 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -232,4 +232,4 @@ Module NDivMod <: NDivSig.
  Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 End NDivMod.
 
-Module Export NDivPropMod := NDivPropFunct NDivMod.
+Module Export NDivPropMod := NDivPropFunct NDivMod NPeanoPropMod.