From 1cf7c7f03e8e9f93e39bf702d57feb6a353df920 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 23 Oct 2023 13:35:31 +0100 Subject: [PATCH 01/78] definition of `Irreducible`; refactoring of `Prime` and `Composite` --- src/Data/Nat/Primality.agda | 139 ++++++++++++++++++++++++++---------- 1 file changed, 100 insertions(+), 39 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 361df42b73..ff35509d42 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -8,80 +8,140 @@ module Data.Nat.Primality where -open import Data.Empty using (⊥) open import Data.Nat.Base open import Data.Nat.Divisibility open import Data.Nat.GCD using (module GCD; module Bézout) open import Data.Nat.Properties -open import Data.Product.Base using (∃; _×_; map₂; _,_) -open import Data.Sum.Base using (_⊎_; inj₁; inj₂) +open import Data.Product.Base using (_×_; map₂; _,_) +open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (flip; _∘_; _∘′_) 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.Unary using (Pred; Decidable; IUniversal; Satisfiable) open import Relation.Binary.PropositionalEquality - using (refl; cong) + using (_≡_; refl; cong) private variable - n : ℕ + n p : ℕ + ------------------------------------------------------------------------ -- Definitions -- Definition of compositeness +CompositeAt : ℕ → Pred ℕ _ +CompositeAt n d = 1 < d × d < n × d ∣ n + Composite : ℕ → Set -Composite 0 = ⊥ -Composite 1 = ⊥ -Composite n = ∃ λ d → 2 ≤ d × d < n × d ∣ n +Composite n = ∃⟨ CompositeAt n ⟩ + +¬Composite[0] : ¬ Composite 0 +¬Composite[0] (_ , _ , () , _) + +¬Composite[1] : ¬ Composite 1 +¬Composite[1] (_ , s⇒≢ 1 Date: Mon, 23 Oct 2023 13:43:17 +0100 Subject: [PATCH 02/78] tidying up old cruft --- src/Data/Nat/Primality.agda | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index ff35509d42..b24aff2567 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -159,7 +159,7 @@ euclidsLemma m n {p} (prime p-prime) p∣m*n = result p∣rmn r = begin p ∣⟨ p∣m*n ⟩ m * n ∣⟨ n∣m*n r ⟩ - r * (m * n) ≡˘⟨ *-assoc r m n ⟩ + r * (m * n) ≡⟨ *-assoc r m n ⟨ r * m * n ∎ result : p ∣ m ⊎ p ∣ n @@ -174,14 +174,14 @@ euclidsLemma m n {p} (prime p-prime) p∣m*n = result ... | Bézout.result 1 _ (Bézout.+- r s 1+sp≡rm) = inj₂ (flip ∣m+n∣m⇒∣n (n∣m*n*o s n) (begin p ∣⟨ p∣rmn r ⟩ - r * m * n ≡˘⟨ cong (_* n) 1+sp≡rm ⟩ + r * m * n ≡⟨ cong (_* n) 1+sp≡rm ⟨ n + s * p * n ≡⟨ +-comm n (s * p * n) ⟩ s * p * n + n ∎)) ... | Bézout.result 1 _ (Bézout.-+ r s 1+rm≡sp) = inj₂ (flip ∣m+n∣m⇒∣n (p∣rmn r) (begin p ∣⟨ n∣m*n*o s n ⟩ - s * p * n ≡˘⟨ cong (_* n) 1+rm≡sp ⟩ + s * p * n ≡⟨ cong (_* n) 1+rm≡sp ⟨ n + r * m * n ≡⟨ +-comm n (r * m * n) ⟩ r * m * n + n ∎)) @@ -201,4 +201,3 @@ private -- Example: 6 is composite 6-is-composite : Composite 6 6-is-composite = from-yes (composite? 6) - From 5d31e32e168de04af0a44411f7e35cc6ab16942e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 23 Oct 2023 14:13:05 +0100 Subject: [PATCH 03/78] knock-on consequences: `Coprimality` --- src/Data/Nat/Coprimality.agda | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index 1df320ea96..ae8a175b2a 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -141,9 +141,7 @@ coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout prime⇒coprime : ∀ m → Prime m → ∀ n → 0 < n → n < m → Coprime m n -prime⇒coprime (suc (suc _)) p _ _ _ {0} (0∣m , _) = - contradiction (0∣⇒≡0 0∣m) λ() -prime⇒coprime (suc (suc _)) _ _ _ _ {1} _ = refl -prime⇒coprime (suc (suc _)) p (suc _) _ n Date: Tue, 24 Oct 2023 00:55:56 +0100 Subject: [PATCH 04/78] considerable refactoring of `Primality` --- src/Data/Nat/Primality.agda | 153 ++++++++++++++++++++++++++---------- 1 file changed, 110 insertions(+), 43 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index b24aff2567..39841f4523 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -11,8 +11,9 @@ module Data.Nat.Primality where open import Data.Nat.Base open import Data.Nat.Divisibility open import Data.Nat.GCD using (module GCD; module Bézout) +open import Data.Nat.Induction using (<-rec; <-Rec) open import Data.Nat.Properties -open import Data.Product.Base using (_×_; map₂; _,_) +open import Data.Product.Base using (_×_; map₂; _,_; proj₂) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (flip; _∘_; _∘′_) open import Relation.Nullary.Decidable as Dec @@ -24,30 +25,44 @@ open import Relation.Binary.PropositionalEquality private variable - n p : ℕ + k m n p : ℕ ------------------------------------------------------------------------ -- Definitions +-- Definition of 'not rough'-ness + +record SmoothAt (k n d : ℕ) : Set where + constructor mkSmoothAt + field + 1 1 are greater than or equal to k -¬Composite[1] : ¬ Composite 1 -¬Composite[1] (_ , s 1 are greater than or equal to 2 +2-rough : 2 Rough n +2-rough (mkSmoothAt 1 1 divides it, then k must be prime +rough⇒∣⇒prime : 1 < k → k Rough n → k ∣ n → Prime k +rough⇒∣⇒prime 1⇒≢ 1⇒≢ 1 Date: Tue, 24 Oct 2023 01:04:01 +0100 Subject: [PATCH 05/78] knock-on consequences: `Coprimality` --- src/Data/Nat/Coprimality.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index ae8a175b2a..5d6fc0b02d 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -143,5 +143,5 @@ prime⇒coprime : ∀ m → Prime m → ∀ n → 0 < n → n < m → Coprime m n prime⇒coprime _ (prime p) _ _ _ {0} (0∣m , _) = contradiction (0∣⇒≡0 0∣m) λ() prime⇒coprime _ _ _ _ _ {1} _ = refl -prime⇒coprime _ (prime p) (suc _) _ n Date: Tue, 24 Oct 2023 01:11:13 +0100 Subject: [PATCH 06/78] refactoring: no appeal to `Data.Nat.Induction` --- src/Data/Nat/Primality.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 39841f4523..7920598493 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -11,7 +11,6 @@ module Data.Nat.Primality where open import Data.Nat.Base open import Data.Nat.Divisibility open import Data.Nat.GCD using (module GCD; module Bézout) -open import Data.Nat.Induction using (<-rec; <-Rec) open import Data.Nat.Properties open import Data.Product.Base using (_×_; map₂; _,_; proj₂) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) From c5074a815e18d801cb8958f65670cabb11562daf Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 24 Oct 2023 08:55:49 +0100 Subject: [PATCH 07/78] refactoring: renamed `SmoothAt` and its constructor; added pattern synonym; proved `Decidable Irreducible`; misc. tweaks --- src/Data/Nat/Primality.agda | 79 ++++++++++++++++++++++--------------- 1 file changed, 48 insertions(+), 31 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 7920598493..4d61ce8e81 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -16,7 +16,7 @@ open import Data.Product.Base using (_×_; map₂; _,_; proj₂) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (flip; _∘_; _∘′_) open import Relation.Nullary.Decidable as Dec - using (yes; no; from-yes; ¬?; decidable-stable; _×-dec_; _→-dec_) + using (yes; no; from-yes; ¬?; decidable-stable; _×-dec_; _⊎-dec_; _→-dec_) open import Relation.Nullary.Negation using (¬_; contradiction) open import Relation.Unary using (Pred; Decidable; IUniversal; Satisfiable) open import Relation.Binary.PropositionalEquality @@ -26,25 +26,29 @@ private variable k m n p : ℕ +pattern 1<2+n {n} = s1 {d} d 1 are greater than or equal to k _RoughAt_ : ℕ → ℕ → Pred ℕ _ -k RoughAt n = ¬_ ∘ SmoothAt k n +k RoughAt n = ¬_ ∘ BoundedCompositeAt k n _Rough_ : ℕ → ℕ → Set k Rough n = ∀[ k RoughAt n ] @@ -66,11 +70,9 @@ PrimeAt n = n RoughAt n Prime : ℕ → Set Prime n = 1 < n × ∀[ PrimeAt n ] -pattern 1<2+n {n} = s⇒∤ 1 1 are greater than or equal to 2 2-rough : 2 Rough n -2-rough (mkSmoothAt 11 (s1 m

⇒≢ 1⇒≢ 11 d

Date: Tue, 24 Oct 2023 08:56:01 +0100 Subject: [PATCH 08/78] knock-on consequences: `Coprimality` --- src/Data/Nat/Coprimality.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index 5d6fc0b02d..3e1db8b066 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -141,7 +141,7 @@ coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout prime⇒coprime : ∀ m → Prime m → ∀ n → 0 < n → n < m → Coprime m n -prime⇒coprime _ (prime p) _ _ _ {0} (0∣m , _) = contradiction (0∣⇒≡0 0∣m) λ() -prime⇒coprime _ _ _ _ _ {1} _ = refl -prime⇒coprime _ (prime p) _ z Date: Tue, 24 Oct 2023 09:39:06 +0100 Subject: [PATCH 09/78] refactoring: removed `NonZero` analysis; misc. tweaks --- src/Data/Nat/Primality.agda | 17 +++-------------- 1 file changed, 3 insertions(+), 14 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 4d61ce8e81..6a09dc4689 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -86,7 +86,7 @@ Irreducible n = ∀[ IrreducibleAt n ] -- 1 is always rough _rough-1 : ∀ k → k Rough 1 -(_ rough-1) (boundedComposite 1⇒∤ 1⇒∤ 1 1 are greater than or equal to 2 2-rough : 2 Rough n @@ -151,15 +151,6 @@ irreducible[2] {suc _} d∣2 with ∣⇒≤ d∣2 ... | z1 m

Date: Tue, 24 Oct 2023 09:39:46 +0100 Subject: [PATCH 10/78] knock-on consequences: `Coprimality`; tightened `import`s --- src/Data/Nat/Coprimality.agda | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index 3e1db8b066..42c7e9150d 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -8,7 +8,6 @@ module Data.Nat.Coprimality where -open import Data.Empty open import Data.Nat.Base open import Data.Nat.Divisibility open import Data.Nat.GCD From dce2edc5c9226ccec05958e8c007cef9307aa25d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 24 Oct 2023 09:43:18 +0100 Subject: [PATCH 11/78] knock-on consequences: `Coprimality`; tightened `import`s --- src/Data/Nat/Coprimality.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index 42c7e9150d..0e311df8e9 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -20,8 +20,7 @@ open import Function.Base using (_∘_) open import Level using (0ℓ) open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_; refl; trans; cong; subst) -open import Relation.Nullary as Nullary hiding (recompute) -open import Relation.Nullary.Negation using (contradiction) +open import Relation.Nullary as Nullary using (¬_; contradiction; yes ; no) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Symmetric; Decidable) From 44c2c19eb6ef6d91e4930e78c7d4fe0bd2af8f66 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 24 Oct 2023 15:12:27 +0100 Subject: [PATCH 12/78] refactoring: every number is `1-rough` --- src/Data/Nat/Primality.agda | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 6a09dc4689..7eee7e72ed 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -88,6 +88,10 @@ Irreducible n = ∀[ IrreducibleAt n ] _rough-1 : ∀ k → k Rough 1 (_ rough-1) (boundedComposite 1⇒∤ 1 1 are greater than or equal to 2 2-rough : 2 Rough n 2-rough (boundedComposite 1 Date: Wed, 25 Oct 2023 04:48:14 +0100 Subject: [PATCH 13/78] knock-on consequences: `Coprimality`; use of smart constructor --- src/Data/Nat/Coprimality.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index 0e311df8e9..1a594c9826 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -142,4 +142,4 @@ prime⇒coprime : ∀ m → Prime m → prime⇒coprime _ (prime p) _ _ _ {0} (0∣m , _) = contradiction (0∣⇒≡0 0∣m) λ() prime⇒coprime _ _ _ _ _ {1} _ = refl prime⇒coprime _ (prime p) _ z1 (<-≤-trans (s≤s (∣⇒≤ d∣n)) n Date: Wed, 25 Oct 2023 05:22:25 +0100 Subject: [PATCH 14/78] refactoring: every number is `0-rough`; streamlining; inverse to `prime`; documentation --- src/Data/Nat/Primality.agda | 27 +++++++++++++++++++-------- 1 file changed, 19 insertions(+), 8 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 7eee7e72ed..c7604846b3 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -70,12 +70,21 @@ PrimeAt n = n RoughAt n Prime : ℕ → Set Prime n = 1 < n × ∀[ PrimeAt n ] +-- smart constructor: prime +-- this takes a proof p that n = suc (suc _) is n-Rough +-- and thereby enforces that n is a fortiori NonZero + pattern prime {n} p = 1<2+n {n} , p +-- smart destructor + +prime⁻¹ : Prime n → n Rough n +prime⁻¹ (prime p) = p + -- Definition of irreducibility IrreducibleAt : ℕ → Pred ℕ _ -IrreducibleAt n m = m ∣ n → m ≡ 1 ⊎ m ≡ n +IrreducibleAt n d = d ∣ n → d ≡ 1 ⊎ d ≡ n Irreducible : ℕ → Set Irreducible n = ∀[ IrreducibleAt n ] @@ -88,6 +97,10 @@ Irreducible n = ∀[ IrreducibleAt n ] _rough-1 : ∀ k → k Rough 1 (_ rough-1) (boundedComposite 1⇒∤ 1 1 divides it, then k must be prime +-- If a number n is k-rough, and k > 1 divides n, then k must be prime rough⇒∣⇒prime : 1 < k → k Rough n → k ∣ n → Prime k rough⇒∣⇒prime 11 (s1 (s Date: Wed, 25 Oct 2023 18:49:08 +0100 Subject: [PATCH 15/78] attempt to optimise for a nearly-common case pseudo-constructor --- src/Data/Nat/Primality.agda | 46 +++++++++++++++++++------------------ 1 file changed, 24 insertions(+), 22 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index c7604846b3..7959e85fa7 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -16,15 +16,15 @@ open import Data.Product.Base using (_×_; map₂; _,_; proj₂) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (flip; _∘_; _∘′_) open import Relation.Nullary.Decidable as Dec - using (yes; no; from-yes; ¬?; decidable-stable; _×-dec_; _⊎-dec_; _→-dec_) + using (yes; no; from-yes; from-no; ¬?; decidable-stable; _×-dec_; _⊎-dec_; _→-dec_) open import Relation.Nullary.Negation using (¬_; contradiction) open import Relation.Unary using (Pred; Decidable; IUniversal; Satisfiable) open import Relation.Binary.PropositionalEquality - using (_≡_; refl; cong) + using (_≡_; _≢_; refl; cong) private variable - k m n p : ℕ + d k m n p : ℕ pattern 1<2+n {n} = s 1 divides n, then k must be prime -rough⇒∣⇒prime : 1 < k → k Rough n → k ∣ n → Prime k -rough⇒∣⇒prime 1 1 divides n, then p must be prime +rough⇒∣⇒prime : 1 < p → p Rough n → p ∣ n → Prime p +rough⇒∣⇒prime 1

1 (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n + composite[4] : Composite 4 -composite[4] = 2 , boundedComposite>1 (s1 m

1 m

1 d

Date: Wed, 25 Oct 2023 19:01:48 +0100 Subject: [PATCH 16/78] fiddling now --- 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 7959e85fa7..876a7068c0 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -136,8 +136,8 @@ rough⇒∣⇒prime 1

1 (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n composite[4] : Composite 4 From c7988894e11d39e24f32b4c2aa359b95d66612c2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 26 Oct 2023 10:44:19 +0100 Subject: [PATCH 17/78] refactoring: better use of `primality` API --- CHANGELOG.md | 5 +++++ src/Data/Nat/Coprimality.agda | 14 ++++++++++---- src/Data/Nat/Primality.agda | 12 ++++++------ 3 files changed, 21 insertions(+), 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9d9f403d64..7767295d3e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2753,6 +2753,11 @@ Additions to existing modules <-asym : Asymmetric _<_ ``` +* Added a new definition to `Data.Nat.Coprimality`: + ```agda + prime⇒coprime≢0 : Prime p → .{{_ : NonZero n}} → n < p → Coprime p n + ``` + * Added a new pattern synonym to `Data.Nat.Divisibility.Core`: ```agda pattern divides-refl q = divides q refl diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index 1a594c9826..837e801959 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -16,6 +16,7 @@ open import Data.Nat.Primality open import Data.Nat.Properties open import Data.Nat.DivMod open import Data.Product.Base as Prod +open import Data.Sum.Base as Sum using (inj₁; inj₂) open import Function.Base using (_∘_) open import Level using (0ℓ) open import Relation.Binary.PropositionalEquality.Core as P @@ -137,9 +138,14 @@ coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout ------------------------------------------------------------------------ -- Primality implies coprimality. +prime⇒coprime≢0 : ∀ {p} → Prime p → + ∀ {n} .{{_ : NonZero n}} → n < p → Coprime p n +prime⇒coprime≢0 {p} pr@(prime _) n

1 (<-≤-trans (s≤s (∣⇒≤ d∣n)) n1 (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n composite[4] : Composite 4 @@ -196,9 +196,8 @@ irreducible? n@(suc _) = Dec.map′ bounded-irr⇒irr irr⇒bounded-irr BoundedIrreducible : Pred ℕ _ BoundedIrreducible n = ∀ {m} → m < n → m ∣ n → m ≡ 1 ⊎ m ≡ n bounded-irr⇒irr : BoundedIrreducible n → Irreducible n - bounded-irr⇒irr bounded-irr m∣n with m≤n⇒m Date: Fri, 27 Oct 2023 07:39:50 +0100 Subject: [PATCH 18/78] `Rough` is bounded --- src/Data/Nat/Primality.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index af7fa2d2f0..b2d8a0034e 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -120,6 +120,9 @@ rough⇒∣⇒rough : k Rough m → n ∣ m → k Rough n rough⇒∣⇒rough r n∣m (boundedComposite 1n → rough (boundedComposite 1n ∣-refl) + ------------------------------------------------------------------------ -- Corollary: relationship between roughness and primality @@ -141,7 +144,7 @@ composite[2+k≢n≢0] : .{{NonZero n}} → let d = suc (suc k) in composite[2+k≢n≢0] d≢n d∣n = boundedComposite>1 (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n composite[4] : Composite 4 -composite[4] = 2 , composite[2+k≢n≢0] (from-no (2 ≟ 4)) (divides-refl 2) +composite[4] = 2 , composite[2+k≢n≢0] (λ()) (divides-refl 2) ------------------------------------------------------------------------ -- Basic (non-)instances of Prime From 00086b76f4cfbb480fd54652cb30e059ce9423cf Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Oct 2023 08:42:01 +0100 Subject: [PATCH 19/78] removed unnecessary implicits --- src/Data/Nat/Coprimality.agda | 3 +-- src/Data/Nat/Primality.agda | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index 837e801959..f7d31d517f 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -140,8 +140,7 @@ coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout prime⇒coprime≢0 : ∀ {p} → Prime p → ∀ {n} .{{_ : NonZero n}} → n < p → Coprime p n -prime⇒coprime≢0 {p} pr@(prime _) n

n → rough (boundedComposite 1n ∣-refl) +rough⇒≤ 1n → rough (boundedComposite 1n ∣-refl) ------------------------------------------------------------------------ -- Corollary: relationship between roughness and primality From 232b6d6a3cd8fce09a654482d9cf7b3c04dd94a9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Oct 2023 08:43:57 +0100 Subject: [PATCH 20/78] comment --- src/Data/Nat/Primality.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index ba4930c0aa..0a77cd561a 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -120,6 +120,7 @@ rough⇒∣⇒rough : k Rough m → n ∣ m → k Rough n rough⇒∣⇒rough r n∣m (boundedComposite 1 1 is k-rough, then k ≤ n rough⇒≤ : 1 < n → k Rough n → k ≤ n rough⇒≤ 1n → rough (boundedComposite 1n ∣-refl) From 0a6954d12d94747e6ae7816f86fe598393954d93 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 28 Oct 2023 15:57:21 +0100 Subject: [PATCH 21/78] refactoring: comprehensive shift over to `NonTrivial` instances --- src/Data/Nat/Primality.agda | 200 +++++++++++++++++++++--------------- 1 file changed, 120 insertions(+), 80 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 0a77cd561a..5db798ff50 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -6,8 +6,9 @@ {-# OPTIONS --cubical-compatible --safe #-} -module Data.Nat.Primality where +module Data.Nat.PrimalityINSTANCE where +open import Data.Bool.Base using (Bool; true; false; not; T) open import Data.Nat.Base open import Data.Nat.Divisibility open import Data.Nat.GCD using (module GCD; module Bézout) @@ -26,60 +27,94 @@ private variable d k m n p : ℕ +------------------------------------------------------------------------ +-- Definitions for `Data.Nat.Base` + +pattern 2+ n = suc (suc n) + +trivial : ℕ → Bool +trivial 0 = true +trivial 1 = true +trivial (2+ _) = false + +Unit NonUnit NonTrivial : Pred ℕ _ +Unit = T ∘ (_≡ᵇ 1) +NonUnit = T ∘ not ∘ (_≡ᵇ 1) +NonTrivial = T ∘ not ∘ trivial + +instance + nonUnit[0] : NonUnit 0 + nonUnit[0] = _ + + nonTrivial⇒nonUnit : .{{NonTrivial n}} → NonUnit n + nonTrivial⇒nonUnit {n = 2+ _} = _ + +nonUnit⇒≢1 : .{{NonUnit n}} → n ≢ 1 +nonUnit⇒≢1 ⦃()⦄ refl +instance + nonTrivial : NonTrivial (2+ n) + nonTrivial = _ + +nonTrivial⇒≢1 : .{{NonTrivial n}} → n ≢ 1 +nonTrivial⇒≢1 ⦃()⦄ refl + +nonTrivial⇒nonZero : .{{NonTrivial n}} → NonZero n +nonTrivial⇒nonZero {n = 2+ k} = _ + pattern 1<2+n {n} = s1 : .{{NonTrivial n}} → 1 < n +nonTrivial⇒n>1 {n = 2+ _} = 1<2+n + +n>1⇒nonTrivial : 1 < n → NonTrivial n +n>1⇒nonTrivial 1<2+n = _ + ------------------------------------------------------------------------ -- Definitions -- Definition of 'not rough'-ness -record BoundedCompositeAt (k n d : ℕ) : Set where +record _BoundedComposite_ (k n d : ℕ) : Set where constructor boundedComposite field - 11 {d} d 1 are greater than or equal to k +composite : .{{NonZero n}} → {{NonTrivial d}} → + d ≢ n → d ∣ n → Composite n +composite {d = d} d≢n d∣n = d , boundedComposite≢ d≢n d∣n -_RoughAt_ : ℕ → ℕ → Pred ℕ _ -k RoughAt n = ¬_ ∘ BoundedCompositeAt k n +-- Definition of 'rough': a number is k-rough +-- if all its non-trivial factors d 1 are greater than or equal to k -_Rough_ : ℕ → ℕ → Set -k Rough n = ∀[ k RoughAt n ] +_Rough_ : ℕ → Pred ℕ _ +k Rough n = ∀[ ¬_ ∘ k BoundedComposite n ] -- Definition of primality: complement of Composite +-- Constructor: prime +-- takes a proof isPrime that NonTrivial p is p-Rough +-- and thereby enforces that p is a fortiori NonZero -PrimeAt : ℕ → Pred ℕ _ -PrimeAt n = n RoughAt n - -Prime : ℕ → Set -Prime n = 1 < n × ∀[ PrimeAt n ] - --- smart constructor: prime --- this takes a proof p that n = suc (suc _) is n-Rough --- and thereby enforces that n is a fortiori NonZero - -pattern prime {n} r = 1<2+n {n} , r - --- smart destructor - -prime⁻¹ : Prime n → n Rough n -prime⁻¹ (prime r) = r +record Prime (p : ℕ) : Set where + constructor prime + field + {{nt}} : NonTrivial p + isPrime : p Rough p -- Definition of irreducibility @@ -95,41 +130,37 @@ Irreducible n = ∀[ IrreducibleAt n ] -- 1 is always rough _rough-1 : ∀ k → k Rough 1 -(_ rough-1) (boundedComposite 1⇒∤ 1 1 are greater than or equal to 2 2-rough : 2 Rough n -2-rough (boundedComposite 1 1 is k-rough, then k ≤ n -rough⇒≤ : 1 < n → k Rough n → k ≤ n -rough⇒≤ 1n → rough (boundedComposite 1n ∣-refl) +rough⇒∣⇒rough r n∣m (boundedComposite d 1 divides n, then p must be prime -rough⇒∣⇒prime : 1 < p → p Rough n → p ∣ n → Prime p -rough⇒∣⇒prime 1

1 (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n - composite[4] : Composite 4 -composite[4] = 2 , composite[2+k≢n≢0] (λ()) (divides-refl 2) +composite[4] = composite {d = 2} (λ ()) (divides 2 refl) ------------------------------------------------------------------------ -- Basic (non-)instances of Prime ¬prime[0] : ¬ Prime 0 -¬prime[0] (() , _) +¬prime[0] () ¬prime[1] : ¬ Prime 1 -¬prime[1] (s1⇒nonTrivial 11 , d∣n) (anyUpTo? (λ d → 1 1 d∣n) + (λ (prime p) {d} d1⇒nonTrivial 11 m

⇒≢ 1 Date: Sat, 28 Oct 2023 16:11:14 +0100 Subject: [PATCH 22/78] refactoring: oops! --- src/Data/Nat/Primality.agda | 28 ++++++++++++---------------- 1 file changed, 12 insertions(+), 16 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 5db798ff50..8dbc1c1bdb 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -6,7 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} -module Data.Nat.PrimalityINSTANCE where +module Data.Nat.Primality where open import Data.Bool.Base using (Bool; true; false; not; T) open import Data.Nat.Base @@ -73,9 +73,9 @@ n>1⇒nonTrivial 1<2+n = _ ------------------------------------------------------------------------ -- Definitions --- Definition of 'not rough'-ness +-- Definition of having a non-trivil divispr below a given bound -record _BoundedComposite_ (k n d : ℕ) : Set where +record BoundedComposite (k n d : ℕ) : Set where constructor boundedComposite field {{nt}} : NonTrivial d @@ -85,13 +85,13 @@ record _BoundedComposite_ (k n d : ℕ) : Set where -- smart constructor boundedComposite≢ : .{{NonZero n}} → {{NonTrivial d}} → - d ≢ n → d ∣ n → (n BoundedComposite n) d + d ≢ n → d ∣ n → BoundedComposite n n d boundedComposite≢ d≢n d∣n = boundedComposite (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n -- Definition of compositeness Composite : Pred ℕ _ -Composite n = ∃⟨ n BoundedComposite n ⟩ +Composite n = ∃⟨ BoundedComposite n n ⟩ -- smart constructor @@ -103,12 +103,12 @@ composite {d = d} d≢n d∣n = d , boundedComposite≢ d≢n d∣n -- if all its non-trivial factors d 1 are greater than or equal to k _Rough_ : ℕ → Pred ℕ _ -k Rough n = ∀[ ¬_ ∘ k BoundedComposite n ] +k Rough n = ∀[ ¬_ ∘ BoundedComposite k n ] -- Definition of primality: complement of Composite --- Constructor: prime --- takes a proof isPrime that NonTrivial p is p-Rough --- and thereby enforces that p is a fortiori NonZero +-- Constructor `prime` takes a proof isPrime that +-- NonTrivial p is p-Rough, and thereby enforces that +-- p is a fortiori NonZero and NonUnit record Prime (p : ℕ) : Set where constructor prime @@ -118,11 +118,8 @@ record Prime (p : ℕ) : Set where -- Definition of irreducibility -IrreducibleAt : ℕ → Pred ℕ _ -IrreducibleAt n d = d ∣ n → d ≡ 1 ⊎ d ≡ n - Irreducible : ℕ → Set -Irreducible n = ∀[ IrreducibleAt n ] +Irreducible n = ∀[ (λ d → d ∣ n → d ≡ 1 ⊎ d ≡ n) ] ------------------------------------------------------------------------ @@ -132,15 +129,14 @@ Irreducible n = ∀[ IrreducibleAt n ] _rough-1 : ∀ k → k Rough 1 (_ rough-1) {2+ _} (boundedComposite _ d∣1@(divides q@(suc _) ())) --- Any number is 0-rough +-- Any number is 0-, 1- and 2-rough, +-- because no non-trivial factor d can be less than 0 , 1, 2 0-rough : 0 Rough n 0-rough (boundedComposite () _) --- Any number is 1-rough 1-rough : 1 Rough n 1-rough (boundedComposite ⦃()⦄ z 1 are greater than or equal to 2 2-rough : 2 Rough n 2-rough (boundedComposite ⦃()⦄ (s Date: Sat, 28 Oct 2023 16:24:18 +0100 Subject: [PATCH 23/78] tidying up: removed infixes --- src/Data/Nat/Coprimality.agda | 4 ++-- src/Data/Nat/Primality.agda | 37 +++++++++++++++++++---------------- 2 files changed, 22 insertions(+), 19 deletions(-) diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index f7d31d517f..68fd054b85 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -141,8 +141,8 @@ coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout prime⇒coprime≢0 : ∀ {p} → Prime p → ∀ {n} .{{_ : NonZero n}} → n < p → Coprime p n prime⇒coprime≢0 p n

1 : .{{NonTrivial n}} → 1 < n -nonTrivial⇒n>1 {n = 2+ _} = 1<2+n +nonTrivial⇒n>1 {n = 2+ _} = 1<2+n n>1⇒nonTrivial : 1 < n → NonTrivial n n>1⇒nonTrivial 1<2+n = _ @@ -73,7 +73,7 @@ n>1⇒nonTrivial 1<2+n = _ ------------------------------------------------------------------------ -- Definitions --- Definition of having a non-trivil divispr below a given bound +-- Definition of having a non-trivial divisor below a given bound record BoundedComposite (k n d : ℕ) : Set where constructor boundedComposite @@ -102,11 +102,11 @@ composite {d = d} d≢n d∣n = d , boundedComposite≢ d≢n d∣n -- Definition of 'rough': a number is k-rough -- if all its non-trivial factors d 1 are greater than or equal to k -_Rough_ : ℕ → Pred ℕ _ -k Rough n = ∀[ ¬_ ∘ BoundedComposite k n ] +Rough : ℕ → Pred ℕ _ +Rough k n = ∀[ ¬_ ∘ BoundedComposite k n ] -- Definition of primality: complement of Composite --- Constructor `prime` takes a proof isPrime that +-- Constructor `prime` takes a proof isPrime that -- NonTrivial p is p-Rough, and thereby enforces that -- p is a fortiori NonZero and NonUnit @@ -114,40 +114,43 @@ record Prime (p : ℕ) : Set where constructor prime field {{nt}} : NonTrivial p - isPrime : p Rough p + isPrime : Rough p p -- Definition of irreducibility -Irreducible : ℕ → Set -Irreducible n = ∀[ (λ d → d ∣ n → d ≡ 1 ⊎ d ≡ n) ] +Irreducible : Pred ℕ _ +Irreducible n = ∀[ irreducible n ] + where + irreducible : ℕ → Pred ℕ _ + irreducible n d = d ∣ n → d ≡ 1 ⊎ d ≡ n ------------------------------------------------------------------------ -- Basic properties of Rough -- 1 is always rough -_rough-1 : ∀ k → k Rough 1 -(_ rough-1) {2+ _} (boundedComposite _ d∣1@(divides q@(suc _) ())) +rough-1 : ∀ k → Rough k 1 +rough-1 _ {2+ _} (boundedComposite _ d∣1@(divides q@(suc _) ())) -- Any number is 0-, 1- and 2-rough, --- because no non-trivial factor d can be less than 0 , 1, 2 -0-rough : 0 Rough n +-- because no non-trivial factor d can be less than 0, 1, or 2 +0-rough : Rough 0 n 0-rough (boundedComposite () _) -1-rough : 1 Rough n +1-rough : Rough 1 n 1-rough (boundedComposite ⦃()⦄ z 1 divides n, then p must be prime -rough⇒∣⇒prime : ⦃ NonTrivial p ⦄ → p Rough n → p ∣ n → Prime p +rough⇒∣⇒prime : ⦃ NonTrivial p ⦄ → Rough p n → p ∣ n → Prime p rough⇒∣⇒prime r p∣n = prime (rough⇒∣⇒rough r p∣n) ------------------------------------------------------------------------ From cc9e3a95bd4f216964cbcd290fcc69111f53cc37 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 28 Oct 2023 18:08:48 +0100 Subject: [PATCH 24/78] =?UTF-8?q?tidying=20up:=20restored=20`rough?= =?UTF-8?q?=E2=87=92=E2=89=A4`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Nat/Primality.agda | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 4275dc74bd..c2ab717b9e 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -143,6 +143,10 @@ rough-1 _ {2+ _} (boundedComposite _ d∣1@(divides q@(suc _) ())) 2-rough : Rough 2 n 2-rough (boundedComposite ⦃()⦄ (s 1 is k-rough, then k ≤ n +rough⇒≤ : ⦃ NonTrivial n ⦄ → Rough k n → k ≤ n +rough⇒≤ rough = ≮⇒≥ λ k>n → rough (boundedComposite k>n ∣-refl) + -- If a number n is k-rough, and k ∤ n, then n is (suc k)-rough ∤⇒rough-suc : k ∤ n → Rough k n → Rough (suc k) n ∤⇒rough-suc k∤n r (boundedComposite d<1+k d∣n) with m<1+n⇒m Date: Sat, 28 Oct 2023 23:58:29 +0100 Subject: [PATCH 25/78] further refinements; added `NonTrivial` proofs --- src/Data/Nat/Primality.agda | 43 ++++++++++++++++++++++++++----------- 1 file changed, 31 insertions(+), 12 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index c2ab717b9e..cc41775d4b 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -82,12 +82,15 @@ record BoundedComposite (k n d : ℕ) : Set where d1 : 1 < d → d < n → d ∣ n → BoundedComposite n n d +boundedComposite>1 11⇒nonTrivial 11⇒nonTrivial 11 11 , d∣n) (anyUpTo? (λ d → 1 1 d∣n) - (λ (prime p) {d} d1⇒nonTrivial 11 1 Date: Wed, 1 Nov 2023 19:16:53 +0000 Subject: [PATCH 26/78] tidying up --- src/Data/Nat/Primality.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index cc41775d4b..2cc52b9eac 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -13,11 +13,11 @@ open import Data.Nat.Base open import Data.Nat.Divisibility open import Data.Nat.GCD using (module GCD; module Bézout) open import Data.Nat.Properties -open import Data.Product.Base using (_×_; map₂; _,_; proj₂) +open import Data.Product.Base using (_×_; map₂; _,_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (flip; _∘_; _∘′_) open import Relation.Nullary.Decidable as Dec - using (yes; no; from-yes; from-no; ¬?; decidable-stable; _×-dec_; _⊎-dec_; _→-dec_) + using (yes; no; from-yes; ¬?; _×-dec_; _⊎-dec_; _→-dec_; decidable-stable) open import Relation.Nullary.Negation using (¬_; contradiction) open import Relation.Unary using (Pred; Decidable; IUniversal; Satisfiable) open import Relation.Binary.PropositionalEquality @@ -178,7 +178,7 @@ rough⇒∣⇒prime r p∣n = prime (rough⇒∣⇒rough r p∣n) ¬composite[1] (_ , composite[1]) = 1-rough composite[1] composite[4] : Composite 4 -composite[4] = composite {d = 2} (λ ()) (divides 2 refl) +composite[4] = composite {d = 2} (λ ()) (divides-refl 2) ------------------------------------------------------------------------ -- Basic (non-)instances of Prime @@ -320,7 +320,7 @@ euclidsLemma m n {p} (prime pr) p∣m*n = result ... | Bézout.result 0 g _ = contradiction (0∣⇒≡0 (GCD.gcd∣n g)) (≢-nonZero⁻¹ _) -- this should be a typechecker-rejectable case!? - -- if the GCD of m and p is one then m and p is coprime, and we know + -- if the GCD of m and p is one then m and p are coprime, and we know -- that for some integers s and r, sm + rp = 1. We can use this fact -- to determine that p divides n ... | Bézout.result 1 _ (Bézout.+- r s 1+sp≡rm) = From df55fb167802962c8ae957ce03d0e7afbdcdcd70 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 3 Nov 2023 06:06:33 +0000 Subject: [PATCH 27/78] moving definitions to `Data.Nat.Base` --- CHANGELOG.md | 12 ++++++++++++ src/Data/Nat/Base.agda | 40 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 52 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7767295d3e..58023743fd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2728,6 +2728,18 @@ Additions to existing modules s≤″s⁻¹ : suc m ≤″ suc n → m ≤″ n s<″s⁻¹ : suc m <″ suc n → m <″ n + pattern 2+ n = suc (suc n) + pattern 1<2+n {n} = s1⇒nonTrivial : 1 < n → NonTrivial n + nonZero⇒≢1⇒nonTrivial : .⦃ NonZero n ⦄ → n ≢ 1 → NonTrivial n + nonTrivial⇒nonZero : .⦃ NonTrivial n ⦄ → NonZero n + nonTrivial⇒n>1 : .⦃ NonTrivial n ⦄ → 1 < n + nonTrivial⇒≢1 : .⦃ NonTrivial n ⦄ → n ≢ 1 + _⊔′_ : ℕ → ℕ → ℕ _⊓′_ : ℕ → ℕ → ℕ ∣_-_∣′ : ℕ → ℕ → ℕ diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index f2755c55fc..8f2e142950 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -16,11 +16,13 @@ open import Algebra.Definitions.RawMagma using (_∣ˡ_) open import Data.Bool.Base using (Bool; true; false; T; not) open import Data.Parity.Base using (Parity; 0ℙ; 1ℙ) open import Data.Product.Base using (_,_) +open import Function.Base using (_∘_) open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl) open import Relation.Nullary.Negation.Core using (¬_; contradiction) +open import Relation.Unary using (Pred) ------------------------------------------------------------------------ -- Types @@ -130,6 +132,44 @@ instance >-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n > 0 >-nonZero⁻¹ (suc n) = z1⇒nonTrivial : ∀ {n} → 1 < n → NonTrivial n +n>1⇒nonTrivial 1<2+n = _ + +nonZero⇒≢1⇒nonTrivial : ∀ {n} → .⦃ NonZero n ⦄ → n ≢ 1 → NonTrivial n +nonZero⇒≢1⇒nonTrivial {1} = contradiction refl +nonZero⇒≢1⇒nonTrivial {2+ _} = _ + +-- Destructors + +nonTrivial⇒nonZero : ∀ {n} → .⦃ NonTrivial n ⦄ → NonZero n +nonTrivial⇒nonZero {n = 2+ k} = _ + +nonTrivial⇒n>1 : ∀ n → .⦃ NonTrivial n ⦄ → 1 < n +nonTrivial⇒n>1 (2+ _) = 1<2+n + +nonTrivial⇒≢1 : ∀ {n} → .⦃ NonTrivial n ⦄ → n ≢ 1 +nonTrivial⇒≢1 ⦃()⦄ refl + ------------------------------------------------------------------------ -- Raw bundles From 66b3da671e4ab2bf96f3a3996cd4e0612764d807 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 3 Nov 2023 06:50:42 +0000 Subject: [PATCH 28/78] propagated changes; many more explicit s required? --- src/Data/Nat/Primality.agda | 71 ++++++++----------------------------- 1 file changed, 14 insertions(+), 57 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 2cc52b9eac..68c393a4b0 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -8,7 +8,6 @@ module Data.Nat.Primality where -open import Data.Bool.Base using (Bool; true; false; not; T) open import Data.Nat.Base open import Data.Nat.Divisibility open import Data.Nat.GCD using (module GCD; module Bézout) @@ -27,49 +26,6 @@ private variable d k m n p : ℕ ------------------------------------------------------------------------- --- Definitions for `Data.Nat.Base` - -pattern 2+ n = suc (suc n) - -trivial : ℕ → Bool -trivial 0 = true -trivial 1 = true -trivial (2+ _) = false - -Unit NonUnit NonTrivial : Pred ℕ _ -Unit = T ∘ (_≡ᵇ 1) -NonUnit = T ∘ not ∘ (_≡ᵇ 1) -NonTrivial = T ∘ not ∘ trivial - -instance - nonUnit[0] : NonUnit 0 - nonUnit[0] = _ - - nonTrivial⇒nonUnit : .{{NonTrivial n}} → NonUnit n - nonTrivial⇒nonUnit {n = 2+ _} = _ - -nonUnit⇒≢1 : .{{NonUnit n}} → n ≢ 1 -nonUnit⇒≢1 ⦃()⦄ refl -instance - nonTrivial : NonTrivial (2+ n) - nonTrivial = _ - -nonTrivial⇒≢1 : .{{NonTrivial n}} → n ≢ 1 -nonTrivial⇒≢1 ⦃()⦄ refl - -nonTrivial⇒nonZero : .{{NonTrivial n}} → NonZero n -nonTrivial⇒nonZero {n = 2+ k} = _ - -pattern 1<2+n {n} = s1 : .{{NonTrivial n}} → 1 < n -nonTrivial⇒n>1 {n = 2+ _} = 1<2+n - -n>1⇒nonTrivial : 1 < n → NonTrivial n -n>1⇒nonTrivial 1<2+n = _ - - ------------------------------------------------------------------------ -- Definitions @@ -84,9 +40,9 @@ record BoundedComposite (k n d : ℕ) : Set where -- smart constructors -boundedComposite≢ : .{{NonZero n}} → {{NonTrivial d}} → +boundedComposite≢ : {{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → BoundedComposite n n d -boundedComposite≢ d≢n d∣n = boundedComposite (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n +boundedComposite≢ ⦃ nt ⦄ d≢n d∣n = boundedComposite ⦃ nt ⦄ (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n boundedComposite>1 : 1 < d → d < n → d ∣ n → BoundedComposite n n d boundedComposite>1 11⇒nonTrivial 11 11 , d∣n) + (map₂ λ {d} (boundedComposite d1 d , d∣n) (anyUpTo? (λ d → 1 1 d∣n) + (λ r → prime ⦃ nonTrivial {n} ⦄ λ {d} (boundedComposite d1 d) d∣n) (λ (prime p) {d} d1 1 Date: Fri, 3 Nov 2023 07:03:23 +0000 Subject: [PATCH 29/78] `NonTrivial` is `Recomputable` --- CHANGELOG.md | 1 + src/Data/Nat/Base.agda | 3 +++ src/Data/Nat/Primality.agda | 14 +++++++------- 3 files changed, 11 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 58023743fd..32c7ad6c86 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2736,6 +2736,7 @@ Additions to existing modules instance nonTrivial : NonTrivial (2+ n) n>1⇒nonTrivial : 1 < n → NonTrivial n nonZero⇒≢1⇒nonTrivial : .⦃ NonZero n ⦄ → n ≢ 1 → NonTrivial n + recompute-nonTrivial : .⦃ NonTrivial n ⦄ → NonTrivial n nonTrivial⇒nonZero : .⦃ NonTrivial n ⦄ → NonZero n nonTrivial⇒n>1 : .⦃ NonTrivial n ⦄ → 1 < n nonTrivial⇒≢1 : .⦃ NonTrivial n ⦄ → n ≢ 1 diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 8f2e142950..a16798beda 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -159,6 +159,9 @@ nonZero⇒≢1⇒nonTrivial : ∀ {n} → .⦃ NonZero n ⦄ → n ≢ 1 → Non nonZero⇒≢1⇒nonTrivial {1} = contradiction refl nonZero⇒≢1⇒nonTrivial {2+ _} = _ +recompute-nonTrivial : ∀ {n} → .⦃ NonTrivial n ⦄ → NonTrivial n +recompute-nonTrivial {2+ _} = _ + -- Destructors nonTrivial⇒nonZero : ∀ {n} → .⦃ NonTrivial n ⦄ → NonZero n diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 68c393a4b0..236e33ea7b 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -34,15 +34,15 @@ private record BoundedComposite (k n d : ℕ) : Set where constructor boundedComposite field - {{nt}} : NonTrivial d + .{{nt}} : NonTrivial d d1 : 1 < d → d < n → d ∣ n → BoundedComposite n n d boundedComposite>1 11⇒nonTrivial 1 Date: Fri, 3 Nov 2023 08:29:39 +0000 Subject: [PATCH 30/78] all instances of `NonTrivial` now irrelevant; weird to need `NonTrivial 2` explicitly --- src/Data/Nat/Primality.agda | 42 ++++++++++++++++++++++--------------- 1 file changed, 25 insertions(+), 17 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 236e33ea7b..143cdb56a6 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -26,6 +26,10 @@ private variable d k m n p : ℕ + instance + nt[2] : NonTrivial 2 + nt[2] = nonTrivial {0} + ------------------------------------------------------------------------ -- Definitions @@ -45,18 +49,21 @@ boundedComposite≢ : .{{NonTrivial d}} → .{{NonZero n}} → boundedComposite≢ d≢n d∣n = boundedComposite (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n boundedComposite>1 : 1 < d → d < n → d ∣ n → BoundedComposite n n d -boundedComposite>1 11⇒nonTrivial 11 11⇒nonTrivial 1 1 is k-rough, then k ≤ n -rough⇒≤ : ⦃ NonTrivial n ⦄ → Rough k n → k ≤ n +rough⇒≤ : .⦃ NonTrivial n ⦄ → Rough k n → k ≤ n rough⇒≤ rough = ≮⇒≥ λ k>n → rough (boundedComposite k>n ∣-refl) -- If a number n is k-rough, and k ∤ n, then n is (suc k)-rough @@ -121,7 +128,7 @@ rough⇒∣⇒rough r n∣m (boundedComposite d 1 divides n, then p must be prime -rough⇒∣⇒prime : ⦃ NonTrivial p ⦄ → Rough p n → p ∣ n → Prime p +rough⇒∣⇒prime : .⦃ NonTrivial p ⦄ → Rough p n → p ∣ n → Prime p rough⇒∣⇒prime r p∣n = prime (rough⇒∣⇒rough r p∣n) ------------------------------------------------------------------------ @@ -134,7 +141,8 @@ rough⇒∣⇒prime r p∣n = prime (rough⇒∣⇒rough r p∣n) ¬composite[1] (_ , composite[1]) = 1-rough composite[1] composite[4] : Composite 4 -composite[4] = composite {d = 2} ⦃ nonTrivial {2} ⦄ (λ ()) (divides-refl 2) +composite[4] = composite≢ {d = 2} (λ()) (divides-refl 2) + ------------------------------------------------------------------------ -- Basic (non-)instances of Prime @@ -146,7 +154,7 @@ composite[4] = composite {d = 2} ⦃ nonTrivial {2} ⦄ (λ ()) (divides-refl 2) ¬prime[1] () prime[2] : Prime 2 -prime[2] = prime ⦃ nonTrivial {2} ⦄ 2-rough +prime[2] = prime 2-rough ------------------------------------------------------------------------ -- Basic (non-)instances of Irreducible @@ -201,7 +209,7 @@ prime? : Decidable Prime prime? 0 = no ¬prime[0] prime? 1 = no ¬prime[1] prime? n@(2+ _) = Dec.map′ - (λ r → prime ⦃ nonTrivial {n} ⦄ λ {d} (boundedComposite d1 d) d∣n) + (λ r → prime λ {d} (boundedComposite d1 d) d∣n) (λ (prime p) {d} d1 1 Date: Fri, 3 Nov 2023 08:50:21 +0000 Subject: [PATCH 31/78] tidying up `Coprimality`, eg with `variable`s --- src/Data/Nat/Coprimality.agda | 53 ++++++++++++++++++----------------- 1 file changed, 27 insertions(+), 26 deletions(-) diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index 68fd054b85..1ebf20eedb 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -25,6 +25,9 @@ open import Relation.Nullary as Nullary using (¬_; contradiction; yes ; no) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Symmetric; Decidable) +private + variable d k m n p : ℕ + open ≤-Reasoning ------------------------------------------------------------------------ @@ -34,22 +37,22 @@ open ≤-Reasoning -- prime), i.e. if their only common divisor is 1. Coprime : Rel ℕ 0ℓ -Coprime m n = ∀ {i} → i ∣ m × i ∣ n → i ≡ 1 +Coprime m n = ∀ {d} → d ∣ m × d ∣ n → d ≡ 1 ------------------------------------------------------------------------ -- Relationship between GCD and coprimality -coprime⇒GCD≡1 : ∀ {m n} → Coprime m n → GCD m n 1 -coprime⇒GCD≡1 {m} {n} c = GCD.is (1∣ m , 1∣ n) (∣-reflexive ∘ c) +coprime⇒GCD≡1 : Coprime m n → GCD m n 1 +coprime⇒GCD≡1 {m} {n} coprime = GCD.is (1∣ m , 1∣ n) (∣-reflexive ∘ coprime) -GCD≡1⇒coprime : ∀ {m n} → GCD m n 1 → Coprime m n +GCD≡1⇒coprime : GCD m n 1 → Coprime m n GCD≡1⇒coprime g cd with divides q eq ← GCD.greatest g cd = m*n≡1⇒n≡1 q _ (P.sym eq) -coprime⇒gcd≡1 : ∀ {m n} → Coprime m n → gcd m n ≡ 1 +coprime⇒gcd≡1 : Coprime m n → gcd m n ≡ 1 coprime⇒gcd≡1 coprime = GCD.unique (gcd-GCD _ _) (coprime⇒GCD≡1 coprime) -gcd≡1⇒coprime : ∀ {m n} → gcd m n ≡ 1 → Coprime m n +gcd≡1⇒coprime : gcd m n ≡ 1 → Coprime m n gcd≡1⇒coprime gcd≡1 = GCD≡1⇒coprime (subst (GCD _ _) gcd≡1 (gcd-GCD _ _)) coprime-/gcd : ∀ m n .{{_ : NonZero (gcd m n)}} → @@ -66,14 +69,14 @@ private 0≢1 : 0 ≢ 1 0≢1 () - 2+≢1 : ∀ {n} → suc (suc n) ≢ 1 + 2+≢1 : ∀ {n} → 2+ n ≢ 1 2+≢1 () coprime? : Decidable Coprime -coprime? i j with mkGCD i j -... | (0 , g) = no (0≢1 ∘ GCD.unique g ∘ coprime⇒GCD≡1) -... | (1 , g) = yes (GCD≡1⇒coprime g) -... | (suc (suc d) , g) = no (2+≢1 ∘ GCD.unique g ∘ coprime⇒GCD≡1) +coprime? m n with mkGCD m n +... | (0 , g) = no (0≢1 ∘ GCD.unique g ∘ coprime⇒GCD≡1) +... | (1 , g) = yes (GCD≡1⇒coprime g) +... | (2+ _ , g) = no (2+≢1 ∘ GCD.unique g ∘ coprime⇒GCD≡1) ------------------------------------------------------------------------ -- Other basic properties @@ -86,20 +89,20 @@ coprime? i j with mkGCD i j -- Nothing except for 1 is coprime to 0. 0-coprimeTo-m⇒m≡1 : ∀ {m} → Coprime 0 m → m ≡ 1 -0-coprimeTo-m⇒m≡1 {m} c = c (m ∣0 , ∣-refl) +0-coprimeTo-m⇒m≡1 {m} coprime = coprime (m ∣0 , ∣-refl) -¬0-coprimeTo-2+ : ∀ {n} → ¬ Coprime 0 (2 + n) +¬0-coprimeTo-2+ : ∀ {n} → ¬ Coprime 0 (2+ n) ¬0-coprimeTo-2+ coprime = contradiction (0-coprimeTo-m⇒m≡1 coprime) λ() -- If m and n are coprime, then n + m and n are also coprime. -coprime-+ : ∀ {m n} → Coprime m n → Coprime (n + m) n -coprime-+ c (d₁ , d₂) = c (∣m+n∣m⇒∣n d₁ d₂ , d₂) +coprime-+ : Coprime m n → Coprime (n + m) n +coprime-+ coprime (d₁ , d₂) = coprime (∣m+n∣m⇒∣n d₁ d₂ , d₂) -- Recomputable -recompute : ∀ {n d} → .(Coprime n d) → Coprime n d -recompute {n} {d} c = Nullary.recompute (coprime? n d) c +recompute : .(Coprime n d) → Coprime n d +recompute {n} {d} coprime = Nullary.recompute (coprime? n d) coprime ------------------------------------------------------------------------ -- Relationship with Bezout's lemma @@ -107,8 +110,8 @@ recompute {n} {d} c = Nullary.recompute (coprime? n d) c -- If the "gcd" in Bézout's identity is non-zero, then the "other" -- divisors are coprime. -Bézout-coprime : ∀ {i j d} .{{_ : NonZero d}} → - Bézout.Identity d (i * d) (j * d) → Coprime i j +Bézout-coprime : .{{_ : NonZero d}} → + Bézout.Identity d (m * d) (n * d) → Coprime m n Bézout-coprime {d = suc _} (Bézout.+- x y eq) (divides-refl q₁ , divides-refl q₂) = lem₁₀ y q₂ x q₁ eq Bézout-coprime {d = suc _} (Bézout.-+ x y eq) (divides-refl q₁ , divides-refl q₂) = @@ -116,21 +119,20 @@ Bézout-coprime {d = suc _} (Bézout.-+ x y eq) (divides-refl q₁ , divides-ref -- Coprime numbers satisfy Bézout's identity. -coprime-Bézout : ∀ {i j} → Coprime i j → Bézout.Identity 1 i j +coprime-Bézout : Coprime m n → Bézout.Identity 1 m n coprime-Bézout = Bézout.identity ∘ coprime⇒GCD≡1 -- If i divides jk and is coprime to j, then it divides k. -coprime-divisor : ∀ {k i j} → Coprime i j → i ∣ j * k → i ∣ k -coprime-divisor {k} c (divides q eq′) with coprime-Bézout c +coprime-divisor : Coprime m n → m ∣ n * k → m ∣ k +coprime-divisor {k = k} c (divides q eq′) with coprime-Bézout c ... | Bézout.+- x y eq = divides (x * k ∸ y * q) (lem₈ x y eq eq′) ... | Bézout.-+ x y eq = divides (y * q ∸ x * k) (lem₉ x y eq eq′) -- If d is a common divisor of mk and nk, and m and n are coprime, -- then d divides k. -coprime-factors : ∀ {d m n k} → - Coprime m n → d ∣ m * k × d ∣ n * k → d ∣ k +coprime-factors : Coprime m n → d ∣ m * k × d ∣ n * k → d ∣ k coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout c ... | Bézout.+- x y eq = divides (x * q₁ ∸ y * q₂) (lem₁₁ x y eq eq₁ eq₂) ... | Bézout.-+ x y eq = divides (y * q₂ ∸ x * q₁) (lem₁₁ y x eq eq₂ eq₁) @@ -138,8 +140,7 @@ coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout ------------------------------------------------------------------------ -- Primality implies coprimality. -prime⇒coprime≢0 : ∀ {p} → Prime p → - ∀ {n} .{{_ : NonZero n}} → n < p → Coprime p n +prime⇒coprime≢0 : Prime p → .{{_ : NonZero n}} → n < p → Coprime p n prime⇒coprime≢0 p n

Date: Fri, 3 Nov 2023 09:47:14 +0000 Subject: [PATCH 32/78] `NonTrivial` is `Decidable` --- src/Data/Nat/Properties.agda | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 37b1f33ee0..9d7ddf1ebe 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -60,6 +60,15 @@ nonZero? : U.Decidable NonZero nonZero? zero = no NonZero.nonZero nonZero? (suc n) = yes _ +------------------------------------------------------------------------ +-- Properties of NonTrivial +------------------------------------------------------------------------ + +nonTrivial? : U.Decidable NonTrivial +nonTrivial? 0 = no λ() +nonTrivial? 1 = no λ() +nonTrivial? (2+ n) = yes _ + ------------------------------------------------------------------------ -- Properties of _≡_ ------------------------------------------------------------------------ From 4022d3edbc5f09e0c79a7869faef20f040de66bc Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 3 Nov 2023 10:44:23 +0000 Subject: [PATCH 33/78] systematise proofs of `Decidable` properties via the `UpTo` predicates --- src/Data/Nat/Primality.agda | 175 +++++++++++++++++++++++------------- 1 file changed, 114 insertions(+), 61 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 143cdb56a6..80627180c9 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -8,7 +8,7 @@ module Data.Nat.Primality where -open import Data.Nat.Base +open import Data.Nat.Base hiding (less-than-or-equal) open import Data.Nat.Divisibility open import Data.Nat.GCD using (module GCD; module Bézout) open import Data.Nat.Properties @@ -16,9 +16,9 @@ open import Data.Product.Base using (_×_; map₂; _,_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (flip; _∘_; _∘′_) open import Relation.Nullary.Decidable as Dec - using (yes; no; from-yes; ¬?; _×-dec_; _⊎-dec_; _→-dec_; decidable-stable) + using (yes; no; from-yes; from-no; ¬?; _×-dec_; _⊎-dec_; _→-dec_; decidable-stable) open import Relation.Nullary.Negation using (¬_; contradiction) -open import Relation.Unary using (Pred; Decidable; IUniversal; Satisfiable) +open import Relation.Unary using (Pred; Decidable; IUniversal; Satisfiable; _∩_; _⇒_) open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong) @@ -35,8 +35,8 @@ private -- Definition of having a non-trivial divisor below a given bound -record BoundedComposite (k n d : ℕ) : Set where - constructor boundedComposite +record HasBoundedDivisor (k n d : ℕ) : Set where + constructor hasBoundedDivisor field .{{nt}} : NonTrivial d d1 : 1 < d → d < n → d ∣ n → BoundedComposite n n d -boundedComposite>1 11 : 1 < d → d < n → d ∣ n → HasBoundedDivisor n n d +hasBoundedDivisor>1 11⇒nonTrivial 1 1 is k-rough, then k ≤ n rough⇒≤ : .⦃ NonTrivial n ⦄ → Rough k n → k ≤ n -rough⇒≤ rough = ≮⇒≥ λ k>n → rough (boundedComposite k>n ∣-refl) +rough⇒≤ rough = ≮⇒≥ λ k>n → rough (hasBoundedDivisor k>n ∣-refl) -- If a number n is k-rough, and k ∤ n, then n is (suc k)-rough ∤⇒rough-suc : k ∤ n → Rough k n → Rough (suc k) n -∤⇒rough-suc k∤n r (boundedComposite d<1+k d∣n) with m<1+n⇒m1 11 d , d∣n) - (anyUpTo? (λ d → 1 1 d) d∣n) - (λ (prime p) {d} d1 1 Date: Fri, 3 Nov 2023 11:14:38 +0000 Subject: [PATCH 34/78] =?UTF-8?q?explicit=20quantifier=20now=20in=20`compo?= =?UTF-8?q?site=E2=89=A2`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Nat/Primality.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 80627180c9..66c4ef09b0 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -66,12 +66,12 @@ CompositeUpTo n = ∃⟨ (_< n) ∩ HasNonTrivialDivisor ⟩ -- smart constructors -composite≢ : .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → Composite n -composite≢ {d = d} d≢n d∣n = d , hasBoundedDivisor≢ d≢n d∣n - composite : .{{NonTrivial d}} → d < n → d ∣ n → Composite n composite {d = d} d Date: Fri, 3 Nov 2023 12:28:43 +0000 Subject: [PATCH 35/78] Nathan's simplification --- src/Data/Nat/Primality.agda | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 66c4ef09b0..21ed0ad99e 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -102,14 +102,14 @@ module _ (n : ℕ) where private - irreducible : Pred ℕ _ - irreducible d = d ∣ n → d ≡ 1 ⊎ d ≡ n + Irreducible′ : Pred ℕ _ + Irreducible′ d = d ∣ n → d ≡ 1 ⊎ d ≡ n Irreducible : Set - Irreducible = ∀[ irreducible ] + Irreducible = ∀[ Irreducible′ ] IrreducibleUpTo : Set - IrreducibleUpTo = ∀[ (_< n) ⇒ irreducible ] + IrreducibleUpTo = ∀[ (_< n) ⇒ Irreducible′ ] ------------------------------------------------------------------------ -- Basic properties of Rough @@ -370,7 +370,7 @@ euclidsLemma m n {p} (prime pr) p∣m*n = result -- if the GCD of m and p is greater than one, then it must be p and hence p ∣ m. ... | Bézout.result d@(2+ _) g _ with d ≟ p ... | yes d≡p@refl = inj₁ (GCD.gcd∣m g) - ... | no d≢p = contradiction d∣p λ d∣p → pr (hasBoundedDivisor≢ d≢p d∣p) + ... | no d≢p = contradiction (hasBoundedDivisor≢ d≢p d∣p) pr where d∣p : d ∣ p d∣p = GCD.gcd∣n g From de78ca9bba347a4434826b700b806555c93d6a3f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 3 Nov 2023 17:18:42 +0000 Subject: [PATCH 36/78] interaction of `NonZero` and `NonTrivial` instances --- src/Data/Nat/Properties.agda | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 9d7ddf1ebe..f6ac4f311c 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -911,6 +911,12 @@ m*n≡0⇒m≡0∨n≡0 (suc m) {zero} eq = inj₂ refl m*n≢0 : ∀ m n → .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n) m*n≢0 (suc m) (suc n) = _ +m*n≢0⇒m≢0 : ∀ m {n} → .{{NonZero (m * n)}} → NonZero m +m*n≢0⇒m≢0 (suc _) = _ + +m*n≢0⇒n≢0 : ∀ m {n} → .{{NonZero (m * n)}} → NonZero n +m*n≢0⇒n≢0 m {n} rewrite *-comm m n = m*n≢0⇒m≢0 n {m} + m*n≡0⇒m≡0 : ∀ m n .{{_ : NonZero n}} → m * n ≡ 0 → m ≡ 0 m*n≡0⇒m≡0 zero (suc _) eq = refl @@ -931,6 +937,12 @@ m*n≡1⇒n≡1 m n eq = m*n≡1⇒m≡1 n m (trans (*-comm n m) eq) (m * o) * (n * p) ∎ where open CommSemigroupProperties *-commutativeSemigroup +m≢0∧n>1⇒m*n>1 : ∀ m n → .{{_ : NonZero m}} .{{_ : NonTrivial n}} → NonTrivial (m * n) +m≢0∧n>1⇒m*n>1 (suc m) (2+ n) = _ + +n≢0∧m>1⇒m*n>1 : ∀ m n → .{{_ : NonZero n}} .{{_ : NonTrivial m}} → NonTrivial (m * n) +n≢0∧m>1⇒m*n>1 m n rewrite *-comm m n = m≢0∧n>1⇒m*n>1 n m + ------------------------------------------------------------------------ -- Other properties of _*_ and _≤_/_<_ From 2f456a84a53cb18564193c10292e9e404f4d47c7 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 3 Nov 2023 17:38:13 +0000 Subject: [PATCH 37/78] divisor now a record field; final lemmas: closure under divisibility; plus partial `CHANGELOG` entries --- CHANGELOG.md | 24 ++++++---- src/Data/Nat/Primality.agda | 87 ++++++++++++++++++++---------------- src/Data/Nat/Properties.agda | 4 +- 3 files changed, 67 insertions(+), 48 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 32c7ad6c86..81d6753eab 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2778,13 +2778,17 @@ Additions to existing modules * Added new definitions and proofs to `Data.Nat.Primality`: ```agda - Composite : ℕ → Set - composite? : Decidable composite - composite⇒¬prime : Composite n → ¬ Prime n - ¬composite⇒prime : 2 ≤ n → ¬ Composite n → Prime n - prime⇒¬composite : Prime n → ¬ Composite n - ¬prime⇒composite : 2 ≤ n → ¬ Prime n → Composite n - euclidsLemma : Prime p → p ∣ m * n → p ∣ m ⊎ p ∣ n + Composite : ℕ → Set + composite? : Decidable Composite + Irreducible : ℕ → Set + irreducible? : Decidable Irreducible + composite⇒¬prime : Composite n → ¬ Prime n + ¬composite⇒prime : .{{NonTrivial n} → ¬ Composite n → Prime n + prime⇒¬composite : Prime n → ¬ Composite n + ¬prime⇒composite : .{{NonTrivial n} → ¬ Prime n → Composite n + prime⇒irreducible : Prime p → Irreducible p + irreducible⇒prime : .{{NonTrivial p}} → Irreducible p → Prime p + euclidsLemma : Prime p → p ∣ m * n → p ∣ m ⊎ p ∣ n ``` * Added new proofs in `Data.Nat.Properties`: @@ -2794,8 +2798,12 @@ Additions to existing modules n+1+m≢m : n + suc m ≢ m m*n≡0⇒m≡0 : .{{_ : NonZero n}} → m * n ≡ 0 → m ≡ 0 n>0⇒n≢0 : n > 0 → n ≢ 0 - m^n≢0 : .{{_ : NonZero m}} → NonZero (m ^ n) m*n≢0 : .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n) + m*n≢0⇒m≢0 : .{{NonZero (m * n)}} → NonZero m + m*n≢0⇒n≢0 : .{{NonZero (m * n)}} → NonZero n + m≢0∧n>1⇒m*n>1 : .{{_ : NonZero m}} .{{_ : NonTrivial n}} → NonTrivial (m * n) + n≢0∧m>1⇒m*n>1 : .{{_ : NonZero n}} .{{_ : NonTrivial m}} → NonTrivial (m * n) + m^n≢0 : .{{_ : NonZero m}} → NonZero (m ^ n) m≤n⇒n∸m≤n : m ≤ n → n ∸ m ≤ n s1 : 1 < d → d < n → d ∣ n → HasBoundedDivisor n n d -hasBoundedDivisor>1 11 : 1 < d → d < n → d ∣ n → HasBoundedNonTrivialDivisor n n +hasBoundedNonTrivialDivisor>1 11⇒nonTrivial 11⇒m*n>1 q d + _ = m*n≢0⇒m≢0 q -- Definition of 'rough': a number is k-rough -- if all its non-trivial factors d are bounded below by k Rough : ℕ → Pred ℕ _ -Rough k n = ∀[ ¬_ ∘ HasBoundedDivisor k n ] +Rough k n = ¬ HasBoundedNonTrivialDivisor k n -- Definition of primality: complement of Composite -- Constructor `prime` takes a proof isPrime that @@ -116,33 +129,32 @@ module _ (n : ℕ) where -- 1 is always rough rough-1 : ∀ k → Rough k 1 -rough-1 _ {2+ _} (hasBoundedDivisor _ d∣1@(divides q@(suc _) ())) +rough-1 _ (hasBoundedNonTrivialDivisor _ d∣1) = contradiction (∣1⇒≡1 d∣1) nonTrivial⇒≢1 -- Any number is 0-, 1- and 2-rough, -- because no non-trivial factor d can be less than 0, 1, or 2 0-rough : Rough 0 n -0-rough (hasBoundedDivisor () _) +0-rough (hasBoundedNonTrivialDivisor () _) 1-rough : Rough 1 n -1-rough (hasBoundedDivisor ⦃()⦄ z 1 is k-rough, then k ≤ n rough⇒≤ : .⦃ NonTrivial n ⦄ → Rough k n → k ≤ n -rough⇒≤ rough = ≮⇒≥ λ k>n → rough (hasBoundedDivisor k>n ∣-refl) +rough⇒≤ rough = ≮⇒≥ λ k>n → rough (hasBoundedNonTrivialDivisor k>n ∣-refl) -- If a number n is k-rough, and k ∤ n, then n is (suc k)-rough ∤⇒rough-suc : k ∤ n → Rough k n → Rough (suc k) n -∤⇒rough-suc k∤n r (hasBoundedDivisor d<1+k d∣n) with m<1+n⇒m1⇒m*n>1 : ∀ m n → .{{_ : NonZero m}} .{{_ : NonTrivial n}} → NonTrivial (m * n) +m≢0∧n>1⇒m*n>1 : ∀ m n .{{_ : NonZero m}} .{{_ : NonTrivial n}} → NonTrivial (m * n) m≢0∧n>1⇒m*n>1 (suc m) (2+ n) = _ -n≢0∧m>1⇒m*n>1 : ∀ m n → .{{_ : NonZero n}} .{{_ : NonTrivial m}} → NonTrivial (m * n) +n≢0∧m>1⇒m*n>1 : ∀ m n .{{_ : NonZero n}} .{{_ : NonTrivial m}} → NonTrivial (m * n) n≢0∧m>1⇒m*n>1 m n rewrite *-comm m n = m≢0∧n>1⇒m*n>1 n m ------------------------------------------------------------------------ From 207cda4a95f2f294b88919e9fd5c3f08925c1f2b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 3 Nov 2023 18:11:55 +0000 Subject: [PATCH 38/78] '(non-)instances' become '(counter-)examples' --- src/Data/Nat/Primality.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 5fb996939f..76c36499f5 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -164,7 +164,7 @@ rough⇒∣⇒prime : .⦃ NonTrivial p ⦄ → Rough p n → p ∣ n → Prime rough⇒∣⇒prime r p∣n = prime (rough⇒∣⇒rough r p∣n) ------------------------------------------------------------------------ --- Basic (non-)instances of Composite +-- Basic (counter-)examples of Composite ¬composite[0] : ¬ Composite 0 ¬composite[0] composite[0] = 0-rough composite[0] @@ -180,7 +180,7 @@ composite[6] = composite≢ 3 (λ()) (divides-refl 2) ------------------------------------------------------------------------ --- Basic (non-)instances of Prime +-- Basic (counter-)examples of Prime ¬prime[0] : ¬ Prime 0 ¬prime[0] () @@ -192,7 +192,7 @@ prime[2] : Prime 2 prime[2] = prime 2-rough ------------------------------------------------------------------------ --- Basic (non-)instances of Irreducible +-- Basic (counter-)examples of Irreducible ¬irreducible[0] : ¬ Irreducible 0 ¬irreducible[0] irr[0] = [ (λ ()) , (λ ()) ]′ (irr[0] {2} (divides-refl 0)) From d4cb3d498cf4c287c0d16e3c60378512f5d652a6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 3 Nov 2023 18:28:19 +0000 Subject: [PATCH 39/78] stylistics --- src/Data/Nat/Primality.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 76c36499f5..689fdeb28b 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -211,8 +211,8 @@ irreducible[2] {suc _} d∣2 with ∣⇒≤ d∣2 -- NonTrivial composite⇒nonTrivial : Composite n → NonTrivial n -composite⇒nonTrivial {1} = flip contradiction ¬composite[1] -composite⇒nonTrivial {2+ _} _ = _ +composite⇒nonTrivial {1} composite[1] = contradiction composite[1] ¬composite[1] +composite⇒nonTrivial {2+ _} _ = _ prime⇒nonTrivial : Prime p → NonTrivial p prime⇒nonTrivial (prime _) = recompute-nonTrivial @@ -227,7 +227,7 @@ prime⇒nonZero : Prime p → NonZero p prime⇒nonZero (prime _) = nonTrivial⇒nonZero irreducible⇒nonZero : Irreducible n → NonZero n -irreducible⇒nonZero {zero} = flip contradiction ¬irreducible[0] +irreducible⇒nonZero {zero} = flip contradiction ¬irreducible[0] irreducible⇒nonZero {suc _} _ = _ From e9b151b9b43293a9760885c7206eec30f496dbcc Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 6 Nov 2023 08:35:36 +0000 Subject: [PATCH 40/78] removed `k` as a variable/parameter --- src/Data/Nat/Primality.agda | 65 ++++++++++++++++++------------------- 1 file changed, 32 insertions(+), 33 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 689fdeb28b..5b0bd3936c 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -24,8 +24,7 @@ open import Relation.Binary.PropositionalEquality private variable - d k m n p : ℕ - + d m n o p : ℕ instance nt[2] : NonTrivial 2 nt[2] = nonTrivial {0} @@ -35,13 +34,13 @@ private -- Definition of having a non-trivial divisor below a given bound -record HasBoundedNonTrivialDivisor (k n : ℕ) : Set where +record HasBoundedNonTrivialDivisor (m n : ℕ) : Set where constructor hasBoundedNonTrivialDivisor field {divisor} : ℕ - .{{nt}} : NonTrivial divisor - d1 : 1 < d → d < n → d ∣ n → HasBoundedNonTrivialDivisor n n +hasBoundedNonTrivialDivisor>1 : 1 < d → d < m → d ∣ n → HasBoundedNonTrivialDivisor m n hasBoundedNonTrivialDivisor>1 11⇒nonTrivial 11⇒m*n>1 q d _ = m*n≢0⇒m≢0 q --- Definition of 'rough': a number is k-rough --- if all its non-trivial factors d are bounded below by k +-- Definition of 'rough': a number is m-rough +-- if all its non-trivial factors d are bounded below by m Rough : ℕ → Pred ℕ _ -Rough k n = ¬ HasBoundedNonTrivialDivisor k n +Rough m n = ¬ HasBoundedNonTrivialDivisor m n -- Definition of primality: complement of Composite -- Constructor `prime` takes a proof isPrime that @@ -128,7 +127,7 @@ module _ (n : ℕ) where -- Basic properties of Rough -- 1 is always rough -rough-1 : ∀ k → Rough k 1 +rough-1 : ∀ m → Rough m 1 rough-1 _ (hasBoundedNonTrivialDivisor _ d∣1) = contradiction (∣1⇒≡1 d∣1) nonTrivial⇒≢1 -- Any number is 0-, 1- and 2-rough, @@ -142,19 +141,19 @@ rough-1 _ (hasBoundedNonTrivialDivisor _ d∣1) = contradiction (∣1⇒≡1 d 2-rough : Rough 2 n 2-rough (hasBoundedNonTrivialDivisor ⦃()⦄ (s 1 is k-rough, then k ≤ n -rough⇒≤ : .⦃ NonTrivial n ⦄ → Rough k n → k ≤ n -rough⇒≤ rough = ≮⇒≥ λ k>n → rough (hasBoundedNonTrivialDivisor k>n ∣-refl) +-- If a number n > 1 is m-rough, then m ≤ n +rough⇒≤ : .⦃ NonTrivial n ⦄ → Rough m n → m ≤ n +rough⇒≤ rough = ≮⇒≥ λ m>n → rough (hasBoundedNonTrivialDivisor m>n ∣-refl) --- If a number n is k-rough, and k ∤ n, then n is (suc k)-rough -∤⇒rough-suc : k ∤ n → Rough k n → Rough (suc k) n -∤⇒rough-suc k∤n r (hasBoundedNonTrivialDivisor d<1+k d∣n) with m<1+n⇒m Date: Mon, 6 Nov 2023 09:00:57 +0000 Subject: [PATCH 41/78] renamed fields and smart constructors --- src/Data/Nat/Primality.agda | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 5b0bd3936c..03ef66efaf 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -37,23 +37,21 @@ private record HasBoundedNonTrivialDivisor (m n : ℕ) : Set where constructor hasBoundedNonTrivialDivisor field - {divisor} : ℕ - .{{nt}} : NonTrivial divisor - d1 : 1 < d → d < m → d ∣ n → HasBoundedNonTrivialDivisor m n -hasBoundedNonTrivialDivisor>1 11⇒nonTrivial 1 Date: Mon, 6 Nov 2023 09:05:41 +0000 Subject: [PATCH 42/78] moved smart constructors; made a local definition --- src/Data/Nat/Base.agda | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index a16798beda..bd747e86cd 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -30,6 +30,9 @@ open import Relation.Unary using (Pred) open import Agda.Builtin.Nat public using (zero; suc) renaming (Nat to ℕ) +--smart constructor +pattern 2+ n = suc (suc n) + ------------------------------------------------------------------------ -- Boolean equality relation @@ -63,6 +66,7 @@ m < n = suc m ≤ n pattern z1⇒nonTrivial : ∀ {n} → 1 < n → NonTrivial n From ba7c7825e83aa5e4d2c076024ec55b08ea821690 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 6 Nov 2023 10:39:18 +0000 Subject: [PATCH 43/78] tidying up --- src/Data/Nat/Base.agda | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index bd747e86cd..e2545ab5af 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -146,7 +146,6 @@ NonTrivial = T ∘ not ∘ trivial trivial 1 = true trivial (2+ _) = false - instance nonTrivial : ∀ {n} → NonTrivial (2+ n) nonTrivial = _ @@ -156,10 +155,6 @@ instance n>1⇒nonTrivial : ∀ {n} → 1 < n → NonTrivial n n>1⇒nonTrivial 1<2+n = _ -nonZero⇒≢1⇒nonTrivial : ∀ {n} → .⦃ NonZero n ⦄ → n ≢ 1 → NonTrivial n -nonZero⇒≢1⇒nonTrivial {1} = contradiction refl -nonZero⇒≢1⇒nonTrivial {2+ _} = _ - recompute-nonTrivial : ∀ {n} → .⦃ NonTrivial n ⦄ → NonTrivial n recompute-nonTrivial {2+ _} = _ From 22e6c38f33a5976b4a7a703c5edc50d68f8f4a99 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 6 Nov 2023 10:41:28 +0000 Subject: [PATCH 44/78] refactoring per review comments: equivalence of `UpTo` predicates; making more things `private` --- src/Data/Nat/Primality.agda | 163 +++++++++++++++++++++--------------- 1 file changed, 94 insertions(+), 69 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 03ef66efaf..413d804fd8 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -12,13 +12,15 @@ open import Data.Nat.Base open import Data.Nat.Divisibility open import Data.Nat.GCD using (module GCD; module Bézout) open import Data.Nat.Properties -open import Data.Product.Base using (_×_; map₂; _,_) +open import Data.Product.Base using (∃-syntax; _×_; map₂; _,_) open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′) open import Function.Base using (flip; _∘_; _∘′_) +open import Function.Bundles using (_⇔_; mk⇔) open import Relation.Nullary.Decidable as Dec using (yes; no; from-yes; from-no; ¬?; _×-dec_; _⊎-dec_; _→-dec_; decidable-stable) open import Relation.Nullary.Negation using (¬_; contradiction) -open import Relation.Unary using (Pred; Decidable; IUniversal; Satisfiable; _∩_; _⇒_) +open import Relation.Unary using (Pred; Decidable) +open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; cong) @@ -32,6 +34,22 @@ private ------------------------------------------------------------------------ -- Definitions +-- The definitions of `Prime` and `Composite` in this module are intended to +-- be built up as complementary pairs of `Decidable` predicates, with `Prime` +-- given *negatively* as the universal closure of the negation of `Composite`, +-- where this is given *positively* as an existential witnessing a non-trivial +-- divisor, where such quantification is proxied by an explicit `record` type. + +-- For technical reasons, in order to be able to prove decidability via the +-- `all?` and `any?` combinators for *bounded* predicates on ℕ, we further +-- define the bounded counterparts to predicates `P...` as `P...UpTo` and show +-- the equivalence of the two. + +-- Finally, the definitions of the predicates `Composite` and `Prime` as the +-- 'diagonal' instances of relations involving such bounds on the possible +-- non-trivial divisors leads to the following positive/existential predicate +-- as the basis for the whole development. + -- Definition of having a non-trivial divisor below a given bound record HasBoundedNonTrivialDivisor (m n : ℕ) : Set where @@ -60,12 +78,21 @@ hasBoundedNonTrivialDivisor-∣ (hasBoundedNonTrivialDivisor d Date: Mon, 6 Nov 2023 10:47:21 +0000 Subject: [PATCH 45/78] tidying up: names congruent to ordering relation --- src/Data/Nat/Base.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index e2545ab5af..57a90be651 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -152,7 +152,7 @@ instance -- Constructors -n>1⇒nonTrivial : ∀ {n} → 1 < n → NonTrivial n +n>1⇒nonTrivial : ∀ {n} → n > 1 → NonTrivial n n>1⇒nonTrivial 1<2+n = _ recompute-nonTrivial : ∀ {n} → .⦃ NonTrivial n ⦄ → NonTrivial n @@ -163,7 +163,7 @@ recompute-nonTrivial {2+ _} = _ nonTrivial⇒nonZero : ∀ {n} → .⦃ NonTrivial n ⦄ → NonZero n nonTrivial⇒nonZero {n = 2+ k} = _ -nonTrivial⇒n>1 : ∀ n → .⦃ NonTrivial n ⦄ → 1 < n +nonTrivial⇒n>1 : ∀ n → .⦃ NonTrivial n ⦄ → n > 1 nonTrivial⇒n>1 (2+ _) = 1<2+n nonTrivial⇒≢1 : ∀ {n} → .⦃ NonTrivial n ⦄ → n ≢ 1 From eaf3d6b92c61f752c7583ca2b8d49b089e79c404 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 6 Nov 2023 11:08:43 +0000 Subject: [PATCH 46/78] removed variable `k`; removed old proof in favour of new one with `NonZero` instance --- CHANGELOG.md | 1 + src/Data/Nat/Coprimality.agda | 35 +++++++++++++++-------------------- 2 files changed, 16 insertions(+), 20 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 87f1f16208..428b8586c9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3633,6 +3633,7 @@ This is a full list of proofs that have changed form to use irrelevant instance * In `Data.Nat.Coprimality`: ``` Bézout-coprime : ∀ {i j d} → Bézout.Identity (suc d) (i * suc d) (j * suc d) → Coprime i j + prime⇒coprime : ∀ m → Prime m → ∀ n → 0 < n → n < m → Coprime m n ``` * In `Data.Nat.Divisibility` diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index 1ebf20eedb..1d04513ea9 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -26,7 +26,7 @@ open import Relation.Binary.Core using (Rel) open import Relation.Binary.Definitions using (Symmetric; Decidable) private - variable d k m n p : ℕ + variable d m n o p : ℕ open ≤-Reasoning @@ -88,11 +88,11 @@ coprime? m n with mkGCD m n -- Nothing except for 1 is coprime to 0. -0-coprimeTo-m⇒m≡1 : ∀ {m} → Coprime 0 m → m ≡ 1 +0-coprimeTo-m⇒m≡1 : Coprime 0 m → m ≡ 1 0-coprimeTo-m⇒m≡1 {m} coprime = coprime (m ∣0 , ∣-refl) -¬0-coprimeTo-2+ : ∀ {n} → ¬ Coprime 0 (2+ n) -¬0-coprimeTo-2+ coprime = contradiction (0-coprimeTo-m⇒m≡1 coprime) λ() +¬0-coprimeTo-2+ : .{{NonTrivial n}} → ¬ Coprime 0 n +¬0-coprimeTo-2+ coprime = contradiction (0-coprimeTo-m⇒m≡1 coprime) nonTrivial⇒≢1 -- If m and n are coprime, then n + m and n are also coprime. @@ -110,7 +110,7 @@ recompute {n} {d} coprime = Nullary.recompute (coprime? n d) coprime -- If the "gcd" in Bézout's identity is non-zero, then the "other" -- divisors are coprime. -Bézout-coprime : .{{_ : NonZero d}} → +Bézout-coprime : .{{NonZero d}} → Bézout.Identity d (m * d) (n * d) → Coprime m n Bézout-coprime {d = suc _} (Bézout.+- x y eq) (divides-refl q₁ , divides-refl q₂) = lem₁₀ y q₂ x q₁ eq @@ -122,17 +122,17 @@ Bézout-coprime {d = suc _} (Bézout.-+ x y eq) (divides-refl q₁ , divides-ref coprime-Bézout : Coprime m n → Bézout.Identity 1 m n coprime-Bézout = Bézout.identity ∘ coprime⇒GCD≡1 --- If i divides jk and is coprime to j, then it divides k. +-- If m divides n*o and is coprime to n, then it divides o. -coprime-divisor : Coprime m n → m ∣ n * k → m ∣ k -coprime-divisor {k = k} c (divides q eq′) with coprime-Bézout c -... | Bézout.+- x y eq = divides (x * k ∸ y * q) (lem₈ x y eq eq′) -... | Bézout.-+ x y eq = divides (y * q ∸ x * k) (lem₉ x y eq eq′) +coprime-divisor : Coprime m n → m ∣ n * o → m ∣ o +coprime-divisor {o = o} c (divides q eq′) with coprime-Bézout c +... | Bézout.+- x y eq = divides (x * o ∸ y * q) (lem₈ x y eq eq′) +... | Bézout.-+ x y eq = divides (y * q ∸ x * o) (lem₉ x y eq eq′) --- If d is a common divisor of mk and nk, and m and n are coprime, --- then d divides k. +-- If d is a common divisor of m*o and n*o, and m and n are coprime, +-- then d divides o. -coprime-factors : Coprime m n → d ∣ m * k × d ∣ n * k → d ∣ k +coprime-factors : Coprime m n → d ∣ m * o × d ∣ n * o → d ∣ o coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout c ... | Bézout.+- x y eq = divides (x * q₁ ∸ y * q₂) (lem₁₁ x y eq eq₁ eq₂) ... | Bézout.-+ x y eq = divides (y * q₂ ∸ x * q₁) (lem₁₁ y x eq eq₂ eq₁) @@ -140,12 +140,7 @@ coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout ------------------------------------------------------------------------ -- Primality implies coprimality. -prime⇒coprime≢0 : Prime p → .{{_ : NonZero n}} → n < p → Coprime p n -prime⇒coprime≢0 p n

Date: Mon, 6 Nov 2023 11:24:15 +0000 Subject: [PATCH 47/78] removed `recomputable` in favour of a private lemma --- src/Data/Nat/Base.agda | 3 --- src/Data/Nat/Primality.agda | 3 +++ 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 57a90be651..fe4d5a370c 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -155,9 +155,6 @@ instance n>1⇒nonTrivial : ∀ {n} → n > 1 → NonTrivial n n>1⇒nonTrivial 1<2+n = _ -recompute-nonTrivial : ∀ {n} → .⦃ NonTrivial n ⦄ → NonTrivial n -recompute-nonTrivial {2+ _} = _ - -- Destructors nonTrivial⇒nonZero : ∀ {n} → .⦃ NonTrivial n ⦄ → NonZero n diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 413d804fd8..057ab5be1e 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -31,6 +31,9 @@ private nt[2] : NonTrivial 2 nt[2] = nonTrivial {0} + recompute-nonTrivial : ∀ {n} → .{{NonTrivial n}} → NonTrivial n + recompute-nonTrivial {n} {{nontrivial}} = Dec.recompute (nonTrivial? n) nontrivial + ------------------------------------------------------------------------ -- Definitions From d8d26eebd4e46431dd43a3dffea3d9f1108d2d0d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 6 Nov 2023 11:57:58 +0000 Subject: [PATCH 48/78] regularised use of instance brackets --- src/Data/Nat/Primality.agda | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 057ab5be1e..08d970b180 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -93,7 +93,7 @@ private CompositeUpTo⇔Composite = mk⇔ comp-upto⇒comp comp⇒comp-upto where comp-upto⇒comp : CompositeUpTo n → Composite n - comp-upto⇒comp (_ , d 1 is m-rough, then m ≤ n -rough⇒≤ : .⦃ NonTrivial n ⦄ → Rough m n → m ≤ n +rough⇒≤ : .{{NonTrivial n}} → Rough m n → m ≤ n rough⇒≤ rough = ≮⇒≥ λ m>n → rough (hasBoundedNonTrivialDivisor m>n ∣-refl) -- If a number n is m-rough, and m ∤ n, then n is (suc m)-rough @@ -208,7 +208,7 @@ rough⇒∣⇒rough r n∣o hbntd = r (hasBoundedNonTrivialDivisor-∣ hbntd n -- Corollary: relationship between roughness and primality -- If a number n is p-rough, and p > 1 divides n, then p must be prime -rough⇒∣⇒prime : .⦃ NonTrivial p ⦄ → Rough p n → p ∣ n → Prime p +rough⇒∣⇒prime : .{{NonTrivial p}} → Rough p n → p ∣ n → Prime p rough⇒∣⇒prime r p∣n = prime (rough⇒∣⇒rough r p∣n) ------------------------------------------------------------------------ @@ -338,14 +338,14 @@ private composite⇒¬prime : Composite n → ¬ Prime n composite⇒¬prime composite[d] (prime p) = p composite[d] -¬composite⇒prime : .⦃ NonTrivial n ⦄ → ¬ Composite n → Prime n +¬composite⇒prime : .{{NonTrivial n}} → ¬ Composite n → Prime n ¬composite⇒prime = prime prime⇒¬composite : Prime n → ¬ Composite n prime⇒¬composite (prime p) = p -- note that this has to recompute the factor! -¬prime⇒composite : .⦃ NonTrivial n ⦄ → ¬ Prime n → Composite n +¬prime⇒composite : .{{NonTrivial n}} → ¬ Prime n → Composite n ¬prime⇒composite {n} ¬prime[n] = decidable-stable (composite? n) (¬prime[n] ∘′ ¬composite⇒prime) @@ -358,7 +358,7 @@ prime⇒irreducible pp@(prime pr) {m@(2+ _)} m∣p = inj₂ (≤∧≮⇒≡ (∣⇒≤ m∣p) λ m

Date: Mon, 6 Nov 2023 12:32:48 +0000 Subject: [PATCH 49/78] made instances more explicit --- src/Data/Nat/Coprimality.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index 1d04513ea9..384a9c6e37 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -92,7 +92,7 @@ coprime? m n with mkGCD m n 0-coprimeTo-m⇒m≡1 {m} coprime = coprime (m ∣0 , ∣-refl) ¬0-coprimeTo-2+ : .{{NonTrivial n}} → ¬ Coprime 0 n -¬0-coprimeTo-2+ coprime = contradiction (0-coprimeTo-m⇒m≡1 coprime) nonTrivial⇒≢1 +¬0-coprimeTo-2+ {n} coprime = contradiction (0-coprimeTo-m⇒m≡1 coprime) (nonTrivial⇒≢1 {n}) -- If m and n are coprime, then n + m and n are also coprime. From b14229313d4e55f016ef74b8933ec064083767fd Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 6 Nov 2023 12:33:06 +0000 Subject: [PATCH 50/78] made instances more explicit --- src/Data/Rational/Base.agda | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Data/Rational/Base.agda b/src/Data/Rational/Base.agda index 1e49894eb6..0948447163 100644 --- a/src/Data/Rational/Base.agda +++ b/src/Data/Rational/Base.agda @@ -16,7 +16,7 @@ open import Data.Integer.Base as ℤ open import Data.Nat.GCD open import Data.Nat.Coprimality as C using (Coprime; Bézout-coprime; coprime-/gcd; coprime?; ¬0-coprimeTo-2+) -open import Data.Nat.Base as ℕ using (ℕ; zero; suc) hiding (module ℕ) +open import Data.Nat.Base as ℕ using (ℕ; zero; suc; 2+) hiding (module ℕ) open import Data.Rational.Unnormalised.Base as ℚᵘ using (ℚᵘ; mkℚᵘ) open import Data.Sum.Base using (inj₂) open import Function.Base using (id) @@ -189,10 +189,11 @@ open ℤ public -- Constructors ≢-nonZero : ∀ {p} → p ≢ 0ℚ → NonZero p -≢-nonZero {mkℚ -[1+ _ ] _ _} _ = _ -≢-nonZero {mkℚ +[1+ _ ] _ _} _ = _ -≢-nonZero {mkℚ +0 zero _} p≢0 = contradiction refl p≢0 -≢-nonZero {mkℚ +0 (suc d) c} p≢0 = contradiction (λ {i} → C.recompute c {i}) ¬0-coprimeTo-2+ +≢-nonZero {mkℚ -[1+ _ ] _ _} _ = _ +≢-nonZero {mkℚ +[1+ _ ] _ _} _ = _ +≢-nonZero {mkℚ +0 zero _} p≢0 = contradiction refl p≢0 +≢-nonZero {mkℚ +0 d@(suc m) c} p≢0 = + contradiction (λ {d} → C.recompute c {d}) (¬0-coprimeTo-2+ {{ℕ.nonTrivial {m}}}) >-nonZero : ∀ {p} → p > 0ℚ → NonZero p >-nonZero {p@(mkℚ _ _ _)} (*<* p-nonZero {toℚᵘ p} (ℚᵘ.*<* p Date: Mon, 6 Nov 2023 13:38:41 +0000 Subject: [PATCH 51/78] blank line --- src/Data/Nat/Primality.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 08d970b180..254c2afaa0 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -27,6 +27,7 @@ open import Relation.Binary.PropositionalEquality private variable d m n o p : ℕ + instance nt[2] : NonTrivial 2 nt[2] = nonTrivial {0} From 698d53fd211521552e794e93d887516900d3ac3b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 6 Nov 2023 13:54:10 +0000 Subject: [PATCH 52/78] =?UTF-8?q?made=20`nonTrivial=E2=87=92nonZero`=20tak?= =?UTF-8?q?e=20an=20explicit=20argument=20in=20lieu=20of=20being=20able=20?= =?UTF-8?q?to=20make=20it=20an=20`instance`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Nat/Base.agda | 4 ++-- src/Data/Nat/Primality.agda | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index fe4d5a370c..5c0ee70410 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -157,8 +157,8 @@ n>1⇒nonTrivial 1<2+n = _ -- Destructors -nonTrivial⇒nonZero : ∀ {n} → .⦃ NonTrivial n ⦄ → NonZero n -nonTrivial⇒nonZero {n = 2+ k} = _ +nonTrivial⇒nonZero : ∀ n → .⦃ NonTrivial n ⦄ → NonZero n +nonTrivial⇒nonZero (2+ _) = _ nonTrivial⇒n>1 : ∀ n → .⦃ NonTrivial n ⦄ → n > 1 nonTrivial⇒n>1 (2+ _) = 1<2+n diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 254c2afaa0..85a5765173 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -273,7 +273,7 @@ composite⇒nonZero : Composite n → NonZero n composite⇒nonZero {suc _} _ = _ prime⇒nonZero : Prime p → NonZero p -prime⇒nonZero (prime _) = nonTrivial⇒nonZero +prime⇒nonZero _ = nonTrivial⇒nonZero _ irreducible⇒nonZero : Irreducible n → NonZero n irreducible⇒nonZero {zero} = flip contradiction ¬irreducible[0] From 4a1c53e338dacc29c77c2936a6436635c433ada5 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 6 Nov 2023 14:20:44 +0000 Subject: [PATCH 53/78] regularised use of instance brackets --- CHANGELOG.md | 42 ++++++++++++++++++------------------- src/Data/Nat/Primality.agda | 2 +- 2 files changed, 22 insertions(+), 22 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 428b8586c9..322c2102de 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2738,11 +2738,11 @@ Additions to existing modules NonTrivial : Pred ℕ 0ℓ instance nonTrivial : NonTrivial (2+ n) n>1⇒nonTrivial : 1 < n → NonTrivial n - nonZero⇒≢1⇒nonTrivial : .⦃ NonZero n ⦄ → n ≢ 1 → NonTrivial n - recompute-nonTrivial : .⦃ NonTrivial n ⦄ → NonTrivial n - nonTrivial⇒nonZero : .⦃ NonTrivial n ⦄ → NonZero n - nonTrivial⇒n>1 : .⦃ NonTrivial n ⦄ → 1 < n - nonTrivial⇒≢1 : .⦃ NonTrivial n ⦄ → n ≢ 1 + nonZero⇒≢1⇒nonTrivial : .{{NonZero n}} → n ≢ 1 → NonTrivial n + recompute-nonTrivial : .{{NonTrivial n}} → NonTrivial n + nonTrivial⇒nonZero : .{{NonTrivial n}} → NonZero n + nonTrivial⇒n>1 : .{{NonTrivial n}} → 1 < n + nonTrivial⇒≢1 : .{{NonTrivial n}} → n ≢ 1 _⊔′_ : ℕ → ℕ → ℕ _⊓′_ : ℕ → ℕ → ℕ @@ -2814,7 +2814,7 @@ Additions to existing modules m<1+n⇒m Date: Mon, 6 Nov 2023 18:02:16 +0000 Subject: [PATCH 54/78] regularised use of instance brackets --- src/Data/Nat/Base.agda | 8 ++++---- src/Data/Nat/Primality.agda | 4 ++-- src/Data/Nat/Properties.agda | 2 +- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 5c0ee70410..974dc59033 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -157,14 +157,14 @@ n>1⇒nonTrivial 1<2+n = _ -- Destructors -nonTrivial⇒nonZero : ∀ n → .⦃ NonTrivial n ⦄ → NonZero n +nonTrivial⇒nonZero : ∀ n → .{{NonTrivial n}} → NonZero n nonTrivial⇒nonZero (2+ _) = _ -nonTrivial⇒n>1 : ∀ n → .⦃ NonTrivial n ⦄ → n > 1 +nonTrivial⇒n>1 : ∀ n → .{{NonTrivial n}} → n > 1 nonTrivial⇒n>1 (2+ _) = 1<2+n -nonTrivial⇒≢1 : ∀ {n} → .⦃ NonTrivial n ⦄ → n ≢ 1 -nonTrivial⇒≢1 ⦃()⦄ refl +nonTrivial⇒≢1 : ∀ {n} → .{{NonTrivial n}} → n ≢ 1 +nonTrivial⇒≢1 {{()}} refl ------------------------------------------------------------------------ -- Raw bundles diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 6aa311bf0d..6cf0eb17a2 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -186,10 +186,10 @@ rough-1 _ (hasBoundedNonTrivialDivisor _ d∣1) = contradiction (∣1⇒≡1 d 0-rough (hasBoundedNonTrivialDivisor () _) 1-rough : Rough 1 n -1-rough (hasBoundedNonTrivialDivisor ⦃()⦄ z 1 is m-rough, then m ≤ n rough⇒≤ : .{{NonTrivial n}} → Rough m n → m ≤ n diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 58a50f6929..9df927064a 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -1725,7 +1725,7 @@ pred-mono-≤ : pred Preserves _≤_ ⟶ _≤_ pred-mono-≤ {zero} _ = z≤n pred-mono-≤ {suc _} {suc _} m≤n = s≤s⁻¹ m≤n -pred-mono-< : .⦃ _ : NonZero m ⦄ → m < n → pred m < pred n +pred-mono-< : .{{NonZero m}} → m < n → pred m < pred n pred-mono-< {m = suc _} {n = suc _} = s Date: Wed, 8 Nov 2023 15:31:28 +0000 Subject: [PATCH 55/78] trimming --- src/Data/Nat/Primality.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 6cf0eb17a2..190fba11ea 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -32,7 +32,7 @@ private nt[2] : NonTrivial 2 nt[2] = nonTrivial {0} - recompute-nonTrivial : ∀ {n} → .{{NonTrivial n}} → NonTrivial n + recompute-nonTrivial : .{{NonTrivial n}} → NonTrivial n recompute-nonTrivial {n} {{nontrivial}} = Dec.recompute (nonTrivial? n) nontrivial ------------------------------------------------------------------------ From ee466704398512c59ade3726728eb42f3b19cba4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 15 Nov 2023 04:10:29 +0000 Subject: [PATCH 56/78] tidied up `Coprimality` entries --- CHANGELOG.md | 5 ----- 1 file changed, 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 322c2102de..e74bb984b8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2769,11 +2769,6 @@ Additions to existing modules <-asym : Asymmetric _<_ ``` -* Added a new definition to `Data.Nat.Coprimality`: - ```agda - prime⇒coprime≢0 : Prime p → .{{_ : NonZero n}} → n < p → Coprime p n - ``` - * Added a new pattern synonym to `Data.Nat.Divisibility.Core`: ```agda pattern divides-refl q = divides q refl From f87fdcc9c6bc68dca3ed605119dd38dd277e880d Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 16 Nov 2023 13:28:03 +0900 Subject: [PATCH 57/78] Make HasBoundedNonTrivialDivisor infix --- src/Data/Nat/Primality.agda | 66 ++++++++++++++++++------------------- 1 file changed, 33 insertions(+), 33 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 190fba11ea..ab0b969315 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -56,8 +56,8 @@ private -- Definition of having a non-trivial divisor below a given bound -record HasBoundedNonTrivialDivisor (m n : ℕ) : Set where - constructor hasBoundedNonTrivialDivisor +record _HasNonTrivialDivisorLessThan_ (m n : ℕ) : Set where + constructor hasNonTrivialDivisorLessThan field {divisor} : ℕ .{{nontrivial}} : NonTrivial divisor @@ -66,21 +66,21 @@ record HasBoundedNonTrivialDivisor (m n : ℕ) : Set where -- smart constructors -hasBoundedNonTrivialDivisor-≢ : .{{NonTrivial d}} → .{{NonZero n}} → +hasNonTrivialDivisorLessThan-≢ : .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → - HasBoundedNonTrivialDivisor n n -hasBoundedNonTrivialDivisor-≢ d≢n d∣n - = hasBoundedNonTrivialDivisor (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n + n HasNonTrivialDivisorLessThan n +hasNonTrivialDivisorLessThan-≢ d≢n d∣n + = hasNonTrivialDivisorLessThan (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n -hasBoundedNonTrivialDivisor-∣ : HasBoundedNonTrivialDivisor m n → n ∣ o → - HasBoundedNonTrivialDivisor m o -hasBoundedNonTrivialDivisor-∣ (hasBoundedNonTrivialDivisor d1⇒m*n>1 q d _ = m*n≢0⇒m≢0 q @@ -117,7 +117,7 @@ composite-∣ (hasBoundedNonTrivialDivisor {d} d 1 is m-rough, then m ≤ n rough⇒≤ : .{{NonTrivial n}} → Rough m n → m ≤ n -rough⇒≤ rough = ≮⇒≥ λ m>n → rough (hasBoundedNonTrivialDivisor m>n ∣-refl) +rough⇒≤ rough = ≮⇒≥ λ m>n → rough (hasNonTrivialDivisorLessThan m>n ∣-refl) -- If a number n is m-rough, and m ∤ n, then n is (suc m)-rough ∤⇒rough-suc : m ∤ n → Rough m n → Rough (suc m) n -∤⇒rough-suc m∤n r (hasBoundedNonTrivialDivisor d<1+m d∣n) with m<1+n⇒m Date: Thu, 16 Nov 2023 13:42:21 +0900 Subject: [PATCH 58/78] Make NonTrivial into a record to fix instance resolution bug --- src/Data/Nat/Base.agda | 32 ++++++++++++++++++-------------- src/Data/Nat/Primality.agda | 4 ---- 2 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index 974dc59033..ed05804550 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -78,7 +78,7 @@ s b ------------------------------------------------------------------------ -- Simple predicates --- Defining `NonZero` in terms of `T` and therefore ultimately `⊤` and --- `⊥` allows Agda to automatically infer nonZero-ness for any natural --- of the form `suc n`. Consequently in many circumstances this --- eliminates the need to explicitly pass a proof when the NonZero --- argument is either an implicit or an instance argument. +-- Defining these predicates in terms of `T` and therefore ultimately +-- `⊤` and `⊥` allows Agda to automatically infer them for any natural +-- of the correct form. Consequently in many circumstances this +-- eliminates the need to explicitly pass a proof when the predicate +-- argument is either an implicit or an instance argument. See `_/_` +-- and `_%_` further down this file for examples. -- --- See `Data.Nat.DivMod` for an example. +-- Furthermore, defining these predicates as single-field records +-- (rather defining them directly as the type of their field) is +-- necessary as the current version of Agda is far better at +-- reconstructing meta-variable values for the record parameters. + +-- A predicate saying that a number is not equal to 0. record NonZero (n : ℕ) : Set where field @@ -138,13 +144,11 @@ instance -- The property of being a non-zero, non-unit -NonTrivial : Pred ℕ 0ℓ -NonTrivial = T ∘ not ∘ trivial - where - trivial : ℕ → Bool - trivial 0 = true - trivial 1 = true - trivial (2+ _) = false +record NonTrivial (n : ℕ) : Set where + field + nonTrivial : T (1 <ᵇ n) + +-- Instances instance nonTrivial : ∀ {n} → NonTrivial (2+ n) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index ab0b969315..0ae4dc7081 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -28,10 +28,6 @@ private variable d m n o p : ℕ - instance - nt[2] : NonTrivial 2 - nt[2] = nonTrivial {0} - recompute-nonTrivial : .{{NonTrivial n}} → NonTrivial n recompute-nonTrivial {n} {{nontrivial}} = Dec.recompute (nonTrivial? n) nontrivial From 4cc0687e4c2ccfa3e771ed0b01639fe95094075d Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 16 Nov 2023 14:15:58 +0900 Subject: [PATCH 59/78] Move HasNonTrivialDivisor to Divisibility.Core and hide UpTo lemmas --- src/Data/Nat/Divisibility.agda | 14 +++++++++ src/Data/Nat/Divisibility/Core.agda | 21 ++++++++++--- src/Data/Nat/Primality.agda | 49 +++++++---------------------- 3 files changed, 43 insertions(+), 41 deletions(-) diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index bb30716e01..c9093dfefc 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -308,3 +308,17 @@ 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 _HasNonTrivialDivisorLessThan_ + +hasNonTrivialDivisorLessThan-≢ : ∀ {d n} → .{{NonTrivial d}} → .{{NonZero n}} → + d ≢ n → d ∣ n → + n HasNonTrivialDivisorLessThan n +hasNonTrivialDivisorLessThan-≢ d≢n d∣n + = hasNonTrivialDivisorLessThan (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n + +hasNonTrivialDivisorLessThan-∣ : ∀ {m n o} → m HasNonTrivialDivisorLessThan n → n ∣ o → + m HasNonTrivialDivisorLessThan o +hasNonTrivialDivisorLessThan-∣ (hasNonTrivialDivisorLessThan d Date: Thu, 16 Nov 2023 14:27:28 +0900 Subject: [PATCH 60/78] Rearrange file to follow standard ordering of lemmas in the rest of the library --- src/Data/Nat/Primality.agda | 368 ++++++++++++++++++------------------ 1 file changed, 188 insertions(+), 180 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 32af28855d..93344e5db9 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -33,24 +33,72 @@ private ------------------------------------------------------------------------ -- Definitions +------------------------------------------------------------------------ + +-- The definitions of `Prime` and `Composite` in this module are +-- intended to be built up as complementary pairs of `Decidable` +-- predicates, with `Prime` given *negatively* as the universal closure +-- of the negation of `Composite`, where this is given *positively* as +-- an existential witnessing a non-trivial divisor, where such +-- quantification is proxied by an explicit `record` type. + +-- For technical reasons, in order to be able to prove decidability via +-- the `all?` and `any?` combinators for *bounded* predicates on ℕ, we +-- further define the bounded counterparts to predicates `P...` as +-- `P...UpTo` and show the equivalence of the two. + +-- Finally, the definitions of the predicates `Composite` and `Prime` +-- as the 'diagonal' instances of relations involving such bounds on +-- the possible non-trivial divisors leads to the following +-- positive/existential predicate as the basis for the whole development. + +------------------------------------------------------------------------ +-- Roughness + +-- Definition of 'rough': a number is m-rough if all its non-trivial +-- divisors are bounded below by m. + +Rough : ℕ → Pred ℕ _ +Rough m n = ¬ (m HasNonTrivialDivisorLessThan n) + +------------------------------------------------------------------------ +-- Primality + +-- Definition of Prime as the diagonal of Rough (and hence the +-- complement of Composite below). + +-- Constructor `prime` takes a proof isPrime that NonTrivial p is p-Rough +-- and thereby enforces that: +-- * p is a fortiori NonZero and NonUnit +-- * any non-trivial divisor of p must be at least p, ie p itself --- The definitions of `Prime` and `Composite` in this module are intended to --- be built up as complementary pairs of `Decidable` predicates, with `Prime` --- given *negatively* as the universal closure of the negation of `Composite`, --- where this is given *positively* as an existential witnessing a non-trivial --- divisor, where such quantification is proxied by an explicit `record` type. +record Prime (p : ℕ) : Set where + constructor prime + field + .{{nontrivial}} : NonTrivial p + isPrime : Rough p p --- For technical reasons, in order to be able to prove decidability via the --- `all?` and `any?` combinators for *bounded* predicates on ℕ, we further --- define the bounded counterparts to predicates `P...` as `P...UpTo` and show --- the equivalence of the two. +-- equivalent bounded predicate definition; proof of equivalence + +private + PrimeUpTo : Pred ℕ _ + PrimeUpTo n = ∀ {d} → d < n → NonTrivial d → d ∤ n + + PrimeUpTo⇔Prime : .{{NonTrivial n}} → PrimeUpTo n ⇔ Prime n + PrimeUpTo⇔Prime = mk⇔ prime-upto⇒prime prime⇒prime-upto + where + prime-upto⇒prime : .{{NonTrivial n}} → PrimeUpTo n → Prime n + prime-upto⇒prime upto = prime + λ (hasNonTrivialDivisorLessThan d1⇒m*n>1 q d _ = m*n≢0⇒m≢0 q --- Definition of 'rough': a number is m-rough --- if all its non-trivial divisors d are bounded below by m - -Rough : ℕ → Pred ℕ _ -Rough m n = ¬ (m HasNonTrivialDivisorLessThan n) - --- Definition of Prime as the complement of Composite, via diagonal of Rough - --- Constructor `prime` takes a proof isPrime that NonTrivial p is p-Rough --- and thereby enforces that: --- * p is a fortiori NonZero and NonUnit --- * any non-trivial divisor of p must be at least p, ie p itself - -record Prime (p : ℕ) : Set where - constructor prime - field - .{{nontrivial}} : NonTrivial p - isPrime : Rough p p - --- equivalent bounded predicate definition; proof of equivalence - -private - PrimeUpTo : Pred ℕ _ - PrimeUpTo n = ∀ {d} → d < n → NonTrivial d → d ∤ n - - PrimeUpTo⇔Prime : .{{NonTrivial n}} → PrimeUpTo n ⇔ Prime n - PrimeUpTo⇔Prime = mk⇔ prime-upto⇒prime prime⇒prime-upto - where - prime-upto⇒prime : .{{NonTrivial n}} → PrimeUpTo n → Prime n - prime-upto⇒prime upto = prime - λ (hasNonTrivialDivisorLessThan dn → rough (hasNonTrivialDivisorLessThan m>n rough⇒∣⇒rough : Rough m o → n ∣ o → Rough m n rough⇒∣⇒rough r n∣o hbntd = r (hasNonTrivialDivisorLessThan-∣ hbntd n∣o) ------------------------------------------------------------------------- --- Corollary: relationship between roughness and primality - --- If a number n is p-rough, and p > 1 divides n, then p must be prime -rough⇒∣⇒prime : .{{NonTrivial p}} → Rough p n → p ∣ n → Prime p -rough⇒∣⇒prime r p∣n = prime (rough⇒∣⇒rough r p∣n) ------------------------------------------------------------------------ --- Basic (counter-)examples of Composite - -¬composite[0] : ¬ Composite 0 -¬composite[0] composite[0] = 0-rough composite[0] - -¬composite[1] : ¬ Composite 1 -¬composite[1] composite[1] = 1-rough composite[1] - -composite[4] : Composite 4 -composite[4] = composite-≢ 2 (λ()) (divides-refl 2) - -composite[6] : Composite 6 -composite[6] = composite-≢ 3 (λ()) (divides-refl 2) +-- Prime - ------------------------------------------------------------------------- --- Basic (counter-)examples of Prime +-- Basic (counter-)examples ¬prime[0] : ¬ Prime 0 ¬prime[0] () @@ -213,55 +212,17 @@ composite[6] = composite-≢ 3 (λ()) (divides-refl 2) prime[2] : Prime 2 prime[2] = prime 2-rough ------------------------------------------------------------------------- --- Basic (counter-)examples of Irreducible - -¬irreducible[0] : ¬ Irreducible 0 -¬irreducible[0] irr[0] = [ (λ ()) , (λ ()) ]′ (irr[0] {2} (divides-refl 0)) - -irreducible[1] : Irreducible 1 -irreducible[1] m|1 = inj₁ (∣1⇒≡1 m|1) - -irreducible[2] : Irreducible 2 -irreducible[2] {zero} 0∣2 with () ← 0∣⇒≡0 0∣2 -irreducible[2] {suc _} d∣2 with ∣⇒≤ d∣2 -... | z 1 divides n, then p must be prime +rough⇒∣⇒prime : .{{NonTrivial p}} → Rough p n → p ∣ n → Prime p +rough⇒∣⇒prime r p∣n = prime (rough⇒∣⇒rough r p∣n) prime⇒nonZero : Prime p → NonZero p prime⇒nonZero _ = nonTrivial⇒nonZero _ -irreducible⇒nonZero : Irreducible n → NonZero n -irreducible⇒nonZero {zero} = flip contradiction ¬irreducible[0] -irreducible⇒nonZero {suc _} _ = _ - - ------------------------------------------------------------------------- --- Decidability +prime⇒nonTrivial : Prime p → NonTrivial p +prime⇒nonTrivial _ = recompute-nonTrivial -composite? : Decidable Composite -composite? n = Dec.map (CompositeUpTo⇔Composite {n}) (compositeUpTo? n) - where - compositeUpTo? : Decidable CompositeUpTo - compositeUpTo? n = anyUpTo? (λ d → nonTrivial? d ×-dec d ∣? n) n - prime? : Decidable Prime prime? 0 = no ¬prime[0] prime? 1 = no ¬prime[1] @@ -270,70 +231,6 @@ prime? n@(2+ _) = Dec.map PrimeUpTo⇔Prime (primeUpTo? n) primeUpTo? : Decidable PrimeUpTo primeUpTo? n = allUpTo? (λ d → nonTrivial? d →-dec ¬? (d ∣? n)) n -irreducible? : Decidable Irreducible -irreducible? zero = no ¬irreducible[0] -irreducible? n@(suc _) = Dec.map (IrreducibleUpTo⇔Irreducible {n}) (irreducibleUpTo? n) - where - irreducibleUpTo? : Decidable IrreducibleUpTo - irreducibleUpTo? n = allUpTo? (λ m → (m ∣? n) →-dec (m ≟ 1 ⊎-dec m ≟ n)) n - --- Examples --- --- Once we have the above decision procedures, then instead of constructing proofs --- of eg Prime-ness by hand, we call the appropriate function, and use the witness --- extraction functions `from-yes`, `from-no` to return the checked proofs - -private - - -- Example: 2 is prime, but not-composite. - 2-is-prime : Prime 2 - 2-is-prime = from-yes (prime? 2) - - 2-is-not-composite : ¬ Composite 2 - 2-is-not-composite = from-no (composite? 2) - - - -- Example: 4 and 6 are composite, hence not-prime - 4-is-composite : Composite 4 - 4-is-composite = from-yes (composite? 4) - - 4-is-not-prime : ¬ Prime 4 - 4-is-not-prime = from-no (prime? 4) - - 6-is-composite : Composite 6 - 6-is-composite = from-yes (composite? 6) - - 6-is-not-prime : ¬ Prime 6 - 6-is-not-prime = from-no (prime? 6) - ------------------------------------------------------------------------- --- Relationships between compositeness, primality, and irreducibility - -composite⇒¬prime : Composite n → ¬ Prime n -composite⇒¬prime composite[d] (prime p) = p composite[d] - -¬composite⇒prime : .{{NonTrivial n}} → ¬ Composite n → Prime n -¬composite⇒prime = prime - -prime⇒¬composite : Prime n → ¬ Composite n -prime⇒¬composite (prime p) = p - --- note that this has to recompute the factor! -¬prime⇒composite : .{{NonTrivial n}} → ¬ Prime n → Composite n -¬prime⇒composite {n} ¬prime[n] = - decidable-stable (composite? n) (¬prime[n] ∘′ ¬composite⇒prime) - -prime⇒irreducible : Prime p → Irreducible p -prime⇒irreducible pp@(prime _) {0} 0∣p - = contradiction (0∣⇒≡0 0∣p) (≢-nonZero⁻¹ _ {{prime⇒nonZero pp}}) -prime⇒irreducible _ {1} 1∣p = inj₁ refl -prime⇒irreducible pp@(prime pr) {m@(2+ _)} m∣p - = inj₂ (≤∧≮⇒≡ (∣⇒≤ {{prime⇒nonZero pp}} m∣p) λ m

Date: Thu, 16 Nov 2023 14:46:46 +0900 Subject: [PATCH 61/78] Move UpTo predicates into decidability proofs --- src/Data/Nat/Primality.agda | 168 +++++++++++++++++------------------- 1 file changed, 79 insertions(+), 89 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 93344e5db9..a961f001dd 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -42,12 +42,7 @@ private -- an existential witnessing a non-trivial divisor, where such -- quantification is proxied by an explicit `record` type. --- For technical reasons, in order to be able to prove decidability via --- the `all?` and `any?` combinators for *bounded* predicates on ℕ, we --- further define the bounded counterparts to predicates `P...` as --- `P...UpTo` and show the equivalence of the two. - --- Finally, the definitions of the predicates `Composite` and `Prime` +-- The definitions of the predicates `Composite` and `Prime` -- as the 'diagonal' instances of relations involving such bounds on -- the possible non-trivial divisors leads to the following -- positive/existential predicate as the basis for the whole development. @@ -55,22 +50,19 @@ private ------------------------------------------------------------------------ -- Roughness --- Definition of 'rough': a number is m-rough if all its non-trivial --- divisors are bounded below by m. - +-- A number is m-rough if all its non-trivial divisors are bounded below +-- by m. Rough : ℕ → Pred ℕ _ Rough m n = ¬ (m HasNonTrivialDivisorLessThan n) ------------------------------------------------------------------------ -- Primality --- Definition of Prime as the diagonal of Rough (and hence the --- complement of Composite below). - --- Constructor `prime` takes a proof isPrime that NonTrivial p is p-Rough --- and thereby enforces that: +-- Prime as the diagonal of Rough (and hence the complement of Composite +-- as defined below). The constructor `prime` takes a proof `isPrime` +-- that NonTrivial p is p-Rough and thereby enforces that: -- * p is a fortiori NonZero and NonUnit --- * any non-trivial divisor of p must be at least p, ie p itself +-- * any non-trivial divisor of p must be at least p, i.e. p itself record Prime (p : ℕ) : Set where constructor prime @@ -78,88 +70,19 @@ record Prime (p : ℕ) : Set where .{{nontrivial}} : NonTrivial p isPrime : Rough p p --- equivalent bounded predicate definition; proof of equivalence - -private - PrimeUpTo : Pred ℕ _ - PrimeUpTo n = ∀ {d} → d < n → NonTrivial d → d ∤ n - - PrimeUpTo⇔Prime : .{{NonTrivial n}} → PrimeUpTo n ⇔ Prime n - PrimeUpTo⇔Prime = mk⇔ prime-upto⇒prime prime⇒prime-upto - where - prime-upto⇒prime : .{{NonTrivial n}} → PrimeUpTo n → Prime n - prime-upto⇒prime upto = prime - λ (hasNonTrivialDivisorLessThan d1⇒m*n>1 q d - _ = m*n≢0⇒m≢0 q - ------------------------------------------------------------------------ -- Irreducibility -- Definition of irreducibility: kindergarten version of `Prime` - -Irreducible′ : Rel ℕ _ -Irreducible′ d n = d ∣ n → d ≡ 1 ⊎ d ≡ n - Irreducible : Pred ℕ _ -Irreducible n = ∀ {d} → Irreducible′ d n - --- equivalent bounded predicate definition; proof of equivalence - -private - IrreducibleUpTo : Pred ℕ _ - IrreducibleUpTo n = ∀ {d} → d < n → Irreducible′ d n - - IrreducibleUpTo⇔Irreducible : .{{NonZero n}} → IrreducibleUpTo n ⇔ Irreducible n - IrreducibleUpTo⇔Irreducible = mk⇔ irr-upto⇒irr irr⇒irr-upto - where - irr-upto⇒irr : .{{NonZero n}} → IrreducibleUpTo n → Irreducible n - irr-upto⇒irr irr-upto m∣n - = [ flip irr-upto m∣n , inj₂ ]′ (m≤n⇒mn → rough (hasNonTrivialDivisorLessThan m>n rough⇒∣⇒rough : Rough m o → n ∣ o → Rough m n rough⇒∣⇒rough r n∣o hbntd = r (hasNonTrivialDivisorLessThan-∣ hbntd n∣o) - ------------------------------------------------------------------------ -- Prime @@ -228,6 +150,28 @@ prime? 0 = no ¬prime[0] prime? 1 = no ¬prime[1] prime? n@(2+ _) = Dec.map PrimeUpTo⇔Prime (primeUpTo? n) where + -- For technical reasons, in order to be able to prove decidability via + -- the `all?` and `any?` combinators for *bounded* predicates on ℕ, we + -- further define the bounded counterparts to predicates `P...` as + -- `P...UpTo` and show the equivalence of the two. + + -- An equivalent bounded predicate definition + PrimeUpTo : Pred ℕ _ + PrimeUpTo n = ∀ {d} → d < n → NonTrivial d → d ∤ n + + -- Proof of equvialence + prime⇒prime-upto : Prime n → PrimeUpTo n + prime⇒prime-upto (prime p) {d} d1⇒m*n>1 q d + _ = m*n≢0⇒m≢0 q + -- Basic (counter-)examples of Composite ¬composite[0] : ¬ Composite 0 @@ -305,8 +264,23 @@ composite⇒nonTrivial {1} composite[1] = contradiction composite[1] ¬compos composite⇒nonTrivial {2+ _} _ = _ composite? : Decidable Composite -composite? n = Dec.map (CompositeUpTo⇔Composite {n}) (compositeUpTo? n) +composite? n = Dec.map CompositeUpTo⇔Composite (compositeUpTo? n) where + -- equivalent bounded predicate definition + CompositeUpTo : Pred ℕ _ + CompositeUpTo n = ∃[ d ] d < n × NonTrivial d × d ∣ n + + -- proof of equivalence + comp-upto⇒comp : CompositeUpTo n → Composite n + comp-upto⇒comp (_ , d Date: Thu, 16 Nov 2023 14:59:00 +0900 Subject: [PATCH 62/78] No-op refactoring to curb excessively long lines --- src/Data/Nat/Primality.agda | 81 ++++++++++++++++++++++--------------- 1 file changed, 48 insertions(+), 33 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index a961f001dd..f4058dfe8c 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -18,7 +18,7 @@ open import Function.Base using (flip; _∘_; _∘′_) open import Function.Bundles using (_⇔_; mk⇔) open import Relation.Nullary.Decidable as Dec using (yes; no; from-yes; from-no; ¬?; _×-dec_; _⊎-dec_; _→-dec_; decidable-stable) -open import Relation.Nullary.Negation using (¬_; contradiction) +open import Relation.Nullary.Negation using (¬_; contradiction; contradiction₂) open import Relation.Unary using (Pred; Decidable) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality @@ -29,7 +29,8 @@ private d m n o p : ℕ recompute-nonTrivial : .{{NonTrivial n}} → NonTrivial n - recompute-nonTrivial {n} {{nontrivial}} = Dec.recompute (nonTrivial? n) nontrivial + recompute-nonTrivial {n} {{nontrivial}} = + Dec.recompute (nonTrivial? n) nontrivial ------------------------------------------------------------------------ -- Definitions @@ -93,7 +94,8 @@ Irreducible n = ∀ {d} → d ∣ n → d ≡ 1 ⊎ d ≡ n -- 1 is always n-rough rough-1 : ∀ n → Rough n 1 -rough-1 _ (hasNonTrivialDivisorLessThan _ d∣1) = contradiction (∣1⇒≡1 d∣1) nonTrivial⇒≢1 +rough-1 _ (hasNonTrivialDivisorLessThan _ d∣1) = + contradiction (∣1⇒≡1 d∣1) nonTrivial⇒≢1 -- Any number is 0-, 1- and 2-rough, -- because no non-trivial factor d can be less than 0, 1, or 2 @@ -108,11 +110,13 @@ rough-1 _ (hasNonTrivialDivisorLessThan _ d∣1) = contradiction (∣1⇒≡1 d -- If a number n > 1 is m-rough, then m ≤ n rough⇒≤ : .{{NonTrivial n}} → Rough m n → m ≤ n -rough⇒≤ rough = ≮⇒≥ λ m>n → rough (hasNonTrivialDivisorLessThan m>n ∣-refl) - +rough⇒≤ rough = ≮⇒≥ n≮m + where n≮m = λ m>n → rough (hasNonTrivialDivisorLessThan m>n ∣-refl) + -- If a number n is m-rough, and m ∤ n, then n is (suc m)-rough ∤⇒rough-suc : m ∤ n → Rough m n → Rough (suc m) n -∤⇒rough-suc m∤n r (hasNonTrivialDivisorLessThan d<1+m d∣n) with m<1+n⇒m Date: Thu, 16 Nov 2023 15:08:38 +0900 Subject: [PATCH 63/78] Make a couple of names consistent with style-guide --- src/Data/Nat/Base.agda | 1 - src/Data/Nat/Primality.agda | 11 +++++------ 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda index ed05804550..128c330138 100644 --- a/src/Data/Nat/Base.agda +++ b/src/Data/Nat/Base.agda @@ -16,7 +16,6 @@ open import Algebra.Definitions.RawMagma using (_∣ˡ_) open import Data.Bool.Base using (Bool; true; false; T; not) open import Data.Parity.Base using (Parity; 0ℙ; 1ℙ) open import Data.Product.Base using (_,_) -open import Function.Base using (_∘_) open import Level using (0ℓ) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality.Core diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index f4058dfe8c..cc89176e9c 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -64,7 +64,6 @@ Rough m n = ¬ (m HasNonTrivialDivisorLessThan n) -- that NonTrivial p is p-Rough and thereby enforces that: -- * p is a fortiori NonZero and NonUnit -- * any non-trivial divisor of p must be at least p, i.e. p itself - record Prime (p : ℕ) : Set where constructor prime field @@ -98,7 +97,7 @@ rough-1 _ (hasNonTrivialDivisorLessThan _ d∣1) = contradiction (∣1⇒≡1 d∣1) nonTrivial⇒≢1 -- Any number is 0-, 1- and 2-rough, --- because no non-trivial factor d can be less than 0, 1, or 2 +-- because no non-trivial factor d can be strictly less than 0, 1, or 2 0-rough : Rough 0 n 0-rough (hasNonTrivialDivisorLessThan () _) @@ -121,8 +120,8 @@ rough⇒≤ rough = ≮⇒≥ n≮m ... | inj₂ d≡m@refl = contradiction d∣n m∤n -- If a number is m-rough, then so are all of its divisors -rough⇒∣⇒rough : Rough m o → n ∣ o → Rough m n -rough⇒∣⇒rough r n∣o hbntd = r (hasNonTrivialDivisorLessThan-∣ hbntd n∣o) +rough∧∣⇒rough : Rough m o → n ∣ o → Rough m n +rough∧∣⇒rough r n∣o hbntd = r (hasNonTrivialDivisorLessThan-∣ hbntd n∣o) ------------------------------------------------------------------------ -- Prime @@ -140,8 +139,8 @@ prime[2] = prime 2-rough -- Relationship between roughness and primality. -- If a number n is p-rough, and p > 1 divides n, then p must be prime -rough⇒∣⇒prime : .{{NonTrivial p}} → Rough p n → p ∣ n → Prime p -rough⇒∣⇒prime r p∣n = prime (rough⇒∣⇒rough r p∣n) +rough∧∣⇒prime : .{{NonTrivial p}} → Rough p n → p ∣ n → Prime p +rough∧∣⇒prime r p∣n = prime (rough∧∣⇒rough r p∣n) prime⇒nonZero : Prime p → NonZero p prime⇒nonZero _ = nonTrivial⇒nonZero _ From 92b1e03cadb8538268430ba6e4044edefabc1f34 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 16 Nov 2023 15:08:44 +0000 Subject: [PATCH 64/78] new definition of `Prime` --- CHANGELOG.md | 20 ++++++++++++++++---- src/Data/Nat/Primality.agda | 24 ++++++++++++------------ 2 files changed, 28 insertions(+), 16 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e74bb984b8..a00d39e23d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -645,10 +645,14 @@ Non-backwards compatible changes * To make it easier to use, reason about and read, the definition has been changed to: ```agda - Prime 0 = ⊥ - Prime 1 = ⊥ - Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n + record Prime (p : ℕ) : Set where + constructor prime + field + .{{nontrivial}} : NonTrivial p + notComposite : ¬ Composite p ``` + where `Composite` is now defined as the diagonal of the relation + `Divisibility.Core.HasNonTrivialDivisorLessThan` ### Changes to operation reduction behaviour in `Data.Rational(.Unnormalised)` @@ -2769,9 +2773,17 @@ Additions to existing modules <-asym : Asymmetric _<_ ``` -* Added a new pattern synonym to `Data.Nat.Divisibility.Core`: +* Added a new pattern synonym and a new definition to `Data.Nat.Divisibility.Core`: ```agda pattern divides-refl q = divides q refl + + record _HasNonTrivialDivisorLessThan_ (m n : ℕ) : Set where + constructor hasNonTrivialDivisorLessThan + field + {divisor} : ℕ + .{{nontrivial}} : NonTrivial divisor + divisor-< : divisor < m + divisor-∣ : divisor ∣ n ``` * Added new definitions and proofs to `Data.Nat.Primality`: diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index cc89176e9c..681d69e1ea 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -56,26 +56,26 @@ private Rough : ℕ → Pred ℕ _ Rough m n = ¬ (m HasNonTrivialDivisorLessThan n) +------------------------------------------------------------------------ +-- Compositeness + +-- A number is composite if it has a proper non-trivial divisor. +Composite : Pred ℕ _ +Composite n = n HasNonTrivialDivisorLessThan n + ------------------------------------------------------------------------ -- Primality --- Prime as the diagonal of Rough (and hence the complement of Composite --- as defined below). The constructor `prime` takes a proof `isPrime` --- that NonTrivial p is p-Rough and thereby enforces that: +-- Prime as the complement of Composite (and hence the diagonal of Rough +-- as defined above). The constructor `prime` takes a proof `notComposite` +-- that NonTrivial p is not composite and thereby enforces that: -- * p is a fortiori NonZero and NonUnit --- * any non-trivial divisor of p must be at least p, i.e. p itself +-- * p is p-Rough, i.e. any proper divisor must be at least p, i.e. p itself record Prime (p : ℕ) : Set where constructor prime field .{{nontrivial}} : NonTrivial p - isPrime : Rough p p - ------------------------------------------------------------------------- --- Compositeness - --- A number is composite if it has a proper non-trivial divisor. -Composite : Pred ℕ _ -Composite n = n HasNonTrivialDivisorLessThan n + notComposite : ¬ Composite p ------------------------------------------------------------------------ -- Irreducibility From dd508e27db6868b17b3c2dd5890a17299fe62815 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 16 Nov 2023 15:42:39 +0000 Subject: [PATCH 65/78] renamed fundamental definition --- CHANGELOG.md | 4 +-- src/Data/Nat/Divisibility.agda | 25 +++++++++-------- src/Data/Nat/Divisibility/Core.agda | 4 +-- src/Data/Nat/Primality.agda | 42 ++++++++++++++--------------- 4 files changed, 37 insertions(+), 38 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a00d39e23d..59eb03dcb9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2777,8 +2777,8 @@ Additions to existing modules ```agda pattern divides-refl q = divides q refl - record _HasNonTrivialDivisorLessThan_ (m n : ℕ) : Set where - constructor hasNonTrivialDivisorLessThan + record _BoundedNonTrivialDivisor_ (m n : ℕ) : Set where + constructor boundedNonTrivialDivisor field {divisor} : ℕ .{{nontrivial}} : NonTrivial divisor diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index c9093dfefc..a5239c7ad7 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -12,7 +12,7 @@ open import Algebra open import Data.Nat.Base open import Data.Nat.DivMod open import Data.Nat.Properties -open import Data.Unit.Base using (tt) +--open import Data.Unit.Base using (tt) open import Function.Base using (_∘′_; _$_) open import Function.Bundles using (_⇔_; mk⇔) open import Level using (0ℓ) @@ -310,15 +310,14 @@ m≤n⇒m!∣n! m≤n = help (≤⇒≤′ m≤n) help {m} {suc n} (≤′-step m≤′n) = ∣n⇒∣m*n (suc n) (help m≤′n) ------------------------------------------------------------------------ --- Properties of _HasNonTrivialDivisorLessThan_ - -hasNonTrivialDivisorLessThan-≢ : ∀ {d n} → .{{NonTrivial d}} → .{{NonZero n}} → - d ≢ n → d ∣ n → - n HasNonTrivialDivisorLessThan n -hasNonTrivialDivisorLessThan-≢ d≢n d∣n - = hasNonTrivialDivisorLessThan (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n - -hasNonTrivialDivisorLessThan-∣ : ∀ {m n o} → m HasNonTrivialDivisorLessThan n → n ∣ o → - m HasNonTrivialDivisorLessThan o -hasNonTrivialDivisorLessThan-∣ (hasNonTrivialDivisorLessThan d 1 is m-rough, then m ≤ n rough⇒≤ : .{{NonTrivial n}} → Rough m n → m ≤ n rough⇒≤ rough = ≮⇒≥ n≮m - where n≮m = λ m>n → rough (hasNonTrivialDivisorLessThan m>n ∣-refl) + where n≮m = λ m>n → rough (boundedNonTrivialDivisor m>n ∣-refl) -- If a number n is m-rough, and m ∤ n, then n is (suc m)-rough ∤⇒rough-suc : m ∤ n → Rough m n → Rough (suc m) n -∤⇒rough-suc m∤n r (hasNonTrivialDivisorLessThan d<1+m d∣n) +∤⇒rough-suc m∤n r (boundedNonTrivialDivisor d<1+m d∣n) with m<1+n⇒m1⇒m*n>1 q d _ = m*n≢0⇒m≢0 q @@ -279,10 +279,10 @@ composite? n = Dec.map CompositeUpTo⇔Composite (compositeUpTo? n) -- Proof of equivalence comp-upto⇒comp : CompositeUpTo n → Composite n comp-upto⇒comp (_ , d Date: Thu, 16 Nov 2023 15:44:20 +0000 Subject: [PATCH 66/78] one last reference in `CHANGELOG` --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 59eb03dcb9..96e83bad64 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -652,7 +652,7 @@ Non-backwards compatible changes notComposite : ¬ Composite p ``` where `Composite` is now defined as the diagonal of the relation - `Divisibility.Core.HasNonTrivialDivisorLessThan` + `Divisibility.Core.BoundedNonTrivialDivisor` ### Changes to operation reduction behaviour in `Data.Rational(.Unnormalised)` From 2141011aeb77341872fd6ea0adb5988af214d9f2 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 17 Nov 2023 05:54:25 +0000 Subject: [PATCH 67/78] more better words; one fewer definition --- CHANGELOG.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 96e83bad64..fa566471a0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -652,7 +652,7 @@ Non-backwards compatible changes notComposite : ¬ Composite p ``` where `Composite` is now defined as the diagonal of the relation - `Divisibility.Core.BoundedNonTrivialDivisor` + `Data.Nat.Divisibility.Core.BoundedNonTrivialDivisor` defined below. ### Changes to operation reduction behaviour in `Data.Rational(.Unnormalised)` @@ -2738,7 +2738,6 @@ Additions to existing modules pattern 2+ n = suc (suc n) pattern 1<2+n {n} = s1⇒nonTrivial : 1 < n → NonTrivial n From 1e36fc6290f9bec7dbaa840bc920459cf57b545b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 18 Nov 2023 09:10:00 +0000 Subject: [PATCH 68/78] tidied up `Definitions` section; rejigged order of proofs of properties to reflect definitional order --- src/Data/Nat/Primality.agda | 181 ++++++++++++++++++------------------ 1 file changed, 90 insertions(+), 91 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 8317e1d8f8..a927253dc7 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -36,17 +36,15 @@ private -- Definitions ------------------------------------------------------------------------ --- The definitions of `Prime` and `Composite` in this module are --- intended to be built up as complementary pairs of `Decidable` --- predicates, with `Prime` given *negatively* as the universal closure --- of the negation of `Composite`, where this is given *positively* as --- an existential witnessing a non-trivial divisor, where such --- quantification is proxied by an explicit `record` type. - --- The definitions of the predicates `Composite` and `Prime` --- as the 'diagonal' instances of relations involving such bounds on --- the possible non-trivial divisors leads to the following --- positive/existential predicate as the basis for the whole development. +-- The positive/existential relation `BoundedNonTrivialDivisor` is +-- the basis for the whole development, as it captures the possible +-- non-trivial divisors of a given number; its complement, `Rough`, +-- therefore sets *lower* bounds on any possible such divisors. + +-- The predicate `Composite` is then defined as the 'diagonal' instance +-- of `BoundedNonTrivialDivisor`, while `Prime` is essentially defined as +-- the complement of `Composite`. Finally, `Irreducible` is the positive +-- analogue of `Prime`. ------------------------------------------------------------------------ -- Roughness @@ -80,7 +78,6 @@ record Prime (p : ℕ) : Set where ------------------------------------------------------------------------ -- Irreducibility --- Definition of irreducibility: kindergarten version of `Prime` Irreducible : Pred ℕ _ Irreducible n = ∀ {d} → d ∣ n → d ≡ 1 ⊎ d ≡ n @@ -97,7 +94,7 @@ rough-1 _ (boundedNonTrivialDivisor _ d∣1) = contradiction (∣1⇒≡1 d∣1) nonTrivial⇒≢1 -- Any number is 0-, 1- and 2-rough, --- because no non-trivial factor d can be strictly less than 0, 1, or 2 +-- because no proper divisor d can be strictly less than 0, 1, or 2 0-rough : Rough 0 n 0-rough (boundedNonTrivialDivisor () _) @@ -121,10 +118,79 @@ rough⇒≤ rough = ≮⇒≥ n≮m -- If a number is m-rough, then so are all of its divisors rough∧∣⇒rough : Rough m o → n ∣ o → Rough m n -rough∧∣⇒rough r n∣o hbntd = r (boundedNonTrivialDivisor-∣ hbntd n∣o) +rough∧∣⇒rough r n∣o bntd = r (boundedNonTrivialDivisor-∣ bntd n∣o) + +------------------------------------------------------------------------ +-- Compositeness + +-- Smart constructors + +composite : .{{NonTrivial d}} → d < n → d ∣ n → Composite n +composite {d = d} = boundedNonTrivialDivisor {divisor = d} + +composite-≢ : ∀ d → .{{NonTrivial d}} → .{{NonZero n}} → + d ≢ n → d ∣ n → Composite n +composite-≢ d = boundedNonTrivialDivisor-≢ {d} + +composite-∣ : .{{NonZero n}} → Composite m → m ∣ n → Composite n +composite-∣ (boundedNonTrivialDivisor {d} d1⇒m*n>1 q d + _ = m*n≢0⇒m≢0 q + +-- Basic (counter-)examples of Composite + +¬composite[0] : ¬ Composite 0 +¬composite[0] composite[0] = 0-rough composite[0] + +¬composite[1] : ¬ Composite 1 +¬composite[1] composite[1] = 1-rough composite[1] + +composite[4] : Composite 4 +composite[4] = composite-≢ 2 (λ()) (divides-refl 2) + +composite[6] : Composite 6 +composite[6] = composite-≢ 3 (λ()) (divides-refl 2) + +composite⇒nonZero : Composite n → NonZero n +composite⇒nonZero {suc _} _ = _ + +composite⇒nonTrivial : Composite n → NonTrivial n +composite⇒nonTrivial {1} composite[1] = + contradiction composite[1] ¬composite[1] +composite⇒nonTrivial {2+ _} _ = _ + +composite? : Decidable Composite +composite? n = Dec.map CompositeUpTo⇔Composite (compositeUpTo? n) + where + -- For technical reasons, in order to be able to prove decidability + -- via the `all?` and `any?` combinators for *bounded* predicates on + -- `ℕ`, we further define the bounded counterparts to predicates + -- `P...` as `P...UpTo` and show the equivalence of the two. + + -- Equivalent bounded predicate definition + CompositeUpTo : Pred ℕ _ + CompositeUpTo n = ∃[ d ] d < n × NonTrivial d × d ∣ n + + -- Proof of equivalence + comp-upto⇒comp : CompositeUpTo n → Composite n + comp-upto⇒comp (_ , d 1 divides n, then p must be prime -rough∧∣⇒prime : .{{NonTrivial p}} → Rough p n → p ∣ n → Prime p -rough∧∣⇒prime r p∣n = prime (rough∧∣⇒rough r p∣n) - prime⇒nonZero : Prime p → NonZero p prime⇒nonZero _ = nonTrivial⇒nonZero _ @@ -153,12 +214,7 @@ prime? 0 = no ¬prime[0] prime? 1 = no ¬prime[1] prime? n@(2+ _) = Dec.map PrimeUpTo⇔Prime (primeUpTo? n) where - -- For technical reasons, in order to be able to prove decidability - -- via the `all?` and `any?` combinators for *bounded* predicates on - -- `ℕ`, we further define the bounded counterparts to predicates - -- `P...` as `P...UpTo` and show the equivalence of the two. - - -- An equivalent bounded predicate definition + -- Equivalent bounded predicate definition PrimeUpTo : Pred ℕ _ PrimeUpTo n = ∀ {d} → d < n → NonTrivial d → d ∤ n @@ -228,70 +284,12 @@ euclidsLemma m n {p} pp@(prime pr) p∣m*n = result ... | no d≢p = contradiction (boundedNonTrivialDivisor-≢ d≢p (GCD.gcd∣n g)) pr ------------------------------------------------------------------------- --- Compositeness - --- Smart constructors - -composite : .{{NonTrivial d}} → d < n → d ∣ n → Composite n -composite {d = d} = boundedNonTrivialDivisor {divisor = d} - -composite-≢ : ∀ d → .{{NonTrivial d}} → .{{NonZero n}} → - d ≢ n → d ∣ n → Composite n -composite-≢ d = boundedNonTrivialDivisor-≢ {d} - -composite-∣ : .{{NonZero n}} → Composite m → m ∣ n → Composite n -composite-∣ (boundedNonTrivialDivisor {d} d1⇒m*n>1 q d - _ = m*n≢0⇒m≢0 q - --- Basic (counter-)examples of Composite - -¬composite[0] : ¬ Composite 0 -¬composite[0] composite[0] = 0-rough composite[0] - -¬composite[1] : ¬ Composite 1 -¬composite[1] composite[1] = 1-rough composite[1] - -composite[4] : Composite 4 -composite[4] = composite-≢ 2 (λ()) (divides-refl 2) - -composite[6] : Composite 6 -composite[6] = composite-≢ 3 (λ()) (divides-refl 2) - -composite⇒nonZero : Composite n → NonZero n -composite⇒nonZero {suc _} _ = _ - -composite⇒nonTrivial : Composite n → NonTrivial n -composite⇒nonTrivial {1} composite[1] = - contradiction composite[1] ¬composite[1] -composite⇒nonTrivial {2+ _} _ = _ - -composite? : Decidable Composite -composite? n = Dec.map CompositeUpTo⇔Composite (compositeUpTo? n) - where - -- Equivalent bounded predicate definition - CompositeUpTo : Pred ℕ _ - CompositeUpTo n = ∃[ d ] d < n × NonTrivial d × d ∣ n - - -- Proof of equivalence - comp-upto⇒comp : CompositeUpTo n → Composite n - comp-upto⇒comp (_ , d 1 divides n, then p must be prime +rough∧∣⇒prime : .{{NonTrivial p}} → Rough p n → p ∣ n → Prime p +rough∧∣⇒prime r p∣n = prime (rough∧∣⇒rough r p∣n) +-- Relationship between compositeness and primality. composite⇒¬prime : Composite n → ¬ Prime n composite⇒¬prime composite[d] (prime p) = p composite[d] @@ -352,10 +350,11 @@ irreducible? n@(suc _) = irreducibleUpTo? n = allUpTo? (λ m → (m ∣? n) →-dec (m ≟ 1 ⊎-dec m ≟ n)) n +-- Relationship between primality and irreducibility. prime⇒irreducible : Prime p → Irreducible p -prime⇒irreducible pp@(prime _) {0} 0∣p +prime⇒irreducible pp@(prime _) {0} 0∣p = contradiction (0∣⇒≡0 0∣p) (≢-nonZero⁻¹ _ {{prime⇒nonZero pp}}) -prime⇒irreducible _ {1} 1∣p = inj₁ refl +prime⇒irreducible _ {1} 1∣p = inj₁ refl prime⇒irreducible pp@(prime pr) {m@(2+ _)} m∣p = inj₂ (≤∧≮⇒≡ (∣⇒≤ {{prime⇒nonZero pp}} m∣p) m≮p) where m≮p = λ m

Date: Sat, 18 Nov 2023 09:24:34 +0000 Subject: [PATCH 69/78] =?UTF-8?q?refactored=20proof=20of=20`prime=E2=87=92?= =?UTF-8?q?irreducible`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Nat/Primality.agda | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index a927253dc7..ab1be5157c 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -352,13 +352,16 @@ irreducible? n@(suc _) = -- Relationship between primality and irreducibility. prime⇒irreducible : Prime p → Irreducible p -prime⇒irreducible pp@(prime _) {0} 0∣p - = contradiction (0∣⇒≡0 0∣p) (≢-nonZero⁻¹ _ {{prime⇒nonZero pp}}) -prime⇒irreducible _ {1} 1∣p = inj₁ refl -prime⇒irreducible pp@(prime pr) {m@(2+ _)} m∣p - = inj₂ (≤∧≮⇒≡ (∣⇒≤ {{prime⇒nonZero pp}} m∣p) m≮p) - where m≮p = λ m

Date: Sat, 18 Nov 2023 10:24:10 +0000 Subject: [PATCH 70/78] finishing touches --- CHANGELOG.md | 10 ++++++++++ src/Data/Nat/Divisibility.agda | 14 ++++++++++++-- src/Data/Nat/Primality.agda | 7 +++++-- 3 files changed, 27 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fa566471a0..f586e2ac7d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2785,6 +2785,16 @@ Additions to existing modules divisor-∣ : divisor ∣ n ``` +* Added new proofs to `Data.Nat.Divisibility`: + ```agda + boundedNonTrivialDivisor-≢ : .{{NonTrivial d}} → .{{NonZero n}} → + d ≢ n → d ∣ n → n BoundedNonTrivialDivisor n + boundedNonTrivialDivisor-∣ : m BoundedNonTrivialDivisor n → n ∣ o → + m BoundedNonTrivialDivisor o + boundedNonTrivialDivisor-≤ : m BoundedNonTrivialDivisor n → m ≤ o → + o BoundedNonTrivialDivisor n + ``` + * Added new definitions and proofs to `Data.Nat.Primality`: ```agda Composite : ℕ → Set diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index a5239c7ad7..240c381434 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -12,11 +12,10 @@ open import Algebra open import Data.Nat.Base open import Data.Nat.DivMod open import Data.Nat.Properties ---open import Data.Unit.Base using (tt) open import Function.Base using (_∘′_; _$_) open import Function.Bundles using (_⇔_; mk⇔) open import Level using (0ℓ) -open import Relation.Nullary.Decidable as Dec using (False; yes; no) +open import Relation.Nullary.Decidable as Dec using (yes; no) open import Relation.Nullary.Negation.Core using (contradiction) open import Relation.Binary.Core using (_⇒_) open import Relation.Binary.Bundles using (Preorder; Poset) @@ -312,12 +311,23 @@ m≤n⇒m!∣n! m≤n = help (≤⇒≤′ m≤n) ------------------------------------------------------------------------ -- Properties of _BoundedNonTrivialDivisor_ +-- Smart constructor + boundedNonTrivialDivisor-≢ : ∀ {d n} → .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → n BoundedNonTrivialDivisor n boundedNonTrivialDivisor-≢ d≢n d∣n = boundedNonTrivialDivisor (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n +-- Monotonicity wrt ∣ + boundedNonTrivialDivisor-∣ : ∀ {m n o} → m BoundedNonTrivialDivisor n → n ∣ o → m BoundedNonTrivialDivisor o boundedNonTrivialDivisor-∣ (boundedNonTrivialDivisor d 1 divides n, then p must be prime rough∧∣⇒prime : .{{NonTrivial p}} → Rough p n → p ∣ n → Prime p rough∧∣⇒prime r p∣n = prime (rough∧∣⇒rough r p∣n) From 59eb7c4f5e73064103fc29938802deed4787afee Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 18 Nov 2023 11:15:25 +0000 Subject: [PATCH 71/78] missing lemma from irrelevant instance list --- CHANGELOG.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f586e2ac7d..4cd7f7b38a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3648,8 +3648,9 @@ This is a full list of proofs that have changed form to use irrelevant instance * In `Data.Nat.Coprimality`: ``` - Bézout-coprime : ∀ {i j d} → Bézout.Identity (suc d) (i * suc d) (j * suc d) → Coprime i j - prime⇒coprime : ∀ m → Prime m → ∀ n → 0 < n → n < m → Coprime m n + ¬0-coprimeTo-2+ : ∀ {n} → ¬ Coprime 0 (2 + n) + Bézout-coprime : ∀ {i j d} → Bézout.Identity (suc d) (i * suc d) (j * suc d) → Coprime i j + prime⇒coprime : ∀ m → Prime m → ∀ n → 0 < n → n < m → Coprime m n ``` * In `Data.Nat.Divisibility` From 46a6e48b481c50b3a2e6a3ff438b0c28f28c46af Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 19 Nov 2023 10:05:49 +0000 Subject: [PATCH 72/78] regularised final proof to use `contradiction` --- src/Data/Nat/Coprimality.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda index 384a9c6e37..f385944f50 100644 --- a/src/Data/Nat/Coprimality.agda +++ b/src/Data/Nat/Coprimality.agda @@ -143,4 +143,4 @@ coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout prime⇒coprime : Prime p → .{{NonZero n}} → n < p → Coprime p n prime⇒coprime p n

Date: Sun, 19 Nov 2023 10:06:41 +0000 Subject: [PATCH 73/78] added fixity `infix 10` --- src/Data/Nat/Divisibility/Core.agda | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Data/Nat/Divisibility/Core.agda b/src/Data/Nat/Divisibility/Core.agda index 491b531f91..a64302c4cd 100644 --- a/src/Data/Nat/Divisibility/Core.agda +++ b/src/Data/Nat/Divisibility/Core.agda @@ -49,6 +49,8 @@ pattern divides-refl q = divides q refl -- Relation for having a non-trivial divisor below a given bound. -- Useful when reasoning about primality. +infix 10 _BoundedNonTrivialDivisor_ + record _BoundedNonTrivialDivisor_ (m n : ℕ) : Set where constructor boundedNonTrivialDivisor field From 9537512cf7f83d1236c50f5b1a9a941dc36ef3e4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 19 Nov 2023 10:08:51 +0000 Subject: [PATCH 74/78] added fixity `infix 10`; made `composite` a pattern synonym; knock-on improvements --- src/Data/Nat/Primality.agda | 53 ++++++++++++++++++------------------- 1 file changed, 26 insertions(+), 27 deletions(-) diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index b72cd55f74..09f014638a 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -51,8 +51,10 @@ private -- A number is m-rough if all its non-trivial divisors are bounded below -- by m. -Rough : ℕ → Pred ℕ _ -Rough m n = ¬ (m BoundedNonTrivialDivisor n) +infix 10 _Rough_ + +_Rough_ : ℕ → Pred ℕ _ +m Rough n = ¬ (m BoundedNonTrivialDivisor n) ------------------------------------------------------------------------ -- Compositeness @@ -89,35 +91,35 @@ Irreducible n = ∀ {d} → d ∣ n → d ≡ 1 ⊎ d ≡ n -- Roughness -- 1 is always n-rough -rough-1 : ∀ n → Rough n 1 +rough-1 : ∀ n → n Rough 1 rough-1 _ (boundedNonTrivialDivisor _ d∣1) = contradiction (∣1⇒≡1 d∣1) nonTrivial⇒≢1 -- Any number is 0-, 1- and 2-rough, -- because no proper divisor d can be strictly less than 0, 1, or 2 -0-rough : Rough 0 n +0-rough : 0 Rough n 0-rough (boundedNonTrivialDivisor () _) -1-rough : Rough 1 n +1-rough : 1 Rough n 1-rough (boundedNonTrivialDivisor {{()}} z 1 is m-rough, then m ≤ n -rough⇒≤ : .{{NonTrivial n}} → Rough m n → m ≤ n +rough⇒≤ : .{{NonTrivial n}} → m Rough n → m ≤ n rough⇒≤ rough = ≮⇒≥ n≮m where n≮m = λ m>n → rough (boundedNonTrivialDivisor m>n ∣-refl) -- If a number n is m-rough, and m ∤ n, then n is (suc m)-rough -∤⇒rough-suc : m ∤ n → Rough m n → Rough (suc m) n +∤⇒rough-suc : m ∤ n → m Rough n → (suc m) Rough n ∤⇒rough-suc m∤n r (boundedNonTrivialDivisor d<1+m d∣n) with m<1+n⇒m1⇒m*n>1 q d _ = m*n≢0⇒m≢0 q @@ -175,12 +177,11 @@ composite? n = Dec.map CompositeUpTo⇔Composite (compositeUpTo? n) -- Proof of equivalence comp-upto⇒comp : CompositeUpTo n → Composite n - comp-upto⇒comp (_ , d 1 divides n, then p must be prime -rough∧∣⇒prime : .{{NonTrivial p}} → Rough p n → p ∣ n → Prime p +rough∧∣⇒prime : .{{NonTrivial p}} → p Rough n → p ∣ n → Prime p rough∧∣⇒prime r p∣n = prime (rough∧∣⇒rough r p∣n) -- Relationship between compositeness and primality. @@ -362,13 +362,12 @@ prime⇒irreducible {p} pp@(prime pr) = irr irr {0} 0∣p = contradiction (0∣⇒≡0 0∣p) (≢-nonZero⁻¹ p) irr {1} 1∣p = inj₁ refl irr {2+ _} d∣p = inj₂ (≤∧≮⇒≡ (∣⇒≤ d∣p) d≮p) - where d≮p = λ d

Date: Sun, 19 Nov 2023 10:10:35 +0000 Subject: [PATCH 75/78] comprehensive `CHNAGELOG` entry; whitespace fixes --- CHANGELOG.md | 18 +++++++++++++++--- src/Data/Nat/Divisibility/Core.agda | 2 +- src/Data/Nat/Primality.agda | 8 ++++---- 3 files changed, 20 insertions(+), 8 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4cd7f7b38a..8ee62ae4a0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2776,8 +2776,9 @@ Additions to existing modules ```agda pattern divides-refl q = divides q refl + infix 10 _BoundedNonTrivialDivisor_ record _BoundedNonTrivialDivisor_ (m n : ℕ) : Set where - constructor boundedNonTrivialDivisor + constructor boundedNonTrivialDivisor field {divisor} : ℕ .{{nontrivial}} : NonTrivial divisor @@ -2795,9 +2796,20 @@ Additions to existing modules o BoundedNonTrivialDivisor n ``` -* Added new definitions and proofs to `Data.Nat.Primality`: +* Added new definitions, smart constructors and proofs to `Data.Nat.Primality`: ```agda + infix 10 _Rough_ + _Rough_ : ℕ → Pred ℕ _ + 0-rough : 0 Rough n + 1-rough : 1 Rough n + 2-rough : 2 Rough n + rough⇒≤ : .{{NonTrivial n}} → m Rough n → m ≤ n + ∤⇒rough-suc : m ∤ n → m Rough n → (suc m) Rough n + rough∧∣⇒rough : m Rough o → n ∣ o → m Rough n Composite : ℕ → Set + composite-≢ : .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → + Composite n + composite-∣ : .{{NonZero n}} → Composite m → m ∣ n → Composite n composite? : Decidable Composite Irreducible : ℕ → Set irreducible? : Decidable Irreducible @@ -2871,7 +2883,7 @@ Additions to existing modules ⊓≡⊓′ : m ⊓ n ≡ m ⊓′ n ∣-∣≡∣-∣′ : ∣ m - n ∣ ≡ ∣ m - n ∣′ - nonZero? : Decidable NonZero + nonTrivial? : Decidable NonTrivial eq? : A ↣ ℕ → DecidableEquality A ≤-<-connex : Connex _≤_ _<_ ≥->-connex : Connex _≥_ _>_ diff --git a/src/Data/Nat/Divisibility/Core.agda b/src/Data/Nat/Divisibility/Core.agda index a64302c4cd..b419d73964 100644 --- a/src/Data/Nat/Divisibility/Core.agda +++ b/src/Data/Nat/Divisibility/Core.agda @@ -19,7 +19,7 @@ open import Relation.Nullary.Negation using (¬_) open import Relation.Binary.Core using (Rel) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong₂; module ≡-Reasoning) - + ------------------------------------------------------------------------ -- Main definition -- diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda index 09f014638a..a0d37730d5 100644 --- a/src/Data/Nat/Primality.agda +++ b/src/Data/Nat/Primality.agda @@ -39,7 +39,7 @@ private -- The positive/existential relation `BoundedNonTrivialDivisor` is -- the basis for the whole development, as it captures the possible -- non-trivial divisors of a given number; its complement, `Rough`, --- therefore sets *lower* bounds on any possible such divisors. +-- therefore sets *lower* bounds on any possible such divisors. -- The predicate `Composite` is then defined as the 'diagonal' instance -- of `BoundedNonTrivialDivisor`, while `Prime` is essentially defined as @@ -110,7 +110,7 @@ rough-1 _ (boundedNonTrivialDivisor _ d∣1) = rough⇒≤ : .{{NonTrivial n}} → m Rough n → m ≤ n rough⇒≤ rough = ≮⇒≥ n≮m where n≮m = λ m>n → rough (boundedNonTrivialDivisor m>n ∣-refl) - + -- If a number n is m-rough, and m ∤ n, then n is (suc m)-rough ∤⇒rough-suc : m ∤ n → m Rough n → (suc m) Rough n ∤⇒rough-suc m∤n r (boundedNonTrivialDivisor d<1+m d∣n) @@ -218,7 +218,7 @@ prime? n@(2+ _) = Dec.map PrimeUpTo⇔Prime (primeUpTo? n) -- Equivalent bounded predicate definition PrimeUpTo : Pred ℕ _ PrimeUpTo n = ∀ {d} → d < n → NonTrivial d → d ∤ n - + -- Proof of equivalence prime⇒prime-upto : Prime n → PrimeUpTo n prime⇒prime-upto (prime p) {d} d Date: Thu, 23 Nov 2023 17:18:49 +0800 Subject: [PATCH 76/78] Rename 1<2+ to sz1⇒nonTrivial : ∀ {n} → n > 1 → NonTrivial n -n>1⇒nonTrivial 1<2+n = _ +n>1⇒nonTrivial sz1 : ∀ n → .{{NonTrivial n}} → n > 1 -nonTrivial⇒n>1 (2+ _) = 1<2+n +nonTrivial⇒n>1 (2+ _) = sz Date: Fri, 24 Nov 2023 13:22:18 +0800 Subject: [PATCH 77/78] Rename hasNonTrivialDivisor relation --- src/Data/Nat/Divisibility.agda | 24 ++++++++++++------------ src/Data/Nat/Divisibility/Core.agda | 10 +++++----- src/Data/Nat/Primality.agda | 24 ++++++++++++------------ 3 files changed, 29 insertions(+), 29 deletions(-) diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda index 240c381434..9083642f80 100644 --- a/src/Data/Nat/Divisibility.agda +++ b/src/Data/Nat/Divisibility.agda @@ -313,21 +313,21 @@ m≤n⇒m!∣n! m≤n = help (≤⇒≤′ m≤n) -- Smart constructor -boundedNonTrivialDivisor-≢ : ∀ {d n} → .{{NonTrivial d}} → .{{NonZero n}} → - d ≢ n → d ∣ n → n BoundedNonTrivialDivisor n -boundedNonTrivialDivisor-≢ d≢n d∣n - = boundedNonTrivialDivisor (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n +hasNonTrivialDivisor-≢ : ∀ {d n} → .{{NonTrivial d}} → .{{NonZero n}} → + d ≢ n → d ∣ n → n HasNonTrivialDivisorLessThan n +hasNonTrivialDivisor-≢ d≢n d∣n + = hasNonTrivialDivisor (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n -- Monotonicity wrt ∣ -boundedNonTrivialDivisor-∣ : ∀ {m n o} → m BoundedNonTrivialDivisor n → n ∣ o → - m BoundedNonTrivialDivisor o -boundedNonTrivialDivisor-∣ (boundedNonTrivialDivisor d 1 is m-rough, then m ≤ n rough⇒≤ : .{{NonTrivial n}} → m Rough n → m ≤ n rough⇒≤ rough = ≮⇒≥ n≮m - where n≮m = λ m>n → rough (boundedNonTrivialDivisor m>n ∣-refl) + where n≮m = λ m>n → rough (hasNonTrivialDivisor m>n ∣-refl) -- If a number n is m-rough, and m ∤ n, then n is (suc m)-rough ∤⇒rough-suc : m ∤ n → m Rough n → (suc m) Rough n -∤⇒rough-suc m∤n r (boundedNonTrivialDivisor d<1+m d∣n) +∤⇒rough-suc m∤n r (hasNonTrivialDivisor d<1+m d∣n) with m<1+n⇒m Date: Fri, 24 Nov 2023 13:25:47 +0800 Subject: [PATCH 78/78] Updated CHANGELOG --- CHANGELOG.md | 26 +++++++------------------- 1 file changed, 7 insertions(+), 19 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8ee62ae4a0..af7a35ea0f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -651,8 +651,8 @@ Non-backwards compatible changes .{{nontrivial}} : NonTrivial p notComposite : ¬ Composite p ``` - where `Composite` is now defined as the diagonal of the relation - `Data.Nat.Divisibility.Core.BoundedNonTrivialDivisor` defined below. + where `Composite` is now defined as the diagonal of the new relation + `_HasNonTrivialDivisorLessThan_` in `Data.Nat.Divisibility.Core`. ### Changes to operation reduction behaviour in `Data.Rational(.Unnormalised)` @@ -2775,25 +2775,14 @@ Additions to existing modules * Added a new pattern synonym and a new definition to `Data.Nat.Divisibility.Core`: ```agda pattern divides-refl q = divides q refl - - infix 10 _BoundedNonTrivialDivisor_ - record _BoundedNonTrivialDivisor_ (m n : ℕ) : Set where - constructor boundedNonTrivialDivisor - field - {divisor} : ℕ - .{{nontrivial}} : NonTrivial divisor - divisor-< : divisor < m - divisor-∣ : divisor ∣ n + record _HasNonTrivialDivisorLessThan_ (m n : ℕ) : Set where ``` * Added new proofs to `Data.Nat.Divisibility`: ```agda - boundedNonTrivialDivisor-≢ : .{{NonTrivial d}} → .{{NonZero n}} → - d ≢ n → d ∣ n → n BoundedNonTrivialDivisor n - boundedNonTrivialDivisor-∣ : m BoundedNonTrivialDivisor n → n ∣ o → - m BoundedNonTrivialDivisor o - boundedNonTrivialDivisor-≤ : m BoundedNonTrivialDivisor n → m ≤ o → - o BoundedNonTrivialDivisor n + hasNonTrivialDivisor-≢ : .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → n HasNonTrivialDivisorLessThan n + hasNonTrivialDivisor-∣ : m HasNonTrivialDivisorLessThan n → m ∣ o → o HasNonTrivialDivisorLessThan n + hasNonTrivialDivisor-≤ : m HasNonTrivialDivisorLessThan n → n ≤ o → m HasNonTrivialDivisorLessThan o ``` * Added new definitions, smart constructors and proofs to `Data.Nat.Primality`: @@ -2807,8 +2796,7 @@ Additions to existing modules ∤⇒rough-suc : m ∤ n → m Rough n → (suc m) Rough n rough∧∣⇒rough : m Rough o → n ∣ o → m Rough n Composite : ℕ → Set - composite-≢ : .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → - Composite n + composite-≢ : .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → Composite n composite-∣ : .{{NonZero n}} → Composite m → m ∣ n → Composite n composite? : Decidable Composite Irreducible : ℕ → Set