diff options
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/Zdiv.v | 89 | ||||
| -rw-r--r-- | theories/ZArith/auxiliary.v | 42 |
2 files changed, 44 insertions, 87 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 4c560c6b..228a882a 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zdiv.v 10999 2008-05-27 15:55:22Z letouzey $ i*) +(*i $Id: Zdiv.v 11477 2008-10-20 15:16:14Z letouzey $ i*) (* Contribution by Claude Marché and Xavier Urbain *) @@ -901,66 +901,63 @@ Proof. intros; rewrite Zmult_mod, Zmod_mod, <- Zmult_mod; auto. Qed. -(** For a specific number n, equality modulo n is hence a nice setoid - equivalence, compatible with the usual operations. Due to restrictions - with Coq setoids, we cannot state this in a section, but it works - at least with a module. *) +(** For a specific number N, equality modulo N is hence a nice setoid + equivalence, compatible with [+], [-] and [*]. *) -Module Type SomeNumber. - Parameter n:Z. -End SomeNumber. +Definition eqm N a b := (a mod N = b mod N). -Module EqualityModulo (M:SomeNumber). +Lemma eqm_refl N : forall a, (eqm N) a a. +Proof. unfold eqm; auto. Qed. - Definition eqm a b := (a mod M.n = b mod M.n). - Infix "==" := eqm (at level 70). +Lemma eqm_sym N : forall a b, (eqm N) a b -> (eqm N) b a. +Proof. unfold eqm; auto. Qed. - Lemma eqm_refl : forall a, a == 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. +Proof. unfold eqm; eauto with *. Qed. - Lemma eqm_sym : forall a b, a == b -> b == a. - Proof. unfold eqm; auto. 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. - Lemma eqm_trans : forall a b c, a == b -> b == c -> a == c. - Proof. unfold eqm; eauto with *. Qed. - - Add Relation Z eqm - reflexivity proved by eqm_refl - symmetry proved by eqm_sym - transitivity proved by eqm_trans as eqm_setoid. - - Add Morphism Zplus : Zplus_eqm. - Proof. +Add Parametric Morphism N : Zplus + with signature (eqm N) ==> (eqm N) ==> (eqm N) as Zplus_eqm. +Proof. unfold eqm; intros; rewrite Zplus_mod, H, H0, <- Zplus_mod; auto. - Qed. +Qed. - Add Morphism Zminus : Zminus_eqm. - Proof. +Add Parametric Morphism N : Zminus + with signature (eqm N) ==> (eqm N) ==> (eqm N) as Zminus_eqm. +Proof. unfold eqm; intros; rewrite Zminus_mod, H, H0, <- Zminus_mod; auto. - Qed. +Qed. - Add Morphism Zmult : Zmult_eqm. - Proof. +Add Parametric Morphism N : Zmult + with signature (eqm N) ==> (eqm N) ==> (eqm N) as Zmult_eqm. +Proof. unfold eqm; intros; rewrite Zmult_mod, H, H0, <- Zmult_mod; auto. - Qed. +Qed. - Add Morphism Zopp : Zopp_eqm. - Proof. - intros; change (-x == -y) with (0-x == 0-y). +Add Parametric Morphism N : Zopp + with signature (eqm N) ==> (eqm N) as Zopp_eqm. +Proof. + intros; change ((eqm N) (-x) (-y)) with ((eqm N) (0-x) (0-y)). rewrite H; red; auto. - Qed. - - Lemma Zmod_eqm : forall a, a mod M.n == a. - Proof. - unfold eqm; intros; apply Zmod_mod. - Qed. +Qed. - (* Zmod and Zdiv are not full morphisms with respect to eqm. - For instance, take n=2. Then 3 == 1 but we don't have - 1 mod 3 == 1 mod 1 nor 1/3 == 1/1. - *) +Lemma Zmod_eqm N : forall a, (eqm N) (a mod N) a. +Proof. + intros; exact (Zmod_mod a N). +Qed. -End EqualityModulo. +(* NB: Zmod and Zdiv are not morphisms with respect to eqm. + For instance, let (==) be (eqm 2). Then we have (3 == 1) but: + ~ (3 mod 3 == 1 mod 3) + ~ (1 mod 3 == 1 mod 1) + ~ (3/3 == 1/3) + ~ (1/3 == 1/1) +*) Lemma Zdiv_Zdiv : forall a b c, 0<=b -> 0<=c -> (a/b)/c = a/(b*c). Proof. diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index 726fb45a..ffc3e70f 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: auxiliary.v 9302 2006-10-27 21:21:17Z barras $ i*) +(*i $Id: auxiliary.v 11739 2009-01-02 19:33:19Z herbelin $ i*) (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) @@ -91,46 +91,6 @@ Proof. rewrite Zplus_opp_r; trivial. Qed. -(**********************************************************************) -(** * Factorization lemmas *) - -Theorem Zred_factor0 : forall n:Z, n = n * 1. - intro x; rewrite (Zmult_1_r x); reflexivity. -Qed. - -Theorem Zred_factor1 : forall n:Z, n + n = n * 2. -Proof. - exact Zplus_diag_eq_mult_2. -Qed. - -Theorem Zred_factor2 : forall n m:Z, n + n * m = n * (1 + m). -Proof. - intros x y; pattern x at 1 in |- *; rewrite <- (Zmult_1_r x); - rewrite <- Zmult_plus_distr_r; trivial with arith. -Qed. - -Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m). -Proof. - intros x y; pattern x at 2 in |- *; rewrite <- (Zmult_1_r x); - rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm; - trivial with arith. -Qed. - -Theorem Zred_factor4 : forall n m p:Z, n * m + n * p = n * (m + p). -Proof. - intros x y z; symmetry in |- *; apply Zmult_plus_distr_r. -Qed. - -Theorem Zred_factor5 : forall n m:Z, n * 0 + m = m. -Proof. - intros x y; rewrite <- Zmult_0_r_reverse; auto with arith. -Qed. - -Theorem Zred_factor6 : forall n:Z, n = n + 0. -Proof. - intro; rewrite Zplus_0_r; trivial with arith. -Qed. - Theorem Zle_mult_approx : forall n m p:Z, n > 0 -> p > 0 -> 0 <= m -> 0 <= m * n + p. Proof. |