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

10 files changed, 48 insertions, 46 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index 26ba0a8d40..5663408d1b 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -12,9 +12,8 @@
 
 Require Export ZBase.
 
-Module ZAddPropFunct (Import Z : ZAxiomsSig).
+Module ZAddPropFunct (Import Z : ZAxiomsSig').
 Include ZBasePropFunct Z.
-Local Open Scope NumScope.
 
 (** Theorems that are either not valid on N or have different proofs
     on N and Z *)
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index 282709c475..de12993f89 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -12,9 +12,8 @@
 
 Require Export ZLt.
 
-Module ZAddOrderPropFunct (Import Z : ZAxiomsSig).
+Module ZAddOrderPropFunct (Import Z : ZAxiomsSig').
 Include ZOrderPropFunct Z.
-Local Open Scope NumScope.
 
 (** Theorems that are either not valid on N or have different proofs
     on N and Z *)
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 4b3d18be4b..9158a214da 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -14,22 +14,25 @@ Require Export NZAxioms.
 
 Set Implicit Arguments.
 
-Module Type ZAxiomsSig.
-Include Type NZOrdAxiomsSig.
-Local Open Scope NumScope.
+Module Type Opp (Import T:Typ).
+ Parameter Inline opp : t -> t.
+End Opp.
 
-Parameter Inline opp : t -> t.
-Declare Instance opp_wd : Proper (eq==>eq) opp.
+Module Type OppNotation (T:Typ)(Import O : Opp T).
+ Notation "- x" := (opp x) (at level 35, right associativity).
+End OppNotation.
 
-Notation "- x" := (opp x) (at level 35, right associativity) : NumScope.
-Notation "- 1" := (- (1)) : NumScope.
+Module Type Opp' (T:Typ) := Opp T <+ OppNotation T.
 
-(* Integers are obtained by postulating that every number has a predecessor *)
+(** We obtain integers by postulating that every number has a predecessor. *)
 
-Axiom succ_pred : forall n, S (P n) == n.
+Module Type IsOpp (Import Z : NZAxiomsSig')(Import O : Opp' Z).
+ Declare Instance opp_wd : Proper (eq==>eq) opp.
+ Axiom succ_pred : forall n, S (P n) == n.
+ Axiom opp_0 : - 0 == 0.
+ Axiom opp_succ : forall n, - (S n) == P (- n).
+End IsOpp.
 
-Axiom opp_0 : - 0 == 0.
-Axiom opp_succ : forall n, - (S n) == P (- n).
-
-End ZAxiomsSig.
+Module Type ZAxiomsSig := NZOrdAxiomsSig <+ Opp <+ IsOpp.
+Module Type ZAxiomsSig' := NZOrdAxiomsSig' <+ Opp' <+ IsOpp.
 
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 64a122c714..9b5a80762f 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -14,9 +14,8 @@ Require Export Decidable.
 Require Export ZAxioms.
 Require Import NZProperties.
 
-Module ZBasePropFunct (Import Z : ZAxiomsSig).
+Module ZBasePropFunct (Import Z : ZAxiomsSig').
 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 9140556546..ba79ae24b7 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -23,17 +23,18 @@
 
 Require Import ZAxioms ZProperties NZDiv.
 
-Open Scope NumScope.
-
-Module Type ZDiv (Import Z : ZAxiomsSig).
- Include Type NZDivCommon Z. (** div, mod, compat with eq, equation a=bq+r *)
+Module Type ZDivSpecific (Import Z : ZAxiomsSig')(Import DM : DivMod' Z).
  Definition abs z := max z (-z).
  Axiom mod_always_pos : forall a b, 0 <= a mod b < abs b.
-End ZDiv.
+End ZDivSpecific.
+
+Module Type ZDiv (Z:ZAxiomsSig)
+ := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z.
 
 Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
+Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation.
 
-Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z).
+Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
@@ -159,7 +160,7 @@ Qed.
 Parameter sign : t -> t.
 Parameter sign_pos : forall t, sign t == 1 <-> 0<t.
 Parameter sign_0 : forall t, sign t == 0 <-> t==0.
-Parameter sign_neg : forall t, sign t == -1 <-> t<0.
+Parameter sign_neg : forall t, sign t == -(1) <-> t<0.
 Parameter sign_abs : forall t, t * sign t == abs t.
 (** END TODO *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index 611432a6de..99df15f230 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -26,17 +26,18 @@
 
 Require Import ZAxioms ZProperties NZDiv.
 
-Open Scope NumScope.
-
-Module Type ZDiv (Import Z : ZAxiomsSig).
- Include Type NZDivCommon Z. (** div, mod, compat with eq, equation a=bq+r *)
+Module Type ZDivSpecific (Import Z:ZAxiomsSig')(Import DM : DivMod' Z).
  Axiom mod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b.
  Axiom mod_neg_bound : forall a b, b < 0 -> b < a mod b <= 0.
-End ZDiv.
+End ZDivSpecific.
+
+Module Type ZDiv (Z:ZAxiomsSig)
+ := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z.
 
 Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
+Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation.
 
-Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z).
+Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index c60bf7c6aa..0468b3bf58 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -26,18 +26,19 @@
 
 Require Import ZAxioms ZProperties NZDiv.
 
-Open Scope NumScope.
-
-Module Type ZDiv (Import Z : ZAxiomsSig).
- Include Type NZDivCommon Z. (** div, mod, compat with eq, equation a=bq+r *)
+Module Type ZDivSpecific (Import Z:ZAxiomsSig')(Import DM : DivMod' Z).
  Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
  Axiom mod_opp_l : forall a b, b ~= 0 -> (-a) mod b == - (a mod b).
  Axiom mod_opp_r : forall a b, b ~= 0 -> a mod (-b) == a mod b.
-End ZDiv.
+End ZDivSpecific.
+
+Module Type ZDiv (Z:ZAxiomsSig)
+ := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z.
 
 Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
+Module Type ZDivSig' := ZAxiomsSig' <+ ZDiv <+ DivModNotation.
 
-Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z).
+Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index e77f9c453c..849bf6b407 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -12,9 +12,8 @@
 
 Require Export ZMul.
 
-Module ZOrderPropFunct (Import Z : ZAxiomsSig).
+Module ZOrderPropFunct (Import Z : ZAxiomsSig').
 Include ZMulPropFunct Z.
-Local Open Scope NumScope.
 
 (** Instances of earlier theorems for m == 0 *)
 
@@ -124,10 +123,10 @@ Proof.
 intro; apply lt_neq; apply lt_pred_l.
 Qed.
 
-Theorem lt_n1_r : forall n m, n < m -> m < 0 -> n < -1.
+Theorem lt_n1_r : forall n m, n < m -> m < 0 -> n < -(1).
 Proof.
 intros n m H1 H2. apply -> lt_le_pred in H2.
-setoid_replace (P 0) with (-1) in H2. now apply lt_le_trans with m.
+setoid_replace (P 0) with (-(1)) in H2. now apply lt_le_trans with m.
 apply <- eq_opp_r. now rewrite opp_pred, opp_0.
 Qed.
 
diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v
index 4be2ac887b..84d840ad20 100644
--- a/theories/Numbers/Integer/Abstract/ZMul.v
+++ b/theories/Numbers/Integer/Abstract/ZMul.v
@@ -12,9 +12,8 @@
 
 Require Export ZAdd.
 
-Module ZMulPropFunct (Import Z : ZAxiomsSig).
+Module ZMulPropFunct (Import Z : ZAxiomsSig').
 Include ZAddPropFunct Z.
-Local Open Scope NumScope.
 
 (** A note on naming: right (correspondingly, left) distributivity
     happens when the sum is multiplied by a number on the right
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index bd9a857145..99be58ebd8 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -12,9 +12,10 @@
 
 Require Export ZAddOrder.
 
-Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig).
+Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig').
 Include ZAddOrderPropFunct Z.
-Local Open Scope NumScope.
+
+Local Notation "- 1" := (-(1)).
 
 Theorem mul_lt_mono_nonpos :
   forall n m p q, m <= 0 -> n < m -> q <= 0 -> p < q ->  m * q < n * p.