Add left- and right- Pointwise congruence for _++_ on List

CHANGELOG.md

@@ -32,6 +32,18 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Data.List.Relation.Binary.Equality.Setoid`:
+  ```agda
+  ++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs
+  ++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs
+  ```
+
+* In `Data.List.Relation.Binary.Pointwise`:
+  ```agda
+  ++⁺ʳ : Reflexive R → ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R)
+  ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
+  ```
+
 * New lemma in `Data.Vec.Properties`:
   ```agda
   map-concat : map f (concat xss) ≡ concat (map (map f) xss)

src/Data/List/Relation/Binary/Equality/Setoid.agda

@@ -29,6 +29,8 @@ open Setoid S renaming (Carrier to A)
 private
   variable
     p q : Level
+    ws xs xs′ ys ys′ zs : List A
+    xss yss : List (List A)
 
 ------------------------------------------------------------------------
 -- Definition of equality
@@ -113,9 +115,15 @@ foldr⁺ ∙⇔◦ e≈f xs≋ys = PW.foldr⁺ ∙⇔◦ e≈f xs≋ys
 ------------------------------------------------------------------------
 -- _++_
 
-++⁺ : ∀ {ws xs ys zs} → ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs
+++⁺ : ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs
 ++⁺ = PW.++⁺
 
+++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs
+++⁺ʳ xs = PW.++⁺ʳ refl xs
+
+++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs
+++⁺ˡ zs = PW.++⁺ˡ refl zs
+
 ++-cancelˡ : ∀ xs {ys zs} → xs ++ ys ≋ xs ++ zs → ys ≋ zs
 ++-cancelˡ xs = PW.++-cancelˡ xs
 
@@ -125,7 +133,7 @@ foldr⁺ ∙⇔◦ e≈f xs≋ys = PW.foldr⁺ ∙⇔◦ e≈f xs≋ys
 ------------------------------------------------------------------------
 -- concat
 
-concat⁺ : ∀ {xss yss} → Pointwise _≋_ xss yss → concat xss ≋ concat yss
+concat⁺ : Pointwise _≋_ xss yss → concat xss ≋ concat yss
 concat⁺ = PW.concat⁺
 
 ------------------------------------------------------------------------
@@ -146,14 +154,14 @@ module _ {n} {f g : Fin n → A}
 module _ {P : Pred A p} (P? : U.Decidable P) (resp : P Respects _≈_)
   where
 
-  filter⁺ : ∀ {xs ys} → xs ≋ ys → filter P? xs ≋ filter P? ys
+  filter⁺ : xs ≋ ys → filter P? xs ≋ filter P? ys
   filter⁺ xs≋ys = PW.filter⁺ P? P? resp (resp ∘ sym) xs≋ys
 
 ------------------------------------------------------------------------
 -- reverse
 
-ʳ++⁺ : ∀{xs xs′ ys ys′} → xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′
+ʳ++⁺ : xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′
 ʳ++⁺ = PW.ʳ++⁺
 
-reverse⁺ : ∀ {xs ys} → xs ≋ ys → reverse xs ≋ reverse ys
+reverse⁺ : xs ≋ ys → reverse xs ≋ reverse ys
 reverse⁺ = PW.reverse⁺

src/Data/List/Relation/Binary/Pointwise.agda

@@ -26,7 +26,7 @@ open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec using (map′)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary.Core renaming (Rel to Rel₂)
-open import Relation.Binary.Definitions using (_Respects_; _Respects₂_)
+open import Relation.Binary.Definitions using (Reflexive; _Respects_; _Respects₂_)
 open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; Poset)
 open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence; IsPartialOrder; IsPreorder)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
@@ -166,6 +166,15 @@ tabulate⁻ {n = suc n} (x∼y ∷ xs∼ys) (fsuc i) = tabulate⁻ xs∼ys i
 ++-cancelʳ {xs = xs}     (y ∷ ys) []       eq   =
   contradiction (≡.trans (≡.sym (length-++ (y ∷ ys))) (Pointwise-length eq)) (m≢1+n+m (length xs) ∘ ≡.sym)
 
+module _ (rfl : Reflexive R) where
+
+  ++⁺ʳ : ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R)
+  ++⁺ʳ xs = ++⁺ (refl rfl)
+
+  ++⁺ˡ : ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R)
+  ++⁺ˡ zs rs = ++⁺ rs (refl rfl)
+
+
 ------------------------------------------------------------------------
 -- concat
 
@@ -261,8 +270,7 @@ lookup⁺ (_   ∷ Rxys) (fsuc i) = lookup⁺ Rxys i
 
 Pointwise-≡⇒≡ : Pointwise {A = A} _≡_ ⇒ _≡_
 Pointwise-≡⇒≡ []               = ≡.refl
-Pointwise-≡⇒≡ (≡.refl ∷ xs∼ys) with Pointwise-≡⇒≡ xs∼ys
-... | ≡.refl = ≡.refl
+Pointwise-≡⇒≡ (≡.refl ∷ xs∼ys) = ≡.cong (_ ∷_) (Pointwise-≡⇒≡ xs∼ys)
 
 ≡⇒Pointwise-≡ :  _≡_ ⇒ Pointwise {A = A} _≡_
 ≡⇒Pointwise-≡ ≡.refl = refl ≡.refl