[ new ] associativity of Appending

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
 --------------------------------
 
@@ -126,6 +129,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)
@@ -171,6 +205,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

@@ -12,13 +12,12 @@ open import Data.Product.Base as Σ 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
-    C : Set c
+    A B : Set a
     x y : A
     xs ys : List A
     R S : REL A B ℓ
@@ -60,8 +59,6 @@ map : R ⇒ S → Pointwise R ⇒ Pointwise S
 map R⇒S []            = []
 map R⇒S (Rxy ∷ Rxsys) = R⇒S Rxy ∷ map R⇒S Rxsys
 
-unzip : ∀ {r s} {R : REL A B r} {S : REL B C s} {xs zs} →
-  Pointwise (λ x z → ∃[ y ] R x y × S y z) xs zs →
-  ∃[ ys ] Pointwise R xs ys × Pointwise S ys zs
+unzip : Pointwise (R ; S) ⇒ (Pointwise R ; Pointwise S)
 unzip [] = [] , [] , []
-unzip ((y , r , s) ∷ xs∼zs) = Σ.map (y ∷_) (Σ.map (r ∷_) (s ∷_)) (unzip xs∼zs)
+unzip ((y , r , s) ∷ xs∼ys) = Σ.map (y ∷_) (Σ.map (r ∷_) (s ∷_)) (unzip xs∼ys)

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

@@ -13,114 +13,86 @@ open import Data.List.Relation.Ternary.Appending
 open import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise; []; _∷_)
 open import Data.Product.Base as Σ 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
+    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 _  {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
+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
 
-module _ {a b c x y p l r p′ l′ r′}
-         {A : Set a} {B : Set b} {C : Set c} {X : Set x} {Y : Set y}
-         {P : REL A X p} {L : REL X C l} {R : REL B C r}
-         {P′ : REL Y C p′} {L′ : REL A Y l′} {R′ : REL B Y r′}
-         where
-
-  module _ (f : ∀ {b c} → R b c → ∃[ y ] R′ b y × P′ y c)
-           (g : ∀ {a c} → ∃[ x ] P a x × L x c → ∃[ y ] L′ a y × P′ y c)
-           where
-
-    through→ : ∀ {as bs cs} →
-      ∃[ xs ] Pointwise P as xs × Appending L R xs bs cs →
-      ∃[ ys ] Appending L′ R′ as bs ys × Pointwise P′ ys cs
-    through→ (_ , [] , []++ rs) =
-      let _ , rs′ , ps′ = Pw.unzip (Pw.map f rs) in
-      _ , []++ rs′ , ps′
-    through→ (_ , p ∷ ps , l ∷ lrs) =
-      let _ , l′ , p′ = g (_ , p , l) in
-      Σ.map _ (Σ.map (l′ ∷_) (p′ ∷_)) (through→ (_ , ps , lrs))
-
-  module _ (f : ∀ {b c} → ∃[ y ] R′ b y × P′ y c → R b c)
-           (g : ∀ {a c} → ∃[ y ] L′ a y × P′ y c → ∃[ x ] P a x × L x c)
-           where
-
-    through← : ∀ {as bs cs} →
-      ∃[ ys ] Appending L′ R′ as bs ys × Pointwise P′ ys cs →
-      ∃[ xs ] Pointwise P as xs × Appending L R xs bs cs
-    through← (_ , []++ rs′ , ps′) =
-      _ , [] , []++ (Pw.transitive (λ r′ p′ → f (_ , r′ , p′)) rs′ ps′)
-    through← (_ , l′ ∷ lrs′ , p′ ∷ ps′) =
-      let _ , p , l = g (_ , l′ , p′) in
-      Σ.map _ (Σ.map (p ∷_) (l ∷_)) (through← (_ , lrs′ , ps′))
-
-module _ {a b c d x y l m r s l′ m′ r′ s′}
-         {A : Set a} {B : Set b} {C : Set c} {D : Set d} {X : Set x} {Y : Set y}
-         {L : REL A X l} {R : REL B X r} {L′ : REL X D l′} {R′ : REL C D r′}
-         {M : REL B Y m} {S : REL C Y s} {M′ : REL A D m′} {S′ : REL Y D s′}
-         where
-
-  module _ (f : ∀ {c d} → R′ c d → ∃[ y ] S c y × S′ y d)
-           (g : ∀ {b d} → ∃[ x ] R b x × L′ x d → ∃[ y ] M b y × S′ y d)
-           (h : ∀ {a d} → ∃[ x ] L a x × L′ x d → M′ a d)
-           where
-
-    assoc→ : ∀ {as bs cs ds} →
-      ∃[ xs ] Appending L R as bs xs × Appending L′ R′ xs cs ds →
-      ∃[ ys ] Appending M S bs cs ys × Appending M′ S′ as ys ds
-    assoc→ (_ , []++ rs , lrs′) =
-      let _ , mss , ss′ = through→ f g (_ , rs , lrs′) in
-      _ , mss , []++ ss′
-    assoc→ (_ , l ∷ lrs , l′ ∷ lrs′) =
-      Σ.map id (Σ.map id (h (_ , l , l′) ∷_)) (assoc→ (_ , lrs , lrs′))
-
-  module _ (f : ∀ {c d} → ∃[ y ] S c y × S′ y d → R′ c d)
-           (g : ∀ {b d} → ∃[ y ] M b y × S′ y d → ∃[ x ] R b x × L′ x d)
-           (h : ∀ {a d} → M′ a d → ∃[ x ] L a x × L′ x d)
-           where
-
-    assoc← : ∀ {as bs cs ds} →
-      ∃[ ys ] Appending M S bs cs ys × Appending M′ S′ as ys ds →
-      ∃[ xs ] Appending L R as bs xs × Appending L′ R′ xs cs ds
-    assoc← (_ , mss , []++ ss′) =
-      let _ , rs , lrs′ = through← f g (_ , mss , ss′) in
-      _ , []++ rs , lrs′
-    assoc← (_ , mss , m′ ∷ mss′) =
-      let _ , l , l′ = h m′ in
-      Σ.map _ (Σ.map (l ∷_) (l′ ∷_)) (assoc← (_ , mss , mss′))
+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
+  Σ.map _ (Σ.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
+  Σ.map _ (Σ.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′) =
+  Σ.map id (Σ.map id (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
+  Σ.map _ (Σ.map (l ∷_) (l′ ∷_)) (assoc← f g h (_ , mss , mss′))

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

@@ -8,29 +8,28 @@
 
 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 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 ds : List A
 
-  trans′ : ∀ {x z} → ∃[ y ] x ≈ y × y ≈ z → x ≈ z
-  trans′ (_ , p , q) = S.trans p q
-
-  trans⁻¹ : ∀ {x z} → x ≈ z → ∃[ y ] x ≈ y × y ≈ z
-  trans⁻¹ q = _ , q , S.refl
-
 ------------------------------------------------------------------------
 -- Re-exporting existing properties
 
@@ -51,23 +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→ trans⁻¹ id
+through→ = Appendingₚ.through→ ≈⇒≈;≈ id
 
 through← :
   ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs →
   ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs
-through← = Appendingₚ.through← trans′ id
+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→ trans⁻¹ id trans′
+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