module Data.Nat.Prime where

Prime and composite numbers🔗

A number $n$ is prime when it is greater than two (which we split into being positive and being apart from 1), and, if $d$ is any other number that divides $n,$ then either $d = 1$ or $d = n .$ Since we’ve assumed $n \neq = 1,$ these cases are disjoint, so being a prime is a proposition.

record is-prime (n : Nat) : Type where
  field
    ⦃ positive ⦄ : Positive n
    prime≠1   : n ≠ 1
    primality : ∀ d → d ∣ n → (d ≡ 1) ⊎ (d ≡ n)

We note that a prime number has no proper divisors, in that, if $d \neq = 1$ and $d \neq = n,$ then $d$ does not divide $n .$

  ¬proper-divisor : ∀ {d} → d ≠ 1 → d ≠ n → ¬ d ∣ n
  ¬proper-divisor ¬d=1 ¬d=n d∣n with primality _ d∣n
  ... | inl d=1 = ¬d=1 d=1
  ... | inr d=n = ¬d=n d=n

Conversely, if $n > 2$ is a number that is not prime, it is called composite. Instead of defining is-composite to be the literal negation of is-prime, we instead define this notion positively: To say that a number is composite is to give a prime $p$ and a number $q \geq 2$ such that $qp = n$ and $p$ is the smallest divisor of $n .$

record is-composite (n : Nat) : Type where
  field
    {p q} : Nat

    p-prime  : is-prime p
    q-proper : 1 < q

    factors : q * p ≡ n
    least : ∀ p' → 1 < p' → p' ∣ n → p ≤ p'

Note that the assumption that $p$ is a prime is simply for convenience: the least proper divisor of any number is always a prime.

least-divisor→is-prime
  : ∀ p n → 1 < p → p ∣ n → (∀ p' → 1 < p' → p' ∣ n → p ≤ p') → is-prime p
