/
aks.v
1773 lines (1637 loc) · 67.6 KB
/
aks.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
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
From mathcomp Require Import all_ssreflect all_fingroup all_field.
From mathcomp Require Import ssralg finalg poly polydiv zmodp vector qpoly.
From mathcomp Require cyclic.
Require Import more_thm rootn lcm_lbound.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory.
Local Open Scope ring_scope.
(******************************************************************************)
(* *)
(* This is a direct transcription of the correctness proof of the *)
(* AKS algorithm as given for HOL4 by Hing Lun Chan in his PhD thesis *)
(* *)
(******************************************************************************)
Section AKS.
Import Pdiv.CommonRing.
Import Pdiv.RingMonic.
Definition introspective {R : ringType} n k (p : {poly R}) :=
rmodp (p ^+ n) ('X^k - 1) == rmodp (p \Po 'X^n) ('X^k - 1).
Notation " n '⋈[' k ] p" := (introspective n k p)
(at level 40, format "n '⋈[' k ] p").
Lemma introspective1l (R : ringType) k (p : {poly R}) : 1 ⋈[k] p.
Proof. by rewrite /introspective expr1 comp_polyXr. Qed.
Lemma introspective1r (R : ringType) n k : n ⋈[k] (1 : {poly R}).
Proof. by rewrite /introspective expr1n comp_polyC polyC1. Qed.
Lemma introspectiveX (R : ringType) k n : n ⋈[k] ('X : {poly R}).
Proof. by rewrite /introspective comp_polyX. Qed.
(* 98 *)
Lemma introspec_char (F : finFieldType) (k p c : nat) :
p \in [char F] -> p ⋈[k] ('X + c%:R%:P : {poly F}).
Proof.
move=> pC; apply/eqP; congr (rmodp _ _).
have Pp : prime p by apply: charf_prime pC.
have Cn : [char F].-nat p by rewrite pnatE.
rewrite comp_polyD comp_polyC comp_polyX.
rewrite exprDn_char; first by rewrite -polyC_exp fin_little_fermat.
by rewrite pnatE // (rmorph_char (GRing.RMorphism.clone _ _ _ polyC)).
Qed.
(* 99 *)
Lemma introspecMl (R : comRingType) (k m n : nat) (p : {poly R}) :
m ⋈[k] p -> n ⋈[k] p -> m * n ⋈[k] p.
Proof.
case: m => // m.
have XmD1 : 'X^m.+1 != 1 :> {poly R}.
apply/eqP => /(congr1 (size : {poly R} -> _)).
by rewrite size_polyXn size_polyC oner_eq0.
case: k => [|k mIp nIp].
rewrite /introspective !subrr !rmodp0 exprM => /eqP->.
rewrite comp_poly_exp => /eqP->.
by rewrite -comp_polyA comp_Xn_poly -exprM.
have XM : ('X^k.+1 - 1 : {poly R}) \is monic.
rewrite qualifE /= lead_coefDl ?lead_coefXn ?unitr1 //.
by rewrite size_polyXn size_opp size_polyC oner_neq0.
rewrite /introspective exprM -rmodpX // (eqP mIp) rmodpX //.
rewrite exprM -['X^m.+1 ^+_]comp_Xn_poly comp_poly_exp comp_polyA.
rewrite -subr_eq0 -rmodpB // -comp_polyB.
apply: rdvdp_trans (_ : rdvdp (('X^k.+1 -1) \Po 'X^m.+1) _) => //.
- by apply: monic_comp_poly => //; rewrite qualifE /= lead_coefXn.
- rewrite comp_polyB comp_Xn_poly comp_polyC -exprM mulnC exprM.
by apply: dvdp_geom.
apply: rdvdp_comp_poly => //; first by rewrite qualifE /= lead_coefXn.
by rewrite /rdvdp rmodpB // subr_eq0.
Qed.
(* 100 *)
Lemma introspecMr (R : comRingType) (k n : nat) (p q : {poly R}) :
n ⋈[k] p -> n ⋈[k] q -> n ⋈[k] (p * q).
Proof.
case: k => [|k nIp nIq].
rewrite /introspective !subrr !rmodp0.
by rewrite comp_polyM exprMn => /eqP-> /eqP->.
have Xlf := monic_Xn_sub_1 R (isT : 0 < k.+1).
rewrite /introspective exprMn -rmodp_mulmr // (eqP nIq).
rewrite rmodp_mulmr // mulrC.
rewrite -rmodp_mulmr // (eqP nIp) rmodp_mulmr //.
by rewrite mulrC comp_polyM.
Qed.
(* 102 *)
Lemma introspec_fin_div (F : finFieldType) k n p (c : nat) :
coprime k n -> p \in [char F] -> (p %| n)%N ->
n ⋈[k] ('X + c%:R%:P : {poly F}) -> (n %/ p) ⋈[k] ('X + c%:R%:P : {poly F}).
Proof.
move=> kCn pC pDn nIkX.
have pP : prime p by case/andP: pC.
have k_gt0 : 0 < k.
case: k {nIkX}kCn pDn pP => //.
rewrite /coprime gcd0n => /eqP->.
by rewrite dvdn1 => /eqP->.
rewrite /introspective -!Pdiv.IdomainMonic.modpE ?monic_Xn_sub_1 //.
have kNZ : k%:R != 0 :> F.
rewrite -(dvdn_charf pC); apply/negP => pDk.
move: pP.
have : (p %| 1)%N by rewrite -(eqP kCn) dvdn_gcd pDk.
by rewrite dvdn1 => /eqP->.
have pCF : [char {poly F}].-nat p.
rewrite /pnat prime_gt0 //=; apply/allP => q.
rewrite primes_prime //= inE => /eqP->.
rewrite inE pP -polyC_natr polyC_eq0 /=.
by case/andP : pC.
rewrite -subr_eq0 -modpN -modpD -[_ == 0]/(_ %| _).
rewrite -(separable_exp _ (separable_polyXnsub1 _) (prime_gt0 pP)) //.
rewrite exprDn_char // exprNn_char // -exprM divnK //.
rewrite comp_polyD comp_polyC [_ ^+ p]exprDn_char //.
rewrite comp_poly_exp comp_Xn_poly -exprM divnK //.
rewrite -polyC_exp fin_little_fermat //.
rewrite /dvdp modpD modpN subr_eq0 //.
move: nIkX.
rewrite /introspective -!Pdiv.IdomainMonic.modpE ?monic_Xn_sub_1 //.
by rewrite comp_polyD comp_polyC comp_polyX.
Qed.
(* I've departed from Chan thesis as it is not easy
to build non-constructive sets in Coq. So I turn
them into properties. Trying to sort things out
when doing the proof by contradiction
*)
(* This 𝒩 as a predicate *)
Definition is_iexp (R : ringType) (k s m : nat) :=
coprime m k /\ forall c, 0 < c <= s -> m ⋈[k] ('X + c%:R%:P : {poly R}).
Lemma is_iexp1 (R : ringType) k s : is_iexp R k s 1.
Proof.
split=> [|c cR]; first by rewrite /coprime gcd1n.
by apply: introspective1l.
Qed.
Lemma is_iexp_mul (R : comRingType) k s m1 m2 :
is_iexp R k s m1 -> is_iexp R k s m2 -> is_iexp R k s (m1 * m2).
Proof.
move=> [m1Ck Hm1] [m2Ck Hm2]; split; first by rewrite coprimeMl m1Ck.
by move=> c Hc; apply: introspecMl; [apply: Hm1 | apply: Hm2].
Qed.
Lemma is_iexp_X (R : comRingType) k s m n :
is_iexp R k s m -> is_iexp R k s (m ^ n).
Proof.
move=> mI; elim: n => [|n IH]; first by apply: is_iexp1.
by rewrite expnS; apply: is_iexp_mul.
Qed.
(* 103 *)
Lemma is_iexp_fin_char (F : finFieldType) k s p :
p \in [char F] -> coprime p k -> is_iexp F k s p.
Proof. by move=> pC pCk; split => // c _; apply: introspec_char. Qed.
Lemma is_iexp_fin_div (F : finFieldType) k s n p :
p \in [char F] -> coprime p k -> (p %| n)%N ->
is_iexp F k s n -> is_iexp F k s (n %/ p).
Proof.
move=> pC pCk pDn[nCk nI]; split => [|c cB].
by have := nCk; rewrite -{1}(divnK pDn) coprimeMl => /andP[].
apply: introspec_fin_div => //; first by rewrite coprime_sym.
by apply: nI.
Qed.
(* This is 𝒫 *)
Definition is_ipoly (R : ringType) (k s : nat) (p : {poly R}):=
forall m, is_iexp R k s m -> m ⋈[k] p.
Lemma is_ipoly1 (R : ringType) k s : is_ipoly k s (1 : {poly R}).
Proof. by move=> m _; apply: introspective1r. Qed.
Lemma is_ipoly_Xaddc (R : ringType) k s c :
0 <= c <= s -> is_ipoly k s ('X + c%:R%:P : {poly R}).
Proof.
rewrite leq_eqVlt; case: eqP => /= [<- _ m _|_ cB m [_]]; last by apply.
by rewrite addr0; apply: introspectiveX.
Qed.
(* This is 𝓜_k *)
Definition is_iexpm (R : ringType) (k s mk : nat) :=
exists2 m, mk = (m %% k)%N & is_iexp R k s m.
Inductive is_iexpm_spec
(R : ringType) (k s : nat) (mk : 'Z_k) : bool -> Prop :=
is_iexpm_spec_true :
forall (m : nat), (mk = m %% k :> nat)%N -> is_iexp R k s m ->
@is_iexpm_spec R k s mk true
| is_iexpm_spec_false :
(forall (m : nat), is_iexp R k s m -> (mk != m %% k :> nat)%N) ->
@is_iexpm_spec R k s mk false.
(* I've put Mk in {set 'Z_k} but its natural ambient is units_Zp! *)
Definition Mk_spec R s k (M : {set 'Z_k}) :=
(forall x, @is_iexpm_spec R k s x (x \in M)).
Lemma Mk_Cexists R k s :
classically (exists M : {set 'Z_k}, Mk_spec R s M).
Proof.
rewrite /Mk_spec.
suff : classically (exists M : {set 'Z_k},
forall x : 'Z_k, x \in (enum 'Z_k) -> uniq (enum 'Z_k) ->
is_iexpm_spec R s x (x \in M)).
apply: classic_bind => [[M HM]].
apply/classicP=> [] []; exists M => x.
apply: HM => //; first by rewrite mem_enum inE.
by apply: enum_uniq.
elim: (enum _) => [|a l] //.
by apply/classicP=> [] []; exists setT=> x; rewrite inE.
apply: classic_bind => [[M HM]].
have /classic_bind := @classic_pick nat
(fun m => (a = m %% k :> nat)%N /\ is_iexp R k s m).
apply => [] [[ma [maE maI]]|Ha].
apply/classicP => [] []; exists (a |: M) => x.
rewrite !inE => /orP[/eqP-> /= /andP[aNIi Ul]|xIl /= /andP[aNIl Ul]].
by rewrite eqxx; apply: is_iexpm_spec_true maI.
case: eqP => [xE|_ /=]; first by case/negP: aNIl; rewrite -xE.
by apply: HM.
apply/classicP => [] []; exists (M :\ a) => x.
rewrite !inE => /orP[/eqP-> /= /andP[aNIi Ul]|xIl /= /andP[aNIl Ul]].
rewrite eqxx; apply: is_iexpm_spec_false=> m Hm.
by apply/eqP=> eE; case: (Ha m).
rewrite (_ : x != a); first by by apply: HM.
by apply: contra aNIl => /eqP<-.
Qed.
Lemma is_iexpm1 (R : comRingType) k s (M : {set 'Z_k}) :
1 < k -> Mk_spec R s M -> 1 \in M.
Proof.
move=> k_gt1 MS; case: MS => // /(_ 1%N (is_iexp1 _ _ _)).
by rewrite modn_small ?eqxx.
Qed.
Lemma is_iexpm_mul (R : comRingType) k s (M : {set 'Z_k}) x y :
1 < k -> Mk_spec R s M -> x \in M -> y \in M -> (x * y) \in M.
Proof.
move=> k_gt1 MS.
(do 3 case: (MS) => //) => Hm m1 yE m1I m xE mI _ _.
have /eqP[] := Hm _ (is_iexp_mul mI m1I).
by rewrite -modnMml -xE -modnMmr -yE /= {3}Zp_cast.
Qed.
Lemma is_iexpm_X (R : comRingType) k s (M : {set 'Z_k}) x n :
1 < k -> Mk_spec R s M -> x \in M -> (x ^+ n) \in M.
Proof.
move=> k_gt1 MS xM.
elim: n => [|n IH]; first by apply: is_iexpm1.
by rewrite exprS; apply: is_iexpm_mul.
Qed.
(* 104 *)
Lemma is_iexpm_totient R k s (M : {set 'Z_k}) :
1 < k -> Mk_spec R s M -> #|M| <= totient k.
Proof.
move:M; case: k => [|[|k /= M _ HM]] //.
suff <-: #|[set i in 'I_k.+2 | coprime i k.+2]| = totient k.+2.
apply/subset_leq_card/subsetP=> x; rewrite !inE; case: HM => // m -> [].
by rewrite coprime_modl.
rewrite -sum1_card big_mkcond /=.
rewrite totient_count_coprime big_mkord.
by apply: eq_bigr => i _; rewrite inE coprime_sym.
Qed.
(* 104 *)
Lemma is_iexpm_order (R : comRingType) k s (M : {set 'Z_k}) n :
1 < k -> Mk_spec R s M -> is_iexp R k s n -> order_modn k n <= #|M|.
Proof.
move=> k_gt1 HMk nIN.
have kCn : coprime k n by case: nIN; rewrite coprime_sym.
rewrite order_modnE //; case: insubP => //= u nE uE.
rewrite -[#[_]%g](card_imset _ val_inj).
apply/subset_leq_card/subsetP => y /imsetP[z /cycleP[i ->] ->].
rewrite FinRing.val_unitX /= uE.
apply: is_iexpm_X (HMk) _ => //.
case: HMk => // /(_ _ nIN) /eqP[] /=.
by rewrite -val_Zp_nat.
Qed.
(* 105 *)
Lemma rmodn_trans {R : ringType} (p q h z : {poly R}) :
h \is monic -> z \is monic -> rdvdp h z ->
rmodp p z = rmodp q z -> rmodp p h = rmodp q h.
Proof.
move=> hM zM /(rdvdp_trans hM zM) => /(_ (p - q)).
rewrite /rdvdp !rmodpB // !subr_eq0 => H /eqP H1; apply/eqP.
by apply: H.
Qed.
(* 106 we reformulate it because we can't have order for poly directly *)
Lemma poly_order_rmod_inj (R : ringType) (h : {poly R}) k m n :
h \is monic -> 1 < size h -> 0 < k -> rdvdp h ('X^k - 1) ->
m < poly_order h 'X k -> n < poly_order h 'X k ->
rmodp 'X^m h = rmodp 'X^n h-> m = n.
Proof.
move=> hM hS k_gt0 hDxk.
wlog : m n / m <= n => [Hw |mLn] mLp nLp xmExn.
case: (leqP m n) => [/Hw|nLm]; first by apply.
by apply/sym_equal/Hw => //; apply: ltnW.
move: mLn; rewrite leq_eqVlt => /orP[/eqP//|mLn].
have xkE1 : rmodp 'X^k h = 1.
move: hDxk; rewrite /rdvdp rmodpB // [rmodp 1 _]rmodp_small.
by rewrite subr_eq0 => /eqP.
by rewrite size_polyC oner_neq0.
have [|o_gt0] := leqP (poly_order h 'X k) 0.
have kB : 0 < k <= k by rewrite k_gt0 leqnn.
by rewrite leqn0 => /eqP/poly_order_eq0_rmodp /(_ kB) /eqP[].
pose v := (poly_order h 'X k - n + m)%N.
have /poly_order_lt/eqP[] :
(0 < poly_order h 'X k - n + m < poly_order h 'X k )%nat.
rewrite (leq_trans _ (_ : 0 + m < _)) //; last first.
by rewrite ltn_add2r subn_gt0.
rewrite -{2}[poly_order _ _ _](@subnK m); last by apply: ltnW.
by rewrite ltn_add2r ltn_sub2l //.
rewrite exprD -rmodp_mulmr // xmExn rmodp_mulmr // -exprD subnK //.
by apply/eqP/poly_order_gt0_rmodp.
by apply/ltnW.
Qed.
(* 107 *)
Lemma Mk_root_Mk (R : comRingType) (h : {poly R}) k s
(M : {set 'Z_k}) (p q : {poly R}) n :
Mk_spec R s M ->
h \is monic -> 1 < size h -> 0 < k -> rdvdp h ('X^k - 1) ->
is_ipoly k s p -> is_ipoly k s q -> rmodp p h = rmodp q h ->
n \in M -> rmodp ((p - q) \Po 'X^n) h = 0.
Proof.
move=> HM hM hS k_gt0 hDxk pI qI phEqh nIM; apply/eqP.
case: HM nIM => // m nE mI _.
have xkM := monic_Xn_sub_1 R k_gt0.
have F : rmodp 'X^n ('X^k - 1) = rmodp 'X^m ('X^k - 1) :> {poly R}.
have F1 : rmodp 'X^k ('X^k - 1) = 1 :> {poly R}.
rewrite -{1}['X^k](subrK (1 : {poly R})) addrC rmodpD // rmodpp //.
by rewrite addr0 rmodp_small // size_polyC oner_eq0 /= size_Xn_sub_1.
rewrite (divn_eq m k) exprD mulnC exprM.
rewrite mulrC -rmodp_mulmr // -[in RHS]rmodpX // F1 expr1n.
by rewrite rmodp_mulmr // mulr1 nE.
rewrite comp_polyB rmodpB // subr_eq0; apply/eqP.
apply: etrans (_ : rmodp (p^+m) h = _).
apply: rmodn_trans hDxk _ => //.
rewrite -rmodp_compr // F rmodp_compr //.
by apply/esym/eqP/pI.
apply: etrans (_ : rmodp (q^+m) h = _).
by rewrite -rmodpX // phEqh rmodpX.
apply: esym.
apply: rmodn_trans hDxk _ => //.
rewrite -rmodp_compr // F rmodp_compr //.
by apply/esym/eqP/qI.
Qed.
(*108*)
Lemma Mk_rmodp_inj (R : fieldType) (h : {poly R}) k s
(M : {set 'Z_k}) (p q : {poly R}) :
Mk_spec R s M ->
monic_irreducible_poly h -> 0 < k -> rdvdp h ('X^k - 1) ->
poly_order h 'X k = k -> size p <= #|M| -> size q <= #|M| ->
is_ipoly k s p -> is_ipoly k s q -> rmodp p h = rmodp q h -> p = q.
Proof.
have [|M_gt0] := leqP #|M| 0.
rewrite leqn0 => /eqP->; rewrite !leqn0 !size_poly_eq0.
by move=> ? ? ? ? ? /eqP-> /eqP->.
move=> HMk hMI k_gt0 hDxk XoE pS qS pI qI /eqP.
have hS : 1 < size h by case: hMI; case.
have hI : irreducible_poly h by case: hMI.
have hM : h \is monic by case: hMI.
have hQE : mk_monic h = h by rewrite /mk_monic hS hM.
pose l : seq {poly %/ h with hMI} :=
map (fun i : 'I_ _ => (in_qpoly h 'X^i)) (enum M).
have Ul : uniq l.
apply/(uniqP 0) => i j; rewrite !inE size_map -cardE => Hi1 Hj1.
rewrite !(nth_map ord0) -?cardE // => /val_eqP /eqP /= HH.
suff : nth ord0 (enum M) i = nth ord0 (enum M) j.
by have /(uniqP ord0) := enum_uniq (pred_of_set M); apply=> //;
rewrite inE -cardE.
apply/val_inj => /=; move: HH.
apply: (poly_order_rmod_inj _ _ k_gt0); rewrite hQE ?XoE //.
- have: nth ord0 (enum M) i \in M by rewrite -mem_enum mem_nth // -cardE.
by case: HMk => // m -> _; rewrite ltn_mod //.
have: nth ord0 (enum M) j \in M by rewrite -mem_enum mem_nth // -cardE.
by case: HMk => // m -> _; rewrite ltn_mod.
rewrite -subr_eq0 -rmodpB // => /eqP => u.
apply/eqP; rewrite -subr_eq0; apply/eqP/(@map_fpoly_div_inj _ h).
rewrite map_poly0.
apply: roots_geq_poly_eq0 Ul _ => //; last first.
rewrite (@size_map_poly _ _ (GRing.RMorphism.clone _ _ _ (qfpoly_const hMI))).
rewrite size_map (leq_trans (size_add _ _)) //= size_opp.
by rewrite geq_max -cardE pS.
apply/allP=> i /mapP[j jI ->]; apply/eqP.
rewrite -in_qpoly_comp_horner //.
apply/val_inj => /=.
rewrite hQE //.
apply: Mk_root_Mk => //.
by apply/eqP; rewrite -subr_eq0 -rmodpB //; apply/eqP.
by rewrite -mem_enum.
Qed.
(* This is 𝒬_h *)
Definition is_iexph (R : ringType) (k s: nat) h ph :=
exists2 p : {poly R}, ph = in_qpoly h p & is_ipoly k s p.
Inductive is_iexph_spec
(R : ringType) (k s : nat) (h : {poly R}) ph : bool -> Prop :=
is_iexph_spec_true :
forall p, ph = in_qpoly h p -> is_ipoly k s p ->
@is_iexph_spec R k s h ph true
| is_iexph_spec_false :
(forall p, is_ipoly k s p -> ph != in_qpoly h p) ->
@is_iexph_spec R k s h ph false.
Definition Qh_spec (R : finRingType) k s (h :{poly R})
(M : {set {poly %/ h}}) :=
(forall x, @is_iexph_spec R k s h x (x \in M)).
Lemma Qh_Cexists (R : finRingType) k s (h : {poly R}) :
classically (exists M : {set {poly %/ h}}, Qh_spec k s M).
Proof.
rewrite /Qh_spec.
suff : classically (exists M : {set {poly %/ h}},
forall x : {poly %/ h}, x \in (enum {poly %/ h}) ->
uniq (enum {poly %/ h}) ->
is_iexph_spec k s x (x \in M)).
apply: classic_bind => [[M HM]].
apply/classicP=> [] []; exists M => x.
apply: HM; first by rewrite mem_enum inE.
by apply: enum_uniq.
elim: (enum _) => [|a l] //.
by apply/classicP=> [] []; exists setT=> x; rewrite inE.
apply: classic_bind => [[M HM]].
have /classic_bind := @classic_pick _
(fun p : {poly R} => a = in_qpoly h p /\ is_ipoly k s p).
apply => [] [[ma [maE maI]]|Ha].
apply/classicP => [] []; exists (a |: M) => x.
rewrite !inE => /orP[/eqP-> /= /andP[aNIi Ul]|xIl /= /andP[aNIl Ul]].
by rewrite eqxx; apply: is_iexph_spec_true maI.
case: eqP => [xE|_ /=]; first by case/negP: aNIl; rewrite -xE.
by apply: HM.
apply/classicP => [] []; exists (M :\ a) => x.
rewrite !inE => /orP[/eqP-> /= /andP[aNIi Ul]|xIl /= /andP[aNIl Ul]].
rewrite eqxx; apply: is_iexph_spec_false=> m Hm.
by apply/eqP=> eE; case: (Ha m).
rewrite (_ : x != a); first by by apply: HM.
by apply: contra aNIl => /eqP<-.
Qed.
(*109*)
Lemma lower_bound_card_Qh (F : finFieldType) (h : {poly F}) k s p
(M : {set 'Z_k}) (Q : {set {poly %/ h}}) :
Mk_spec F s M -> Qh_spec k s Q -> p \in [char F] -> 1 < order_modn k p ->
coprime k p -> monic_irreducible_poly h -> 1 < k -> rdvdp h ('X^k - 1) ->
poly_order h 'X k = k -> 0 < s < p ->
2 ^ minn s #|M| <= #|Q|.
Proof.
move=> HMk HQh pC pO_gt1 kCp hMI k_gt1 hDxk XoE sB.
have hQE : mk_monic h = h by rewrite /mk_monic !hMI.
rewrite -/{poly %/ h with hMI} in Q HQh *.
set t := minn _ _.
have Mk_gt1 : 1 < #|M|.
apply: leq_trans pO_gt1 _.
apply: is_iexpm_order (HMk) _ => //.
by apply: is_iexp_fin_char; rewrite // coprime_sym.
have t_gt0 : 0 < t.
by rewrite leq_min; case/andP: sB => -> _; rewrite ltnW.
have F1 (b : bool) c :
c <= s -> is_ipoly k s (('X + (c%:R)%:P :{poly F}) ^+ b).
case: b => cD; first by rewrite expr1; apply: is_ipoly_Xaddc.
by rewrite expr0; apply: is_ipoly1.
have F2 (b : bool) c :
c <= s -> size (('X + (c%:R)%:P : {poly F})%R ^+ b) <= 2.
case: b => cD; last by rewrite expr0 size_polyC oner_eq0.
rewrite (_ : 2%N = maxn(size ('X : {poly F})) (size ((c%:R)%:P : {poly F}))).
by rewrite expr1 size_add.
by rewrite size_polyX size_polyC; case: eqP.
pose m := ([ffun i : 'I_t.+1 => i == ord0] |:
[set i | (i : {ffun 'I_t.+1 -> bool}) ord0 == false]) :\
[ffun i : 'I_t.+1 => i != ord0].
have mTrue1 x : x \in m -> exists (i : 'I_t.+1), x i == false.
rewrite !inE => /andP[H /orP[/eqP->|xE]].
case: (t) t_gt0 x H => // t1 _ x H.
by exists (inZp 1); rewrite !ffunE /=; case: eqP.
by exists ord0.
have mTrue2 x : 1 < t -> x \in m -> exists (i : 'I_t.+1),
exists j, [/\ j != i, x i = false & x j = false].
rewrite /m; case: (t) t_gt0 x => // [] [|t1] // _ x _.
rewrite !inE => /andP[H /orP[/eqP->|/eqP xE]].
by exists (inZp 1); exists (inZp 2); rewrite !ffunE.
have [/existsP[i /andP[iE /eqP xiE]]|] :=
boolP [exists i, (i != ord0) && (x i == false)].
by exists ord0; exists i.
rewrite negb_exists => /forallP Hf.
case/eqP: H; apply/ffunP=> i; rewrite !ffunE.
case: eqP => [->|/eqP H] //.
case E : (x i) => //.
by case/negP: (Hf i); rewrite H // E.
have <- : #|m| = 2 ^ t.
rewrite cardsDS; last first.
by apply/subsetP=> j; rewrite !inE => /eqP->; rewrite ffunE eqxx orbT.
rewrite cardsU !cards1.
set u := #|_ :&: _|.
have /eqP->: u == 0%N.
rewrite cards_eq0; apply/eqP/setP=> i; rewrite !inE.
by apply/idP => /andP[/eqP->]; rewrite ffunE eqxx.
rewrite subn0 addnC addnK.
have <- : [set [ffun i => if unlift ord0 i is Some v then f v else false]
| f : {ffun 'I_t -> bool}] =
[set i | (i : {ffun 'I_t.+1 -> bool}) ord0 == false].
apply/setP=> f; rewrite !inE; apply/imsetP/idP=>[[g _ ->]|/eqP fE].
by rewrite ffunE unlift_none.
exists [ffun i => f (fintype.lift ord0 i)]; first by rewrite inE.
apply/ffunP=> j; rewrite ffunE; case: unliftP => [v ->|->] //.
by rewrite ffunE.
rewrite card_imset; first by rewrite card_ffun card_bool card_ord.
move=> f g H; apply/ffunP=> i.
have := (congr1 (fun f : {ffun _ -> _} => f (fintype.lift ord0 i)) H).
by rewrite !ffunE liftK.
pose f := fun (b : {ffun 'I_t.+1 -> bool}) (i : 'I_t.+1) =>
('X + (i%:R)%:P : {poly F}) ^+ b i.
pose g b : {poly %/ h}:= in_qpoly h (\prod_(i < t.+1) f b i).
have F3 b : b \in m -> size (\prod_(i < t.+1) f b i)%R <= #|M|.
have vE i : #|((fun i0 : 'I_t.+1 => i0 != i) : pred _)| = t.
set v := #|_|; rewrite -[t]/(t.+1.-1) -[t.+1]card_ord.
rewrite -cardsT [in RHS](cardsD1 i) inE /=.
by apply: eq_card => j; rewrite !inE andbT.
move: t_gt0; rewrite leq_eqVlt => /orP[/eqP tE1 /mTrue1 [i /eqP iE]| t_gt].
rewrite (bigD1 i) //= {1}/f; rewrite iE expr0 mul1r.
apply: leq_trans (size_prod_leq _ _) _ => /=.
rewrite vE leq_subLR.
rewrite (leq_ltn_trans _ (_ : (\sum_(j < t.+1 | j != i) 2) < _)) //.
apply: leq_sum => j _; apply: F2.
rewrite -ltnS; apply: leq_trans (ltn_ord j) _.
by rewrite ltnS geq_minl.
by rewrite sum_nat_const [#|_|]vE muln2 -addnn ltn_add2l -tE1.
move=> bM; have [i [j [jDi biE bjE]]] := mTrue2 _ t_gt bM.
rewrite (bigD1 i) //= {1}/f; rewrite biE expr0 mul1r.
rewrite (bigD1 j) //= {1}/f; rewrite bjE expr0 mul1r.
apply: leq_trans (size_prod_leq _ _) _ => /=.
set v := #|_|.
have vE1 : v = t.-1.
rewrite -[t]/(t.+1.-1) -[t.+1]card_ord.
rewrite -cardsT [in RHS](cardsD1 i) inE /=.
rewrite [in RHS](cardsD1 j) !inE /= jDi /=.
by apply: eq_card => l; rewrite !inE /= andbT andbC.
rewrite vE1 leq_subLR.
rewrite (leq_ltn_trans _ (_ : (\sum_(l < t.+1 | (l != i) && (l != j)) 2)
< _)) //.
apply: leq_sum => l _; apply: F2.
rewrite -ltnS; apply: leq_trans (ltn_ord l) _.
by rewrite ltnS geq_minl.
rewrite sum_nat_const [#|_|]vE1 muln2 -addnn ltn_add2l.
by rewrite prednK ?geq_minr // ltnW.
have F4 b : b \in m -> is_ipoly k s (\prod_(i < t.+1) f b i).
move=> bIm m1 Hm1.
elim/big_rec: _ => [|i x _ xI]; first by apply: introspective1r.
apply: introspecMr => //.
rewrite /f; case: (b i); last by rewrite expr0; apply: introspective1r.
rewrite expr1; case: (i : nat) (ltn_ord i) => [_|i1].
by rewrite addr0; apply: introspectiveX.
rewrite ltnS => i1Lt.
case: Hm1=> _; apply=> /=; apply: leq_trans i1Lt _.
by rewrite geq_minl.
suff /card_in_imset<- : {in m &, injective g}.
rewrite subset_leqif_cards //; apply/subsetP => i /imsetP[/= b bIm ->].
by case: HQh => // /(_ (\prod_(i < t.+1) f b i) (F4 _ bIm)) /eqP[].
move=> m1 m2 m1I m2I /val_eqP/eqP/= H.
have F5 b (x : 'I_ _) : b \in m ->
(\prod_(i < t.+1) f b i).[-(x%:R)] == 0 = (b x).
move=> bIm; rewrite horner_prod.
apply/GRing.prodf_eq0/idP=> /= [[j _]|bxE]; last first.
by exists x=> //; rewrite /f bxE expr1 !hornerE addrC subrr.
rewrite /f horner_exp !hornerE; case: (boolP (b j)) => bjE; last first.
by rewrite expr0 oner_eq0.
rewrite expr1 addrC.
rewrite {2}/is_true -{}bjE.
wlog: x j / x <= j => [Hw|].
case: (leqP x j)=> [xLj|jLx]; first by apply: Hw.
rewrite -oppr_eq0 opprB => xjE0.
by apply/esym/Hw => //; apply: ltnW.
rewrite leq_eqVlt => /orP[/val_eqP->//|xLhj].
rewrite -natrB 1?ltnW // -(dvdn_charf pC).
rewrite gtnNdvd //; first by rewrite subn_gt0.
apply: leq_ltn_trans (leq_subr _ _) _.
apply: leq_trans (ltn_ord _) _.
apply: leq_ltn_trans (geq_minl _ _) _.
by case/andP: sB.
suff : \prod_(i < t.+1) f m1 i = \prod_(i < t.+1) f m2 i.
by move=> Hprod; apply/ffunP=> i; rewrite -F5 // Hprod F5.
apply: Mk_rmodp_inj (F3 _ m1I) (F3 _ m2I) (F4 _ m1I) (F4 _ m2I) H => //.
- by rewrite hQE.
- by rewrite ltnW.
- by rewrite hQE.
by rewrite hQE.
Qed.
(* 110 *)
Lemma exp_Mk_upper_bound (R : comRingType) k s n a (M : {set 'Z_k}) :
Mk_spec R s M -> 1 < #|M| ->
1 < k -> 1 < n -> isnot_2power n ->
a = up_log 2 n ^ 2 -> a <= order_modn k n ->
s = (sqrtn (totient k) * (up_log 2 n))%N ->
is_iexp R k s n ->
n ^ (sqrtn #|M|) < 2 ^ (minn s #|M|).
Proof.
move=> HMk Mk_gt1 k_gt1 m_g1 nNP aE aLo sE nIN.
set j := order_modn k n in aLo.
set m := up_log 2 n in aE sE.
have F1 : j <= #|M| by apply: is_iexpm_order.
have F2 : #|M| <= totient k by apply: is_iexpm_totient.
have F3 : m ^ 2 <= j by move: aLo; rewrite aE.
apply: leq_trans (_ : (2 ^ m) ^ sqrtn (#|M|) <= _).
rewrite ltn_exp2r; last first.
by rewrite sqrtn_gt0 (leq_trans _ (_ : 2 <= _)).
by have := up_logP n (isT : 1 < 2); rewrite leq_eqVlt (negPf nNP).
case: (leqP s #|M|) => [sLM|MLs].
by rewrite -expnM leq_exp2l // sE mulnC leq_mul2r // orbC leq_sqrtn.
rewrite -expnM leq_exp2l //.
apply: leq_trans (_ : (sqrtn #|M|) ^ 2 <= _); last first.
by have /andP[] := sqrtn_bound #|M|.
rewrite expnS expn1 leq_mul2r // orbC.
rewrite (leq_trans _ (_ : sqrtn j <= _)) //; last by apply: leq_sqrtn.
by rewrite -[m]sqrnK leq_sqrtn .
Qed.
Definition Nbar (p q m : nat) : {set 'I_((p * q) ^ m).+1} :=
[set inZp (p ^ ij.1 * q ^ ij.2) | ij: 'I_m.+1 * 'I_m.+1].
(* 111 *)
(** As Nbar is defined slightly differently, this is the dual version of **)
(** 111 for our version **)
Lemma NbarP (p q m : nat) (x : 'I_ _) :
1 < p -> 1 < q ->
reflect (exists (ij : 'I_m.+1 * 'I_m.+1) , x = (p ^ ij.1 * q ^ ij.2)%N :> nat)
(x \in Nbar p q m).
Proof.
move=> p_gt1 q_gt1.
apply(iffP imsetP) => [[[i j _ -> /=]]|[[i j ijE]]].
by exists (i, j);
rewrite modn_small // ltnS expnMn leq_mul // leq_exp2l // -ltnS.
exists (i, j) => //; apply/val_inj => /=.
by rewrite modn_small // ltnS expnMn leq_mul // leq_exp2l // -ltnS.
Qed.
(* 112 *)
Lemma is_iexp_root (F : fieldType) (h : {poly F}) k s m n p :
0 < k -> monic_irreducible_poly h -> rdvdp h ('X^k - 1) ->
is_iexp F k s m -> is_iexp F k s n -> n = m %[mod k] ->
is_ipoly k s p -> in_qpoly h (('X^n - 'X^m) \Po p) = 0.
Proof.
move=> k_gt0 hMI hDxk1 mI nI mMn pP.
apply/val_inj; rewrite /= /mk_monic !hMI //= -[RHS](rmod0p h).
pose z : {poly F}:= 'X^k - 1.
have zM : z \is monic by apply: monic_Xn_sub_1.
apply: rmodn_trans hDxk1 _; rewrite ?hMI -/z // rmod0p.
rewrite comp_polyB !comp_Xn_poly rmodpB //.
apply/eqP; rewrite subr_eq0; apply/eqP.
have F0 : rmodp 'X^k z = 1.
rewrite -['X^k](subrK 1) rmodpD // rmodpp // add0r rmodp_small //.
by rewrite size_polyC size_Xn_sub_1 ?oner_eq0.
have F1 : rmodp 'X^n z = rmodp 'X^m z.
rewrite (divn_eq n k) (divn_eq m k) !exprD mMn.
rewrite ![(_ * k)%N]mulnC !exprM ![_ * 'X^(_ %% _)]mulrC.
rewrite -rmodp_mulmr // -rmodpX // F0 expr1n rmodp_mulmr // mulr1.
rewrite -rmodp_mulmr // -[in RHS] rmodpX //.
by rewrite F0 expr1n rmodp_mulmr // mulr1.
have F2 : rmodp (p ^+ n) z = rmodp (p \Po 'X^n) z by apply/eqP/pP.
have F3 : rmodp (p ^+ m) z = rmodp (p \Po 'X^m) z by apply/eqP/pP.
have F4 : rmodp (p \Po 'X^m) z = rmodp (p \Po 'X^n) z.
by rewrite -rmodp_compr // -F1 rmodp_compr.
by rewrite F2 -F4 -F3.
Qed.
(* 113 *)
(* in order to be able to talk about Qh I need to limit this theorem to
finField *)
Lemma is_iexp_inj (F : finFieldType) (h : {poly F}) k s
(M : {set 'Z_k}) (Q : {set {poly %/ h}}) p q :
Mk_spec F s M -> Qh_spec k s Q ->
1 < k -> monic_irreducible_poly h -> rdvdp h ('X^k - 1) ->
1 < p -> is_iexp F k s p -> (1 < q) -> is_iexp F k s q ->
(p * q) ^ sqrtn #|M| < #|Q| ->
{in Nbar p q (sqrtn #|M|) &, injective (fun i : 'I_ _ => inZp i : 'Z_k)}.
Proof.
move=> hMK hQh k_gt1 hMI hDxk1 p_gt1 pIN q_gt1 qIN pqLqh i j iIN jIN.
move=> /(congr1 val); rewrite /= [X in _ = _ %[mod X]]Zp_cast // => imEjm.
have k_gt0 : 0 < k by rewrite -ltnS ltnW.
pose r := map_poly (qfpoly_const hMI) ('X^i - 'X^j).
suff : r == 0.
rewrite /r rmorphB /= subr_eq0 => /eqP/map_poly_div_inj.
move=> /(congr1 (size : {poly F} -> nat)).
by rewrite !size_polyXn => [] [] /eqP /val_eqP.
apply/eqP/(@roots_geq_poly_eq0
(GRing.IntegralDomain.clone _ {poly %/ h with hMI}) _ (enum Q)).
- apply/allP => /= x.
rewrite mem_enum; case: hQh => // p1 -> p1I _.
apply/eqP; rewrite -in_qpoly_comp_horner.
apply: is_iexp_root p1I => //.
case/imsetP: jIN => [[i1 j1] _ -> /=].
rewrite modn_small.
by apply: is_iexp_mul; apply: is_iexp_X.
by rewrite ltnS expnMn leq_mul // leq_exp2l // -ltnS.
case/imsetP: iIN => [[i1 j1] _ -> /=].
rewrite modn_small.
by apply: is_iexp_mul; apply: is_iexp_X.
by rewrite ltnS expnMn leq_mul // leq_exp2l // -ltnS.
- by apply: enum_uniq.
rewrite -cardE.
apply: leq_trans pqLqh.
rewrite /r rmorphB /= !map_polyXn.
apply: leq_trans (size_add _ _) _.
by rewrite size_opp !size_polyXn geq_max !ltn_ord.
Qed.
Definition poly_intro_range (R : ringType) k n s :=
forall c, 0 < c <= s->
rmodp (('X + c%:R%:P)^+n) ('X^k - 1 : {poly R}) =
rmodp ('X^n + c%:R%:P) ('X^k - 1).
Definition aks_criteria (R : ringType) n k :=
[/\ 0 < n, 0 < k,
(forall p, p \in [char R] -> [/\ 1 < order_modn k p, (p %| n)%N & k < p]),
up_log 2 n ^ 2 <= order_modn k n &
poly_intro_range R k n (sqrtn (totient k) * up_log 2 n)
].
Lemma card_Nbar p q m : prime p -> 1 < q -> ~ is_power q p ->
#|Nbar p q m| = m.+1 ^ 2.
Proof.
move=> pP q_gt1 pCq.
have p_gt1 := prime_gt1 pP.
rewrite card_imset=> [|/= [i1 j1] [i2 j2] /(congr1 val)].
by rewrite card_prod card_ord expnS expn1.
rewrite /= !modn_small //; last 2 first.
- by rewrite ltnS expnMn leq_mul // leq_exp2l // -ltnS.
- by rewrite ltnS expnMn leq_mul // leq_exp2l // -ltnS.
wlog i1Li2 : i1 i2 j1 j2 / i1 <= i2 => H.
case: (leqP i1 i2) => [i1Li2|i2Li1]; first by apply H.
by move=> Hi; apply/sym_equal/H; rewrite 1?ltnW.
suff [H1 H2] : (i1 : nat, j1 : nat) = (i2 : nat, j2 : nat).
by congr (_, _); apply: val_inj.
move: (i1Li2) H; rewrite leq_eqVlt => /orP[/eqP<-|i1LEi2 /eqP].
move/eqP; rewrite eqn_pmul2l; last by rewrite expn_gt0 ltnW.
by rewrite eqn_exp2l => // /eqP<-.
rewrite -{1}(subnK i1Li2) addnC expnD -mulnA eqn_pmul2l; last first.
by rewrite expn_gt0 prime_gt0.
case: (leqP j2 j1) => [j1Lj2|j2Lj1].
rewrite -{1}(subnK j1Lj2) expnD eqn_pmul2r; last by rewrite expn_gt0 ltnW.
move: j1Lj2; rewrite leq_eqVlt => /orP[/eqP<-|].
rewrite subnn expn0 eq_sym.
move: i1LEi2; rewrite -subn_gt0; case: (_ - _)%N=> // k _.
by rewrite expnS muln_eq1; case: (p) p_gt1 => // [] [].
rewrite -subn_gt0 => j1j2_gt0 /eqP qE.
case: pCq; apply: prime_is_power_exp j1j2_gt0 _ => //.
by rewrite qE is_power_exp.
have j1LEj2 : j1 <= j2 by rewrite ltnW.
rewrite -[_ ^ _]mul1n -{1}(subnK j1LEj2) expnD mulnA.
rewrite eqn_pmul2r; last by rewrite expn_gt0 ltnW.
move: i1LEi2; rewrite -subn_gt0; case: (_ - _)%N => // k _.
by rewrite expnS -mulnA eq_sym muln_eq1; case: (p) p_gt1 => // [] [].
Qed.
(* 96 *)
Lemma cyclotomic_special_order k p :
(prime p -> 0 < k -> 1 < order_modn k p ->
exists h : {poly 'F_p}, [/\ monic_irreducible_poly h, (h %| 'X^k - 1)%R,
size h = (order_modn k p).+1 & poly_order h 'X k = k]
)%N.
Proof.
set d := order_modn _ _.
move=> pP k_gt0 d_gt1.
have p_gt1 := prime_gt1 pP.
have k_gt1 := order_modn_gt1 d_gt1.
have kCp := order_modn_coprime d_gt1.
have d_gt0 : 0 < d by apply: leq_trans d_gt1.
have /= [L LC] := Fp_splittingField pP d_gt0.
set m := p ^ d in LC.
have m_gt1: m > 1 by rewrite (ltn_exp2l 0) ?prime_gt1.
have m_gt0 := ltnW m_gt1; have m1_gt0: m.-1 > 0 by rewrite -ltnS prednK.
pose Fm := FinFieldExtType L.
have /hasP[x _ xE] :
has (m.-1).-primitive_root [seq val i | i <-
enum (Finite.clone _ {unit Fm})].
apply: cyclic.has_prim_root => //.
- apply/allP => i /mapP[/= x _ -> /=].
apply/unity_rootP => /=.
rewrite -FinRing.val_unitX -(_ : #|[set : {unit Fm}]%g| = m.-1).
by rewrite cyclic.expg_cardG ?inE.
by rewrite card_finField_unit LC.
- rewrite map_inj_uniq; first by apply: enum_uniq.
by apply: val_inj.
by rewrite size_map -cardE -cardsT card_finField_unit LC.
have kDm1 : (k %| m.-1)%N by rewrite -subn1 -eqn_mod_dvd // order_modn_exp.
have mkDm1 : (m.-1 %/ k %| m.-1)%N.
by apply/dvdnP; exists k; rewrite mulnC divnK.
pose z := x ^+ (m.-1 %/ k).
have kPr : k.-primitive_root z.
rewrite {1}(_ : k = m.-1 %/ gcdn (m.-1 %/ k) m.-1)%N //.
by apply: exp_prim_root.
by rewrite (gcdn_idPl mkDm1) divnA // mulnC mulnK.
have /polyOver1P[h hE] := minPolyOver 1 z.
have g1L : galois 1%AS {: L}%AS.
by apply: finField_galois (sub1v _).
pose g := ('Gal({: L}%AS /<<1; z>>))%G.
pose E := <<1; z>>%VS.
pose e := \dim E.
have dE : d = \dim {: L}.
have /eqP := @card_vspace _ Fm _ {:L}.
by rewrite card_vspacef LC card_Fp // eqn_exp2l // => /eqP.
have eDd : (e %| d)%N.
by rewrite dE; apply/field_dimS/subvf.
have kDpe : (k %| (p ^ e).-1)%N.
rewrite (prim_order_dvd kPr) -subn1 expfB ?expr1; last first.
by rewrite -(exp1n e) ltn_exp2r ?prime_gt1 // adim_gt0.
have: z \in E by apply: memv_adjoin.
rewrite Fermat's_little_theorem -/E card_Fp -/e // => /eqP->.
rewrite divff //.
apply/eqP=> zE0; have /eqP := prim_expr_order kPr.
by rewrite zE0 expr0n eqn0Ngt k_gt0 eq_sym oner_eq0.
have peE1 : p ^ e = 1 %[mod k].
rewrite -[_ ^ _]prednK ?expn_gt0 ?prime_gt0 //.
by rewrite -addn1 -modnDm (eqP kDpe) add0n modn_mod.
have hS : size h = d.+1.
have := size_minPoly 1%AS z.
rewrite /adjoin_degree dimv1 divn1 -/E -/e.
rewrite hE size_map_poly prednK ?adim_gt0 // => ->.
congr (_.+1); apply/eqP; rewrite eqn_dvd.
apply/andP; split.
by rewrite dE; apply/field_dimS/subvf.
rewrite /d order_modnE //; case: insubP => [u|/negP[]]; rewrite !unitZpE //=.
move=> _ uE.
rewrite cyclic.order_dvdn.
apply/eqP/val_eqP.
rewrite FinRing.val_unitX /= uE.
rewrite -natrX.
by rewrite -(Zp_nat_mod k_gt1) peE1 modn_small //.
have minD : minPoly 1%AS z %| 'X^k - 1.
apply: minPoly_dvdp.
Time by rewrite !rpredB //= ?rpredX //= ?polyOverX //= ?rpred1 //=.
(* by rewrite !(rpredB, rpredX, polyOverX, rpred1). *)
rewrite rootE !hornerE -exprM divnK //.
by rewrite prim_expr_order // subrr.
have hD : h %| 'X^k - 1.
move: minD.
have ->: 'X^k - 1 = map_poly (in_alg L) ('X^k - 1).
by rewrite raddfB /= rmorphXn /= map_polyX /= rmorph1.
by rewrite hE dvdp_map.
have hM : h \is monic.
have := monic_minPoly 1 z.
by rewrite hE map_monic.
exists h; split => //.
- split => //.
split=> [|p1 Sp1 p1Dh]; first by rewrite hS.
pose fp1 := map_poly (in_alg L) p1.
have /(minPoly_irr (alg_polyOver _ _))/orP[] :
fp1 %| minPoly 1%AS z by rewrite hE dvdp_map.
by rewrite hE eqp_map.
rewrite -(_ : map_poly (in_alg L) 1 = 1).
by rewrite eqp_map -size_poly_eq1 (negPf Sp1).
by rewrite map_polyC /= scale1r.
apply: poly_orderE=> [||k1 k1_gt0 /eqP]; first by rewrite k_gt0 leqnn.
apply/eqP; rewrite -[1](@rmodp_small _ _ h) ?size_poly1 ?hS //.
rewrite -subr_eq0 -rmodpB //.
by rewrite -[_ == 0]/(rdvdp h ('X^k - 1)) -dvdpE.
rewrite -[1](@rmodp_small _ _ h) ?size_poly1 ?hS //.
rewrite -subr_eq0 -rmodpB //.
rewrite -[_ == 0]/(rdvdp h ('X^k1 - 1)) -dvdpE => hDk1.
apply: dvdn_leq => //.
suff: minPoly 1%AS z %| 'X^k1 - 1.
move=> Hk1.
rewrite (prim_order_dvd kPr).
have : ('X^k1 - 1).[z] == 0.
by case/dvdpP: Hk1 => r ->; rewrite hornerE minPolyxx mulr0.
by rewrite !hornerE subr_eq0.
rewrite hE.
have ->: 'X^k1 - 1 = map_poly (in_alg L) ('X^k1 - 1).
by rewrite raddfB /= rmorphXn /= map_polyX /= rmorph1.
by rewrite dvdp_map.
Time Qed.
(*115 *)
Lemma main_aks p n k (F := (FinRing.Ring.clone _ 'F_p)) :
prime p -> aks_criteria F n k -> is_power n p.
Proof.
move=> pP; have p_gt1 := prime_gt1 pP.
have pC : p \in [char F] by apply: char_Fp.
pose a := (up_log 2 n) ^ 2; pose s := (sqrtn (totient k) * up_log 2 n)%N.
move => [n_gt0 k_gt0 /(_ p pC) [pO_gt1 pDn kLp lnLnO Hr]].
have k_gt1 : 1 < k by apply: order_modn_gt1 pO_gt1.
have := dvdn_leq n_gt0 pDn.
rewrite leq_eqVlt => /orP[/eqP<-|pLn]; first by rewrite is_power_id.
have [/eqP nE|/negP nis2p] := boolP (is_2power n).
move: pDn; rewrite nE.
rewrite Euclid_dvdX // => /andP[/prime_nt_dvdP->] //.
by move=> _; apply: is_power_exp.
by case: (p) pP => // [] // [].
have n_gt1 : 1 < n.
apply: leq_trans (prime_gt1 pP) _.
by apply: dvdn_leq.
have n_gt2 : 2 < n by case: (n) n_gt1 nis2p => [|[|[|]]].
have kCn : coprime k n.
apply: order_modn_coprime.
apply: leq_trans lnLnO.
rewrite (@ltn_exp2r 1 _ 2) //.
by apply: (@leq_up_log 2 3).
have kCp : coprime k p by apply: order_modn_coprime.
have nI : is_iexp (GRing.Ring.clone _ 'F_p) k s n.
split => [|c cB]; first by rewrite coprime_sym.
apply/eqP.
rewrite comp_polyD comp_polyC comp_polyX.
by apply: Hr.
have [h [hMI hDxk1 jS hO]]:= cyclotomic_special_order pP k_gt0 pO_gt1.
have [//|/negP nP] := boolP (is_power n p).
have /classicP[] := @Mk_Cexists F k s.
move=> [M hMk].
have /classicP[] := @Qh_Cexists F k s h.
move=> [Q hQh].
pose t := #|M|.
have t_gt1 : 1 < t.
apply: leq_trans pO_gt1 _.
apply: is_iexpm_order (hMk) _ => //.
apply: is_iexp_fin_char; first by apply: char_Fp.
by rewrite coprime_sym.
have nLst : n ^ sqrtn t < 2 ^ minn s t.
apply: exp_Mk_upper_bound hMk _ _ _ _ _ _ _ _ => //.
by apply/negP.
have stLQ : 2 ^ minn s t <= #|Q|.
apply: (@lower_bound_card_Qh _ _ _ _ p) => //; first by rewrite -dvdpE.
rewrite muln_gt0 sqrtn_gt0 totient_gt0 k_gt0.
rewrite (@leq_up_log 2 2) //=.
apply: leq_trans (kLp).
rewrite ltnS.
apply: leq_trans (totient_leq _).
have /andP[/(leq_trans _)->//] := sqrtn_bound (totient k).
rewrite expnS expn1 leq_mul2l -(sqrnK (up_log 2 n)).
rewrite leq_sqrtn ?orbT //.
by apply: leq_trans (leq_order_totient n _).
pose q := (n %/ p)%N.
have nE : n = (q * p)%N.
by rewrite [n](divn_eq _ p) (eqP pDn) addn0.
have q_gt1 : 1 < q.
case: leqP => //.
move: n_gt1 nP; rewrite nE.
by case: (q) => [|[|]] // _ []; rewrite mul1n is_power_id.
have pI : is_iexp F k s p by apply: is_iexp_fin_char; rewrite 1? coprime_sym.
have qI : is_iexp F k s q by apply: is_iexp_fin_div; rewrite 1? coprime_sym.
pose N1 := Nbar p q (sqrtn t).
pose f := fun i : 'I_((p * q) ^ sqrtn t).+1 => inZp i : 'Z_k.
have : #|f @: N1| <= t.
apply/subset_leq_card/subsetP => x /imsetP[y /imsetP[/= [i1 j1 _]-> -> /=]].
set m := (_ ^ _ * _)%N.
have mI : is_iexp F k s m.
by apply: is_iexp_mul; apply: is_iexp_X.
case: hMk => //= /(_ _ mI)/eqP[].
rewrite /= Zp_cast // [(m %% _)%N]modn_small //.
by rewrite ltnS expnMn leq_mul // leq_exp2l // -ltnS.
rewrite leqNgt=> /negP[].
rewrite card_in_imset; last first.
apply: (is_iexp_inj hMk hQh) => //; first by rewrite -dvdpE.
rewrite mulnC -nE.
by apply: leq_trans stLQ.
rewrite card_Nbar //; last first.
move=> H; case: nP.
by rewrite nE (eqP H) -expnSr is_power_exp.
by have /andP[] := sqrtn_bound t.
Qed.
(******************************************************************************)
(* Now that we have the main theorem we can start building the algorithm *)
(******************************************************************************)
(******************************************************************************)
(* Power Free *)
(******************************************************************************)
Fixpoint power_free (n : nat) k :=
if k is k1.+1 then
if k1 is _.+1 then
if is_rootn k n then false
else power_free n k1
else (1 < n)
else (1 < n).
Lemma power_freeSS n k :
power_free n k.+2 = if is_rootn k.+2 n then false else power_free n k.+1.
Proof. by []. Qed.
Compute (fun n => power_free n (up_log 2 n)) 128%N.
Lemma power_freePn n :
~~ power_free n (up_log 2 n) ->
exists m, exists2 k, 1 < k & n = m ^ k.
Proof.
elim: up_log => [|[|k] IH].
- case: n => [|[|n]] //= _; first by exists 0%N; exists 2%N.
by exists 1%N; exists 2%N.
- case: {IH}n => [|[|n]] //= _; first by exists 0%N; exists 2%N.
by exists 1%N; exists 2%N.