|
| 1 | +------------------------------------------------------------------------ |
| 2 | +-- The Agda standard library |
| 3 | +-- |
| 4 | +-- Prime factorisation of natural numbers and its properties |
| 5 | +------------------------------------------------------------------------ |
| 6 | + |
| 7 | +{-# OPTIONS --cubical-compatible --safe #-} |
| 8 | + |
| 9 | +module Data.Nat.Primality.Factorisation where |
| 10 | + |
| 11 | +open import Data.Empty using (⊥-elim) |
| 12 | +open import Data.Nat.Base |
| 13 | +open import Data.Nat.Divisibility |
| 14 | +open import Data.Nat.Properties |
| 15 | +open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder) |
| 16 | +open import Data.Nat.Primality |
| 17 | +open import Data.Product as Π using (∃-syntax; _×_; _,_; proj₁; proj₂) |
| 18 | +open import Data.List.Base using (List; []; _∷_; _++_; product) |
| 19 | +open import Data.List.Membership.Propositional using (_∈_) |
| 20 | +open import Data.List.Membership.Propositional.Properties using (∈-∃++) |
| 21 | +open import Data.List.Relation.Unary.All as All using (All; []; _∷_) |
| 22 | +open import Data.List.Relation.Unary.Any using (here; there) |
| 23 | +open import Data.List.Relation.Binary.Permutation.Propositional |
| 24 | + using (_↭_; prep; swap; ↭-reflexive; ↭-refl; ↭-trans; refl; module PermutationReasoning) |
| 25 | +open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (product-↭; All-resp-↭; shift) |
| 26 | +open import Data.Sum.Base using (inj₁; inj₂) |
| 27 | +open import Function.Base using (_$_; _∘_; _|>_; flip) |
| 28 | +open import Induction using (build) |
| 29 | +open import Induction.Lexicographic using (_⊗_; [_⊗_]) |
| 30 | +open import Relation.Nullary.Decidable using (yes; no) |
| 31 | +open import Relation.Nullary.Negation using (contradiction) |
| 32 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; module ≡-Reasoning) |
| 33 | + |
| 34 | +private |
| 35 | + variable |
| 36 | + n : ℕ |
| 37 | + |
| 38 | +------------------------------------------------------------------------ |
| 39 | +-- Core definition |
| 40 | + |
| 41 | +record PrimeFactorisation (n : ℕ) : Set where |
| 42 | + field |
| 43 | + factors : List ℕ |
| 44 | + isFactorisation : n ≡ product factors |
| 45 | + factorsPrime : All Prime factors |
| 46 | + |
| 47 | +open PrimeFactorisation public using (factors) |
| 48 | +open PrimeFactorisation |
| 49 | + |
| 50 | +------------------------------------------------------------------------ |
| 51 | +-- Finding a factorisation |
| 52 | + |
| 53 | +primeFactorisation[1] : PrimeFactorisation 1 |
| 54 | +primeFactorisation[1] = record |
| 55 | + { factors = [] |
| 56 | + ; isFactorisation = refl |
| 57 | + ; factorsPrime = [] |
| 58 | + } |
| 59 | + |
| 60 | +primeFactorisation[p] : Prime n → PrimeFactorisation n |
| 61 | +primeFactorisation[p] {n} pr = record |
| 62 | + { factors = n ∷ [] |
| 63 | + ; isFactorisation = sym (*-identityʳ n) |
| 64 | + ; factorsPrime = pr ∷ [] |
| 65 | + } |
| 66 | + |
| 67 | +-- This builds up three important things: |
| 68 | +-- * a proof that every number we've gotten to so far has increasingly higher |
| 69 | +-- possible least prime factor, so we don't have to repeat smaller factors |
| 70 | +-- over and over (this is the "m" and "rough" parameters) |
| 71 | +-- * a witness that this limit is getting closer to the number of interest, in a |
| 72 | +-- way that helps the termination checker (the "k" and "eq" parameters) |
| 73 | +-- * a proof that we can factorise any smaller number, which is useful when we |
| 74 | +-- encounter a factor, as we can then divide by that factor and continue from |
| 75 | +-- there without termination issues |
| 76 | +factorise : ∀ n → .{{NonZero n}} → PrimeFactorisation n |
| 77 | +factorise 1 = primeFactorisation[1] |
| 78 | +factorise n₀@(2+ _) = build [ <-recBuilder ⊗ <-recBuilder ] P facRec (n₀ , suc n₀ ∸ 4) 2-rough refl |
| 79 | + where |
| 80 | + P : ℕ × ℕ → Set |
| 81 | + P (n , k) = ∀ {m} → .{{NonTrivial n}} → .{{NonTrivial m}} → m Rough n → suc n ∸ m * m ≡ k → PrimeFactorisation n |
| 82 | + |
| 83 | + facRec : ∀ n×k → (<-Rec ⊗ <-Rec) P n×k → P n×k |
| 84 | + facRec (n , zero) _ rough eq = |
| 85 | + -- Case 1: m * m > n, ∴ Prime n |
| 86 | + primeFactorisation[p] (rough∧square>⇒prime rough (m∸n≡0⇒m≤n eq)) |
| 87 | + facRec (n@(2+ _) , suc k) (recFactor , recQuotient) {m@(2+ _)} rough eq with m ∣? n |
| 88 | + -- Case 2: m ∤ n, try larger m, reducing k accordingly |
| 89 | + ... | no m∤n = recFactor (≤-<-trans (m∸n≤m k (m + m)) (n<1+n k)) {suc m} (∤⇒rough-suc m∤n rough) $ begin |
| 90 | + suc n ∸ (suc m + m * suc m) ≡⟨ cong (λ # → suc n ∸ (suc m + #)) (*-suc m m) ⟩ |
| 91 | + suc n ∸ (suc m + (m + m * m)) ≡⟨ cong (suc n ∸_) (+-assoc (suc m) m (m * m)) ⟨ |
| 92 | + suc n ∸ (suc (m + m) + m * m) ≡⟨ cong (suc n ∸_) (+-comm (suc (m + m)) (m * m)) ⟩ |
| 93 | + suc n ∸ (m * m + suc (m + m)) ≡⟨ ∸-+-assoc (suc n) (m * m) (suc (m + m)) ⟨ |
| 94 | + (suc n ∸ m * m) ∸ suc (m + m) ≡⟨ cong (_∸ suc (m + m)) eq ⟩ |
| 95 | + suc k ∸ suc (m + m) ∎ |
| 96 | + where open ≡-Reasoning |
| 97 | + -- Case 3: m ∣ n, record m and recurse on the quotient |
| 98 | + ... | yes m∣n = record |
| 99 | + { factors = m ∷ ps |
| 100 | + ; isFactorisation = sym m*Πps≡n |
| 101 | + ; factorsPrime = rough∧∣⇒prime rough m∣n ∷ primes |
| 102 | + } |
| 103 | + where |
| 104 | + m<n : m < n |
| 105 | + m<n = begin-strict |
| 106 | + m <⟨ s≤s (≤-trans (m≤n+m m _) (+-monoʳ-≤ _ (m≤m+n m _))) ⟩ |
| 107 | + pred (m * m) <⟨ s<s⁻¹ (m∸n≢0⇒n<m λ eq′ → 0≢1+n (trans (sym eq′) eq)) ⟩ |
| 108 | + n ∎ |
| 109 | + where open ≤-Reasoning |
| 110 | + |
| 111 | + q = quotient m∣n |
| 112 | + |
| 113 | + instance _ = n>1⇒nonTrivial (quotient>1 m∣n m<n) |
| 114 | + |
| 115 | + factorisation[q] : PrimeFactorisation q |
| 116 | + factorisation[q] = recQuotient (quotient-< m∣n) (suc q ∸ m * m) (rough∧∣⇒rough rough (quotient-∣ m∣n)) refl |
| 117 | + |
| 118 | + ps = factors factorisation[q] |
| 119 | + |
| 120 | + primes = factorsPrime factorisation[q] |
| 121 | + |
| 122 | + m*Πps≡n : m * product ps ≡ n |
| 123 | + m*Πps≡n = begin |
| 124 | + m * product ps ≡⟨ cong (m *_) (isFactorisation factorisation[q]) ⟨ |
| 125 | + m * q ≡⟨ m∣n⇒n≡m*quotient m∣n ⟨ |
| 126 | + n ∎ |
| 127 | + where open ≡-Reasoning |
| 128 | + |
| 129 | +------------------------------------------------------------------------ |
| 130 | +-- Properties of a factorisation |
| 131 | + |
| 132 | +factorisationHasAllPrimeFactors : ∀ {as} {p} → Prime p → p ∣ product as → All Prime as → p ∈ as |
| 133 | +factorisationHasAllPrimeFactors {[]} {2+ p} pPrime p∣Πas [] = contradiction (∣1⇒≡1 p∣Πas) λ () |
| 134 | +factorisationHasAllPrimeFactors {a ∷ as} {p} pPrime p∣aΠas (aPrime ∷ asPrime) with euclidsLemma a (product as) pPrime p∣aΠas |
| 135 | +... | inj₂ p∣Πas = there (factorisationHasAllPrimeFactors pPrime p∣Πas asPrime) |
| 136 | +... | inj₁ p∣a with prime⇒irreducible aPrime p∣a |
| 137 | +... | inj₁ refl = contradiction pPrime ¬prime[1] |
| 138 | +... | inj₂ refl = here refl |
| 139 | + |
| 140 | +private |
| 141 | + factorisationUnique′ : (as bs : List ℕ) → product as ≡ product bs → All Prime as → All Prime bs → as ↭ bs |
| 142 | + factorisationUnique′ [] [] Πas≡Πbs asPrime bsPrime = refl |
| 143 | + factorisationUnique′ [] (b@(2+ _) ∷ bs) Πas≡Πbs prime[as] (_ ∷ prime[bs]) = |
| 144 | + contradiction Πas≡Πbs (<⇒≢ Πas<Πbs) |
| 145 | + where |
| 146 | + Πas<Πbs : product [] < product (b ∷ bs) |
| 147 | + Πas<Πbs = begin-strict |
| 148 | + 1 ≡⟨⟩ |
| 149 | + 1 * 1 <⟨ *-monoˡ-< 1 {1} {b} sz<ss ⟩ |
| 150 | + b * 1 ≤⟨ *-monoʳ-≤ b (productOfPrimes≥1 prime[bs]) ⟩ |
| 151 | + b * product bs ≡⟨⟩ |
| 152 | + product (b ∷ bs) ∎ |
| 153 | + where open ≤-Reasoning |
| 154 | + |
| 155 | + factorisationUnique′ (a ∷ as) bs Πas≡Πbs (prime[a] ∷ prime[as]) prime[bs] = a∷as↭bs |
| 156 | + where |
| 157 | + a∣Πbs : a ∣ product bs |
| 158 | + a∣Πbs = divides (product as) $ begin |
| 159 | + product bs ≡⟨ Πas≡Πbs ⟨ |
| 160 | + product (a ∷ as) ≡⟨⟩ |
| 161 | + a * product as ≡⟨ *-comm a (product as) ⟩ |
| 162 | + product as * a ∎ |
| 163 | + where open ≡-Reasoning |
| 164 | + |
| 165 | + shuffle : ∃[ bs′ ] bs ↭ a ∷ bs′ |
| 166 | + shuffle with ys , zs , p ← ∈-∃++ (factorisationHasAllPrimeFactors prime[a] a∣Πbs prime[bs]) |
| 167 | + = ys ++ zs , ↭-trans (↭-reflexive p) (shift a ys zs) |
| 168 | + |
| 169 | + bs′ = proj₁ shuffle |
| 170 | + bs↭a∷bs′ = proj₂ shuffle |
| 171 | + |
| 172 | + Πas≡Πbs′ : product as ≡ product bs′ |
| 173 | + Πas≡Πbs′ = *-cancelˡ-≡ (product as) (product bs′) a {{prime⇒nonZero prime[a]}} $ begin |
| 174 | + a * product as ≡⟨ Πas≡Πbs ⟩ |
| 175 | + product bs ≡⟨ product-↭ bs↭a∷bs′ ⟩ |
| 176 | + a * product bs′ ∎ |
| 177 | + where open ≡-Reasoning |
| 178 | + |
| 179 | + prime[bs'] : All Prime bs′ |
| 180 | + prime[bs'] = All.tail (All-resp-↭ bs↭a∷bs′ prime[bs]) |
| 181 | + |
| 182 | + a∷as↭bs : a ∷ as ↭ bs |
| 183 | + a∷as↭bs = begin |
| 184 | + a ∷ as <⟨ factorisationUnique′ as bs′ Πas≡Πbs′ prime[as] prime[bs'] ⟩ |
| 185 | + a ∷ bs′ ↭⟨ bs↭a∷bs′ ⟨ |
| 186 | + bs ∎ |
| 187 | + where open PermutationReasoning |
| 188 | + |
| 189 | +factorisationUnique : (f f′ : PrimeFactorisation n) → factors f ↭ factors f′ |
| 190 | +factorisationUnique {n} f f′ = |
| 191 | + factorisationUnique′ (factors f) (factors f′) Πf≡Πf′ (factorsPrime f) (factorsPrime f′) |
| 192 | + where |
| 193 | + Πf≡Πf′ : product (factors f) ≡ product (factors f′) |
| 194 | + Πf≡Πf′ = begin |
| 195 | + product (factors f) ≡⟨ isFactorisation f ⟨ |
| 196 | + n ≡⟨ isFactorisation f′ ⟩ |
| 197 | + product (factors f′) ∎ |
| 198 | + where open ≡-Reasoning |
0 commit comments