From 52f5200a2814f8194180529bc74bb3ffaeb0661c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 27 Sep 2024 12:56:10 +0100 Subject: [PATCH 1/4] fix issue #2482 --- CHANGELOG.md | 9 +++++++++ src/Relation/Binary/Bundles.agda | 20 ++++++++++++++++++++ src/Relation/Binary/Structures.agda | 20 ++++++++++++++++++++ 3 files changed, 49 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index a513e4978f..016007f535 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -270,6 +270,15 @@ Additions to existing modules _≡?_ : DecidableEquality (Vec A n) ``` +* In `Relation.Binary.Structures`: + ```agda + record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where + field + isPreorder : IsPreorder _≲_ + _≟_ : Decidable _≈_ + _≲?_ : Decidable _≲_ + ``` + * In `Relation.Nullary.Decidable`: ```agda does-⇔ : A ⇔ B → (a? : Dec A) → (b? : Dec B) → does a? ≡ does b? diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index 5d29cabe57..9b34ce6f76 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -132,6 +132,26 @@ record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open Preorder preorder public hiding (Carrier; _≈_; _≲_; isPreorder) + +record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where + field + Carrier : Set c + _≈_ : Rel Carrier ℓ₁ -- The underlying equality. + _≲_ : Rel Carrier ℓ₂ -- The relation. + isDecPreorder : IsDecPreorder _≈_ _≲_ + + open IsDecPreorder isDecPreorder public + using (_≲?_; isPreorder) + + preorder : Preorder c ℓ₁ ℓ₂ + preorder = record + { isPreorder = isPreorder + } + + open Preorder preorder public + hiding (Carrier; _≈_; _≲_; isPreorder) + + ------------------------------------------------------------------------ -- Partial orders ------------------------------------------------------------------------ diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda index 14426b4cff..7dab646316 100644 --- a/src/Relation/Binary/Structures.agda +++ b/src/Relation/Binary/Structures.agda @@ -119,6 +119,26 @@ record IsTotalPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where open IsPreorder isPreorder public +record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where + field + isPreorder : IsPreorder _≲_ + _≟_ : Decidable _≈_ + _≲?_ : Decidable _≲_ + + open IsPreorder isPreorder public + hiding (module Eq) + + module Eq where + + isDecEquivalence : IsDecEquivalence + isDecEquivalence = record + { isEquivalence = isEquivalence + ; _≟_ = _≟_ + } + + open IsDecEquivalence isDecEquivalence public + + ------------------------------------------------------------------------ -- Partial orders ------------------------------------------------------------------------ From 9b03e410de2c4866c14a879a876d69c66cc05b2b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 28 Sep 2024 09:21:06 +0100 Subject: [PATCH 2/4] add `isDecPreorder` manifest fields to `IsDec*Order` structures --- CHANGELOG.md | 2 ++ src/Relation/Binary/Bundles.agda | 2 +- src/Relation/Binary/Structures.agda | 28 ++++++++++------------------ 3 files changed, 13 insertions(+), 19 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 352c80bc78..0cbd55758c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -274,6 +274,7 @@ Additions to existing modules ```agda record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) ``` + plus associated sub-bundles. * In `Relation.Binary.Construct.Interior.Symmetric`: ```agda @@ -294,6 +295,7 @@ Additions to existing modules _≟_ : Decidable _≈_ _≲?_ : Decidable _≲_ ``` + plus associated `isDecPreorder` fields in each higher `IsDec*Order` structure. * In `Relation.Nullary.Decidable`: ```agda diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index 9b34ce6f76..b36948083b 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -193,7 +193,7 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where private module DPO = IsDecPartialOrder isDecPartialOrder open DPO public - using (_≟_; _≤?_; isPartialOrder) + using (_≟_; _≤?_; isPartialOrder; isDecPreorder) poset : Poset c ℓ₁ ℓ₂ poset = record diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda index 7dab646316..3bbfc6db27 100644 --- a/src/Relation/Binary/Structures.agda +++ b/src/Relation/Binary/Structures.agda @@ -166,15 +166,15 @@ record IsDecPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) whe open IsPartialOrder isPartialOrder public hiding (module Eq) - module Eq where - - isDecEquivalence : IsDecEquivalence - isDecEquivalence = record - { isEquivalence = isEquivalence - ; _≟_ = _≟_ - } + isDecPreorder : IsDecPreorder _≤_ + isDecPreorder = record + { isPreorder = isPreorder + ; _≟_ = _≟_ + ; _≲?_ = _≤?_ + } - open IsDecEquivalence isDecEquivalence public + open IsDecPreorder isDecPreorder public + using (module Eq) record IsStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where @@ -254,16 +254,8 @@ record IsDecTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where ; _≤?_ = _≤?_ } - module Eq where - - isDecEquivalence : IsDecEquivalence - isDecEquivalence = record - { isEquivalence = isEquivalence - ; _≟_ = _≟_ - } - - open IsDecEquivalence isDecEquivalence public - + open IsDecPartialOrder isDecPartialOrder public + using (isDecPreorder; module Eq) -- Note that these orders are decidable. The current implementation -- of `Trichotomous` subsumes irreflexivity and asymmetry. See From 722efd1eb3c50e5b5b28a2264f5a776b17f7de81 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 1 Oct 2024 09:02:18 +0100 Subject: [PATCH 3/4] refactored derived sub-`Bundles` --- src/Relation/Binary/Bundles.agda | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index b36948083b..b7d3be963e 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -140,8 +140,10 @@ record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where _≲_ : Rel Carrier ℓ₂ -- The relation. isDecPreorder : IsDecPreorder _≈_ _≲_ - open IsDecPreorder isDecPreorder public - using (_≲?_; isPreorder) + private module DPO = IsDecPreorder isDecPreorder + + open DPO public + using (_≟_; _≲?_; isPreorder) preorder : Preorder c ℓ₁ ℓ₂ preorder = record @@ -149,7 +151,15 @@ record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where } open Preorder preorder public - hiding (Carrier; _≈_; _≲_; isPreorder) + hiding (Carrier; _≈_; _≲_; isPreorder; module Eq) + + module Eq where + decSetoid : DecSetoid c ℓ₁ + decSetoid = record + { isDecEquivalence = DPO.Eq.isDecEquivalence + } + + open DecSetoid decSetoid public ------------------------------------------------------------------------ @@ -203,13 +213,11 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open Poset poset public hiding (Carrier; _≈_; _≤_; isPartialOrder; module Eq) - module Eq where - decSetoid : DecSetoid c ℓ₁ - decSetoid = record - { isDecEquivalence = DPO.Eq.isDecEquivalence - } + decPreorder : DecPreorder c ℓ₁ ℓ₂ + decPreorder = record { isDecPreorder = isDecPreorder } - open DecSetoid decSetoid public + open DecPreorder decPreorder public + using (module Eq) record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where From d0dcd55361be2ba0c47dcbefaef7e14f54d3e96e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 4 Oct 2024 10:06:49 +0100 Subject: [PATCH 4/4] fixed knock-on consequences --- CHANGELOG.md | 2 ++ .../Binary/Construct/Interior/Symmetric.agda | 13 +++++++------ 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0cbd55758c..3a3f010404 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -283,7 +283,9 @@ Additions to existing modules and for `Reflexive` and `Transitive` relations `R`: ```agda isDecEquivalence : Decidable R → IsDecEquivalence (SymInterior R) + isDecPreorder : Decidable R → IsDecPreorder (SymInterior R) R isDecPartialOrder : Decidable R → IsDecPartialOrder (SymInterior R) R + decPreorder : Decidable R → DecPreorder _ _ _ decPoset : Decidable R → DecPoset _ _ _ ``` diff --git a/src/Relation/Binary/Construct/Interior/Symmetric.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda index 50b75b309d..733a36ea05 100644 --- a/src/Relation/Binary/Construct/Interior/Symmetric.agda +++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda @@ -100,12 +100,6 @@ module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where module _ (R? : Decidable R) where - isDecEquivalence : IsDecEquivalence (SymInterior R) - isDecEquivalence = record - { isEquivalence = isEquivalence - ; _≟_ = decidable R? - } - isDecPartialOrder : IsDecPartialOrder (SymInterior R) R isDecPartialOrder = record { isPartialOrder = isPartialOrder @@ -115,3 +109,10 @@ module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where decPoset : DecPoset _ ℓ ℓ decPoset = record { isDecPartialOrder = isDecPartialOrder } + + open DecPoset public + using (isDecPreorder; decPreorder) + + isDecEquivalence : IsDecEquivalence (SymInterior R) + isDecEquivalence = DecPoset.Eq.isDecEquivalence decPoset +