diff --git a/CHANGELOG.md b/CHANGELOG.md index 1860e7a73d..32258f0604 100644 --- a/CHANGELOG.md +++ b/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 _ diff --git a/src/Data/List/Relation/Binary/Pointwise/Base.agda b/src/Data/List/Relation/Binary/Pointwise/Base.agda index e547aea169..9a7a928742 100644 --- a/src/Data/List/Relation/Binary/Pointwise/Base.agda +++ b/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) diff --git a/src/Data/List/Relation/Ternary/Appending/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Properties.agda index 4063d504a7..9ab5089f08 100644 --- a/src/Data/List/Relation/Ternary/Appending/Properties.agda +++ b/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′)) diff --git a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda index 1e2ef9cd6a..a8b6464f66 100644 --- a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda +++ b/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 ≈;≈⇒≈ diff --git a/src/Relation/Binary/Properties/Setoid.agda b/src/Relation/Binary/Properties/Setoid.agda index f21eb2f4df..c037352df4 100644 --- a/src/Relation/Binary/Properties/Setoid.agda +++ b/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