From 80d9f50fd358d4dd364a838afaf9ac6dcab55409 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 26 Feb 2024 18:57:37 +0000 Subject: [PATCH] refactored proofs from #2023 --- CHANGELOG.md | 35 +++++++++++-------- .../Binary/Construct/Composition.agda | 3 ++ src/Relation/Binary/Properties/Setoid.agda | 7 ++-- 3 files changed, 27 insertions(+), 18 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9b45f2409b..b569f488e4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -141,28 +141,28 @@ Additions to existing modules * In `Data.List.Relation.Ternary.Appending.Setoid.Properties`: ```agda - through→ : ∃[ xs ] Pointwise _≈_ as xs × Appending xs bs cs → + 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 → + 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 → + 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 + 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`: @@ -210,6 +210,11 @@ Additions to existing modules * In `Function.Bundles`, added `_⟶ₛ_` as a synonym for `Func` that can be used infix. +* Added new proofs in `Relation.Binary.Construct.Composition`: + ```agda + transitive⇒≈;≈⊆≈ : Transitive ≈ → (≈ ; ≈) ⇒ ≈ + ``` + * Added new definitions in `Relation.Binary.Definitions` ``` Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y) diff --git a/src/Relation/Binary/Construct/Composition.agda b/src/Relation/Binary/Construct/Composition.agda index 0f7a3cb02c..35df23947d 100644 --- a/src/Relation/Binary/Construct/Composition.agda +++ b/src/Relation/Binary/Construct/Composition.agda @@ -82,3 +82,6 @@ module _ (L : Rel A ℓ₁) (R : Rel A ℓ₂) (comm : R ; L ⇒ L ; R) where ; trans = transitive Oˡ.trans Oʳ.trans } where module Oˡ = IsPreorder Oˡ; module Oʳ = IsPreorder Oʳ + +transitive⇒≈;≈⊆≈ : (≈ : Rel A ℓ) → Transitive ≈ → (≈ ; ≈) ⇒ ≈ +transitive⇒≈;≈⊆≈ _ trans (_ , l , r) = trans l r diff --git a/src/Relation/Binary/Properties/Setoid.agda b/src/Relation/Binary/Properties/Setoid.agda index c037352df4..1b56c32d2a 100644 --- a/src/Relation/Binary/Properties/Setoid.agda +++ b/src/Relation/Binary/Properties/Setoid.agda @@ -15,7 +15,8 @@ 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 (_;_) +open import Relation.Binary.Construct.Composition + using (_;_; impliesˡ; transitive⇒≈;≈⊆≈) module Relation.Binary.Properties.Setoid {a ℓ} (S : Setoid a ℓ) where @@ -83,10 +84,10 @@ preorder = record -- Equality is closed under composition ≈;≈⇒≈ : _≈_ ; _≈_ ⇒ _≈_ -≈;≈⇒≈ (_ , p , q) = trans p q +≈;≈⇒≈ = transitive⇒≈;≈⊆≈ _ trans ≈⇒≈;≈ : _≈_ ⇒ _≈_ ; _≈_ -≈⇒≈;≈ q = _ , q , refl +≈⇒≈;≈ = impliesˡ _≈_ _≈_ refl id ------------------------------------------------------------------------ -- Other properties