Add prime factorization and its properties #1969
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 | ||
|
|
||
MatthewDaggitt marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| open PrimeFactorisation public using (factors) | ||
| open PrimeFactorisation | ||
|
|
||
| ------------------------------------------------------------------------ | ||
| -- Finding a factorisation | ||
Taneb marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| 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 | ||
jamesmckinna marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| suc n ∸ (suc m + m * suc m) ≡⟨ cong (λ # → suc n ∸ (suc m + #)) (*-suc m m) ⟩ | ||
|
There was a problem hiding this comment. Can this equality reasoning be simplified or made more clear? There was a problem hiding this comment. Yes, probably, and I will look at this in my (eventual) review. Glad that I held off until you made the sqrt breakthrough ;-) UPDATED: I think on balance, invoke the solver begin
suc n ∸ (suc m) * (suc m) ≡⟨ cong (suc n ∸_) [1+m]*[1+m]≡m*m+[1+2*m] ⟩
suc n ∸ (m * m + suc (2 * m)) ≡˘⟨ ∸-+-assoc (suc n) (m * m) (suc (2 * m)) ⟩
(suc n ∸ m * m) ∸ suc (2 * m) ≡⟨ cong (_∸ suc (2 * m)) eq ⟩
suc k ∸ suc (2 * m) ∎
where
open ≡-Reasoning
open +-*-Solver using (solve; _:*_; _:+_; con; _:=_)
[1+m]*[1+m]≡m*m+[1+2*m] : (suc m) * (suc m) ≡ m * m + suc (2 * m)
[1+m]*[1+m]≡m*m+[1+2*m] = solve 1 (λ m → (con 1 :+ m) :* (con 1 :+ m) := (m :* m) :+ (con 1 :+ (con 2 :* m))) refl 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 _))) ⟩ | ||
|
There was a problem hiding this comment. Can this step of the inequality reasoning be made more legible? There was a problem hiding this comment. Yes, I'd say very probably... but I'll investigate! UPDATED: no, but in the interests of isolating some lemmas, much like with the other piece of equational reasoning, I came up with this instead: where
[1+n]<n*n : ∀ {n} → .{{NonTrivial n}} → suc n < n * n
[1+n]<n*n {n@(2+ m)} rewrite *-suc m m = s<s $ s<s $ begin
n ≤⟨ m≤n+m _ m ⟩
m + n ≤⟨ +-monoʳ-≤ m (m≤m+n n _) ⟩
m + (n + m * n) ∎
where open ≤-Reasoning
m<n : m < n
m<n with m≤n⇒m<n∨m≡n (rough⇒≤ rough)
... | inj₁ m<n = m<n
... | inj₂ refl = contradiction eq ¬eq
where
¬eq : suc n ∸ n * n ≢ suc k
¬eq rewrite m≤n⇒m∸n≡0 (<⇒≤ $ [1+n]<n*n) = 0≢1+n |
||
| 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 | ||
jamesmckinna marked this conversation as resolved.
Show resolved
Hide resolved
|
||
|
|
||
| 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 | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The 'traditional' notion of PrimeFactorisation uses a list of (multiplicity, prime) pairs and has the extra invariant that all primes are distinct.
I am not suggesting you change this definition - but you should probably comment on your design choice, so that this aspect doesn't puzzle a maintainer years down the road.