Data.List.Base.reverse is self adjoint wrt Data.List.Relation.Binary.Subset.Setoid._⊆_ (#2378)

* `reverse` is `SelfInverse`

* use `Injective` for `reverse-injective`

* fixes #2353

* combinatory form

* removed redundant implicits

* added comment on unit/counit of the adjunction

Author: jamesmckinna

CHANGELOG.md

@@ -329,13 +329,20 @@ 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
   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
@@ -373,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)

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
 

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 : Injective {A = List A} _≡_ _≡_ reverse
+reverse-injective = selfInverse⇒injective reverse-selfInverse
 
 -- reverse preserves length.
 

src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda

@@ -10,18 +10,19 @@ 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
 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,13 +210,47 @@ 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 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 ⟩
+    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
 
 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