From 8554c45319c4d10e2659777e428635ecb559d078 Mon Sep 17 00:00:00 2001 From: James Wood Date: Mon, 17 Jul 2023 17:49:47 +0100 Subject: [PATCH 1/3] [ new ] associativity of Appending --- .../List/Relation/Binary/Pointwise/Base.agda | 9 ++- .../Ternary/Appending/Properties.agda | 70 +++++++++++++++++++ .../Ternary/Appending/Setoid/Properties.agda | 28 +++++++- 3 files changed, 103 insertions(+), 4 deletions(-) diff --git a/src/Data/List/Relation/Binary/Pointwise/Base.agda b/src/Data/List/Relation/Binary/Pointwise/Base.agda index e547aea169..158456a469 100644 --- a/src/Data/List/Relation/Binary/Pointwise/Base.agda +++ b/src/Data/List/Relation/Binary/Pointwise/Base.agda @@ -8,7 +8,7 @@ module Data.List.Relation.Binary.Pointwise.Base where -open import Data.Product.Base using (_×_; <_,_>) +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; _⇒_) @@ -18,6 +18,7 @@ private a b c ℓ : Level A : Set a B : Set b + C : Set c x y : A xs ys : List A R S : REL A B ℓ @@ -58,3 +59,9 @@ 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 : ∀ {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 [] = [] , [] , [] +unzip ((y , r , s) ∷ xs∼zs) = Σ.map (y ∷_) (Σ.map (r ∷_) (s ∷_)) (unzip xs∼zs) diff --git a/src/Data/List/Relation/Ternary/Appending/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Properties.agda index 4508a7f719..ea8f8107f1 100644 --- a/src/Data/List/Relation/Ternary/Appending/Properties.agda +++ b/src/Data/List/Relation/Ternary/Appending/Properties.agda @@ -11,6 +11,8 @@ 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 Σ using (∃-syntax; _×_; _,_) +open import Function.Base using (id) open import Level using (Level) open import Relation.Binary using (REL; Rel; Trans) open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl) @@ -53,3 +55,71 @@ conicalˡ ([]++ rs) = refl conicalʳ : Appending L R 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′)) diff --git a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda index 0530b8b965..e1aaceaf9e 100644 --- a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda +++ b/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda @@ -14,7 +14,8 @@ open import Data.List.Base as List using (List; []) import Data.List.Properties as Listₚ open import Data.List.Relation.Binary.Pointwise using (Pointwise; []) import Data.List.Relation.Ternary.Appending.Properties as Appendingₚ -open import Data.Product using (_,_) +open import Data.Product using (∃-syntax; _×_; _,_) +open import Function.Base using (id) open import Relation.Binary.PropositionalEquality.Core using (refl) open import Data.List.Relation.Ternary.Appending.Setoid S @@ -22,13 +23,19 @@ module S = Setoid S; open S renaming (Carrier to A) using (_≈_) private variable - as bs cs : List A + 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 open Appendingₚ public - hiding (respʳ-≋; respˡ-≋) + using (conicalˡ; conicalʳ) ------------------------------------------------------------------------ -- Proving setoid-specific ones @@ -49,3 +56,18 @@ respʳ-≋ = Appendingₚ.respʳ-≋ S.trans S.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 + +through→ : + ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs → + ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs +through→ = Appendingₚ.through→ trans⁻¹ id + +through← : + ∃[ ys ] Appending as bs ys × Pointwise _≈_ ys cs → + ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs +through← = Appendingₚ.through← trans′ 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′ From f4ce50c4862fc3cb6319f94b99460cdc074649a2 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Sun, 25 Feb 2024 18:22:01 +0800 Subject: [PATCH 2/3] Removed unneeded variable --- src/Data/List/Relation/Binary/Pointwise/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Relation/Binary/Pointwise/Base.agda b/src/Data/List/Relation/Binary/Pointwise/Base.agda index 95286ad011..087bbee1ee 100644 --- a/src/Data/List/Relation/Binary/Pointwise/Base.agda +++ b/src/Data/List/Relation/Binary/Pointwise/Base.agda @@ -17,7 +17,7 @@ open import Relation.Binary.Construct.Composition using (_;_) private variable a b c ℓ : Level - A B C : Set a + A B : Set a x y : A xs ys : List A R S : REL A B ℓ From 5f7c9425c14d54d5d4811cc069560c11c4d92a3a Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Mon, 26 Feb 2024 08:39:02 +0800 Subject: [PATCH 3/3] Renamed Product module --- src/Data/List/Relation/Binary/Pointwise/Base.agda | 5 +++-- .../List/Relation/Ternary/Appending/Properties.agda | 10 +++++----- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/Data/List/Relation/Binary/Pointwise/Base.agda b/src/Data/List/Relation/Binary/Pointwise/Base.agda index 087bbee1ee..9a7a928742 100644 --- a/src/Data/List/Relation/Binary/Pointwise/Base.agda +++ b/src/Data/List/Relation/Binary/Pointwise/Base.agda @@ -8,7 +8,7 @@ module Data.List.Relation.Binary.Pointwise.Base where -open import Data.Product.Base as Σ using (_×_; _,_; <_,_>; ∃-syntax) +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; _⇒_) @@ -61,4 +61,5 @@ 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) = Σ.map (y ∷_) (Σ.map (r ∷_) (s ∷_)) (unzip xs∼ys) +unzip ((y , r , s) ∷ xs∼ys) = + Product.map (y ∷_) (Product.map (r ∷_) (s ∷_)) (unzip xs∼ys) diff --git a/src/Data/List/Relation/Ternary/Appending/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Properties.agda index acd3d52b2e..9ab5089f08 100644 --- a/src/Data/List/Relation/Ternary/Appending/Properties.agda +++ b/src/Data/List/Relation/Ternary/Appending/Properties.agda @@ -11,7 +11,7 @@ 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 Σ using (∃-syntax; _×_; _,_) +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) @@ -59,7 +59,7 @@ through→ f g (_ , [] , []++ rs) = _ , []++ 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)) + Product.map _ (Product.map (l′ ∷_) (p′ ∷_)) (through→ f g (_ , ps , lrs)) through← : ((R ; S) ⇒ T) → @@ -70,7 +70,7 @@ 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′)) + Product.map _ (Product.map (p ∷_) (l ∷_)) (through← f g (_ , lrs′ , ps′)) assoc→ : (R ⇒ (S ; T)) → @@ -82,7 +82,7 @@ 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′)) + Product.map₂ (Product.map₂ (h (_ , l , l′) ∷_)) (assoc→ f g h (_ , lrs , lrs′)) assoc← : ((S ; T) ⇒ R) → @@ -95,4 +95,4 @@ assoc← f g h (_ , mss , []++ ss′) = _ , []++ 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′)) + Product.map _ (Product.map (l ∷_) (l′ ∷_)) (assoc← f g h (_ , mss , mss′))