-
Notifications
You must be signed in to change notification settings - Fork 239
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add prime factorization and its properties (#1969)
* Add prime factorization and its properties * Add missing header comment I'd missed this when copy-pasting from my old code in a separate repo * Remove completely trivial lemma * Use equational reasoning in quotient|n proof * Fix typo in module header * Factorization => Factorisation * Use Nat lemma in extend-|/ * [ cleanup ] part of the proof * [ cleanup ] finishing up the job * [ cleanup ] a little bit more * [ cleanup ] the import list * [ fix ] header style * [ fix ] broken merge: missing import * Move Data.Nat.Rough to Data.Nat.Primality.Rough * Rename productPreserves↭⇒≡ to product-↭ * Use proof of Prime=>NonZero * Open reasoning once in factoriseRec * Rename Factorisation => PrimeFactorisation * Move wheres around * Tidy up Rough a bit * Move quotient|n to top of file * Replace factorisationPullToFront with slightly more generally useful factorisationHasAllPrimeFactors and a bit of logic * Fix import after merge * Clean up proof of 2-rough-n * Make argument to 2-rough-n implicit * Rename 2-rough-n to 2-rough * Complete merge, rewrite factorisation logic a bit Rewrite partially based on suggestions from James McKinna * Short circuit when candidate is greater than square root of product * Remove redefined lemma * Minor simplifications * Remove private pattern synonyms * Change name of lemma * Typo * Remove using list from import It feels like we're importing half the module anyway * Clean up proof * Fixes after merge * Addressed some feedback * Fix previous merge --------- Co-authored-by: Guillaume Allais <[email protected]> Co-authored-by: MatthewDaggitt <[email protected]>
- Loading branch information
1 parent
9a4453e
commit 6dcfbdd
Showing
4 changed files
with
267 additions
and
5 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,198 @@ | ||
| ------------------------------------------------------------------------ | ||
| -- 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 | ||
| open import Data.Nat.Properties | ||
| open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder) | ||
| open import Data.Nat.Primality | ||
| open import Data.Product as Π using (∃-syntax; _×_; _,_; proj₁; proj₂) | ||
| open import Data.List.Base using (List; []; _∷_; _++_; product) | ||
| open import Data.List.Membership.Propositional using (_∈_) | ||
| open import Data.List.Membership.Propositional.Properties using (∈-∃++) | ||
| open import Data.List.Relation.Unary.All as All using (All; []; _∷_) | ||
| open import Data.List.Relation.Unary.Any using (here; there) | ||
| open import Data.List.Relation.Binary.Permutation.Propositional | ||
| using (_↭_; prep; swap; ↭-reflexive; ↭-refl; ↭-trans; refl; module PermutationReasoning) | ||
| open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (product-↭; All-resp-↭; shift) | ||
| open import Data.Sum.Base using (inj₁; inj₂) | ||
| open import Function.Base using (_$_; _∘_; _|>_; flip) | ||
| open import Induction using (build) | ||
| open import Induction.Lexicographic using (_⊗_; [_⊗_]) | ||
| open import Relation.Nullary.Decidable using (yes; no) | ||
| open import Relation.Nullary.Negation using (contradiction) | ||
| open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; module ≡-Reasoning) | ||
|
|
||
| private | ||
| variable | ||
| n : ℕ | ||
|
|
||
| ------------------------------------------------------------------------ | ||
| -- Core definition | ||
|
|
||
| record PrimeFactorisation (n : ℕ) : Set where | ||
| field | ||
| factors : List ℕ | ||
| isFactorisation : n ≡ product factors | ||
| factorsPrime : All Prime factors | ||
|
|
||
| open PrimeFactorisation public using (factors) | ||
| open PrimeFactorisation | ||
|
|
||
| ------------------------------------------------------------------------ | ||
| -- Finding a factorisation | ||
|
|
||
| primeFactorisation[1] : PrimeFactorisation 1 | ||
| primeFactorisation[1] = record | ||
| { factors = [] | ||
| ; isFactorisation = refl | ||
| ; factorsPrime = [] | ||
| } | ||
|
|
||
| primeFactorisation[p] : Prime n → PrimeFactorisation n | ||
| primeFactorisation[p] {n} pr = record | ||
| { factors = n ∷ [] | ||
| ; isFactorisation = sym (*-identityʳ n) | ||
| ; factorsPrime = pr ∷ [] | ||
| } | ||
|
|
||
| -- 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 factors | ||
| -- over and over (this is the "m" and "rough" parameters) | ||
| -- * a witness that this limit is getting closer to the number of interest, in a | ||
| -- way that helps the termination checker (the "k" and "eq" parameters) | ||
| -- * 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 | ||
| factorise : ∀ n → .{{NonZero n}} → PrimeFactorisation n | ||
| factorise 1 = primeFactorisation[1] | ||
| factorise n₀@(2+ _) = build [ <-recBuilder ⊗ <-recBuilder ] P facRec (n₀ , suc n₀ ∸ 4) 2-rough refl | ||
| where | ||
| P : ℕ × ℕ → Set | ||
| P (n , k) = ∀ {m} → .{{NonTrivial n}} → .{{NonTrivial m}} → m Rough n → suc n ∸ m * m ≡ k → PrimeFactorisation n | ||
|
|
||
| facRec : ∀ n×k → (<-Rec ⊗ <-Rec) P n×k → P n×k | ||
| facRec (n , zero) _ rough eq = | ||
| -- Case 1: m * m > n, ∴ Prime n | ||
| primeFactorisation[p] (rough∧square>⇒prime rough (m∸n≡0⇒m≤n eq)) | ||
| facRec (n@(2+ _) , suc k) (recFactor , recQuotient) {m@(2+ _)} rough eq with m ∣? n | ||
| -- Case 2: m ∤ n, try larger m, reducing k accordingly | ||
| ... | no m∤n = recFactor (≤-<-trans (m∸n≤m k (m + m)) (n<1+n k)) {suc m} (∤⇒rough-suc m∤n rough) $ begin | ||
| suc n ∸ (suc m + m * suc m) ≡⟨ cong (λ # → suc n ∸ (suc m + #)) (*-suc m m) ⟩ | ||
| suc n ∸ (suc m + (m + m * m)) ≡⟨ cong (suc n ∸_) (+-assoc (suc m) m (m * m)) ⟨ | ||
| suc n ∸ (suc (m + m) + m * m) ≡⟨ cong (suc n ∸_) (+-comm (suc (m + m)) (m * m)) ⟩ | ||
| suc n ∸ (m * m + suc (m + m)) ≡⟨ ∸-+-assoc (suc n) (m * m) (suc (m + m)) ⟨ | ||
| (suc n ∸ m * m) ∸ suc (m + m) ≡⟨ cong (_∸ suc (m + m)) eq ⟩ | ||
| suc k ∸ suc (m + m) ∎ | ||
| where open ≡-Reasoning | ||
| -- Case 3: m ∣ n, record m and recurse on the quotient | ||
| ... | yes m∣n = record | ||
| { factors = m ∷ ps | ||
| ; isFactorisation = sym m*Πps≡n | ||
| ; factorsPrime = rough∧∣⇒prime rough m∣n ∷ primes | ||
| } | ||
| where | ||
| m<n : m < n | ||
| m<n = begin-strict | ||
| m <⟨ s≤s (≤-trans (m≤n+m m _) (+-monoʳ-≤ _ (m≤m+n m _))) ⟩ | ||
| pred (m * m) <⟨ s<s⁻¹ (m∸n≢0⇒n<m λ eq′ → 0≢1+n (trans (sym eq′) eq)) ⟩ | ||
| n ∎ | ||
| where open ≤-Reasoning | ||
|
|
||
| q = quotient m∣n | ||
|
|
||
| instance _ = n>1⇒nonTrivial (quotient>1 m∣n m<n) | ||
|
|
||
| factorisation[q] : PrimeFactorisation q | ||
| factorisation[q] = recQuotient (quotient-< m∣n) (suc q ∸ m * m) (rough∧∣⇒rough rough (quotient-∣ m∣n)) refl | ||
|
|
||
| ps = factors factorisation[q] | ||
|
|
||
| primes = factorsPrime factorisation[q] | ||
|
|
||
| m*Πps≡n : m * product ps ≡ n | ||
| m*Πps≡n = begin | ||
| m * product ps ≡⟨ cong (m *_) (isFactorisation factorisation[q]) ⟨ | ||
| m * q ≡⟨ m∣n⇒n≡m*quotient m∣n ⟨ | ||
| n ∎ | ||
| where open ≡-Reasoning | ||
|
|
||
| ------------------------------------------------------------------------ | ||
| -- Properties of a factorisation | ||
|
|
||
| factorisationHasAllPrimeFactors : ∀ {as} {p} → Prime p → p ∣ product as → All Prime as → p ∈ as | ||
| factorisationHasAllPrimeFactors {[]} {2+ p} pPrime p∣Πas [] = contradiction (∣1⇒≡1 p∣Πas) λ () | ||
| factorisationHasAllPrimeFactors {a ∷ as} {p} pPrime p∣aΠas (aPrime ∷ asPrime) with euclidsLemma a (product as) pPrime p∣aΠas | ||
| ... | inj₂ p∣Πas = there (factorisationHasAllPrimeFactors pPrime p∣Πas asPrime) | ||
| ... | inj₁ p∣a with prime⇒irreducible aPrime p∣a | ||
| ... | inj₁ refl = contradiction pPrime ¬prime[1] | ||
| ... | inj₂ refl = here refl | ||
|
|
||
| private | ||
| factorisationUnique′ : (as bs : List ℕ) → product as ≡ product bs → All Prime as → All Prime bs → as ↭ bs | ||
| factorisationUnique′ [] [] Πas≡Πbs asPrime bsPrime = refl | ||
| factorisationUnique′ [] (b@(2+ _) ∷ bs) Πas≡Πbs prime[as] (_ ∷ prime[bs]) = | ||
| contradiction Πas≡Πbs (<⇒≢ Πas<Πbs) | ||
| where | ||
| Πas<Πbs : product [] < product (b ∷ bs) | ||
| Πas<Πbs = begin-strict | ||
| 1 ≡⟨⟩ | ||
| 1 * 1 <⟨ *-monoˡ-< 1 {1} {b} sz<ss ⟩ | ||
| b * 1 ≤⟨ *-monoʳ-≤ b (productOfPrimes≥1 prime[bs]) ⟩ | ||
| b * product bs ≡⟨⟩ | ||
| product (b ∷ bs) ∎ | ||
| where open ≤-Reasoning | ||
|
|
||
| factorisationUnique′ (a ∷ as) bs Πas≡Πbs (prime[a] ∷ prime[as]) prime[bs] = 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 with ys , zs , p ← ∈-∃++ (factorisationHasAllPrimeFactors prime[a] a∣Πbs prime[bs]) | ||
| = ys ++ zs , ↭-trans (↭-reflexive p) (shift a ys zs) | ||
|
|
||
| bs′ = proj₁ shuffle | ||
| bs↭a∷bs′ = proj₂ shuffle | ||
|
|
||
| Πas≡Πbs′ : product as ≡ product bs′ | ||
| Πas≡Πbs′ = *-cancelˡ-≡ (product as) (product bs′) a {{prime⇒nonZero prime[a]}} $ begin | ||
| a * product as ≡⟨ Πas≡Πbs ⟩ | ||
| product bs ≡⟨ product-↭ bs↭a∷bs′ ⟩ | ||
| a * product bs′ ∎ | ||
| where open ≡-Reasoning | ||
|
|
||
| prime[bs'] : All Prime bs′ | ||
| prime[bs'] = All.tail (All-resp-↭ bs↭a∷bs′ prime[bs]) | ||
|
|
||
| a∷as↭bs : a ∷ as ↭ bs | ||
| a∷as↭bs = begin | ||
| a ∷ as <⟨ factorisationUnique′ as bs′ Πas≡Πbs′ prime[as] prime[bs'] ⟩ | ||
| a ∷ bs′ ↭⟨ bs↭a∷bs′ ⟨ | ||
| bs ∎ | ||
| where open PermutationReasoning | ||
|
|
||
| factorisationUnique : (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 |