From 03dcf080ac322bc0776bd8c7ab762813f9b2d809 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 24 Oct 2022 16:38:08 +0200 Subject: [PATCH 1/5] Add raw bundles to Data.List.Base --- CHANGELOG.md | 4 +++- src/Data/List/Base.agda | 20 ++++++++++++++++++++ 2 files changed, 23 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 02014e8d9f..0725baeb62 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1689,10 +1689,12 @@ Other minor changes deduplicateᵇ : (A → A → Bool) → List A → List A ``` -* Added new functions to `Data.List.Base`: +* Added new functions and definitions to `Data.List.Base`: ```agda catMaybes : List (Maybe A) → List A ap : List (A → B) → List A → List B + ++-rawMagma : Set a → RawMagma a _ + ++-rawMonoid : Set a → RawMonoid a _ ``` * Added new proofs in `Data.List.Relation.Binary.Lex.Strict`: diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 3ab3c2f923..2cee335208 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -11,6 +11,7 @@ module Data.List.Base where +open import Algebra.Bundles.Raw using (RawMagma; RawMonoid) open import Data.Bool.Base as Bool using (Bool; false; true; not; _∧_; _∨_; if_then_else_) open import Data.Fin.Base using (Fin; zero; suc) @@ -27,6 +28,7 @@ open import Relation.Unary using (Pred; Decidable) open import Relation.Unary.Properties using (∁?) open import Relation.Binary.Core using (Rel) import Relation.Binary.Definitions as B +open import Relation.Binary.PropositionalEquality.Core using (_≡_) private variable @@ -463,6 +465,24 @@ infixl 6 _∷ʳ?_ _∷ʳ?_ : List A → Maybe A → List A xs ∷ʳ? x = maybe′ (xs ∷ʳ_) xs x +------------------------------------------------------------------------ +-- Raw algebraic bundles + +module _ (A : Set a) where + ++-rawMagma : RawMagma a _ + ++-rawMagma = record + { Carrier = List A + ; _≈_ = _≡_ + ; _∙_ = _++_ + } + + ++-[]-rawMonoid : RawMonoid a _ + ++-[]-rawMonoid = record + { Carrier = List A + ; _≈_ = _≡_ + ; _∙_ = _++_ + ; ε = [] + } ------------------------------------------------------------------------ -- DEPRECATED From e7c4eca1ea50d46e68aa14440aebfbfc6b510878 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 24 Oct 2022 16:38:33 +0200 Subject: [PATCH 2/5] Add proofs that length is a magma/monoid homomorphism --- CHANGELOG.md | 3 +++ src/Data/List/Properties.agda | 16 ++++++++++++++++ 2 files changed, 19 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0725baeb62..f2ee6b8282 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1727,6 +1727,9 @@ Other minor changes concatMap-pure : concatMap [_] ≗ id concatMap-map : concatMap g (map f xs) ≡ concatMap (g ∘′ f) xs map-concatMap : map f ∘′ concatMap g ≗ concatMap (map f ∘′ g) + + length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length + length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-rawMagma length ``` * Added new patterns and definitions to `Data.Nat.Base`: diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index d2866cfa81..3282f75a72 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -13,6 +13,7 @@ module Data.List.Properties where open import Algebra.Bundles open import Algebra.Definitions as AlgebraicDefinitions using (Involutive) +open import Algebra.Morphism.Structures using (IsMagmaHomomorphism; IsMonoidHomomorphism) import Algebra.Structures as AlgebraicStructures open import Data.Bool.Base using (Bool; false; true; not; if_then_else_) open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ) @@ -240,6 +241,21 @@ module _ (A : Set a) where ; isMonoid = ++-isMonoid } +module _ (A : Set a) where + length-isMagmaHomomorphism : IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length + length-isMagmaHomomorphism = record + { isRelHomomorphism = record + { cong = cong length + } + ; homo = λ xs ys → length-++ xs {ys} + } + + length-isMonoidHomomorphism : IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length + length-isMonoidHomomorphism = record + { isMagmaHomomorphism = length-isMagmaHomomorphism + ; ε-homo = refl + } + ------------------------------------------------------------------------ -- alignWith From 3d145f9f6db5cbd170b8563e855a97f1be20c5dc Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 24 Oct 2022 16:53:04 +0200 Subject: [PATCH 3/5] Fix error in changelog --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f2ee6b8282..3bdf5abdab 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1694,7 +1694,7 @@ Other minor changes catMaybes : List (Maybe A) → List A ap : List (A → B) → List A → List B ++-rawMagma : Set a → RawMagma a _ - ++-rawMonoid : Set a → RawMonoid a _ + ++-[]-rawMonoid : Set a → RawMonoid a _ ``` * Added new proofs in `Data.List.Relation.Binary.Lex.Strict`: From ece93f83413997f2ee4f0a6fb33b76cbb815366e Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 24 Oct 2022 20:07:39 +0200 Subject: [PATCH 4/5] Another typo fix --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3bdf5abdab..fd80f6ad53 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1729,7 +1729,7 @@ Other minor changes map-concatMap : map f ∘′ concatMap g ≗ concatMap (map f ∘′ g) length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length - length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-rawMagma length + length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length ``` * Added new patterns and definitions to `Data.Nat.Base`: From 220cec21d1fd2a18b898020f5e41d782aa1af893 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 25 Oct 2022 07:34:30 +0200 Subject: [PATCH 5/5] Add a blank line after the module declaration --- src/Data/List/Properties.agda | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 3282f75a72..5cfc4b3635 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -242,6 +242,7 @@ module _ (A : Set a) where } module _ (A : Set a) where + length-isMagmaHomomorphism : IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length length-isMagmaHomomorphism = record { isRelHomomorphism = record