From d6b274bb631155b0cded29a5ce2c73a6b6657f3f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 9 Jan 2025 16:50:54 +0000 Subject: [PATCH 1/7] refactor: `resp` not `subst` --- src/Data/List/Membership/Propositional.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Membership/Propositional.agda b/src/Data/List/Membership/Propositional.agda index 2f5edc2d7e..60c2a9aa71 100644 --- a/src/Data/List/Membership/Propositional.agda +++ b/src/Data/List/Membership/Propositional.agda @@ -10,7 +10,7 @@ module Data.List.Membership.Propositional {a} {A : Set a} where open import Data.List.Relation.Unary.Any using (Any) -open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; resp; subst) +open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; resp) open import Relation.Binary.PropositionalEquality.Properties using (setoid) import Data.List.Membership.Setoid as SetoidMembership @@ -26,7 +26,7 @@ open SetoidMembership (setoid A) public hiding (lose) infix 4 _≢∈_ _≢∈_ : ∀ {x y : A} {xs} → x ∈ xs → y ∈ xs → Set _ -_≢∈_ x∈xs y∈xs = ∀ x≡y → subst (_∈ _) x≡y x∈xs ≢ y∈xs +_≢∈_ x∈xs y∈xs = ∀ x≡y → resp (_∈ _) x≡y x∈xs ≢ y∈xs ------------------------------------------------------------------------ -- Other operations From 61f31a7c501ddfcb05b7f624ece2221916903148 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 9 Jan 2025 16:53:32 +0000 Subject: [PATCH 2/7] =?UTF-8?q?refactor:=20make=20`=E2=88=89[]`=20postfix,?= =?UTF-8?q?=20explicit;=20remove=20all=20uses=20of=20`rewrite`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../Propositional/Properties/Core.agda | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda index 65485abb0e..80a51e3559 100644 --- a/src/Data/List/Membership/Propositional/Properties/Core.agda +++ b/src/Data/List/Membership/Propositional/Properties/Core.agda @@ -20,7 +20,7 @@ open import Function.Base using (flip; id; _∘_) open import Function.Bundles using (_↔_; mk↔ₛ′) open import Level using (Level) open import Relation.Binary.PropositionalEquality.Core - using (_≡_; refl; cong; resp) + using (_≡_; refl; trans; cong; resp) open import Relation.Unary using (Pred; _⊆_) private @@ -33,8 +33,8 @@ private ------------------------------------------------------------------------ -- Basics -∉[] : x ∉ [] -∉[] () +_∉[] : (x : A) → x ∉ [] +_ ∉[] = λ() ------------------------------------------------------------------------ -- find satisfies a simple equality when the predicate is a @@ -42,7 +42,8 @@ private find-∈ : (x∈xs : x ∈ xs) → find x∈xs ≡ (x , x∈xs , refl) find-∈ (here refl) = refl -find-∈ (there x∈xs) rewrite find-∈ x∈xs = refl +find-∈ (there x∈xs) + = cong (λ where (x , x∈xs , eq) → x , there x∈xs , eq) (find-∈ x∈xs) ------------------------------------------------------------------------ -- Lemmas relating map and find. @@ -59,7 +60,8 @@ module _ {P : Pred A p} where let x , x∈xs , px = find p in find (Any.map f p) ≡ (x , x∈xs , f px) find∘map (here p) f = refl - find∘map (there p) f rewrite find∘map p f = refl + find∘map (there p) f + = cong (λ where (x , x∈xs , eq) → x , there x∈xs , eq) (find∘map p f) ------------------------------------------------------------------------ -- Any can be expressed using _∈_ @@ -67,14 +69,15 @@ module _ {P : Pred A p} where module _ {P : Pred A p} where ∃∈-Any : (∃ λ x → x ∈ xs × P x) → Any P xs - ∃∈-Any (x , x∈xs , px) = lose {P = P} x∈xs px + ∃∈-Any (x , x∈xs , px) = lose x∈xs px ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p ∃∈-Any∘find p = map∘find p refl find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p find∘∃∈-Any p@(x , x∈xs , px) - rewrite find∘map x∈xs (flip (resp P) px) | find-∈ x∈xs = refl + = trans (find∘map x∈xs (flip (resp P) px)) + (cong (λ (x , x∈xs , eq) → x , x∈xs , resp P eq px) (find-∈ x∈xs)) Any↔ : (∃ λ x → x ∈ xs × P x) ↔ Any P xs Any↔ = mk↔ₛ′ ∃∈-Any find ∃∈-Any∘find find∘∃∈-Any From 46bb9249aca9ab4ec8e705ba0e60d25c682b5435 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 9 Jan 2025 16:55:04 +0000 Subject: [PATCH 3/7] =?UTF-8?q?refactor:=20make=20`=E2=88=89[]`=20postfix,?= =?UTF-8?q?=20explicitly=20quantified?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- CHANGELOG.md | 4 ++-- src/Data/List/Membership/Setoid/Properties.agda | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 62b67cddcd..043c344257 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -312,7 +312,7 @@ Additions to existing modules map∷⁻ : xs ∈ map (y ∷_) xss → ∃[ ys ] ys ∈ xss × xs ≡ y ∷ ys map∷-decomp∈ : (x ∷ xs) ∈ map (y ∷_) xss → x ≡ y × xs ∈ xss ∈-map∷⁻ : xs ∈ map (x ∷_) xss → x ∈ xs - ∉[] : x ∉ [] + _∉[] : ∀ x → x ∉ [] deduplicate-∈⇔ : z ∈ xs ⇔ z ∈ deduplicate _≈?_ xs ``` @@ -333,7 +333,7 @@ Additions to existing modules y ∈₂ map f (filter P? xs) ∈-concatMap⁺ : Any ((y ∈_) ∘ f) xs → y ∈ concatMap f xs ∈-concatMap⁻ : y ∈ concatMap f xs → Any ((y ∈_) ∘ f) xs - ∉[] : x ∉ [] + _∉[] : ∀ x → x ∉ [] deduplicate-∈⇔ : _≈_ Respectsʳ (flip R) → z ∈ xs ⇔ z ∈ deduplicate R? xs ``` diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda index 988c01a07e..a77893c11a 100644 --- a/src/Data/List/Membership/Setoid/Properties.agda +++ b/src/Data/List/Membership/Setoid/Properties.agda @@ -49,8 +49,8 @@ module _ (S : Setoid c ℓ) where open Membership S - ∉[] : ∀ {x} → x ∉ [] - ∉[] () + _∉[] : ∀ x → x ∉ [] + _ ∉[] = λ() ------------------------------------------------------------------------ -- Equality properties From e6288eaa08dcf45dd6bcecfb43c352341b828f4a Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 12 Jan 2025 17:22:20 +0000 Subject: [PATCH 4/7] knock-on viscosity --- src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index 901ee8b942..636812e46e 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -53,7 +53,7 @@ module _ (S : Setoid a ℓ) where open Subset S ∷⊈[] : ∀ {x xs} → x ∷ xs ⊈ [] - ∷⊈[] p = Membershipₚ.∉[] S $ p (here refl) + ∷⊈[] p = (S Membershipₚ.∉[]) _ $ p (here refl) ⊆[]⇒≡[] : (_⊆ []) ⋐ (_≡ []) ⊆[]⇒≡[] {x = []} _ = ≡.refl From a8fcb0a8e821d65e1599f7ed129abb4bb3963653 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 12 Jan 2025 17:31:00 +0000 Subject: [PATCH 5/7] tweak --- src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda index 636812e46e..0743dd2cfd 100644 --- a/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda +++ b/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda @@ -53,7 +53,7 @@ module _ (S : Setoid a ℓ) where open Subset S ∷⊈[] : ∀ {x xs} → x ∷ xs ⊈ [] - ∷⊈[] p = (S Membershipₚ.∉[]) _ $ p (here refl) + ∷⊈[] p = Membershipₚ._∉[] S _ $ p (here refl) ⊆[]⇒≡[] : (_⊆ []) ⋐ (_≡ []) ⊆[]⇒≡[] {x = []} _ = ≡.refl From e38125d9a7f64bffed22542b1e5788131b10b1c6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 14 Jan 2025 12:20:54 +0000 Subject: [PATCH 6/7] =?UTF-8?q?Revert=20"refactor:=20make=20`=E2=88=89[]`?= =?UTF-8?q?=20postfix,=20explicit;=20remove=20all=20uses=20of=20`rewrite`"?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This reverts commit 61f31a7c501ddfcb05b7f624ece2221916903148. Following discussion on the PR --- .../Propositional/Properties/Core.agda | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda index 80a51e3559..65485abb0e 100644 --- a/src/Data/List/Membership/Propositional/Properties/Core.agda +++ b/src/Data/List/Membership/Propositional/Properties/Core.agda @@ -20,7 +20,7 @@ open import Function.Base using (flip; id; _∘_) open import Function.Bundles using (_↔_; mk↔ₛ′) open import Level using (Level) open import Relation.Binary.PropositionalEquality.Core - using (_≡_; refl; trans; cong; resp) + using (_≡_; refl; cong; resp) open import Relation.Unary using (Pred; _⊆_) private @@ -33,8 +33,8 @@ private ------------------------------------------------------------------------ -- Basics -_∉[] : (x : A) → x ∉ [] -_ ∉[] = λ() +∉[] : x ∉ [] +∉[] () ------------------------------------------------------------------------ -- find satisfies a simple equality when the predicate is a @@ -42,8 +42,7 @@ _ ∉[] = λ() find-∈ : (x∈xs : x ∈ xs) → find x∈xs ≡ (x , x∈xs , refl) find-∈ (here refl) = refl -find-∈ (there x∈xs) - = cong (λ where (x , x∈xs , eq) → x , there x∈xs , eq) (find-∈ x∈xs) +find-∈ (there x∈xs) rewrite find-∈ x∈xs = refl ------------------------------------------------------------------------ -- Lemmas relating map and find. @@ -60,8 +59,7 @@ module _ {P : Pred A p} where let x , x∈xs , px = find p in find (Any.map f p) ≡ (x , x∈xs , f px) find∘map (here p) f = refl - find∘map (there p) f - = cong (λ where (x , x∈xs , eq) → x , there x∈xs , eq) (find∘map p f) + find∘map (there p) f rewrite find∘map p f = refl ------------------------------------------------------------------------ -- Any can be expressed using _∈_ @@ -69,15 +67,14 @@ module _ {P : Pred A p} where module _ {P : Pred A p} where ∃∈-Any : (∃ λ x → x ∈ xs × P x) → Any P xs - ∃∈-Any (x , x∈xs , px) = lose x∈xs px + ∃∈-Any (x , x∈xs , px) = lose {P = P} x∈xs px ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p ∃∈-Any∘find p = map∘find p refl find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p find∘∃∈-Any p@(x , x∈xs , px) - = trans (find∘map x∈xs (flip (resp P) px)) - (cong (λ (x , x∈xs , eq) → x , x∈xs , resp P eq px) (find-∈ x∈xs)) + rewrite find∘map x∈xs (flip (resp P) px) | find-∈ x∈xs = refl Any↔ : (∃ λ x → x ∈ xs × P x) ↔ Any P xs Any↔ = mk↔ₛ′ ∃∈-Any find ∃∈-Any∘find find∘∃∈-Any From 042569e075bb048c2828c5da3d43b9c8fa5492f9 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 14 Jan 2025 12:40:18 +0000 Subject: [PATCH 7/7] by hand: this time is it right? --- .../Membership/Propositional/Properties/Core.agda | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda index 65485abb0e..b849d04f3b 100644 --- a/src/Data/List/Membership/Propositional/Properties/Core.agda +++ b/src/Data/List/Membership/Propositional/Properties/Core.agda @@ -20,7 +20,7 @@ open import Function.Base using (flip; id; _∘_) open import Function.Bundles using (_↔_; mk↔ₛ′) open import Level using (Level) open import Relation.Binary.PropositionalEquality.Core - using (_≡_; refl; cong; resp) + using (_≡_; refl; trans; cong; resp) open import Relation.Unary using (Pred; _⊆_) private @@ -42,7 +42,8 @@ private find-∈ : (x∈xs : x ∈ xs) → find x∈xs ≡ (x , x∈xs , refl) find-∈ (here refl) = refl -find-∈ (there x∈xs) rewrite find-∈ x∈xs = refl +find-∈ (there x∈xs) + = cong (λ where (x , x∈xs , eq) → x , there x∈xs , eq) (find-∈ x∈xs) ------------------------------------------------------------------------ -- Lemmas relating map and find. @@ -59,7 +60,8 @@ module _ {P : Pred A p} where let x , x∈xs , px = find p in find (Any.map f p) ≡ (x , x∈xs , f px) find∘map (here p) f = refl - find∘map (there p) f rewrite find∘map p f = refl + find∘map (there p) f + = cong (λ where (x , x∈xs , eq) → x , there x∈xs , eq) (find∘map p f) ------------------------------------------------------------------------ -- Any can be expressed using _∈_ @@ -67,14 +69,15 @@ module _ {P : Pred A p} where module _ {P : Pred A p} where ∃∈-Any : (∃ λ x → x ∈ xs × P x) → Any P xs - ∃∈-Any (x , x∈xs , px) = lose {P = P} x∈xs px + ∃∈-Any (x , x∈xs , px) = lose x∈xs px ∃∈-Any∘find : (p : Any P xs) → ∃∈-Any (find p) ≡ p ∃∈-Any∘find p = map∘find p refl find∘∃∈-Any : (p : ∃ λ x → x ∈ xs × P x) → find (∃∈-Any p) ≡ p find∘∃∈-Any p@(x , x∈xs , px) - rewrite find∘map x∈xs (flip (resp P) px) | find-∈ x∈xs = refl + = trans (find∘map x∈xs (flip (resp P) px)) + (cong (λ (x , x∈xs , eq) → x , x∈xs , resp P eq px) (find-∈ x∈xs)) Any↔ : (∃ λ x → x ∈ xs × P x) ↔ Any P xs Any↔ = mk↔ₛ′ ∃∈-Any find ∃∈-Any∘find find∘∃∈-Any