diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:05 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-05 15:12:05 +0000 |
commit | 81d7335ba1a07a7a30e206ae3ffc4412f3a54f46 (patch) | |
tree | 21dbdd2c920d95fd7607d19eaa8fa1a348e41208 /theories/ZArith/Zdiv.v | |
parent | 0bdae59ed5a1800ccaadb9a989f1e67f4ef61e50 (diff) |
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
Diffstat (limited to 'theories/ZArith/Zdiv.v')
-rw-r--r-- | theories/ZArith/Zdiv.v | 47 |
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. |