From 85c485f00eda3ab8d9736f44c9b4db8708d9455f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 15 Jan 2024 15:56:23 +0000 Subject: [PATCH 01/25] Add `Data.Nat.Bounded` --- CHANGELOG.md | 5 +++ src/Data/Nat/Bounded.agda | 69 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 74 insertions(+) create mode 100644 src/Data/Nat/Bounded.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 5b3079dee4..7b6d42e757 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,6 +29,11 @@ Deprecated names New modules ----------- +* Equivalence of `Fin` and an 'obvious' definition of 'bounded natural number' type, in: + ```agda + Data.Nat.Bounded + ``` + Additions to existing modules ----------------------------- diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda new file mode 100644 index 0000000000..c83724dd06 --- /dev/null +++ b/src/Data/Nat/Bounded.agda @@ -0,0 +1,69 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Bounded natural numbers, and their equivalence to `Fin` +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Nat.Bounded where + +open import Data.Nat.Base as ℕ +import Data.Nat.Properties as ℕ +open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ) +import Data.Fin.Properties as Fin +open import Function.Base using (id; _∘_; _on_) +open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl) +open import Relation.Nullary.Decidable.Core using (recompute) +open import Relation.Nullary.Negation.Core using (¬_) + +private + variable + m n : ℕ + +------------------------------------------------------------------------ +-- Definition + +record BoundedNat (n : ℕ) : Set where + constructor ⟦_⟧< + field + value : ℕ + .{{bounded}} : value < n + +open BoundedNat public using () renaming (value to ⟦_⟧) + +-- Constructor + +⟦0⟧< : ∀ n → .{{ NonZero n }} → BoundedNat n +⟦0⟧< (n@(suc _)) = ⟦ zero ⟧< where instance _ = z Date: Sat, 20 Jan 2024 11:35:28 +0000 Subject: [PATCH 02/25] renamed type; removed `instance`-based field; stumbled over isomorphism --- CHANGELOG.md | 3 ++- src/Data/Nat/Bounded.agda | 56 ++++++++++++++++++++++++--------------- 2 files changed, 37 insertions(+), 22 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7b6d42e757..78c81c98bc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,7 +29,8 @@ Deprecated names New modules ----------- -* Equivalence of `Fin` and an 'obvious' definition of 'bounded natural number' type, in: +* Isomorphism between `Fin` and an 'obvious' definition `ℕ<` of + 'bounded natural number' type, in: ```agda Data.Nat.Bounded ``` diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index c83724dd06..7bb3ff419c 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -12,9 +12,12 @@ open import Data.Nat.Base as ℕ import Data.Nat.Properties as ℕ open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ) import Data.Fin.Properties as Fin +open import Data.Product.Base using (_,_) open import Function.Base using (id; _∘_; _on_) +open import Function.Bundles using (_⤖_; mk⤖) +open import Function.Definitions using (Bijective; Injective; Surjective) open import Relation.Binary.Core using (_⇒_) -open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl) open import Relation.Nullary.Decidable.Core using (recompute) open import Relation.Nullary.Negation.Core using (¬_) @@ -25,45 +28,56 @@ private ------------------------------------------------------------------------ -- Definition -record BoundedNat (n : ℕ) : Set where - constructor ⟦_⟧< +record ℕ< (n : ℕ) : Set where + constructor ⟦_⟧<_ field value : ℕ - .{{bounded}} : value < n + .bounded : value < n -open BoundedNat public using () renaming (value to ⟦_⟧) +open ℕ< public using () renaming (value to ⟦_⟧) -- Constructor -⟦0⟧< : ∀ n → .{{ NonZero n }} → BoundedNat n -⟦0⟧< (n@(suc _)) = ⟦ zero ⟧< where instance _ = z Date: Sat, 20 Jan 2024 11:57:23 +0000 Subject: [PATCH 03/25] got there in the end: yuk! --- src/Data/Nat/Bounded.agda | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index 7bb3ff419c..d6785f0bc7 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -13,11 +13,12 @@ import Data.Nat.Properties as ℕ open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ) import Data.Fin.Properties as Fin open import Data.Product.Base using (_,_) -open import Function.Base using (id; _∘_; _on_) +open import Function.Base using (id; _∘_; _$_; _on_) open import Function.Bundles using (_⤖_; mk⤖) -open import Function.Definitions using (Bijective; Injective; Surjective) +open import Function.Consequences.Propositional + using (inverseᵇ⇒bijective; strictlyInverseˡ⇒inverseˡ; strictlyInverseʳ⇒inverseʳ) open import Relation.Binary.Core using (_⇒_) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; _≗_) open import Relation.Nullary.Decidable.Core using (recompute) open import Relation.Nullary.Negation.Core using (¬_) @@ -52,7 +53,7 @@ isBounded (⟦ _ ⟧< i Date: Mon, 22 Jan 2024 07:20:31 +0000 Subject: [PATCH 04/25] added `nonZeroIndex` --- src/Data/Nat/Bounded.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index d6785f0bc7..5f6c355bb0 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -47,6 +47,9 @@ open ℕ< public using () renaming (value to ⟦_⟧) ¬ℕ<[0] : ¬ ℕ< 0 ¬ℕ<[0] () +nonZeroIndex : ℕ< n → NonZero n +nonZeroIndex {n = suc _} _ = _ + isBounded : (i : ℕ< n) → ⟦ i ⟧ < n isBounded (⟦ _ ⟧< i Date: Tue, 23 Jan 2024 09:07:32 +0000 Subject: [PATCH 05/25] =?UTF-8?q?added=20`=E2=84=95<`=20literals?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 1 + src/Data/Nat/Bounded.agda | 14 +++++++++++++- src/Data/Nat/Bounded/Literals.agda | 15 +++++++++++++++ 3 files changed, 29 insertions(+), 1 deletion(-) create mode 100644 src/Data/Nat/Bounded/Literals.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 78c81c98bc..c565c63b69 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -33,6 +33,7 @@ New modules 'bounded natural number' type, in: ```agda Data.Nat.Bounded + Data.Nat.Bounded.Literals ``` Additions to existing modules diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index 5f6c355bb0..9dc021cd98 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -8,6 +8,7 @@ module Data.Nat.Bounded where +open import Data.Bool.Base using (T) open import Data.Nat.Base as ℕ import Data.Nat.Properties as ℕ open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ) @@ -68,7 +69,7 @@ toFin : ℕ< n → Fin n toFin (⟦ _ ⟧< i Date: Wed, 24 Jan 2024 16:51:27 +0000 Subject: [PATCH 06/25] added `DecidableEquality` --- src/Data/Nat/Bounded.agda | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index 9dc021cd98..f264c5dba5 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -19,8 +19,9 @@ open import Function.Bundles using (_⤖_; mk⤖) open import Function.Consequences.Propositional using (inverseᵇ⇒bijective; strictlyInverseˡ⇒inverseˡ; strictlyInverseʳ⇒inverseʳ) open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; _≗_) -open import Relation.Nullary.Decidable.Core using (recompute) +open import Relation.Nullary.Decidable.Core using (recompute; map′) open import Relation.Nullary.Negation.Core using (¬_) private @@ -62,6 +63,11 @@ bounded≡⇒⟦⟧≡⟦⟧ = cong ⟦_⟧ ⟦⟧≡⟦⟧⇒bounded≡ : (_≡_ on ⟦_⟧) ⇒ _≡_ {A = ℕ< n} ⟦⟧≡⟦⟧⇒bounded≡ refl = refl +infix 4 _≟_ +_≟_ : DecidableEquality (ℕ< n) +i ≟ j = map′ ⟦⟧≡⟦⟧⇒bounded≡ bounded≡⇒⟦⟧≡⟦⟧ {!⟦ i ⟧ ℕ.≟ ⟦ j ⟧!} -- (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) + + ------------------------------------------------------------------------ -- Conversion to and from `Fin n` From 11bb6992b7f4737353e8e84e403952205ca8a9f2 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 24 Jan 2024 19:03:17 +0000 Subject: [PATCH 07/25] too hasty to push --- src/Data/Nat/Bounded.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index f264c5dba5..965c232111 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -65,7 +65,7 @@ bounded≡⇒⟦⟧≡⟦⟧ = cong ⟦_⟧ infix 4 _≟_ _≟_ : DecidableEquality (ℕ< n) -i ≟ j = map′ ⟦⟧≡⟦⟧⇒bounded≡ bounded≡⇒⟦⟧≡⟦⟧ {!⟦ i ⟧ ℕ.≟ ⟦ j ⟧!} -- (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n)) +i ≟ j = map′ ⟦⟧≡⟦⟧⇒bounded≡ bounded≡⇒⟦⟧≡⟦⟧ (⟦ i ⟧ ℕ.≟ ⟦ j ⟧) ------------------------------------------------------------------------ From 51b62806c1cf11772a4772eefc115b973094ddea Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 25 Jan 2024 08:13:26 +0000 Subject: [PATCH 08/25] added projection from Nat; additional constructors --- src/Data/Nat/Bounded.agda | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index 965c232111..5fbb6b7fe8 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -10,6 +10,7 @@ module Data.Nat.Bounded where open import Data.Bool.Base using (T) open import Data.Nat.Base as ℕ +import Data.Nat.DivMod as ℕ import Data.Nat.Properties as ℕ open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ) import Data.Fin.Properties as Fin @@ -39,10 +40,19 @@ record ℕ< (n : ℕ) : Set where open ℕ< public using () renaming (value to ⟦_⟧) --- Constructor +-- Constructors: '0 mod n', 'n-1 mod n', '1 mod n' -⟦0⟧< : ∀ n → .{{ NonZero n }} → ℕ< n -⟦0⟧< (n@(suc _)) = ⟦ zero ⟧< z-nonZero⁻¹ _ +⟦-1⟧< {n = suc m} = ⟦ m ⟧< ℕ.n<1+n m + +⟦1⟧< : .{{ NonTrivial n }} → ℕ< n +⟦1⟧< = ⟦ 1 ⟧< nonTrivial⇒n>1 _ + +-- Projection from ℕ + +π : .{{ NonZero n }} → ℕ → ℕ< n +π {n} m = ⟦ m % n ⟧< ℕ.m%n Date: Thu, 25 Jan 2024 15:10:30 +0000 Subject: [PATCH 09/25] tweak to [[1]]< --- src/Data/Nat/Bounded.agda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index 5fbb6b7fe8..4d0ebd4f81 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -46,8 +46,9 @@ open ℕ< public using () renaming (value to ⟦_⟧) ⟦0⟧< = ⟦ 0 ⟧< >-nonZero⁻¹ _ ⟦-1⟧< {n = suc m} = ⟦ m ⟧< ℕ.n<1+n m -⟦1⟧< : .{{ NonTrivial n }} → ℕ< n -⟦1⟧< = ⟦ 1 ⟧< nonTrivial⇒n>1 _ +⟦1⟧< : .{{ NonZero n }} → ℕ< n +⟦1⟧< {n = 1} = ⟦0⟧< +⟦1⟧< {n = 2+ _} = ⟦ 1 ⟧< nonTrivial⇒n>1 _ -- Projection from ℕ From e560b6f304d695c9b91d6cccfe698e06dc16770a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 1 Feb 2024 07:29:16 +0000 Subject: [PATCH 10/25] tweak --- src/Data/Nat/Bounded.agda | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index 4d0ebd4f81..a971efe699 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -40,15 +40,13 @@ record ℕ< (n : ℕ) : Set where open ℕ< public using () renaming (value to ⟦_⟧) --- Constructors: '0 mod n', 'n-1 mod n', '1 mod n' +-- Constructors: 'n-1 mod n', '0 mod n', '1 mod n' -⟦0⟧< ⟦-1⟧< : .{{ NonZero n }} → ℕ< n -⟦0⟧< = ⟦ 0 ⟧< >-nonZero⁻¹ _ +⟦-1⟧< ⟦0⟧< ⟦1⟧< : .{{ NonZero n }} → ℕ< n ⟦-1⟧< {n = suc m} = ⟦ m ⟧< ℕ.n<1+n m - -⟦1⟧< : .{{ NonZero n }} → ℕ< n -⟦1⟧< {n = 1} = ⟦0⟧< -⟦1⟧< {n = 2+ _} = ⟦ 1 ⟧< nonTrivial⇒n>1 _ +⟦0⟧< = ⟦ 0 ⟧< >-nonZero⁻¹ _ +⟦1⟧< {n = 1} = ⟦0⟧< +⟦1⟧< {n = 2+ _} = ⟦ 1 ⟧< nonTrivial⇒n>1 _ -- Projection from ℕ From 0fe029ef07ab163132fbfbbcfe7faa0f12e3c2a6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 4 Feb 2024 11:20:25 +0000 Subject: [PATCH 11/25] rename projection from `Nat` --- src/Data/Nat/Bounded.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index a971efe699..19506f60c4 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -50,8 +50,8 @@ open ℕ< public using () renaming (value to ⟦_⟧) -- Projection from ℕ -π : .{{ NonZero n }} → ℕ → ℕ< n -π {n} m = ⟦ m % n ⟧< ℕ.m%n Date: Mon, 5 Feb 2024 05:56:03 +0000 Subject: [PATCH 12/25] added `Equivalence` proof --- src/Data/Nat/Bounded.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index 19506f60c4..13070c4e61 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -16,7 +16,7 @@ open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ) import Data.Fin.Properties as Fin open import Data.Product.Base using (_,_) open import Function.Base using (id; _∘_; _$_; _on_) -open import Function.Bundles using (_⤖_; mk⤖) +open import Function.Bundles using (_⤖_; mk⤖; _↔_; mk↔ₛ′) open import Function.Consequences.Propositional using (inverseᵇ⇒bijective; strictlyInverseˡ⇒inverseˡ; strictlyInverseʳ⇒inverseʳ) open import Relation.Binary.Core using (_⇒_) @@ -97,6 +97,9 @@ boundedNat⤖Fin = mk⤖ $ inverseᵇ⇒bijective $ , strictlyInverseʳ⇒inverseʳ {f⁻¹ = fromFin} toFin fromFin∘toFin≐id +boundedNat↔Fin : ℕ< n ↔ Fin n +boundedNat↔Fin = mk↔ₛ′ toFin fromFin toFin∘fromFin≐id fromFin∘toFin≐id + ------------------------------------------------------------------------ -- Literals From 821f51c3562f962dfebd1e091898a6479fd1b453 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 5 Feb 2024 09:05:10 +0000 Subject: [PATCH 13/25] =?UTF-8?q?inverting=20`from=E2=84=95`=20lemmas?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Data/Nat/Bounded.agda | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index 13070c4e61..edb8ba37ba 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -21,7 +21,8 @@ open import Function.Consequences.Propositional using (inverseᵇ⇒bijective; strictlyInverseˡ⇒inverseˡ; strictlyInverseʳ⇒inverseʳ) open import Relation.Binary.Core using (_⇒_) open import Relation.Binary.Definitions -open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; _≗_) +open import Relation.Binary.PropositionalEquality + using (_≡_; refl; sym; trans; cong; subst; _≗_) open import Relation.Nullary.Decidable.Core using (recompute; map′) open import Relation.Nullary.Negation.Core using (¬_) @@ -64,6 +65,7 @@ nonZeroIndex {n = suc _} _ = _ isBounded : (i : ℕ< n) → ⟦ i ⟧ < n isBounded (⟦ _ ⟧< i Date: Mon, 5 Feb 2024 12:39:22 +0000 Subject: [PATCH 14/25] added quotient equivalence relation --- src/Data/Nat/Bounded.agda | 47 ++++++++++++++++++++++++++++++++++----- 1 file changed, 41 insertions(+), 6 deletions(-) diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index edb8ba37ba..ab1167f11c 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -19,7 +19,7 @@ open import Function.Base using (id; _∘_; _$_; _on_) open import Function.Bundles using (_⤖_; mk⤖; _↔_; mk↔ₛ′) open import Function.Consequences.Propositional using (inverseᵇ⇒bijective; strictlyInverseˡ⇒inverseˡ; strictlyInverseʳ⇒inverseʳ) -open import Relation.Binary.Core using (_⇒_) +open import Relation.Binary.Core using (Rel; _⇒_) open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; subst; _≗_) @@ -108,12 +108,11 @@ boundedNat↔Fin = mk↔ₛ′ toFin fromFin toFin∘fromFin≐id fromFin∘toFi data _/∼≡_ : ℕ → ℕ< n → Set where ‵fromℕ : ∀ m (i : ℕ< n) → (⟦ i ⟧ + m * n) /∼≡ i -module _ {n} .{{_ : NonZero n}} m where +module _ {n} .{{_ : NonZero n}} {m} {i : ℕ< n} where - private i = fromℕ {n} m - - _/∼≡fromℕ : m /∼≡ i - _/∼≡fromℕ = subst (_/∼≡ i) (sym (ℕ.m≡m%n+[m/n]*n m n)) (‵fromℕ (m / n) i) + _/∼≡fromℕ : fromℕ {n} m ≡ i → m /∼≡ i + _/∼≡fromℕ refl = let i = fromℕ {n} m in + subst (_/∼≡ i) (sym (ℕ.m≡m%n+[m/n]*n m n)) (‵fromℕ (m / n) i) module _ {n} {m} {i : ℕ< n} where @@ -123,6 +122,42 @@ module _ {n} {m} {i : ℕ< n} where (‵fromℕ {n = n} m i) /∼≡fromℕ⁻¹ = ⟦⟧≡⟦⟧⇒bounded≡ $ trans (ℕ.[m+kn]%n≡m%n ⟦ i ⟧ m n) (ℕ.m Date: Fri, 9 Feb 2024 16:21:00 +0000 Subject: [PATCH 15/25] module refactoring --- CHANGELOG.md | 2 + src/Data/Nat/Bounded.agda | 172 +++------------------------ src/Data/Nat/Bounded/Base.agda | 94 +++++++++++++++ src/Data/Nat/Bounded/Literals.agda | 26 +++- src/Data/Nat/Bounded/Properties.agda | 124 +++++++++++++++++++ 5 files changed, 255 insertions(+), 163 deletions(-) create mode 100644 src/Data/Nat/Bounded/Base.agda create mode 100644 src/Data/Nat/Bounded/Properties.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 108d153a01..41a2264204 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -39,7 +39,9 @@ New modules 'bounded natural number' type, in: ```agda Data.Nat.Bounded + Data.Nat.Bounded.Base Data.Nat.Bounded.Literals + Data.Nat.Bounded.Properties ``` Additions to existing modules diff --git a/src/Data/Nat/Bounded.agda b/src/Data/Nat/Bounded.agda index ab1167f11c..0af9e09467 100644 --- a/src/Data/Nat/Bounded.agda +++ b/src/Data/Nat/Bounded.agda @@ -1,171 +1,29 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Bounded natural numbers, and their equivalence to `Fin` +-- Bounded natural numbers ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Nat.Bounded where -open import Data.Bool.Base using (T) -open import Data.Nat.Base as ℕ -import Data.Nat.DivMod as ℕ -import Data.Nat.Properties as ℕ -open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ) -import Data.Fin.Properties as Fin -open import Data.Product.Base using (_,_) -open import Function.Base using (id; _∘_; _$_; _on_) -open import Function.Bundles using (_⤖_; mk⤖; _↔_; mk↔ₛ′) -open import Function.Consequences.Propositional - using (inverseᵇ⇒bijective; strictlyInverseˡ⇒inverseˡ; strictlyInverseʳ⇒inverseʳ) -open import Relation.Binary.Core using (Rel; _⇒_) -open import Relation.Binary.Definitions -open import Relation.Binary.PropositionalEquality - using (_≡_; refl; sym; trans; cong; subst; _≗_) -open import Relation.Nullary.Decidable.Core using (recompute; map′) -open import Relation.Nullary.Negation.Core using (¬_) - -private - variable - m n : ℕ - ------------------------------------------------------------------------- --- Definition - -record ℕ< (n : ℕ) : Set where - constructor ⟦_⟧<_ - field - value : ℕ - .bounded : value < n - -open ℕ< public using () renaming (value to ⟦_⟧) - --- Constructors: 'n-1 mod n', '0 mod n', '1 mod n' - -⟦-1⟧< ⟦0⟧< ⟦1⟧< : .{{ NonZero n }} → ℕ< n -⟦-1⟧< {n = suc m} = ⟦ m ⟧< ℕ.n<1+n m -⟦0⟧< = ⟦ 0 ⟧< >-nonZero⁻¹ _ -⟦1⟧< {n = 1} = ⟦0⟧< -⟦1⟧< {n = 2+ _} = ⟦ 1 ⟧< nonTrivial⇒n>1 _ - --- Projection from ℕ - -fromℕ : .{{ NonZero n }} → ℕ → ℕ< n -fromℕ {n} m = ⟦ m % n ⟧< ℕ.m%n-nonZero⁻¹ _ +⟦1⟧< {n = 1} = ⟦0⟧< +⟦1⟧< {n = 2+ _} = ⟦ 1 ⟧< nonTrivial⇒n>1 _ + +-- Projection from ℕ + +fromℕ : .{{ NonZero n }} → ℕ → ℕ< n +fromℕ {n} m = ⟦ m % n ⟧< ℕ.m%n Date: Fri, 9 Feb 2024 16:27:53 +0000 Subject: [PATCH 16/25] cosmetic --- src/Data/Nat/Bounded/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index c660ee5435..052afd3379 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -74,7 +74,7 @@ module _ {m} {i : ℕ< n} where _/∼≡fromℕ : fromℕ m ≡ i → m /∼≡ i _/∼≡fromℕ = _/∼≡fromℕ′ where - _/∼≡fromℕ′ : .{{_ : NonZero n}} → fromℕ {n} m ≡ i → m /∼≡ i + _/∼≡fromℕ′ : .{{_ : NonZero n}} → fromℕ m ≡ i → m /∼≡ i _/∼≡fromℕ′ refl = subst (_/∼≡ i) (sym (ℕ.m≡m%n+[m/n]*n m n)) (‵fromℕ (m / n) i) From 823016b60f23df3f5c08355bee2fee6736d61191 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 9 Feb 2024 18:37:20 +0000 Subject: [PATCH 17/25] added two simple lemmas about underlying values --- src/Data/Nat/Bounded/Properties.agda | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index 052afd3379..7ef2cf3fa6 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -36,6 +36,13 @@ private ------------------------------------------------------------------------ -- Equality on values is propositional equality +⟦0⟧≡0 : .{{_ : NonZero n}} → ⟦ ⟦0⟧< {n = n} ⟧ ≡ 0 +⟦0⟧≡0 {n = suc _} = refl + +⟦1⟧≡1 : .{{_ : NonTrivial n}} → + let instance _ = nonTrivial⇒nonZero n in ⟦ ⟦1⟧< {n = n} ⟧ ≡ 1 +⟦1⟧≡1 {n = 2+ _} = refl + ≡⇒⟦⟧≡⟦⟧ : _≡_ {A = ℕ< n} ⇒ (_≡_ on ⟦_⟧) ≡⇒⟦⟧≡⟦⟧ = cong ⟦_⟧ From 623d854cd0244a7e4eb15950130a16efee6d5a71 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 10 Feb 2024 11:29:58 +0000 Subject: [PATCH 18/25] final lemma about the retraction --- src/Data/Nat/Bounded/Properties.agda | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index 7ef2cf3fa6..1207da094e 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -49,6 +49,11 @@ private ⟦⟧≡⟦⟧⇒≡ : (_≡_ on ⟦_⟧) ⇒ _≡_ {A = ℕ< n} ⟦⟧≡⟦⟧⇒≡ refl = refl +fromℕ∘toℕ≐id : (i : ℕ< n) → let instance _ = nonZeroIndex i + in fromℕ ⟦ i ⟧ ≡ i +fromℕ∘toℕ≐id i = let instance _ = nonZeroIndex i + in ⟦⟧≡⟦⟧⇒≡ $ ℕ.m Date: Tue, 13 Feb 2024 11:56:01 +0000 Subject: [PATCH 19/25] tweaks to accomodate #2292 --- src/Data/Nat/Bounded/Base.agda | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda index 01b73f50bc..a230b09b06 100644 --- a/src/Data/Nat/Bounded/Base.agda +++ b/src/Data/Nat/Bounded/Base.agda @@ -20,7 +20,7 @@ open import Relation.Nullary.Negation.Core using (¬_) private variable - m n : ℕ + m n o : ℕ ------------------------------------------------------------------------ -- Definition @@ -87,8 +87,10 @@ record _∼_ {n} (lhs rhs : ℕ) : Set where lhs/∼≡ : lhs /∼≡ k rhs/∼≡ : rhs /∼≡ k -≡-Mod : ℕ → Rel ℕ _ -≡-Mod n i j = _∼_ {n} i j +≡-Modℕ : ℕ → Rel ℕ _ +≡-Modℕ n = _∼_ {n} -syntax ≡-Mod n i j = i ≡ j mod n +syntax ≡-Modℕ n m o = m ≡ o modℕ n +nonZeroModulus : (m ≡ o modℕ n) → NonZero n +nonZeroModulus eq = nonZeroIndex k where open _∼_ eq From f0f4883934e1e89e382ad1fb05c93f7be23065c4 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Tue, 13 Feb 2024 11:59:37 +0000 Subject: [PATCH 20/25] additions to support #2292 --- src/Data/Nat/Bounded/Properties.agda | 124 +++++++++++++++++++++++---- 1 file changed, 105 insertions(+), 19 deletions(-) diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index 1207da094e..c7e8231a9f 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -8,6 +8,7 @@ module Data.Nat.Bounded.Properties where +import Algebra.Definitions as Definitions open import Data.Fin.Base as Fin using (Fin) import Data.Fin.Properties as Fin open import Data.Nat.Base as ℕ @@ -23,15 +24,16 @@ open import Relation.Binary.Structures using (IsPartialEquivalence; IsEquivalenc open import Relation.Binary.Core using (_⇒_) open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality - using (_≡_; refl; erefl; sym; trans; cong; subst; _≗_) + hiding (isEquivalence; setoid) open import Relation.Nullary.Decidable.Core using (map′) open import Data.Nat.Bounded.Base as ℕ< private variable - m n : ℕ - i j : ℕ< n + m n o : ℕ + i j k : ℕ< n + ------------------------------------------------------------------------ -- Equality on values is propositional equality @@ -49,10 +51,25 @@ private ⟦⟧≡⟦⟧⇒≡ : (_≡_ on ⟦_⟧) ⇒ _≡_ {A = ℕ< n} ⟦⟧≡⟦⟧⇒≡ refl = refl +fromℕ[n]≡0 : .{{_ : NonZero n}} → fromℕ n ≡ ⟦0⟧< +fromℕ[n]≡0 {n} = ⟦⟧≡⟦⟧⇒≡ (ℕ.n%n≡0 n) + +module _ (m-nonZero (ℕ.m-nonZero (ℕ.m-nonZero (ℕ.m Date: Tue, 13 Feb 2024 12:14:04 +0000 Subject: [PATCH 21/25] refactored arithmetic --- src/Data/Nat/Bounded/Properties.agda | 33 ++++++++++++++-------------- 1 file changed, 17 insertions(+), 16 deletions(-) diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index c7e8231a9f..739b8bb8d4 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -191,35 +191,36 @@ module _ .{{_ : NonZero n}} (m o : ℕ) where open ≡-Reasoning + +-distrib-% : ((m % n) + (o % n)) ≡ (m + o) modℕ n + +-distrib-% = %≡%⇒≡-mod $ begin + (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ + (m + o) % n ∎ + +-distribˡ-% : ((m % n) + o) ≡ (m + o) modℕ n - +-distribˡ-% = %≡%⇒≡-mod $ begin + +-distribˡ-% = ≡-mod-trans (%≡%⇒≡-mod $ (begin (m % n + o) % n ≡⟨ ℕ.%-distribˡ-+ (m % n) o n ⟩ (m % n % n + o % n) % n ≡⟨ cong ((_% n) ∘ (_+ o % n)) (ℕ.m%n%n≡m%n m n) ⟩ - (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ - (m + o) % n ∎ + (m % n + o % n) % n ∎)) +-distrib-% +-distribʳ-% : (m + (o % n)) ≡ (m + o) modℕ n - +-distribʳ-% = %≡%⇒≡-mod $ begin + +-distribʳ-% = ≡-mod-trans (%≡%⇒≡-mod $ begin (m + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m (o % n) n ⟩ (m % n + o % n % n) % n ≡⟨ cong ((_% n) ∘ (m % n +_)) (ℕ.m%n%n≡m%n o n) ⟩ - (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ - (m + o) % n ∎ + (m % n + o % n) % n ∎) +-distrib-% - +-distrib-% : ((m % n) + (o % n)) ≡ (m + o) modℕ n - +-distrib-% = %≡%⇒≡-mod $ begin - (m % n + o % n) % n ≡⟨ ℕ.%-distribˡ-+ m o n ⟨ - (m + o) % n ∎ + *-distrib-% : ((m % n) * (o % n)) ≡ (m * o) modℕ n + *-distrib-% = %≡%⇒≡-mod $ begin + ((m % n) * (o % n)) % n ≡⟨ ℕ.%-distribˡ-* m o n ⟨ + (m * o) % n ∎ *-distribˡ-% : ((m % n) * o) ≡ (m * o) modℕ n - *-distribˡ-% = %≡%⇒≡-mod $ begin + *-distribˡ-% = ≡-mod-trans (%≡%⇒≡-mod $ begin (m % n * o) % n ≡⟨ ℕ.%-distribˡ-* (m % n) o n ⟩ (m % n % n * (o % n)) % n ≡⟨ cong ((_% n) ∘ (_* (o % n))) (ℕ.m%n%n≡m%n m n) ⟩ - (m % n * (o % n)) % n ≡⟨ ℕ.%-distribˡ-* m o n ⟨ - (m * o) % n ∎ + (m % n * (o % n)) % n ∎) *-distrib-% *-distribʳ-% : (m * (o % n)) ≡ (m * o) modℕ n - *-distribʳ-% = %≡%⇒≡-mod $ begin + *-distribʳ-% = ≡-mod-trans (%≡%⇒≡-mod $ begin (m * (o % n)) % n ≡⟨ ℕ.%-distribˡ-* m (o % n) n ⟩ (m % n * (o % n % n)) % n ≡⟨ cong ((_% n) ∘ (m % n *_)) (ℕ.m%n%n≡m%n o n) ⟩ - (m % n * (o % n)) % n ≡⟨ ℕ.%-distribˡ-* m o n ⟨ - (m * o) % n ∎ + (m % n * (o % n)) % n ∎) *-distrib-% From 10d408373d0716acd3a2dbee72636744f67d72b3 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 14 Feb 2024 12:54:54 +0000 Subject: [PATCH 22/25] revised imports --- src/Data/Nat/Bounded/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda index 739b8bb8d4..1bb2dc88d3 100644 --- a/src/Data/Nat/Bounded/Properties.agda +++ b/src/Data/Nat/Bounded/Properties.agda @@ -24,7 +24,7 @@ open import Relation.Binary.Structures using (IsPartialEquivalence; IsEquivalenc open import Relation.Binary.Core using (_⇒_) open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality - hiding (isEquivalence; setoid) + using (_≡_; refl; erefl; sym; trans; cong; subst; _≗_; module ≡-Reasoning) open import Relation.Nullary.Decidable.Core using (map′) open import Data.Nat.Bounded.Base as ℕ< From 078d4f6c7487303f8a107e2bd0a32b7e7806414d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sun, 17 Mar 2024 16:26:08 +0000 Subject: [PATCH 23/25] fixed up `CHANGELOG` --- CHANGELOG.md | 23 +++++------------------ 1 file changed, 5 insertions(+), 18 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a42d323cf4..a2d3aa7efe 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -64,7 +64,7 @@ New modules ```agda Algebra.Module.Construct.Idealization ``` - + * The unique morphism from the initial, resp. terminal, algebra: ```agda Algebra.Morphism.Construct.Initial @@ -171,7 +171,7 @@ Additions to existing modules quasigroup : Quasigroup _ _ isLoop : IsLoop _∙_ _\\_ _//_ ε loop : Loop _ _ - + \\-leftDividesˡ : LeftDividesˡ _∙_ _\\_ \\-leftDividesʳ : LeftDividesʳ _∙_ _\\_ \\-leftDivides : LeftDivides _∙_ _\\_ @@ -190,7 +190,7 @@ Additions to existing modules identityʳ-unique : x ∙ y ≈ x → y ≈ ε identity-unique : Identity x _∙_ → x ≈ ε ``` - + * In `Algebra.Properties.Monoid.Mult`: ```agda ×-homo-0 : ∀ x → 0 × x ≈ 0# @@ -213,7 +213,7 @@ Additions to existing modules _\\_ : Op₂ A x \\ y = (x ⁻¹) ∙ y ``` - + * In `Data.Container.Indexed.Core`: ```agda Subtrees o c = (r : Response c) → X (next c r) @@ -315,7 +315,7 @@ Additions to existing modules pred-injective : .{{NonZero m}} → .{{NonZero n}} → pred m ≡ pred n → m ≡ n pred-cancel-≡ : pred m ≡ pred n → ((m ≡ 0 × n ≡ 1) ⊎ (m ≡ 1 × n ≡ 0)) ⊎ m ≡ n ``` - + * Added new proofs to `Data.Nat.Primality`: ```agda rough∧square>⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n @@ -378,16 +378,3 @@ Additions to existing modules ```agda ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋ ``` - -* Added module `Data.Vec.Functional.Relation.Binary.Permutation`: - ```agda - _↭_ : IRel (Vector A) _ - ``` - -* Added new file `Data.Vec.Functional.Relation.Binary.Permutation.Properties`: - ```agda - ↭-refl : Reflexive (Vector A) _↭_ - ↭-reflexive : xs ≡ ys → xs ↭ ys - ↭-sym : Symmetric (Vector A) _↭_ - ↭-trans : Transitive (Vector A) _↭_ - ``` From 3c3cbf3149710c05f58dae28d1fd8dadd02072f3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 28 Jul 2024 10:56:36 +0100 Subject: [PATCH 24/25] update `CHANGELOG` to v2.2 --- CHANGELOG.md | 662 +-------------------------------------------------- 1 file changed, 2 insertions(+), 660 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6052661fa8..80da9ee48e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ -Version 2.1-dev +Version 2.2-dev =============== -The library has been tested using Agda 2.6.4, 2.6.4.1, and 2.6.4.3. +The library has been tested using Agda 2.6.4.3. Highlights ---------- @@ -9,678 +9,20 @@ Highlights Bug-fixes --------- -* Fix statement of `Data.Vec.Properties.toList-replicate`, where `replicate` - was mistakenly applied to the level of the type `A` instead of the - variable `x` of type `A`. - -* Module `Data.List.Relation.Ternary.Appending.Setoid.Properties` no longer - exports the `Setoid` module under the alias `S`. - -* Remove unbound parameter from `Data.List.Properties.length-alignWith`, - `alignWith-map` and `map-alignWith`. - Non-backwards compatible changes -------------------------------- -* The modules and morphisms in `Algebra.Module.Morphism.Structures` are now - parametrized by _raw_ bundles rather than lawful bundles, in line with other - modules defining morphism structures. -* The definitions in `Algebra.Module.Morphism.Construct.Composition` are now - parametrized by _raw_ bundles, and as such take a proof of transitivity. -* The definitions in `Algebra.Module.Morphism.Construct.Identity` are now - parametrized by _raw_ bundles, and as such take a proof of reflexivity. -* The module `IO.Primitive` was moved to `IO.Primitive.Core`. - -Other major improvements ------------------------- - Minor improvements ------------------ -The size of the dependency graph for many modules has been -reduced. This may lead to speed ups for first-time loading of some -modules. Deprecated modules ------------------ -* `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` deprecated in favour of - `Data.List.Relation.Binary.Sublist.Propositional.Slice`. - Deprecated names ---------------- -* In `Algebra.Properties.Semiring.Mult`: - ```agda - 1×-identityʳ ↦ ×-homo-1 - ``` - -* In `Algebra.Structures.IsGroup`: - ```agda - _-_ ↦ _//_ - ``` - -* In `Algebra.Structures.Biased`: - ```agda - IsRing* ↦ Algebra.Structures.IsRing - isRing* ↦ Algebra.Structures.isRing - ``` - -* In `Data.List.Base`: - ```agda - scanr ↦ Data.List.Scans.Base.scanr - scanl ↦ Data.List.Scans.Base.scanl - ``` - -* In `Data.List.Properties`: - ```agda - scanr-defn ↦ Data.List.Scans.Properties.scanr-defn - scanl-defn ↦ Data.List.Scans.Properties.scanl-defn - ``` - -* In `Data.List.NonEmpty.Base`: - ```agda - inits : List A → List⁺ (List A) - tails : List A → List⁺ (List A) - ``` - -* In `Data.List.NonEmpty.Properties`: - ```agda - toList-inits : toList ∘ List⁺.inits ≗ List.inits - toList-tails : toList ∘ List⁺.tails ≗ List.tails - ``` - -* In `Data.Nat.Divisibility.Core`: - ```agda - *-pres-∣ ↦ Data.Nat.Divisibility.*-pres-∣ - ``` - -* In `IO.Base`: - ```agda - untilRight ↦ untilInj₂ - ``` - New modules ----------- -* Pointwise lifting of algebraic structures `IsX` and bundles `X` from - carrier set `C` to function space `A → C`: - ``` - Algebra.Construct.Pointwise - ``` - -* Raw bundles for module-like algebraic structures: - ``` - Algebra.Module.Bundles.Raw - ``` - -* Nagata's construction of the "idealization of a module": - ```agda - Algebra.Module.Construct.Idealization - ``` - -* The unique morphism from the initial, resp. terminal, algebra: - ```agda - Algebra.Morphism.Construct.Initial - Algebra.Morphism.Construct.Terminal - ``` - -* Pointwise and equality relations over indexed containers: - ```agda - Data.Container.Indexed.Relation.Binary.Pointwise - Data.Container.Indexed.Relation.Binary.Pointwise.Properties - Data.Container.Indexed.Relation.Binary.Equality.Setoid - ``` - -* Properties of `List` modulo `Setoid` equality (currently only the ([],++) monoid): - ``` - Data.List.Relation.Binary.Equality.Setoid.Properties - ``` - -* `Data.List.Relation.Binary.Sublist.Propositional.Slice` - replacing `Data.List.Relation.Binary.Sublist.Propositional.Disjoint` (*) - and adding new functions: - - `⊆-upper-bound-is-cospan` generalising `⊆-disjoint-union-is-cospan` from (*) - - `⊆-upper-bound-cospan` generalising `⊆-disjoint-union-cospan` from (*) - ``` - -* Refactoring of `Data.List.Base.{scanr|scanl}` and their properties: - ``` - Data.List.Scans.Base - Data.List.Scans.Properties - ``` - -* Isomorphism between `Fin` and an 'obvious' definition `ℕ<` of - 'bounded natural number' type, in: - ```agda - Data.Nat.Bounded - Data.Nat.Bounded.Base - Data.Nat.Bounded.Literals - Data.Nat.Bounded.Properties - ``` - -* Prime factorisation of natural numbers. - ``` - Data.Nat.Primality.Factorisation - ``` - -* `Data.Vec.Functional.Relation.Binary.Permutation`, defining: - ```agda - _↭_ : IRel (Vector A) _ - ``` - -* `Data.Vec.Functional.Relation.Binary.Permutation.Properties` of the above: - ```agda - ↭-refl : Reflexive (Vector A) _↭_ - ↭-reflexive : xs ≡ ys → xs ↭ ys - ↭-sym : Symmetric (Vector A) _↭_ - ↭-trans : Transitive (Vector A) _↭_ - isIndexedEquivalence : {A : Set a} → IsIndexedEquivalence (Vector A) _↭_ - indexedSetoid : {A : Set a} → IndexedSetoid ℕ a _ - ``` - -* `Function.Relation.Binary.Equality` - ```agda - setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _ - ``` - and a convenient infix version - ```agda - _⇨_ = setoid - ``` - -* Consequences of 'infinite descent' for (accessible elements of) well-founded relations: - ```agda - Induction.InfiniteDescent - ``` - -* Symmetric interior of a binary relation - ``` - Relation.Binary.Construct.Interior.Symmetric - ``` - -* Properties of `Setoid`s with decidable equality relation: - ``` - Relation.Binary.Properties.DecSetoid - ``` - -* Pointwise and equality relations over indexed containers: - ```agda - Data.Container.Indexed.Relation.Binary.Pointwise - Data.Container.Indexed.Relation.Binary.Pointwise.Properties - Data.Container.Indexed.Relation.Binary.Equality.Setoid - ``` - -* New IO primitives to handle buffering - ```agda - IO.Primitive.Handle - IO.Handle - ``` - -* `System.Random` bindings: - ```agda - System.Random.Primitive - System.Random - ``` - -* Show modules: - ```agda - Data.List.Show - Data.Vec.Show - Data.Vec.Bounded.Show - ``` - -* Decidability for the subset relation on lists: - ```agda - Data.List.Relation.Binary.Subset.DecSetoid (_⊆?_) - Data.List.Relation.Binary.Subset.DecPropositional - ``` - -* Decidability for the disjoint relation on lists: - ```agda - Data.List.Relation.Binary.Disjoint.DecSetoid (disjoint?) - Data.List.Relation.Binary.Disjoint.DecPropositional - ``` - Additions to existing modules ----------------------------- - -* In `Algebra.Bundles` - ```agda - record SuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) - ``` - -* In `Algebra.Bundles.Raw` - ```agda - record RawSuccessorSet c ℓ : Set (suc (c ⊔ ℓ)) - ``` - -* Exporting more `Raw` substructures from `Algebra.Bundles.Ring`: - ```agda - rawNearSemiring : RawNearSemiring _ _ - rawRingWithoutOne : RawRingWithoutOne _ _ - +-rawGroup : RawGroup _ _ - ``` - -* In `Algebra.Construct.Terminal`: - ```agda - rawNearSemiring : RawNearSemiring c ℓ - nearSemiring : NearSemiring c ℓ - ``` - -* In `Algebra.Module.Bundles`, raw bundles are re-exported and the bundles expose their raw counterparts. - -* In `Algebra.Module.Construct.DirectProduct`: - ```agda - rawLeftSemimodule : RawLeftSemimodule R m ℓm → RawLeftSemimodule m′ ℓm′ → RawLeftSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawLeftModule : RawLeftModule R m ℓm → RawLeftModule m′ ℓm′ → RawLeftModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawRightSemimodule : RawRightSemimodule R m ℓm → RawRightSemimodule m′ ℓm′ → RawRightSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawRightModule : RawRightModule R m ℓm → RawRightModule m′ ℓm′ → RawRightModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawBisemimodule : RawBisemimodule R m ℓm → RawBisemimodule m′ ℓm′ → RawBisemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawBimodule : RawBimodule R m ℓm → RawBimodule m′ ℓm′ → RawBimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawSemimodule : RawSemimodule R m ℓm → RawSemimodule m′ ℓm′ → RawSemimodule R (m ⊔ m′) (ℓm ⊔ ℓm′) - rawModule : RawModule R m ℓm → RawModule m′ ℓm′ → RawModule R (m ⊔ m′) (ℓm ⊔ ℓm′) - ``` - -* In `Algebra.Module.Construct.TensorUnit`: - ```agda - rawLeftSemimodule : RawLeftSemimodule _ c ℓ - rawLeftModule : RawLeftModule _ c ℓ - rawRightSemimodule : RawRightSemimodule _ c ℓ - rawRightModule : RawRightModule _ c ℓ - rawBisemimodule : RawBisemimodule _ _ c ℓ - rawBimodule : RawBimodule _ _ c ℓ - rawSemimodule : RawSemimodule _ c ℓ - rawModule : RawModule _ c ℓ - ``` - -* In `Algebra.Module.Construct.Zero`: - ```agda - rawLeftSemimodule : RawLeftSemimodule R c ℓ - rawLeftModule : RawLeftModule R c ℓ - rawRightSemimodule : RawRightSemimodule R c ℓ - rawRightModule : RawRightModule R c ℓ - rawBisemimodule : RawBisemimodule R c ℓ - rawBimodule : RawBimodule R c ℓ - rawSemimodule : RawSemimodule R c ℓ - rawModule : RawModule R c ℓ - ``` - -* In `Algebra.Morphism.Structures` - ```agda - module SuccessorSetMorphisms (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂) where - record IsSuccessorSetHomomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ - record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ - record IsSuccessorSetIsomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _ - -* In `Algebra.Properties.AbelianGroup`: - ``` - ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x - ``` - -* In `Algebra.Properties.Group`: - ```agda - isQuasigroup : IsQuasigroup _∙_ _\\_ _//_ - quasigroup : Quasigroup _ _ - isLoop : IsLoop _∙_ _\\_ _//_ ε - loop : Loop _ _ - - \\-leftDividesˡ : LeftDividesˡ _∙_ _\\_ - \\-leftDividesʳ : LeftDividesʳ _∙_ _\\_ - \\-leftDivides : LeftDivides _∙_ _\\_ - //-rightDividesˡ : RightDividesˡ _∙_ _//_ - //-rightDividesʳ : RightDividesʳ _∙_ _//_ - //-rightDivides : RightDivides _∙_ _//_ - - ⁻¹-selfInverse : SelfInverse _⁻¹ - x∙y⁻¹≈ε⇒x≈y : ∀ x y → (x ∙ y ⁻¹) ≈ ε → x ≈ y - x≈y⇒x∙y⁻¹≈ε : ∀ {x y} → x ≈ y → (x ∙ y ⁻¹) ≈ ε - \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_ - comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x - ⁻¹-anti-homo-// : (x // y) ⁻¹ ≈ y // x - ⁻¹-anti-homo-\\ : (x \\ y) ⁻¹ ≈ y \\ x - ``` - -* In `Algebra.Properties.Loop`: - ```agda - identityˡ-unique : x ∙ y ≈ y → x ≈ ε - identityʳ-unique : x ∙ y ≈ x → y ≈ ε - identity-unique : Identity x _∙_ → x ≈ ε - ``` - -* In `Algebra.Properties.Monoid.Mult`: - ```agda - ×-homo-0 : ∀ x → 0 × x ≈ 0# - ×-homo-1 : ∀ x → 1 × x ≈ x - ``` - -* In `Algebra.Properties.Semiring.Mult`: - ```agda - ×-homo-0# : ∀ x → 0 × x ≈ 0# * x - ×-homo-1# : ∀ x → 1 × x ≈ 1# * x - idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x - ``` - -* In `Algebra.Structures` - ```agda - record IsSuccessorSet (suc# : Op₁ A) (zero# : A) : Set _ - -* In `Algebra.Structures.IsGroup`: - ```agda - infixl 6 _//_ - _//_ : Op₂ A - x // y = x ∙ (y ⁻¹) - infixr 6 _\\_ - _\\_ : Op₂ A - x \\ y = (x ⁻¹) ∙ y - ``` - -* In `Algebra.Structures.IsCancellativeCommutativeSemiring` add the - extra property as an exposed definition: - ```agda - *-cancelʳ-nonZero : AlmostRightCancellative 0# * - ``` - -* In `Data.Container.Indexed.Core`: - ```agda - Subtrees o c = (r : Response c) → X (next c r) - ``` - -* In `Data.Fin.Properties`: - ```agda - nonZeroIndex : Fin n → ℕ.NonZero n - ``` - -* In `Data.Float.Base`: - ```agda - _≤_ : Rel Float _ - ``` - -* In `Data.Integer.Divisibility`: introduce `divides` as an explicit pattern synonym - ```agda - pattern divides k eq = Data.Nat.Divisibility.divides k eq - ``` - -* In `Data.Integer.Properties`: - ```agda - ◃-nonZero : .{{_ : ℕ.NonZero n}} → NonZero (s ◃ n) - sign-* : .{{NonZero (i * j)}} → sign (i * j) ≡ sign i Sign.* sign j - i*j≢0 : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j) - ``` - -* In `Data.List.Base` redefine `inits` and `tails` in terms of: - ```agda - tail∘inits : List A → List (List A) - tail∘tails : List A → List (List A) - ``` - -* In `Data.List.Membership.Setoid.Properties`: - ```agda - reverse⁺ : x ∈ xs → x ∈ reverse xs - reverse⁻ : x ∈ reverse xs → x ∈ xs - ``` - -* In `Data.List.NonEmpty.Base`: - ```agda - inits : List A → List⁺ (List A) - tails : List A → List⁺ (List A) - ``` - -* In `Data.List.Properties`: - ```agda - length-catMaybes : length (catMaybes xs) ≤ length xs - applyUpTo-∷ʳ : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n) - applyDownFrom-∷ʳ : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n) - upTo-∷ʳ : upTo n ∷ʳ n ≡ upTo (suc n) - downFrom-∷ʳ : applyDownFrom suc n ∷ʳ 0 ≡ downFrom (suc n) - reverse-selfInverse : SelfInverse {A = List A} _≡_ reverse - reverse-applyUpTo : reverse (applyUpTo f n) ≡ applyDownFrom f n - reverse-upTo : reverse (upTo n) ≡ downFrom n - reverse-applyDownFrom : reverse (applyDownFrom f n) ≡ applyUpTo f n - reverse-downFrom : reverse (downFrom n) ≡ upTo n - mapMaybe-map : mapMaybe f ∘ map g ≗ mapMaybe (f ∘ g) - map-mapMaybe : map g ∘ mapMaybe f ≗ mapMaybe (Maybe.map g ∘ f) - align-map : align (map f xs) (map g ys) ≡ map (map f g) (align xs ys) - zip-map : zip (map f xs) (map g ys) ≡ map (map f g) (zip xs ys) - unzipWith-map : unzipWith f ∘ map g ≗ unzipWith (f ∘ g) - map-unzipWith : map (map g) (map h) ∘ unzipWith f ≗ unzipWith (map g h ∘ f) - unzip-map : unzip ∘ map (map f g) ≗ map (map f) (map g) ∘ unzip - splitAt-map : splitAt n ∘ map f ≗ map (map f) (map f) ∘ splitAt n - uncons-map : uncons ∘ map f ≗ map (map f (map f)) ∘ uncons - last-map : last ∘ map f ≗ map f ∘ last - tail-map : tail ∘ map f ≗ map (map f) ∘ tail - mapMaybe-cong : f ≗ g → mapMaybe f ≗ mapMaybe g - zipWith-cong : (∀ a b → f a b ≡ g a b) → ∀ as → zipWith f as ≗ zipWith g as - unzipWith-cong : f ≗ g → unzipWith f ≗ unzipWith g - foldl-cong : (∀ x y → f x y ≡ g x y) → ∀ x → foldl f x ≗ foldl g x - alignWith-flip : alignWith f xs ys ≡ alignWith (f ∘ swap) ys xs - alignWith-comm : f ∘ swap ≗ f → alignWith f xs ys ≡ alignWith f ys xs - align-flip : align xs ys ≡ map swap (align ys xs) - zip-flip : zip xs ys ≡ map swap (zip ys xs) - unzipWith-swap : unzipWith (swap ∘ f) ≗ swap ∘ unzipWith f - unzip-swap : unzip ∘ map swap ≗ swap ∘ unzip - take-take : take n (take m xs) ≡ take (n ⊓ m) xs - take-drop : take n (drop m xs) ≡ drop m (take (m + n) xs) - zip-unzip : uncurry′ zip ∘ unzip ≗ id - unzipWith-zipWith : f ∘ uncurry′ g ≗ id → length xs ≡ length ys → unzipWith f (zipWith g xs ys) ≡ (xs , ys) - unzip-zip : length xs ≡ length ys → unzip (zip xs ys) ≡ (xs , ys) - mapMaybe-++ : mapMaybe f (xs ++ ys) ≡ mapMaybe f xs ++ mapMaybe f ys - unzipWith-++ : unzipWith f (xs ++ ys) ≡ zip _++_ _++_ (unzipWith f xs) (unzipWith f ys) - catMaybes-concatMap : catMaybes ≗ concatMap fromMaybe - catMaybes-++ : catMaybes (xs ++ ys) ≡ catMaybes xs ++ catMaybes ys - map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f) - ``` - -* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`: - ```agda - ⊆-trans-idˡ : (trans-reflˡ : ∀ {x y} (p : x ≈ y) → trans ≈-refl p ≡ p) → - (pxs : xs ⊆ ys) → ⊆-trans ⊆-refl pxs ≡ pxs - ⊆-trans-idʳ : (trans-reflʳ : ∀ {x y} (p : x ≈ y) → trans p ≈-refl ≡ p) → - (pxs : xs ⊆ ys) → ⊆-trans pxs ⊆-refl ≡ pxs - ⊆-trans-assoc : (≈-assoc : ∀ {w x y z} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z) → - trans p (trans q r) ≡ trans (trans p q) r) → - (ps : as ⊆ bs) (qs : bs ⊆ cs) (rs : cs ⊆ ds) → - ⊆-trans ps (⊆-trans qs rs) ≡ ⊆-trans (⊆-trans ps qs) rs - ``` - -* In `Data.List.Relation.Binary.Subset.Setoid.Properties`: - ```agda - map⁺ : f Preserves _≈_ ⟶ _≈′_ → as ⊆ bs → map f as ⊆′ map f bs - - reverse-selfAdjoint : as ⊆ reverse bs → reverse as ⊆ bs - reverse⁺ : as ⊆ bs → reverse as ⊆ reverse bs - reverse⁻ : reverse as ⊆ reverse bs → as ⊆ bs - ``` - -* In `Data.List.Relation.Unary.All.Properties`: - ```agda - All-catMaybes⁺ : All (Maybe.All P) xs → All P (catMaybes xs) - Any-catMaybes⁺ : All (Maybe.Any P) xs → All P (catMaybes xs) - ``` - -* In `Data.List.Relation.Unary.AllPairs.Properties`: - ```agda - catMaybes⁺ : AllPairs (Pointwise R) xs → AllPairs R (catMaybes xs) - tabulate⁺-< : (i < j → R (f i) (f j)) → AllPairs R (tabulate f) - ``` - -* In `Data.List.Relation.Ternary.Appending.Setoid.Properties`: - ```agda - through→ : ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs → - ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs - through← : ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs → - ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs - assoc→ : ∃[ xs ] Appending as bs xs × Appending xs cs ds → - ∃[ ys ] Appending bs cs ys × Appending as ys ds - ``` - -* In `Data.List.Relation.Ternary.Appending.Properties`: - ```agda - through→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) → - ∃[ xs ] Pointwise U as xs × Appending V R xs bs cs → - ∃[ ys ] Appending W S as bs ys × Pointwise T ys cs - through← : ((R ; S) ⇒ T) → ((U ; S) ⇒ (V ; W)) → - ∃[ ys ] Appending U R as bs ys × Pointwise S ys cs → - ∃[ xs ] Pointwise V as xs × Appending W T xs bs cs - assoc→ : (R ⇒ (S ; T)) → ((U ; V) ⇒ (W ; T)) → ((Y ; V) ⇒ X) → - ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds → - ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds - assoc← : ((S ; T) ⇒ R) → ((W ; T) ⇒ (U ; V)) → (X ⇒ (Y ; V)) → - ∃[ ys ] Appending W S bs cs ys × Appending X T as ys ds → - ∃[ xs ] Appending Y U as bs xs × Appending V R xs cs ds - ``` - -* In `Data.List.Relation.Binary.Pointwise.Base`: - ```agda - unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S) - ``` - -* In `Data.Maybe.Relation.Binary.Pointwise`: - ```agda - pointwise⊆any : Pointwise R (just x) ⊆ Any (R x) - ``` - -* In `Data.List.Relation.Binary.Sublist.Setoid`: - ```agda - ⊆-upper-bound : ∀ {xs ys zs} (τ : xs ⊆ zs) (σ : ys ⊆ zs) → UpperBound τ σ - ``` - -* In `Data.Nat.Divisibility`: - ```agda - quotient≢0 : m ∣ n → .{{NonZero n}} → NonZero quotient - - m∣n⇒n≡quotient*m : m ∣ n → n ≡ quotient * m - m∣n⇒n≡m*quotient : m ∣ n → n ≡ m * quotient - quotient-∣ : m ∣ n → quotient ∣ n - quotient>1 : m ∣ n → m < n → 1 < quotient - quotient-< : m ∣ n → .{{NonTrivial m}} → .{{NonZero n}} → quotient < n - n/m≡quotient : m ∣ n → .{{_ : NonZero m}} → n / m ≡ quotient - - m/n≡0⇒m⇒prime : .{{NonTrivial n}} → m Rough n → m * m > n → Prime n - productOfPrimes≢0 : All Prime as → NonZero (product as) - productOfPrimes≥1 : All Prime as → product as ≥ 1 - ``` - -* Added new proofs to `Data.List.Relation.Binary.Permutation.Propositional.Properties`: - ```agda - product-↭ : product Preserves _↭_ ⟶ _≡_ - ``` - -* In `Data.Rational.Properties`: - ```agda - 1≢0 : 1ℚ ≢ 0ℚ - - #⇒invertible : p ≢ q → Invertible 1ℚ _*_ (p - q) - invertible⇒# : Invertible 1ℚ _*_ (p - q) → p ≢ q - - isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ - isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ - heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ - heytingField : HeytingField 0ℓ 0ℓ 0ℓ - ``` - -* Added new functions in `Data.String.Base`: - ```agda - map : (Char → Char) → String → String - between : String → String → String → String - ``` - -* Re-exported new types and functions in `IO`: - ```agda - BufferMode : Set - noBuffering : BufferMode - lineBuffering : BufferMode - blockBuffering : Maybe ℕ → BufferMode - Handle : Set - stdin : Handle - stdout : Handle - stderr : Handle - hSetBuffering : Handle → BufferMode → IO ⊤ - hGetBuffering : Handle → IO BufferMode - hFlush : Handle → IO ⊤ - ``` - -* Added new functions in `IO.Base`: - ```agda - whenInj₂ : E ⊎ A → (A → IO ⊤) → IO ⊤ - forever : IO ⊤ → IO ⊤ - ``` - -* In `IO.Primitive.Core`: - ```agda - _>>_ : IO A → IO B → IO B - ``` - -* In `Data.Word.Base`: - ```agda - _≤_ : Rel Word64 zero - ``` - -* Added new definition in `Relation.Binary.Construct.Closure.Transitive` - ```agda - transitive⁻ : Transitive _∼_ → TransClosure _∼_ ⇒ _∼_ - ``` - -* Added new definition in `Relation.Unary` - ``` - Stable : Pred A ℓ → Set _ - ``` - -* In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can - be used infix. - -* Added new proofs in `Relation.Binary.Construct.Composition`: - ```agda - transitive⇒≈;≈⊆≈ : Transitive ≈ → (≈ ; ≈) ⇒ ≈ - ``` - -* Added new definitions in `Relation.Binary.Definitions` - ``` - Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y) - Empty _∼_ = ∀ {x y} → x ∼ y → ⊥ - ``` - -* Added new proofs in `Relation.Binary.Properties.Setoid`: - ```agda - ≉-irrefl : Irreflexive _≈_ _≉_ - ≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_ - ≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_ - ``` - -* Added new definitions in `Relation.Nullary` - ``` - Recomputable : Set _ - WeaklyDecidable : Set _ - ``` - -* Added new proof in `Relation.Nullary.Decidable`: - ```agda - ⌊⌋-map′ : (a? : Dec A) → ⌊ map′ t f a? ⌋ ≡ ⌊ a? ⌋ - ``` - -* Added new definitions in `Relation.Unary` - ``` - Stable : Pred A ℓ → Set _ - WeaklyDecidable : Pred A ℓ → Set _ - ``` - -* Enhancements to `Tactic.Cong` - see `README.Tactic.Cong` for details. - - Provide a marker function, `⌞_⌟`, for user-guided anti-unification. - - Improved support for equalities between terms with instance arguments, - such as terms that contain `_/_` or `_%_`. From 00421a6334d4bd7581f013cde9dc33b07e36945a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 28 Jul 2024 10:58:52 +0100 Subject: [PATCH 25/25] update `CHANGELOG` --- CHANGELOG.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 80da9ee48e..44330832ae 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -24,5 +24,14 @@ Deprecated names New modules ----------- +* Isomorphism between `Fin` and an 'obvious' definition `ℕ<` of + 'bounded natural number' type, in: + ```agda + Data.Nat.Bounded + Data.Nat.Bounded.Base + Data.Nat.Bounded.Literals + Data.Nat.Bounded.Properties + ``` + Additions to existing modules -----------------------------