------------------------------------------------------------------------
-- The Agda standard library
--
-- Primality
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Nat.Primality where
open import Data.List.Base using ([]; _∷_)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
open import Data.Nat.Base
open import Data.Nat.Divisibility
open import Data.Nat.GCD using (module GCD; module Bézout)
open import Data.Nat.ListAction using (product)
open import Data.Nat.ListAction.Properties using (product≢0)
open import Data.Nat.Properties
open import Data.Product.Base using (∃-syntax; _×_; map₂; _,_)
open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function.Base using (flip; _∘_; _∘′_)
open import Function.Bundles using (_⇔_; mk⇔)
open import Relation.Nullary.Decidable as Dec
using (yes; no; from-yes; from-no; ¬?; _×-dec_; _⊎-dec_; _→-dec_; decidable-stable)
open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction₂)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; _≢_; refl; cong)
private
variable
d m n o p : ℕ
recompute-nonTrivial : .{{NonTrivial n}} → NonTrivial n
recompute-nonTrivial {n} {{nontrivial}} =
Dec.recompute (nonTrivial? n) nontrivial
------------------------------------------------------------------------
-- Definitions
------------------------------------------------------------------------
-- The positive/existential relation `BoundedNonTrivialDivisor` is
-- the basis for the whole development, as it captures the possible
-- non-trivial divisors of a given number; its complement, `Rough`,
-- therefore sets *lower* bounds on any possible such divisors.
-- The predicate `Composite` is then defined as the 'diagonal' instance
-- of `BoundedNonTrivialDivisor`, while `Prime` is essentially defined as
-- the complement of `Composite`. Finally, `Irreducible` is the positive
-- analogue of `Prime`.
------------------------------------------------------------------------
-- Roughness
-- A number is m-rough if all its non-trivial divisors are bounded below
-- by m.
infix 10 _Rough_
_Rough_ : ℕ → Pred ℕ _
m Rough n = ¬ (n HasNonTrivialDivisorLessThan m)
------------------------------------------------------------------------
-- Compositeness
-- A number is composite if it has a proper non-trivial divisor.
Composite : Pred ℕ _
Composite n = n HasNonTrivialDivisorLessThan n
-- A shorter pattern synonym for the record constructor producing a
-- witness for `Composite`.
pattern
composite {d} d<n d∣n = hasNonTrivialDivisor {divisor = d} d<n d∣n
------------------------------------------------------------------------
-- Primality
-- Prime as the complement of Composite (and hence the diagonal of Rough
-- as defined above). The constructor `prime` takes a proof `notComposite`
-- that NonTrivial p is not composite and thereby enforces that:
-- * p is a fortiori NonZero and NonUnit
-- * p is p-Rough, i.e. any proper divisor must be at least p, i.e. p itself
record Prime (p : ℕ) : Set where
constructor prime
field
.{{nontrivial}} : NonTrivial p
notComposite : ¬ Composite p
------------------------------------------------------------------------
-- Irreducibility
Irreducible : Pred ℕ _
Irreducible n = ∀ {d} → d ∣ n → d ≡ 1 ⊎ d ≡ n
------------------------------------------------------------------------
-- Properties
------------------------------------------------------------------------
------------------------------------------------------------------------
-- Roughness
-- 1 is always n-rough
rough-1 : ∀ n → n Rough 1
rough-1 _ (hasNonTrivialDivisor _ d∣1) =
contradiction (∣1⇒≡1 d∣1) nonTrivial⇒≢1
-- Any number is 0-, 1- and 2-rough,
-- because no proper divisor d can be strictly less than 0, 1, or 2
0-rough : 0 Rough n
0-rough (hasNonTrivialDivisor () _)
1-rough : 1 Rough n
1-rough (hasNonTrivialDivisor {{()}} z<s _)
2-rough : 2 Rough n
2-rough (hasNonTrivialDivisor {{()}} (s<s z<s) _)
-- If a number n > 1 is m-rough, then m ≤ n
rough⇒≤ : .{{NonTrivial n}} → m Rough n → m ≤ n
rough⇒≤ rough = ≮⇒≥ n≮m
where n≮m = λ m>n → rough (hasNonTrivialDivisor m>n ∣-refl)
-- If a number n is m-rough, and m ∤ n, then n is (suc m)-rough
∤⇒rough-suc : m ∤ n → m Rough n → (suc m) Rough n
∤⇒rough-suc m∤n r (hasNonTrivialDivisor d<1+m d∣n)
with m<1+n⇒m<n∨m≡n d<1+m
... | inj₁ d<m = r (hasNonTrivialDivisor d<m d∣n)
... | inj₂ d≡m@refl = contradiction d∣n m∤n
-- If a number is m-rough, then so are all of its divisors
rough∧∣⇒rough : m Rough o → n ∣ o → m Rough n
rough∧∣⇒rough r n∣o bntd = r (hasNonTrivialDivisor-∣ bntd n∣o)
------------------------------------------------------------------------
-- Compositeness
-- Smart constructors
composite-≢ : ∀ d → .{{NonTrivial d}} → .{{NonZero n}} →
d ≢ n → d ∣ n → Composite n
composite-≢ d = hasNonTrivialDivisor-≢ {d}
composite-∣ : .{{NonZero n}} → Composite m → m ∣ n → Composite n
composite-∣ (composite {d} d<m d∣n) m∣n@(divides-refl q)
= composite (*-monoʳ-< q d<m) (*-monoʳ-∣ q d∣n)
where instance
_ = m≢0∧n>1⇒m*n>1 q d
_ = m*n≢0⇒m≢0 q
-- Basic (counter-)examples of Composite
¬composite[0] : ¬ Composite 0
¬composite[0] = 0-rough
¬composite[1] : ¬ Composite 1
¬composite[1] = 1-rough
composite[4] : Composite 4
composite[4] = composite-≢ 2 (λ()) (divides-refl 2)
composite[6] : Composite 6
composite[6] = composite-≢ 3 (λ()) (divides-refl 2)
composite⇒nonZero : Composite n → NonZero n
composite⇒nonZero {suc _} _ = _
composite⇒nonTrivial : Composite n → NonTrivial n
composite⇒nonTrivial {1} composite[1] =
contradiction composite[1] ¬composite[1]
composite⇒nonTrivial {2+ _} _ = _
composite? : Decidable Composite
composite? n = Dec.map CompositeUpTo⇔Composite (compositeUpTo? n)
where
-- For technical reasons, in order to be able to prove decidability
-- via the `all?` and `any?` combinators for *bounded* predicates on
-- `ℕ`, we further define the bounded counterparts to predicates
-- `P...` as `P...UpTo` and show the equivalence of the two.
-- Equivalent bounded predicate definition
CompositeUpTo : Pred ℕ _
CompositeUpTo n = ∃[ d ] d < n × NonTrivial d × d ∣ n
-- Proof of equivalence
comp-upto⇒comp : CompositeUpTo n → Composite n
comp-upto⇒comp (_ , d<n , ntd , d∣n) = composite d<n d∣n
where instance _ = ntd
comp⇒comp-upto : Composite n → CompositeUpTo n
comp⇒comp-upto (composite d<n d∣n) = _ , d<n , recompute-nonTrivial , d∣n
CompositeUpTo⇔Composite : CompositeUpTo n ⇔ Composite n
CompositeUpTo⇔Composite = mk⇔ comp-upto⇒comp comp⇒comp-upto
-- Proof of decidability
compositeUpTo? : Decidable CompositeUpTo
compositeUpTo? n = anyUpTo? (λ d → nonTrivial? d ×-dec d ∣? n) n
------------------------------------------------------------------------
-- Primality
-- Basic (counter-)examples
¬prime[0] : ¬ Prime 0
¬prime[0] ()
¬prime[1] : ¬ Prime 1
¬prime[1] ()
prime[2] : Prime 2
prime[2] = prime 2-rough
prime⇒nonZero : Prime p → NonZero p
prime⇒nonZero _ = nonTrivial⇒nonZero _
prime⇒nonTrivial : Prime p → NonTrivial p
prime⇒nonTrivial _ = recompute-nonTrivial
prime? : Decidable Prime
prime? 0 = no ¬prime[0]
prime? 1 = no ¬prime[1]
prime? n@(2+ _) = Dec.map PrimeUpTo⇔Prime (primeUpTo? n)
where
-- Equivalent bounded predicate definition
PrimeUpTo : Pred ℕ _
PrimeUpTo n = ∀ {d} → d < n → NonTrivial d → d ∤ n
-- Proof of equivalence
prime⇒prime-upto : Prime n → PrimeUpTo n
prime⇒prime-upto (prime p) {d} d<n ntd d∣n
= p (composite d<n d∣n) where instance _ = ntd
prime-upto⇒prime : .{{NonTrivial n}} → PrimeUpTo n → Prime n
prime-upto⇒prime upto = prime
λ (composite d<n d∣n) → upto d<n recompute-nonTrivial d∣n
PrimeUpTo⇔Prime : .{{NonTrivial n}} → PrimeUpTo n ⇔ Prime n
PrimeUpTo⇔Prime = mk⇔ prime-upto⇒prime prime⇒prime-upto
-- Proof of decidability
primeUpTo? : Decidable PrimeUpTo
primeUpTo? n = allUpTo? (λ d → nonTrivial? d →-dec ¬? (d ∣? n)) n
-- Euclid's lemma - for p prime, if p ∣ m * n, then either p ∣ m or p ∣ n.
--
-- This demonstrates that the usual definition of prime numbers matches
-- the ring theoretic definition of a prime element of the semiring ℕ.
-- This is useful for proving many other theorems involving prime numbers.
euclidsLemma : ∀ m n {p} → Prime p → p ∣ m * n → p ∣ m ⊎ p ∣ n
euclidsLemma m n {p} pp@(prime pr) p∣m*n = result
where
open ∣-Reasoning
instance _ = prime⇒nonZero pp
p∣rmn : ∀ r → p ∣ r * m * n
p∣rmn r = begin
p ∣⟨ p∣m*n ⟩
m * n ∣⟨ n∣m*n r ⟩
r * (m * n) ≡⟨ *-assoc r m n ⟨
r * m * n ∎
result : p ∣ m ⊎ p ∣ n
result with Bézout.lemma m p
-- if the GCD of m and p is zero then p must be zero, which is
-- impossible as p is a prime.
-- note: this should be a typechecker-rejectable case!?
... | Bézout.result 0 g _ =
contradiction (0∣⇒≡0 (GCD.gcd∣n g)) (≢-nonZero⁻¹ _)
-- if the GCD of m and p is one then m and p are coprime, and we know
-- that for some integers s and r, sm + rp = 1. We can use this fact
-- to determine that p divides n
... | Bézout.result 1 _ (Bézout.+- r s 1+sp≡rm) =
inj₂ (flip ∣m+n∣m⇒∣n (n∣m*n*o s n) (begin
p ∣⟨ p∣rmn r ⟩
r * m * n ≡⟨ cong (_* n) 1+sp≡rm ⟨
n + s * p * n ≡⟨ +-comm n (s * p * n) ⟩
s * p * n + n ∎))
... | Bézout.result 1 _ (Bézout.-+ r s 1+rm≡sp) =
inj₂ (flip ∣m+n∣m⇒∣n (p∣rmn r) (begin
p ∣⟨ n∣m*n*o s n ⟩
s * p * n ≡⟨ cong (_* n) 1+rm≡sp ⟨
n + r * m * n ≡⟨ +-comm n (r * m * n) ⟩
r * m * n + n ∎))
-- if the GCD of m and p is greater than one, then it must be p and
-- hence p ∣ m.
... | Bézout.result d@(2+ _) g _ with d ≟ p
... | yes d≡p@refl = inj₁ (GCD.gcd∣m g)
... | no d≢p = contradiction (composite-≢ d d≢p (GCD.gcd∣n g)) pr
-- Relationship between roughness and primality.
prime⇒rough : Prime p → p Rough p
prime⇒rough (prime pr) = pr
-- If a number n is p-rough, and p > 1 divides n, then p must be prime
rough∧∣⇒prime : .{{NonTrivial p}} → p Rough n → p ∣ n → Prime p
rough∧∣⇒prime r p∣n = prime (rough∧∣⇒rough r p∣n)
-- If a number n is m-rough, and m * m > n, then n must be prime.
rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n
rough∧square>⇒prime rough m*m>n = prime ¬composite
where
¬composite : ¬ Composite _
¬composite (composite d<n d∣n) = contradiction (m∣n⇒n≡quotient*m d∣n)
(<⇒≢ (<-≤-trans m*m>n (*-mono-≤
(rough⇒≤ (rough∧∣⇒rough rough (quotient-∣ d∣n)))
(rough⇒≤ (rough∧∣⇒rough rough d∣n)))))
where instance _ = n>1⇒nonTrivial (quotient>1 d∣n d<n)
-- Relationship between compositeness and primality.
composite⇒¬prime : Composite n → ¬ Prime n
composite⇒¬prime composite[d] (prime p) = p composite[d]
¬composite⇒prime : .{{NonTrivial n}} → ¬ Composite n → Prime n
¬composite⇒prime = prime
prime⇒¬composite : Prime n → ¬ Composite n
prime⇒¬composite (prime p) = p
-- Note that this has to recompute the factor!
¬prime⇒composite : .{{NonTrivial n}} → ¬ Prime n → Composite n
¬prime⇒composite {n} ¬prime[n] =
decidable-stable (composite? n) (¬prime[n] ∘′ ¬composite⇒prime)
productOfPrimes≢0 : ∀ {as} → All Prime as → NonZero (product as)
productOfPrimes≢0 pas = product≢0 (All.map prime⇒nonZero pas)
productOfPrimes≥1 : ∀ {as} → All Prime as → product as ≥ 1
productOfPrimes≥1 {as} pas = >-nonZero⁻¹ _ {{productOfPrimes≢0 pas}}
------------------------------------------------------------------------
-- Basic (counter-)examples of Irreducible
¬irreducible[0] : ¬ Irreducible 0
¬irreducible[0] irr[0] = contradiction₂ 2≡1⊎2≡0 (λ ()) (λ ())
where 2≡1⊎2≡0 = irr[0] {2} (divides-refl 0)
irreducible[1] : Irreducible 1
irreducible[1] m∣1 = inj₁ (∣1⇒≡1 m∣1)
irreducible[2] : Irreducible 2
irreducible[2] {zero} 0∣2 with () ← 0∣⇒≡0 0∣2
irreducible[2] {suc _} d∣2 with ∣⇒≤ d∣2
... | z<s = inj₁ refl
... | s<s z<s = inj₂ refl
irreducible⇒nonZero : Irreducible n → NonZero n
irreducible⇒nonZero {zero} = flip contradiction ¬irreducible[0]
irreducible⇒nonZero {suc _} _ = _
irreducible? : Decidable Irreducible
irreducible? zero = no ¬irreducible[0]
irreducible? n@(suc _) =
Dec.map IrreducibleUpTo⇔Irreducible (irreducibleUpTo? n)
where
-- Equivalent bounded predicate definition
IrreducibleUpTo : Pred ℕ _
IrreducibleUpTo n = ∀ {d} → d < n → d ∣ n → d ≡ 1 ⊎ d ≡ n
-- Proof of equivalence
irr-upto⇒irr : .{{NonZero n}} → IrreducibleUpTo n → Irreducible n
irr-upto⇒irr irr-upto m∣n
= [ flip irr-upto m∣n , inj₂ ]′ (m≤n⇒m<n∨m≡n (∣⇒≤ m∣n))
irr⇒irr-upto : Irreducible n → IrreducibleUpTo n
irr⇒irr-upto irr m<n m∣n = irr m∣n
IrreducibleUpTo⇔Irreducible : .{{NonZero n}} →
IrreducibleUpTo n ⇔ Irreducible n
IrreducibleUpTo⇔Irreducible = mk⇔ irr-upto⇒irr irr⇒irr-upto
-- Decidability
irreducibleUpTo? : Decidable IrreducibleUpTo
irreducibleUpTo? n = allUpTo?
(λ m → (m ∣? n) →-dec (m ≟ 1 ⊎-dec m ≟ n)) n
-- Relationship between primality and irreducibility.
prime⇒irreducible : Prime p → Irreducible p
prime⇒irreducible {p} pp@(prime pr) = irr
where
instance _ = prime⇒nonZero pp
irr : .{{NonZero p}} → Irreducible p
irr {0} 0∣p = contradiction (0∣⇒≡0 0∣p) (≢-nonZero⁻¹ p)
irr {1} 1∣p = inj₁ refl
irr {2+ _} d∣p = inj₂ (≤∧≮⇒≡ (∣⇒≤ d∣p) d≮p)
where d≮p = λ d<p → pr (composite d<p d∣p)
irreducible⇒prime : .{{NonTrivial p}} → Irreducible p → Prime p
irreducible⇒prime irr = prime
λ (composite d<p d∣p) → [ nonTrivial⇒≢1 , (<⇒≢ d<p) ]′ (irr d∣p)
------------------------------------------------------------------------
-- Using decidability
-- Once we have the above decision procedures, then instead of
-- constructing proofs of e.g. Prime-ness by hand, we call the
-- appropriate function, and use the witness extraction functions
-- `from-yes`, `from-no` to return the checked proofs.
private
-- Example: 2 is prime, but not-composite.
2-is-prime : Prime 2
2-is-prime = from-yes (prime? 2)
2-is-not-composite : ¬ Composite 2
2-is-not-composite = from-no (composite? 2)
-- Example: 4 and 6 are composite, hence not-prime
4-is-composite : Composite 4
4-is-composite = from-yes (composite? 4)
4-is-not-prime : ¬ Prime 4
4-is-not-prime = from-no (prime? 4)
6-is-composite : Composite 6
6-is-composite = from-yes (composite? 6)
6-is-not-prime : ¬ Prime 6
6-is-not-prime = from-no (prime? 6)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4