[Proof Ground 2020] Infinitude Of Primes

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

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. 

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