[ new ] associativity of Appending (#2023)

* [ new ] associativity of Appending

* Removed unneeded variable

* Renamed Product module

---------

Co-authored-by: MatthewDaggitt <[email protected]>

CHANGELOG.md

@@ -13,6 +13,9 @@ Bug-fixes
   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`.
+
 Non-backwards compatible changes
 --------------------------------
 
@@ -131,6 +134,37 @@ Additions to existing modules
   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)
@@ -176,6 +210,12 @@ Additions to existing modules
   Stable          : Pred A ℓ → Set _
   ```
 
+* Added new proofs in `Relation.Binary.Properties.Setoid`:
+  ```agda
+  ≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_
+  ≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_
+  ```
+
 * Added new definitions in `Relation.Nullary`
   ```
   Recomputable    : Set _

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

@@ -8,16 +8,16 @@
 
 module Data.List.Relation.Binary.Pointwise.Base where
 
-open import Data.Product.Base using (_×_; <_,_>)
+open import Data.Product.Base as Product using (_×_; _,_; <_,_>; ∃-syntax)
 open import Data.List.Base using (List; []; _∷_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (REL; _⇒_)
+open import Relation.Binary.Construct.Composition using (_;_)
 
 private
   variable
     a b c ℓ : Level
-    A : Set a
-    B : Set b
+    A B : Set a
     x y : A
     xs ys : List A
     R S : REL A B ℓ
@@ -58,3 +58,8 @@ rec P c n (Rxy ∷ Rxsys) = c Rxy (rec P c n Rxsys)
 map : R ⇒ S → Pointwise R ⇒ Pointwise S
 map R⇒S []            = []
 map R⇒S (Rxy ∷ Rxsys) = R⇒S Rxy ∷ map R⇒S Rxsys
+
+unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S)
+unzip [] = [] , [] , []
+unzip ((y , r , s) ∷ xs∼ys) =
+  Product.map (y ∷_) (Product.map (r ∷_) (s ∷_)) (unzip xs∼ys)

src/Data/List/Relation/Ternary/Appending/Properties.agda

@@ -10,48 +10,89 @@ module Data.List.Relation.Ternary.Appending.Properties where
 
 open import Data.List.Base using (List; [])
 open import Data.List.Relation.Ternary.Appending
+open import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise; []; _∷_)
+open import Data.Product.Base as Product using (∃-syntax; _×_; _,_)
+open import Function.Base using (id)
 open import Data.List.Relation.Binary.Pointwise.Base as Pw using (Pointwise; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise.Properties as Pw using (transitive)
 open import Level using (Level)
-open import Relation.Binary.Core using (REL; Rel)
+open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Definitions using (Trans)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+open import Relation.Binary.Construct.Composition using (_;_)
 
 private
   variable
-    a a′ b b′ c c′ l r : Level
-    A : Set a
-    A′ : Set a′
-    B : Set b
-    B′ : Set b′
-    C : Set c
-    C′ : Set c′
-    L : REL A C l
-    R : REL B C r
-    as : List A
-    bs : List B
-    cs : List C
-
-module _  {e} {E : REL C C′ e} {L′ : REL A C′ l} {R′ : REL B C′ r}
-          (LEL′ : Trans L E L′) (RER′ : Trans R E R′)
-          where
+    a ℓ l r : Level
+    A A′ B B′ C C′ D D′ : Set a
+    R S T U V W X Y : REL A B ℓ
+    as bs cs ds : List A
+
+module _  (RST : Trans R S T) (USV : Trans U S V) where
 
-  respʳ-≋ : ∀ {cs′} → Appending L R as bs cs → Pointwise E cs cs′ → Appending L′ R′ as bs cs′
-  respʳ-≋ ([]++ rs) es       = []++ Pw.transitive RER′ rs es
-  respʳ-≋ (l ∷ lrs) (e ∷ es) = LEL′ l e ∷ respʳ-≋ lrs es
+  respʳ-≋ : Appending R U as bs cs → Pointwise S cs ds → Appending T V as bs ds
+  respʳ-≋ ([]++ rs) es       = []++ Pw.transitive USV rs es
+  respʳ-≋ (l ∷ lrs) (e ∷ es) = RST l e ∷ respʳ-≋ lrs es
 
-module _  {eᴬ eᴮ} {Eᴬ : REL A′ A eᴬ} {Eᴮ : REL B′ B eᴮ}
-          {L′ : REL A′ C l} (ELL′ : Trans Eᴬ L L′)
-          {R′ : REL B′ C r} (ERR′ : Trans Eᴮ R R′)
+module _  {T : REL A B l} (RST : Trans R S T)
+          {W : REL A B r} (ERW : Trans U V W)
           where
 
-  respˡ-≋ : ∀ {as′ bs′} → Pointwise Eᴬ as′ as → Pointwise Eᴮ bs′ bs →
-            Appending L R as bs cs → Appending L′ R′ as′ bs′ cs
-  respˡ-≋ []         esʳ ([]++ rs) = []++ Pw.transitive ERR′ esʳ rs
-  respˡ-≋ (eˡ ∷ esˡ) esʳ (l ∷ lrs) = ELL′ eˡ l ∷ respˡ-≋ esˡ esʳ lrs
+  respˡ-≋ : ∀ {as′ bs′} → Pointwise R as′ as → Pointwise U bs′ bs →
+            Appending S V as bs cs → Appending T W as′ bs′ cs
+  respˡ-≋ []         esʳ ([]++ rs) = []++ Pw.transitive ERW esʳ rs
+  respˡ-≋ (eˡ ∷ esˡ) esʳ (l ∷ lrs) = RST eˡ l ∷ respˡ-≋ esˡ esʳ lrs
 
-conicalˡ : Appending L R as bs [] → as ≡ []
+conicalˡ : Appending R S as bs [] → as ≡ []
 conicalˡ ([]++ rs) = refl
 
-conicalʳ : Appending L R as bs [] → bs ≡ []
+conicalʳ : Appending R S as bs [] → bs ≡ []
 conicalʳ ([]++ []) = refl
+
+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→ f g (_ , [] , []++ rs) =
+  let _ , rs′ , ps′ = Pw.unzip (Pw.map f rs) in
+  _ , []++ rs′ , ps′
+through→ f g (_ , p ∷ ps , l ∷ lrs) =
+  let _ , l′ , p′ = g (_ , p , l) in
+  Product.map _ (Product.map (l′ ∷_) (p′ ∷_)) (through→ f g (_ , ps , lrs))
+
+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
+through← f g (_ , []++ rs′ , ps′) =
+  _ , [] , []++ (Pw.transitive (λ r′ p′ → f (_ , r′ , p′)) rs′ ps′)
+through← f g (_ , l′ ∷ lrs′ , p′ ∷ ps′) =
+  let _ , p , l = g (_ , l′ , p′) in
+  Product.map _ (Product.map (p ∷_) (l ∷_)) (through← f g (_ , lrs′ , ps′))
+
+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→ f g h (_ , []++ rs , lrs′) =
+  let _ , mss , ss′ = through→ f g (_ , rs , lrs′) in
+  _ , mss , []++ ss′
+assoc→ f g h (_ , l ∷ lrs , l′ ∷ lrs′) =
+  Product.map₂ (Product.map₂ (h (_ , l , l′) ∷_)) (assoc→ f g h (_ , lrs , lrs′))
+
+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
+assoc← f g h (_ , mss , []++ ss′) =
+  let _ , rs , lrs′ = through← f g (_ , mss , ss′) in
+  _ , []++ rs , lrs′
+assoc← f g h (_ , mss , m′ ∷ mss′) =
+  let _ , l , l′ = h m′ in
+  Product.map _ (Product.map (l ∷_) (l′ ∷_)) (assoc← f g h (_ , mss , mss′))

src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda

@@ -8,27 +8,33 @@
 
 open import Relation.Binary.Bundles using (Setoid)
 
-module Data.List.Relation.Ternary.Appending.Setoid.Properties {c l} (S : Setoid c l) where
+module Data.List.Relation.Ternary.Appending.Setoid.Properties
+  {c l} (S : Setoid c l)
+  where
 
 open import Data.List.Base as List using (List; [])
 import Data.List.Properties as Listₚ
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
 import Data.List.Relation.Ternary.Appending.Properties as Appendingₚ
-open import Data.Product.Base using (_,_)
+open import Data.Product using (∃-syntax; _×_; _,_)
+open import Function.Base using (id)
+open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
+open import Relation.Binary.Construct.Composition using (_;_)
 
+open Setoid S renaming (Carrier to A)
+open import Relation.Binary.Properties.Setoid S using (≈;≈⇒≈; ≈⇒≈;≈)  
 open import Data.List.Relation.Ternary.Appending.Setoid S
-module S = Setoid S; open S renaming (Carrier to A) using (_≈_)
 
 private
   variable
-    as bs cs : List A
+    as bs cs ds : List A
 
 ------------------------------------------------------------------------
 -- Re-exporting existing properties
 
 open Appendingₚ public
-  hiding (respʳ-≋; respˡ-≋)
+  using (conicalˡ; conicalʳ)
 
 ------------------------------------------------------------------------
 -- Proving setoid-specific ones
@@ -44,8 +50,23 @@ open Appendingₚ public
 
 respʳ-≋ : ∀ {cs′} → Appending as bs cs → Pointwise _≈_ cs cs′ →
           Appending as bs cs′
-respʳ-≋ = Appendingₚ.respʳ-≋ S.trans S.trans
+respʳ-≋ = Appendingₚ.respʳ-≋ trans trans
 
 respˡ-≋ : ∀ {as′ bs′} → Pointwise _≈_ as′ as → Pointwise _≈_ bs′ bs →
           Appending as bs cs → Appending as′ bs′ cs
-respˡ-≋ = Appendingₚ.respˡ-≋ S.trans S.trans
+respˡ-≋ = Appendingₚ.respˡ-≋ trans trans
+
+through→ :
+  ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs →
+  ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs
+through→ = Appendingₚ.through→ ≈⇒≈;≈ id
+
+through← :
+  ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs →
+  ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs
+through← = Appendingₚ.through← ≈;≈⇒≈ id
+
+assoc→ :
+  ∃[ xs ] Appending as bs xs × Appending xs cs ds →
+  ∃[ ys ] Appending bs cs ys × Appending as ys ds
+assoc→ = Appendingₚ.assoc→ ≈⇒≈;≈ id ≈;≈⇒≈

src/Relation/Binary/Properties/Setoid.agda

@@ -9,11 +9,13 @@
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘_; id; _$_; flip)
 open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.Bundles using (Setoid; Preorder; Poset)
 open import Relation.Binary.Definitions
   using (Symmetric; _Respectsˡ_; _Respectsʳ_; _Respects₂_)
 open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder)
+open import Relation.Binary.Construct.Composition using (_;_)
 
 module Relation.Binary.Properties.Setoid {a ℓ} (S : Setoid a ℓ) where
 
@@ -77,6 +79,15 @@ preorder = record
 ≉-resp₂ : _≉_ Respects₂ _≈_
 ≉-resp₂ = ≉-respʳ , ≉-respˡ
 
+------------------------------------------------------------------------
+-- Equality is closed under composition
+
+≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_
+≈;≈⇒≈ (_ , p , q) = trans p q
+
+≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_
+≈⇒≈;≈ q = _ , q , refl
+
 ------------------------------------------------------------------------
 -- Other properties