blob: dfd3e81425b2e88710c62e4230b2bb6d0e36d12c (
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
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
|
(*************************************************************)
(* 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 *)
(*************************************************************)
Set Implicit Arguments.
Require Import ZArith Znumtheory Zpow_facts.
Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31.
Require Import ZCAux.
Require Import W.
Require Import Mod_op.
Require Import LucasLehmer.
Require Import Coqprime.Bits.
Import CyclicAxioms DoubleType DoubleBase.
Open Scope Z_scope.
Section test.
Variable w: Type.
Variable w_op: ZnZ.Ops w.
Variable op_spec: ZnZ.Specs w_op.
Variable p: positive.
Variable b: w.
Notation "[| x |]" :=
(ZnZ.to_Z x) (at level 0, x at level 99).
Hypothesis p_more_1: 2 < Zpos p.
Hypothesis b_p: [|b|] = 2 ^ Zpos p - 1.
Lemma b_pos: 0 < [|b|].
rewrite b_p; auto with zarith.
assert (2 ^ 0 < 2 ^ Zpos p); auto with zarith.
apply Zpower_lt_monotone; auto with zarith.
rewrite Zpower_0_r in H; auto with zarith.
Qed.
Hint Resolve b_pos.
Variable m_op: mod_op w.
Variable m_op_spec: mod_spec w_op b m_op.
Let w2 := m_op.(add_mod) ZnZ.one ZnZ.one.
Lemma w1_b: [|ZnZ.one|] = 1 mod [|b|].
rewrite ZnZ.spec_1; simpl; auto.
rewrite Zmod_small; auto with zarith.
split; auto with zarith.
rewrite b_p.
assert (2 ^ 1 < 2 ^ Zpos p); auto with zarith.
apply Zpower_lt_monotone; auto with zarith.
rewrite Zpower_1_r in H; auto with zarith.
Qed.
Lemma w2_b: [|w2|] = 2 mod [|b|].
unfold w2; rewrite (add_mod_spec m_op_spec _ _ _ _ w1_b w1_b).
rewrite w1_b; rewrite <- Zplus_mod; auto with zarith.
Qed.
Let w4 := m_op.(add_mod) w2 w2.
Lemma w4_b: [|w4|] = 4 mod [|b|].
unfold w4; rewrite (add_mod_spec m_op_spec _ _ _ _ w2_b w2_b).
rewrite w2_b; rewrite <- Zplus_mod; auto with zarith.
Qed.
Let square_m2 :=
let square := m_op.(square_mod) in
let sub := m_op.(sub_mod) in
fun x => sub (square x) w2.
Definition lucastest :=
ZnZ.to_Z (iter_pos (Pminus p 2) _ square_m2 w4).
Theorem lucastest_aux_correct:
forall p1 z n, 0 <= n -> [|z|] = fst (s n) mod (2 ^ Zpos p - 1) ->
[|iter_pos p1 _ square_m2 z|] = fst (s (n + Zpos p1)) mod (2 ^ Zpos p - 1).
intros p1; pattern p1; apply Pind; simpl iter_pos; simpl s; clear p1.
intros z p1 Hp1 H.
unfold square_m2.
rewrite <- b_p in H.
generalize (square_mod_spec m_op_spec _ _ H); intros H1.
rewrite (sub_mod_spec m_op_spec _ _ _ _ H1 w2_b).
rewrite H1; rewrite w2_b; auto with zarith.
rewrite H; rewrite <- Zmult_mod; auto with zarith.
rewrite <- Zminus_mod; auto with zarith.
rewrite sn; simpl; auto with zarith.
rewrite b_p; auto.
intros p1 Rec w1 z Hz Hw1.
rewrite Pplus_one_succ_l; rewrite iter_pos_plus;
simpl iter_pos.
match goal with |- context[square_m2 ?X] =>
set (tmp := X); unfold square_m2; unfold tmp; clear tmp
end.
generalize (Rec _ _ Hz Hw1); intros H1.
rewrite <- b_p in H1.
generalize (square_mod_spec m_op_spec _ _ H1); intros H2.
rewrite (sub_mod_spec m_op_spec _ _ _ _ H2 w2_b).
rewrite H2; rewrite w2_b; auto with zarith.
rewrite H1; rewrite <- Zmult_mod; auto with zarith.
rewrite <- Zminus_mod; auto with zarith.
replace (z + Zpos (1 + p1)) with ((z + Zpos p1) + 1); auto with zarith.
rewrite sn; simpl fst; try rewrite b_p; auto with zarith.
rewrite Zpos_plus_distr; auto with zarith.
Qed.
Theorem lucastest_prop: lucastest = fst(s (Zpos p -2)) mod (2 ^ Zpos p - 1).
unfold lucastest.
assert (F: 0 <= 0); auto with zarith.
generalize (lucastest_aux_correct (p -2) w4 F); simpl Zplus;
rewrite Zpos_minus; auto with zarith.
rewrite Zmax_right; auto with zarith.
intros tmp; apply tmp; clear tmp.
rewrite <- b_p; simpl; exact w4_b.
Qed.
Theorem lucastest_prop_cor: lucastest = 0 -> (2 ^ Zpos p - 1 | fst(s (Zpos p - 2)))%Z.
intros H.
apply Zmod_divide.
assert (H1: 2 ^ 1 < 2 ^ Zpos p); auto with zarith.
apply Zpower_lt_monotone; auto with zarith.
rewrite Zpower_1_r in H1; auto with zarith.
apply trans_equal with (2:= H); apply sym_equal; apply lucastest_prop; auto.
Qed.
Theorem lucastest_prime: lucastest = 0 -> prime (2 ^ Zpos p - 1).
intros H1; case (prime_dec (2 ^ Zpos p - 1)); auto; intros H2.
case Zdivide_div_prime_le_square with (2 := H2).
assert (H3: 2 ^ 1 < 2 ^ Zpos p); auto with zarith.
apply Zpower_lt_monotone; auto with zarith.
rewrite Zpower_1_r in H3; auto with zarith.
intros q (H3, (H4, H5)).
contradict H5; apply Zlt_not_le.
generalize q_more_than_square; unfold Mp; intros tmp; apply tmp;
auto; clear tmp.
apply lucastest_prop_cor; auto.
case (Zle_lt_or_eq 2 q); auto.
apply prime_ge_2; auto.
intros H5; subst.
absurd (2 <= 1); auto with arith.
apply Zdivide_le; auto with zarith.
case H4; intros x Hx.
exists (2 ^ (Zpos p -1) - x).
rewrite Zmult_minus_distr_r; rewrite <- Hx; unfold Mp.
pattern 2 at 2; rewrite <- Zpower_1_r; rewrite <- Zpower_exp; auto with zarith.
replace (Zpos p - 1 + 1) with (Zpos p); auto with zarith.
Qed.
End test.
Definition znz_of_Z (w: Type) (op: ZnZ.Ops w) z :=
match z with
| Zpos p => snd (ZnZ.of_pos p)
| _ => ZnZ.zero
end.
Definition lucas p :=
let op := cmk_op (Peano.pred (nat_of_P (get_height 31 p))) in
let b := znz_of_Z op (Zpower 2 (Zpos p) - 1) in
let zp := znz_of_Z op (Zpos p) in
let mod_op := mmake_mod_op op b zp in
lucastest op p mod_op.
Theorem lucas_prime:
forall p, 2 < Zpos p -> lucas p = 0 -> prime (2 ^ Zpos p - 1).
unfold lucas; intros p Hp H.
match type of H with lucastest (cmk_op ?x) ?y ?z = _ =>
set (w_op := (cmk_op x)); assert(A1: ZnZ.Specs w_op)
end.
unfold w_op; apply cmk_spec.
assert (F0: Zpos p <= Zpos (ZnZ.digits w_op)).
unfold w_op, base; rewrite (cmk_op_digits (Peano.pred (nat_of_P (get_height 31 p)))).
generalize (get_height_correct 31 p).
replace (Z_of_nat (Peano.pred (nat_of_P (get_height 31 p)))) with
((Zpos (get_height 31 p) - 1) ); auto with zarith.
rewrite pred_of_minus; rewrite inj_minus1; auto with zarith.
rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto with zarith.
generalize (lt_O_nat_of_P (get_height 31 p)); auto with zarith.
assert (F1: ZnZ.to_Z (znz_of_Z w_op (2 ^ (Zpos p) - 1)) = 2 ^ (Zpos p) - 1).
assert (F1: 0 < 2 ^ (Zpos p) - 1).
assert (F2: 2 ^ 0 < 2 ^ (Zpos p)); auto with zarith.
apply Zpower_lt_monotone; auto with zarith.
rewrite Zpower_0_r in F2; auto with zarith.
case_eq (2 ^ (Zpos p) - 1); simpl ZnZ.to_Z.
intros HH; contradict F1; rewrite HH; auto with zarith.
2: intros p1 HH; contradict F1; rewrite HH;
apply Zle_not_lt; red; simpl; intros; discriminate.
intros p1 Hp1; apply ZnZ.of_pos_correct; auto.
rewrite <- Hp1.
unfold base.
apply Zlt_le_trans with (2 ^ (Zpos p)); auto with zarith.
apply Zpower_le_monotone; auto with zarith.
match type of H with lucastest (cmk_op ?x) ?y ?z = _ =>
apply
(@lucastest_prime _ _ (cmk_spec x) p (znz_of_Z w_op (2 ^ Zpos p -1)) Hp F1 z)
end; auto with zarith; fold w_op.
eapply mmake_mod_spec with (p := p); auto with zarith.
unfold znz_of_Z; unfold znz_of_Z in F1; rewrite F1.
assert (F2: 2 ^ 1 < 2 ^ (Zpos p)); auto with zarith.
apply Zpower_lt_monotone; auto with zarith.
rewrite Zpower_1_r in F2; auto with zarith.
rewrite ZnZ.of_Z_correct; auto with zarith.
split; auto with zarith.
apply Zle_lt_trans with (1 := F0); auto with zarith.
unfold base; apply Zpower2_lt_lin; auto with zarith.
Qed.
|
