Diamond-shape instead of linear hiearchy in Numbers/NatInt

NZBase -- NZAdd -- NZMul
 |                  |
NZOrder ---------- NZAddOrder -- NZMulOrder -- NZProperties

This is done by transforming NZBase into a
functorial module type, and making NZAdd NZMul NZOrder
accept an instance of NZBase as parameter. This is possible
thanks to a combination of various new features of modules:
 - interactive proofs in module type (ie functors can be
   turned into type functors)
 - Include Type in Module (ie type functors can be turned
   into functors)
 - Include Self, <+ , etc, etc...

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

6 files changed, 37 insertions, 25 deletions

diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index f7e6699aba..579d2197f5 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -13,8 +13,7 @@
 Require Import NZAxioms.
 Require Import NZBase.
 
-Module NZAddPropFunct (Import NZ : NZAxiomsSig).
-Include NZBasePropFunct NZ.
+Module NZAddProp (Import NZ : NZAxiomsSig)(Import NZBase : NZBaseProp NZ).
 Local Open Scope NumScope.
 
 Hint Rewrite
@@ -87,5 +86,6 @@ Proof.
 intro n; now nzsimpl.
 Qed.
 
-End NZAddPropFunct.
+End NZAddProp.
 
+Module NZAddPropFunct (NZ : NZAxiomsSig) := NZBasePropFunct NZ <+ NZAddProp NZ.
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index fcfbfd123c..b51216fd25 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -10,10 +10,12 @@
 
 (*i $Id$ i*)
 
-Require Import NZAxioms NZOrder.
+Require Import NZAxioms NZBase NZMul NZOrder.
 
-Module NZAddOrderPropFunct (Import NZ : NZOrdAxiomsSig).
-Include NZOrderPropFunct NZ.
+Module NZAddOrderProp
+ (Import NZ : NZOrdAxiomsSig)(Import NZBase : NZBaseProp NZ).
+Include NZMulProp NZ NZBase.
+Include NZOrderProp NZ NZBase.
 Local Open Scope NumScope.
 
 Theorem add_lt_mono_l : forall n m p, n < m <-> p + n < p + m.
@@ -150,5 +152,8 @@ Proof.
 intros n m H; apply add_le_cases; now nzsimpl.
 Qed.
 
-End NZAddOrderPropFunct.
+End NZAddOrderProp.
+
+Module NZAddOrderPropFunct (NZ:NZOrdAxiomsSig) :=
+ NZBasePropFunct NZ <+ NZAddOrderProp NZ.
 
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 889d9c2e53..20a85e2ef5 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -10,8 +10,7 @@
 
 (*i $Id$ i*)
 
-Require Import DecidableType2 OrderedType2.
-Require Export NumPrelude.
+Require Export DecidableType2 OrderedType2 NumPrelude.
 
 Delimit Scope NumScope with Num.
 Local Open Scope NumScope.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index b958245652..2decfafca1 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -12,12 +12,10 @@
 
 Require Import NZAxioms.
 
-Module NZBasePropFunct (Import NZ : NZAxiomsSig).
+Module Type NZBaseProp (Import NZ : NZDomainSig).
 Local Open Scope NumScope.
 
-Definition eq_refl := @Equivalence_Reflexive _ _ eq_equiv.
-Definition eq_sym := @Equivalence_Symmetric _ _ eq_equiv.
-Definition eq_trans := @Equivalence_Transitive _ _ eq_equiv.
+Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *)
 
 (* TODO: how register ~= (which is just a notation) as a Symmetric relation,
     hence allowing "symmetry" tac ? *)
@@ -83,5 +81,9 @@ 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.
 
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index c76e25c64c..0daca2b875 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -10,11 +10,10 @@
 
 (*i $Id$ i*)
 
-Require Import NZAxioms.
-Require Import NZAdd.
+Require Import NZAxioms NZBase NZAdd.
 
-Module NZMulPropFunct (Import NZ : NZAxiomsSig).
-Include NZAddPropFunct NZ.
+Module NZMulProp (Import NZ : NZAxiomsSig)(Import NZBase : NZBaseProp NZ).
+Include NZAddProp NZ NZBase.
 Local Open Scope NumScope.
 
 Theorem mul_0_r : forall n, n * 0 == 0.
@@ -68,5 +67,6 @@ Proof.
 intro n. now nzsimpl.
 Qed.
 
-End NZMulPropFunct.
+End NZMulProp.
 
+Module NZMulPropFunct (NZ : NZAxiomsSig) := NZBasePropFunct NZ <+ NZMulProp NZ.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 4c54cc3b86..315d963c4c 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -10,13 +10,9 @@
 
 (*i $Id$ i*)
 
-Require Import NZAxioms.
-Require Import NZMul.
-Require Import Decidable.
-Require Import OrderTac.
+Require Import NZAxioms NZBase Decidable OrderTac.
 
-Module NZOrderPropFunct (Import NZ : NZOrdAxiomsSig).
-Include NZMulPropFunct NZ. (* In fact only NZBase is used here *)
+Module NZOrderProp (Import NZ : NZOrdSig)(Import NZBase : NZBaseProp NZ).
 Local Open Scope NumScope.
 
 Instance le_wd : Proper (eq==>eq==>iff) le.
@@ -653,6 +649,16 @@ Qed.
 
 End WF.
 
+End NZOrderProp.
+
+Module NZOrderPropFunct (NZ : NZOrdSig) := NZBasePropFunct NZ <+ NZOrderProp NZ.
+
+
+(** To Merge with GenericMinMax ... *)
+
+Module NZMinMaxPropFunct (Import NZ : NZOrdAxiomsSig).
+Include NZOrderPropFunct NZ.
+
 (** * Compatibility of [min] and [max]. *)
 
 Instance min_wd : Proper (eq==>eq==>eq) min.
@@ -671,5 +677,5 @@ rewrite 2 max_r; auto. now rewrite <-Hn,<-Hm.
 rewrite 2 max_l; auto. now rewrite <-Hn,<-Hm.
 Qed.
 
-End NZOrderPropFunct.
+End NZMinMaxPropFunct.