From 98dff4fa83ae7ddc244639d0cd7bcd001347e7c6 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Sat, 13 May 2023 07:01:27 +0200 Subject: [PATCH 01/38] Add prime factorization and its properties --- .../Permutation/Propositional/Properties.agda | 28 +++- src/Data/Nat/Divisibility.agda | 6 + src/Data/Nat/Primality.agda | 19 ++- src/Data/Nat/Primality/Factorization.agda | 122 ++++++++++++++++++ src/Data/Nat/Rough.agda | 62 +++++++++ 5 files changed, 231 insertions(+), 6 deletions(-) create mode 100644 src/Data/Nat/Primality/Factorization.agda create mode 100644 src/Data/Nat/Rough.agda diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index 700fc277ff..470c9f3d78 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/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 + diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index 07a80bcdd9..a5039c66bd 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/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)) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index e634095eea..12906d3820 100644 --- a/src/Data/Nat/Primality.agda +++ b/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

⇒≢ (<-transʳ (*-monoˡ-≤ (2 + k) q≤1) (<-transʳ (≤-reflexive (+-identityʳ (2 + k))) (≤‴⇒≤ 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 Date: Sat, 13 May 2023 07:11:37 +0200 Subject: [PATCH 02/38] Add missing header comment I'd missed this when copy-pasting from my old code in a separate repo --- src/Data/Nat/Primality/Factorization.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Data/Nat/Primality/Factorization.agda b/src/Data/Nat/Primality/Factorization.agda index 6610a08b81..3785156b87 100644 --- a/src/Data/Nat/Primality/Factorization.agda +++ b/src/Data/Nat/Primality/Factorization.agda @@ -93,6 +93,9 @@ factorize (suc (suc n)) = <-rec (λ n′ → ∀ {k} → 2 ≤ n′ → k ≤‴ 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) From 9c054498a1dbfa653aad622111d09e2ed6d64467 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 15 May 2023 12:00:59 +0200 Subject: [PATCH 03/38] Remove completely trivial lemma --- src/Data/Nat/Primality/Factorization.agda | 4 ++-- src/Data/Nat/Rough.agda | 9 --------- 2 files changed, 2 insertions(+), 11 deletions(-) diff --git a/src/Data/Nat/Primality/Factorization.agda b/src/Data/Nat/Primality/Factorization.agda index 3785156b87..8d6de267dd 100644 --- a/src/Data/Nat/Primality/Factorization.agda +++ b/src/Data/Nat/Primality/Factorization.agda @@ -62,7 +62,7 @@ factorize (suc (suc n)) = <-rec (λ n′ → ∀ {k} → 2 ≤ n′ → k ≤‴ 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-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 Date: Mon, 15 May 2023 12:04:17 +0200 Subject: [PATCH 04/38] Use equational reasoning in quotient|n proof --- src/Data/Nat/Divisibility.agda | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index a5039c66bd..727874fa8e 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -305,4 +305,8 @@ m≤n⇒m!∣n! m≤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)) +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 From 7ec38012ee349607731fec10028d2a6eda4a5dfb Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 15 May 2023 12:04:39 +0200 Subject: [PATCH 05/38] Fix typo in module header --- src/Data/Nat/Primality/Factorization.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Primality/Factorization.agda b/src/Data/Nat/Primality/Factorization.agda index 8d6de267dd..24962fed6f 100644 --- a/src/Data/Nat/Primality/Factorization.agda +++ b/src/Data/Nat/Primality/Factorization.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Prime factorization of naturla numbers and its properties +-- Prime factorization of natural numbers and its properties ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} From 8e0d749e2e33df22abb871bd63741de14b7cc338 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 15 May 2023 12:08:16 +0200 Subject: [PATCH 06/38] Factorization => Factorisation --- ...{Factorization.agda => Factorisation.agda} | 76 +++++++++---------- 1 file changed, 38 insertions(+), 38 deletions(-) rename src/Data/Nat/Primality/{Factorization.agda => Factorisation.agda} (62%) diff --git a/src/Data/Nat/Primality/Factorization.agda b/src/Data/Nat/Primality/Factorisation.agda similarity index 62% rename from src/Data/Nat/Primality/Factorization.agda rename to src/Data/Nat/Primality/Factorisation.agda index 24962fed6f..11e86101fb 100644 --- a/src/Data/Nat/Primality/Factorization.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -1,12 +1,12 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Prime factorization of natural numbers and its properties +-- Prime factorisation of natural numbers and its properties ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} -module Data.Nat.Primality.Factorization where +module Data.Nat.Primality.Factorisation where open import Data.Empty open import Data.Nat.Base @@ -29,15 +29,15 @@ open import Relation.Binary.PropositionalEquality as ≡ -- Core definition ------------------------------------------------------------------------ -record Factorization (n : ℕ) : Set where +record Factorisation (n : ℕ) : Set where field factors : List ℕ - isFactorization : product factors ≡ n + isFactorisation : product factors ≡ n factorsPrime : All Prime factors -open Factorization public using (factors) +open Factorisation public using (factors) --- Finding a factorization +-- Finding a factorisation ------------------------------------------------------------------------ -- this builds up three important things: @@ -46,32 +46,32 @@ open Factorization public using (factors) -- 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 +-- * 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 -factorize : ∀ n → .{{NonZero n}} → Factorization n -factorize 1 = record +factorise : ∀ n → .{{NonZero n}} → Factorisation n +factorise 1 = record { factors = [] - ; isFactorization = refl + ; isFactorisation = 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)) +factorise (suc (suc n)) = <-rec (λ n′ → ∀ {k} → 2 ≤ n′ → k ≤‴ n′ → k Rough n′ → Factorisation n′) factoriseRec (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 + factoriseRec : ∀ n → <-Rec (λ n′ → ∀ {k} → 2 ≤ n′ → k ≤‴ n′ → k Rough n′ → Factorisation n′) n → ∀ {k} → 2 ≤ n → k ≤‴ n → k Rough n → Factorisation n + factoriseRec (suc (suc n)) rec (s≤s (s≤s n≤z)) ≤‴-refl k-rough-n = record { factors = 2 + n ∷ [] - ; isFactorization = *-identityʳ (2 + n) + ; isFactorisation = *-identityʳ (2 + n) ; factorsPrime = (λ 2≤d d-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 : Factorisation (quotient k∣n) res = rec (quotient k∣n) q Date: Mon, 15 May 2023 12:29:04 +0200 Subject: [PATCH 07/38] Use Nat lemma in extend-|/ --- src/Data/Nat/Rough.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Nat/Rough.agda b/src/Data/Nat/Rough.agda index 430dde6e91..0cfe525b57 100644 --- a/src/Data/Nat/Rough.agda +++ b/src/Data/Nat/Rough.agda @@ -12,8 +12,9 @@ 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.Nat.Properties using (_≟_; <-trans; ≤∧≢⇒<; m<1+n⇒m Date: Mon, 15 May 2023 15:11:40 +0100 Subject: [PATCH 08/38] [ cleanup ] part of the proof --- src/Data/Nat/Primality/Factorisation.agda | 49 +++++++++++++++-------- 1 file changed, 32 insertions(+), 17 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 11e86101fb..357a8db65c 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -50,44 +50,59 @@ open Factorisation public using (factors) -- 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) + factorise : ∀ n → .{{NonZero n}} → Factorisation n factorise 1 = record { factors = [] ; isFactorisation = refl ; factorsPrime = [] } -factorise (suc (suc n)) = <-rec (λ n′ → ∀ {k} → 2 ≤ n′ → k ≤‴ n′ → k Rough n′ → Factorisation n′) factoriseRec (2 + n) {2} (s≤s (s≤s z≤n)) (≤⇒≤‴ (s≤s (s≤s z≤n))) (2-rough-n (2 + n)) +factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+n) (2-rough-n (2 + n)) where - factoriseRec : ∀ n → <-Rec (λ n′ → ∀ {k} → 2 ≤ n′ → k ≤‴ n′ → k Rough n′ → Factorisation n′) n → ∀ {k} → 2 ≤ n → k ≤‴ n → k Rough n → Factorisation n - factoriseRec (suc (suc n)) rec (s≤s (s≤s n≤z)) ≤‴-refl k-rough-n = record + + P : ℕ → Set + P n′ = ∀ {k} → 2 ≤ n′ → k ≤‴ n′ → k Rough n′ → Factorisation 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 = (λ 2≤d d⇒≢ (<-transʳ (*-monoˡ-≤ (2 + k) q≤1) (<-transʳ (≤-reflexive (+-identityʳ (2 + k))) (≤‴⇒≤ k-nonZero (<-transˡ (s≤s z≤n) 2≤q) ⦄ (s≤s (s≤s z≤n))) (≤-reflexive (sym (_∣_.equality k∣n))) + 2≤q = ≮⇒≥ (λ q<2 → contradiction (_∣_.equality k∣n) (>⇒≢ (prf (≤-pred q<2)))) where + + prf : quotient k∣n ≤ 1 → k∣n .quotient * 2+ k < 2+ n + prf q≤1 = let open ≤-Reasoning in begin-strict + k∣n .quotient * 2+ k ≤⟨ *-monoˡ-≤ (2 + k) q≤1 ⟩ + 2 + k + 0 ≡⟨ +-identityʳ (2 + k) ⟩ + 2 + k <⟨ ≤‴⇒≤ k-nonZero (<-transˡ (s≤s z≤n) 2≤q) ⦄ 2≤2+n) (≤-reflexive (sym (_∣_.equality k∣n))) res : Factorisation (quotient k∣n) res = rec (quotient k∣n) q Date: Mon, 15 May 2023 16:09:58 +0100 Subject: [PATCH 09/38] [ cleanup ] finishing up the job --- src/Data/Nat/Primality/Factorisation.agda | 115 +++++++++++++++++----- 1 file changed, 88 insertions(+), 27 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 357a8db65c..9d6b74a8b3 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -53,6 +53,7 @@ open Factorisation public using (factors) 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}} → Factorisation n factorise 1 = record @@ -84,29 +85,49 @@ factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+ ; factorsPrime = roughn∧∣n⇒prime k-rough-n 2≤2+n k∣n ∷ Factorisation.factorsPrime res } where + + q : ℕ + q = quotient k∣n + -- we know that k < n, so if q is 0 or 1 then q * k < n - 2≤q : 2 ≤ quotient k∣n + 2≤q : 2 ≤ q 2≤q = ≮⇒≥ (λ q<2 → contradiction (_∣_.equality k∣n) (>⇒≢ (prf (≤-pred q<2)))) where - prf : quotient k∣n ≤ 1 → k∣n .quotient * 2+ k < 2+ n - prf q≤1 = let open ≤-Reasoning in begin-strict - k∣n .quotient * 2+ k ≤⟨ *-monoˡ-≤ (2 + k) q≤1 ⟩ - 2 + k + 0 ≡⟨ +-identityʳ (2 + k) ⟩ - 2 + k <⟨ ≤‴⇒≤ k-nonZero (<-transˡ (s≤s z≤n) 2≤q) ⦄ 2≤2+n) (≤-reflexive (sym (_∣_.equality k∣n))) + q-nonZero 0 Date: Mon, 15 May 2023 16:26:18 +0100 Subject: [PATCH 10/38] [ cleanup ] a little bit more --- src/Data/Nat/Primality/Factorisation.agda | 25 +++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 9d6b74a8b3..7bd73f7f06 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -21,7 +21,7 @@ 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 Function.Base using (_$_; _∘_; _|>_; flip) open import Relation.Nullary.Decidable open import Relation.Nullary.Negation open import Relation.Binary.PropositionalEquality as ≡ @@ -36,6 +36,7 @@ record Factorisation (n : ℕ) : Set where factorsPrime : All Prime factors open Factorisation public using (factors) +open Factorisation -- Finding a factorisation ------------------------------------------------------------------------ @@ -80,9 +81,9 @@ factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+ factoriseRec (2+ n) rec {suc (suc k)} 2≤2+n (≤‴-step k Date: Mon, 15 May 2023 16:32:22 +0100 Subject: [PATCH 11/38] [ cleanup ] the import list --- src/Data/Nat/Primality/Factorisation.agda | 29 ++++++++++++----------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 7bd73f7f06..543eb4eb2c 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -8,23 +8,24 @@ module Data.Nat.Primality.Factorisation where -open import Data.Empty +open import Data.Empty using (⊥-elim) open import Data.Nat.Base -open import Data.Nat.Divisibility +open import Data.Nat.Divisibility using (_∣_; _∣?_; quotient; quotient∣n; ∣-trans; ∣1⇒≡1; divides) 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.Nat.Induction using (<-Rec; <-rec) +open import Data.Nat.Primality using (Prime; euclidsLemma; ∣p⇒≡1∨≡p; Prime⇒NonZero) +open import Data.Nat.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 ↭ -open import Data.List.Relation.Binary.Permutation.Propositional.Properties -open import Data.Sum.Base + using (_↭_; prep; swap; ↭-refl; refl; module PermutationReasoning) +open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (productPreserves↭⇒≡; All-resp-↭) +open import Data.Sum.Base using (inj₁; inj₂) open import Function.Base using (_$_; _∘_; _|>_; flip) -open import Relation.Nullary.Decidable -open import Relation.Nullary.Negation -open import Relation.Binary.PropositionalEquality as ≡ +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 ------------------------------------------------------------------------ @@ -149,7 +150,7 @@ factorisationPullToFront {a ∷ as} {p} pPrime p∣aΠas (aPrime ∷ 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 ⟩ + a ∷ p ∷ as′ ↭⟨ swap a p refl ⟩ p ∷ a ∷ as′ ∎ where open PermutationReasoning ... | inj₁ p∣a with ∣p⇒≡1∨≡p p aPrime p∣a From dd898f9be14b277d08cde850e5c4bcfe0ab559c1 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Mon, 15 May 2023 16:34:29 +0100 Subject: [PATCH 12/38] [ fix ] header style --- src/Data/Nat/Primality/Factorisation.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 543eb4eb2c..e402f6f9a3 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -27,8 +27,8 @@ 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 ------------------------------------------------------------------------ +-- Core definition record Factorisation (n : ℕ) : Set where field @@ -39,8 +39,8 @@ record Factorisation (n : ℕ) : Set where open Factorisation public using (factors) open Factorisation --- Finding a factorisation ------------------------------------------------------------------------ +-- Finding a factorisation -- this builds up three important things: -- * a proof that every number we've gotten to so far has increasingly higher From bec7b21cb14d3bff50199f624264b60491a7b238 Mon Sep 17 00:00:00 2001 From: Guillaume Allais Date: Mon, 15 May 2023 17:09:27 +0100 Subject: [PATCH 13/38] [ fix ] broken merge: missing import --- .../Relation/Binary/Permutation/Propositional/Properties.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index 3623338531..c435bb8aa5 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -30,7 +30,7 @@ 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 private @@ -373,4 +373,3 @@ productPreserves↭⇒≡ (swap {xs} {ys} x y r) = begin (y * x) * product ys ≡⟨ *-assoc y x (product ys) ⟩ y * (x * product ys) ∎ where open ≡-Reasoning - From 294bdade4b86b78eb8569c3c560003763516683c Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 12 Jun 2023 10:15:00 +0200 Subject: [PATCH 14/38] Move Data.Nat.Rough to Data.Nat.Primality.Rough --- src/Data/Nat/Primality/Factorisation.agda | 2 +- src/Data/Nat/{ => Primality}/Rough.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) rename src/Data/Nat/{ => Primality}/Rough.agda (98%) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index e402f6f9a3..72f951cc19 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -14,7 +14,7 @@ open import Data.Nat.Divisibility using (_∣_; _∣?_; quotient; quotient∣n; 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.Rough using (_Rough_; 2-rough-n; extend-∤; roughn∧∣n⇒prime) +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; []; _∷_) diff --git a/src/Data/Nat/Rough.agda b/src/Data/Nat/Primality/Rough.agda similarity index 98% rename from src/Data/Nat/Rough.agda rename to src/Data/Nat/Primality/Rough.agda index 0cfe525b57..f1b83ef7d4 100644 --- a/src/Data/Nat/Rough.agda +++ b/src/Data/Nat/Primality/Rough.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -module Data.Nat.Rough where +module Data.Nat.Primality.Rough where open import Data.Nat.Base using (ℕ; suc; _≤_; _<_; z≤n; s≤s; _+_) open import Data.Nat.Divisibility using (_∣_; _∤_; ∣-trans; ∣1⇒≡1) From 8796eee72286fc214a17d94aada3cef4603341e8 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 12 Jun 2023 10:16:56 +0200 Subject: [PATCH 15/38] =?UTF-8?q?Rename=20productPreserves=E2=86=AD?= =?UTF-8?q?=E2=87=92=E2=89=A1=20to=20product-=E2=86=AD?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Binary/Permutation/Propositional/Properties.agda | 12 ++++++------ src/Data/Nat/Primality/Factorisation.agda | 4 ++-- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index c435bb8aa5..e3cb7ca9e9 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -363,13 +363,13 @@ module _ {ℓ} {R : Rel A ℓ} (R? : Decidable R) where ------------------------------------------------------------------------ -- 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 +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) (productPreserves↭⇒≡ r) ⟩ + (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 diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 72f951cc19..60e7c300cf 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -20,7 +20,7 @@ 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 (productPreserves↭⇒≡; All-resp-↭) +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) @@ -188,7 +188,7 @@ factorisationUnique′ (a ∷ as) bs Πas≡Πbs (aPrime ∷ asPrime) bsPrime = Π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 ≡⟨ productPreserves↭⇒≡ bs↭a∷bs′ ⟩ + product bs ≡⟨ product-↭ bs↭a∷bs′ ⟩ a * product bs′ ∎ where open ≡-Reasoning bs′Prime : All Prime bs′ From f0948e8abf47448ec8309de40ab7c1cf61b88de7 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 12 Jun 2023 10:21:13 +0200 Subject: [PATCH 16/38] Use proof of Prime=>NonZero --- src/Data/Nat/Primality.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 12906d3820..9080bdb70b 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -21,7 +21,7 @@ open import Relation.Nullary.Decidable as Dec open import Relation.Nullary.Negation using (¬_; contradiction) open import Relation.Unary using (Decidable) open import Relation.Binary.PropositionalEquality.Core - using (_≡_; refl; sym; cong; subst) + using (_≡_; refl; sym; cong) private variable @@ -153,6 +153,6 @@ 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 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

Date: Mon, 12 Jun 2023 11:41:06 +0200 Subject: [PATCH 17/38] Open reasoning once in factoriseRec --- src/Data/Nat/Primality/Factorisation.agda | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 60e7c300cf..7e442ed0b6 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -87,6 +87,7 @@ factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+ ; factorsPrime = roughn∧∣n⇒prime k-rough-n 2≤2+n k∣n ∷ factorsPrime res } where + open ≤-Reasoning q : ℕ q = quotient k∣n @@ -100,19 +101,19 @@ factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+ q * 2+ k ≤⟨ *-monoˡ-≤ (2 + k) q≤1 ⟩ 2 + k + 0 ≡⟨ +-identityʳ (2 + k) ⟩ 2 + k <⟨ ≤‴⇒≤ k-nonZero 0 Date: Mon, 12 Jun 2023 11:41:48 +0200 Subject: [PATCH 18/38] Rename Factorisation => PrimeFactorisation --- src/Data/Nat/Primality/Factorisation.agda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 7e442ed0b6..5c343fe6ae 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -30,14 +30,14 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; modu ------------------------------------------------------------------------ -- Core definition -record Factorisation (n : ℕ) : Set where +record PrimeFactorisation (n : ℕ) : Set where field factors : List ℕ isFactorisation : product factors ≡ n factorsPrime : All Prime factors -open Factorisation public using (factors) -open Factorisation +open PrimeFactorisation public using (factors) +open PrimeFactorisation ------------------------------------------------------------------------ -- Finding a factorisation @@ -57,7 +57,7 @@ private pattern 2≤2+n = s≤s (s≤s z≤n) pattern 1<2+n = 2≤2+n -factorise : ∀ n → .{{NonZero n}} → Factorisation n +factorise : ∀ n → .{{NonZero n}} → PrimeFactorisation n factorise 1 = record { factors = [] ; isFactorisation = refl @@ -67,7 +67,7 @@ factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+ where P : ℕ → Set - P n′ = ∀ {k} → 2 ≤ n′ → k ≤‴ n′ → k Rough n′ → Factorisation n′ + 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 @@ -118,7 +118,7 @@ factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+ q≮2+k : q ≮ 2 + k q≮2+k q Date: Mon, 12 Jun 2023 11:44:48 +0200 Subject: [PATCH 19/38] Move wheres around --- src/Data/Nat/Primality/Factorisation.agda | 116 ++++++++++++---------- 1 file changed, 61 insertions(+), 55 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 5c343fe6ae..072534b9ff 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -143,16 +143,17 @@ factorisationPullToFront : ∀ {as} {p} → Prime p → p ∣ product as → All 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 +... | 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 + 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 @@ -161,52 +162,57 @@ factorisationPullToFront {a ∷ as} {p} pPrime p∣aΠas (aPrime ∷ asPrime) 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 + 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 + 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 From 4073e5f330d777b3722bc31d9799aeb6fcbc84dc Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 15 Aug 2023 14:25:25 +0200 Subject: [PATCH 20/38] Tidy up Rough a bit --- src/Data/Nat/Primality/Rough.agda | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/src/Data/Nat/Primality/Rough.agda b/src/Data/Nat/Primality/Rough.agda index f1b83ef7d4..12dcd2bbdc 100644 --- a/src/Data/Nat/Primality/Rough.agda +++ b/src/Data/Nat/Primality/Rough.agda @@ -19,6 +19,10 @@ open import Function.Base using (_∘_; flip) open import Relation.Nullary.Decidable.Core using (yes; no) open import Relation.Binary.PropositionalEquality.Core using (refl) +private + variable + k m n : ℕ + -- 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 @@ -28,26 +32,26 @@ k Rough n = ∀ {d} → 1 < d → d < k → d ∤ n 2-rough-n n {1} (s≤s ()) 1<2 2-rough-n n {suc (suc d)} 1 Date: Tue, 15 Aug 2023 14:26:17 +0200 Subject: [PATCH 21/38] Move quotient|n to top of file --- src/Data/Nat/Divisibility.agda | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index 1f835fed42..4945a54951 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -29,6 +29,16 @@ import Relation.Binary.PropositionalEquality.Properties as PropEq open import Data.Nat.Divisibility.Core public +------------------------------------------------------------------------ +-- 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 + ------------------------------------------------------------------------ -- Relationship with _%_ @@ -305,12 +315,3 @@ m≤n⇒m!∣n! m≤n = help (≤⇒≤′ 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 From 87022d854c042e7e95e7152bcacc45180a7f20aa Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 15 Aug 2023 14:42:32 +0200 Subject: [PATCH 22/38] Replace factorisationPullToFront with slightly more generally useful factorisationHasAllPrimeFactors and a bit of logic --- src/Data/Nat/Primality/Factorisation.agda | 32 +++++++++-------------- 1 file changed, 12 insertions(+), 20 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 072534b9ff..7ed0c65a9d 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -16,11 +16,14 @@ 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.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 as ↭ using (_↭_; prep; swap; ↭-refl; refl; module PermutationReasoning) -open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (product-↭; All-resp-↭) +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 Relation.Nullary.Decidable using (yes; no) @@ -139,25 +142,13 @@ 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 - +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 ∣p⇒≡1∨≡p p aPrime p∣a ... | inj₁ refl = ⊥-elim pPrime -... | inj₂ refl = as , ↭-refl +... | inj₂ refl = here refl factorisationUnique′ : (as bs : List ℕ) → product as ≡ product bs → All Prime as → All Prime bs → as ↭ bs factorisationUnique′ [] [] Πas≡Πbs asPrime bsPrime = refl @@ -184,7 +175,8 @@ factorisationUnique′ (a ∷ as) bs Πas≡Πbs (aPrime ∷ asPrime) bsPrime = where open ≡-Reasoning shuffle : ∃[ bs′ ] bs ↭ a ∷ bs′ - shuffle = factorisationPullToFront aPrime a∣Πbs bsPrime + shuffle with ys , zs , p ← ∈-∃++ (factorisationHasAllPrimeFactors aPrime a∣Πbs bsPrime) + = ys ++ zs , ↭.↭-trans (↭.↭-reflexive p) (shift a ys zs) bs′ = proj₁ shuffle bs↭a∷bs′ = proj₂ shuffle From 230d4987d5e9a1fc972cf520153b71a71d40a55a Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 3 Oct 2023 11:40:50 +0200 Subject: [PATCH 23/38] Fix import after merge --- .../Relation/Binary/Permutation/Propositional/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda index 72606c5be5..7eac2c7d50 100644 --- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda @@ -26,7 +26,7 @@ open import Data.Product.Base using (_,_; _×_; ∃; ∃₂) open import Function.Base using (_∘_; _⟨_⟩_) open import Level using (Level) open import Relation.Unary using (Pred) -open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_) +open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_) open import Relation.Binary.Definitions using (_Respects_; Decidable) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_ ; refl ; cong; cong₂; _≢_; module ≡-Reasoning) From 1f1ed8e2936cccad06b8ed5ae7dcf986017a3a70 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 3 Oct 2023 11:45:21 +0200 Subject: [PATCH 24/38] Clean up proof of 2-rough-n --- src/Data/Nat/Primality/Rough.agda | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Data/Nat/Primality/Rough.agda b/src/Data/Nat/Primality/Rough.agda index 12dcd2bbdc..cdedb49275 100644 --- a/src/Data/Nat/Primality/Rough.agda +++ b/src/Data/Nat/Primality/Rough.agda @@ -12,7 +12,7 @@ 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; ≤∧≢⇒<; m<1+n⇒md with () ← ≤⇒≯ 1d extend-∤ : k Rough n → k ∤ n → suc k Rough n extend-∤ k-rough-n k∤n 1 Date: Tue, 3 Oct 2023 11:46:12 +0200 Subject: [PATCH 25/38] Make argument to 2-rough-n implicit --- src/Data/Nat/Primality/Factorisation.agda | 6 +++--- src/Data/Nat/Primality/Rough.agda | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 7ed0c65a9d..b9fefe723a 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -66,7 +66,7 @@ factorise 1 = record ; isFactorisation = refl ; factorsPrime = [] } -factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+n) (2-rough-n (2 + n)) +factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+n) 2-rough-n where P : ℕ → Set @@ -79,9 +79,9 @@ factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+ ; factorsPrime = k-rough-n ∷ [] } factoriseRec (2+ n) rec {0} 2≤2+n (≤‴-step (≤‴-step kd with () ← ≤⇒≯ 1d +2-rough-n : 2 Rough n +2-rough-n 1d with () ← ≤⇒≯ 1d extend-∤ : k Rough n → k ∤ n → suc k Rough n extend-∤ k-rough-n k∤n 1 Date: Tue, 3 Oct 2023 11:47:58 +0200 Subject: [PATCH 26/38] Rename 2-rough-n to 2-rough --- src/Data/Nat/Primality/Factorisation.agda | 8 ++++---- src/Data/Nat/Primality/Rough.agda | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index b9fefe723a..3733671452 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -14,7 +14,7 @@ open import Data.Nat.Divisibility using (_∣_; _∣?_; quotient; quotient∣n; 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.Nat.Primality.Rough using (_Rough_; 2-rough; 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.Membership.Propositional using (_∈_) @@ -66,7 +66,7 @@ factorise 1 = record ; isFactorisation = refl ; factorsPrime = [] } -factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+n) 2-rough-n +factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+n) 2-rough where P : ℕ → Set @@ -79,9 +79,9 @@ factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+ ; factorsPrime = k-rough-n ∷ [] } factoriseRec (2+ n) rec {0} 2≤2+n (≤‴-step (≤‴-step kd with () ← ≤⇒≯ 1d +2-rough : 2 Rough n +2-rough 1d with () ← ≤⇒≯ 1d extend-∤ : k Rough n → k ∤ n → suc k Rough n extend-∤ k-rough-n k∤n 1 Date: Thu, 21 Dec 2023 22:12:45 +0100 Subject: [PATCH 27/38] Complete merge, rewrite factorisation logic a bit Rewrite partially based on suggestions from James McKinna --- src/Data/Nat/Primality/Factorisation.agda | 122 +++++++++------------- src/Data/Nat/Primality/Rough.agda | 56 ---------- 2 files changed, 50 insertions(+), 128 deletions(-) delete mode 100644 src/Data/Nat/Primality/Rough.agda diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 3733671452..87ae337062 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -10,11 +10,10 @@ 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.Divisibility using (_∣_; _∣?_; quotient; quotient∣n; ∣-trans; ∣1⇒≡1; divides; quotient-<; m|n⇒n≡m*quotient; hasNonTrivialDivisor; quotient≢0; quotient-∣; quotient>1) 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; extend-∤; roughn∧∣n⇒prime) +open import Data.Nat.Primality using (Prime; prime; euclidsLemma; prime⇒irreducible; prime⇒nonZero; _Rough_; 2-rough; ∤⇒rough-suc; rough∧∣⇒prime; ¬prime[1]; rough∧∣⇒rough) open import Data.Product as Π using (∃-syntax; _,_; proj₁; proj₂) open import Data.List.Base using (List; []; _∷_; _++_; product) open import Data.List.Membership.Propositional using (_∈_) @@ -28,7 +27,7 @@ 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) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; module ≡-Reasoning) ------------------------------------------------------------------------ -- Core definition @@ -48,9 +47,9 @@ open PrimeFactorisation -- 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) +-- 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≤n parameter) +-- 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 @@ -66,74 +65,53 @@ factorise 1 = record ; isFactorisation = refl ; factorsPrime = [] } -factorise (2+ n) = <-rec P factoriseRec (2 + n) {2} 2≤2+n (≤⇒≤‴ 2≤2+n) 2-rough +factorise (2+ n₀) = <-rec P facRec (2+ n₀) 2-rough n₀ refl 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 ∷ [] + P n = ∀ {m} → .{{NonTrivial n}} → .{{NonTrivial m}} → m Rough n → (k : ℕ) → (n ≡ m + k) → PrimeFactorisation n + + facRec : ∀ n → <-Rec P n → P n + -- Case 1: m = n, ∴ Prime n + facRec (2+ _) rec {m} rough zero eq rewrite eq | +-identityʳ m = record + { factors = m ∷ [] + ; isFactorisation = *-identityʳ m + ; factorsPrime = prime rough ∷ [] } - factoriseRec (2+ n) rec {0} 2≤2+n (≤‴-step (≤‴-step k⇒≢ (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-nonZero 01⇒nonTrivial (quotient>1 m∣n md with () ← ≤⇒≯ 1d - -extend-∤ : k Rough n → k ∤ n → suc k Rough n -extend-∤ k-rough-n k∤n 1 Date: Fri, 22 Dec 2023 11:58:05 +0100 Subject: [PATCH 28/38] Short circuit when candidate is greater than square root of product --- src/Data/Nat/Primality.agda | 11 ++++ src/Data/Nat/Primality/Factorisation.agda | 64 ++++++++++++----------- 2 files changed, 45 insertions(+), 30 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 620f0c87b0..6745e9f38d 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -294,6 +294,17 @@ prime⇒rough (prime pr) = pr rough∧∣⇒prime : .{{NonTrivial p}} → p Rough n → p ∣ n → Prime p rough∧∣⇒prime r p∣n = prime (rough∧∣⇒rough r p∣n) +-- If a number n is m-rough, and m * m > n, then n must be prime. +rough∧>square⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n +rough∧>square⇒prime rough m*m>n = prime ¬composite + where + ¬composite : ¬ Composite _ + ¬composite (hasNonTrivialDivisor dn (*-mono-≤ + (≮⇒≥ λ q1⇒nonTrivial (quotient>1 d∣n d1) open import Data.Nat.Properties -open import Data.Nat.Induction using (<-Rec; <-rec) -open import Data.Nat.Primality using (Prime; prime; euclidsLemma; prime⇒irreducible; prime⇒nonZero; _Rough_; 2-rough; ∤⇒rough-suc; rough∧∣⇒prime; ¬prime[1]; rough∧∣⇒rough) -open import Data.Product as Π using (∃-syntax; _,_; proj₁; proj₂) +open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder) +open import Data.Nat.Primality using (Prime; prime; euclidsLemma; prime⇒irreducible; prime⇒nonZero; _Rough_; 2-rough; ∤⇒rough-suc; rough∧∣⇒prime; ¬prime[1]; rough∧∣⇒rough; rough∧>square⇒prime) +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 (∈-∃++) @@ -25,6 +25,8 @@ open import Data.List.Relation.Binary.Permutation.Propositional as ↭ 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) @@ -65,22 +67,30 @@ factorise 1 = record ; isFactorisation = refl ; factorsPrime = [] } -factorise (2+ n₀) = <-rec P facRec (2+ n₀) 2-rough n₀ refl +factorise n₀@(2+ _) = build [ <-recBuilder ⊗ <-recBuilder ] P facRec (n₀ , suc n₀ ∸ 4) 2-rough refl where - P : ℕ → Set - P n = ∀ {m} → .{{NonTrivial n}} → .{{NonTrivial m}} → m Rough n → (k : ℕ) → (n ≡ m + k) → PrimeFactorisation n - - facRec : ∀ n → <-Rec P n → P n - -- Case 1: m = n, ∴ Prime n - facRec (2+ _) rec {m} rough zero eq rewrite eq | +-identityʳ m = record - { factors = m ∷ [] - ; isFactorisation = *-identityʳ m - ; factorsPrime = prime rough ∷ [] + 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 + -- Case 1: m * m > n, ∴ Prime n + facRec (n , zero) _ rough eq = record + { factors = n ∷ [] + ; isFactorisation = *-identityʳ n + ; factorsPrime = rough∧>square⇒prime rough (m∸n≡0⇒m≤n eq) ∷ [] } - facRec n@(2+ _) rec {m@(2+ _)} rough (suc k) eq with m ∣? n - -- Case 2: m ∤ n, try larger m - ... | no m∤n = facRec n rec (∤⇒rough-suc m∤n rough) k (trans eq (+-suc m k)) - -- Case 3: m ∣ n: record m and recurse on the quotient + 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 (2 * 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)) ≡˘⟨ cong (λ # → suc n ∸ (m * m + suc (m + #))) (+-identityʳ 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 + -- Case 3: m ∣ n, record m and recurse on the quotient ... | yes m∣n = record { factors = m ∷ ps ; isFactorisation = m*Πps≡n @@ -89,28 +99,22 @@ factorise (2+ n₀) = <-rec P facRec (2+ n₀) 2-rough n₀ refl where m1⇒nonTrivial (quotient>1 m∣n m1⇒nonTrivial (quotient>1 m∣n m Date: Fri, 22 Dec 2023 13:22:42 +0100 Subject: [PATCH 29/38] Remove redefined lemma --- src/Data/Nat/Divisibility.agda | 10 ---------- src/Data/Nat/Primality/Factorisation.agda | 2 +- 2 files changed, 1 insertion(+), 11 deletions(-) diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index d2e508850d..abac2915a7 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -72,16 +72,6 @@ quotient-< {m} {n} m∣n = begin-strict n/m≡quotient : (m∣n : m ∣ n) .{{_ : NonZero m}} → n / m ≡ quotient m∣n n/m≡quotient {m = m} (divides-refl q) = m*n/n≡m q m ------------------------------------------------------------------------- --- 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 - ------------------------------------------------------------------------ -- Relationship with _%_ diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 2e309051c6..a551332959 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -10,7 +10,7 @@ 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; quotient-<; m|n⇒n≡m*quotient; hasNonTrivialDivisor; quotient≢0; quotient-∣; quotient>1) +open import Data.Nat.Divisibility using (_∣_; _∣?_; quotient; ∣-trans; ∣1⇒≡1; divides; quotient-<; m|n⇒n≡m*quotient; hasNonTrivialDivisor; quotient≢0; quotient-∣; quotient>1) open import Data.Nat.Properties open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder) open import Data.Nat.Primality using (Prime; prime; euclidsLemma; prime⇒irreducible; prime⇒nonZero; _Rough_; 2-rough; ∤⇒rough-suc; rough∧∣⇒prime; ¬prime[1]; rough∧∣⇒rough; rough∧>square⇒prime) From 510b7ec8fdc77b49e7d31874866dec186c8428cf Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 22 Dec 2023 14:54:36 +0100 Subject: [PATCH 30/38] Minor simplifications --- src/Data/Nat/Primality/Factorisation.agda | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index a551332959..41348c90d1 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -10,7 +10,7 @@ module Data.Nat.Primality.Factorisation where open import Data.Empty using (⊥-elim) open import Data.Nat.Base -open import Data.Nat.Divisibility using (_∣_; _∣?_; quotient; ∣-trans; ∣1⇒≡1; divides; quotient-<; m|n⇒n≡m*quotient; hasNonTrivialDivisor; quotient≢0; quotient-∣; quotient>1) +open import Data.Nat.Divisibility using (_∣_; _∣?_; quotient; ∣1⇒≡1; divides; quotient-<; m|n⇒n≡m*quotient; hasNonTrivialDivisor; quotient-∣; quotient>1) open import Data.Nat.Properties open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder) open import Data.Nat.Primality using (Prime; prime; euclidsLemma; prime⇒irreducible; prime⇒nonZero; _Rough_; 2-rough; ∤⇒rough-suc; rough∧∣⇒prime; ¬prime[1]; rough∧∣⇒rough; rough∧>square⇒prime) @@ -81,14 +81,13 @@ factorise n₀@(2+ _) = build [ <-recBuilder ⊗ <-recBuilder ] P facRec (n₀ , } 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 (2 * m)) (n<1+n k)) {suc m} (∤⇒rough-suc m∤n rough) $ begin + ... | 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)) ≡˘⟨ cong (λ # → suc n ∸ (m * m + suc (m + #))) (+-identityʳ 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) ∎ + 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 From 9f2ef51794588c7981579863f04d740966018a80 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 22 Dec 2023 14:55:41 +0100 Subject: [PATCH 31/38] Remove private pattern synonyms --- src/Data/Nat/Primality/Factorisation.agda | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 41348c90d1..9fb7611a38 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -56,11 +56,6 @@ open PrimeFactorisation -- 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 = [] @@ -139,7 +134,7 @@ factorisationUnique′ [] (suc (suc b) ∷ bs) Πas≡Πbs asPrime (bPrime ∷ b Πas<Πbs : product [] < product (2+ b ∷ bs) Πas<Πbs = begin-strict 1 ≡⟨⟩ - 1 * 1 <⟨ *-monoˡ-< 1 {1} {2 + b} 1<2+n ⟩ + 1 * 1 <⟨ *-monoˡ-< 1 {1} {2 + b} sz Date: Wed, 31 Jan 2024 10:11:10 +0100 Subject: [PATCH 32/38] Change name of lemma --- src/Data/Nat/Primality.agda | 8 ++++---- src/Data/Nat/Primality/Factorisation.agda | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 6745e9f38d..007a378df3 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -295,14 +295,14 @@ rough∧∣⇒prime : .{{NonTrivial p}} → p Rough n → p ∣ n → Prime p rough∧∣⇒prime r p∣n = prime (rough∧∣⇒rough r p∣n) -- If a number n is m-rough, and m * m > n, then n must be prime. -rough∧>square⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n -rough∧>square⇒prime rough m*m>n = prime ¬composite +rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n +rough∧square>⇒prime rough m*m>n = prime ¬composite where ¬composite : ¬ Composite _ ¬composite (hasNonTrivialDivisor dn (*-mono-≤ - (≮⇒≥ λ q1⇒nonTrivial (quotient>1 d∣n d1) open import Data.Nat.Properties open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder) -open import Data.Nat.Primality using (Prime; prime; euclidsLemma; prime⇒irreducible; prime⇒nonZero; _Rough_; 2-rough; ∤⇒rough-suc; rough∧∣⇒prime; ¬prime[1]; rough∧∣⇒rough; rough∧>square⇒prime) +open import Data.Nat.Primality using (Prime; prime; euclidsLemma; prime⇒irreducible; prime⇒nonZero; _Rough_; 2-rough; ∤⇒rough-suc; rough∧∣⇒prime; ¬prime[1]; rough∧∣⇒rough; rough∧square>⇒prime) open import Data.Product as Π using (∃-syntax; _×_; _,_; proj₁; proj₂) open import Data.List.Base using (List; []; _∷_; _++_; product) open import Data.List.Membership.Propositional using (_∈_) @@ -72,7 +72,7 @@ factorise n₀@(2+ _) = build [ <-recBuilder ⊗ <-recBuilder ] P facRec (n₀ , facRec (n , zero) _ rough eq = record { factors = n ∷ [] ; isFactorisation = *-identityʳ n - ; factorsPrime = rough∧>square⇒prime rough (m∸n≡0⇒m≤n eq) ∷ [] + ; factorsPrime = 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 From 286bc7e3efae5c183b7455b1cf8559a09bd80e4e Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 31 Jan 2024 10:11:37 +0100 Subject: [PATCH 33/38] Typo --- src/Data/Nat/Primality/Factorisation.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 65746bab97..509c078535 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -48,7 +48,7 @@ open PrimeFactorisation -- 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 +-- 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) From 50631906165a1b0eb683966dfba2307b1706294a Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 31 Jan 2024 10:12:14 +0100 Subject: [PATCH 34/38] Remove using list from import It feels like we're importing half the module anyway --- src/Data/Nat/Primality/Factorisation.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 509c078535..8cfb65b202 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -13,7 +13,7 @@ open import Data.Nat.Base open import Data.Nat.Divisibility using (_∣_; _∣?_; quotient; ∣1⇒≡1; divides; quotient-<; m|n⇒n≡m*quotient; hasNonTrivialDivisor; quotient-∣; quotient>1) open import Data.Nat.Properties open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder) -open import Data.Nat.Primality using (Prime; prime; euclidsLemma; prime⇒irreducible; prime⇒nonZero; _Rough_; 2-rough; ∤⇒rough-suc; rough∧∣⇒prime; ¬prime[1]; rough∧∣⇒rough; rough∧square>⇒prime) +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 (_∈_) From cf8a9c4996b7ed95e99abc5dd20c27fe7642b249 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 31 Jan 2024 10:13:59 +0100 Subject: [PATCH 35/38] Clean up proof --- src/Data/Nat/Primality/Factorisation.agda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 8cfb65b202..d1e82aa115 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -128,16 +128,16 @@ factorisationHasAllPrimeFactors {a ∷ as} {p} pPrime p∣aΠas (aPrime ∷ asPr 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) = +factorisationUnique′ [] (b@(2+ _) ∷ bs) Πas≡Πbs asPrime (bPrime ∷ bsPrime) = contradiction Πas≡Πbs (<⇒≢ Πas<Πbs) where - Πas<Πbs : product [] < product (2+ b ∷ bs) + Πas<Πbs : product [] < product (b ∷ bs) Πas<Πbs = begin-strict - 1 ≡⟨⟩ - 1 * 1 <⟨ *-monoˡ-< 1 {1} {2 + b} sz Date: Thu, 1 Feb 2024 09:13:11 +0100 Subject: [PATCH 36/38] Fixes after merge --- src/Data/Nat/Primality.agda | 2 +- src/Data/Nat/Primality/Factorisation.agda | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 6a4fd99eb1..ab1bbb4995 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -299,7 +299,7 @@ rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prim rough∧square>⇒prime rough m*m>n = prime ¬composite where ¬composite : ¬ Composite _ - ¬composite (hasNonTrivialDivisor dn (*-mono-≤ (rough⇒≤ (rough∧∣⇒rough rough (quotient-∣ d∣n))) (rough⇒≤ (rough∧∣⇒rough rough d∣n))))) diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index d1e82aa115..2f1b50b7e0 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -10,7 +10,7 @@ module Data.Nat.Primality.Factorisation where open import Data.Empty using (⊥-elim) open import Data.Nat.Base -open import Data.Nat.Divisibility using (_∣_; _∣?_; quotient; ∣1⇒≡1; divides; quotient-<; m|n⇒n≡m*quotient; hasNonTrivialDivisor; quotient-∣; quotient>1) +open import Data.Nat.Divisibility using (_∣_; _∣?_; quotient; ∣1⇒≡1; divides; quotient-<; m∣n⇒n≡m*quotient; hasNonTrivialDivisor; quotient-∣; quotient>1) open import Data.Nat.Properties open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder) open import Data.Nat.Primality @@ -107,7 +107,7 @@ factorise n₀@(2+ _) = build [ <-recBuilder ⊗ <-recBuilder ] P facRec (n₀ , m*Πps≡n : m * product ps ≡ n m*Πps≡n = begin m * product ps ≡⟨ cong (m *_) Πps≡q ⟩ - m * q ≡˘⟨ m|n⇒n≡m*quotient m∣n ⟩ + m * q ≡˘⟨ m∣n⇒n≡m*quotient m∣n ⟩ n ∎ where open ≡-Reasoning From a556522d63b93a18a3cc2faa02c9cd9cf846dec0 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Sun, 3 Mar 2024 13:06:28 +0800 Subject: [PATCH 37/38] Addressed some feedback --- CHANGELOG.md | 14 ++ src/Data/Nat/Primality.agda | 14 +- src/Data/Nat/Primality/Factorisation.agda | 154 ++++++++++++---------- 3 files changed, 110 insertions(+), 72 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e8f0a568f2..863e80c06f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -43,6 +43,8 @@ New modules * `Algebra.Module.Bundles.Raw`: raw bundles for module-like algebraic structures +* `Data.Nat.Primality.Factorisation`: prime factorisation of natural numbers. + Additions to existing modules ----------------------------- @@ -132,6 +134,18 @@ Additions to existing modules pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n ``` + +* Added new proofs to `Data.Nat.Primality`: + ```agda + rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n + productOfPrimes≢0 : All Prime as → NonZero (product as) + productOfPrimes≥1 : All Prime as → product as ≥ 1 + ``` + +* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`: + ```agda + product-↭ : product Preserves _↭_ ⟶ _≡_ + ``` * Added new functions in `Data.String.Base`: ```agda diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index ab1bbb4995..1a491fdf93 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -8,6 +8,8 @@ module Data.Nat.Primality where +open import Data.List.Base using ([]; _∷_; product) +open import Data.List.Relation.Unary.All as All using (All; []; _∷_) open import Data.Nat.Base open import Data.Nat.Divisibility open import Data.Nat.GCD using (module GCD; module Bézout) @@ -299,7 +301,7 @@ rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prim rough∧square>⇒prime rough m*m>n = prime ¬composite where ¬composite : ¬ Composite _ - ¬composite (hasNonTrivialDivisor dn (*-mono-≤ (rough⇒≤ (rough∧∣⇒rough rough (quotient-∣ d∣n))) (rough⇒≤ (rough∧∣⇒rough rough d∣n))))) @@ -320,6 +322,16 @@ prime⇒¬composite (prime p) = p ¬prime⇒composite {n} ¬prime[n] = decidable-stable (composite? n) (¬prime[n] ∘′ ¬composite⇒prime) +productOfPrimes≢0 : ∀ {as} → All Prime as → NonZero (product as) +productOfPrimes≢0 pas = product≢0 (All.map prime⇒nonZero pas) + where + product≢0 : ∀ {ns} → All NonZero ns → NonZero (product ns) + product≢0 [] = _ + product≢0 {n ∷ ns} (nzn ∷ nzns) = m*n≢0 n _ {{nzn}} {{product≢0 nzns}} + +productOfPrimes≥1 : ∀ {as} → All Prime as → product as ≥ 1 +productOfPrimes≥1 {as} pas = >-nonZero⁻¹ _ {{productOfPrimes≢0 pas}} + ------------------------------------------------------------------------ -- Basic (counter-)examples of Irreducible diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda index 2f1b50b7e0..fed89d7d45 100644 --- a/src/Data/Nat/Primality/Factorisation.agda +++ b/src/Data/Nat/Primality/Factorisation.agda @@ -10,7 +10,7 @@ module Data.Nat.Primality.Factorisation where open import Data.Empty using (⊥-elim) open import Data.Nat.Base -open import Data.Nat.Divisibility using (_∣_; _∣?_; quotient; ∣1⇒≡1; divides; quotient-<; m∣n⇒n≡m*quotient; hasNonTrivialDivisor; quotient-∣; quotient>1) +open import Data.Nat.Divisibility open import Data.Nat.Properties open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder) open import Data.Nat.Primality @@ -20,8 +20,8 @@ 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 as ↭ - using (_↭_; prep; swap; ↭-refl; refl; module PermutationReasoning) +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) @@ -31,13 +31,17 @@ 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 : product factors ≡ n + isFactorisation : n ≡ product factors factorsPrime : All Prime factors open PrimeFactorisation public using (factors) @@ -46,7 +50,21 @@ open PrimeFactorisation ------------------------------------------------------------------------ -- Finding a factorisation --- this builds up three important things: +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) @@ -55,39 +73,31 @@ open PrimeFactorisation -- * 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 = record - { factors = [] - ; isFactorisation = refl - ; factorsPrime = [] - } +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 - facRec (n , zero) _ rough eq = record - { factors = n ∷ [] - ; isFactorisation = *-identityʳ n - ; factorsPrime = rough∧square>⇒prime rough (m∸n≡0⇒m≤n eq) ∷ [] - } + 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 ∸_) (+-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)) ≡⟨ ∸-+-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 = m*Πps≡n + ; isFactorisation = sym m*Πps≡n ; factorsPrime = rough∧∣⇒prime rough m∣n ∷ primes } where @@ -97,27 +107,28 @@ factorise n₀@(2+ _) = build [ <-recBuilder ⊗ <-recBuilder ] P facRec (n₀ , pred (m * m) <⟨ s1⇒nonTrivial (quotient>1 m∣n m Date: Sat, 16 Mar 2024 10:33:45 +0800 Subject: [PATCH 38/38] Fix previous merge --- CHANGELOG.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 02b205716f..df954bc614 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -49,6 +49,11 @@ Deprecated names New modules ----------- +* Raw bundles for module-like algebraic structures: + ``` + Algebra.Module.Bundles.Raw + ``` + * Prime factorisation of natural numbers. ``` Data.Nat.Primality.Factorisation