Add prime factorization and its properties

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

@@ -12,7 +12,8 @@ open import Algebra.Bundles
 open import Algebra.Definitions
 open import Algebra.Structures
 open import Data.Bool.Base using (Bool; true; false)
-open import Data.Nat using (suc)
+open import Data.Nat.Base using (suc; _*_)
+open import Data.Nat.Properties using (*-assoc; *-comm)
 open import Data.Product using (-,_; proj₂)
 open import Data.List.Base as List
 open import Data.List.Relation.Binary.Permutation.Propositional
@@ -29,11 +30,9 @@ open import Level using (Level)
 open import Relation.Unary using (Pred)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as ≡
-  using (_≡_ ; refl ; cong; cong₂; _≢_; inspect)
+  using (_≡_ ; refl ; cong; cong₂; _≢_; inspect; module ≡-Reasoning)
 open import Relation.Nullary
 
-open PermutationReasoning
-
 private
   variable
     a b p : Level
@@ -173,6 +172,7 @@ shift v (x ∷ xs) ys = begin
   x ∷ (xs ++ [ v ] ++ ys) <⟨ shift v xs ys ⟩
   x ∷ v ∷ xs ++ ys        <<⟨ refl ⟩
   v ∷ x ∷ xs ++ ys        ∎
+  where open PermutationReasoning
 
 drop-mid-≡ : ∀ {x : A} ws xs {ys} {zs} →
              ws ++ [ x ] ++ ys ≡ xs ++ [ x ] ++ zs →
@@ -217,11 +217,13 @@ drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl
       _ ∷ (xs ++ _ ∷ _) <⟨ shift _ _ _ ⟩
       _ ∷ _ ∷ xs ++ _   <<⟨ refl ⟩
       _ ∷ _ ∷ xs ++ _   ∎
+      where open PermutationReasoning
   drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ [])     refl refl = begin
       _ ∷ _ ∷ ws ++ _   <<⟨ refl ⟩
       _ ∷ (_ ∷ ws ++ _) <⟨ ↭-sym (shift _ _ _) ⟩
       _ ∷ (ws ++ _ ∷ _) <⟨ p ⟩
       _ ∷ _             ∎
+      where open PermutationReasoning
   drop-mid′ (swap y z p) (y ∷ z ∷ ws) (z ∷ y ∷ xs) refl refl = swap y z (drop-mid′ p _ _ refl refl)
   drop-mid′ (trans p₁ p₂) ws  xs refl refl with ∈-∃++ (∈-resp-↭ p₁ (∈-insert ws))
   ... | (h , t , refl) = trans (drop-mid′ p₁ ws h refl refl) (drop-mid′ p₂ h xs refl refl)
@@ -246,6 +248,7 @@ drop-mid {A = A} {x} ws xs p = drop-mid′ p ws xs refl refl
   x ∷ xs ++ ys   <⟨ ++-comm xs ys ⟩
   x ∷ ys ++ xs   ↭˘⟨ shift x ys xs ⟩
   ys ++ (x ∷ xs) ∎
+  where open PermutationReasoning
 
 ++-isMagma : IsMagma {A = List A} _↭_ _++_
 ++-isMagma = record
@@ -301,6 +304,7 @@ shifts xs ys {zs} = begin
   (xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys) ⟩
   (ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩
    ys ++ xs  ++ zs ∎
+   where open PermutationReasoning
 
 ------------------------------------------------------------------------
 -- _∷_
@@ -316,6 +320,7 @@ drop-∷ = drop-mid [] []
   xs ++ [ x ]   ↭⟨ shift x xs [] ⟩
   x ∷ xs ++ []  ≡⟨ Lₚ.++-identityʳ _ ⟩
   x ∷ xs        ∎)
+  where open PermutationReasoning
 
 ------------------------------------------------------------------------
 -- ʳ++
@@ -354,3 +359,18 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where
     (x ∷ xs) ++ y ∷ ys       ≡˘⟨ Lₚ.++-assoc [ x ] xs (y ∷ ys) ⟩
     x ∷ xs ++ y ∷ ys         ∎
     where open PermutationReasoning
