blob: dffa7953223d2365a57f5c1aef9b3becb8a2160f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
|
Require Import ZArith.
Require Import ZAux.
Set Implicit Arguments.
Open Scope Z_scope.
Lemma rel_prime_mod: forall a b, 1 < b ->
rel_prime a b -> a mod b <> 0.
Proof.
intros a b H H1 H2.
case (not_rel_prime_0 _ H).
rewrite <- H2.
apply rel_prime_mod; auto with zarith.
Qed.
Lemma Zmodpl: forall a b n, 0 < n ->
(a mod n + b) mod n = (a + b) mod n.
Proof.
intros a b n H.
rewrite Zmod_plus; auto.
rewrite Zmod_mod; auto.
apply sym_equal; apply Zmod_plus; auto.
Qed.
Lemma Zmodpr: forall a b n, 0 < n ->
(b + a mod n) mod n = (b + a) mod n.
Proof.
intros a b n H; repeat rewrite (Zplus_comm b).
apply Zmodpl; auto.
Qed.
Lemma Zmodml: forall a b n, 0 < n ->
(a mod n * b) mod n = (a * b) mod n.
Proof.
intros a b n H.
rewrite Zmod_mult; auto.
rewrite Zmod_mod; auto.
apply sym_equal; apply Zmod_mult; auto.
Qed.
Lemma Zmodmr: forall a b n, 0 < n ->
(b * (a mod n)) mod n = (b * a) mod n.
Proof.
intros a b n H; repeat rewrite (Zmult_comm b).
apply Zmodml; auto.
Qed.
Ltac is_ok t :=
match t with
| (?x mod _ + ?y mod _) mod _ => constr:false
| (?x mod _ * (?y mod _)) mod _ => constr:false
| ?x mod _ => x
end.
Ltac rmod t :=
match t with
(?x + ?y) mod _ =>
match (is_ok x) with
| false => rmod x
| ?x1 => match (is_ok y) with
|false => rmod y
| ?y1 =>
rewrite <- (Zmod_plus x1 y1)
|false => rmod y
end
end
| (?x * ?y) mod _ =>
match (is_ok x) with
| false => rmod x
| ?x1 => match (is_ok y) with
|false => rmod y
| ?y1 => rewrite <- (Zmod_mult x1 y1)
end
| false => rmod x
end
end.
Lemma Zmod_div_mod: forall n m a, 0 < n -> 0 < m ->
(n | m) -> a mod n = (a mod m) mod n.
Proof.
intros n m a H1 H2 H3.
pattern a at 1; rewrite (Z_div_mod_eq a m); auto with zarith.
case H3; intros q Hq; pattern m at 1; rewrite Hq.
rewrite (Zmult_comm q).
rewrite Zmod_plus; auto.
rewrite <- Zmult_assoc; rewrite Zmod_mult; auto.
rewrite Z_mod_same; try rewrite Zmult_0_l; auto with zarith.
rewrite (Zmod_def_small 0); auto with zarith.
rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith.
Qed.
|
