Cookies disclaimer

I agree 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

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