Prime (and composite) numbers

Cubical/Data/Nat/Primes/Base.agda

@@ -0,0 +1,25 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.Base where
+
+open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Data.Nat.Primes.Lemmas using (1<·1<=3<)
+
+
+record isPrime (n : ℕ) : Type where
+    constructor prime
+    field
+        n-proper : 1 < n
+        primality : ∀ d → d ∣ n → (d ≡ 1) ⊎ (d ≡ n)
+
+record isComposite (n : ℕ) : Type where
+    constructor composite
+    field
+        p q : ℕ
+        p-prime  : isPrime p
+        q-proper : 1 < q
+        factors : p · q ≡ n
+        least : ∀ z → 1 < z → z ∣ n → p ≤ z
+
+    3<n : 3 < n
+    3<n = subst (λ x → 3 < x) factors (1<·1<=3< (isPrime.n-proper p-prime) q-proper)

Cubical/Data/Nat/Primes/Concrete.agda

@@ -0,0 +1,52 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.Concrete where
+
+open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Data.Nat.Primes.Lemmas
+open import Cubical.Data.Nat.Primes.Base
+open import Cubical.Data.Empty as ⊥ hiding (elim)
+
+
+prime2 : isPrime 2
+prime2 = prime (0 , refl) primality-2 where
+    primality-2 : (d : ℕ) → d ∣ 2 → (d ≡ 1) ⊎ (d ≡ 2)
+    primality-2 d d∣2 with (≤-split (m∣n→m≤n snotz d∣2))
+    ... | inr d=2 = inr d=2
+    ... | inl d<2 with <-split d<2
+    ... | inr d=1 = inl d=1
+    ... | inl d<1 = ⊥.rec (¬<1∣sn d 1 d<1 d∣2)
+
+
+private
+
+    -- can be used to directly prove primality of a specific number
+    notDiv : ∀ d n → Σ[ k ∈ ℕ ] (k · d < n) × (n < suc k · d) → ¬ d ∣ n
+    notDiv d n (k , kd<n , n<d+kd) d∣n-trunc
+        with d | (∣-untrunc d∣n-trunc) | (fst (∣-untrunc d∣n-trunc) ≟ k)
+    ...       | d | (c , cd=n) | (eq c=k) = <≠ kd<n (subst (λ x → x · d ≡ n) c=k cd=n)
+    ...       | 0 | (c , cd=n) | (lt c<k) = ¬-<-zero (subst (λ x → k · 0 < x)
+                                                            (sym (cd=n) ∙ sym (0≡m·0 c))
+                                                            kd<n)
+    ... | suc d-1 | (c , cd=n) | (lt c<k) = <≠ (lem1 c k d-1 n c<k kd<n) cd=n
+    ...       | d | (0 , cd=n) | (gt k<c) = ¬-<-zero k<c
+    ... | d | (suc c , d+cd=n) | (gt k<sc) with (<-split k<sc)
+    ...                        | inr k=c = <≠ n<d+kd
+                                           (sym (subst (λ x → d + x · d ≡ n) (sym k=c) d+cd=n))
+    ...                        | inl k<c = <≠ (lem2 c k d n k<c n<d+kd) (sym d+cd=n)
+
+    -- example
+    prime5 : isPrime 5
+    prime5 = prime (3 , refl) primality-5 where
+        primality-5 : (d : ℕ) → d ∣ 5 → (d ≡ 1) ⊎ (d ≡ 5)
+        primality-5 d d∣5 with (≤-split (m∣n→m≤n snotz d∣5))
+        ... | inr d=5 = inr d=5
+        ... | inl d<5 with <-split d<5
+        ... | inr d=4 = ⊥.rec (notDiv 4 5 (1 , (0 , refl) , (2 , refl)) (subst (λ x → x ∣ 5) d=4 d∣5))
+        ... | inl d<4 with <-split d<4
+        ... | inr d=3 = ⊥.rec (notDiv 3 5 (1 , (1 , refl) , (0 , refl)) (subst (λ x → x ∣ 5) d=3 d∣5))
+        ... | inl d<3 with <-split d<3
+        ... | inr d=2 = ⊥.rec (notDiv 2 5 (2 , (0 , refl) , (0 , refl)) (subst (λ x → x ∣ 5) d=2 d∣5))
+        ... | inl d<2 with <-split d<2
+        ... | inr d=1 = inl d=1
+        ... | inl d<1 = ⊥.rec (¬<1∣sn d 4 d<1 d∣5)

