Division: avoid imposing rem as an infix keyword in Z_scope and bigZ_scope.

 No infix notation "rem" for Zrem (that will probably become Z.rem in
 a close future). This way, we avoid conflict with people already using
 rem for their own need. Same for BigZ. We still use infix rem, but
 only in the abstract layer of Numbers, in a way that doesn't inpact
 the rest of Coq. Btw, the axiomatized function is now named rem
 instead of remainder.

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

7 files changed, 18 insertions, 20 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 89fa8e170..f177755fa 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -88,19 +88,19 @@ Module Type ZDiv' (Z:ZAxiomsMiniSig) := NZDiv.NZDiv' Z <+ ZDivSpecific Z.
 *)
 
 Module Type QuotRem (Import A : Typ).
- Parameters Inline quot remainder : t -> t -> t.
+ Parameters Inline quot rem : t -> t -> t.
 End QuotRem.
 
 Module Type QuotRemNotation (A : Typ)(Import B : QuotRem A).
  Infix "÷" := quot (at level 40, left associativity).
- Infix "rem" := remainder (at level 40, no associativity).
+ Infix "rem" := rem (at level 40, no associativity).
 End QuotRemNotation.
 
 Module Type QuotRem' (A : Typ) := QuotRem A <+ QuotRemNotation A.
 
 Module Type QuotRemSpec (Import A : ZAxiomsMiniSig')(Import B : QuotRem' A).
  Declare Instance quot_wd : Proper (eq==>eq==>eq) quot.
- Declare Instance rem_wd : Proper (eq==>eq==>eq) remainder.
+ Declare Instance rem_wd : Proper (eq==>eq==>eq) B.rem.
  Axiom quot_rem : forall a b, b ~= 0 -> a == b*(a÷b) + (a rem b).
  Axiom rem_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= a rem b < b.
  Axiom rem_opp_l : forall a b, b ~= 0 -> (-a) rem b == - (a rem b).
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 37a0057ed..e33265762 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -35,7 +35,7 @@ Module Type ZQuotProp
 
  Module Quot2Div <: NZDiv A.
   Definition div := quot.
-  Definition modulo := remainder.
+  Definition modulo := A.rem.
   Definition div_wd := quot_wd.
   Definition mod_wd := rem_wd.
   Definition div_mod := quot_rem.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 72137eccf..6153ccc75 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -65,7 +65,7 @@ Arguments Scope BigZ.sqrt [bigZ_scope].
 Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.quot [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.remainder [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.rem [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.even [bigZ_scope].
 Arguments Scope BigZ.odd [bigZ_scope].
@@ -92,7 +92,6 @@ Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope.
 Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : bigZ_scope.
 Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
 Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope.
-Infix "rem" := BigZ.remainder (at level 40, no associativity) : bigZ_scope.
 Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope.
 
 Local Open Scope bigZ_scope.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index f4baf32bc..4c4eb6c10 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -461,7 +461,7 @@ Module Make (N:NType) <: ZType.
   | Neg nx, Neg ny => Pos (N.div nx ny)
   end.
 
- Definition remainder x y :=
+ Definition rem x y :=
   if eq_bool y zero then x
   else
     match x, y with
@@ -478,10 +478,10 @@ Module Make (N:NType) <: ZType.
    rewrite Zquot_Zdiv_pos; trivial using N.spec_pos.
  Qed.
 
- Lemma spec_remainder : forall x y,
-   to_Z (remainder x y) = (to_Z x) rem (to_Z y).
+ Lemma spec_rem : forall x y,
+   to_Z (rem x y) = Zrem (to_Z x) (to_Z y).
  Proof.
-  intros x y. unfold remainder. rewrite spec_eq_bool, spec_0.
+  intros x y. unfold rem. rewrite spec_eq_bool, spec_0.
   assert (Hy := Zeq_bool_if (to_Z y) 0). destruct Zeq_bool.
   now rewrite Hy, Zrem_0_r.
   destruct x as [x|x], y as [y|y]; simpl in *; symmetry;
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index f68aa0dbe..5f38d57b8 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -189,7 +189,7 @@ Definition rem_bound_pos := Zrem_bound.
 Definition rem_opp_l := fun a b (_:b<>0) => Zrem_opp_l a b.
 Definition rem_opp_r := fun a b (_:b<>0) => Zrem_opp_r a b.
 Definition quot := Zquot.
-Definition remainder := Zrem.
+Definition rem := Zrem.
 
 (** We define [eq] only here to avoid refering to this [eq] above. *)
 
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index c2a173e22..1c06b0b8e 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -56,7 +56,7 @@ Module Type ZType.
  Parameter div : t -> t -> t.
  Parameter modulo : t -> t -> t.
  Parameter quot : t -> t -> t.
- Parameter remainder : t -> t -> t.
+ Parameter rem : t -> t -> t.
  Parameter gcd : t -> t -> t.
  Parameter sgn : t -> t.
  Parameter abs : t -> t.
@@ -88,7 +88,7 @@ Module Type ZType.
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
  Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
  Parameter spec_quot: forall x y, [quot x y] = [x] ÷ [y].
- Parameter spec_remainder: forall x y, [remainder x y] = [x] rem [y].
+ Parameter spec_rem: forall x y, [rem x y] = Zrem [x] [y].
  Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
  Parameter spec_sgn : forall x, [sgn x] = Zsgn [x].
  Parameter spec_abs : forall x, [abs x] = Zabs [x].
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 6a823a732..62b79fc3a 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -16,8 +16,7 @@ Hint Rewrite
  spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
  spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
- spec_pow spec_log2 spec_even spec_odd spec_gcd spec_quot
- spec_remainder
+ spec_pow spec_log2 spec_even spec_odd spec_gcd spec_quot spec_rem
  : zsimpl.
 
 Ltac zsimpl := autorewrite with zsimpl.
@@ -353,25 +352,25 @@ Definition mod_bound_pos :
 (** Quot / Rem *)
 
 Program Instance quot_wd : Proper (eq==>eq==>eq) quot.
-Program Instance rem_wd : Proper (eq==>eq==>eq) remainder.
+Program Instance rem_wd : Proper (eq==>eq==>eq) rem.
 
-Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + (remainder a b).
+Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + rem a b.
 Proof.
 intros a b _. zify. apply Z_quot_rem_eq.
 Qed.
 
 Theorem rem_bound_pos :
- forall a b, 0<=a -> 0<b -> 0 <= remainder a b /\ remainder a b < b.
+ forall a b, 0<=a -> 0<b -> 0 <= rem a b /\ rem a b < b.
 Proof.
 intros a b. zify. intros. now apply Zrem_bound.
 Qed.
 
-Theorem rem_opp_l : forall a b, ~b==0 -> remainder (-a) b == -(remainder a b).
+Theorem rem_opp_l : forall a b, ~b==0 -> rem (-a) b == -(rem a b).
 Proof.
 intros a b _. zify. apply Zrem_opp_l.
 Qed.
 
-Theorem rem_opp_r : forall a b, ~b==0 -> remainder a (-b) == remainder a b.
+Theorem rem_opp_r : forall a b, ~b==0 -> rem a (-b) == rem a b.
 Proof.
 intros a b _. zify. apply Zrem_opp_r.
 Qed.