+
+------------------------------------------------------------------------
+-- product
+
+productPreserves↭⇒≡ : product Preserves _↭_ ⟶ _≡_
+productPreserves↭⇒≡ refl = refl
+productPreserves↭⇒≡ (prep x r) = cong (x *_) (productPreserves↭⇒≡ r)
+productPreserves↭⇒≡ (trans r s) = ≡.trans (productPreserves↭⇒≡ r) (productPreserves↭⇒≡ s)
+productPreserves↭⇒≡ (swap {xs} {ys} x y r) = begin
+  x * (y * product xs) ≡˘⟨ *-assoc x y (product xs) ⟩
+  (x * y) * product xs ≡⟨ cong₂ _*_ (*-comm x y) (productPreserves↭⇒≡ r) ⟩
+  (y * x) * product ys ≡⟨ *-assoc y x (product ys) ⟩
+  y * (x * product ys) ∎
+  where open ≡-Reasoning
+

src/Data/Nat/Divisibility.agda

@@ -300,3 +300,9 @@ m≤n⇒m!∣n! m≤n = help (≤⇒≤′ m≤n)
   help : ∀ {m n} → m ≤′ n → m ! ∣ n !
   help {m} {n}     ≤′-refl        = ∣-refl
   help {m} {suc n} (≤′-step m≤′n) = ∣n⇒∣m*n (suc n) (help m≤′n)
+
+------------------------------------------------------------------------
+-- Properties of quotient
+
+quotient∣n : ∀ {m n} (m∣n : m ∣ n) → quotient m∣n ∣ n
+quotient∣n {m = m} m∣n = divides m (trans (_∣_.equality m∣n) (*-comm (quotient m∣n) m))

src/Data/Nat/Primality.agda

@@ -20,8 +20,8 @@ open import Relation.Nullary.Decidable as Dec
   using (yes; no; from-yes; ¬?; decidable-stable; _×-dec_; _→-dec_)
 open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Unary using (Decidable)
-open import Relation.Binary.PropositionalEquality
-  using (refl; sym; cong; subst)
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; sym; cong; subst)
 
 private
   variable
@@ -141,3 +141,18 @@ private
   -- Example: 6 is composite
   6-is-composite : Composite 6
   6-is-composite = from-yes (composite? 6)
+
+------------------------------------------------------------------------
+-- Other properties
+
+Prime⇒NonZero : Prime n → NonZero n
+Prime⇒NonZero {suc _} _ = _
+
+Composite⇒NonZero : Composite n → NonZero n
+Composite⇒NonZero {suc _} _ = _
+
+-- If m is a factor of prime p, then it is equal to either 1 or p itself
+∣p⇒≡1∨≡p : ∀ m {p} → Prime p → m ∣ p → m ≡ 1 ⊎ m ≡ p
+∣p⇒≡1∨≡p 0 {p} p-prime m∣p = contradiction (0∣⇒≡0 m∣p) λ p≡0 → subst Prime p≡0 p-prime
+∣p⇒≡1∨≡p 1 {p} p-prime m∣p = inj₁ refl
+∣p⇒≡1∨≡p (suc (suc m)) {suc (suc p)} p-prime m∣p = inj₂ (≤∧≮⇒≡ (∣⇒≤ m∣p) λ m<p → p-prime (s≤s (s≤s z≤n)) m<p m∣p)

src/Data/Nat/Primality/Factorization.agda

