forked from math-comp/math-comp
-
Notifications
You must be signed in to change notification settings - Fork 0
/
prime.v
1440 lines (1214 loc) · 57.1 KB
/
prime.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
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
From mathcomp Require Import fintype div bigop.
(******************************************************************************)
(* This file contains the definitions of: *)
(* prime p <=> p is a prime. *)
(* primes m == the sorted list of prime divisors of m > 1, else [::]. *)
(* pfactor p e == the value p ^ e of a prime factor (p, e). *)
(* NumFactor f == print version of a prime factor, converting the prime *)
(* component to a Num (which can print large values). *)
(* prime_decomp m == the list of prime factors of m > 1, sorted by primes. *)
(* logn p m == the e such that (p ^ e) \in prime_decomp n, else 0. *)
(* trunc_log p m == the largest e such that p ^ e <= m, or 0 if p or m is 0. *)
(* pdiv n == the smallest prime divisor of n > 1, else 1. *)
(* max_pdiv n == the largest prime divisor of n > 1, else 1. *)
(* divisors m == the sorted list of divisors of m > 0, else [::]. *)
(* totient n == the Euler totient (#|{i < n | i and n coprime}|). *)
(* nat_pred == the type of explicit collective nat predicates. *)
(* := simpl_pred nat. *)
(* -> We allow the coercion nat >-> nat_pred, interpreting p as pred1 p. *)
(* -> We define a predType for nat_pred, enabling the notation p \in pi. *)
(* -> We don't have nat_pred >-> pred, which would imply nat >-> Funclass. *)
(* pi^' == the complement of pi : nat_pred, i.e., the nat_pred such *)
(* that (p \in pi^') = (p \notin pi). *)
(* \pi(n) == the set of prime divisors of n, i.e., the nat_pred such *)
(* that (p \in \pi(n)) = (p \in primes n). *)
(* \pi(A) == the set of primes of #|A|, with A a collective predicate *)
(* over a finite Type. *)
(* -> The notation \pi(A) is implemented with a collapsible Coercion. The *)
(* type of A must coerce to finpred_sort (e.g., by coercing to {set T}) *)
(* and not merely implement the predType interface (as seq T does). *)
(* -> The expression #|A| will only appear in \pi(A) after simplification *)
(* collapses the coercion, so it is advisable to do so early on. *)
(* pi.-nat n <=> n > 0 and all prime divisors of n are in pi. *)
(* n`_pi == the pi-part of n -- the largest pi.-nat divisor of n. *)
(* := \prod_(0 <= p < n.+1 | p \in pi) p ^ logn p n. *)
(* -> The nat >-> nat_pred coercion lets us write p.-nat n and n`_p. *)
(* In addition to the lemmas relevant to these definitions, this file also *)
(* contains the dvdn_sum lemma, so that bigop.v doesn't depend on div.v. *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* The complexity of any arithmetic operation with the Peano representation *)
(* is pretty dreadful, so using algorithms for "harder" problems such as *)
(* factoring, that are geared for efficient artihmetic leads to dismal *)
(* performance -- it takes a significant time, for instance, to compute the *)
(* divisors of just a two-digit number. On the other hand, for Peano *)
(* integers, prime factoring (and testing) is linear-time with a small *)
(* constant factor -- indeed, the same as converting in and out of a binary *)
(* representation. This is implemented by the code below, which is then *)
(* used to give the "standard" definitions of prime, primes, and divisors, *)
(* which can then be used casually in proofs with moderately-sized numeric *)
(* values (indeed, the code here performs well for up to 6-digit numbers). *)
Module Import PrimeDecompAux.
(* We start with faster mod-2 and 2-valuation functions. *)
Fixpoint edivn2 q r := if r is r'.+2 then edivn2 q.+1 r' else (q, r).
Lemma edivn2P n : edivn_spec n 2 (edivn2 0 n).
Proof.
rewrite -[n]odd_double_half addnC -{1}[n./2]addn0 -{1}mul2n mulnC.
elim: n./2 {1 4}0 => [|r IHr] q; first by case (odd n) => /=.
by rewrite addSnnS; apply: IHr.
Qed.
Fixpoint elogn2 e q r {struct q} :=
match q, r with
| 0, _ | _, 0 => (e, q)
| q'.+1, 1 => elogn2 e.+1 q' q'
| q'.+1, r'.+2 => elogn2 e q' r'
end.
Variant elogn2_spec n : nat * nat -> Type :=
Elogn2Spec e m of n = 2 ^ e * m.*2.+1 : elogn2_spec n (e, m).
Lemma elogn2P n : elogn2_spec n.+1 (elogn2 0 n n).
Proof.
rewrite -{1}[n.+1]mul1n -[1]/(2 ^ 0) -{1}(addKn n n) addnn.
elim: n {1 4 6}n {2 3}0 (leqnn n) => [|q IHq] [|[|r]] e //=; last first.
by move/ltnW; apply: IHq.
clear 1; rewrite subn1 -[_.-1.+1]doubleS -mul2n mulnA -expnSr.
by rewrite -{1}(addKn q q) addnn; apply: IHq.
Qed.
Definition ifnz T n (x y : T) := if n is 0 then y else x.
Variant ifnz_spec T n (x y : T) : T -> Type :=
| IfnzPos of n > 0 : ifnz_spec n x y x
| IfnzZero of n = 0 : ifnz_spec n x y y.
Lemma ifnzP T n (x y : T) : ifnz_spec n x y (ifnz n x y).
Proof. by case: n => [|n]; [right | left]. Qed.
(* The list of divisors and the Euler function are computed directly from *)
(* the decomposition, using a merge_sort variant sort of the divisor list. *)
Definition add_divisors f divs :=
let: (p, e) := f in
let add1 divs' := merge leq (map (NatTrec.mul p) divs') divs in
iter e add1 divs.
Import NatTrec.
Definition add_totient_factor f m := let: (p, e) := f in p.-1 * p ^ e.-1 * m.
Definition cons_pfactor (p e : nat) pd := ifnz e ((p, e) :: pd) pd.
Notation "p ^? e :: pd" := (cons_pfactor p e pd)
(at level 30, e at level 30, pd at level 60) : nat_scope.
End PrimeDecompAux.
(* For pretty-printing. *)
Definition NumFactor (f : nat * nat) := ([Num of f.1], f.2).
Definition pfactor p e := p ^ e.
Section prime_decomp.
Import NatTrec.
Local Fixpoint prime_decomp_rec m k a b c e :=
let p := k.*2.+1 in
if a is a'.+1 then
if b - (ifnz e 1 k - c) is b'.+1 then
[rec m, k, a', b', ifnz c c.-1 (ifnz e p.-2 1), e] else
if (b == 0) && (c == 0) then
let b' := k + a' in [rec b'.*2.+3, k, a', b', k.-1, e.+1] else
let bc' := ifnz e (ifnz b (k, 0) (edivn2 0 c)) (b, c) in
p ^? e :: ifnz a' [rec m, k.+1, a'.-1, bc'.1 + a', bc'.2, 0] [:: (m, 1)]
else if (b == 0) && (c == 0) then [:: (p, e.+2)] else p ^? e :: [:: (m, 1)]
where "[ 'rec' m , k , a , b , c , e ]" := (prime_decomp_rec m k a b c e).
Definition prime_decomp n :=
let: (e2, m2) := elogn2 0 n.-1 n.-1 in
if m2 < 2 then 2 ^? e2 :: 3 ^? m2 :: [::] else
let: (a, bc) := edivn m2.-2 3 in
let: (b, c) := edivn (2 - bc) 2 in
2 ^? e2 :: [rec m2.*2.+1, 1, a, b, c, 0].
End prime_decomp.
Definition primes n := unzip1 (prime_decomp n).
Definition prime p := if prime_decomp p is [:: (_ , 1)] then true else false.
Definition nat_pred := simpl_pred nat.
Definition pi_arg := nat.
Coercion pi_arg_of_nat (n : nat) : pi_arg := n.
Coercion pi_arg_of_fin_pred T pT (A : @fin_pred_sort T pT) : pi_arg := #|A|.
Arguments pi_arg_of_nat n /.
Arguments pi_arg_of_fin_pred {T pT} A /.
Definition pi_of (n : pi_arg) : nat_pred := [pred p in primes n].
Notation "\pi ( n )" := (pi_of n)
(at level 2, format "\pi ( n )") : nat_scope.
Notation "\p 'i' ( A )" := \pi(#|A|)
(at level 2, format "\p 'i' ( A )") : nat_scope.
Definition pdiv n := head 1 (primes n).
Definition max_pdiv n := last 1 (primes n).
Definition divisors n := foldr add_divisors [:: 1] (prime_decomp n).
Definition totient n := foldr add_totient_factor (n > 0) (prime_decomp n).
(* Correctness of the decomposition algorithm. *)
Lemma prime_decomp_correct :
let pd_val pd := \prod_(f <- pd) pfactor f.1 f.2 in
let lb_dvd q m := ~~ has [pred d | d %| m] (index_iota 2 q) in
let pf_ok f := lb_dvd f.1 f.1 && (0 < f.2) in
let pd_ord q pd := path ltn q (unzip1 pd) in
let pd_ok q n pd := [/\ n = pd_val pd, all pf_ok pd & pd_ord q pd] in
forall n, n > 0 -> pd_ok 1 n (prime_decomp n).
Proof.
rewrite unlock => pd_val lb_dvd pf_ok pd_ord pd_ok.
have leq_pd_ok m p q pd: q <= p -> pd_ok p m pd -> pd_ok q m pd.
rewrite /pd_ok /pd_ord; case: pd => [|[r _] pd] //= leqp [<- ->].
by case/andP=> /(leq_trans _)->.
have apd_ok m e q p pd: lb_dvd p p || (e == 0) -> q < p ->
pd_ok p m pd -> pd_ok q (p ^ e * m) (p ^? e :: pd).
- case: e => [|e]; rewrite orbC /= => pr_p ltqp.
by rewrite mul1n; apply: leq_pd_ok; apply: ltnW.
by rewrite /pd_ok /pd_ord /pf_ok /= pr_p ltqp => [[<- -> ->]].
case=> // n _; rewrite /prime_decomp.
case: elogn2P => e2 m2 -> {n}; case: m2 => [|[|abc]]; try exact: apd_ok.
rewrite [_.-2]/= !ltnS ltn0 natTrecE; case: edivnP => a bc ->{abc}.
case: edivnP => b c def_bc /= ltc2 ltbc3; apply: (apd_ok) => //.
move def_m: _.*2.+1 => m; set k := {2}1; rewrite -[2]/k.*2; set e := 0.
pose p := k.*2.+1; rewrite -{1}[m]mul1n -[1]/(p ^ e)%N.
have{def_m bc def_bc ltc2 ltbc3}:
let kb := (ifnz e k 1).*2 in
[&& k > 0, p < m, lb_dvd p m, c < kb & lb_dvd p p || (e == 0)]
/\ m + (b * kb + c).*2 = p ^ 2 + (a * p).*2.
- rewrite -def_m [in lb_dvd _ _]def_m; split=> //=; last first.
by rewrite -def_bc addSn -doubleD 2!addSn -addnA subnKC // addnC.
rewrite ltc2 /lb_dvd /index_iota /= dvdn2 -def_m.
by rewrite [_.+2]lock /= odd_double.
have [n] := ubnP a.
elim: n => // n IHn in a (k) p m b c (e) * => /ltnSE-le_a_n [].
set kb := _.*2; set d := _ + c => /and5P[lt0k ltpm leppm ltc pr_p def_m].
have def_k1: k.-1.+1 = k := ltn_predK lt0k.
have def_kb1: kb.-1.+1 = kb by rewrite /kb -def_k1; case e.
have eq_bc_0: (b == 0) && (c == 0) = (d == 0).
by rewrite addn_eq0 muln_eq0 orbC -def_kb1.
have lt1p: 1 < p by rewrite ltnS double_gt0.
have co_p_2: coprime p 2 by rewrite /coprime gcdnC gcdnE modn2 /= odd_double.
have if_d0: d = 0 -> [/\ m = (p + a.*2) * p, lb_dvd p p & lb_dvd p (p + a.*2)].
move=> d0; have{d0 def_m} def_m: m = (p + a.*2) * p.
by rewrite d0 addn0 -mulnn -!mul2n mulnA -mulnDl in def_m *.
split=> //; apply/hasPn=> r /(hasPn leppm); apply: contra => /= dv_r.
by rewrite def_m dvdn_mull.
by rewrite def_m dvdn_mulr.
case def_a: a => [|a'] /= in le_a_n *; rewrite !natTrecE -/p {}eq_bc_0.
case: d if_d0 def_m => [[//| def_m {pr_p}pr_p pr_m'] _ | d _ def_m] /=.
rewrite def_m def_a addn0 mulnA -2!expnSr.
by split; rewrite /pd_ord /pf_ok /= ?muln1 ?pr_p ?leqnn.
apply: apd_ok; rewrite // /pd_ok /= /pfactor expn1 muln1 /pd_ord /= ltpm.
rewrite /pf_ok !andbT /=; split=> //; apply: contra leppm.
case/hasP=> r /=; rewrite mem_index_iota => /andP[lt1r ltrm] dvrm; apply/hasP.
have [ltrp | lepr] := ltnP r p.
by exists r; rewrite // mem_index_iota lt1r.
case/dvdnP: dvrm => q def_q; exists q; last by rewrite def_q /= dvdn_mulr.
rewrite mem_index_iota -(ltn_pmul2r (ltnW lt1r)) -def_q mul1n ltrm.
move: def_m; rewrite def_a addn0 -(@ltn_pmul2r p) // mulnn => <-.
apply: (@leq_ltn_trans m); first by rewrite def_q leq_mul.
by rewrite -addn1 leq_add2l.
have def_k2: k.*2 = ifnz e 1 k * kb.
by rewrite /kb; case: (e) => [|e']; rewrite (mul1n, muln2).
case def_b': (b - _) => [|b']; last first.
have ->: ifnz e k.*2.-1 1 = kb.-1 by rewrite /kb; case e.
apply: IHn => {n le_a_n}//; rewrite -/p -/kb; split=> //.
rewrite lt0k ltpm leppm pr_p andbT /=.
by case: ifnzP; [move/ltn_predK->; apply: ltnW | rewrite def_kb1].
apply: (@addIn p.*2).
rewrite -2!addnA -!doubleD -addnA -mulSnr -def_a -def_m /d.
have ->: b * kb = b' * kb + (k.*2 - c * kb + kb).
rewrite addnCA addnC -mulSnr -def_b' def_k2 -mulnBl -mulnDl subnK //.
by rewrite ltnW // -subn_gt0 def_b'.
rewrite -addnA; congr (_ + (_ + _).*2).
case: (c) ltc; first by rewrite -addSnnS def_kb1 subn0 addn0 addnC.
rewrite /kb; case e => [[] // _ | e' c' _] /=; last first.
by rewrite subnDA subnn addnC addSnnS.
by rewrite mul1n -doubleB -doubleD subn1 !addn1 def_k1.
have ltdp: d < p.
move/eqP: def_b'; rewrite subn_eq0 -(@leq_pmul2r kb); last first.
by rewrite -def_kb1.
rewrite mulnBl -def_k2 ltnS -(leq_add2r c); move/leq_trans; apply.
have{ltc} ltc: c < k.*2.
by apply: (leq_trans ltc); rewrite leq_double /kb; case e.
rewrite -{2}(subnK (ltnW ltc)) leq_add2r leq_sub2l //.
by rewrite -def_kb1 mulnS leq_addr.
case def_d: d if_d0 => [|d'] => [[//|{def_m ltdp pr_p} def_m pr_p pr_m'] | _].
rewrite eqxx -doubleS -addnS -def_a doubleD -addSn -/p def_m.
rewrite mulnCA mulnC -expnSr.
apply: IHn => {n le_a_n}//; rewrite -/p -/kb; split.
rewrite lt0k -addn1 leq_add2l {1}def_a pr_m' pr_p /= def_k1 -addnn.
by rewrite leq_addr.
rewrite -addnA -doubleD addnCA def_a addSnnS def_k1 -(addnC k) -mulnSr.
rewrite -[_.*2.+1]/p mulnDl doubleD addnA -mul2n mulnA mul2n -mulSn.
by rewrite -/p mulnn.
have next_pm: lb_dvd p.+2 m.
rewrite /lb_dvd /index_iota 2!subSS subn0 -(subnK lt1p) iota_add.
rewrite has_cat; apply/norP; split=> //=; rewrite orbF subnKC // orbC.
apply/norP; split; apply/dvdnP=> [[q def_q]].
case/hasP: leppm; exists 2; first by rewrite /p -(subnKC lt0k).
by rewrite /= def_q dvdn_mull // dvdn2 /= odd_double.
move/(congr1 (dvdn p)): def_m; rewrite -mulnn -!mul2n mulnA -mulnDl.
rewrite dvdn_mull // dvdn_addr; last by rewrite def_q dvdn_mull.
case/dvdnP=> r; rewrite mul2n => def_r; move: ltdp (congr1 odd def_r).
rewrite odd_double -ltn_double {1}def_r -mul2n ltn_pmul2r //.
by case: r def_r => [|[|[]]] //; rewrite def_d // mul1n /= odd_double.
apply: apd_ok => //; case: a' def_a le_a_n => [|a'] def_a => [_ | lta] /=.
rewrite /pd_ok /= /pfactor expn1 muln1 /pd_ord /= ltpm /pf_ok !andbT /=.
split=> //; apply: contra next_pm.
case/hasP=> q; rewrite mem_index_iota => /andP[lt1q ltqm] dvqm; apply/hasP.
have [ltqp | lepq] := ltnP q p.+2.
by exists q; rewrite // mem_index_iota lt1q.
case/dvdnP: dvqm => r def_r; exists r; last by rewrite def_r /= dvdn_mulr.
rewrite mem_index_iota -(ltn_pmul2r (ltnW lt1q)) -def_r mul1n ltqm /=.
rewrite -(@ltn_pmul2l p.+2) //; apply: (@leq_ltn_trans m).
by rewrite def_r mulnC leq_mul.
rewrite -addn2 mulnn sqrnD mul2n muln2 -addnn addnCA -addnA addnCA addnA.
by rewrite def_a mul1n in def_m; rewrite -def_m addnS -addnA ltnS leq_addr.
set bc := ifnz _ _ _; apply: leq_pd_ok (leqnSn _) _.
rewrite -doubleS -{1}[m]mul1n -[1]/(k.+1.*2.+1 ^ 0)%N.
apply: IHn; first exact: ltnW.
rewrite doubleS -/p [ifnz 0 _ _]/=; do 2?split => //.
rewrite orbT next_pm /= -(leq_add2r d.*2) def_m 2!addSnnS -doubleS leq_add.
- move: ltc; rewrite /kb {}/bc andbT; case e => //= e' _; case: ifnzP => //.
by case: edivn2P.
- by rewrite -{1}[p]muln1 -mulnn ltn_pmul2l.
by rewrite leq_double def_a mulSn (leq_trans ltdp) ?leq_addr.
rewrite mulnDl !muln2 -addnA addnCA doubleD addnCA.
rewrite (_ : _ + bc.2 = d); last first.
rewrite /d {}/bc /kb -muln2.
case: (e) (b) def_b' => //= _ []; first by case: edivn2P.
by case c; do 2?case; rewrite // mul1n /= muln2.
rewrite def_m 3!doubleS addnC -(addn2 p) sqrnD mul2n muln2 -3!addnA.
congr (_ + _); rewrite 4!addnS -!doubleD; congr _.*2.+2.+2.
by rewrite def_a -add2n mulnDl -addnA -muln2 -mulnDr mul2n.
Qed.
Lemma primePn n :
reflect (n < 2 \/ exists2 d, 1 < d < n & d %| n) (~~ prime n).
Proof.
rewrite /prime; case: n => [|[|p2]]; try by do 2!left.
case: (@prime_decomp_correct p2.+2) => //; rewrite unlock.
case: prime_decomp => [|[q [|[|e]]] pd] //=; last first; last by rewrite andbF.
rewrite {1}/pfactor 2!expnS -!mulnA /=.
case: (_ ^ _ * _) => [|u -> _ /andP[lt1q _]]; first by rewrite !muln0.
left; right; exists q; last by rewrite dvdn_mulr.
have lt0q := ltnW lt1q; rewrite lt1q -{1}[q]muln1 ltn_pmul2l //.
by rewrite -[2]muln1 leq_mul.
rewrite {1}/pfactor expn1; case: pd => [|[r e] pd] /=; last first.
case: e => [|e] /=; first by rewrite !andbF.
rewrite {1}/pfactor expnS -mulnA.
case: (_ ^ _ * _) => [|u -> _ /and3P[lt1q ltqr _]]; first by rewrite !muln0.
left; right; exists q; last by rewrite dvdn_mulr.
by rewrite lt1q -{1}[q]mul1n ltn_mul // -[q.+1]muln1 leq_mul.
rewrite muln1 !andbT => def_q pr_q lt1q; right=> [[]] // [d].
by rewrite def_q -mem_index_iota => in_d_2q dv_d_q; case/hasP: pr_q; exists d.
Qed.
Lemma primeP p :
reflect (p > 1 /\ forall d, d %| p -> xpred2 1 p d) (prime p).
Proof.
rewrite -[prime p]negbK; have [npr_p | pr_p] := primePn p.
right=> [[lt1p pr_p]]; case: npr_p => [|[d n1pd]].
by rewrite ltnNge lt1p.
by move/pr_p=> /orP[] /eqP def_d; rewrite def_d ltnn ?andbF in n1pd.
have [lep1 | lt1p] := leqP; first by case: pr_p; left.
left; split=> // d dv_d_p; apply/norP=> [[nd1 ndp]]; case: pr_p; right.
exists d; rewrite // andbC 2!ltn_neqAle ndp eq_sym nd1.
by have lt0p := ltnW lt1p; rewrite dvdn_leq // (dvdn_gt0 lt0p).
Qed.
Lemma prime_nt_dvdP d p : prime p -> d != 1 -> reflect (d = p) (d %| p).
Proof.
case/primeP=> _ min_p d_neq1; apply: (iffP idP) => [/min_p|-> //].
by rewrite (negPf d_neq1) /= => /eqP.
Qed.
Arguments primeP {p}.
Arguments primePn {n}.
Lemma prime_gt1 p : prime p -> 1 < p.
Proof. by case/primeP. Qed.
Lemma prime_gt0 p : prime p -> 0 < p.
Proof. by move/prime_gt1; apply: ltnW. Qed.
Hint Resolve prime_gt1 prime_gt0 : core.
Lemma prod_prime_decomp n :
n > 0 -> n = \prod_(f <- prime_decomp n) f.1 ^ f.2.
Proof. by case/prime_decomp_correct. Qed.
Lemma even_prime p : prime p -> p = 2 \/ odd p.
Proof.
move=> pr_p; case odd_p: (odd p); [by right | left].
have: 2 %| p by rewrite dvdn2 odd_p.
by case/primeP: pr_p => _ dv_p /dv_p/(2 =P p).
Qed.
Lemma prime_oddPn p : prime p -> reflect (p = 2) (~~ odd p).
Proof.
by move=> p_pr; apply: (iffP idP) => [|-> //]; case/even_prime: p_pr => ->.
Qed.
Lemma odd_prime_gt2 p : odd p -> prime p -> p > 2.
Proof. by move=> odd_p /prime_gt1; apply: odd_gt2. Qed.
Lemma mem_prime_decomp n p e :
(p, e) \in prime_decomp n -> [/\ prime p, e > 0 & p ^ e %| n].
Proof.
case: (posnP n) => [-> //| /prime_decomp_correct[def_n mem_pd ord_pd pd_pe]].
have /andP[pr_p ->] := allP mem_pd _ pd_pe; split=> //; last first.
case/splitPr: pd_pe def_n => pd1 pd2 ->.
by rewrite big_cat big_cons /= mulnCA dvdn_mulr.
have lt1p: 1 < p.
apply: (allP (order_path_min ltn_trans ord_pd)).
by apply/mapP; exists (p, e).
apply/primeP; split=> // d dv_d_p; apply/norP=> [[nd1 ndp]].
case/hasP: pr_p; exists d => //.
rewrite mem_index_iota andbC 2!ltn_neqAle ndp eq_sym nd1.
by have lt0p := ltnW lt1p; rewrite dvdn_leq // (dvdn_gt0 lt0p).
Qed.
Lemma prime_coprime p m : prime p -> coprime p m = ~~ (p %| m).
Proof.
case/primeP=> p_gt1 p_pr; apply/eqP/negP=> [d1 | ndv_pm].
case/dvdnP=> k def_m; rewrite -(addn0 m) def_m gcdnMDl gcdn0 in d1.
by rewrite d1 in p_gt1.
by apply: gcdn_def => // d /p_pr /orP[] /eqP->.
Qed.
Lemma dvdn_prime2 p q : prime p -> prime q -> (p %| q) = (p == q).
Proof.
move=> pr_p pr_q; apply: negb_inj.
by rewrite eqn_dvd negb_and -!prime_coprime // coprime_sym orbb.
Qed.
Lemma Euclid_dvd1 p : prime p -> (p %| 1) = false.
Proof. by rewrite dvdn1; case: eqP => // ->. Qed.
Lemma Euclid_dvdM m n p : prime p -> (p %| m * n) = (p %| m) || (p %| n).
Proof.
move=> pr_p; case dv_pm: (p %| m); first exact: dvdn_mulr.
by rewrite Gauss_dvdr // prime_coprime // dv_pm.
Qed.
Lemma Euclid_dvd_prod (I : Type) (r : seq I) (P : pred I) (f : I -> nat) p :
prime p ->
p %| \prod_(i <- r | P i) f i = \big[orb/false]_(i <- r | P i) (p %| f i).
Proof.
move=> pP; apply: big_morph=> [x y|]; [exact: Euclid_dvdM | exact: Euclid_dvd1].
Qed.
Lemma Euclid_dvdX m n p : prime p -> (p %| m ^ n) = (p %| m) && (n > 0).
Proof.
case: n => [|n] pr_p; first by rewrite andbF Euclid_dvd1.
by apply: (inv_inj negbK); rewrite !andbT -!prime_coprime // coprime_pexpr.
Qed.
Lemma mem_primes p n : (p \in primes n) = [&& prime p, n > 0 & p %| n].
Proof.
rewrite andbCA; case: posnP => [-> // | /= n_gt0].
apply/mapP/andP=> [[[q e]]|[pr_p]] /=.
case/mem_prime_decomp=> pr_q e_gt0; case/dvdnP=> u -> -> {p}.
by rewrite -(prednK e_gt0) expnS mulnCA dvdn_mulr.
rewrite {1}(prod_prime_decomp n_gt0) big_seq.
apply big_ind => [| u v IHu IHv | [q e] /= mem_qe dv_p_qe].
- by rewrite Euclid_dvd1.
- by rewrite Euclid_dvdM // => /orP[].
exists (q, e) => //=; case/mem_prime_decomp: mem_qe => pr_q _ _.
by rewrite Euclid_dvdX // dvdn_prime2 // in dv_p_qe; case: eqP dv_p_qe.
Qed.
Lemma sorted_primes n : sorted ltn (primes n).
Proof.
by case: (posnP n) => [-> // | /prime_decomp_correct[_ _]]; apply: path_sorted.
Qed.
Lemma eq_primes m n : (primes m =i primes n) <-> (primes m = primes n).
Proof.
split=> [eqpr| -> //].
by apply: (eq_sorted_irr ltn_trans ltnn); rewrite ?sorted_primes.
Qed.
Lemma primes_uniq n : uniq (primes n).
Proof. exact: (sorted_uniq ltn_trans ltnn (sorted_primes n)). Qed.
(* The smallest prime divisor *)
Lemma pi_pdiv n : (pdiv n \in \pi(n)) = (n > 1).
Proof.
case: n => [|[|n]] //; rewrite /pdiv !inE /primes.
have:= prod_prime_decomp (ltn0Sn n.+1); rewrite unlock.
by case: prime_decomp => //= pf pd _; rewrite mem_head.
Qed.
Lemma pdiv_prime n : 1 < n -> prime (pdiv n).
Proof. by rewrite -pi_pdiv mem_primes; case/and3P. Qed.
Lemma pdiv_dvd n : pdiv n %| n.
Proof.
by case: n (pi_pdiv n) => [|[|n]] //; rewrite mem_primes=> /and3P[].
Qed.
Lemma pi_max_pdiv n : (max_pdiv n \in \pi(n)) = (n > 1).
Proof.
rewrite !inE -pi_pdiv /max_pdiv /pdiv !inE.
by case: (primes n) => //= p ps; rewrite mem_head mem_last.
Qed.
Lemma max_pdiv_prime n : n > 1 -> prime (max_pdiv n).
Proof. by rewrite -pi_max_pdiv mem_primes => /andP[]. Qed.
Lemma max_pdiv_dvd n : max_pdiv n %| n.
Proof.
by case: n (pi_max_pdiv n) => [|[|n]] //; rewrite mem_primes => /andP[].
Qed.
Lemma pdiv_leq n : 0 < n -> pdiv n <= n.
Proof. by move=> n_gt0; rewrite dvdn_leq // pdiv_dvd. Qed.
Lemma max_pdiv_leq n : 0 < n -> max_pdiv n <= n.
Proof. by move=> n_gt0; rewrite dvdn_leq // max_pdiv_dvd. Qed.
Lemma pdiv_gt0 n : 0 < pdiv n.
Proof. by case: n => [|[|n]] //; rewrite prime_gt0 ?pdiv_prime. Qed.
Lemma max_pdiv_gt0 n : 0 < max_pdiv n.
Proof. by case: n => [|[|n]] //; rewrite prime_gt0 ?max_pdiv_prime. Qed.
Hint Resolve pdiv_gt0 max_pdiv_gt0 : core.
Lemma pdiv_min_dvd m d : 1 < d -> d %| m -> pdiv m <= d.
Proof.
move=> lt1d dv_d_m; case: (posnP m) => [->|mpos]; first exact: ltnW.
rewrite /pdiv; apply: leq_trans (pdiv_leq (ltnW lt1d)).
have: pdiv d \in primes m.
by rewrite mem_primes mpos pdiv_prime // (dvdn_trans (pdiv_dvd d)).
case: (primes m) (sorted_primes m) => //= p pm ord_pm.
rewrite inE => /predU1P[-> //|].
by move/(allP (order_path_min ltn_trans ord_pm)); apply: ltnW.
Qed.
Lemma max_pdiv_max n p : p \in \pi(n) -> p <= max_pdiv n.
Proof.
rewrite /max_pdiv !inE => n_p.
case/splitPr: n_p (sorted_primes n) => p1 p2; rewrite last_cat -cat_rcons /=.
rewrite headI /= cat_path -(last_cons 0) -headI last_rcons; case/andP=> _.
move/(order_path_min ltn_trans); case/lastP: p2 => //= p2 q.
by rewrite all_rcons last_rcons ltn_neqAle -andbA => /and3P[].
Qed.
Lemma ltn_pdiv2_prime n : 0 < n -> n < pdiv n ^ 2 -> prime n.
Proof.
case def_n: n => [|[|n']] // _; rewrite -def_n => lt_n_p2.
suffices ->: n = pdiv n by rewrite pdiv_prime ?def_n.
apply/eqP; rewrite eqn_leq leqNgt andbC pdiv_leq; last by rewrite def_n.
move: lt_n_p2; rewrite ltnNge; apply: contra => lt_pm_m.
case/dvdnP: (pdiv_dvd n) => q def_q.
rewrite {2}def_q -mulnn leq_pmul2r // pdiv_min_dvd //.
by rewrite -[pdiv n]mul1n {2}def_q ltn_pmul2r in lt_pm_m.
by rewrite def_q dvdn_mulr.
Qed.
Lemma primePns n :
reflect (n < 2 \/ exists p, [/\ prime p, p ^ 2 <= n & p %| n]) (~~ prime n).
Proof.
apply: (iffP idP) => [npr_p|]; last first.
case=> [|[p [pr_p le_p2_n dv_p_n]]]; first by case: n => [|[]].
apply/negP=> pr_n; move: dv_p_n le_p2_n; rewrite dvdn_prime2 //; move/eqP->.
by rewrite leqNgt -{1}[n]muln1 -mulnn ltn_pmul2l ?prime_gt1 ?prime_gt0.
case: leqP => [lt1p|]; [right | by left].
exists (pdiv n); rewrite pdiv_dvd pdiv_prime //; split=> //.
by case: leqP npr_p => //; move/ltn_pdiv2_prime->; auto.
Qed.
Arguments primePns {n}.
Lemma pdivP n : n > 1 -> {p | prime p & p %| n}.
Proof. by move=> lt1n; exists (pdiv n); rewrite ?pdiv_dvd ?pdiv_prime. Qed.
Lemma primes_mul m n p : m > 0 -> n > 0 ->
(p \in primes (m * n)) = (p \in primes m) || (p \in primes n).
Proof.
move=> m_gt0 n_gt0; rewrite !mem_primes muln_gt0 m_gt0 n_gt0.
by case pr_p: (prime p); rewrite // Euclid_dvdM.
Qed.
Lemma primes_exp m n : n > 0 -> primes (m ^ n) = primes m.
Proof.
case: n => // n _; rewrite expnS; case: (posnP m) => [-> //| m_gt0].
apply/eq_primes => /= p; elim: n => [|n IHn]; first by rewrite muln1.
by rewrite primes_mul ?(expn_gt0, expnS, IHn, orbb, m_gt0).
Qed.
Lemma primes_prime p : prime p -> primes p = [::p].
Proof.
move=> pr_p; apply: (eq_sorted_irr ltn_trans ltnn) => // [|q].
exact: sorted_primes.
rewrite mem_seq1 mem_primes prime_gt0 //=.
by apply/andP/idP=> [[pr_q q_p] | /eqP-> //]; rewrite -dvdn_prime2.
Qed.
Lemma coprime_has_primes m n :
0 < m -> 0 < n -> coprime m n = ~~ has (mem (primes m)) (primes n).
Proof.
move=> m_gt0 n_gt0; apply/eqP/hasPn=> [mn1 p | no_p_mn].
rewrite /= !mem_primes m_gt0 n_gt0 /= => /andP[pr_p p_n].
have:= prime_gt1 pr_p; rewrite pr_p ltnNge -mn1 /=; apply: contra => p_m.
by rewrite dvdn_leq ?gcdn_gt0 ?m_gt0 // dvdn_gcd ?p_m.
case: (ltngtP (gcdn m n) 1) => //; first by rewrite ltnNge gcdn_gt0 ?m_gt0.
move/pdiv_prime; set p := pdiv _ => pr_p.
move/implyP: (no_p_mn p); rewrite /= !mem_primes m_gt0 n_gt0 pr_p /=.
by rewrite !(dvdn_trans (pdiv_dvd _)) // (dvdn_gcdl, dvdn_gcdr).
Qed.
Lemma pdiv_id p : prime p -> pdiv p = p.
Proof. by move=> p_pr; rewrite /pdiv primes_prime. Qed.
Lemma pdiv_pfactor p k : prime p -> pdiv (p ^ k.+1) = p.
Proof. by move=> p_pr; rewrite /pdiv primes_exp ?primes_prime. Qed.
(* Primes are unbounded. *)
Lemma prime_above m : {p | m < p & prime p}.
Proof.
have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1 by rewrite addn1 ltnS fact_gt0.
exists p => //; rewrite ltnNge; apply: contraL p_dv_m1 => p_le_m.
by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1.
Qed.
(* "prime" logarithms and p-parts. *)
Fixpoint logn_rec d m r :=
match r, edivn m d with
| r'.+1, (_.+1 as m', 0) => (logn_rec d m' r').+1
| _, _ => 0
end.
Definition logn p m := if prime p then logn_rec p m m else 0.
Lemma lognE p m :
logn p m = if [&& prime p, 0 < m & p %| m] then (logn p (m %/ p)).+1 else 0.
Proof.
rewrite /logn /dvdn; case p_pr: (prime p) => //.
case def_m: m => // [m']; rewrite !andTb [LHS]/= -def_m /divn modn_def.
case: edivnP def_m => [[|q] [|r] -> _] // def_m; congr _.+1; rewrite [_.1]/=.
have{m def_m}: q < m'.
by rewrite -ltnS -def_m addn0 mulnC -{1}[q.+1]mul1n ltn_pmul2r // prime_gt1.
elim/ltn_ind: m' {q}q.+1 (ltn0Sn q) => -[_ []|r IHr m] //= m_gt0 le_mr.
rewrite -[m in logn_rec _ _ m]prednK //=.
case: edivnP => [[|q] [|_] def_q _] //; rewrite addn0 in def_q.
have{def_q} lt_qm1: q < m.-1.
by rewrite -[q.+1]muln1 -ltnS prednK // def_q ltn_pmul2l // prime_gt1.
have{le_mr} le_m1r: m.-1 <= r by rewrite -ltnS prednK.
by rewrite (IHr r) ?(IHr m.-1) // (leq_trans lt_qm1).
Qed.
Lemma logn_gt0 p n : (0 < logn p n) = (p \in primes n).
Proof. by rewrite lognE -mem_primes; case: {+}(p \in _). Qed.
Lemma ltn_log0 p n : n < p -> logn p n = 0.
Proof. by case: n => [|n] ltnp; rewrite lognE ?andbF // gtnNdvd ?andbF. Qed.
Lemma logn0 p : logn p 0 = 0.
Proof. by rewrite /logn if_same. Qed.
Lemma logn1 p : logn p 1 = 0.
Proof. by rewrite lognE dvdn1 /= andbC; case: eqP => // ->. Qed.
Lemma pfactor_gt0 p n : 0 < p ^ logn p n.
Proof. by rewrite expn_gt0 lognE; case: (posnP p) => // ->. Qed.
Hint Resolve pfactor_gt0 : core.
Lemma pfactor_dvdn p n m : prime p -> m > 0 -> (p ^ n %| m) = (n <= logn p m).
Proof.
move=> p_pr; elim: n m => [|n IHn] m m_gt0; first exact: dvd1n.
rewrite lognE p_pr m_gt0 /=; case dv_pm: (p %| m); last first.
apply/dvdnP=> [] [/= q def_m].
by rewrite def_m expnS mulnCA dvdn_mulr in dv_pm.
case/dvdnP: dv_pm m_gt0 => q ->{m}; rewrite muln_gt0 => /andP[p_gt0 q_gt0].
by rewrite expnSr dvdn_pmul2r // mulnK // IHn.
Qed.
Lemma pfactor_dvdnn p n : p ^ logn p n %| n.
Proof.
case: n => // n; case pr_p: (prime p); first by rewrite pfactor_dvdn.
by rewrite lognE pr_p dvd1n.
Qed.
Lemma logn_prime p q : prime q -> logn p q = (p == q).
Proof.
move=> pr_q; have q_gt0 := prime_gt0 pr_q; rewrite lognE q_gt0 /=.
case pr_p: (prime p); last by case: eqP pr_p pr_q => // -> ->.
by rewrite dvdn_prime2 //; case: eqP => // ->; rewrite divnn q_gt0 logn1.
Qed.
Lemma pfactor_coprime p n :
prime p -> n > 0 -> {m | coprime p m & n = m * p ^ logn p n}.
Proof.
move=> p_pr n_gt0; set k := logn p n.
have dv_pk_n: p ^ k %| n by rewrite pfactor_dvdn.
exists (n %/ p ^ k); last by rewrite divnK.
rewrite prime_coprime // -(@dvdn_pmul2r (p ^ k)) ?expn_gt0 ?prime_gt0 //.
by rewrite -expnS divnK // pfactor_dvdn // ltnn.
Qed.
Lemma pfactorK p n : prime p -> logn p (p ^ n) = n.
Proof.
move=> p_pr; have pn_gt0: p ^ n > 0 by rewrite expn_gt0 prime_gt0.
apply/eqP; rewrite eqn_leq -pfactor_dvdn // dvdnn andbT.
by rewrite -(leq_exp2l _ _ (prime_gt1 p_pr)) dvdn_leq // pfactor_dvdn.
Qed.
Lemma pfactorKpdiv p n : prime p -> logn (pdiv (p ^ n)) (p ^ n) = n.
Proof. by case: n => // n p_pr; rewrite pdiv_pfactor ?pfactorK. Qed.
Lemma dvdn_leq_log p m n : 0 < n -> m %| n -> logn p m <= logn p n.
Proof.
move=> n_gt0 dv_m_n; have m_gt0 := dvdn_gt0 n_gt0 dv_m_n.
case p_pr: (prime p); last by do 2!rewrite lognE p_pr /=.
by rewrite -pfactor_dvdn //; apply: dvdn_trans dv_m_n; rewrite pfactor_dvdn.
Qed.
Lemma ltn_logl p n : 0 < n -> logn p n < n.
Proof.
move=> n_gt0; have [p_gt1 | p_le1] := boolP (1 < p).
by rewrite (leq_trans (ltn_expl _ p_gt1)) // dvdn_leq ?pfactor_dvdnn.
by rewrite lognE (contraNF (@prime_gt1 _)).
Qed.
Lemma logn_Gauss p m n : coprime p m -> logn p (m * n) = logn p n.
Proof.
move=> co_pm; case p_pr: (prime p); last by rewrite /logn p_pr.
have [-> | n_gt0] := posnP n; first by rewrite muln0.
have [m0 | m_gt0] := posnP m; first by rewrite m0 prime_coprime ?dvdn0 in co_pm.
have mn_gt0: m * n > 0 by rewrite muln_gt0 m_gt0.
apply/eqP; rewrite eqn_leq andbC dvdn_leq_log ?dvdn_mull //.
set k := logn p _; have: p ^ k %| m * n by rewrite pfactor_dvdn.
by rewrite Gauss_dvdr ?coprime_expl // -pfactor_dvdn.
Qed.
Lemma logn_coprime p m : coprime p m -> logn p m = 0.
Proof. by move=> coprime_pm; rewrite -[m]muln1 logn_Gauss// logn1. Qed.
Lemma lognM p m n : 0 < m -> 0 < n -> logn p (m * n) = logn p m + logn p n.
Proof.
case p_pr: (prime p); last by rewrite /logn p_pr.
have xlp := pfactor_coprime p_pr.
case/xlp=> m' co_m' def_m /xlp[n' co_n' def_n] {xlp}.
by rewrite {1}def_m {1}def_n mulnCA -mulnA -expnD !logn_Gauss // pfactorK.
Qed.
Lemma lognX p m n : logn p (m ^ n) = n * logn p m.
Proof.
case p_pr: (prime p); last by rewrite /logn p_pr muln0.
elim: n => [|n IHn]; first by rewrite logn1.
have [->|m_gt0] := posnP m; first by rewrite exp0n // lognE andbF muln0.
by rewrite expnS lognM ?IHn // expn_gt0 m_gt0.
Qed.
Lemma logn_div p m n : m %| n -> logn p (n %/ m) = logn p n - logn p m.
Proof.
rewrite dvdn_eq => /eqP def_n.
case: (posnP n) => [-> |]; first by rewrite div0n logn0.
by rewrite -{1 3}def_n muln_gt0 => /andP[q_gt0 m_gt0]; rewrite lognM ?addnK.
Qed.
Lemma dvdn_pfactor p d n : prime p ->
reflect (exists2 m, m <= n & d = p ^ m) (d %| p ^ n).
Proof.
move=> p_pr; have pn_gt0: p ^ n > 0 by rewrite expn_gt0 prime_gt0.
apply: (iffP idP) => [dv_d_pn|[m le_m_n ->]]; last first.
by rewrite -(subnK le_m_n) expnD dvdn_mull.
exists (logn p d); first by rewrite -(pfactorK n p_pr) dvdn_leq_log.
have d_gt0: d > 0 by apply: dvdn_gt0 dv_d_pn.
case: (pfactor_coprime p_pr d_gt0) => q co_p_q def_d.
rewrite {1}def_d ((q =P 1) _) ?mul1n // -dvdn1.
suff: q %| p ^ n * 1 by rewrite Gauss_dvdr // coprime_sym coprime_expl.
by rewrite muln1 (dvdn_trans _ dv_d_pn) // def_d dvdn_mulr.
Qed.
Lemma prime_decompE n : prime_decomp n = [seq (p, logn p n) | p <- primes n].
Proof.
case: n => // n; pose f0 := (0, 0); rewrite -map_comp.
apply: (@eq_from_nth _ f0) => [|i lt_i_n]; first by rewrite size_map.
rewrite (nth_map f0) //; case def_f: (nth _ _ i) => [p e] /=.
congr (_, _); rewrite [n.+1]prod_prime_decomp //.
have: (p, e) \in prime_decomp n.+1 by rewrite -def_f mem_nth.
case/mem_prime_decomp=> pr_p _ _.
rewrite (big_nth f0) big_mkord (bigD1 (Ordinal lt_i_n)) //=.
rewrite def_f mulnC logn_Gauss ?pfactorK //.
apply big_ind => [|m1 m2 com1 com2| [j ltj] /=]; first exact: coprimen1.
by rewrite coprime_mulr com1.
rewrite -val_eqE /= => nji; case def_j: (nth _ _ j) => [q e1] /=.
have: (q, e1) \in prime_decomp n.+1 by rewrite -def_j mem_nth.
case/mem_prime_decomp=> pr_q e1_gt0 _; rewrite coprime_pexpr //.
rewrite prime_coprime // dvdn_prime2 //; apply: contra nji => eq_pq.
rewrite -(nth_uniq 0 _ _ (primes_uniq n.+1)) ?size_map //=.
by rewrite !(nth_map f0) // def_f def_j /= eq_sym.
Qed.
(* Some combinatorial formulae. *)
Lemma divn_count_dvd d n : n %/ d = \sum_(1 <= i < n.+1) (d %| i).
Proof.
have [-> | d_gt0] := posnP d; first by rewrite big_add1 divn0 big1.
apply: (@addnI (d %| 0)); rewrite -(@big_ltn _ 0 _ 0 _ (dvdn d)) // big_mkord.
rewrite (partition_big (fun i : 'I_n.+1 => inord (i %/ d)) 'I_(n %/ d).+1) //=.
rewrite dvdn0 add1n -{1}[_.+1]card_ord -sum1_card; apply: eq_bigr => [[q ?] _].
rewrite (bigD1 (inord (q * d))) /eq_op /= !inordK ?ltnS -?leq_divRL ?mulnK //.
rewrite dvdn_mull ?big1 // => [[i /= ?] /andP[/eqP <- /negPf]].
by rewrite eq_sym dvdn_eq inordK ?ltnS ?leq_div2r // => ->.
Qed.
Lemma logn_count_dvd p n : prime p -> logn p n = \sum_(1 <= k < n) (p ^ k %| n).
Proof.
rewrite big_add1 => p_prime; case: n => [|n]; first by rewrite logn0 big_geq.
rewrite big_mkord -big_mkcond (eq_bigl _ _ (fun _ => pfactor_dvdn _ _ _)) //=.
by rewrite big_ord_narrow ?sum1_card ?card_ord // -ltnS ltn_logl.
Qed.
(* Truncated real log. *)
Definition trunc_log p n :=
let fix loop n k :=
if k is k'.+1 then if p <= n then (loop (n %/ p) k').+1 else 0 else 0
in loop n n.
Lemma trunc_log_bounds p n :
1 < p -> 0 < n -> let k := trunc_log p n in p ^ k <= n < p ^ k.+1.
Proof.
rewrite {+}/trunc_log => p_gt1; have p_gt0 := ltnW p_gt1.
set loop := (loop in loop n n); set m := n; rewrite [in n in loop m n]/m.
have: m <= n by []; elim: n m => [|n IHn] [|m] //= /ltnSE-le_m_n _.
have [le_p_n | // ] := leqP p _; rewrite 2!expnSr -leq_divRL -?ltn_divLR //.
by apply: IHn; rewrite ?divn_gt0 // -ltnS (leq_trans (ltn_Pdiv _ _)).
Qed.
Lemma trunc_log_ltn p n : 1 < p -> n < p ^ (trunc_log p n).+1.
Proof.
have [-> | n_gt0] := posnP n; first by move=> /ltnW; rewrite expn_gt0.
by case/trunc_log_bounds/(_ n_gt0)/andP.
Qed.
Lemma trunc_logP p n : 1 < p -> 0 < n -> p ^ trunc_log p n <= n.
Proof. by move=> p_gt1 /(trunc_log_bounds p_gt1)/andP[]. Qed.
Lemma trunc_log_max p k j : 1 < p -> p ^ j <= k -> j <= trunc_log p k.
Proof.
move=> p_gt1 le_pj_k; rewrite -ltnS -(@ltn_exp2l p) //.
exact: leq_ltn_trans (trunc_log_ltn _ _).
Qed.
(* pi- parts *)
(* Testing for membership in set of prime factors. *)
Canonical nat_pred_pred := Eval hnf in [predType of nat_pred].
Coercion nat_pred_of_nat (p : nat) : nat_pred := pred1 p.
Section NatPreds.
Variables (n : nat) (pi : nat_pred).
Definition negn : nat_pred := [predC pi].
Definition pnat : pred nat := fun m => (m > 0) && all (mem pi) (primes m).
Definition partn := \prod_(0 <= p < n.+1 | p \in pi) p ^ logn p n.
End NatPreds.
Notation "pi ^'" := (negn pi) (at level 2, format "pi ^'") : nat_scope.
Notation "pi .-nat" := (pnat pi) (at level 2, format "pi .-nat") : nat_scope.
Notation "n `_ pi" := (partn n pi) : nat_scope.
Section PnatTheory.
Implicit Types (n p : nat) (pi rho : nat_pred).
Lemma negnK pi : pi^'^' =i pi.
Proof. by move=> p; apply: negbK. Qed.
Lemma eq_negn pi1 pi2 : pi1 =i pi2 -> pi1^' =i pi2^'.
Proof. by move=> eq_pi n; rewrite 3!inE /= eq_pi. Qed.
Lemma eq_piP m n : \pi(m) =i \pi(n) <-> \pi(m) = \pi(n).
Proof.
rewrite /pi_of; have eqs := eq_sorted_irr ltn_trans ltnn.
by split=> [|-> //]; move/(eqs _ _ (sorted_primes m) (sorted_primes n)) ->.
Qed.
Lemma part_gt0 pi n : 0 < n`_pi.
Proof. exact: prodn_gt0. Qed.
Hint Resolve part_gt0 : core.
Lemma sub_in_partn pi1 pi2 n :
{in \pi(n), {subset pi1 <= pi2}} -> n`_pi1 %| n`_pi2.
Proof.
move=> pi12; rewrite ![n`__]big_mkcond /=.
apply (big_ind2 (fun m1 m2 => m1 %| m2)) => // [*|p _]; first exact: dvdn_mul.
rewrite lognE -mem_primes; case: ifP => pi1p; last exact: dvd1n.
by case: ifP => pr_p; [rewrite pi12 | rewrite if_same].
Qed.
Lemma eq_in_partn pi1 pi2 n : {in \pi(n), pi1 =i pi2} -> n`_pi1 = n`_pi2.
Proof.
by move=> pi12; apply/eqP; rewrite eqn_dvd ?sub_in_partn // => p /pi12->.
Qed.
Lemma eq_partn pi1 pi2 n : pi1 =i pi2 -> n`_pi1 = n`_pi2.
Proof. by move=> pi12; apply: eq_in_partn => p _. Qed.
Lemma partnNK pi n : n`_pi^'^' = n`_pi.
Proof. by apply: eq_partn; apply: negnK. Qed.
Lemma widen_partn m pi n :
n <= m -> n`_pi = \prod_(0 <= p < m.+1 | p \in pi) p ^ logn p n.
Proof.
move=> le_n_m; rewrite big_mkcond /=.
rewrite [n`_pi](big_nat_widen _ _ m.+1) // big_mkcond /=.
apply: eq_bigr => p _; rewrite ltnS lognE.
by case: and3P => [[_ n_gt0 p_dv_n]|]; rewrite ?if_same // andbC dvdn_leq.
Qed.
Lemma eq_partn_from_log m n (pi : nat_pred) : 0 < m -> 0 < n ->
{in pi, logn^~ m =1 logn^~ n} -> m`_pi = n`_pi.
Proof.
move=> m0 n0 eq_log; rewrite !(@widen_partn (maxn m n)) ?leq_maxl ?leq_maxr//.
by apply: eq_bigr => p /eq_log ->.
Qed.
Lemma partn0 pi : 0`_pi = 1.
Proof. by apply: big1_seq => [] [|n]; rewrite andbC. Qed.
Lemma partn1 pi : 1`_pi = 1.
Proof. by apply: big1_seq => [] [|[|n]]; rewrite andbC. Qed.
Lemma partnM pi m n : m > 0 -> n > 0 -> (m * n)`_pi = m`_pi * n`_pi.
Proof.
have le_pmul m' n': m' > 0 -> n' <= m' * n' by move/prednK <-; apply: leq_addr.
move=> mpos npos; rewrite !(@widen_partn (n * m)) 3?(le_pmul, mulnC) //.
rewrite !big_mkord -big_split; apply: eq_bigr => p _ /=.
by rewrite lognM // expnD.
Qed.
Lemma partnX pi m n : (m ^ n)`_pi = m`_pi ^ n.
Proof.
elim: n => [|n IHn]; first exact: partn1.
rewrite expnS; case: (posnP m) => [->|m_gt0]; first by rewrite partn0 exp1n.
by rewrite expnS partnM ?IHn // expn_gt0 m_gt0.
Qed.
Lemma partn_dvd pi m n : n > 0 -> m %| n -> m`_pi %| n`_pi.
Proof.
move=> n_gt0 dvmn; case/dvdnP: dvmn n_gt0 => q ->{n}.
by rewrite muln_gt0 => /andP[q_gt0 m_gt0]; rewrite partnM ?dvdn_mull.
Qed.
Lemma p_part p n : n`_p = p ^ logn p n.
Proof.
case (posnP (logn p n)) => [log0 |].
by rewrite log0 [n`_p]big1_seq // => q; case/andP; move/eqnP->; rewrite log0.
rewrite logn_gt0 mem_primes; case/and3P=> _ n_gt0 dv_p_n.
have le_p_n: p < n.+1 by rewrite ltnS dvdn_leq.
by rewrite [n`_p]big_mkord (big_pred1 (Ordinal le_p_n)).
Qed.
Lemma p_part_eq1 p n : (n`_p == 1) = (p \notin \pi(n)).
Proof.
rewrite mem_primes p_part lognE; case: and3P => // [[p_pr _ _]].
by rewrite -dvdn1 pfactor_dvdn // logn1.
Qed.
Lemma p_part_gt1 p n : (n`_p > 1) = (p \in \pi(n)).
Proof. by rewrite ltn_neqAle part_gt0 andbT eq_sym p_part_eq1 negbK. Qed.
Lemma primes_part pi n : primes n`_pi = filter (mem pi) (primes n).
Proof.
have ltnT := ltn_trans.
case: (posnP n) => [-> | n_gt0]; first by rewrite partn0.
apply: (eq_sorted_irr ltnT ltnn); rewrite ?(sorted_primes, sorted_filter) //.
move=> p; rewrite mem_filter /= !mem_primes n_gt0 part_gt0 /=.
apply/andP/and3P=> [[p_pr] | [pi_p p_pr dv_p_n]].
rewrite /partn; apply big_ind => [|n1 n2 IHn1 IHn2|q pi_q].
- by rewrite dvdn1; case: eqP p_pr => // ->.
- by rewrite Euclid_dvdM //; case/orP.
rewrite -{1}(expn1 p) pfactor_dvdn // lognX muln_gt0.
rewrite logn_gt0 mem_primes n_gt0 - andbA /=; case/and3P=> pr_q dv_q_n.
by rewrite logn_prime //; case: eqP => // ->.
have le_p_n: p < n.+1 by rewrite ltnS dvdn_leq.
rewrite [n`_pi]big_mkord (bigD1 (Ordinal le_p_n)) //= dvdn_mulr //.
by rewrite lognE p_pr n_gt0 dv_p_n expnS dvdn_mulr.
Qed.
Lemma filter_pi_of n m : n < m -> filter \pi(n) (index_iota 0 m) = primes n.
Proof.
move=> lt_n_m; have ltnT := ltn_trans; apply: (eq_sorted_irr ltnT ltnn).
- by rewrite sorted_filter // iota_ltn_sorted.
- exact: sorted_primes.
move=> p; rewrite mem_filter mem_index_iota /= mem_primes; case: and3P => //.
by case=> _ n_gt0 dv_p_n; apply: leq_ltn_trans lt_n_m; apply: dvdn_leq.
Qed.
Lemma partn_pi n : n > 0 -> n`_\pi(n) = n.
Proof.
move=> n_gt0; rewrite {3}(prod_prime_decomp n_gt0) prime_decompE big_map.
by rewrite -[n`__]big_filter filter_pi_of.
Qed.
Lemma partnT n : n > 0 -> n`_predT = n.
Proof.
move=> n_gt0; rewrite -{2}(partn_pi n_gt0) {2}/partn big_mkcond /=.
by apply: eq_bigr => p _; rewrite -logn_gt0; case: (logn p _).
Qed.
Lemma eqn_from_log m n : 0 < m -> 0 < n -> logn^~ m =1 logn^~ n -> m = n.
Proof.
by move=> ? ? /(@in1W _ predT)/eq_partn_from_log; rewrite !partnT// => ->.
Qed.