From 7cd23e28a373d9e4251e69fd1cf0005dba96635a Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 2 May 2024 07:58:09 +0100 Subject: [PATCH 1/6] `reverse` is `SelfInverse` --- CHANGELOG.md | 1 + src/Data/List/Properties.agda | 27 ++++++++++++++++++--------- 2 files changed, 19 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 895a3ad3bd..b6cf5c9771 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -336,6 +336,7 @@ Additions to existing modules 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 diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index dc7e8e5831..737ed8924c 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -12,7 +12,9 @@ module Data.List.Properties where open import Algebra.Bundles -open import Algebra.Definitions as AlgebraicDefinitions using (Involutive) +open import Algebra.Consequences.Propositional + using (selfInverse⇒involutive; selfInverse⇒injective) +open import Algebra.Definitions as AlgebraicDefinitions using (SelfInverse; 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_) @@ -1350,7 +1352,7 @@ foldl-ʳ++ f b (x ∷ xs) {ys} = begin unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x unfold-reverse x xs = ʳ++-defn xs --- reverse is an involution with respect to append. +-- reverse is an anti-homomorphism with respect to append. reverse-++ : (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs @@ -1361,20 +1363,27 @@ reverse-++ xs ys = begin ys ʳ++ reverse xs ≡⟨ ʳ++-defn ys ⟩ reverse ys ++ reverse xs ∎ +-- reverse is self-inverse. + +reverse-selfInverse : SelfInverse {A = List A} _≡_ reverse +reverse-selfInverse {x = xs} {y = ys} xs⁻¹≈ys = begin + reverse ys ≡⟨⟩ + ys ʳ++ [] ≡⟨ cong (_ʳ++ []) xs⁻¹≈ys ⟨ + reverse xs ʳ++ [] ≡⟨⟩ + (xs ʳ++ []) ʳ++ [] ≡⟨ ʳ++-ʳ++ xs ⟩ + [] ʳ++ xs ++ [] ≡⟨⟩ + xs ++ [] ≡⟨ ++-identityʳ xs ⟩ + xs ∎ + -- reverse is involutive. reverse-involutive : Involutive {A = List A} _≡_ reverse -reverse-involutive xs = begin - reverse (reverse xs) ≡⟨⟩ - (xs ʳ++ []) ʳ++ [] ≡⟨ ʳ++-ʳ++ xs ⟩ - [] ʳ++ xs ++ [] ≡⟨⟩ - xs ++ [] ≡⟨ ++-identityʳ xs ⟩ - xs ∎ +reverse-involutive = selfInverse⇒involutive reverse-selfInverse -- reverse is injective. reverse-injective : ∀ {xs ys : List A} → reverse xs ≡ reverse ys → xs ≡ ys -reverse-injective = subst₂ _≡_ (reverse-involutive _) (reverse-involutive _) ∘ cong reverse +reverse-injective = selfInverse⇒injective reverse-selfInverse -- reverse preserves length. From 6057d9237016f50bb6088e7f6d72333b00a25bd6 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 2 May 2024 11:54:18 +0100 Subject: [PATCH 2/6] use `Injective` for `reverse-injective` --- src/Data/List/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 737ed8924c..ab9b0241e1 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -1382,7 +1382,7 @@ reverse-involutive = selfInverse⇒involutive reverse-selfInverse -- reverse is injective. -reverse-injective : ∀ {xs ys : List A} → reverse xs ≡ reverse ys → xs ≡ ys +reverse-injective : Injective {A = List A} _≡_ _≡_ reverse reverse-injective = selfInverse⇒injective reverse-selfInverse -- reverse preserves length. From 6e67ffd632528fd0745aac3ff86b9798beca685c Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 2 May 2024 17:59:51 +0100 Subject: [PATCH 3/6] fixes #2353 --- CHANGELOG.md | 13 +++++++ .../List/Membership/Setoid/Properties.agda | 13 +++++++ .../Binary/Subset/Setoid/Properties.agda | 36 +++++++++++++++++-- 3 files changed, 60 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b6cf5c9771..dfd81d2fa6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -329,6 +329,12 @@ Additions to existing modules i*j≢0 : .{{_ : NonZero i}} .{{_ : NonZero j}} → NonZero (i * j) ``` +* In `Data.List.Membership.Setoid.Properties`: + ```agda + reverse⁺ : x ∈ xs → x ∈ reverse xs + reverse⁻ : x ∈ reverse xs → x ∈ xs + ``` + * In `Data.List.Properties`: ```agda length-catMaybes : length (catMaybes xs) ≤ length xs @@ -374,6 +380,13 @@ Additions to existing modules map-catMaybes : map f ∘ catMaybes ≗ catMaybes ∘ map (Maybe.map f) ``` +* In `Data.List.Relation.Binary.Subset.Setoid.Properties`: + ```agda + 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) diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda index c06897367b..a0fcb4881b 100644 --- a/src/Data/List/Membership/Setoid/Properties.agda +++ b/src/Data/List/Membership/Setoid/Properties.agda @@ -238,6 +238,19 @@ module _ (S : Setoid c ℓ) where ∈-concat⁻′ xss v∈c[xss] with find (∈-concat⁻ xss v∈c[xss]) ... | xs , t , s = xs , s , t +------------------------------------------------------------------------ +-- reverse + +module _ (S : Setoid c ℓ) where + + open Membership S using (_∈_) + + reverse⁺ : ∀ {x xs} → x ∈ xs → x ∈ reverse xs + reverse⁺ = Any.reverse⁺ + + reverse⁻ : ∀ {x xs} → x ∈ reverse xs → x ∈ xs + reverse⁻ = Any.reverse⁻ + ------------------------------------------------------------------------ -- cartesianProductWith diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index bc1a693a2f..0dcfd9708a 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -10,10 +10,11 @@ module Data.List.Relation.Binary.Subset.Setoid.Properties where open import Data.Bool.Base using (Bool; true; false) open import Data.List.Base hiding (_∷ʳ_; find) +import Data.List.Properties as List open import Data.List.Relation.Unary.Any as Any using (Any; here; there) open import Data.List.Relation.Unary.All as All using (All) import Data.List.Membership.Setoid as Membership -open import Data.List.Membership.Setoid.Properties +import Data.List.Membership.Setoid.Properties as Membershipₚ open import Data.Nat.Base using (ℕ; s≤s; _≤_) import Data.List.Relation.Binary.Subset.Setoid as Subset import Data.List.Relation.Binary.Sublist.Setoid as Sublist @@ -21,7 +22,7 @@ import Data.List.Relation.Binary.Equality.Setoid as Equality import Data.List.Relation.Binary.Permutation.Setoid as Permutation import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutationₚ open import Data.Product.Base using (_,_) -open import Function.Base using (_∘_; _∘₂_) +open import Function.Base using (_∘_; _∘₂_; _$_) open import Level using (Level) open import Relation.Nullary using (¬_; does; yes; no) open import Relation.Nullary.Negation using (contradiction) @@ -49,6 +50,7 @@ module _ (S : Setoid a ℓ) where open Subset S open Equality S open Membership S + open Membershipₚ ⊆-reflexive : _≋_ ⇒ _⊆_ ⊆-reflexive xs≋ys = ∈-resp-≋ S xs≋ys @@ -167,6 +169,7 @@ module _ (S : Setoid a ℓ) where open Setoid S open Subset S open Membership S + open Membershipₚ xs⊆x∷xs : ∀ xs x → xs ⊆ x ∷ xs xs⊆x∷xs xs x = there @@ -186,6 +189,7 @@ module _ (S : Setoid a ℓ) where open Subset S open Membership S + open Membershipₚ xs⊆xs++ys : ∀ xs ys → xs ⊆ xs ++ ys xs⊆xs++ys xs ys = ∈-++⁺ˡ S @@ -206,6 +210,33 @@ module _ (S : Setoid a ℓ) where ++⁺ : ∀ {ws xs ys zs} → ws ⊆ xs → ys ⊆ zs → ws ++ ys ⊆ xs ++ zs ++⁺ ws⊆xs ys⊆zs = ⊆-trans S (++⁺ˡ _ ws⊆xs) (++⁺ʳ _ ys⊆zs) +------------------------------------------------------------------------ +-- reverse + +module _ (S : Setoid a ℓ) where + + open Setoid S renaming (Carrier to A) + open Subset S + + reverse-selfAdjoint : ∀ {as bs} → as ⊆ reverse bs → reverse as ⊆ bs + reverse-selfAdjoint {as = as} {bs = bs} rs x∈asʳ = reverse⁻ (rs (reverse⁻ x∈asʳ)) + where reverse⁻ = Membershipₚ.reverse⁻ S + + reverse⁺ : ∀ {as bs} → as ⊆ bs → reverse as ⊆ reverse bs + reverse⁺ {as} {bs} rs = reverse-selfAdjoint $ begin + as ⊆⟨ rs ⟩ + bs ≡⟨ List.reverse-involutive bs ⟨ + reverse (reverse bs) ∎ + where open ⊆-Reasoning S + + reverse⁻ : ∀ {as bs} → reverse as ⊆ reverse bs → as ⊆ bs + reverse⁻ {as} {bs} rs = begin + as ≡⟨ List.reverse-involutive as ⟨ + reverse (reverse as) ⊆⟨ reverse-selfAdjoint rs ⟩ + bs ∎ + where open ⊆-Reasoning S + + ------------------------------------------------------------------------ -- filter @@ -213,6 +244,7 @@ module _ (S : Setoid a ℓ) where open Setoid S renaming (Carrier to A) open Subset S + open Membershipₚ filter-⊆ : ∀ {P : Pred A p} (P? : Decidable P) → ∀ xs → filter P? xs ⊆ xs From 6bf1510766c9d1a1ddf5f76455e4aac5568426ee Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 2 May 2024 18:08:34 +0100 Subject: [PATCH 4/6] combinatory form --- src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index 0dcfd9708a..cdc3d67ffe 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -219,7 +219,7 @@ module _ (S : Setoid a ℓ) where open Subset S reverse-selfAdjoint : ∀ {as bs} → as ⊆ reverse bs → reverse as ⊆ bs - reverse-selfAdjoint {as = as} {bs = bs} rs x∈asʳ = reverse⁻ (rs (reverse⁻ x∈asʳ)) + reverse-selfAdjoint {as = as} {bs = bs} rs = reverse⁻ ∘ rs ∘ reverse⁻ where reverse⁻ = Membershipₚ.reverse⁻ S reverse⁺ : ∀ {as bs} → as ⊆ bs → reverse as ⊆ reverse bs From fcf90b08a1057fe89611d0b65017081f28cd6285 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Thu, 2 May 2024 18:27:50 +0100 Subject: [PATCH 5/6] removed redundant implicits --- src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index cdc3d67ffe..a5efb4cdf8 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -219,7 +219,7 @@ module _ (S : Setoid a ℓ) where open Subset S reverse-selfAdjoint : ∀ {as bs} → as ⊆ reverse bs → reverse as ⊆ bs - reverse-selfAdjoint {as = as} {bs = bs} rs = reverse⁻ ∘ rs ∘ reverse⁻ + reverse-selfAdjoint rs = reverse⁻ ∘ rs ∘ reverse⁻ where reverse⁻ = Membershipₚ.reverse⁻ S reverse⁺ : ∀ {as bs} → as ⊆ bs → reverse as ⊆ reverse bs From d1700698ba48a6e49a930736112119b56059bbc4 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 3 May 2024 15:00:20 +0100 Subject: [PATCH 6/6] added comment on unit/counit of the adjunction --- src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index a5efb4cdf8..f42bcd0012 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -222,6 +222,12 @@ module _ (S : Setoid a ℓ) where reverse-selfAdjoint rs = reverse⁻ ∘ rs ∘ reverse⁻ where reverse⁻ = Membershipₚ.reverse⁻ S +-- NB. the unit and counit of this adjunction are given by: +-- reverse-η : ∀ {xs} → xs ⊆ reverse xs +-- reverse-η = Membershipₚ.reverse⁺ S +-- reverse-ε : ∀ {xs} → reverse xs ⊆ xs +-- reverse-ε = Membershipₚ.reverse⁻ S + reverse⁺ : ∀ {as bs} → as ⊆ bs → reverse as ⊆ reverse bs reverse⁺ {as} {bs} rs = reverse-selfAdjoint $ begin as ⊆⟨ rs ⟩