@@ -0,0 +1,125 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Prime factorization of naturla numbers and its properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Nat.Primality.Factorization where
+
+open import Data.Empty
+open import Data.Nat.Base
+open import Data.Nat.Divisibility
+open import Data.Nat.Properties
+open import Data.Nat.Induction
+open import Data.Nat.Primality
+open import Data.Nat.Rough
+open import Data.Product as Π
+open import Data.List.Base
+open import Data.List.Relation.Unary.All as All
+open import Data.List.Relation.Binary.Permutation.Propositional as ↭
+open import Data.List.Relation.Binary.Permutation.Propositional.Properties
+open import Data.Sum.Base
+open import Function.Base
+open import Relation.Nullary.Decidable
+open import Relation.Nullary.Negation
+open import Relation.Binary.PropositionalEquality as ≡
+
+-- Core definition
+------------------------------------------------------------------------
+
+record Factorization (n : ℕ) : Set where
+  field
+    factors : List ℕ
+    isFactorization : product factors ≡ n
+    factorsPrime : All Prime factors
+
+open Factorization public using (factors)
+
+-- Finding a factorization
+------------------------------------------------------------------------
+
+-- this builds up three important things:
+-- * a proof that every number we've gotten to so far has increasingly higher
+--   possible least prime factor, so we don't have to repeat smaller factores
+--   over and over (this is the "k" and "k-rough-n" parameters)
+-- * a witness that this limit is getting closer to the number of interest, in a
+--   way that helps the termination checker (the k≤n parameter)
+-- * a proof that we can factorize any smaller number, which is useful when we
+--   encounter a factor, as we can then divide by that factor and continue from
+--   there without termination issues
+
+factorize : ∀ n → .{{NonZero n}} → Factorization n
+factorize 1 = record
+  { factors = []
+  ; isFactorization = refl
+  ; factorsPrime = []
+  }
+factorize (suc (suc n)) = <-rec (λ n′ → ∀ {k} → 2 ≤ n′ → k ≤‴ n′ → k Rough n′ → Factorization n′) factorizeRec (2 + n) {2} (s≤s (s≤s z≤n)) (≤⇒≤‴ (s≤s (s≤s z≤n))) (2-rough-n (2 + n))
+  where
+  factorizeRec : ∀ n → <-Rec (λ n′ → ∀ {k} → 2 ≤ n′ → k ≤‴ n′ → k Rough n′ → Factorization n′) n → ∀ {k} → 2 ≤ n → k ≤‴ n → k Rough n → Factorization n
+  factorizeRec (suc (suc n)) rec (s≤s (s≤s n≤z)) ≤‴-refl k-rough-n = record
+    { factors = 2 + n ∷ []
+    ; isFactorization = *-identityʳ (2 + n)
+    ; factorsPrime = (λ 2≤d d<n d∣n → rough⇒∤ k-rough-n 2≤d d<n d∣n) ∷ []
+    }
+  factorizeRec (suc (suc n)) rec {0} (s≤s (s≤s z≤n)) (≤‴-step (≤‴-step k<n)) k-rough-n = factorizeRec (2 + n) rec (s≤s (s≤s z≤n)) k<n (2-rough-n (2 + n))
+  factorizeRec (suc (suc n)) rec {1} (s≤s (s≤s z≤n)) (≤‴-step k<n) k-rough-n = factorizeRec (2 + n) rec (s≤s (s≤s z≤n)) k<n (2-rough-n (2 + n))
+  factorizeRec (suc (suc n)) rec {suc (suc k)} (s≤s (s≤s z≤n)) (≤‴-step k<n) k-rough-n with 2 + k ∣? 2 + n
+  ... | no  k∤n = factorizeRec (2 + n) rec {3 + k} (s≤s (s≤s z≤n)) k<n (extend-∤ k-rough-n k∤n)
+  ... | yes k∣n = record
+    { factors = 2 + k ∷ Factorization.factors res
+    ; isFactorization = prop
+    ; factorsPrime = roughn∧∣n⇒prime k-rough-n (s≤s (s≤s z≤n)) k∣n ∷ Factorization.factorsPrime res
+    }
+    where
+      open ≡-Reasoning
+
+      -- we know that k < n, so if q is 0 or 1 then q * k < n
+      2≤q : 2 ≤ quotient k∣n
+      2≤q = ≮⇒≥ λ { (s≤s q≤1) → >⇒≢ (<-transʳ (*-monoˡ-≤ (2 + k) q≤1) (<-transʳ (≤-reflexive (+-identityʳ (2 + k))) (≤‴⇒≤ k<n))) (_∣_.equality k∣n) }
+
+      q<n : quotient k∣n < 2 + n
+      q<n = <-transˡ (m<m*n (quotient k∣n) (2 + k) ⦃ >-nonZero (<-transˡ (s≤s z≤n) 2≤q) ⦄ (s≤s (s≤s z≤n))) (≤-reflexive (sym (_∣_.equality k∣n)))
+
+      res : Factorization (quotient k∣n)
+      res = rec (quotient k∣n) q<n {2 + k} 2≤q (≤⇒≤‴ (≮⇒≥ (λ q<k → rough⇒∤ k-rough-n 2≤q q<k (quotient∣n k∣n)))) λ {d} d<k d-prime → k-rough-n d<k d-prime ∘ flip ∣-trans (quotient∣n k∣n)
+
+      prop : (2 + k) * product (factors res) ≡ 2 + n
+      prop = begin
+        (2 + k) * product (factors res) ≡⟨ cong ((2 + k) *_) (Factorization.isFactorization res) ⟩
+        (2 + k) * quotient k∣n          ≡⟨ *-comm (2 + k) (quotient k∣n) ⟩
+        quotient k∣n * (2 + k)          ≡˘⟨ _∣_.equality k∣n ⟩
+        2 + n                           ∎
+
+------------------------------------------------------------------------
+-- Properties of a factorization
+
+factorization≥1 : ∀ {as} → All Prime as → product as ≥ 1
+factorization≥1 {[]} [] = s≤s z≤n
+factorization≥1 {suc a ∷ as} (pa ∷ asPrime) = *-mono-≤ {1} {1 + a} (s≤s z≤n) (factorization≥1 asPrime)
+
+factorizationPullToFront : ∀ {as} {p} → Prime p → p ∣ product as → All Prime as → ∃[ as′ ] as ↭ (p ∷ as′)
+factorizationPullToFront {[]} {suc (suc p)} pPrime p∣Πas asPrime = contradiction (∣1⇒≡1 p∣Πas) λ ()
+factorizationPullToFront {a ∷ as} {p} pPrime p∣aΠas (aPrime ∷ asPrime) with euclidsLemma a (product as) pPrime p∣aΠas
+... | inj₂ p∣Πas = Π.map (a ∷_) (λ as↭p∷as′ → ↭-trans (prep a as↭p∷as′) (↭.swap a p refl)) (factorizationPullToFront pPrime p∣Πas asPrime)
+... | inj₁ p∣a with ∣p⇒≡1∨≡p p aPrime p∣a
+...   | inj₁ refl = ⊥-elim pPrime
+...   | inj₂ refl = as , ↭-refl
+
+factorizationUnique′ : (as bs : List ℕ) → product as ≡ product bs → All Prime as → All Prime bs → as ↭ bs
+factorizationUnique′ [] [] Πas≡Πbs asPrime bsPrime = refl
+factorizationUnique′ [] (suc (suc b) ∷ bs) Πas≡Πbs asPrime (bPrime ∷ bsPrime) = contradiction Πas≡Πbs (<⇒≢ (<-transˡ (*-monoˡ-< 1 {1} {2 + b} (s≤s (s≤s z≤n))) (*-monoʳ-≤ (2 + b) (factorization≥1 bsPrime))))
+factorizationUnique′ (a ∷ as) bs Πas≡Πbs (aPrime ∷ asPrime) bsPrime with bs′ , bs↭a∷bs′ ← factorizationPullToFront aPrime (divides (product as) (≡.trans (sym Πas≡Πbs) (*-comm a (product as)))) bsPrime = begin
+    a ∷ as  <⟨ factorizationUnique′ as bs′
+               (*-cancelˡ-≡ (product as) (product bs′) a {{Prime⇒NonZero aPrime}} (≡.trans Πas≡Πbs (productPreserves↭⇒≡ bs↭a∷bs′)))
+               asPrime
+               (All.tail (All-resp-↭ bs↭a∷bs′ bsPrime))
+            ⟩
+    a ∷ bs′ ↭˘⟨ bs↭a∷bs′ ⟩
+    bs      ∎
+  where open PermutationReasoning
+
+factorizationUnique : {n : ℕ} (f f′ : Factorization n) → factors f ↭ factors f′
+factorizationUnique f f′ = factorizationUnique′ (factors f) (factors f′) (≡.trans (Factorization.isFactorization f) (sym (Factorization.isFactorization f′))) (Factorization.factorsPrime f) (Factorization.factorsPrime f′)

