From 4fdaf7ca1bf6c9fb3ad284eed6ef298e2d18fbec Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 2 Jul 2024 13:54:47 +0100 Subject: [PATCH 1/2] fixes #1131 --- src/Data/List/Relation/Binary/Equality/Setoid.agda | 6 ++++++ src/Data/List/Relation/Binary/Pointwise.agda | 14 +++++++++++--- 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/src/Data/List/Relation/Binary/Equality/Setoid.agda b/src/Data/List/Relation/Binary/Equality/Setoid.agda index 0253c55460..2fdaadf4d6 100644 --- a/src/Data/List/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/List/Relation/Binary/Equality/Setoid.agda @@ -116,6 +116,12 @@ foldr⁺ ∙⇔◦ e≈f xs≋ys = PW.foldr⁺ ∙⇔◦ e≈f xs≋ys ++⁺ : ∀ {ws xs ys zs} → ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs ++⁺ = PW.++⁺ +++⁺ʳ : ∀ xs {ys zs} → ys ≋ zs → xs ++ ys ≋ xs ++ zs +++⁺ʳ xs = PW.++⁺ʳ refl xs + +++⁺ˡ : ∀ {ws xs} → ws ≋ xs → ∀ zs → ws ++ zs ≋ xs ++ zs +++⁺ˡ rs = PW.++⁺ˡ refl rs + ++-cancelˡ : ∀ xs {ys zs} → xs ++ ys ≋ xs ++ zs → ys ≋ zs ++-cancelˡ xs = PW.++-cancelˡ xs diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda index 76e9d81f54..05e5cee9dd 100644 --- a/src/Data/List/Relation/Binary/Pointwise.agda +++ b/src/Data/List/Relation/Binary/Pointwise.agda @@ -26,7 +26,7 @@ open import Relation.Nullary hiding (Irrelevant) import Relation.Nullary.Decidable as Dec using (map′) open import Relation.Unary as U using (Pred) open import Relation.Binary.Core renaming (Rel to Rel₂) -open import Relation.Binary.Definitions using (_Respects_; _Respects₂_) +open import Relation.Binary.Definitions using (Reflexive;_Respects_; _Respects₂_) open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; Poset) open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence; IsPartialOrder; IsPreorder) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) @@ -166,6 +166,15 @@ tabulate⁻ {n = suc n} (x∼y ∷ xs∼ys) (fsuc i) = tabulate⁻ xs∼ys i ++-cancelʳ {xs = xs} (y ∷ ys) [] eq = contradiction (≡.trans (≡.sym (length-++ (y ∷ ys))) (Pointwise-length eq)) (m≢1+n+m (length xs) ∘ ≡.sym) +module _ (rfl : Reflexive R) where + + ++⁺ʳ : ∀ xs → Pointwise R ys zs → Pointwise R (xs ++ ys) (xs ++ zs) + ++⁺ʳ xs = ++⁺ (refl rfl) + + ++⁺ˡ : Pointwise R ws xs → ∀ zs → Pointwise R (ws ++ zs) (xs ++ zs) + ++⁺ˡ rs zs = ++⁺ rs (refl rfl) + + ------------------------------------------------------------------------ -- concat @@ -261,8 +270,7 @@ lookup⁺ (_ ∷ Rxys) (fsuc i) = lookup⁺ Rxys i Pointwise-≡⇒≡ : Pointwise {A = A} _≡_ ⇒ _≡_ Pointwise-≡⇒≡ [] = ≡.refl -Pointwise-≡⇒≡ (≡.refl ∷ xs∼ys) with Pointwise-≡⇒≡ xs∼ys -... | ≡.refl = ≡.refl +Pointwise-≡⇒≡ (≡.refl ∷ xs∼ys) = ≡.cong (_ ∷_) (Pointwise-≡⇒≡ xs∼ys) ≡⇒Pointwise-≡ : _≡_ ⇒ Pointwise {A = A} _≡_ ≡⇒Pointwise-≡ ≡.refl = refl ≡.refl From 0da6039ef176ff007847872bf4809988238e6291 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 27 Jul 2024 11:24:15 +0100 Subject: [PATCH 2/2] response to review comments --- CHANGELOG.md | 12 ++++++++++++ .../List/Relation/Binary/Equality/Setoid.agda | 18 ++++++++++-------- src/Data/List/Relation/Binary/Pointwise.agda | 8 ++++---- 3 files changed, 26 insertions(+), 12 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 80da9ee48e..d22ba87948 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -26,3 +26,15 @@ New modules Additions to existing modules ----------------------------- + +* In `Data.List.Relation.Binary.Pointwise`: + ```agda + ++⁺ʳ : Reflexive R → ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R) + ++⁺ˡ : Reflexive R → ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R) + ``` + +* In `Data.List.Relation.Binary.Equality.Setoid`: + ```agda + ++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs + ++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs + ``` diff --git a/src/Data/List/Relation/Binary/Equality/Setoid.agda b/src/Data/List/Relation/Binary/Equality/Setoid.agda index 2fdaadf4d6..f245eeaa5e 100644 --- a/src/Data/List/Relation/Binary/Equality/Setoid.agda +++ b/src/Data/List/Relation/Binary/Equality/Setoid.agda @@ -29,6 +29,8 @@ open Setoid S renaming (Carrier to A) private variable p q : Level + ws xs xs′ ys ys′ zs : List A + xss yss : List (List A) ------------------------------------------------------------------------ -- Definition of equality @@ -113,14 +115,14 @@ foldr⁺ ∙⇔◦ e≈f xs≋ys = PW.foldr⁺ ∙⇔◦ e≈f xs≋ys ------------------------------------------------------------------------ -- _++_ -++⁺ : ∀ {ws xs ys zs} → ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs +++⁺ : ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs ++⁺ = PW.++⁺ -++⁺ʳ : ∀ xs {ys zs} → ys ≋ zs → xs ++ ys ≋ xs ++ zs +++⁺ʳ : ∀ xs → ys ≋ zs → xs ++ ys ≋ xs ++ zs ++⁺ʳ xs = PW.++⁺ʳ refl xs -++⁺ˡ : ∀ {ws xs} → ws ≋ xs → ∀ zs → ws ++ zs ≋ xs ++ zs -++⁺ˡ rs = PW.++⁺ˡ refl rs +++⁺ˡ : ∀ zs → ws ≋ xs → ws ++ zs ≋ xs ++ zs +++⁺ˡ zs = PW.++⁺ˡ refl zs ++-cancelˡ : ∀ xs {ys zs} → xs ++ ys ≋ xs ++ zs → ys ≋ zs ++-cancelˡ xs = PW.++-cancelˡ xs @@ -131,7 +133,7 @@ foldr⁺ ∙⇔◦ e≈f xs≋ys = PW.foldr⁺ ∙⇔◦ e≈f xs≋ys ------------------------------------------------------------------------ -- concat -concat⁺ : ∀ {xss yss} → Pointwise _≋_ xss yss → concat xss ≋ concat yss +concat⁺ : Pointwise _≋_ xss yss → concat xss ≋ concat yss concat⁺ = PW.concat⁺ ------------------------------------------------------------------------ @@ -152,14 +154,14 @@ module _ {n} {f g : Fin n → A} module _ {P : Pred A p} (P? : U.Decidable P) (resp : P Respects _≈_) where - filter⁺ : ∀ {xs ys} → xs ≋ ys → filter P? xs ≋ filter P? ys + filter⁺ : xs ≋ ys → filter P? xs ≋ filter P? ys filter⁺ xs≋ys = PW.filter⁺ P? P? resp (resp ∘ sym) xs≋ys ------------------------------------------------------------------------ -- reverse -ʳ++⁺ : ∀{xs xs′ ys ys′} → xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′ +ʳ++⁺ : xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′ ʳ++⁺ = PW.ʳ++⁺ -reverse⁺ : ∀ {xs ys} → xs ≋ ys → reverse xs ≋ reverse ys +reverse⁺ : xs ≋ ys → reverse xs ≋ reverse ys reverse⁺ = PW.reverse⁺ diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda index 05e5cee9dd..56d261a646 100644 --- a/src/Data/List/Relation/Binary/Pointwise.agda +++ b/src/Data/List/Relation/Binary/Pointwise.agda @@ -26,7 +26,7 @@ open import Relation.Nullary hiding (Irrelevant) import Relation.Nullary.Decidable as Dec using (map′) open import Relation.Unary as U using (Pred) open import Relation.Binary.Core renaming (Rel to Rel₂) -open import Relation.Binary.Definitions using (Reflexive;_Respects_; _Respects₂_) +open import Relation.Binary.Definitions using (Reflexive; _Respects_; _Respects₂_) open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; Poset) open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence; IsPartialOrder; IsPreorder) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) @@ -168,11 +168,11 @@ tabulate⁻ {n = suc n} (x∼y ∷ xs∼ys) (fsuc i) = tabulate⁻ xs∼ys i module _ (rfl : Reflexive R) where - ++⁺ʳ : ∀ xs → Pointwise R ys zs → Pointwise R (xs ++ ys) (xs ++ zs) + ++⁺ʳ : ∀ xs → (xs ++_) Preserves (Pointwise R) ⟶ (Pointwise R) ++⁺ʳ xs = ++⁺ (refl rfl) - ++⁺ˡ : Pointwise R ws xs → ∀ zs → Pointwise R (ws ++ zs) (xs ++ zs) - ++⁺ˡ rs zs = ++⁺ rs (refl rfl) + ++⁺ˡ : ∀ zs → (_++ zs) Preserves (Pointwise R) ⟶ (Pointwise R) + ++⁺ˡ zs rs = ++⁺ rs (refl rfl) ------------------------------------------------------------------------