Zdiv: results about eqm (the equality modulo some N) under a section

 These results are quite anecdotic, and may have bad interaction
 with the rest of the typeclass infrastructure.

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

1 files changed, 24 insertions, 23 deletions

diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 563f8080d..be29c8cb5 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -441,49 +441,48 @@ Qed.
 (** For a specific number N, equality modulo N is hence a nice setoid
    equivalence, compatible with [+], [-] and [*]. *)
 
-Definition eqm N a b := (a mod N = b mod N).
+Section EqualityModulo.
+Variable N:Z.
 
-Lemma eqm_refl N : forall a, (eqm N) a a.
+Definition eqm a b := (a mod N = b mod N).
+Infix "==" := eqm (at level 70).
+
+Lemma eqm_refl : forall a, a == a.
 Proof. unfold eqm; auto. Qed.
 
-Lemma eqm_sym N : forall a b, (eqm N) a b -> (eqm N) b a.
+Lemma eqm_sym : forall a b, a == b -> b == a.
 Proof. unfold eqm; auto. Qed.
 
-Lemma eqm_trans N : forall a b c,
-  (eqm N) a b -> (eqm N) b c -> (eqm N) a c.
+Lemma eqm_trans : forall a b c,
+  a == b -> b == c -> a == c.
 Proof. unfold eqm; eauto with *. Qed.
 
-Add Parametric Relation N : Z (eqm N)
-  reflexivity proved by (eqm_refl N)
-  symmetry proved by (eqm_sym N)
-  transitivity proved by (eqm_trans N) as eqm_setoid.
+Instance eqm_setoid : Equivalence eqm.
+Proof.
+ constructor; [exact eqm_refl | exact eqm_sym | exact eqm_trans].
+Qed.
 
-Add Parametric Morphism N : Zplus
-  with signature (eqm N) ==> (eqm N) ==> (eqm N) as Zplus_eqm.
+Instance Zplus_eqm : Proper (eqm ==> eqm ==> eqm) Zplus.
 Proof.
-  unfold eqm; intros; rewrite Zplus_mod, H, H0, <- Zplus_mod; auto.
+  unfold eqm; repeat red; intros. rewrite Zplus_mod, H, H0, <- Zplus_mod; auto.
 Qed.
 
-Add Parametric Morphism N : Zminus
-  with signature (eqm N) ==> (eqm N) ==> (eqm N) as Zminus_eqm.
+Instance Zminus_eqm : Proper (eqm ==> eqm ==> eqm) Zminus.
 Proof.
-  unfold eqm; intros; rewrite Zminus_mod, H, H0, <- Zminus_mod; auto.
+  unfold eqm; repeat red; intros. rewrite Zminus_mod, H, H0, <- Zminus_mod; auto.
 Qed.
 
-Add Parametric Morphism N : Zmult
-  with signature (eqm N) ==> (eqm N) ==> (eqm N) as Zmult_eqm.
+Instance Zmult_eqm : Proper (eqm ==> eqm ==> eqm) Zmult.
 Proof.
-  unfold eqm; intros; rewrite Zmult_mod, H, H0, <- Zmult_mod; auto.
+  unfold eqm; repeat red; intros. rewrite Zmult_mod, H, H0, <- Zmult_mod; auto.
 Qed.
 
-Add Parametric Morphism N : Zopp
-  with signature (eqm N) ==> (eqm N) as Zopp_eqm.
+Instance Zopp_eqm : Proper (eqm ==> eqm) Zopp.
 Proof.
-  intros; change ((eqm N) (-x) (-y)) with ((eqm N) (0-x) (0-y)).
-  rewrite H; red; auto.
+  intros x y H. change ((-x)==(-y)) with ((0-x)==(0-y)). now rewrite H.
 Qed.
 
-Lemma Zmod_eqm N : forall a, (eqm N) (a mod N) a.
+Lemma Zmod_eqm : forall a, (a mod N) == a.
 Proof.
   intros; exact (Zmod_mod a N).
 Qed.
@@ -496,6 +495,8 @@ Qed.
     ~ (1/3 == 1/1)
 *)
 
+End EqualityModulo.
+
 Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c).
 Proof.
  intros. zero_or_not b. rewrite Zmult_comm. zero_or_not c.