###### Cookies disclaimer

Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# [Proof Ground 2020] Infinitude Of Primes

This task asks you to formalize yet another approach to prove the infinitude of primes! We define a function `S` on natural numbers: ``` S 0 = 2 S (n+1) = S(n) * (S(n)+1) ``` Furthermore, let `pf(n)` be the smallest prime factor of `n`. The idea is that `pf(S(n)+1)` generates a new prime for every `n`. The following table illustrates this: ``` n: 0 | 1 | 2 | 3 S(n): 2 | 6 | 42 | 1806 = 42 * 43 pf(S(n)+1): 3 | 7 | 43 | 13 (13 * 139 = 1807) ``` You have two tasks: - Prove that `pf(S(n)+1)` is always prime - Show that, if `pf(S(n)+1) = pf(S(m)+1)`, then `n = m`. Submitted by: Christoph Walther Coq: Fabian Kunze | Lean: Simon Hudon & Kevin Kappelmann | Isabelle: Simon Wimmer

## Resources

Download Files

### Definitions File

```theory Defs
imports Main "HOL-Number_Theory.Eratosthenes"
"HOL-Library.Infinite_Set" \<comment> \<open>Only needed for last theorem\<close>
begin

fun S :: "nat \<Rightarrow> nat" where
"S 0 = 2"
| "S (Suc n) = S n * (S n + 1)"

definition
"pf n = Min (prime_factors n)"

end
```

### Template File

```theory Submission
imports Defs
begin

text \<open>Illustration:
\<open>n\<close>:        0 | 1 | 2  | 3
\<open>S(n)\<close>:     2 | 6 | 42 | 1806 = 42 * 43
\<open>pf(S(n)+1)\<close>: 3 | 7 | 43 | 13 (13 * 139 = 1807)
\<close>

theorem prime_pf_Suc_S:
"prime(pf(S(n)+1))"
sorry

theorem pf_S_inj:
assumes "pf(S(n)+1) = pf(S(m)+1)"
shows "n = m"
sorry

theorem infinitely_many_primes:
"infinite {p :: nat. prime p}"
proof -
let ?S = "(\<lambda>n. pf(S(n)+1)) ` UNIV" let ?P = "{p :: nat. prime p}"
have "?S \<subseteq> ?P"
using prime_pf_Suc_S by auto
moreover have "infinite ?S"
by (intro range_inj_infinite inj_onI, rule pf_S_inj)
ultimately show ?thesis
by (rule infinite_super)
qed

end```

### Check File

```theory Check
imports Submission
begin

theorem prime_pf_Suc_S:
"prime(pf(S(n)+1))"
by (rule Submission.prime_pf_Suc_S)

theorem pf_S_inj:
"pf(S(n)+1) = pf(S(m)+1) \<Longrightarrow> n = m"
by (rule Submission.pf_S_inj)

end```
Download Files

### Definitions File

```import data.nat.prime
import data.list.min_max

definition S : ℕ → ℕ
| 0 := 2
| (n + 1) := S n * (S n + 1)

definition pf (n : ℕ) : ℕ := match n.factors.minimum with
| none := 0
| some n := n
end

----------------------just some definitions to prevent cheating------------------------

definition prime_pf_succ_s_prop : Prop := ∀ (n : ℕ), (pf (S n + 1)).prime

notation `prime_pf_succ_s_prop` := prime_pf_succ_s_prop

definition pf_S_inj_prop : Prop := ∀ {n m : ℕ} (hyp : pf (S n + 1) = pf (S m + 1)), n = m

notation `pf_S_inj_prop` := pf_S_inj_prop
```

### Template File

```import .defs

/- Illustration:
n         0 | 1 | 2  | 3
S n:      2 | 6 | 42 | 1806 = 42 * 43
pf (S n+1): 3 | 7 | 43 | 13 (13 * 139 = 1807)
-/

lemma prime_pf_succ_s : ∀ (n : ℕ), (pf (S n + 1)).prime :=
sorry

lemma pf_S_inj : ∀ {n m : ℕ} (hyp : pf (S n + 1) = pf (S m + 1)), n = m :=
sorry
```

### Check File

```import .defs
import .submission

lemma check_prime_pf_succ_s : prime_pf_succ_s_prop := @prime_pf_succ_s

lemma check_pf_S_inj : pf_S_inj_prop := @pf_S_inj
```
Download Files

### Definitions File

```From Coq Require Export Arith PeanoNat.
Require ZArith.BinInt.

Definition prime (n:nat) :=
2 <= n
/\ forall k, 2 <= k ->
Nat.divide k n -> k = n.

(** this is the function "S" from the exercise statement (renamed to not clash with the nat-constructor [S] ) *)
Fixpoint fS (n:nat) : nat :=
match n with
0 => 2
| S n => fS n * (fS n + 1)
end.

(** We provide the implementation of pf here; the only important properties is [pf_spec], *after* the module. *)
Require Znumtheory BinInt.
Require List ConstructiveEpsilon Lia PeanoNat.

Definition isMinimumOf n (P : nat -> Prop) := P n /\ forall n', P n' -> n <= n'.
Definition primeDivisorOf n k :Prop := prime k /\ Nat.divide k n.

Module pf.
Section pf.
Import List ConstructiveEpsilon Lia PeanoNat.

Lemma lt_wf_rect n (P:nat -> Type):
(forall n, (forall m, m < n -> P m) -> P n) -> P n.
Proof.  pattern n. revert n. apply Fix with (1:=Wf_nat.lt_wf). intuition. Qed.

Let pfOfIs (n k : nat) :Prop :=
2 <= n -> isMinimumOf k (primeDivisorOf n).