least-divisor→is-prime p n gt div least .positive = ≤-trans ≤-ascend gt
least-divisor→is-prime p n gt div least .prime≠1 q = <-irrefl (sym q) gt
least-divisor→is-prime p@(suc p') n gt div least .primality 0 x = absurd (suc≠zero x)
least-divisor→is-prime p@(suc p') n gt div least .primality 1 x = inl refl
least-divisor→is-prime p@(suc p') n gt div least .primality m@(suc (suc k)) x =
  inr (≤-antisym (m∣sn→m≤sn x) (least m (s≤s (s≤s 0≤x)) (∣-trans x div)))

Primality testing🔗

is-prime-or-composite : ∀ n → 1 < n → is-prime n ⊎ is-composite n
is-prime-or-composite n@(suc (suc m)) (s≤s p)
  with Fin-omniscience {n = n} (λ k → 1 < to-nat k × to-nat k ∣ n)
... | inr prime = inl record { prime≠1 = suc≠zero ∘ suc-inj ; primality = no-divisors→prime } where
  no-divisors→prime : ∀ d → d ∣ n → d ≡ 1 ⊎ d ≡ n
  no-divisors→prime d div with d ≡? 1
  ... | yes p = inl p
  ... | no ¬d=1 with d ≡? n
  ... | yes p = inr p
  ... | no ¬d=n =
    let
      ord : d < n
      ord = proper-divisor-< ¬d=n div

      coh : d ≡ to-nat (from-ℕ< (d , ord))
      coh = sym (ap fst (to-from-ℕ< (d , ord)))

      no = case d return (λ x → ¬ x ≡ 1 → x ∣ n → 1 < x) of λ where
        0 p1 div → absurd (<-irrefl (sym div) (s≤s 0≤x))
        1 p1 div → absurd (p1 refl)
        (suc (suc n)) p1 div → s≤s (s≤s 0≤x)
    in absurd (prime (from-ℕ< (d , ord)) ((subst (1 <_) coh (no ¬d=1 div)) , subst (_∣ n) coh div))
... | inl (ix , (proper , div) , least)
  = inr record { p-prime = prime ; q-proper = proper' ; factors = path ; least = least' } where
  open Σ (∣→fibre div) renaming (fst to quot ; snd to path)

  abstract
    least' : (p' : Nat) → 1 < p' → p' ∣ n → to-nat ix ≤ p'
    least' p' x div with ≤-strengthen (m∣n→m≤n div)
    ... | inl same = ≤-trans ≤-ascend (subst (to-nat ix <_) (sym same) (to-ℕ< ix .snd))
    ... | inr less =
      let
        it : ℕ< n
        it = p' , less

        coh : p' ≡ to-nat (from-ℕ< it)
        coh = sym (ap fst (to-from-ℕ< it))

        orig = least (from-ℕ< it) (subst (1 <_) coh x , subst (_∣ n) coh div)
      in ≤-trans orig (subst (to-nat (from-ℕ< it) ≤_) (sym coh) ≤-refl)

  prime : is-prime (to-nat ix)
  prime = least-divisor→is-prime (to-nat ix) n proper div least'

  proper' : 1 < quot
  proper' with quot | path
  ... | 0 | q = absurd (<-irrefl q (s≤s 0≤x))
  ... | 1 | q = absurd (<-irrefl (sym (+-zeror (to-nat ix)) ∙ q) (to-ℕ< ix .snd))
  ... | suc (suc n) | p = s≤s (s≤s 0≤x)

record Factorisation (n : Nat) : Type where
  constructor factored
  field
    primes    : List Nat
    factors   : product primes ≡ n
    is-primes : All is-prime primes

  prime-divides : ∀ {x} → x ∈ₗ primes → x ∣ n
  prime-divides {x} h = subst (x ∣_) factors (work _ _ h) where
    work : ∀ x xs → x ∈ₗ xs → x ∣ product xs
    work x (y ∷ xs) (here p) = subst (λ e → x ∣ e * product xs) p (∣-*l {x} {product xs})
    work x (y ∷ xs) (there p) =
      let
        it = work x xs p
        (div , p) = ∣→fibre it
      in fibre→∣ (y * div , *-associative y div x ∙ ap (y *_) p)

  find-prime-factor : ∀ {x} → is-prime x → x ∣ n → x ∈ₗ primes
  find-prime-factor {num} x d =
    work _ primes x (λ _ → all-∈ is-primes) (subst (num ∣_) (sym factors) d)
    where
    work : ∀ x xs → is-prime x → (∀ x → x ∈ₗ xs → is-prime x) → x ∣ product xs → x ∈ₗ xs
    work x [] xp ps xd = absurd (prime≠1 xp (∣-1 xd))
    work x (y ∷ xs) xp ps xd with x ≡? y
    ... | yes x=y = here x=y
    ... | no ¬p = there $ work x xs xp (λ x w → ps x (there w))
      (|-*-coprime-cancel x y (product xs)
        ⦃ auto ⦄ ⦃ ps y (here refl) .positive ⦄
        xd (distinct-primes→coprime xp (ps y (here refl)) ¬p))

open is-composite using (factors)
open Factorisation

factorisation-unique' : ∀ {n} (a b : Factorisation n) → ∀ p → p ∈ₗ a .primes → p ∈ₗ b .primes
factorisation-unique' a b p p∈a =
  let
    p∣n = prime-divides a p∈a
  in find-prime-factor b (all-∈ (a .is-primes) p∈a) p∣n

factorisation-worker
  : ∀ n → (∀ k → k < n → .⦃ _ : Positive k ⦄ → Factorisation k)
  → .⦃ _ : Positive n ⦄ → Factorisation n
factorisation-worker 1 ind = factored [] refl []
factorisation-worker n@(suc (suc m)) ind with is-prime-or-composite n (s≤s (s≤s 0≤x))
... | inl prime     = factored (n ∷ []) (ap (2 +_) (*-oner m)) (prime ∷ [])
... | inr composite@record{p = p; q = q} =
  let
    instance
      _ : Positive q
      _ = ≤-trans ≤-ascend (composite .q-proper)

    factored ps path primes = ind q $
      prime-divisor-lt p q n (composite .p-prime) (composite .factors)
  in record
    { primes    = p ∷ ps
    ; factors   = ap (p *_) path ·· *-commutative p q ·· composite .factors
    ; is-primes = composite .p-prime ∷ primes
    }

factorial : Nat → Nat
factorial zero = 1
factorial (suc n) = suc n * factorial n

factorial-positive : ∀ n → Positive (factorial n)
factorial-positive zero = s≤s 0≤x
factorial-positive (suc n) = *-preserves-≤ 1 (suc n) 1 (factorial n) (s≤s 0≤x) (factorial-positive n)

≤-factorial : ∀ n → n ≤ factorial n
≤-factorial zero = 0≤x
≤-factorial (suc n) = subst (_≤ factorial (suc n)) (*-oner (suc n)) (*-preserves-≤ (suc n) (suc n) 1 (factorial n) ≤-refl (factorial-positive n))

∣-factorial : ∀ n {m} → m < n → suc m ∣ factorial n
∣-factorial (suc n) {m} m≤n with suc m ≡? suc n
... | yes m=n = subst (_∣ factorial (suc n)) (sym m=n) (∣-*l {suc n} {factorial n})
... | no m≠n  = |-*l-pres {suc m} {suc n} {factorial n} $
  ∣-factorial n {m} (≤-uncap (suc m) n m≠n m≤n)

factorise : (n : Nat) .⦃ _ : Positive n ⦄ → Factorisation n
factorise = Wf-induction _<_ <-wf _ factorisation-worker

new-prime : (n : Nat) → Σ[ p ∈ Nat ] n < p × is-prime p
new-prime n with is-prime-or-composite (suc (factorial n)) (s≤s (factorial-positive n))
new-prime n | inl prime     = suc (factorial n) , s≤s (≤-factorial n) , prime
new-prime n | inr c@record{p = p} with holds? (suc n ≤ p)
new-prime n | inr c@record{p = p} | yes n<p = p , n<p , c .p-prime
new-prime n | inr c@record{p = suc p; q = q} | no ¬n<p =
  let
    rem = ∣-factorial n (<-from-not-≤ _ _ (¬n<p ∘ s≤s))
    rem' : suc p ≡ 1
    rem' = ∣-1 (∣-+-cancel' {n = suc p} {a = 1} {b = factorial n} rem (fibre→∣ (q , c .factors)))
  in absurd (c .p-prime .prime≠1 rem')