Numbers: separation of funs, notations, axioms. Notations via module, without scope.

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

9 files changed, 104 insertions, 165 deletions

diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index bca7c3682b..9535cfdb4a 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -10,12 +10,10 @@
 
 (*i $Id$ i*)
 
-Require Import NZAxioms.
-Require Import NZBase.
+Require Import NZAxioms NZBase.
 
 Module Type NZAddPropSig
- (Import NZ : NZAxiomsSig)(Import NZBase : NZBasePropSig NZ).
-Local Open Scope NumScope.
+ (Import NZ : NZAxiomsSig')(Import NZBase : NZBasePropSig NZ).
 
 Hint Rewrite
  pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz.
diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index 56982c616f..7313c4131c 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -12,9 +12,8 @@
 
 Require Import NZAxioms NZBase NZMul NZOrder.
 
-Module Type NZAddOrderPropSig (Import NZ : NZOrdAxiomsSig).
+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.
 Proof.
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index f6328e2498..5b4e16cafe 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -10,10 +10,7 @@
 
 (*i $Id$ i*)
 
-Require Export DecidableType2 OrderedType2 NumPrelude.
-
-Delimit Scope NumScope with Num.
-Local Open Scope NumScope.
+Require Export DecidableType2 OrderedType2 NumPrelude GenericMinMax.
 
 (** Axiomatization of a domain with zero, successor, predecessor,
     and a bi-directional induction principle. We require [P (S n) = n]
@@ -22,121 +19,93 @@ Local Open Scope NumScope.
     for instance [Z/nZ] (See file [NZDomain for a study of that).
 *)
 
-Module Type NZDomain (Import E : EqualityType).
- (** [E] provides [t], [eq], [eq_equiv : Equivalence eq] *)
-
-Notation "x == y"  := (eq x y) (at level 70) : NumScope.
-Notation "x ~= y" := (~ eq x y) (at level 70) : NumScope.
-
-Parameter Inline zero : t.
-Parameter Inline succ : t -> t.
-Parameter Inline pred : t -> t.
-
-Notation "0" := zero : NumScope.
-Notation S := succ.
-Notation P := pred.
-Notation "1" := (S 0) : NumScope.
-
-Declare Instance succ_wd : Proper (eq ==> eq) S.
-Declare Instance pred_wd : Proper (eq ==> eq) P.
-
-Axiom pred_succ : forall n, P (S n) == n.
-
-Axiom bi_induction :
+Module Type ZeroSuccPred (Import T:Typ).
+ Parameter Inline zero : t.
+ Parameters Inline succ pred : t -> t.
+End ZeroSuccPred.
+
+Module Type ZeroSuccPredNotation (T:Typ)(Import NZ:ZeroSuccPred T).
+ Notation "0" := zero.
+ Notation S := succ.
+ Notation P := pred.
+ Notation "1" := (S 0).
+ Notation "2" := (S 1).
+End ZeroSuccPredNotation.
+
+Module Type ZeroSuccPred' (T:Typ) :=
+ ZeroSuccPred T <+ ZeroSuccPredNotation T.
+
+Module Type IsNZDomain (Import E:Eq')(Import NZ:ZeroSuccPred' E).
+ Declare Instance succ_wd : Proper (eq ==> eq) S.
+ Declare Instance pred_wd : Proper (eq ==> eq) P.
+ Axiom pred_succ : forall n, P (S n) == n.
+ Axiom bi_induction :
   forall A : t -> Prop, Proper (eq==>iff) A ->
     A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n.
+End IsNZDomain.
 
-End NZDomain.
-
-Module Type NZDomainSig := EqualityType <+ NZDomain.
-
-(** A version with decidable type *)
-
-Module Type NZDecDomainSig := DecidableType <+ NZDomain.
+Module Type NZDomainSig := EqualityType <+ ZeroSuccPred <+ IsNZDomain.
+Module Type NZDomainSig' := EqualityType' <+ ZeroSuccPred' <+ IsNZDomain.
 
 
 (** Axiomatization of basic operations : [+] [-] [*] *)
 
-Module Type NZHasBasicFuns (Import NZ : NZDomainSig).
-
-Parameter Inline add : t -> t -> t.
-Parameter Inline sub : t -> t -> t.
-Parameter Inline mul : t -> t -> t.
-
-Notation "x + y" := (add x y) : NumScope.
-Notation "x - y" := (sub x y) : NumScope.
-Notation "x * y" := (mul x y) : NumScope.
-
-Declare Instance add_wd : Proper (eq ==> eq ==> eq) add.
-Declare Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
-Declare Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
-
-Axiom add_0_l : forall n, (0 + n) == n.
-Axiom add_succ_l : forall n m, (S n) + m == S (n + m).
-
-Axiom sub_0_r : forall n, n - 0 == n.
-Axiom sub_succ_r : forall n m, n - (S m) == P (n - m).
-
-Axiom mul_0_l : forall n, 0 * n == 0.
-Axiom mul_succ_l : forall n m, S n * m == n * m + m.
-
-End NZHasBasicFuns.
-
-Module Type NZBasicFunsSig := NZDomainSig <+ NZHasBasicFuns.
-
+Module Type AddSubMul (Import T:Typ).
+ Parameters Inline add sub mul : t -> t -> t.
+End AddSubMul.
+
+Module Type AddSubMulNotation (T:Typ)(Import NZ:AddSubMul T).
+ Notation "x + y" := (add x y).
+ Notation "x - y" := (sub x y).
+ Notation "x * y" := (mul x y).
+End AddSubMulNotation.
+
+Module Type AddSubMul' (T:Typ) := AddSubMul T <+ AddSubMulNotation T.
+
+Module Type IsAddSubMul (Import E:NZDomainSig')(Import NZ:AddSubMul' E).
+ Declare Instance add_wd : Proper (eq ==> eq ==> eq) add.
+ Declare Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
+ Declare Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
+ Axiom add_0_l : forall n, 0 + n == n.
+ Axiom add_succ_l : forall n m, (S n) + m == S (n + m).
+ Axiom sub_0_r : forall n, n - 0 == n.
+ Axiom sub_succ_r : forall n m, n - (S m) == P (n - m).
+ Axiom mul_0_l : forall n, 0 * n == 0.
+ Axiom mul_succ_l : forall n m, S n * m == n * m + m.
+End IsAddSubMul.
+
+Module Type NZBasicFunsSig := NZDomainSig <+ AddSubMul <+ IsAddSubMul.
+Module Type NZBasicFunsSig' := NZDomainSig' <+ AddSubMul' <+IsAddSubMul.
 
 (** Old name for the same interface: *)
 
 Module Type NZAxiomsSig := NZBasicFunsSig.
-
+Module Type NZAxiomsSig' := NZBasicFunsSig'.
 
 (** Axiomatization of order *)
 
-Module Type NZHasOrd (Import NZ : NZDomainSig).
-
-Parameter Inline lt : t -> t -> Prop.
-Parameter Inline le : t -> t -> Prop.
+Module Type NZOrd := NZDomainSig <+ HasLt <+ HasLe.
+Module Type NZOrd' := NZDomainSig' <+ HasLt <+ HasLe <+
+                      LtNotation <+ LeNotation <+ LtLeNotation.
 
-Notation "x < y" := (lt x y) : NumScope.
-Notation "x <= y" := (le x y) : NumScope.
-Notation "x > y" := (lt y x) (only parsing) : NumScope.
-Notation "x >= y" := (le y x) (only parsing) : NumScope.
+Module Type IsNZOrd (Import NZ : NZOrd').
+ Declare Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+ Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
+ Axiom lt_irrefl : forall n, ~ (n < n).
+ Axiom lt_succ_r : forall n m, n < S m <-> n <= m.
+End IsNZOrd.
 
-Notation "x < y < z" := (x<y /\ y<z) : NumScope.
-Notation "x <= y <= z" := (x<=y /\ y<=z) : NumScope.
-Notation "x <= y < z" := (x<=y /\ y<z) : NumScope.
-Notation "x < y <= z" := (x<y /\ y<=z) : NumScope.
-
-Declare Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
-(** Compatibility of [le] can be proved later from [lt_wd]
+(** NB: the compatibility of [le] can be proved later from [lt_wd]
     and [lt_eq_cases] *)
 
-Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
-Axiom lt_irrefl : forall n, ~ (n < n).
-Axiom lt_succ_r : forall n m, n < S m <-> n <= m.
-
-End NZHasOrd.
-
-Module Type NZOrdSig := NZDomainSig <+ NZHasOrd.
-
-
-(** Axiomatization of minimum and maximum *)
-
-Module Type NZHasMinMax (Import NZ : NZOrdSig).
-
-Parameter Inline min : t -> t -> t.
-Parameter Inline max : t -> t -> t.
-
-(** Compatibility of [min] and [max] can be proved later *)
-
-Axiom min_l : forall n m, n <= m -> min n m == n.
-Axiom min_r : forall n m, m <= n -> min n m == m.
-Axiom max_l : forall n m, m <= n -> max n m == n.
-Axiom max_r : forall n m, n <= m -> max n m == m.
+Module Type NZOrdSig := NZOrd <+ IsNZOrd.
+Module Type NZOrdSig' := NZOrd' <+ IsNZOrd.
 
-End NZHasMinMax.
+(** Everything together : *)
 
+Module Type NZOrdAxiomsSig <: NZBasicFunsSig <: NZOrdSig
+ := NZOrdSig <+ AddSubMul <+ IsAddSubMul <+ HasMinMax.
+Module Type NZOrdAxiomsSig' <: NZOrdAxiomsSig
+ := NZOrdSig' <+ AddSubMul' <+ IsAddSubMul <+ HasMinMax.
 
-Module Type NZOrdAxiomsSig :=
- NZDomainSig <+ NZHasBasicFuns <+ NZHasOrd <+ NZHasMinMax.
 
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 04955b3b38..18e3b9b921 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -12,8 +12,7 @@
 
 Require Import NZAxioms.
 
-Module Type NZBasePropSig (Import NZ : NZDomainSig).
-Local Open Scope NumScope.
+Module Type NZBasePropSig (Import NZ : NZDomainSig').
 
 Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *)
 
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index da7d62ceb3..4acd6540d6 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -10,15 +10,20 @@
 
 Require Import NZAxioms NZMulOrder.
 
-Open Scope NumScope.
+(** The first signatures will be common to all divisions over NZ, N and Z *)
 
-(** This first signature will be common to all divisions over NZ, N and Z *)
+Module Type DivMod (Import T:Typ).
+ Parameters div modulo : t -> t -> t.
+End DivMod.
 
-Module Type NZDivCommon (Import NZ : NZAxiomsSig).
- Parameter Inline div : t -> t -> t.
- Parameter Inline modulo : t -> t -> t.
- Infix "/" := div : NumScope.
- Infix "mod" := modulo (at level 40, no associativity) : NumScope.
+Module Type DivModNotation (T:Typ)(Import NZ:DivMod T).
+ Infix "/" := div.
+ Infix "mod" := modulo (at level 40, no associativity).
+End DivModNotation.
+
+Module Type DivMod' (T:Typ) := DivMod T <+ DivModNotation T.
+
+Module Type NZDivCommon (Import NZ : NZAxiomsSig')(Import DM : DivMod' NZ).
  Declare Instance div_wd : Proper (eq==>eq==>eq) div.
  Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
  Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b).
@@ -31,15 +36,18 @@ End NZDivCommon.
     NB: This axiom would also be true for N and Z, but redundant.
 *)
 
-Module Type NZDiv (Import NZ : NZOrdAxiomsSig).
- Include Type NZDivCommon NZ.
+Module Type NZDivSpecific (Import NZ : NZOrdAxiomsSig')(Import DM : DivMod' NZ).
  Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
-End NZDiv.
+End NZDivSpecific.
+
+Module Type NZDiv (NZ:NZOrdAxiomsSig)
+ := DivMod NZ <+ NZDivCommon NZ <+ NZDivSpecific NZ.
 
 Module Type NZDivSig := NZOrdAxiomsSig <+ NZDiv.
+Module Type NZDivSig' := NZOrdAxiomsSig' <+ NZDiv <+ DivModNotation.
 
 Module NZDivPropFunct
- (Import NZ : NZDivSig)(Import NZP : NZMulOrderPropSig NZ).
+ (Import NZ : NZDivSig')(Import NZP : NZMulOrderPropSig NZ).
 
 (** Uniqueness theorems *)
 
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 6dcc9e91fe..eb06cae03c 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -55,8 +55,7 @@ Implicit Arguments iter [A].
 Local Infix "^" := iter.
 
 
-Module NZDomainProp (Import NZ:NZDomainSig).
-Local Open Scope NumScope.
+Module NZDomainProp (Import NZ:NZDomainSig').
 
 (** * Relationship between points thanks to [succ] and [pred]. *)
 
@@ -274,11 +273,11 @@ End NZDomainProp.
     First, relationship with [0], [succ], [pred].
 *)
 
-Module NZOfNat (Import NZ:NZDomainSig).
-Local Open Scope NumScope.
+Module NZOfNat (Import NZ:NZDomainSig').
 
 Definition ofnat (n : nat) : t := (S^n) 0.
-Notation "[ n ]" := (ofnat n) (at level 7) : NumScope.
+Notation "[ n ]" := (ofnat n) (at level 7) : ofnat.
+Local Open Scope ofnat.
 
 Lemma ofnat_zero : [O] == 0.
 Proof.
@@ -306,10 +305,10 @@ End NZOfNat.
     [ofnat] is injective, and hence that NZ is infinite
     (i.e. we ban Z/nZ models) *)
 
-Module NZOfNatOrd (Import NZ:NZOrdSig).
+Module NZOfNatOrd (Import NZ:NZOrdSig').
 Include NZOfNat NZ.
 Include NZOrderPropFunct NZ.
-Local Open Scope NumScope.
+Local Open Scope ofnat.
 
 Theorem ofnat_S_gt_0 :
   forall n : nat, 0 < [Datatypes.S n].
@@ -368,9 +367,9 @@ End NZOfNatOrd.
 (** For basic operations, we can prove correspondance with
     their counterpart in [nat]. *)
 
-Module NZOfNatOps (Import NZ:NZAxiomsSig).
+Module NZOfNatOps (Import NZ:NZAxiomsSig').
 Include NZOfNat NZ.
-Local Open Scope NumScope.
+Local Open Scope ofnat.
 
 Lemma ofnat_add_l : forall n m, [n]+m == (S^n) m.
 Proof.
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index e7c9b05e0c..3c11024e52 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -13,9 +13,8 @@
 Require Import NZAxioms NZBase NZAdd.
 
 Module Type NZMulPropSig
- (Import NZ : NZAxiomsSig)(Import NZBase : NZBasePropSig NZ).
+ (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.
 Proof.
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index a4d8a39729..18f61de598 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -13,9 +13,8 @@
 Require Import NZAxioms.
 Require Import NZAddOrder.
 
-Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig).
+Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig').
 Include Type NZAddOrderPropSig NZ.
-Local Open Scope NumScope.
 
 Theorem mul_lt_pred :
   forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n).
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index a95de8df79..6697c0b3dc 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -13,8 +13,7 @@
 Require Import NZAxioms NZBase Decidable OrderTac.
 
 Module Type NZOrderPropSig
- (Import NZ : NZOrdSig)(Import NZBase : NZBasePropSig NZ).
-Local Open Scope NumScope.
+ (Import NZ : NZOrdSig')(Import NZBase : NZBasePropSig NZ).
 
 Instance le_wd : Proper (eq==>eq==>iff) le.
 Proof.
@@ -137,11 +136,7 @@ Module OrderElts.
  Definition le_lteq := lt_eq_cases.
 End OrderElts.
 Module OrderTac := MakeOrderTac OrderElts.
-Ltac order :=
-  change eq with OrderElts.eq in *;
-  change lt with OrderElts.lt in *;
-  change le with OrderElts.le in *;
-  OrderTac.order.
+Ltac order := OrderTac.order.
 
 (** Some direct consequences of [order]. *)
 
@@ -620,29 +615,3 @@ Module NZOrderPropFunct (Import NZ : NZOrdSig).
  Include Type NZBasePropSig NZ <+ NZOrderPropSig NZ.
 End NZOrderPropFunct.
 
-
-(** 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.
-Proof.
-intros n n' Hn m m' Hm.
-destruct (le_ge_cases n m).
-rewrite 2 min_l; auto. now rewrite <-Hn,<-Hm.
-rewrite 2 min_r; auto. now rewrite <-Hn,<-Hm.
-Qed.
-
-Instance max_wd : Proper (eq==>eq==>eq) max.
-Proof.
-intros n n' Hn m m' Hm.
-destruct (le_ge_cases n m).
-rewrite 2 max_r; auto. now rewrite <-Hn,<-Hm.
-rewrite 2 max_l; auto. now rewrite <-Hn,<-Hm.
-Qed.
-
-End NZMinMaxPropFunct.
-