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

12 files changed, 97 insertions, 90 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index 26ba0a8d4..5663408d1 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 282709c47..de12993f8 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 4b3d18be4..9158a214d 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 64a122c71..9b5a80762 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 914055654..ba79ae24b 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 611432a6d..99df15f23 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 c60bf7c6a..0468b3bf5 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 e77f9c453..849bf6b40 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 4be2ac887..84d840ad2 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 bd9a85714..99be58ebd 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.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 0956f337f..8b5624cdf 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -21,7 +21,18 @@ Open Local Scope pair_scope.
 Module ZPairsAxiomsMod (Import N : NAxiomsSig) <: ZAxiomsSig.
 Module Import NPropMod := NPropFunct N. (* Get all properties of N *)
 
-Local Open Scope NumScope.
+Delimit Scope NScope with N.
+Bind Scope NScope with N.t.
+Infix "=="  := N.eq (at level 70) : NScope.
+Notation "x ~= y" := (~ N.eq x y) (at level 70) : NScope.
+Notation "0" := N.zero : NScope.
+Notation "1" := (N.succ N.zero) : NScope.
+Infix "+" := N.add : NScope.
+Infix "-" := N.sub : NScope.
+Infix "*" := N.mul : NScope.
+Infix "<" := N.lt : NScope.
+Infix "<=" := N.le : NScope.
+Local Open Scope NScope.
 
 (** The definitions of functions ([add], [mul], etc.) will be unfolded
     by the properties functor. Since we don't want [add_comm] to refer
@@ -34,8 +45,8 @@ Module Z.
 Definition t := (N.t * N.t)%type.
 Definition zero : t := (0, 0).
 Definition eq (p q : t) := (p#1 + q#2 == q#1 + p#2).
-Definition succ (n : t) : t := (S n#1, n#2).
-Definition pred (n : t) : t := (n#1, S n#2).
+Definition succ (n : t) : t := (N.succ n#1, n#2).
+Definition pred (n : t) : t := (n#1, N.succ n#2).
 Definition opp (n : t) : t := (n#2, n#1).
 Definition add (n m : t) : t := (n#1 + m#1, n#2 + m#2).
 Definition sub (n m : t) : t := (n#1 + m#2, n#2 + m#1).
@@ -58,20 +69,19 @@ Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2).
 
 End Z.
 
-Delimit Scope IntScope with Int.
-Bind Scope IntScope with Z.t.
-Notation "x == y"  := (Z.eq x y) (at level 70) : IntScope.
-Notation "x ~= y" := (~ Z.eq x y) (at level 70) : IntScope.
-Notation "0" := Z.zero : IntScope.
-Notation "1" := (Z.succ Z.zero) : IntScope.
-Notation "x + y" := (Z.add x y) : IntScope.
-Notation "x - y" := (Z.sub x y) : IntScope.
-Notation "x * y" := (Z.mul x y) : IntScope.
-Notation "- x" := (Z.opp x) : IntScope.
-Notation "x < y" := (Z.lt x y) : IntScope.
-Notation "x <= y" := (Z.le x y) : IntScope.
-Notation "x > y" := (Z.lt y x) (only parsing) : IntScope.
-Notation "x >= y" := (Z.le y x) (only parsing) : IntScope.
+Delimit Scope ZScope with Z.
+Bind Scope ZScope with Z.t.
+Infix "=="  := Z.eq (at level 70) : ZScope.
+Notation "x ~= y" := (~ Z.eq x y) (at level 70) : ZScope.
+Notation "0" := Z.zero : ZScope.
+Notation "1" := (Z.succ Z.zero) : ZScope.
+Infix "+" := Z.add : ZScope.
+Infix "-" := Z.sub : ZScope.
+Infix "*" := Z.mul : ZScope.
+Notation "- x" := (Z.opp x) : ZScope.
+Infix "<" := Z.lt : ZScope.
+Infix "<=" := Z.le : ZScope.
+Local Open Scope ZScope.
 
 Lemma sub_add_opp : forall n m, Z.sub n m = Z.add n (Z.opp m).
 Proof. reflexivity. Qed.
@@ -82,7 +92,7 @@ split.
 unfold Reflexive, Z.eq. reflexivity.
 unfold Symmetric, Z.eq; now symmetry.
 unfold Transitive, Z.eq. intros (n1,n2) (m1,m2) (p1,p2) H1 H2; simpl in *.
-apply (add_cancel_r _ _ (m1+m2)).
+apply (add_cancel_r _ _ (m1+m2)%N).
 rewrite add_shuffle2, H1, add_shuffle1, H2.
 now rewrite add_shuffle1, (add_comm m1).
 Qed.
@@ -122,10 +132,10 @@ intros n1 m1 H1 n2 m2 H2. rewrite 2 sub_add_opp.
 apply add_wd, opp_wd; auto.
 Qed.
 
-Lemma mul_comm : forall n m, (n*m == m*n)%Int.
+Lemma mul_comm : forall n m, n*m == m*n.
 Proof.
 intros (n1,n2) (m1,m2); compute.
-rewrite (add_comm (m1*n2)).
+rewrite (add_comm (m1*n2)%N).
 apply N.add_wd; apply N.add_wd; apply mul_comm.
 Qed.
 
@@ -133,7 +143,7 @@ Instance mul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul.
 Proof.
 assert (forall n, Proper (Z.eq ==> Z.eq) (Z.mul n)).
  unfold Z.mul, Z.eq. intros (n1,n2) (p1,p2) (q1,q2) H; simpl in *.
- rewrite add_shuffle1, (add_comm (n1*p1)).
+ rewrite add_shuffle1, (add_comm (n1*p1)%N).
  symmetry. rewrite add_shuffle1.
  rewrite <- ! mul_add_distr_l.
  rewrite (add_comm p2), (add_comm q2), H.
@@ -152,26 +162,24 @@ Theorem bi_induction :
 Proof.
 intros A0 AS n; unfold Z.zero, Z.succ, Z.eq in *.
 destruct n as [n m].
-cut (forall p, A (p, 0)); [intro H1 |].
-cut (forall p, A (0, p)); [intro H2 |].
+cut (forall p, A (p, 0%N)); [intro H1 |].
+cut (forall p, A (0%N, p)); [intro H2 |].
 destruct (add_dichotomy n m) as [[p H] | [p H]].
-rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm).
+rewrite (A_wd (n, m) (0%N, p)) by (rewrite add_0_l; now rewrite add_comm).
 apply H2.
-rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1.
+rewrite (A_wd (n, m) (p, 0%N)) by now rewrite add_0_r. apply H1.
 induct p. assumption. intros p IH.
-apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite add_0_l, add_1_l].
+apply -> (A_wd (0%N, p) (1%N, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l].
 now apply <- AS.
 induct p. assumption. intros p IH.
-replace 0 with (snd (p, 0)); [| reflexivity].
-replace (S p) with (S (fst (p, 0))); [| reflexivity]. now apply -> AS.
+replace 0%N with (snd (p, 0%N)); [| reflexivity].
+replace (N.succ p) with (N.succ (fst (p, 0%N))); [| reflexivity]. now apply -> AS.
 Qed.
 
 End Induction.
 
 (* Time to prove theorems in the language of Z *)
 
-Open Scope IntScope.
-
 Theorem pred_succ : forall n, Z.pred (Z.succ n) == n.
 Proof.
 unfold Z.pred, Z.succ, Z.eq; intro n; simpl; now nzsimpl.
@@ -221,7 +229,7 @@ Theorem mul_succ_l : forall n m, (Z.succ n) * m == n * m + m.
 Proof.
 intros (n1,n2) (m1,m2); unfold Z.mul, Z.succ, Z.eq; simpl; nzsimpl.
 rewrite <- (add_assoc _ m1), (add_comm m1), (add_assoc _ _ m1).
-now rewrite <- (add_assoc _ m2), (add_comm m2), (add_assoc _ (n2*m1)%Num m2).
+now rewrite <- (add_assoc _ m2), (add_comm m2), (add_assoc _ (n2*m1)%N m2).
 Qed.
 
 (** Order *)
@@ -279,7 +287,7 @@ Proof.
 assert (forall n, Proper (Z.eq==>iff) (Z.lt n)).
  intros (n1,n2). apply proper_sym_impl_iff; auto with *.
  unfold Z.lt, Z.eq; intros (r1,r2) (s1,s2) Eq H; simpl in *.
- apply le_lt_add_lt with (r1+r2)%Num (r1+r2)%Num; [apply le_refl; auto with *|].
+ apply le_lt_add_lt with (r1+r2)%N (r1+r2)%N; [apply le_refl; auto with *|].
  rewrite add_shuffle2, (add_comm s2), Eq.
  rewrite (add_comm s1 n2), (add_shuffle1 n2), (add_comm n2 r1).
  now rewrite <- add_lt_mono_r.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index f752c1976..666ce5454 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -16,18 +16,15 @@ Require Import ZSig.
 
 Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig.
 
-Delimit Scope NumScope with Num.
-Bind Scope NumScope with Z.t.
-Local Open Scope NumScope.
-Local Notation "[ x ]" := (Z.to_Z x) : NumScope.
-Local Infix "=="  := Z.eq (at level 70) : NumScope.
-Local Notation "0" := Z.zero : NumScope.
-Local Infix "+" := Z.add : NumScope.
-Local Infix "-" := Z.sub : NumScope.
-Local Infix "*" := Z.mul : NumScope.
-Local Notation "- x" := (Z.opp x) : NumScope.
-Local Infix "<=" := Z.le : NumScope.
-Local Infix "<" := Z.lt : NumScope.
+Local Notation "[ x ]" := (Z.to_Z x).
+Local Infix "=="  := Z.eq (at level 70).
+Local Notation "0" := Z.zero.
+Local Infix "+" := Z.add.
+Local Infix "-" := Z.sub.
+Local Infix "*" := Z.mul.
+Local Notation "- x" := (Z.opp x).
+Local Infix "<=" := Z.le.
+Local Infix "<" := Z.lt.
 
 Hint Rewrite
  Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