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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
|
(*************************************************************)
(* This file is distributed under the terms of the *)
(* GNU Lesser General Public License Version 2.1 *)
(*************************************************************)
(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *)
(*************************************************************)
(**********************************************************************
ZCAux.v
Auxillary functions & Theorems
**********************************************************************)
Require Import Coq.setoid_ring.ArithRing.
Require Export Coq.ZArith.ZArith Coq.ZArith.Zpow_facts.
Require Export Coq.ZArith.Znumtheory.
Require Export Coqprime.Tactic.
Theorem Zdivide_div_prime_le_square: forall x, 1 < x -> ~prime x -> exists p, prime p /\ (p | x) /\ p * p <= x.
intros x Hx; generalize Hx; pattern x; apply Z_lt_induction; auto with zarith.
clear x Hx; intros x Rec H H1.
case (not_prime_divide x); auto.
intros x1 ((H2, H3), H4); case (prime_dec x1); intros H5.
case (Zle_or_lt (x1 * x1) x); intros H6.
exists x1; auto.
case H4; clear H4; intros x2 H4; subst.
assert (Hx2: x2 <= x1).
case (Zle_or_lt x2 x1); auto; intros H8; contradict H6; apply Zle_not_lt.
apply Zmult_le_compat_r; auto with zarith.
case (prime_dec x2); intros H7.
exists x2; repeat (split; auto with zarith).
apply Zmult_le_compat_l; auto with zarith.
apply Zle_trans with 2%Z; try apply prime_ge_2; auto with zarith.
case (Zle_or_lt 0 x2); intros H8.
case Zle_lt_or_eq with (1 := H8); auto with zarith; clear H8; intros H8; subst; auto with zarith.
case (Zle_lt_or_eq 1 x2); auto with zarith; clear H8; intros H8; subst; auto with zarith.
case (Rec x2); try split; auto with zarith.
intros x3 (H9, (H10, H11)).
exists x3; repeat (split; auto with zarith).
contradict H; apply Zle_not_lt; auto with zarith.
apply Zle_trans with (0 * x1); auto with zarith.
case (Rec x1); try split; auto with zarith.
intros x3 (H9, (H10, H11)).
exists x3; repeat (split; auto with zarith).
apply Zdivide_trans with x1; auto with zarith.
Qed.
Theorem Zmult_interval: forall p q, 0 < p * q -> 1 < p -> 0 < q < p * q.
intros p q H1 H2; assert (0 < q).
case (Zle_or_lt q 0); auto; intros H3; contradict H1; apply Zle_not_lt.
rewrite <- (Zmult_0_r p).
apply Zmult_le_compat_l; auto with zarith.
split; auto.
pattern q at 1; rewrite <- (Zmult_1_l q).
apply Zmult_lt_compat_r; auto with zarith.
Qed.
Theorem prime_induction: forall (P: Z -> Prop), P 0 -> P 1 -> (forall p q, prime p -> P q -> P (p * q)) -> forall p, 0 <= p -> P p.
intros P H H1 H2 p Hp.
generalize Hp; pattern p; apply Z_lt_induction; auto; clear p Hp.
intros p Rec Hp.
case Zle_lt_or_eq with (1 := Hp); clear Hp; intros Hp; subst; auto.
case (Zle_lt_or_eq 1 p); auto with zarith; clear Hp; intros Hp; subst; auto.
case (prime_dec p); intros H3.
rewrite <- (Zmult_1_r p); apply H2; auto.
case (Zdivide_div_prime_le_square p); auto.
intros q (Hq1, ((q2, Hq2), Hq3)); subst.
case (Zmult_interval q q2).
rewrite Zmult_comm; apply Zlt_trans with 1; auto with zarith.
apply Zlt_le_trans with 2; auto with zarith; apply prime_ge_2; auto.
intros H4 H5; rewrite Zmult_comm; apply H2; auto.
apply Rec; try split; auto with zarith.
rewrite Zmult_comm; auto.
Qed.
Theorem div_power_max: forall p q, 1 < p -> 0 < q -> exists n, 0 <= n /\ (p ^n | q) /\ ~(p ^(1 + n) | q).
intros p q H1 H2; generalize H2; pattern q; apply Z_lt_induction; auto with zarith; clear q H2.
intros q Rec H2.
case (Zdivide_dec p q); intros H3.
case (Zdivide_Zdiv_lt_pos p q); auto with zarith; intros H4 H5.
case (Rec (Zdiv q p)); auto with zarith.
intros n (Ha1, (Ha2, Ha3)); exists (n + 1); split; auto with zarith; split.
case Ha2; intros q1 Hq; exists q1.
rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith.
rewrite Zmult_assoc; rewrite <- Hq.
rewrite Zmult_comm; apply Zdivide_Zdiv_eq; auto with zarith.
intros (q1, Hu); case Ha3; exists q1.
apply Zmult_reg_r with p; auto with zarith.
rewrite (Zmult_comm (q / p)); rewrite <- Zdivide_Zdiv_eq; auto with zarith.
apply trans_equal with (1 := Hu); repeat rewrite Zpower_exp; try rewrite Zpower_exp_1; auto with zarith.
ring.
exists 0; repeat split; try rewrite Zpower_1_r; try rewrite Zpower_exp_0; auto with zarith.
Qed.
Theorem prime_div_induction:
forall (P: Z -> Prop) n,
0 < n ->
(P 1) ->
(forall p i, prime p -> 0 <= i -> (p^i | n) -> P (p^i)) ->
(forall p q, rel_prime p q -> P p -> P q -> P (p * q)) ->
forall m, 0 <= m -> (m | n) -> P m.
intros P n P1 Hn H H1 m Hm.
generalize Hm; pattern m; apply Z_lt_induction; auto; clear m Hm.
intros m Rec Hm H2.
case (prime_dec m); intros Hm1.
rewrite <- Zpower_1_r; apply H; auto with zarith.
rewrite Zpower_1_r; auto.
case Zle_lt_or_eq with (1 := Hm); clear Hm; intros Hm; subst.
2: contradict P1; case H2; intros; subst; auto with zarith.
case (Zle_lt_or_eq 1 m); auto with zarith; clear Hm; intros Hm; subst; auto.
case Zdivide_div_prime_le_square with m; auto.
intros p (Hp1, (Hp2, Hp3)).
case (div_power_max p m); auto with zarith.
generalize (prime_ge_2 p Hp1); auto with zarith.
intros i (Hi, (Hi1, Hi2)).
case Zle_lt_or_eq with (1 := Hi); clear Hi; intros Hi.
assert (Hpi: 0 < p ^ i).
apply Zpower_gt_0; auto with zarith.
apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
rewrite (Z_div_exact_2 m (p ^ i)); auto with zarith.
apply H1; auto with zarith.
apply rel_prime_sym; apply rel_prime_Zpower_r; auto with zarith.
apply rel_prime_sym.
apply prime_rel_prime; auto.
contradict Hi2.
case Hi1; intros; subst.
rewrite Z_div_mult in Hi2; auto with zarith.
case Hi2; intros q0 Hq0; subst.
exists q0; rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith.
apply H; auto with zarith.
apply Zdivide_trans with (1 := Hi1); auto.
apply Rec; auto with zarith.
split; auto with zarith.
apply Z_div_pos; auto with zarith.
apply Z_div_lt; auto with zarith.
apply Zle_ge; apply Zle_trans with p.
apply prime_ge_2; auto.
pattern p at 1; rewrite <- Zpower_1_r; apply Zpower_le_monotone; auto with zarith.
apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
apply Z_div_pos; auto with zarith.
apply Zdivide_trans with (2 := H2); auto.
exists (p ^ i); apply Z_div_exact_2; auto with zarith.
apply Zdivide_mod; auto with zarith.
apply Zdivide_mod; auto with zarith.
case Hi2; rewrite <- Hi; rewrite Zplus_0_r; rewrite Zpower_1_r; auto.
Qed.
Theorem prime_div_Zpower_prime: forall n p q, 0 <= n -> prime p -> prime q -> (p | q ^ n) -> p = q.
intros n p q Hp Hq; generalize p q Hq; pattern n; apply natlike_ind; auto; clear n p q Hp Hq.
intros p q Hp Hq; rewrite Zpower_0_r.
intros (r, H); subst.
case (Zmult_interval p r); auto; try rewrite Zmult_comm.
rewrite <- H; auto with zarith.
apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
rewrite <- H; intros H1 H2; contradict H2; auto with zarith.
intros n1 H Rec p q Hp Hq; try rewrite Zpower_Zsucc; auto with zarith; intros H1.
case prime_mult with (2 := H1); auto.
intros H2; apply prime_div_prime; auto.
Qed.
Definition Zmodd a b :=
match a with
| Z0 => 0
| Zpos a' =>
match b with
| Z0 => 0
| Zpos _ => Zmod_POS a' b
| Zneg b' =>
let r := Zmod_POS a' (Zpos b') in
match r with Z0 => 0 | _ => b + r end
end
| Zneg a' =>
match b with
| Z0 => 0
| Zpos _ =>
let r := Zmod_POS a' b in
match r with Z0 => 0 | _ => b - r end
| Zneg b' => - (Zmod_POS a' (Zpos b'))
end
end.
Theorem Zmodd_correct: forall a b, Zmodd a b = Zmod a b.
intros a b; unfold Zmod; case a; simpl; auto.
intros p; case b; simpl; auto.
intros p1; refine (Zmod_POS_correct _ _); auto.
intros p1; rewrite Zmod_POS_correct; auto.
case (Zdiv_eucl_POS p (Zpos p1)); simpl; intros z1 z2; case z2; auto.
intros p; case b; simpl; auto.
intros p1; rewrite Zmod_POS_correct; auto.
case (Zdiv_eucl_POS p (Zpos p1)); simpl; intros z1 z2; case z2; auto.
intros p1; rewrite Zmod_POS_correct; simpl; auto.
case (Zdiv_eucl_POS p (Zpos p1)); auto.
Qed.
Theorem prime_divide_prime_eq:
forall p1 p2, prime p1 -> prime p2 -> Zdivide p1 p2 -> p1 = p2.
intros p1 p2 Hp1 Hp2 Hp3.
assert (Ha: 1 < p1).
inversion Hp1; auto.
assert (Ha1: 1 < p2).
inversion Hp2; auto.
case (Zle_lt_or_eq p1 p2); auto with zarith.
apply Zdivide_le; auto with zarith.
intros Hp4.
case (prime_div_prime p1 p2); auto with zarith.
Qed.
Theorem Zdivide_Zpower: forall n m, 0 < n -> (forall p i, prime p -> 0 < i -> (p^i | n) -> (p^i | m)) -> (n | m).
intros n m Hn; generalize m Hn; pattern n; apply prime_induction; auto with zarith; clear n m Hn.
intros m H1; contradict H1; auto with zarith.
intros p q H Rec m H1 H2.
assert (H3: (p | m)).
rewrite <- (Zpower_1_r p); apply H2; auto with zarith; rewrite Zpower_1_r; apply Zdivide_factor_r.
case (Zmult_interval p q); auto.
apply Zlt_le_trans with 2; auto with zarith; apply prime_ge_2; auto.
case H3; intros k Hk; subst.
intros Hq Hq1.
rewrite (Zmult_comm k); apply Zmult_divide_compat_l.
apply Rec; auto.
intros p1 i Hp1 Hp2 Hp3.
case (Z_eq_dec p p1); intros Hpp1; subst.
case (H2 p1 (Zsucc i)); auto with zarith.
rewrite Zpower_Zsucc; try apply Zmult_divide_compat_l; auto with zarith.
intros q2 Hq2; exists q2.
apply Zmult_reg_r with p1.
contradict H; subst; apply not_prime_0.
rewrite Hq2; rewrite Zpower_Zsucc; try ring; auto with zarith.
apply Gauss with p.
rewrite Zmult_comm; apply H2; auto.
apply Zdivide_trans with (1:= Hp3).
apply Zdivide_factor_l.
apply rel_prime_sym; apply rel_prime_Zpower_r; auto with zarith.
apply prime_rel_prime; auto.
contradict Hpp1; apply prime_divide_prime_eq; auto.
Qed.
Theorem prime_divide_Zpower_Zdiv: forall m a p i, 0 <= i -> prime p -> (m | a) -> ~(m | (a/p)) -> (p^i | a) -> (p^i | m).
intros m a p i Hi Hp (k, Hk) H (l, Hl); subst.
case (Zle_lt_or_eq 0 i); auto with arith; intros Hi1; subst.
assert (Hp0: 0 < p).
apply Zlt_le_trans with 2; auto with zarith; apply prime_ge_2; auto.
case (Zdivide_dec p k); intros H1.
case H1; intros k' H2; subst.
case H; replace (k' * p * m) with ((k' * m) * p); try ring; rewrite Z_div_mult; auto with zarith.
apply Gauss with k.
exists l; rewrite Hl; ring.
apply rel_prime_sym; apply rel_prime_Zpower_r; auto.
apply rel_prime_sym; apply prime_rel_prime; auto.
rewrite Zpower_0_r; apply Zone_divide.
Qed.
Theorem Zle_square_mult: forall a b, 0 <= a <= b -> a * a <= b * b.
intros a b (H1, H2); apply Zle_trans with (a * b); auto with zarith.
Qed.
Theorem Zlt_square_mult_inv: forall a b, 0 <= a -> 0 <= b -> a * a < b * b -> a < b.
intros a b H1 H2 H3; case (Zle_or_lt b a); auto; intros H4; apply Zmult_lt_reg_r with a;
contradict H3; apply Zle_not_lt; apply Zle_square_mult; auto.
Qed.
Theorem Zmod_closeby_eq: forall a b n, 0 <= a -> 0 <= b < n -> a - b < n -> a mod n = b -> a = b.
intros a b n H H1 H2 H3.
case (Zle_or_lt 0 (a - b)); intros H4.
case Zle_lt_or_eq with (1 := H4); clear H4; intros H4; auto with zarith.
contradict H2; apply Zle_not_lt; apply Zdivide_le; auto with zarith.
apply Zmod_divide_minus; auto with zarith.
rewrite <- (Zmod_small a n); try split; auto with zarith.
Qed.
Theorem Zpow_mod_pos_Zpower_pos_correct: forall a m n, 0 < n -> Zpow_mod_pos a m n = (Zpower_pos a m) mod n.
intros a m; elim m; simpl; auto.
intros p Rec n H1; rewrite xI_succ_xO; rewrite Pplus_one_succ_r; rewrite <- Pplus_diag; auto.
repeat rewrite Zpower_pos_is_exp; auto.
repeat rewrite Rec; auto.
replace (Zpower_pos a 1) with a; auto.
2: unfold Zpower_pos; simpl; auto with zarith.
repeat rewrite (fun x => (Zmult_mod x a)); auto.
rewrite (Zmult_mod (Zpower_pos a p)); auto.
case (Zpower_pos a p mod n); auto.
intros p Rec n H1; rewrite <- Pplus_diag; auto.
repeat rewrite Zpower_pos_is_exp; auto.
repeat rewrite Rec; auto.
rewrite (Zmult_mod (Zpower_pos a p)); auto.
case (Zpower_pos a p mod n); auto.
unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto with zarith.
Qed.
Theorem Zpow_mod_Zpower_correct: forall a m n, 1 < n -> 0 <= m -> Zpow_mod a m n = (a ^ m) mod n.
intros a m n; case m; simpl; auto.
intros; apply Zpow_mod_pos_Zpower_pos_correct; auto with zarith.
Qed.
|
