open import 1Lab.Prelude

open import Data.Wellfounded.Properties
open import Data.Nat.Divisible.GCD
open import Data.List.Quantifiers
open import Data.Wellfounded.Base
open import Data.List.Membership
open import Data.Fin.Properties
open import Data.Nat.Properties
open import Data.Nat.Divisible
open import Data.Nat.DivMod
open import Data.List.Base
open import Data.Nat.Order
open import Data.Fin.Base renaming (_β€_ to _β€αΆ _) hiding (_<_)
open import Data.Nat.Base
open import Data.Dec
open import Data.Sum

module Data.Nat.Prime where


Prime and composite numbersπ

A number is prime when it is greater than two (which we split into being positive and being apart from 1), and, if is any other number that divides then either or Since weβve assumed 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 and then does not divide

  Β¬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

  prime>1 : 1 < n
prime>1 = <-from-β€ (primeβ 1 β sym) positive

private unquoteDecl eqv = declare-record-iso eqv (quote is-prime)
open is-prime

abstract instance
H-Level-is-prime : β {n k} β H-Level (is-prime n) (suc k)
H-Level-is-prime = prop-instance $Isoβis-hlevel 1 eqv$ Ξ£-is-hlevel 1 (hlevel 1) Ξ» p β
Ξ£-is-hlevel 1 (hlevel 1) Ξ» q β Ξ -is-hlevelΒ² 1 Ξ» d dn β
disjoint-β-is-prop (hlevel 1) (hlevel 1) (Ξ» (a , b) β q (sym b β a))


Conversely, if 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 and a number such that and is the smallest divisor of

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 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)))

open is-composite hiding (p ; q ; factors)

private unquoteDecl eqv' = declare-record-iso eqv' (quote is-composite)

abstract instance
H-Level-is-composite : β {n k} β H-Level (is-composite n) (suc k)
H-Level-is-composite = prop-instance Ξ» a@record{p = p ; q = q} b@record{p = p' ; q = q'} β
let
open is-composite using (factors)

ap=bp : p β‘ p'
ap=bp = β€-antisym
(a .least p' (prime>1 (b .p-prime)) (fibreββ£ (q' , b .factors)))
(b .least p (prime>1 (a .p-prime)) (fibreββ£ (q , a .factors)))

aq=bq : q β‘ q'
aq=bq = *-injl p q q' (*-commutative p q β a .factors β sym (b .factors) β ap (q' *_) (sym ap=bp) β *-commutative q' p)
in Equiv.injective (IsoβEquiv eqv') (Ξ£-pathp ap=bp (Ξ£-prop-pathp! aq=bq))

prime-divisor-lt : β p q n .β¦ _ : Positive n β¦ β is-prime p β q * p β‘ n β q < n
prime-divisor-lt p q n pprime div with β€-strengthen (mβ£nβmβ€n {q} {n} (fibreββ£ (p , *-commutative p q β div)))
... | inr less = less
... | inl same = absurd (pprime .primeβ 1 $*-injr n p 1 (sym (+-zeror n β sym div β *-commutative q p β ap (p *_) same))) prime-remainder-positive : β p q n .β¦ _ : Positive n β¦ β Β¬ is-prime n β is-prime p β q * p β‘ n β 1 < q prime-remainder-positive p 0 n@(suc _) _ _ div = absurd (zeroβ suc div) prime-remainder-positive p 1 n@(suc _) nn pp div = absurd (nn (subst is-prime (sym (+-zeror p) β div) pp)) prime-remainder-positive p (suc (suc _)) (suc _) _ _ _ = sβ€s (sβ€s 0β€x) distinct-primesβcoprime : β {a b} β is-prime a β is-prime b β Β¬ a β‘ b β is-gcd a b 1 distinct-primesβcoprime {a@(suc a')} {b@(suc b')} apr bpr aβ b = record { gcd-β£l = a , *-oner a ; gcd-β£r = b , *-oner b ; greatest = Ξ» {g'} w2 w β case bpr .primality _ w of Ξ» where (inl p) β subst (_β£ 1) (sym p) β£-refl (inr q) β case apr .primality _ w2 of Ξ» where (inl p) β subst (_β£ 1) (sym p) β£-refl (inr r) β absurd (aβ b (sym r β q)) }  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 : β 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')