From 50bd46db0386af537e42aaae06b7e1fd1b8c41cd Mon Sep 17 00:00:00 2001 From: "Junyoung/\"Clare\" Jang" Date: Thu, 3 Apr 2025 12:21:48 -0400 Subject: [PATCH 1/4] Update PartialSetoid reasoning --- .../Binary/Reasoning/Base/Partial.agda | 49 ++++++++++--------- 1 file changed, 26 insertions(+), 23 deletions(-) diff --git a/src/Relation/Binary/Reasoning/Base/Partial.agda b/src/Relation/Binary/Reasoning/Base/Partial.agda index 5da6792f64..e8e0cbc920 100644 --- a/src/Relation/Binary/Reasoning/Base/Partial.agda +++ b/src/Relation/Binary/Reasoning/Base/Partial.agda @@ -22,52 +22,55 @@ module Relation.Binary.Reasoning.Base.Partial ------------------------------------------------------------------------ -- Definition of "related to" --- This seemingly unnecessary type is used to make it possible to --- infer arguments even if the underlying equality evaluates. +-- This type allows us to track whether reasoning steps +-- include _∼_ or not. infix 4 _IsRelatedTo_ data _IsRelatedTo_ : A → A → Set (a ⊔ ℓ) where - singleStep : ∀ x → x IsRelatedTo x - multiStep : ∀ {x y} (x∼y : x ∼ y) → x IsRelatedTo y + reflexive : ∀ {x y} → x ≡ y → x IsRelatedTo y + relTo : ∀ {x y} (x∼y : x ∼ y) → x IsRelatedTo y + +≡-go : Trans _≡_ _IsRelatedTo_ _IsRelatedTo_ +≡-go x≡y (reflexive y≡z) = reflexive (case x≡y of λ where ≡.refl → y≡z) +≡-go x≡y (relTo y∼z) = relTo (case x≡y of λ where ≡.refl → y∼z) ∼-go : Trans _∼_ _IsRelatedTo_ _IsRelatedTo_ -∼-go x∼y (singleStep y) = multiStep x∼y -∼-go x∼y (multiStep y∼z) = multiStep (trans x∼y y∼z) +∼-go x∼y (reflexive y≡z) = relTo (case y≡z of λ where ≡.refl → x∼y) +∼-go x∼y (relTo y∼z) = relTo (trans x∼y y∼z) stop : Reflexive _IsRelatedTo_ -stop = singleStep _ +stop = reflexive ≡.refl ------------------------------------------------------------------------ -- Types that are used to ensure that the final relation proved by the -- chain of reasoning can be converted into the required relation. -data IsMultiStep {x y} : x IsRelatedTo y → Set (a ⊔ ℓ) where - isMultiStep : ∀ x∼y → IsMultiStep (multiStep x∼y) +data IsRelTo {x y} : x IsRelatedTo y → Set (a ⊔ ℓ) where + isRelTo : ∀ x∼y → IsRelTo (relTo x∼y) -IsMultiStep? : ∀ {x y} (x∼y : x IsRelatedTo y) → Dec (IsMultiStep x∼y) -IsMultiStep? (multiStep x Date: Mon, 7 Apr 2025 14:23:37 -0400 Subject: [PATCH 2/4] Add changelog entry for this PR --- CHANGELOG.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index a6f66aa2f5..06c5552bd3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -25,6 +25,12 @@ Non-backwards compatible changes significantly faster. However, its reduction behaviour on open terms may have changed. +* The implementation of `_IsRelatedTo_` in `Relation.Binary.Reasoning.Base.Partial` + has been modified to support equaltional reasoning at the beginning and the end. + The detail of this issue is described in #2677. Since the names of constructors + of `_IsRelatedTo_` are changed and the reduction behaviour of reasoning steps + are changed, this modification is non-backwards compatible. + Minor improvements ------------------ From 823349b66c973ca958fca8c308b1b84bcfe6ff3c Mon Sep 17 00:00:00 2001 From: "Junyoung/\"Clare\" Jang" Date: Tue, 8 Apr 2025 04:55:28 -0400 Subject: [PATCH 3/4] Fix Changelog link --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 06c5552bd3..a58e9a51f3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -27,7 +27,7 @@ Non-backwards compatible changes * The implementation of `_IsRelatedTo_` in `Relation.Binary.Reasoning.Base.Partial` has been modified to support equaltional reasoning at the beginning and the end. - The detail of this issue is described in #2677. Since the names of constructors + The detail of this issue is described in [#2677](https://github.com/agda/agda-stdlib/pull/2677). Since the names of constructors of `_IsRelatedTo_` are changed and the reduction behaviour of reasoning steps are changed, this modification is non-backwards compatible. From 3f74b5df7f7f276b76eafb1da611126a6bf0b0a4 Mon Sep 17 00:00:00 2001 From: "Junyoung/\"Clare\" Jang" Date: Thu, 10 Apr 2025 07:36:25 -0400 Subject: [PATCH 4/4] Move Changelog entry --- CHANGELOG.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a58e9a51f3..83d5d62842 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -17,6 +17,12 @@ Bug-fixes the record constructors `_,_` incorrectly had no declared fixity. They have been given the fixity `infixr 4 _,_`, consistent with that of `Data.Product.Base`. +* The implementation of `_IsRelatedTo_` in `Relation.Binary.Reasoning.Base.Partial` + has been modified to correctly support equational reasoning at the beginning and the end. + The detail of this issue is described in [#2677](https://github.com/agda/agda-stdlib/pull/2677). Since the names of constructors + of `_IsRelatedTo_` are changed and the reduction behaviour of reasoning steps + are changed, this modification is non-backwards compatible. + Non-backwards compatible changes -------------------------------- @@ -25,12 +31,6 @@ Non-backwards compatible changes significantly faster. However, its reduction behaviour on open terms may have changed. -* The implementation of `_IsRelatedTo_` in `Relation.Binary.Reasoning.Base.Partial` - has been modified to support equaltional reasoning at the beginning and the end. - The detail of this issue is described in [#2677](https://github.com/agda/agda-stdlib/pull/2677). Since the names of constructors - of `_IsRelatedTo_` are changed and the reduction behaviour of reasoning steps - are changed, this modification is non-backwards compatible. - Minor improvements ------------------