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₂; _≢_)
+  using (_≡_ ; refl ; cong; cong₂; _≢_; 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,17 @@ 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
+
+product-↭ : product Preserves _↭_ ⟶ _≡_
+product-↭ refl = refl
+product-↭ (prep x r) = cong (x *_) (product-↭ r)
+product-↭ (trans r s) = ≡.trans (product-↭ r) (product-↭ s)
+product-↭ (swap {xs} {ys} x y r) = begin
+  x * (y * product xs) ≡˘⟨ *-assoc x y (product xs) ⟩
+  (x * y) * product xs ≡⟨ cong₂ _*_ (*-comm x y) (product-↭ 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,13 @@ 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} {n = n} m∣n = divides m $ begin-equality
+  n                ≡⟨ _∣_.equality m∣n ⟩
+  quotient m∣n * m ≡⟨ *-comm (quotient m∣n) m ⟩
+  m * quotient m∣n ∎
+  where open ≤-Reasoning

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)
 
 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) (≢-nonZero⁻¹ p {{Prime⇒NonZero 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/Factorisation.agda

@@ -0,0 +1,218 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Prime factorisation of natural numbers and its properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Nat.Primality.Factorisation where
+
+open import Data.Empty using (⊥-elim)
+open import Data.Nat.Base
+open import Data.Nat.Divisibility using (_∣_; _∣?_; quotient; quotient∣n; ∣-trans; ∣1⇒≡1; divides)
+open import Data.Nat.Properties
+open import Data.Nat.Induction using (<-Rec; <-rec)
+open import Data.Nat.Primality using (Prime; euclidsLemma; ∣p⇒≡1∨≡p; Prime⇒NonZero)
+open import Data.Nat.Primality.Rough using (_Rough_; 2-rough-n; extend-∤; roughn∧∣n⇒prime)
+open import Data.Product as Π using (∃-syntax; _,_; proj₁; proj₂)
+open import Data.List.Base using (List; []; _∷_; product)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+open import Data.List.Relation.Binary.Permutation.Propositional as ↭
+  using (_↭_; prep; swap; ↭-refl; refl; module PermutationReasoning)
+open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (product-↭; All-resp-↭)
+open import Data.Sum.Base using (inj₁; inj₂)
+open import Function.Base using (_$_; _∘_; _|>_; flip)
+open import Relation.Nullary.Decidable using (yes; no)
+open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; module ≡-Reasoning)
+
+------------------------------------------------------------------------
+-- Core definition
+
+record PrimeFactorisation (n : ℕ) : Set where
+  field
+    factors : List ℕ
+    isFactorisation : product factors ≡ n
+    factorsPrime : All Prime factors
+
+open PrimeFactorisation public using (factors)
+open PrimeFactorisation
+
+------------------------------------------------------------------------
+-- Finding a factorisation
+
+-- 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 factorise 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
+
+private
+  pattern 2+ n = suc (suc n)
+  pattern 2≤2+n = s≤s (s≤s z≤n)
+  pattern 1<2+n = 2≤2+n
+
+factorise : ∀ n → .{{NonZero n}} → PrimeFactorisation n
+factorise 1 = record
+  { factors = []
+  ; isFactorisation = refl
+  ; factorsPrime = []
+  }
+factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+n) (2-rough-n (2 + n))
+  where
+
+  P : ℕ → Set
+  P n′ = ∀ {k} → 2 ≤ n′ → k ≤‴ n′ → k Rough n′ → PrimeFactorisation n′
+
+  factoriseRec : ∀ n → <-Rec P n → P n
+  factoriseRec (2+ n) rec (s≤s (s≤s n≤z)) ≤‴-refl k-rough-n = record
+    { factors = 2 + n ∷ []
+    ; isFactorisation = *-identityʳ (2 + n)
+    ; factorsPrime = k-rough-n ∷ []
+    }
+  factoriseRec (2+ n) rec {0} 2≤2+n (≤‴-step (≤‴-step k<n)) k-rough-n =
+    factoriseRec (2+ n) rec 2≤2+n k<n (2-rough-n (2+ n))
+  factoriseRec (2+ n) rec {1} 2≤2+n (≤‴-step k<n) k-rough-n =
+    factoriseRec (2+ n) rec 2≤2+n k<n (2-rough-n (2+ n))
+  factoriseRec (2+ n) rec {suc (suc k)} 2≤2+n (≤‴-step k<n) k-rough-n with 2 + k ∣? 2+ n
+  ... | no  k∤n = factoriseRec (2+ n) rec {3 + k} 2≤2+n k<n (extend-∤ k-rough-n k∤n)
+  ... | yes k∣n = record
+    { factors = 2 + k ∷ factors res
+    ; isFactorisation = prop
+    ; factorsPrime = roughn∧∣n⇒prime k-rough-n 2≤2+n k∣n ∷ factorsPrime res
+    }
+    where
+      open ≤-Reasoning
+
+      q : ℕ
+      q = quotient k∣n
+
+      -- we know that k < n, so if q is 0 or 1 then q * k < n
+      2≤q : 2 ≤ q
+      2≤q = ≮⇒≥ (λ q<2 → contradiction (_∣_.equality k∣n) (>⇒≢ (prf (≤-pred q<2)))) where
+
+        prf : q ≤ 1 → q * 2+ k < 2 + n
+        prf q≤1 = begin-strict
+          q * 2+ k  ≤⟨ *-monoˡ-≤ (2 + k) q≤1 ⟩
+          2 + k + 0 ≡⟨ +-identityʳ (2 + k) ⟩
+          2 + k     <⟨ ≤‴⇒≤ k<n ⟩
+          2 + n     ∎
+
+      0<q : 0 < q
+      0<q = begin-strict
+        0 <⟨ s≤s z≤n ⟩
+        2 ≤⟨ 2≤q ⟩
+        q ∎
+
+      q<n : q < 2 + n
+      q<n = begin-strict
+        q           <⟨ m<m*n q (2 + k) ⦃ >-nonZero 0<q ⦄ 2≤2+n ⟩
+        q * (2 + k) ≡˘⟨ _∣_.equality k∣n ⟩
+        2 + n       ∎
+
+      q≮2+k : q ≮ 2 + k
+      q≮2+k q<k = k-rough-n 2≤q q<k (quotient∣n k∣n)
+
+      res : PrimeFactorisation q
+      res = rec q q<n {2 + k} 2≤q (≤⇒≤‴ (≮⇒≥ q≮2+k))
+          $ λ {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-equality
+        (2 + k) * product (factors res)
+          ≡⟨ cong ((2 + k) *_) (isFactorisation res) ⟩
+        (2 + k) * q
+          ≡⟨ *-comm (2 + k) q ⟩
+        q * (2 + k)
+          ≡˘⟨ _∣_.equality k∣n ⟩
+        2 + n ∎
+
+------------------------------------------------------------------------
+-- Properties of a factorisation
+
+factorisation≥1 : ∀ {as} → All Prime as → product as ≥ 1
+factorisation≥1 {[]} [] = s≤s z≤n
+factorisation≥1 {suc a ∷ as} (pa ∷ asPrime) = *-mono-≤ {1} {1 + a} (s≤s z≤n) (factorisation≥1 asPrime)
+
+factorisationPullToFront : ∀ {as} {p} → Prime p → p ∣ product as → All Prime as → ∃[ as′ ] as ↭ (p ∷ as′)
+factorisationPullToFront {[]} {suc (suc p)} pPrime p∣Πas asPrime = contradiction (∣1⇒≡1 p∣Πas) λ ()
+factorisationPullToFront {a ∷ as} {p} pPrime p∣aΠas (aPrime ∷ asPrime)
+  with euclidsLemma a (product as) pPrime p∣aΠas
+... | inj₂ p∣Πas = Π.map (a ∷_) step ih
+  where
+    ih : ∃[ as′ ] as ↭ (p ∷ as′)
+    ih = factorisationPullToFront pPrime p∣Πas asPrime
+
+    step : ∀ {as′} → as ↭ p ∷ as′ → a ∷ as ↭ p ∷ a ∷ as′
+    step {as′} as↭p∷as′ = begin
+      a ∷ as      ↭⟨ prep a as↭p∷as′ ⟩
+      a ∷ p ∷ as′ ↭⟨ swap a p refl ⟩
+      p ∷ a ∷ as′ ∎
+      where open PermutationReasoning
+
+... | inj₁ p∣a with ∣p⇒≡1∨≡p p aPrime p∣a
+...   | inj₁ refl = ⊥-elim pPrime
+...   | inj₂ refl = as , ↭-refl
+
+factorisationUnique′ : (as bs : List ℕ) → product as ≡ product bs → All Prime as → All Prime bs → as ↭ bs
+factorisationUnique′ [] [] Πas≡Πbs asPrime bsPrime = refl
+factorisationUnique′ [] (suc (suc b) ∷ bs) Πas≡Πbs asPrime (bPrime ∷ bsPrime) =
+  contradiction Πas≡Πbs (<⇒≢ Πas<Πbs)
+  where
+    Πas<Πbs : product [] < product (2+ b ∷ bs)
+    Πas<Πbs = begin-strict
+      1                    ≡⟨⟩
+      1       * 1          <⟨ *-monoˡ-< 1 {1} {2 + b} 1<2+n ⟩
+      (2 + b) * 1          ≤⟨ *-monoʳ-≤ (2 + b) (factorisation≥1 bsPrime) ⟩
+      2+ b    * product bs ≡⟨⟩
+      product (2+ b ∷ bs)  ∎
+      where open ≤-Reasoning
+
+factorisationUnique′ (a ∷ as) bs Πas≡Πbs (aPrime ∷ asPrime) bsPrime = a∷as↭bs
+  where
+    a∣Πbs : a ∣ product bs
+    a∣Πbs = divides (product as) $ begin
+      product bs       ≡˘⟨ Πas≡Πbs ⟩
+      product (a ∷ as) ≡⟨⟩
+      a * product as   ≡⟨ *-comm a (product as) ⟩
+      product as * a   ∎
+      where open ≡-Reasoning
+
+    shuffle : ∃[ bs′ ] bs ↭ a ∷ bs′
+    shuffle = factorisationPullToFront aPrime a∣Πbs bsPrime
+
+    bs′ = proj₁ shuffle
+    bs↭a∷bs′ = proj₂ shuffle
+
+    Πas≡Πbs′ : product as ≡ product bs′
+    Πas≡Πbs′ = *-cancelˡ-≡ (product as) (product bs′) a {{Prime⇒NonZero aPrime}} $ begin
+      a * product as  ≡⟨ Πas≡Πbs ⟩
+      product bs      ≡⟨ product-↭ bs↭a∷bs′ ⟩
+      a * product bs′ ∎
+      where open ≡-Reasoning
+
+    bs′Prime : All Prime bs′
+    bs′Prime = All.tail (All-resp-↭ bs↭a∷bs′ bsPrime)
+
+    a∷as↭bs : a ∷ as ↭ bs
+    a∷as↭bs = begin
+      a ∷ as  <⟨ factorisationUnique′ as bs′ Πas≡Πbs′ asPrime bs′Prime ⟩
+      a ∷ bs′ ↭˘⟨ bs↭a∷bs′ ⟩
+      bs      ∎
+      where open PermutationReasoning
+
+factorisationUnique : {n : ℕ} (f f′ : PrimeFactorisation n) → factors f ↭ factors f′
+factorisationUnique {n} f f′ =
+  factorisationUnique′ (factors f) (factors f′) Πf≡Πf′ (factorsPrime f) (factorsPrime f′)
+  where
+    Πf≡Πf′ : product (factors f) ≡ product (factors f′)
+    Πf≡Πf′ = begin
+      product (factors f)  ≡⟨ isFactorisation f ⟩
+      n                    ≡˘⟨ isFactorisation f′ ⟩
+      product (factors f′) ∎
+      where open ≡-Reasoning