Lemma min_computable P:
(exists n, P n)
-> (forall n, {P n} + {~ P n})
-> {k & isMinimumOf k P}.
Proof.
intros H Pdec.
apply constructive_indefinite_ground_description_nat_Acc in H as (n&HPn). 2:easy.
revert P HPn Pdec.
induction n as [n IH] using lt_wf_rect.
intros.
destruct (Pdec 0).
{ exists 0. hnf. intuition lia. }
destruct n as [ | n]. 1:easy.
edestruct IH with (P:= fun i => P (S i) ) (m:=n) as (k'&?&Hk).
1,2,3:now eauto.
exists (S k'). split. 1:now easy. intros []. easy. intros ?%Hk. lia.
Qed.

Import BinInt.

Lemma divide_agree n m:
(0 < n -> 0 <= m ->
(n | m)%Z <-> Nat.divide (Z.to_nat n) (Z.to_nat m))%Z.
Proof.
intros. rewrite <- Nat.mod_divide,<-Z.mod_divide. 2:lia. 2:{now intros ->%(Znat.Z2Nat.inj _ 0);nia. }
rewrite <- (Znat.Z2Nat.id m) at 1. rewrite <- (Znat.Z2Nat.id n) at 1. 2-3:lia.
rewrite <- (Zdiv.mod_Zmod).
2:{now intros ->%(Znat.Z2Nat.inj _ 0);nia. }
rewrite <- Znat.Nat2Z.inj_iff. reflexivity.
Qed.

Lemma prime_agree n :
Znumtheory.prime n <-> prime (Z.to_nat n).
Proof.
rewrite <- Znumtheory.prime_alt. unfold Defs.prime,Znumtheory.prime'.
split.
-intros [H H']. split. {apply (Znat.Z2Nat.inj_le 2). all:lia. }
intros k ? H4. apply Nat.eq_dne. intros H1.
rewrite <- (Znat.Nat2Z.id k) in  H4.
apply divide_agree in H4. 2-3:lia.
eapply H'. 2:eassumption. apply Z.divide_pos_le in H4.
assert (Z.of_nat k <> n). intros <-. rewrite Znat.Nat2Z.id in H1. all:lia.
-intros [H H']. split. {destruct n. 1,3:easy. cbn in H. lia. }
intros ? [] H4. apply divide_agree in H4. 2-3:nia.
apply H' in H4. apply Znat.Z2Nat.inj in H4 as ->. 4:apply Znat.Z2Nat.inj_lt in H0.
4:replace (Z.to_nat 1) with 1 in H0 by reflexivity. all:lia.
Qed.

Definition pf_computable n : {k & pfOfIs n k}.
Proof.
unfold pfOfIs,primeDivisorOf. destruct (Compare_dec.le_dec 2 n) as [Hn|]. 2:now eexists 0.
edestruct min_computable as (k&Hk).
3:{ exists k. intros _. exact Hk. } all:cbn.
-revert Hn. induction n using lt_wf_rect. intros ?.
setoid_rewrite <- Znat.Nat2Z.id. setoid_rewrite <- prime_agree.
destruct (Znumtheory.prime_dec (Z.of_nat n)) as [ | H']. now eauto using Nat.divide_refl.
apply Znumtheory.not_prime_divide in H' as (m&[]&?). 2:lia.
destruct (H (Z.to_nat m)) as (p&Hp_prime&Hp_div).
2:apply Znat.Nat2Z.inj_le. apply Znat.Nat2Z.inj_lt. 1,2:rewrite Znat.Z2Nat.id.
3:replace (Z.of_nat 2) with 2%Z by reflexivity. 1-4:lia.
eexists. rewrite prime_agree. rewrite Znat.Nat2Z.id. split. eassumption.
etransitivity. eassumption. setoid_rewrite <- divide_agree. all:intuition lia.
-intros m. destruct (Znumtheory.prime_dec (Z.of_nat m)) as [H|H].
all:rewrite prime_agree, Znat.Nat2Z.id in H. 2:now right;intuition.
unfold prime in *.
destruct (Nat.eq_dec (n mod m) 0) as [H'|H']. all:rewrite Nat.mod_divide in H';[|lia]. all:intuition.
Qed.

End pf.
End pf.

(** You can ignore the above module. *)
Definition pf n:= (projT1 (pf.pf_computable n)).

Definition pf_spec n :
2 <= n -> primeDivisorOf n (pf n) /\ forall k, primeDivisorOf n k -> pf n <= k.
Proof.
unfold pf. destruct pf.pf_computable. eauto.
Qed.
```

### Template File

```Require Import Defs.

(** * Task 1*)
Lemma prime_pf_S_fS (n:nat):
prime (pf (fS n + 1)).
Proof.
Admitted.

(** * Task2 *)
Lemma pf_fS_inj (n m:nat) :
pf (fS n + 1) = pf (fS m + 1)
-> n = m.
Proof.
Admitted.

(** * Final Conclusion *)
Require Import List Lia.

Lemma infinitely_many_primes':
forall n, exists L, n <= length L
/\ Forall prime L
/\ NoDup L.
Proof.
intros n. exists (map (fun i => pf(fS i + 1)) (seq 0 n)).
repeat split.
-now rewrite map_length,seq_length.
-apply Forall_forall. intros ? (?&<-&?)%in_map_iff.
eauto using prime_pf_S_fS.
-erewrite NoDup_nth with (d:= pf(fS 0 + 1)).
rewrite map_length,seq_length.
setoid_rewrite  map_nth with (d:=0)(f:=(fun i0 : nat => pf (fS i0 + 1))). intros ? ? ? ? H'. setoid_rewrite seq_nth in H'. cbn in H'. 2-3:nia.
now apply pf_fS_inj.
Qed.
```

Terms and Conditions