Cubical/Data/Nat/Primes/DecProps.agda

@@ -0,0 +1,104 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.DecProps where
+
+open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Data.Nat.Primes.Lemmas
+open import Cubical.Data.Nat.Primes.Base
+open import Cubical.Data.Nat.Primes.Factors
+open import Cubical.Data.Empty as ⊥ hiding (elim)
+open import Cubical.Data.Sum.Properties
+
+open isPrime
+open isComposite
+
+
+private
+    variable
+        ℓ ℓ' : Level
+
+    funcProp : {A : Type ℓ} {B : A → Type ℓ'} → (∀ a → isProp (B a)) → isProp (∀ a → B a)
+    funcProp BProp f g = funExt (λ x → BProp x (f x) (g x))
+
+    PropIso : ∀ {A : Type ℓ} {B : Type ℓ'} → isProp A → isProp B → (A → B) → (B → A) → Iso A B
+    PropIso propA propB fun inv = iso fun inv (λ _ → propB _ _) (λ _ → propA _ _)
+
+primeProp : ∀ n → isProp (isPrime n)
+primeProp n (prime 1<n primality) (prime 1<n' primality') =
+    cong₂ prime
+    (isProp≤ 1<n 1<n')
+    (funcProp  (λ x → funcProp  (λ x∣n →
+    isProp⊎ (isSetℕ x 1) (isSetℕ x n)
+    λ x=1 x=n → ¬n<n (subst (λ y → y < n) (sym x=1 ∙ x=n) 1<n)
+    ))
+    primality primality' )
+
+compProp : ∀ n → isProp (isComposite n)
+compProp n (composite p q pp 1<q pq=n least) (composite p' q' pp' 1<q' pq=n' least') =
+    λ i → composite
+    (p=p' i)
+    (q=q' i)
+    ((isProp→PathP (λ j → primeProp (p=p' j)) pp pp') i)
+    ((isProp→PathP (λ j → isProp≤ {n = q=q' j}) 1<q 1<q') i)
+    ((isProp→PathP (λ j → isSetℕ (p=p' j · q=q' j) n) pq=n pq=n') i)
+    ((isProp→PathP (λ j → leastProp (p=p' j)) least least') i)
+    where
+        1<p : 1 < p
+        1<p = n-proper pp
+        1<p' : 1 < p'
+        1<p' = n-proper pp'
+
+        p∣n : p ∣ n
+        p∣n = ∣ (q , ·-comm q p ∙ pq=n) ∣₁
+        p'∣n : p' ∣ n
+        p'∣n = ∣ (q' , ·-comm q' p' ∙ pq=n') ∣₁
+
+        p=p' : p ≡ p'
+        p=p' = ≤-antisym (least p' 1<p' p'∣n) (least' p 1<p p∣n)
+
+        q=q' : q ≡ q'
+        q=q' = inj-·0< q q' (<-weaken 1<p) (pq=n ∙ sym (subst (λ x → x · q' ≡ n) (sym p=p') pq=n'))
+
+        leastProp : ∀ x → isProp ((p'' : ℕ) → 1 < p'' → p'' ∣ n → x ≤ p'')
+        leastProp x = funcProp (λ a → funcProp (λ 1<a → funcProp (λ a∣n → isProp≤)))
+
+prime→¬comp : ∀ n → isPrime n → ¬ isComposite n
+prime→¬comp n (prime 1<n primality) (composite p q pp 1<q pq=n _)
+    with (primality q ∣ (p , pq=n) ∣₁)
+... | inl q=1 = <≠ 1<q (sym q=1)
+... | inr q=n = <≠ (PropFac< q p n (n-proper pp) (<-weaken 1<n) (·-comm q p ∙ pq=n)) q=n
+
+¬comp→prime : ∀ n → 1 < n → ¬ isComposite n → isPrime n
+¬comp→prime n 1<n ¬nc with primeOrComp n 1<n
+... | inl np = np
+... | inr nc = ⊥.rec (¬nc nc)
+
+comp→¬prime : ∀ n → isComposite n → ¬ isPrime n
+comp→¬prime n nc np = prime→¬comp n np nc
+
+¬prime→comp : ∀ n → 1 < n → ¬ isPrime n → isComposite n
+¬prime→comp n 1<n ¬np with primeOrComp n 1<n
+... | inr nc = nc
+... | inl np = ⊥.rec (¬np np)
+
+prime≡¬comp : ∀ n → 1 < n → (isPrime n) ≡ (¬ isComposite n)
+prime≡¬comp n 1<n =
+    isoToPath (PropIso (primeProp n) (isProp¬ (isComposite n)) (prime→¬comp n) (¬comp→prime n 1<n))
+
+comp≡¬prime : ∀ n → 1 < n → (isComposite n) ≡ (¬ isPrime n)
+comp≡¬prime n 1<n =
+    isoToPath (PropIso (compProp n) (isProp¬ (isPrime n)) (comp→¬prime n) (¬prime→comp n 1<n))
+
+DecPrime : ∀ n → Dec (isPrime n)
+DecPrime 0 = no λ (prime 1<0 _) → ¬-<-zero 1<0
+DecPrime 1 = no λ (prime 1<1 _) → ¬n<n 1<1
+DecPrime n@(suc (suc n-2)) with (primeOrComp n (n-2 , +-comm n-2 2))
+... | inl np = yes np
+... | inr nc = no (comp→¬prime n nc)
+
+DecComp : ∀ n → Dec (isComposite n)
+DecComp 0 = no λ 0c → ¬n<n (<-trans (2 , refl) (isComposite.3<n 0c))
+DecComp 1 = no λ 1c → ¬n<n (<-trans (1 , refl) (isComposite.3<n 1c))
+DecComp n@(suc (suc n-2)) with (primeOrComp n (n-2 , +-comm n-2 2))
+... | inr nc = yes nc
+... | inl np = no (prime→¬comp n np)

Cubical/Data/Nat/Primes/Factors.agda

@@ -0,0 +1,109 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.Factors where
+
+open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Data.Nat.Primes.Lemmas
+open import Cubical.Data.Nat.Primes.Base
+open import Cubical.Data.Empty as ⊥ hiding (elim)
+
+
+leastFactorIsPrime : ∀ n p → HasFactor n p → (∀ d → HasFactor n d → p ≤ d) → isPrime p
+leastFactorIsPrime _ 0 (1<p , _) _ = ⊥.rec (¬-<-zero 1<p)
+leastFactorIsPrime n p@(suc p-1) (1<p , p∣n) least = prime 1<p primality where
+    primality : ∀ (d : ℕ) → d ∣ p → (d ≡ 1) ⊎ (d ≡ p)
+    primality zero d∣p = ⊥.rec (¬z∣sn p-1 d∣p)
+    primality d@(suc d-1) d∣p with ≤-split (m∣n→m≤n snotz d∣p)
+    ... | inr d=p = inr d=p
+    ... | inl d<p with (d ≟ 1)
+    ... | eq d=1 = inl d=1
+    ... | lt d<1 = ⊥.rec (¬s<1 d<1)
+    ... | gt 1<d = ⊥.rec (<-asym d<p (least d (1<d , ∣-trans d∣p p∣n)))
+
+
+primeOrComp : ∀ n → 1 < n → (isPrime n) ⊎ (isComposite n)
+primeOrComp zero 1<0 = ⊥.rec (¬-<-zero 1<0)
+primeOrComp n@(suc n-1) 1<n = answer where
+
+    LF : Σ[ p ∈ ℕ ] (HasFactor n p) × (∀ z → (HasFactor n z) → p ≤ z)
+    LF = findLeast (1<n , ∣-refl refl) DecHF
+
+    p = LF .fst
+    HFnp = LF .snd .fst
+    1<p = HFnp .fst
+    p∣n = ∣-untrunc (HFnp .snd)
+    q = p∣n .fst
+    p≤n = m∣n→m≤n snotz (HFnp .snd)
+    pq=n = ·-comm p q ∙ p∣n .snd
+
+    p-least : ∀ z → (HasFactor n z) → p ≤ z
+    p-least = LF .snd .snd
+
+    p-prime : isPrime p
+    p-prime = leastFactorIsPrime n p HFnp p-least
+
+    answer : (isPrime n) ⊎ (isComposite n)
+    answer with (Dichotomyℕ n p)
+    ... | inl n≤p = inl (subst (λ x → isPrime x) (≤-antisym p≤n n≤p) p-prime)
+    ... | inr p<n = inr (composite p q p-prime 1<q pq=n (λ z 1<z z∣n → p-least z (1<z , z∣n)))
+            where
+                1<q : 1 < q
+                1<q with (1 ≟ q)
+                ... | lt 1<q = 1<q
+                ... | gt q<1 = ⊥.rec (1<→¬=0 n 1<n
+                                     (sym pq=n ∙ cong (p ·_) (<1→0 q q<1) ∙ sym (0≡m·0 p)))
+                ... | eq 1=q = ⊥.rec (¬n<n (subst (λ x → x < n)
+                                                  (subst
+                                                        (λ x → p ≡ p · x)
+                                                        1=q
+                                                        (sym (·-identityʳ p)) ∙ pq=n)
+                                                  p<n))
+
+newPrime : ∀ n → Σ[ p ∈ ℕ ] (n < p) × (isPrime p)
+newPrime n with primeOrComp (suc (factorial n)) (suc< (0<factorial n))
+... | inl sfnp = (suc (factorial n)) , suc-≤-suc (n≤! n) , sfnp
+... | inr (composite p q pp 1<q pq=n least) with Dichotomyℕ p n
+... | inr n<p = p , n<p , pp
+... | inl p≤n = ⊥.rec (<≠ 1<p (sym (div1→1 p p∣1))) where
+        1<p = pp .isPrime.n-proper
+        p∣1 : p ∣ 1
+        p∣1 = ∣+-cancel p 1 (n !) (≤n∣n! p n p≤n (1<→¬=0 p 1<p)) (∥_∥₁.∣ q , ·-comm q p ∙ pq=n ∣₁)
+
+
+record PrimeFactors (n : ℕ) : Type where
+    no-eta-equality
+    constructor pfs
+    field
+        primes : List ℕ
+        factored : product primes ≡ n
+        allPrime : All isPrime primes
+open PrimeFactors
+
+PF-prime : ∀ n → isPrime n → PrimeFactors n
+PF-prime n np = pfs (n ∷ []) (·-identityʳ n) (np ∷ [])
+
+PF-comp-work : ∀ n → (∀ m → m < n → isComposite m → PrimeFactors m) → isComposite n →
+               PrimeFactors n
+PF-comp-work n rec nComp@(composite p q p-prime 1<q pq=n _) =
+    pfs (p ∷ primes qFacs)
+        (subst (λ x → p · x ≡ n) (sym (factored qFacs)) pq=n)
+        (p-prime ∷ allPrime qFacs)
+        where
+            qFacs : PrimeFactors q
+            qFacs with (primeOrComp q 1<q)
+            ... | inl qp = PF-prime q qp
+            ... | inr qc = rec q (PropFac< q p n 1<p 0<n (·-comm q p ∙ pq=n)) qc where
+                    1<p = isPrime.n-proper p-prime
+                    0<n = <-trans (2 , refl) (isComposite.3<n nComp)
+
+PF-comp : ∀ n → isComposite n → PrimeFactors n
+PF-comp = WFI.induction <-wellfounded PF-comp-work
+
+PF-aux : ∀ n → (isPrime n) ⊎ (isComposite n) → PrimeFactors n
+PF-aux n (inl np) = PF-prime n np
+PF-aux n (inr nc) = PF-comp n nc
+
+factorize : ∀ n → 0 < n  → PrimeFactors n
+factorize 0 0<0 = ⊥.rec (¬n<n 0<0)
+factorize 1 _ = pfs [] refl []
+factorize n@(suc (suc n-2)) _ = PF-aux n (primeOrComp n (n-2 , +-comm n-2 2))

Cubical/Data/Nat/Primes/Imports.agda

@@ -0,0 +1,20 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.Imports where
+
+open import Cubical.Foundations.Prelude public
+open import Cubical.Foundations.Function public
+open import Cubical.Foundations.Isomorphism public
+
+open import Cubical.Data.Nat hiding (elim) public
+open import Cubical.Data.Nat.Order public
+open import Cubical.Data.Nat.Divisibility public
+open import Cubical.Data.Empty as ⊥ hiding (elim) public
+open import Cubical.Data.Unit public
+open import Cubical.Data.Sigma public
+open import Cubical.Data.List hiding (elim ; rec ; map) public
+open import Cubical.Data.Sum hiding (elim ; rec ; map) public
+open import Cubical.Relation.Nullary public
+open import Cubical.HITs.PropositionalTruncation hiding (map2 ; rec) public
+open import Cubical.Induction.WellFounded public
+open import Cubical.Data.Fin hiding (elim) public

Cubical/Data/Nat/Primes/Infinitude.agda

@@ -0,0 +1,61 @@
+{-# OPTIONS --safe -W noUnsupportedIndexedMatch #-}
+
+module Cubical.Data.Nat.Primes.Infinitude where
+
+open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Data.Nat.Primes.Lemmas
+open import Cubical.Data.Nat.Primes.Base
+open import Cubical.Data.Nat.Primes.Split
+open import Cubical.Data.Nat.Primes.Concrete
+open import Cubical.Data.Nat.Primes.Factors
+open import Cubical.Data.Nat.Primes.DecProps
+
+
+nextPrime : (n : ℕ) → Σ[ p ∈ ℕ ] ((n < p) × (isPrime p)) × ((z : ℕ) → (n < z) × isPrime z → p ≤ z)
+nextPrime n = findLeast (((newPrime n) .snd)) (DecProd (<Dec n) DecPrime)
+
+nthPrime : (n : ℕ) → Σ[ p ∈ ℕ ] isPrime p × (countBelow isPrime DecPrime p ≡ n)
+nthPrime zero = (least-prime .fst , least-prime .snd .fst , refl) where
+    least-prime = findLeast prime2 DecPrime
+nthPrime (suc n) = (next-prime .fst , next-prime .snd .fst .snd , snprimes) where
+    IH = nthPrime n
+
+    p#n = IH .fst
+    p#n-prime = IH .snd .fst
+    #p<p#n=n = IH .snd .snd
+
+    next-prime : Σ[ q ∈ ℕ ] ((p#n < q) × isPrime q) × (∀ z → (p#n < z) × isPrime z → q ≤ z)
+    next-prime = nextPrime p#n
+
+    q = next-prime .fst
+    p#n<q = next-prime .snd .fst .fst
+    p#n≤q = <-weaken p#n<q
+    q-prime = next-prime .snd .fst .snd
+    q-least = next-prime .snd .snd
+
+    sum : countBelow isPrime DecPrime q
+          ≡ countRange isPrime DecPrime p#n q p#n≤q + countBelow isPrime DecPrime p#n
+    sum = sym (countWorks isPrime DecPrime p#n q p#n≤q)
+    p1 : countRange isPrime DecPrime p#n q p#n≤q ≡ 1
+    p1 = leastAboveLow isPrime DecPrime p#n q p#n-prime
+         (isPropDec (primeProp p#n) (DecPrime p#n) (yes p#n-prime))
+         q-least p#n<q
+
+    snprimes : countBelow isPrime DecPrime q ≡ suc n
+    snprimes = sum ∙ add-equations p1 #p<p#n=n
+
+
+open Iso
+ℕ≅primeℕ : Iso ℕ (Σ ℕ isPrime)
+fun      ℕ≅primeℕ n = (pn .fst , pn .snd .fst) where pn = nthPrime n
+inv      ℕ≅primeℕ (p , _) = countBelow isPrime DecPrime p
+leftInv  ℕ≅primeℕ n = nthPrime n .snd .snd
+rightInv ℕ≅primeℕ (p , p-prime) =
+    ΣPathP (answer , isProp→PathP (λ i → primeProp (answer i)) pn-prime p-prime) where
+        pn = nthPrime (countBelow isPrime DecPrime p)
+        pn-prime = pn .snd .fst
+        answer : pn .fst ≡ p
+        answer = countBelowYesInj isPrime DecPrime (pn .fst) p pn-prime p-prime
+                 (isPropDec (primeProp (pn .fst)) (DecPrime (pn .fst)) (yes pn-prime))
+                 (isPropDec (primeProp p) (DecPrime p) (yes p-prime))
+                 (pn .snd .snd)