From 7206bd0d88a6d2f7cb744e5b5c1ab7b115a157f5 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Wed, 18 Oct 2023 09:39:32 +0900 Subject: [PATCH 1/4] Added remaining flipped and negated relations to binary relation bundles --- CHANGELOG.md | 30 ++++--- .../Lattice/Properties/Semilattice.agda | 4 +- .../Product/Relation/Binary/Lex/Strict.agda | 2 +- src/Relation/Binary/Bundles.agda | 88 +++++++++++++------ .../Binary/Properties/DecTotalOrder.agda | 3 +- src/Relation/Binary/Properties/Poset.agda | 5 -- .../Binary/Properties/TotalOrder.agda | 5 +- src/Relation/Binary/Structures.agda | 33 ++++--- 8 files changed, 107 insertions(+), 63 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2dcdb3d924..817d96d012 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -849,18 +849,24 @@ Non-backwards compatible changes IO.Effectful IO.Instances ``` -### (Issue #2096) Introduction of flipped relation symbol for `Relation.Binary.Bundles.Preorder` - -* Previously, the relation symbol `_∼_` was (notationally) symmetric, so that its - converse relation could only be discussed *semantically* in terms of `flip _∼_` - in `Relation.Binary.Properties.Preorder`, `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}` - -* Now, the symbol `_∼_` has been renamed to a new symbol `_≲_`, with `_≳_` - introduced as a definition in `Relation.Binary.Bundles.Preorder` whose properties - in `Relation.Binary.Properties.Preorder` now refer to it. Partial backwards compatible - has been achieved by redeclaring a deprecated version of the old name in the record. - Therefore, only _declarations_ of `PartialOrder` records will need their field names - updating. +### (Issue #2096) Introduction of flipped and negated relation symbols to bundles in `Relation.Binary.Bundles` + +* Previously, bundles such as `Preorder`, `Poset`, `TotalOrder` etc. did not have the flipped + and negated versions of the operators exposed. In some cases they could obtained by opening the + relevant `Relation.Binary.Properties.X` file but usually they had to be redefined every time. + +* To fix this, these bundles now all export all 4 versons of the operator: normal, converse, negated, + converse-negated. Accordingly they are no longer exported from the corresponding `Properties` file. + +* To make this work for `Preorder`, it was necessary to change the name of the relation symbol. + Previously, the symbol was `_∼_` which is (notationally) symmetric, so that its + converse relation could only be discussed *semantically* in terms of `flip _∼_`. + +* Now, the `Preorder` record field `_∼_` has been renamed to `_≲_`, with `_≳_` + introduced as a definition in `Relation.Binary.Bundles.Preorder`. + Partial backwards compatible has been achieved by redeclaring a deprecated version + of the old symbol in the record. Therefore, only _declarations_ of `PartialOrder` records will + need their field names updating. ### (Issue #1214) Reorganisation of the introduction of negated relation symbols under `Relation.Binary` diff --git a/src/Algebra/Lattice/Properties/Semilattice.agda b/src/Algebra/Lattice/Properties/Semilattice.agda index 38554aedfa..7b8135ced7 100644 --- a/src/Algebra/Lattice/Properties/Semilattice.agda +++ b/src/Algebra/Lattice/Properties/Semilattice.agda @@ -27,8 +27,8 @@ import Relation.Binary.Construct.NaturalOrder.Left _≈_ _∧_ poset : Poset c ℓ ℓ poset = LeftNaturalOrder.poset isSemilattice -open Poset poset using (_≤_; isPartialOrder) -open PosetProperties poset using (_≥_; ≥-isPartialOrder) +open Poset poset using (_≤_; _≥_; isPartialOrder) +open PosetProperties poset using (≥-isPartialOrder) ------------------------------------------------------------------------ -- Every algebraic semilattice can be turned into an order-theoretic one. diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda index 42d139893d..39d86602f2 100644 --- a/src/Data/Product/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda @@ -240,7 +240,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} (isEquivalence pre₁) (isEquivalence pre₂) ; reflexive = ×-reflexive _≈₁_ _<₁_ _<₂_ (reflexive pre₂) ; trans = ×-transitive {_<₂_ = _<₂_} - (isEquivalence pre₁) (∼-resp-≈ pre₁) + (isEquivalence pre₁) (≲-resp-≈ pre₁) (trans pre₁) (trans pre₂) } where open IsPreorder diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index eb7975f376..641803f8ef 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -43,13 +43,15 @@ record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where isEquivalence : IsEquivalence _≈_ open IsEquivalence isEquivalence public + using (refl; reflexive; isPartialEquivalence) partialSetoid : PartialSetoid c ℓ partialSetoid = record { isPartialEquivalence = isPartialEquivalence } - open PartialSetoid partialSetoid public using (_≉_) + open PartialSetoid partialSetoid public + hiding (Carrier; _≈_; isPartialEquivalence) record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where @@ -60,14 +62,15 @@ record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where isDecEquivalence : IsDecEquivalence _≈_ open IsDecEquivalence isDecEquivalence public + using (_≟_; isEquivalence) setoid : Setoid c ℓ setoid = record { isEquivalence = isEquivalence } - open Setoid setoid public using (partialSetoid; _≉_) - + open Setoid setoid public + hiding (Carrier; _≈_; isEquivalence) ------------------------------------------------------------------------ -- Preorders @@ -99,6 +102,9 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≳_ _≳_ = flip _≲_ + infix 4 _⋧_ + _⋧_ = flip _⋦_ + -- Deprecated. infix 4 _∼_ _∼_ = _≲_ @@ -117,14 +123,15 @@ record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isTotalPreorder : IsTotalPreorder _≈_ _≲_ open IsTotalPreorder isTotalPreorder public - hiding (module Eq) + using (total; isPreorder) preorder : Preorder c ℓ₁ ℓ₂ - preorder = record { isPreorder = isPreorder } + preorder = record + { isPreorder = isPreorder + } open Preorder preorder public - using (module Eq; _≳_; _⋦_) - + hiding (Carrier; _≈_; _≲_; isPreorder) ------------------------------------------------------------------------ -- Partial orders @@ -139,7 +146,7 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isPartialOrder : IsPartialOrder _≈_ _≤_ open IsPartialOrder isPartialOrder public - hiding (module Eq) + using (antisym; isPreorder) preorder : Preorder c ℓ₁ ℓ₂ preorder = record @@ -147,8 +154,13 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where } open Preorder preorder public - using (module Eq) - renaming (_⋦_ to _≰_) + hiding (Carrier; _≈_; _≲_; isPreorder) + renaming + ( _⋦_ to _≰_; _≳_ to _≥_; _⋧_ to _≱_ + ; ≲-respˡ-≈ to ≤-respˡ-≈ + ; ≲-respʳ-≈ to ≤-respʳ-≈ + ; ≲-resp-≈ to ≤-resp-≈ + ) record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where @@ -159,9 +171,10 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where _≤_ : Rel Carrier ℓ₂ isDecPartialOrder : IsDecPartialOrder _≈_ _≤_ - private - module DPO = IsDecPartialOrder isDecPartialOrder - open DPO public hiding (module Eq) + private module DPO = IsDecPartialOrder isDecPartialOrder + + open DPO public + using (_≟_; _≤?_; isPartialOrder) poset : Poset c ℓ₁ ℓ₂ poset = record @@ -169,7 +182,7 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where } open Poset poset public - using (preorder; _≰_) + hiding (Carrier; _≈_; _≤_; isPartialOrder; module Eq) module Eq where decSetoid : DecSetoid c ℓ₁ @@ -203,6 +216,12 @@ record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) _≮_ : Rel Carrier _ x ≮ y = ¬ (x < y) + infix 4 _>_ + _>_ = flip _<_ + + infix 4 _≯_ + _≯_ = flip _≮_ + record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _<_ @@ -212,9 +231,10 @@ record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂ _<_ : Rel Carrier ℓ₂ isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_ - private - module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder - open DSPO public hiding (module Eq) + private module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder + + open DSPO public + using (_ Date: Wed, 18 Oct 2023 13:34:10 +0900 Subject: [PATCH 2/4] Fix typo --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 817d96d012..9fa8c269c0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -855,7 +855,7 @@ Non-backwards compatible changes and negated versions of the operators exposed. In some cases they could obtained by opening the relevant `Relation.Binary.Properties.X` file but usually they had to be redefined every time. -* To fix this, these bundles now all export all 4 versons of the operator: normal, converse, negated, +* To fix this, these bundles now all export all 4 versions of the operator: normal, converse, negated, converse-negated. Accordingly they are no longer exported from the corresponding `Properties` file. * To make this work for `Preorder`, it was necessary to change the name of the relation symbol. From 418dc50fa43bca1f9a1966bfed47eb027371ea04 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 19 Oct 2023 10:27:33 +0900 Subject: [PATCH 3/4] Add bundle re-exporting algorithm to README.Design.Hierarchies --- README/Design/Hierarchies.agda | 37 ++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/README/Design/Hierarchies.agda b/README/Design/Hierarchies.agda index 09d5504a91..9995f97212 100644 --- a/README/Design/Hierarchies.agda +++ b/README/Design/Hierarchies.agda @@ -249,6 +249,43 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where -- differently, as a function with an unknown domain an codomain is -- of little use. +------------------------- +-- Bundle re-exporting -- +------------------------- + +In general ensuring that bundles re-export everything in their +sub-bundles can get a little tricky. + +Imagine we have the following general scenario where bundle A is a +direct refinement of bundle C (i.e. the record `IsA` has a `IsC` field) +but is also morally a refinement of bundles B and D. + + Structures Bundles + ========== ======= + IsA A + / || \ / || \ +IsB IsC IsD B C D + +The procedure for re-exports in the bundles is as follows: + +1. `open IsA isA public using (IsC, M)` where `M` is everything exported + by `IsA` that is not exported by `IsC`. + +2. Construct `c : C` via the `isC` obtained in step 1. + +3. `open C c public hiding (N)` where `N` is the list of fields shared + by both `A` and `C`. + +4. Construct `b : B` via the `isB` obtained in step 1. + +5. `open B b public using (O)` where `O` is everything exported by `B` + but not exported by `IsA`. + +6. Construct `d : D` via the `isC` obtained in step 1. + +7. `open D d public using (P)` where `P` is everything exported by `D` + but not exported by IsA + ------------------------------------------------------------------------ -- Other hierarchy modules ------------------------------------------------------------------------ From 94616a54cf1fc406e2df4eaa38daacc8f81de163 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 19 Oct 2023 10:59:23 +0900 Subject: [PATCH 4/4] Actually add comment tokens --- README/Design/Hierarchies.agda | 48 +++++++++++++++++----------------- 1 file changed, 24 insertions(+), 24 deletions(-) diff --git a/README/Design/Hierarchies.agda b/README/Design/Hierarchies.agda index 9995f97212..bc9220ba23 100644 --- a/README/Design/Hierarchies.agda +++ b/README/Design/Hierarchies.agda @@ -253,38 +253,38 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where -- Bundle re-exporting -- ------------------------- -In general ensuring that bundles re-export everything in their -sub-bundles can get a little tricky. +-- In general ensuring that bundles re-export everything in their +-- sub-bundles can get a little tricky. -Imagine we have the following general scenario where bundle A is a -direct refinement of bundle C (i.e. the record `IsA` has a `IsC` field) -but is also morally a refinement of bundles B and D. +-- Imagine we have the following general scenario where bundle A is a +-- direct refinement of bundle C (i.e. the record `IsA` has a `IsC` field) +-- but is also morally a refinement of bundles B and D. - Structures Bundles - ========== ======= - IsA A - / || \ / || \ -IsB IsC IsD B C D +-- Structures Bundles +-- ========== ======= +-- IsA A +-- / || \ / || \ +-- IsB IsC IsD B C D + +-- The procedure for re-exports in the bundles is as follows: -The procedure for re-exports in the bundles is as follows: +-- 1. `open IsA isA public using (IsC, M)` where `M` is everything +-- exported by `IsA` that is not exported by `IsC`. -1. `open IsA isA public using (IsC, M)` where `M` is everything exported - by `IsA` that is not exported by `IsC`. +-- 2. Construct `c : C` via the `isC` obtained in step 1. -2. Construct `c : C` via the `isC` obtained in step 1. +-- 3. `open C c public hiding (N)` where `N` is the list of fields +-- shared by both `A` and `C`. -3. `open C c public hiding (N)` where `N` is the list of fields shared - by both `A` and `C`. +-- 4. Construct `b : B` via the `isB` obtained in step 1. -4. Construct `b : B` via the `isB` obtained in step 1. +-- 5. `open B b public using (O)` where `O` is everything exported +-- by `B` but not exported by `IsA`. + +-- 6. Construct `d : D` via the `isC` obtained in step 1. -5. `open B b public using (O)` where `O` is everything exported by `B` - but not exported by `IsA`. - -6. Construct `d : D` via the `isC` obtained in step 1. - -7. `open D d public using (P)` where `P` is everything exported by `D` - but not exported by IsA +-- 7. `open D d public using (P)` where `P` is everything exported +-- by `D` but not exported by `IsA` ------------------------------------------------------------------------ -- Other hierarchy modules