src/Data/Nat/Rough.agda

@@ -0,0 +1,62 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Natural numbers whose prime factors are all above a bound
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Nat.Rough where
+
+open import Data.Nat.Base using (ℕ; suc; _≤_; _<_; z≤n; s≤s; _+_)
+open import Data.Nat.Divisibility using (_∣_; _∤_; ∣-trans; ∣1⇒≡1)
+open import Data.Nat.Induction using (<-rec; <-Rec)
+open import Data.Nat.Primality using (Prime; composite?)
+open import Data.Nat.Properties using (_≟_; <-trans; ≤∧≢⇒<)
+open import Data.Product.Base using (_,_)
+open import Function.Base using (_∘_; flip)
+open import Relation.Nullary.Decidable.Core using (yes; no)
+open import Relation.Binary.PropositionalEquality.Core using (refl)
+
+-- A number is k-rough if all its prime factors are greater than or equal to k
+_Rough_ : ℕ → ℕ → Set
+k Rough n = ∀ {d} → 1 < d → d < k → d ∤ n
+
+-- any number is 2-rough because all primes are greater than or equal to 2
+2-rough-n : ∀ n → 2 Rough n
+2-rough-n n {1} (s≤s ()) 1<2
+2-rough-n n {suc (suc d)} 1<d (s≤s (s≤s ()))
+
+-- if a number is k-rough, and it's not a multiple of k, then it's (k+1)-rough
+extend-∤ : ∀ {k n} → k Rough n → k ∤ n → suc k Rough n
+extend-∤ {k = k} k-rough-n k∤n {suc d} 1<d (s≤s d<k) with suc d ≟ k
+... | yes refl = k∤n
+... | no  d≢k  = k-rough-n 1<d (≤∧≢⇒< d<k d≢k)
+
+-- 1 is always rough
+b-rough-1 : ∀ k → k Rough 1
+b-rough-1 k {d} 1<d d<k d∣1 with ∣1⇒≡1 d∣1
+b-rough-1 k {.1} (s≤s ()) d<k d∣1 | refl
+
+-- if a number is k-rough, then so are all of its divisors
+reduce-∣ : ∀ {k m n} → k Rough m → n ∣ m → k Rough n
+reduce-∣ k-rough-n n∣m d<k d-prime d∣n = k-rough-n d<k d-prime (∣-trans d∣n n∣m)
+
+-- if a number is k-rough, then no number 2 ≤ d < k will divide it, whether prime or not
+rough⇒∤ : ∀ {d k n} → k Rough n → 2 ≤ d → d < k → d ∤ n
+rough⇒∤ {d} {k} {n} k-rough-n = <-rec (λ d′ → 2 ≤ d′ → d′ < k → d′ ∤ n) (rough⇒∤Rec k-rough-n) d
+  where
+    rough⇒∤Rec : ∀ {n k} → k Rough n → ∀ d → <-Rec (λ d′ → 2 ≤ d′ → d′ < k → d′ ∤ n) d → 2 ≤ d → d < k → d ∤ n
+    rough⇒∤Rec {n} {k} k-rough-n (suc (suc d)) rec (s≤s (s≤s z≤n)) d<k with composite? (2 + d)
+    ... | yes (d′ , 2≤d′ , d′<d , d′∣d) = rec d′ d′<d 2≤d′ (<-trans d′<d d<k) ∘ ∣-trans d′∣d
+    ... | no ¬d-composite = k-rough-n {2 + d} (s≤s (s≤s z≤n)) d<k
+
+-- if a number is k-rough, and k divides it, then it must be prime
+roughn∧∣n⇒prime : ∀ {k n} → k Rough n → 2 ≤ k → k ∣ n → Prime k
+roughn∧∣n⇒prime {k = suc (suc k)} {n = n} k-rough-n (s≤s (s≤s z≤n)) k∣n
+  = <-rec (λ d → 2 ≤ d → d < 2 + k → d ∤ 2 + k) (roughn∧∣n⇒primeRec k-rough-n k∣n) _
+  where
+  roughn∧∣n⇒primeRec : ∀ {k n} → k Rough n → k ∣ n → ∀ d → <-Rec (λ d′ → 2 ≤ d′ → d′ < k → d′ ∤ k) d → 2 ≤ d → d < k → d ∤ k
+  roughn∧∣n⇒primeRec {k} {n} k-rough-n k∣n (suc (suc d)) rec (s≤s (s≤s z≤n)) d<k with composite? (2 + d)
+  ... | yes (d′ , 2≤d′ , d′<d , d′∣d) = rec d′ d′<d 2≤d′ (<-trans d′<d d<k) ∘ ∣-trans d′∣d
+  ... | no ¬d-composite = k-rough-n (s≤s (s≤s z≤n)) d<k ∘ flip ∣-trans k∣n