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
|
(*************************************************************)
(* 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 *)
(*************************************************************)
Require Import ZArith.
Require Export Znumtheory.
Require Import Tactic.
Require Import ZCAux.
Require Import Zp.
Require Import FGroup.
Require Import EGroup.
Require Import Euler.
Open Scope Z_scope.
Theorem Pocklington:
forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 ->
(forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) ->
forall n, prime n -> (n | N) -> n mod F1 = 1.
intros N F1 R1 HF1 HR1 Neq Rec n Hn H.
assert (HN: 1 < N).
assert (0 < N - 1); auto with zarith.
rewrite Neq; auto with zarith.
apply Zlt_le_trans with (1* R1); auto with zarith.
assert (Hn1: 1 < n); auto with zarith.
apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
assert (H1: (F1 | n - 1)).
2: rewrite <- (Zmod_small 1 F1); auto with zarith.
2: case H1; intros k H1'.
2: replace n with (1 + (n - 1)); auto with zarith.
2: rewrite H1'; apply Z_mod_plus; auto with zarith.
apply Zdivide_Zpower; auto with zarith.
intros p i Hp Hi HiF1.
case (Rec p); auto.
apply Zdivide_trans with (2 := HiF1).
apply Zpower_divide; auto with zarith.
intros a (Ha1, (Ha2, Ha3)).
assert (HNn: a ^ (N - 1) mod n = 1).
apply Zdivide_mod_minus; auto with zarith.
apply Zdivide_trans with (1 := H).
apply Zmod_divide_minus; auto with zarith.
assert (~(n | a)).
intros H1; absurd (0 = 1); auto with zarith.
rewrite <- HNn; auto.
apply sym_equal; apply Zdivide_mod; auto with zarith.
apply Zdivide_trans with (1 := H1); apply Zpower_divide; auto with zarith.
assert (Hr: rel_prime a n).
apply rel_prime_sym; apply prime_rel_prime; auto.
assert (Hz: 0 < Zorder a n).
apply Zorder_power_pos; auto.
apply Zdivide_trans with (Zorder a n).
apply prime_divide_Zpower_Zdiv with (N - 1); auto with zarith.
apply Zorder_div_power; auto with zarith.
intros H1; absurd (1 < n); auto; apply Zle_not_lt; apply Zdivide_le; auto with zarith.
rewrite <- Ha3; apply Zdivide_Zgcd; auto with zarith.
apply Zmod_divide_minus; auto with zarith.
case H1; intros t Ht; rewrite Ht.
assert (Ht1: 0 <= t).
apply Zmult_le_reg_r with (Zorder a n); auto with zarith.
rewrite Zmult_0_l; rewrite <- Ht.
apply Zge_le; apply Z_div_ge0; auto with zarith.
apply Zlt_gt; apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith.
rewrite Zpower_mod; auto with zarith.
rewrite Zorder_power_is_1; auto with zarith.
rewrite Zpower_1_l; auto with zarith.
apply Zmod_small; auto with zarith.
apply Zdivide_trans with (1:= HiF1); rewrite Neq; apply Zdivide_factor_r.
apply Zorder_div; auto.
Qed.
Theorem PocklingtonCorollary1:
forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> N < F1 * F1 ->
(forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) ->
prime N.
intros N F1 R1 H H1 H2 H3 H4; case (prime_dec N); intros H5; auto.
assert (HN: 1 < N).
assert (0 < N - 1); auto with zarith.
rewrite H2; auto with zarith.
apply Zlt_le_trans with (1* R1); auto with zarith.
case Zdivide_div_prime_le_square with (2:= H5); auto with zarith.
intros n (Hn, (Hn1, Hn2)).
assert (Hn3: 0 <= n).
apply Zle_trans with 2; try apply prime_ge_2; auto with zarith.
absurd (n = 1).
intros H6; contradict Hn; subst; apply not_prime_1.
rewrite <- (Zmod_small n F1); try split; auto.
apply Pocklington with (R1 := R1) (4 := H4); auto.
apply Zlt_square_mult_inv; auto with zarith.
Qed.
Theorem PocklingtonCorollary2:
forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 ->
(forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) ->
forall n, 0 <= n -> (n | N) -> n mod F1 = 1.
intros N F1 R1 H1 H2 H3 H4 n H5; pattern n; apply prime_induction; auto.
assert (HN: 1 < N).
assert (0 < N - 1); auto with zarith.
rewrite H3; auto with zarith.
apply Zlt_le_trans with (1* R1); auto with zarith.
intros (u, Hu); contradict HN; subst; rewrite Zmult_0_r; auto with zarith.
intro H6; rewrite Zmod_small; auto with zarith.
intros p q Hp Hp1 Hp2; rewrite Zmult_mod; auto with zarith.
rewrite Pocklington with (n := p) (R1 := R1) (4 := H4); auto.
rewrite Hp1.
rewrite Zmult_1_r; rewrite Zmod_small; auto with zarith.
apply Zdivide_trans with (2 := Hp2); apply Zdivide_factor_l.
apply Zdivide_trans with (2 := Hp2); apply Zdivide_factor_r; auto.
Qed.
Definition isSquare x := exists y, x = y * y.
Theorem PocklingtonExtra:
forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> Zeven F1 -> Zodd R1 ->
(forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) ->
forall m, 1 <= m -> (forall l, 1 <= l < m -> ~((l * F1 + 1) | N)) ->
let s := (R1 / (2 * F1)) in
let r := (R1 mod (2 * F1)) in
N < (m * F1 + 1) * (2 * F1 * F1 + (r - m) * F1 + 1) ->
(s = 0 \/ ~ isSquare (r * r - 8 * s)) -> prime N.
intros N F1 R1 H1 H2 H3 OF1 ER1 H4 m H5 H6 s r H7 H8.
case (prime_dec N); auto; intros H9.
assert (HN: 1 < N).
assert (0 < N - 1); auto with zarith.
rewrite H3; auto with zarith.
apply Zlt_le_trans with (1* R1); auto with zarith.
case Zdivide_div_prime_le_square with N; auto.
intros X (Hx1, (Hx2, Hx3)).
assert (Hx0: 1 < X).
apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
pose (c := (X / F1)).
assert(Hc1: 0 <= c); auto with zarith.
apply Zge_le; unfold c; apply Z_div_ge0; auto with zarith.
assert (Hc2: X = c * F1 + 1).
rewrite (Z_div_mod_eq X F1); auto with zarith.
eq_tac; auto.
rewrite (Zmult_comm F1); auto.
apply PocklingtonCorollary2 with (R1 := R1) (4 := H4); auto with zarith.
case Zle_lt_or_eq with (1 := Hc1); clear Hc1; intros Hc1.
2: contradict Hx0; rewrite Hc2; try rewrite <- Hc1; auto with zarith.
case (Zle_or_lt m c); intros Hc3.
2: case Zle_lt_or_eq with (1 := H5); clear H5; intros H5; auto with zarith.
2: case (H6 c); auto with zarith; rewrite <- Hc2; auto.
2: contradict Hc3; rewrite <- H5; auto with zarith.
pose (d := ((N / X) / F1)).
assert(Hd0: 0 <= N / X); try apply Z_div_pos; auto with zarith.
(*
apply Zge_le; unfold d; repeat apply Z_div_ge0; auto with zarith.
*)
assert(Hd1: 0 <= d); auto with zarith.
apply Zge_le; unfold d; repeat apply Z_div_ge0; auto with zarith.
assert (Hd2: N / X = d * F1 + 1).
rewrite (Z_div_mod_eq (N / X) F1); auto with zarith.
eq_tac; auto.
rewrite (Zmult_comm F1); auto.
apply PocklingtonCorollary2 with (R1 := R1) (4 := H4); auto with zarith.
exists X; auto with zarith.
apply Zdivide_Zdiv_eq; auto with zarith.
case Zle_lt_or_eq with (1 := Hd0); clear Hd0; intros Hd0.
2: contradict HN; rewrite (Zdivide_Zdiv_eq X N); auto with zarith.
2: rewrite <- Hd0; auto with zarith.
case (Zle_lt_or_eq 1 (N / X)); auto with zarith; clear Hd0; intros Hd0.
2: contradict H9; rewrite (Zdivide_Zdiv_eq X N); auto with zarith.
2: rewrite <- Hd0; rewrite Zmult_1_r; auto with zarith.
case Zle_lt_or_eq with (1 := Hd1); clear Hd1; intros Hd1.
2: contradict Hd0; rewrite Hd2; try rewrite <- Hd1; auto with zarith.
case (Zle_or_lt m d); intros Hd3.
2: case Zle_lt_or_eq with (1 := H5); clear H5; intros H5; auto with zarith.
2: case (H6 d); auto with zarith; rewrite <- Hd2; auto.
2: exists X; auto with zarith.
2: apply Zdivide_Zdiv_eq; auto with zarith.
2: contradict Hd3; rewrite <- H5; auto with zarith.
assert (L5: N = (c * F1 + 1) * (d * F1 + 1)).
rewrite <- Hc2; rewrite <- Hd2; apply Zdivide_Zdiv_eq; auto with zarith.
assert (L6: R1 = c * d * F1 + c + d).
apply trans_equal with ((N - 1) / F1).
rewrite H3; rewrite Zmult_comm; apply sym_equal; apply Z_div_mult; auto with zarith.
rewrite L5.
match goal with |- (?X / ?Y = ?Z) => replace X with (Z * Y) end; try ring; apply Z_div_mult; auto with zarith.
assert (L6_1: Zodd (c + d)).
case (Zeven_odd_dec (c + d)); auto; intros O1.
contradict ER1; apply Zeven_not_Zodd; rewrite L6; rewrite <- Zplus_assoc; apply Zeven_plus_Zeven; auto.
apply Zeven_mult_Zeven_r; auto.
assert (L6_2: Zeven (c * d)).
case (Zeven_odd_dec c); intros HH1.
apply Zeven_mult_Zeven_l; auto.
case (Zeven_odd_dec d); intros HH2.
apply Zeven_mult_Zeven_r; auto.
contradict L6_1; apply Zeven_not_Zodd; apply Zodd_plus_Zodd; auto.
assert ((c + d) mod (2 * F1) = r).
rewrite <- Z_mod_plus with (b := Zdiv2 (c * d)); auto with zarith.
match goal with |- ?X mod _ = _ => replace X with R1 end; auto.
rewrite L6; pattern (c * d) at 1.
rewrite Zeven_div2 with (1 := L6_2); ring.
assert (L9: c + d - r < 2 * F1).
apply Zplus_lt_reg_r with (r - m).
apply Zmult_lt_reg_r with (F1); auto with zarith.
apply Zplus_lt_reg_r with 1.
match goal with |- ?X < ?Y =>
replace Y with (2 * F1 * F1 + (r - m) * F1 + 1); try ring;
replace X with ((((c + d) - m) * F1) + 1); try ring
end.
apply Zmult_lt_reg_r with (m * F1 + 1); auto with zarith.
apply Zlt_trans with (m * F1 + 0); auto with zarith.
rewrite Zplus_0_r; apply Zmult_lt_O_compat; auto with zarith.
repeat rewrite (fun x => Zmult_comm x (m * F1 + 1)).
apply Zle_lt_trans with (2 := H7).
rewrite L5.
match goal with |- ?X <= ?Y =>
replace X with ((m * (c + d) - m * m ) * F1 * F1 + (c + d) * F1 + 1); try ring;
replace Y with ((c * d) * F1 * F1 + (c + d) * F1 + 1); try ring
end.
repeat apply Zplus_le_compat_r.
repeat apply Zmult_le_compat_r; auto with zarith.
assert (tmp: forall p q, 0 <= p - q -> q <= p); auto with zarith; try apply tmp.
match goal with |- _ <= ?X =>
replace X with ((c - m) * (d - m)); try ring; auto with zarith
end.
assert (L10: c + d = r).
apply Zmod_closeby_eq with (2 * F1); auto with zarith.
unfold r; apply Z_mod_lt; auto with zarith.
assert (L11: 2 * s = c * d).
apply Zmult_reg_r with F1; auto with zarith.
apply trans_equal with (R1 - (c + d)).
rewrite L10; rewrite (Z_div_mod_eq R1 (2 * F1)); auto with zarith.
unfold s, r; ring.
rewrite L6; ring.
case H8; intro H10.
absurd (0 < c * d); auto with zarith.
apply Zmult_lt_O_compat; auto with zarith.
case H10; exists (c - d); auto with zarith.
rewrite <- L10.
replace (8 * s) with (4 * (2 * s)); auto with zarith; try rewrite L11; ring.
Qed.
Theorem PocklingtonExtraCorollary:
forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> Zeven F1 -> Zodd R1 ->
(forall p, prime p -> (p | F1) -> exists a, 1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) ->
let s := (R1 / (2 * F1)) in
let r := (R1 mod (2 * F1)) in
N < 2 * F1 * F1 * F1 -> (s = 0 \/ ~ isSquare (r * r - 8 * s)) -> prime N.
intros N F1 R1 H1 H2 H3 OF1 ER1 H4 s r H5 H6.
apply PocklingtonExtra with (6 := H4) (R1 := R1) (m := 1); auto with zarith.
apply Zlt_le_trans with (1 := H5).
match goal with |- ?X <= ?K * ((?Y + ?Z) + ?T) =>
rewrite <- (Zplus_0_l X);
replace (K * ((Y + Z) + T)) with ((F1 * (Z + T) + Y + Z + T) + X);[idtac | ring]
end.
apply Zplus_le_compat_r.
case (Zle_lt_or_eq 0 r); unfold r; auto with zarith.
case (Z_mod_lt R1 (2 * F1)); auto with zarith.
intros HH; repeat ((rewrite <- (Zplus_0_r 0); apply Zplus_le_compat)); auto with zarith.
intros HH; contradict ER1; apply Zeven_not_Zodd.
rewrite (Z_div_mod_eq R1 (2 * F1)); auto with zarith.
rewrite <- HH; rewrite Zplus_0_r.
rewrite <- Zmult_assoc; apply Zeven_2p.
Qed.
|
