Skip to content

Commit de39db2

Browse files
TragicusTragicus
committed
next_prime
1 parent cd52116 commit de39db2

File tree

1 file changed

+60
-74
lines changed

1 file changed

+60
-74
lines changed

‎theories/showcase/pnt.v‎

Lines changed: 60 additions & 74 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
1-
From mathcomp Require Import all_ssreflect classical_sets
2-
boolp topology ssralg ereal ssrnum.
3-
From mathcomp Require Import sequences reals interval
4-
rat all_analysis archimedean ssrint.
5-
Import Order.OrdinalOrder Num.Theory Order.POrderTheory
6-
finset GRing.Theory Num.Def.
1+
From mathcomp Require Import all_ssreflect classical_sets boolp topology ssralg.
2+
From mathcomp Require Import ereal ssrnum sequences reals interval rat.
3+
From mathcomp Require Import all_analysis archimedean ssrint.
4+
Import Order.OrdinalOrder Num.Theory Order.POrderTheory finset GRing.Theory.
5+
Import Num.Def.
76

87
(**md**************************************************************************)
98
(* # The Prime Number Theorem *)
@@ -29,59 +28,66 @@ Local Open Scope classical_set_scope.
2928
Local Open Scope set_scope.
3029
Local Open Scope nat_scope.
3130

32-
Fixpoint prime_search (i j : nat) : nat :=
33-
match j with
34-
| 0 => i`!.+1
35-
| j'.+1 => if prime (i`!.+1 - j) then i`!.+1 - j else prime_search i j'
36-
end.
31+
Section prime_seq.
3732

38-
Fixpoint prime_seq (n : nat) : nat :=
39-
match n with
40-
| 0 => 2
41-
| i.+1 => let k := prime_seq i in prime_search k (k`! - k)
42-
end.
33+
Let next_prime_subproof (i : nat) : {j : 'I_(i`! - i).+1 | prime (i.+1 + j)}.
34+
Proof.
35+
suff: [exists j : 'I_(i`! - i).+1, prime (i.+1 + (tnth (ord_tuple _) j))].
36+
rewrite (existsb_tnth (fun x : 'I_(i`! - i).+1 => prime (i.+1 + x))).
37+
move=> /(nth_find ord0) ij.
38+
by eexists; apply: ij.
39+
apply/negbNE/negP; rewrite negb_exists => /forallP noprime.
40+
set q := pdiv (i`!.+1).
41+
have qprime: prime q by apply/pdiv_prime/fact_gt0.
42+
case: (leqP q i) => [qlei|iltq].
43+
have /dvdn_fact : 0 < q <= i by rewrite pdiv_gt0.
44+
by rewrite (@dvdn_add_eq _ _ 1) ?Euclid_dvd1 // addn1; apply: pdiv_dvd.
45+
have qlt : q - i.+1 < (i`! - i).+1.
46+
by rewrite -subSn// subSS -subSn ?fact_geq//; apply/leq_sub2r/pdiv_leq.
47+
move: (noprime (Ordinal qlt)) => /negP; apply.
48+
by rewrite tnth_ord_tuple subnKC// ltnW.
49+
Qed.
50+
51+
Definition next_prime (i : nat) : nat :=
52+
i.+1 + [arg min_(j < val (next_prime_subproof i) | prime (i.+1 + j)) val j].
53+
54+
Lemma prime_next_prime (i : nat) : prime (next_prime i).
55+
Proof.
56+
by rewrite /next_prime; case: arg_minnP => //; case: next_prime_subproof.
57+
Qed.
58+
59+
Lemma next_prime_min (i j : nat) : i < j < next_prime i -> ~~ prime j.
60+
Proof.
61+
rewrite /next_prime.
62+
case: arg_minnP => [|k kP kmin]; first by case: next_prime_subproof.
63+
move=> /andP[] ij.
64+
rewrite -(ltn_subLR _ ij) => jk.
65+
have jlt := ltn_trans jk (ltn_ord k).
66+
apply/negP; rewrite -[j](subnKC ij) => jP.
67+
move: (kmin (Ordinal jlt) jP) => /= /(leq_trans jk).
68+
by rewrite ltnn.
69+
Qed.
70+
71+
Lemma next_prime_lt i : i < next_prime i.
72+
Proof.
73+
rewrite /next_prime.
74+
case: arg_minnP => [|j _ _]; first by case: next_prime_subproof.
75+
exact: leq_addr.
76+
Qed.
77+
78+
Definition prime_seq (n : nat) : nat := iter n next_prime 2.
4379

4480
Lemma leq_prime_seq: {mono prime_seq : m n / m <= n}.
4581
Proof.
4682
move=> m n.
4783
apply: (@Order.NatMonotonyTheory.incn_inP _ nat predT) => // {m n} [n /= _ _].
48-
have prgtid i : forall j, i < i`!.+1 - j -> prime_search i j > i.
49-
elim=> /= [_|n0 HR]; first exact: (leq_ltn_trans (fact_geq i) (ltnSn i`!)).
50-
case: (prime (i`!.+1 - n0.+1)) => [// | ilt].
51-
exact/HR/(leq_trans _ (leq_sub2l i`!.+1 (leqnSn n0))).
52-
set k := prime_seq n. set pk := prime_search k (k`! - k).
53-
apply: prgtid. rewrite subnBAC; last exact: leqnSn.
54-
by rewrite -ltn_subLR// subnn subSnn.
55-
exact: fact_geq.
84+
exact: next_prime_lt.
5685
Qed.
5786

5887
Lemma mem_prime_seq (p : nat) : p \in range prime_seq = prime p.
5988
Proof.
6089
apply/idP/idP => [|primep].
61-
rewrite inE => -[] [|n] _ <- //.
62-
set i := prime_seq n.
63-
suff find_prime: forall (j : nat),
64-
(forall k : nat, j < k <= i`! - i -> ~ prime (i`!.+1 - k))
65-
-> prime (prime_search i j).
66-
apply: (find_prime (i`! - i)) => k /andP [] kb1 kb2.
67-
have := (leq_ltn_trans kb2 kb1).
68-
by rewrite ltnn.
69-
elim=> [/= nprimeltq|n0 HR NoPrimeBefore /=]; last first.
70-
case: ifP => // noprime. apply: HR => k.
71-
case: (ltnP n0.+1 k) => [n01ltk|klen0] /andP [] ? ?.
72-
by apply: NoPrimeBefore; rewrite n01ltk.
73-
suff ->: k = n0.+1 by rewrite noprime.
74-
by apply: eqP; rewrite eqn_leq klen0.
75-
set q := pdiv (i`!.+1).
76-
have qprime: prime q by apply/pdiv_prime /fact_gt0.
77-
move: (pdiv_leq (ltn0Sn i`!)). rewrite leq_eqVlt => /orP [/eqP <- //|].
78-
case: (leqP q i) => [qlei|iltq qlt]; last first.
79-
move: (nprimeltq (i`!.+1 - q)).
80-
rewrite subn_gt0 qlt /= (@leq_sub2lE _ i.+1) => [/(_ iltq)|].
81-
by rewrite subKn// ltnW.
82-
exact: fact_geq.
83-
have /dvdn_fact : 0 < q <= i by rewrite pdiv_gt0.
84-
by rewrite (@dvdn_add_eq _ _ 1) ?Euclid_dvd1 // addn1; apply: pdiv_dvd.
90+
by rewrite inE => -[] [|n] _ <- //=; apply: prime_next_prime.
8591
case: (@Order.TotalTheory.arg_maxP _ _ 'I_p.+1 ord0
8692
(fun m => prime_seq m <= p) prime_seq) => /= [|n pgepsi pptargmax].
8793
exact: prime_gt1.
@@ -92,34 +98,14 @@ have pltpsni1: p < prime_seq n.+1.
9298
move: (contra (pptargmax (Ordinal nltp))).
9399
rewrite [(_ <= _)%O](leq_prime_seq (Ordinal nltp) n) ltnn => /(_ erefl).
94100
by rewrite ltnNge.
95-
suff NoPrime k : prime_seq n < k < prime_seq n.+1 -> ~~ prime k => [|/=].
96-
move: pgepsi.
97-
rewrite leq_eqVlt => /orP [/eqP <-|psnltp]; first by rewrite inE.
98-
move: (NoPrime p). rewrite psnltp pltpsni1 => /(_ erefl).
99-
by rewrite primep.
100-
set psn := prime_seq n.
101-
rewrite -[X in X < _](subKn (fact_geq psn)).
102-
elim: (psn`! - psn) => /= [|n0 HR].
103-
rewrite subn0 ltnS => /andP [] kb1 kb2.
104-
have := (leq_ltn_trans kb2 kb1).
105-
by rewrite ltnn.
106-
case: (boolP (prime (psn`! - n0))) => [_ /andP [] kb1| noprime /andP []].
107-
case: (ltnP n0 psn`!) => [n0ltpsnf|]; last first.
108-
rewrite -subn_eq0 subSS => /eqP ->.
109-
by rewrite ltn0.
110-
rewrite subSn// ltnS => kb2.
111-
have := (leq_ltn_trans kb2 kb1).
112-
by rewrite ltnn.
113-
case: (leqP k (psn`! - n0)); last by move=> kb1 _ kb2; apply: HR; rewrite kb1.
114-
rewrite leq_eqVlt => /orP [/eqP -> _ _ // | kb1].
115-
rewrite -subSn; last first.
116-
rewrite -(@ltn_sub2rE n0) // subnn.
117-
exact: (leq_ltn_trans _ kb1).
118-
rewrite subSS => kb2.
119-
have := (leq_ltn_trans kb2 kb1).
120-
by rewrite ltnn.
101+
move: pgepsi.
102+
rewrite leq_eqVlt => /orP [/eqP <-|psnltp]; first by rewrite inE.
103+
move: (@next_prime_min (prime_seq n) p). rewrite psnltp pltpsni1 => /(_ erefl).
104+
by rewrite primep.
121105
Qed.
122106

107+
End prime_seq.
108+
123109
Section DivergenceSumInversePrimeNumbers.
124110

125111
Let P (k N : nat) :=

0 commit comments

Comments
 (0)