-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathexercise2.v
291 lines (245 loc) · 8.05 KB
/
exercise2.v
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
From elpi Require Import elpi.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(** Elements *)
Definition elements {A} (f : _ -> A) n :=
let l := iota 0 n.+1 in zip l (map f l).
(** Triangular number *)
Definition delta n := (n.+1 * n)./2.
Lemma deltaE n : delta n = (n.+1 * n)./2.
Proof. by []. Qed.
Lemma delta1 : delta 1 = 1.
Proof. by []. Qed.
Compute elements delta 10.
(** Hints : halfD half_bit_double *)
Lemma deltaS n : delta n.+1 = delta n + n.+1.
Proof.
(*D*)rewrite !deltaE -addn2 mulnDl mulnC halfD.
(*D*)rewrite !oddM andbF add0n mul2n.
(*D*)suff -> : ((n.+1).*2)./2 = n.+1 by [].
(*D*)by rewrite -[RHS](half_bit_double n.+1 false).
(*A*)Qed.
(* Hints half_leq *)
Lemma leq_delta m n : m <= n -> delta m <= delta n.
Proof.
(*D*)by move=> H; apply: half_leq; apply: leq_mul.
(*A*)Qed.
(** Hints sqrnD *)
Lemma delta_square n : (8 * delta n).+1 = n.*2.+1 ^ 2.
Proof.
(*D*)elim: n => // n IH.
(*D*)rewrite deltaS mulnDr -addSn IH.
(*D*)rewrite doubleS -addn1 -addnS -addSn addn1.
(*D*)rewrite sqrnD -addnA /=.
(*D*)congr (_ + _).
(*D*)rewrite mulnS.
(*D*)rewrite [_ * 2]mulSn mulnDr addnA.
(*D*)congr (_ + _).
(*D*)by rewrite mulnCA -muln2 -!mulnA mulnC.
(*A*)Qed.
(** Triangular root *)
Definition troot n :=
let l := iota 0 n.+2 in
(find (fun x => n < delta x) l).-1.
Lemma trootE n :
troot n = (find (fun x => n < delta x) (iota 0 n.+2)).-1.
Proof. by []. Qed.
Compute elements troot 10.
Lemma troot_gt0 n : 0 < n -> 0 < troot n.
Proof.
(*D*)by case: n.
(*A*)Qed.
(** Hints before_find find_size size_iota nth_iota *)
Lemma leq_delta_root m : delta (troot m) <= m.
Proof.
(*D*)rewrite trootE leqNgt.
(*D*)set l := iota _ _; set f := (fun _ => _).
(*D*)case E : (find f l).-1 => [|n] //.
(*D*)have /(before_find 0) :
(*D*) (find f l).-1 < find f l by rewrite prednK // E.
(*D*)rewrite E nth_iota // /f => [->//|].
(*D*)rewrite -[m.+2](size_iota 0) -E prednK; first by apply: find_size.
(*D*)by case: find E.
(*A*)Qed.
(** Hints hasP mem_iota half_bit_double half_leq nth_find nth_iota *)
Lemma ltn_delta_root m : m < delta (troot m).+1.
Proof.
(*D*)rewrite /troot leqNgt.
(*D*)set l := iota _ _; set f := (fun _ => _).
(*D*)have Hfl : has f l.
(*D*) apply/hasP; exists m.+1; first by rewrite mem_iota leq0n leqnn.
(*D*) rewrite /f /delta -{1}[m.+1](half_bit_double _ false).
(*D*) by apply/half_leq; rewrite add0n -mul2n leq_mul2r orbT.
(*D*)have := nth_find 0 Hfl; rewrite {1}/f.
(*D*)case E : _.-1 => [|n] //.
(*D*) case: find E => // [] [|n] //.
(*D*) by rewrite nth_iota //=; case: (m).
(*D*)rewrite nth_iota.
(*D*) by rewrite -E prednK // ltnNge ltnS.
(*D*)by rewrite -(size_iota 0 m.+2) -has_find.
(*A*)Qed.
Lemma leq_root_delta m n : (n <= troot m) = (delta n <= m).
Proof.
(*D*)case: leqP => [/leq_delta/leq_trans->//|dmLn].
(*D*) apply: leq_delta_root.
(*D*)apply/sym_equal/idP/negP.
(*D*)rewrite -ltnNge.
(*D*)by apply: leq_trans (ltn_delta_root _) (leq_delta dmLn).
(*A*)Qed.
Lemma leq_troot m n : m <= n -> troot m <= troot n.
Proof.
(*D*)by move=> mLn; rewrite leq_root_delta (leq_trans (leq_delta_root _)).
(*A*)Qed.
Lemma troot_delta m n : (troot m == n) = (delta n <= m < delta n.+1).
Proof.
(*D*)by rewrite ltnNge -!leq_root_delta -ltnNge ltnS -eqn_leq eq_sym.
(*A*)Qed.
Lemma troot_deltaK n : troot (delta n) = n.
Proof.
(*D*)by apply/eqP; rewrite troot_delta leqnn deltaS -addn1 leq_add2l.
(*A*)Qed.
(** The modulo for triangular numbers *)
Definition tmod n := n - delta (troot n).
Lemma tmodE n : tmod n = n - delta (troot n).
Proof. by []. Qed.
Lemma tmod_delta n : tmod (delta n) = 0.
Proof.
(*D*)by rewrite tmodE troot_deltaK subnn.
(*A*)Qed.
Lemma delta_tmod n : n = delta (troot n) + tmod n.
Proof.
(*D*)by rewrite addnC (subnK (leq_delta_root _)).
(*A*)Qed.
Lemma leq_tmod_troot n : tmod n <= troot n.
Proof.
(*D*)by rewrite leq_subLR -ltnS -addnS -deltaS ltn_delta_root.
(*A*)Qed.
Lemma ltn_troot m n : troot m < troot n -> m < n.
Proof.
(*D*)rewrite leq_root_delta deltaS => /(leq_trans _) -> //.
(*D*)by rewrite [X in X < _]delta_tmod ltn_add2l ltnS leq_tmod_troot.
(*A*)Qed.
Lemma leq_tmod m n : troot m = troot n -> (tmod m <= tmod n) = (m <= n).
Proof.
(*D*)move=> tmEtn.
(*D*)rewrite [X in _ = (X <= _)]delta_tmod.
(*D*)rewrite [X in _ = (_ <= X)]delta_tmod.
(*D*)by rewrite tmEtn leq_add2l.
(*A*)Qed.
Lemma leq_troot_mod m n :
m <= n =
((troot m < troot n) || ((troot m == troot n) && (tmod m <= tmod n))).
Proof.
(*D*)case: leqP => [|dmGdn] /= ; last first.
(*D*) apply/idP.
(*D*) apply: (leq_trans (_ : _ <= delta (troot m).+1)).
(*D*) by rewrite ltnW // ltn_delta_root.
(*D*) apply: (leq_trans (_ : _ <= delta (troot n))).
(*D*) by apply: leq_delta.
(*D*) by apply: leq_delta_root.
(*D*)rewrite leq_eqVlt => /orP[/eqP dnEdm|dmLdn].
(*D*) rewrite dnEdm eqxx /=.
(*D*) rewrite [X in (X <= _) = _]delta_tmod [X in _ <= X = _]delta_tmod.
by rewrite dnEdm leq_add2l.
(*D*)rewrite (gtn_eqF dmLdn) /=.
(*D*)apply/idP/negP.
(*D*)rewrite -ltnNge.
(*D*)apply: (leq_trans (ltn_delta_root _)).
(*D*)apply: (leq_trans _ (leq_delta_root _)).
(*D*)by apply: leq_delta.
(*A*)Qed.
(** Fermat Numbers *)
Definition fermat n := (2 ^ (2 ^ n)).+1.
Lemma fermatE n : fermat n = (2 ^ (2 ^ n)).+1.
Proof. by []. Qed.
Compute elements (prime \o fermat) 4.
(** Hints : subn_sqr subnBA odd_double_half *)
Lemma dvd_exp_odd a k :
0 < a -> odd k -> a.+1 %| (a ^ k).+1.
Proof.
move=> aP kO.
(*D*)rewrite -[k]odd_double_half {}kO add1n.
(*D*)elim: {k}_./2 => [|k IH]; first by apply/dvdnn.
(*D*)rewrite doubleS.
(*D*)rewrite (_ : (a ^ k.*2.+3).+1 =
(*D*) (a ^ 2 * (a ^ k.*2.+1).+1) - (a ^ 2 - 1)); last first.
(*D*) rewrite mulnSr -expnD !addSn subnBA ?expn_gt0 ?aP //.
(*D*) by rewrite addnAC addnK addn1.
(*D*)rewrite dvdn_sub ?dvdn_mull //.
(*D*)by rewrite -[X in _ %| _ - X](exp1n 2) subn_sqr addn1 dvdn_mull.
(*A*)Qed.
(** Hints: logn_gt0 mem_primes dvdn2 *)
Lemma odd_log_eq0 n : 0 < n -> logn 2 n = 0 -> odd n.
Proof.
(*D*)case: n => // n _ HL.
(*D*)have : 2 \notin primes n.+1.
(*D*) rewrite -logn_gt0.
(*D*) by case: (logn 2 n.+1) HL.
(*D*)by rewrite mem_primes /= dvdn2 negbK.
(*A*)Qed.
(** Hints pfactor_dvdnn logn_div pfactorK *)
Lemma odd_div_log n : 0 < n -> odd (n %/ 2 ^ logn 2 n).
Proof.
(*D*)move=> nP.
(*D*)apply: odd_log_eq0.
(*D*) rewrite divn_gt0 ?expn_gt0 //.
(*D*) apply: dvdn_leq => //.
(*D*) apply: pfactor_dvdnn.
(*D*)rewrite logn_div.
(*D*) by rewrite pfactorK // subnn.
(*D*)by apply: pfactor_dvdnn.
(*A*)Qed.
(** Hints divnK pfactor_dvdnn prime_nt_dvdP prime_nt_dvdP *)
Lemma prime_2expS m :
0 < m -> prime (2 ^ m).+1 -> m = 2 ^ logn 2 m.
Proof.
(*D*)move=> mP Hp.
(*D*)pose a := 2 ^ logn 2 m.
(*D*)pose b := m %/ a.
(*D*)have : (2 ^ a).+1 %| (2 ^ m).+1.
(*D*) rewrite -(divnK (pfactor_dvdnn 2 m)).
(*D*) rewrite mulnC expnM.
(*D*)apply: dvd_exp_odd; first by apply: expn_gt0.
(*D*) by apply: odd_div_log.
(*D*)have F : (2 ^ a).+1 != 1.
(*D*) by rewrite eq_sym neq_ltn ltnS expn_gt0.
(*D*)move=> /(prime_nt_dvdP Hp).
(*D*)move=> /(_ F) [] /eqP.
(*D*)by rewrite eqn_exp2l // => /eqP{1}<-.
(*A*)Qed.
(** Hints oddX neq_ltn expn_gt0 *)
Lemma odd_fermat n : odd (fermat n).
Proof.
(*D*)by rewrite /= oddX negb_or eq_sym neq_ltn expn_gt0.
(*A*)Qed.
(** Hint subn_sqr *)
Lemma dvdn_exp2m1 a k : a.+1 %| (a ^ (2 ^ k.+1)).-1.
Proof.
(*D*)elim: k => /= [|k IH].
(*D*) rewrite expn1 -subn1 -[X in _ %| _ - X](exp1n 2).
(*D*) by rewrite subn_sqr addn1 dvdn_mull //.
(*D*)rewrite -subn1 -{2}[1](exp1n 2) expnS mulnC expnM subn_sqr.
(*D*)by rewrite dvdn_mulr // subn1.
(*A*)Qed.
(** Hints subnK expnD expnM *)
Lemma dvdn_fermat m n : m < n -> fermat m %| (fermat n).-2.
Proof.
(*D*)move=> mLn.
(*D*)rewrite fermatE /= -(subnK mLn) -addSnnS addnC.
(*D*)by rewrite expnD expnM dvdn_exp2m1.
(*A*)Qed.
Lemma fermat_gt1 n : 1 < fermat n.
Proof.
(*D*)by rewrite ltnS expn_gt0.
(*A*)Qed.
(** Hints gcdnMDl coprimen2 *)
Lemma coprime_fermat m n : m < n -> coprime (fermat m) (fermat n).
Proof.
(*D*)move=> mLn.
(*D*)rewrite /coprime -(subnK (fermat_gt1 n)) subn2.
(*D*)case/dvdnP: (dvdn_fermat mLn) => k ->.
(*D*)by rewrite gcdnMDl [_ == _]coprimen2 odd_fermat.
(*A*)Qed.