From 72fb46f964c3f8dbfbf227e563aeddcc17dd20a8 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 15 Sep 2023 12:21:33 +0100 Subject: [PATCH 01/33] choosing precedence = 4 --- CHANGELOG.md | 8 ++++++++ src/Relation/Binary/Bundles.agda | 11 +++++++++++ 2 files changed, 19 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0485996a5c..0b6052baec 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1809,6 +1809,14 @@ Other minor changes ``` and their corresponding algebraic subbundles. + The following negated relation symbols have now been added + ```agda + infix 4 _≁_ _≰_ _≮_ + Preorder._≁_ : Rel Carrier _ + Poset._≰_ : Rel Carrier _ + StrictPartialOrder._≮_ : Rel Carrier _ + ``` + * Added new proofs to `Algebra.Consequences.Base`: ```agda reflexive+selfInverse⇒involutive : Reflexive _≈_ → diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index 5a0621629f..1d181701d5 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -91,6 +91,9 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open Setoid setoid public + infix 4 _≁_ + _≁_ : Rel Carrier _ + x ≁ y = ¬ (x ∼ y) record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _≲_ @@ -133,6 +136,10 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open Preorder preorder public using (module Eq) + infix 4 _≰_ + _≰_ : Rel Carrier _ + x ≰ y = ¬ (x ≤ y) + record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _≤_ @@ -182,6 +189,10 @@ record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) open Setoid setoid public + infix 4 _≮_ + _≮_ : Rel Carrier _ + x ≮ y = ¬ (x < y) + record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _<_ From ba82a9d4b1ec55c163758015162e83dd83f43521 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 15 Sep 2023 13:08:52 +0100 Subject: [PATCH 02/33] knock-on changes --- CHANGELOG.md | 3 +++ src/Relation/Binary/Bundles.agda | 2 +- src/Relation/Binary/Properties/Poset.agda | 26 +++++++++++++------ .../Binary/Properties/TotalOrder.agda | 3 +-- 4 files changed, 23 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0b6052baec..a53c7fa905 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -928,6 +928,9 @@ Non-backwards compatible changes lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x) lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x) ``` + + * Moved `_≰_` from `Relation.Binary.Properties.Poset` to `Relation.Binary.Bundles.Poset` (issue #1214) + * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to `¬¬-excluded-middle`. diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index 1d181701d5..430d6a8e35 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -242,7 +242,7 @@ record TotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where } open Poset poset public - using (module Eq; preorder) + using (module Eq; preorder; _≰_) totalPreorder : TotalPreorder c ℓ₁ ℓ₂ totalPreorder = record diff --git a/src/Relation/Binary/Properties/Poset.agda b/src/Relation/Binary/Properties/Poset.agda index add0e20b28..d1eddaebbc 100644 --- a/src/Relation/Binary/Properties/Poset.agda +++ b/src/Relation/Binary/Properties/Poset.agda @@ -20,7 +20,7 @@ open import Relation.Nullary.Negation using (contradiction) module Relation.Binary.Properties.Poset {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where -open Poset P renaming (Carrier to A) +open Poset P renaming (Carrier to A; _≰_ to _≰A_) -- issue #1214 import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict import Relation.Binary.Properties.Preorder preorder as PreorderProperties @@ -62,15 +62,10 @@ open Poset ≥-poset public ------------------------------------------------------------------------ -- Negated order -infix 4 _≰_ - -_≰_ : Rel A p₃ -x ≰ y = ¬ (x ≤ y) - -≰-respˡ-≈ : _≰_ Respectsˡ _≈_ +≰-respˡ-≈ : _≰A_ Respectsˡ _≈_ ≰-respˡ-≈ x≈y = _∘ ≤-respˡ-≈ (Eq.sym x≈y) -≰-respʳ-≈ : _≰_ Respectsʳ _≈_ +≰-respʳ-≈ : _≰A_ Respectsʳ _≈_ ≰-respʳ-≈ x≈y = _∘ ≤-respʳ-≈ (Eq.sym x≈y) ------------------------------------------------------------------------ @@ -133,3 +128,18 @@ mono⇒cong = Consequences.mono⇒cong _≈_ _≈_ Eq.sym reflexive antisym antimono⇒cong : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → f Preserves _≈_ ⟶ _≈_ antimono⇒cong = Consequences.antimono⇒cong _≈_ _≈_ Eq.sym reflexive antisym + + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +infix 4 _≰_ +_≰_ = _≰A_ +{-# WARNING_ON_USAGE _≤_ +"Warning: _≰_ was deprecated in v2.0. Please use Relation.Binary.Bundles.Poset._≰_ instead" +#-} diff --git a/src/Relation/Binary/Properties/TotalOrder.agda b/src/Relation/Binary/Properties/TotalOrder.agda index 540de19905..e5b67c9e11 100644 --- a/src/Relation/Binary/Properties/TotalOrder.agda +++ b/src/Relation/Binary/Properties/TotalOrder.agda @@ -90,8 +90,7 @@ open PosetProperties public open PosetProperties public using - ( _≰_ - ; ≰-respʳ-≈ + ( ≰-respʳ-≈ ; ≰-respˡ-≈ ) From 568ffc3270005748dc83029b55c38bd9e456b925 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 15 Sep 2023 13:46:44 +0100 Subject: [PATCH 03/33] knock-on changes --- src/Relation/Binary/Properties/DecTotalOrder.agda | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Relation/Binary/Properties/DecTotalOrder.agda b/src/Relation/Binary/Properties/DecTotalOrder.agda index 2923a0d047..2075e36a5c 100644 --- a/src/Relation/Binary/Properties/DecTotalOrder.agda +++ b/src/Relation/Binary/Properties/DecTotalOrder.agda @@ -87,8 +87,7 @@ open StrictTotalOrder <-strictTotalOrder public open TotalOrderProperties public using - ( _≰_ - ; ≰-respʳ-≈ + ( ≰-respʳ-≈ ; ≰-respˡ-≈ ; ≰⇒> ; ≰⇒≥ From 3e022d68f9058ebbbec5844fcd432aa1d88c0b07 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 15 Sep 2023 13:56:43 +0100 Subject: [PATCH 04/33] refactored `Poset` to rename field from `Preorder` --- src/Relation/Binary/Bundles.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index 430d6a8e35..f57635b4b5 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -134,12 +134,12 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where } open Preorder preorder public - using (module Eq) - + using (module Eq) renaming (_≁_ to _≰_) +{- infix 4 _≰_ _≰_ : Rel Carrier _ x ≰ y = ¬ (x ≤ y) - +-} record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _≤_ From cfb537a3ce09448a5b858c213c9f6649aeff0796 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 15 Sep 2023 14:54:25 +0100 Subject: [PATCH 05/33] further propagation of the negated relations --- src/Relation/Binary/Bundles.agda | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index f57635b4b5..9a980b2c69 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -110,7 +110,7 @@ record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where preorder = record { isPreorder = isPreorder } open Preorder preorder public - using (module Eq) + using (module Eq) renaming (_≁_ to _≰_) ------------------------------------------------------------------------ @@ -135,11 +135,7 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open Preorder preorder public using (module Eq) renaming (_≁_ to _≰_) -{- - infix 4 _≰_ - _≰_ : Rel Carrier _ - x ≰ y = ¬ (x ≤ y) --} + record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _≤_ @@ -159,7 +155,7 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where } open Poset poset public - using (preorder) + using (preorder; _≰_) module Eq where decSetoid : DecSetoid c ℓ₁ @@ -211,6 +207,8 @@ record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂ { isStrictPartialOrder = isStrictPartialOrder } + open StrictPartialOrder strictPartialOrder using (_≮_) + module Eq where decSetoid : DecSetoid c ℓ₁ @@ -267,7 +265,7 @@ record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where { isTotalOrder = isTotalOrder } - open TotalOrder totalOrder public using (poset; preorder) + open TotalOrder totalOrder public using (poset; preorder; _≰_) decPoset : DecPoset c ℓ₁ ℓ₂ decPoset = record @@ -299,7 +297,7 @@ record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) wh } open StrictPartialOrder strictPartialOrder public - using (module Eq) + using (module Eq; _≮_) decSetoid : DecSetoid c ℓ₁ decSetoid = record From e7d01797d37caca81777429b01e3484471b9062f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 15 Sep 2023 15:03:12 +0100 Subject: [PATCH 06/33] now the relations are definitionally equal --- src/Relation/Binary/Properties/Poset.agda | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/Relation/Binary/Properties/Poset.agda b/src/Relation/Binary/Properties/Poset.agda index d1eddaebbc..d119b9b150 100644 --- a/src/Relation/Binary/Properties/Poset.agda +++ b/src/Relation/Binary/Properties/Poset.agda @@ -6,6 +6,7 @@ {-# OPTIONS --cubical-compatible --safe #-} +open import Data.Product.Base using (_,_) open import Function.Base using (flip; _∘_) open import Relation.Binary.Core using (Rel; _Preserves_⟶_) open import Relation.Binary.Bundles using (Poset; StrictPartialOrder) @@ -85,7 +86,7 @@ _<_ = ToStrict._<_ } open StrictPartialOrder <-strictPartialOrder public - using ( <-resp-≈; <-respʳ-≈; <-respˡ-≈) + using (_≮_; <-resp-≈; <-respʳ-≈; <-respˡ-≈) renaming ( irrefl to <-irrefl ; asym to <-asym @@ -104,6 +105,16 @@ open StrictPartialOrder <-strictPartialOrder public ≤⇒≯ : ∀ {x y} → x ≤ y → ¬ (y < x) ≤⇒≯ = ToStrict.≤⇒≯ antisym +------------------------------------------------------------------------ +-- Relating ≮ and λ x y → ¬ (x < y): now definitionally equal! + +private + ≮⇒¬< : ∀ {x y} → x ≮ y → ¬ (x < y) + ≮⇒¬< x≮y x Date: Fri, 15 Sep 2023 15:09:31 +0100 Subject: [PATCH 07/33] fix-whitespace --- src/Relation/Binary/Properties/Poset.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Relation/Binary/Properties/Poset.agda b/src/Relation/Binary/Properties/Poset.agda index d119b9b150..09f53ffb8d 100644 --- a/src/Relation/Binary/Properties/Poset.agda +++ b/src/Relation/Binary/Properties/Poset.agda @@ -108,7 +108,7 @@ open StrictPartialOrder <-strictPartialOrder public ------------------------------------------------------------------------ -- Relating ≮ and λ x y → ¬ (x < y): now definitionally equal! -private +private ≮⇒¬< : ∀ {x y} → x ≮ y → ¬ (x < y) ≮⇒¬< x≮y x Date: Fri, 15 Sep 2023 17:12:08 +0100 Subject: [PATCH 08/33] one more knock-on import change --- src/Data/List/Sort/MergeSort.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Sort/MergeSort.agda b/src/Data/List/Sort/MergeSort.agda index 9648718d0d..13060a36bc 100644 --- a/src/Data/List/Sort/MergeSort.agda +++ b/src/Data/List/Sort/MergeSort.agda @@ -21,7 +21,7 @@ open import Data.List.Relation.Binary.Permutation.Propositional import Data.List.Relation.Binary.Permutation.Propositional.Properties as Perm open import Data.Maybe.Base using (just) open import Relation.Nullary.Decidable using (does) -open import Data.Nat using (_<_; _>_; z_; z Date: Fri, 15 Sep 2023 18:08:44 +0100 Subject: [PATCH 09/33] =?UTF-8?q?`TotalOrder`=20now=20exports=20`=5F?= =?UTF-8?q?=E2=89=B1=5F`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Relation/Binary/Properties/TotalOrder.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Relation/Binary/Properties/TotalOrder.agda b/src/Relation/Binary/Properties/TotalOrder.agda index e5b67c9e11..48f788ab7f 100644 --- a/src/Relation/Binary/Properties/TotalOrder.agda +++ b/src/Relation/Binary/Properties/TotalOrder.agda @@ -59,7 +59,7 @@ open PosetProperties public } open TotalOrder ≥-totalOrder public - using () renaming (total to ≥-total) + using () renaming (total to ≥-total; _≰_ to _≱_) ------------------------------------------------------------------------ -- _<_ - the strict version is a strict partial order From 8c8fdf6056792c75960049624183c6f19509278d Mon Sep 17 00:00:00 2001 From: James McKinna Date: Fri, 15 Sep 2023 18:11:09 +0100 Subject: [PATCH 10/33] =?UTF-8?q?`Properties.Poset`=20now=20uses=20(rename?= =?UTF-8?q?d)=20`=5F=E2=89=B0=5F`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Relation/Binary/Properties/Poset.agda | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Relation/Binary/Properties/Poset.agda b/src/Relation/Binary/Properties/Poset.agda index 09f53ffb8d..7b8a60fd29 100644 --- a/src/Relation/Binary/Properties/Poset.agda +++ b/src/Relation/Binary/Properties/Poset.agda @@ -21,7 +21,7 @@ open import Relation.Nullary.Negation using (contradiction) module Relation.Binary.Properties.Poset {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where -open Poset P renaming (Carrier to A; _≰_ to _≰A_) -- issue #1214 +open Poset P renaming (Carrier to A; _≰_ to _≰A_) -- issue #1214 see below import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict import Relation.Binary.Properties.Preorder preorder as PreorderProperties @@ -99,10 +99,10 @@ open StrictPartialOrder <-strictPartialOrder public ≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y ≤∧≉⇒< = ToStrict.≤∧≉⇒< -<⇒≱ : ∀ {x y} → x < y → ¬ (y ≤ x) +<⇒≱ : ∀ {x y} → x < y → y ≰A x <⇒≱ = ToStrict.<⇒≱ antisym -≤⇒≯ : ∀ {x y} → x ≤ y → ¬ (y < x) +≤⇒≯ : ∀ {x y} → x ≤ y → y ≮ x ≤⇒≯ = ToStrict.≤⇒≯ antisym ------------------------------------------------------------------------ @@ -149,6 +149,8 @@ antimono⇒cong = Consequences.antimono⇒cong _≈_ _≈_ Eq.sym reflexive anti -- Version 2.0 +-- issue #1214: locally to this module, we rename the relation _≰_, +-- so that we can deprecate it here, yet re-export it elsewhere infix 4 _≰_ _≰_ = _≰A_ {-# WARNING_ON_USAGE _≤_ From 593ee3d65def9f192e139cf710c6c14a0bcdd84f Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 16 Sep 2023 07:09:00 +0100 Subject: [PATCH 11/33] much more extensive documentation --- CHANGELOG.md | 68 ++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 58 insertions(+), 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index a53c7fa905..d611459179 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -762,6 +762,40 @@ Non-backwards compatible changes IO.Effectful IO.Instances ``` +### (Issue #1214) Reorganisation of the introduction of negated relation symbols under `Relation.Binary` + +* Previously, negated relation symbols `_≰_` (for `Poset`) and `_≮_` (`StrictPartialOrder`) + were introduced in the corresponding `Relation.Binary.Properties` modules, for re-export. + +* Now they are introduced as definitions in the corresponding `Relation.Binary.Bundles`, + together with, for uniformity's sake, an additional negated symbol `_≁_` for `Preorder`. + +* Accordingly, `_≰_` is in fact now a renamed `public` re-export from `Preorder` + in each of `TotalPreorder` and `Poset`, as the negated version of the corresponding + symbol introduced as a field name for the relation there. + +* As knock-on changes, public re-exports of `Preorder`, `Poset`, `StrictPartialOrder` + in derived bundles also now need to re-export the new symbols accordingly. + +* Backwards compatibility has been maintained, with deprecated definitions in the + corresponding `Relation.Binary.Properties` modules, and the corresponding client + client module `import`s being adjusted accordingly. + +* Elsewhere under `Relation.Binary.Properties` etc. the use of *explicitly* negated + relation symbols have now been replaced by their definitionally equal counterparts + using the new symbols accordingly. + +* NB modules such as `Relation.Binary.Construct.NonStrictToStrict` which operate + only on the the underlying `Structures` such as `IsPartialOrder` etc., are unable + to make use of the new symbols. + +* NB the corresponding situation regarding the `flip`ped relation symbols `_≥_`, + `_>_` (and their negated versions!) has not (yet) been addressed; to develop + a parallel architecture to that above, there would need to be a suitable symbol + for the flipped relation `_∼_` (and its negation!) in `Relation.Bundles.Preorder`, + now handled purely semantically via `flip ∼` in `Relation.Binary.Properties.Preorder`, + `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}` etc. Similarly, for the strict + ordering relation `_<_` defined in `Relation.Binary.Properties.Poset`... ### Other @@ -929,8 +963,6 @@ Non-backwards compatible changes lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x) ``` - * Moved `_≰_` from `Relation.Binary.Properties.Poset` to `Relation.Binary.Bundles.Poset` (issue #1214) - * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to `¬¬-excluded-middle`. @@ -1501,6 +1533,16 @@ Deprecated names invPreorder ↦ converse-preorder ``` +* Moved negated relation symbol from `Relation.Binary.Properties.Poset`: + ``` + _≰_ ↦ Relation.Binary.Bundles.Poset._≰_ + ``` + +* Moved negated relation symbol from `Relation.Binary.Properties.TotalOrder`: + ``` + _≮_ ↦ Relation.Binary.Bundles.StrictPartialOrder._≮_ + ``` + ### Renamed Data.Erased to Data.Irrelevant * This fixes the fact we had picked the wrong name originally. The erased modality @@ -1812,14 +1854,6 @@ Other minor changes ``` and their corresponding algebraic subbundles. - The following negated relation symbols have now been added - ```agda - infix 4 _≁_ _≰_ _≮_ - Preorder._≁_ : Rel Carrier _ - Poset._≰_ : Rel Carrier _ - StrictPartialOrder._≮_ : Rel Carrier _ - ``` - * Added new proofs to `Algebra.Consequences.Base`: ```agda reflexive+selfInverse⇒involutive : Reflexive _≈_ → @@ -2815,6 +2849,20 @@ Other minor changes prependVLams : List String → Term → Term ``` +* Added new definitions to `Relation.Binary.Bundles`: + + The following negated relation symbols have now been added, with their + (obvious) intended semantics: + ```agda + infix 4 _≁_ _≰_ _≮_ + Preorder._≁_ : Rel Carrier _ + StrictPartialOrder._≮_ : Rel Carrier _ + ``` + Additionally, `Poset._≰_` is defined by renaming public export of `Preorder._≁_` + + The corresponding former definitions in `Relation.Binary.Properties.*` + have been deprecated. + * Added new operations in `Relation.Binary.Construct.Closure.Equivalence`: ``` fold : IsEquivalence _∼_ → _⟶_ ⇒ _∼_ → EqClosure _⟶_ ⇒ _∼_ From 5f1cbe9d6c346d4b1d8ed3fb3c945b46ffd49746 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 16 Sep 2023 07:15:38 +0100 Subject: [PATCH 12/33] replaced negated relation by its definitional equivalent --- src/Relation/Binary/Properties/DecTotalOrder.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Relation/Binary/Properties/DecTotalOrder.agda b/src/Relation/Binary/Properties/DecTotalOrder.agda index 2075e36a5c..65a7c561d2 100644 --- a/src/Relation/Binary/Properties/DecTotalOrder.agda +++ b/src/Relation/Binary/Properties/DecTotalOrder.agda @@ -80,7 +80,7 @@ open TotalOrderProperties public } open StrictTotalOrder <-strictTotalOrder public - using () renaming (compare to <-compare) + using (_≮_) renaming (compare to <-compare) ------------------------------------------------------------------------ -- _≰_ - the negated order @@ -93,5 +93,5 @@ open TotalOrderProperties public ; ≰⇒≥ ) -≮⇒≥ : ∀ {x y} → ¬ (x < y) → y ≤ x +≮⇒≥ : ∀ {x y} → x ≮ y → y ≤ x ≮⇒≥ = ToStrict.≮⇒≥ Eq.sym _≟_ reflexive total From 91ac637023a6b0a0405039acc40fe926802af722 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 16 Sep 2023 07:17:41 +0100 Subject: [PATCH 13/33] `inverse` should be `converse` --- src/Relation/Binary/Properties/StrictPartialOrder.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Relation/Binary/Properties/StrictPartialOrder.agda b/src/Relation/Binary/Properties/StrictPartialOrder.agda index 7420a2e24f..680323c770 100644 --- a/src/Relation/Binary/Properties/StrictPartialOrder.agda +++ b/src/Relation/Binary/Properties/StrictPartialOrder.agda @@ -17,7 +17,7 @@ import Relation.Binary.Construct.StrictToNonStrict open StrictPartialOrder SPO ------------------------------------------------------------------------ --- The inverse relation is also a strict partial order. +-- The converse relation is also a strict partial order. >-strictPartialOrder : StrictPartialOrder s₁ s₂ s₃ >-strictPartialOrder = EqAndOrd.strictPartialOrder SPO From 1d8dd808db868ffb3f385e8a2842ee754423c32e Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 16 Sep 2023 08:06:25 +0100 Subject: [PATCH 14/33] revised deprecations --- CHANGELOG.md | 42 ++++++++++--------- .../Binary/Properties/StrictTotalOrder.agda | 19 ++++++++- .../Binary/Properties/TotalOrder.agda | 23 ++++++++-- 3 files changed, 60 insertions(+), 24 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d611459179..29975dec65 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -354,8 +354,8 @@ Non-backwards compatible changes * The module `Function.Definitions` no longer has two equalities as module arguments, as they did not interact as intended with the re-exports from `Function.Definitions.(Core1/Core2)`. The latter have been removed and their definitions folded into `Function.Definitions`. - -* In `Function.Definitions` the types of `Surjective`, `Injective` and `Surjective` + +* In `Function.Definitions` the types of `Surjective`, `Injective` and `Surjective` have been changed from: ``` Surjective f = ∀ y → ∃ λ x → f x ≈₂ y @@ -370,16 +370,16 @@ Non-backwards compatible changes ``` This is for several reasons: i) the new definitions compose much more easily, ii) Agda can better infer the equalities used. - + To ease backwards compatibility: - - the old definitions have been moved to the new names `StrictlySurjective`, - `StrictlyInverseˡ` and `StrictlyInverseʳ`. - - The records in `Function.Structures` and `Function.Bundles` export proofs - of these under the names `strictlySurjective`, `strictlyInverseˡ` and - `strictlyInverseʳ`, + - the old definitions have been moved to the new names `StrictlySurjective`, + `StrictlyInverseˡ` and `StrictlyInverseʳ`. + - The records in `Function.Structures` and `Function.Bundles` export proofs + of these under the names `strictlySurjective`, `strictlyInverseˡ` and + `strictlyInverseʳ`, - Conversion functions have been added in both directions to - `Function.Consequences(.Propositional)`. - + `Function.Consequences(.Propositional)`. + #### Proofs of non-zeroness/positivity/negativity as instance arguments * Many numeric operations in the library require their arguments to be non-zero, @@ -762,20 +762,22 @@ Non-backwards compatible changes IO.Effectful IO.Instances ``` -### (Issue #1214) Reorganisation of the introduction of negated relation symbols under `Relation.Binary` +### (Issue #1214) Reorganisation of the introduction of negated relation symbols under `Relation.Binary` -* Previously, negated relation symbols `_≰_` (for `Poset`) and `_≮_` (`StrictPartialOrder`) - were introduced in the corresponding `Relation.Binary.Properties` modules, for re-export. +* Previously, negated relation symbols `_≰_` (for `Poset`) and `_≮_` (`TotalOrder`) + were introduced in the corresponding `Relation.Binary.Properties` modules, for re-export. * Now they are introduced as definitions in the corresponding `Relation.Binary.Bundles`, - together with, for uniformity's sake, an additional negated symbol `_≁_` for `Preorder`. + together with, for uniformity's sake, an additional negated symbol `_≁_` for `Preorder`. + NB `_≮_` is now introduced *earlier* in the hierarchy, at `StrictPartialOrder`, which + incurs some rather complicated deprecation gymnastics... * Accordingly, `_≰_` is in fact now a renamed `public` re-export from `Preorder` in each of `TotalPreorder` and `Poset`, as the negated version of the corresponding symbol introduced as a field name for the relation there. * As knock-on changes, public re-exports of `Preorder`, `Poset`, `StrictPartialOrder` - in derived bundles also now need to re-export the new symbols accordingly. + in derived bundles also now need to re-export the new symbols accordingly. * Backwards compatibility has been maintained, with deprecated definitions in the corresponding `Relation.Binary.Properties` modules, and the corresponding client @@ -783,11 +785,11 @@ Non-backwards compatible changes * Elsewhere under `Relation.Binary.Properties` etc. the use of *explicitly* negated relation symbols have now been replaced by their definitionally equal counterparts - using the new symbols accordingly. + using the new symbols accordingly. * NB modules such as `Relation.Binary.Construct.NonStrictToStrict` which operate only on the the underlying `Structures` such as `IsPartialOrder` etc., are unable - to make use of the new symbols. + to make use of the new symbols. * NB the corresponding situation regarding the `flip`ped relation symbols `_≥_`, `_>_` (and their negated versions!) has not (yet) been addressed; to develop @@ -2298,7 +2300,7 @@ Other minor changes length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length - + take-map : take n (map f xs) ≡ map f (take n xs) drop-map : drop n (map f xs) ≡ map f (drop n xs) head-map : head (map f xs) ≡ Maybe.map f (head xs) @@ -2859,9 +2861,9 @@ Other minor changes StrictPartialOrder._≮_ : Rel Carrier _ ``` Additionally, `Poset._≰_` is defined by renaming public export of `Preorder._≁_` - + The corresponding former definitions in `Relation.Binary.Properties.*` - have been deprecated. + have been deprecated. * Added new operations in `Relation.Binary.Construct.Closure.Equivalence`: ``` diff --git a/src/Relation/Binary/Properties/StrictTotalOrder.agda b/src/Relation/Binary/Properties/StrictTotalOrder.agda index f8b0062474..dc4c046e06 100644 --- a/src/Relation/Binary/Properties/StrictTotalOrder.agda +++ b/src/Relation/Binary/Properties/StrictTotalOrder.agda @@ -12,7 +12,9 @@ module Relation.Binary.Properties.StrictTotalOrder {s₁ s₂ s₃} (STO : StrictTotalOrder s₁ s₂ s₃) where -open StrictTotalOrder STO +-- issue #1214: locally to this module, we hide the relation _≮_, so +-- that we can deprecate its export here, yet re-export it elsewhere +open StrictTotalOrder STO hiding (_≮_) open import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ import Relation.Binary.Properties.StrictPartialOrder as SPO open import Relation.Binary.Consequences @@ -26,3 +28,18 @@ decTotalOrder = record } open DecTotalOrder decTotalOrder public + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +-- issue #1214: see above +infix 4 _≮_ +_≮_ = StrictTotalOrder._≮_ STO +{-# WARNING_ON_USAGE _≮_ +"Warning: export of _≮_ from this module was deprecated in v2.0. Please import from Relation.Binary.Bundles.StrictPartialOrder._≮_ instead" +#-} diff --git a/src/Relation/Binary/Properties/TotalOrder.agda b/src/Relation/Binary/Properties/TotalOrder.agda index 48f788ab7f..d8b7853d69 100644 --- a/src/Relation/Binary/Properties/TotalOrder.agda +++ b/src/Relation/Binary/Properties/TotalOrder.agda @@ -13,7 +13,9 @@ open import Relation.Binary.Structures using (IsTotalOrder) module Relation.Binary.Properties.TotalOrder {t₁ t₂ t₃} (T : TotalOrder t₁ t₂ t₃) where -open TotalOrder T +-- issue #1214: locally to this module, we rename the relation _≰_, so +-- that we can deprecate it here, yet re-export it elsewhere +open TotalOrder T renaming (_≰_ to _≰A_) open import Data.Product.Base using (proj₁) open import Data.Sum.Base using (inj₁; inj₂) @@ -94,8 +96,23 @@ open PosetProperties public ; ≰-respˡ-≈ ) -≰⇒> : ∀ {x y} → x ≰ y → y < x +≰⇒> : ∀ {x y} → x ≰A y → y < x ≰⇒> = ToStrict.≰⇒> Eq.sym reflexive total -≰⇒≥ : ∀ {x y} → x ≰ y → y ≤ x +≰⇒≥ : ∀ {x y} → x ≰A y → y ≤ x ≰⇒≥ x≰y = proj₁ (≰⇒> x≰y) + +------------------------------------------------------------------------ +-- DEPRECATED +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.0 + +-- issue #1214: see above +infix 4 _≰_ +_≰_ = _≰A_ +{-# WARNING_ON_USAGE _≰_ +"Warning: export of _≰_ from this module was deprecated in v2.0. Please import from Relation.Binary.Bundles.Poset instead" +#-} From ae4be25c6ba7743996c87e5032d89d2d8b2e2695 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 16 Sep 2023 08:30:27 +0100 Subject: [PATCH 15/33] removed redundant `private` block --- src/Relation/Binary/Properties/Poset.agda | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/src/Relation/Binary/Properties/Poset.agda b/src/Relation/Binary/Properties/Poset.agda index 7b8a60fd29..96cc72398d 100644 --- a/src/Relation/Binary/Properties/Poset.agda +++ b/src/Relation/Binary/Properties/Poset.agda @@ -105,16 +105,6 @@ open StrictPartialOrder <-strictPartialOrder public ≤⇒≯ : ∀ {x y} → x ≤ y → y ≮ x ≤⇒≯ = ToStrict.≤⇒≯ antisym ------------------------------------------------------------------------- --- Relating ≮ and λ x y → ¬ (x < y): now definitionally equal! - -private - ≮⇒¬< : ∀ {x y} → x ≮ y → ¬ (x < y) - ≮⇒¬< x≮y x Date: Sat, 16 Sep 2023 08:42:29 +0100 Subject: [PATCH 16/33] revised deprecation strategy, again --- src/Relation/Binary/Properties/DecTotalOrder.agda | 13 +++++++++++-- .../Binary/Properties/StrictTotalOrder.agda | 4 ++-- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/Relation/Binary/Properties/DecTotalOrder.agda b/src/Relation/Binary/Properties/DecTotalOrder.agda index 65a7c561d2..ce00a08cad 100644 --- a/src/Relation/Binary/Properties/DecTotalOrder.agda +++ b/src/Relation/Binary/Properties/DecTotalOrder.agda @@ -12,9 +12,11 @@ open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder) module Relation.Binary.Properties.DecTotalOrder - {d₁ d₂ d₃} (DT : DecTotalOrder d₁ d₂ d₃) where + {d₁ d₂ d₃} (DTO : DecTotalOrder d₁ d₂ d₃) where -open DecTotalOrder DT hiding (trans) +-- issue #1214: locally to this module, we hide the relation _≰_, so +-- that we can deprecate its export here, yet re-export it elsewhere +open DecTotalOrder DTO hiding (trans; _≰_) import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict @@ -95,3 +97,10 @@ open TotalOrderProperties public ≮⇒≥ : ∀ {x y} → x ≮ y → y ≤ x ≮⇒≥ = ToStrict.≮⇒≥ Eq.sym _≟_ reflexive total + +-- issue #1214: see above +infix 4 _≰_ +_≰_ = DecTotalOrder._≰_ DTO +{-# WARNING_ON_USAGE _≰_ +"Warning: export of _≰_ from this module was deprecated in v2.0, in favour of a direct public export from Relation.Binary.Bundles.Poset instead" +#-} diff --git a/src/Relation/Binary/Properties/StrictTotalOrder.agda b/src/Relation/Binary/Properties/StrictTotalOrder.agda index dc4c046e06..1f5b0fbc1a 100644 --- a/src/Relation/Binary/Properties/StrictTotalOrder.agda +++ b/src/Relation/Binary/Properties/StrictTotalOrder.agda @@ -20,7 +20,7 @@ import Relation.Binary.Properties.StrictPartialOrder as SPO open import Relation.Binary.Consequences ------------------------------------------------------------------------ --- _<_ - the strict version is a strict total order +-- _<_ - the strict version is a decidable total order decTotalOrder : DecTotalOrder _ _ _ decTotalOrder = record @@ -41,5 +41,5 @@ open DecTotalOrder decTotalOrder public infix 4 _≮_ _≮_ = StrictTotalOrder._≮_ STO {-# WARNING_ON_USAGE _≮_ -"Warning: export of _≮_ from this module was deprecated in v2.0. Please import from Relation.Binary.Bundles.StrictPartialOrder._≮_ instead" +"Warning: export of _≮_ from this module was deprecated in v2.0, in favour of a direct public export from Relation.Binary.Bundles.StrictPartialOrder instead" #-} From 5575ab44ffc70636979d13a90636b26cf78ed969 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 16 Sep 2023 08:53:51 +0100 Subject: [PATCH 17/33] revised forward pointer to issues #2096 #2098 --- CHANGELOG.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 29975dec65..ed0ba9a0b8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -791,13 +791,13 @@ Non-backwards compatible changes only on the the underlying `Structures` such as `IsPartialOrder` etc., are unable to make use of the new symbols. -* NB the corresponding situation regarding the `flip`ped relation symbols `_≥_`, - `_>_` (and their negated versions!) has not (yet) been addressed; to develop - a parallel architecture to that above, there would need to be a suitable symbol - for the flipped relation `_∼_` (and its negation!) in `Relation.Bundles.Preorder`, - now handled purely semantically via `flip ∼` in `Relation.Binary.Properties.Preorder`, - `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}` etc. Similarly, for the strict - ordering relation `_<_` defined in `Relation.Binary.Properties.Poset`... +* NB (issues #2096 #2098) the corresponding situation regarding the `flip`ped + relation symbols `_≥_`, `_>_` (and their negated versions!) has not (yet) + been addressed; to develop a parallel architecture to that above, there + would need to be a suitable symbol for the flipped relation `_∼_` (and its negation!) + in `Relation.Bundles.Preorder`, currently handled purely semantically via `flip ∼` + in `Relation.Binary.Properties.Preorder`, `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}` + etc. Similarly, for the strict ordering relation `_<_` defined in `Relation.Binary.Properties.Poset`... ### Other From b730e8d1af366f6fc8b7afaaa184d9e2f92deef0 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Sat, 16 Sep 2023 16:06:51 +0100 Subject: [PATCH 18/33] cosmetic symbol change, plus updated `CHANGELOG` to describe it --- CHANGELOG.md | 19 +++++++++---------- src/Relation/Binary/Bundles.agda | 2 +- 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ed0ba9a0b8..c3bcb3c3be 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -772,12 +772,11 @@ Non-backwards compatible changes NB `_≮_` is now introduced *earlier* in the hierarchy, at `StrictPartialOrder`, which incurs some rather complicated deprecation gymnastics... -* Accordingly, `_≰_` is in fact now a renamed `public` re-export from `Preorder` - in each of `TotalPreorder` and `Poset`, as the negated version of the corresponding - symbol introduced as a field name for the relation there. +* Accordingly, in fact we now have `_⋦_` (in `TotalPreorder`) and `_≰_` (in `Poset`) + as renamed `public` re-exports from `_≁_` in `Preorder`. * As knock-on changes, public re-exports of `Preorder`, `Poset`, `StrictPartialOrder` - in derived bundles also now need to re-export the new symbols accordingly. + in derived bundles also now need to re-export the various new symbols accordingly. * Backwards compatibility has been maintained, with deprecated definitions in the corresponding `Relation.Binary.Properties` modules, and the corresponding client @@ -792,12 +791,12 @@ Non-backwards compatible changes to make use of the new symbols. * NB (issues #2096 #2098) the corresponding situation regarding the `flip`ped - relation symbols `_≥_`, `_>_` (and their negated versions!) has not (yet) - been addressed; to develop a parallel architecture to that above, there - would need to be a suitable symbol for the flipped relation `_∼_` (and its negation!) - in `Relation.Bundles.Preorder`, currently handled purely semantically via `flip ∼` - in `Relation.Binary.Properties.Preorder`, `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}` - etc. Similarly, for the strict ordering relation `_<_` defined in `Relation.Binary.Properties.Poset`... + relation symbols `_≥_`, `_>_` (and their negated versions!) has not (yet) been + addressed; to develop a parallel architecture to that above, there would need + to be a suitable symbol for the flipped relation `_∼_` (and its negation!) in + `Relation.Bundles.Preorder`, currently handled purely semantically via `flip ∼` in + `Relation.Binary.Properties.Preorder`, `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}` + etc. Ditto. the strict ordering relation `_<_` defined in `Relation.Binary.Properties.Poset`... ### Other diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index 9a980b2c69..4858035f52 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -110,7 +110,7 @@ record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where preorder = record { isPreorder = isPreorder } open Preorder preorder public - using (module Eq) renaming (_≁_ to _≰_) + using (module Eq) renaming (_≁_ to _⋦_) ------------------------------------------------------------------------ From 4b52284770dcb97d73baaa506c04361a618194f1 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 4 Oct 2023 12:00:02 +0100 Subject: [PATCH 19/33] revised `CHANGELOG` after merge of #2114 --- CHANGELOG.md | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3d9dd8621b..7b318598c7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -802,12 +802,12 @@ Non-backwards compatible changes were introduced in the corresponding `Relation.Binary.Properties` modules, for re-export. * Now they are introduced as definitions in the corresponding `Relation.Binary.Bundles`, - together with, for uniformity's sake, an additional negated symbol `_≁_` for `Preorder`. + together with, for uniformity's sake, an additional negated symbol `_⋦_` for `Preorder`. NB `_≮_` is now introduced *earlier* in the hierarchy, at `StrictPartialOrder`, which incurs some rather complicated deprecation gymnastics... -* Accordingly, in fact we now have `_⋦_` (in `TotalPreorder`) and `_≰_` (in `Poset`) - as renamed `public` re-exports from `_≁_` in `Preorder`. +* Accordingly, in fact we now have `_≰_` (in `Poset`) as a renamed `public` re-export + from `_⋦_` in `Preorder`, with `TotalPreorder` inheriting `_⋦_` from `Preorder`. * As knock-on changes, public re-exports of `Preorder`, `Poset`, `StrictPartialOrder` in derived bundles also now need to re-export the various new symbols accordingly. @@ -824,13 +824,9 @@ Non-backwards compatible changes only on the the underlying `Structures` such as `IsPartialOrder` etc., are unable to make use of the new symbols. -* NB (issues #2096 #2098) the corresponding situation regarding the `flip`ped - relation symbols `_≥_`, `_>_` (and their negated versions!) has not (yet) been - addressed; to develop a parallel architecture to that above, there would need - to be a suitable symbol for the flipped relation `_∼_` (and its negation!) in - `Relation.Bundles.Preorder`, currently handled purely semantically via `flip ∼` in - `Relation.Binary.Properties.Preorder`, `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}` - etc. Ditto. the strict ordering relation `_<_` defined in `Relation.Binary.Properties.Poset`... +* NB (issue #2098) the corresponding situation regarding the `flip`ped relation + symbols `_≥_`, `_>_` (and their negated versions!) has not (yet) been addressed. + Ditto. the strict ordering relation `_<_` defined in `Relation.Binary.Properties.Poset`... ### Changes to triple reasoning interface From ec79e09917e259d2fec0dd4a391dd1f18a47f176 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 4 Oct 2023 12:32:43 +0100 Subject: [PATCH 20/33] further revised `CHANGELOG` after merge of #2114 --- CHANGELOG.md | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1d9e024189..cde9dacf58 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -601,7 +601,7 @@ Non-backwards compatible changes raw bundles to `Data.X.Base`, this definition can now be made directly. Knock-on consequences include the need to retain the old constructor name, now introduced as a pattern synonym, and introduction of (a function equivalent to) the former - field name/projection function `proof` as `≤″-proof` in `Data.Nat.Properties`. + field name/projection function `proof` as `≤″-proof` in `Data.Nat.Properties`. * Accordingly, the definition has been changed to: ```agda @@ -867,9 +867,8 @@ Non-backwards compatible changes Therefore, only _declarations_ of `PartialOrder` records will need their field names updating. -* NB (issues #1214 #2098) the corresponding situation regarding the `flip`ped - relation symbols `_≥_`, `_>_` (and their negated versions!) has not (yet) - been addressed. +* NB (issue #2098) the corresponding situation regarding the `flip`ped + relation symbols `_≥_`, `_>_` has not (yet) been addressed. ### Standardisation of `insertAt`/`updateAt`/`removeAt` @@ -890,12 +889,12 @@ Non-backwards compatible changes ``` _─_ ↦ removeAt ``` - + * In `Data.Vec.Base`: ```agda insert ↦ insertAt remove ↦ removeAt - + updateAt : Fin n → (A → A) → Vec A n → Vec A n ↦ updateAt : Vec A n → Fin n → (A → A) → Vec A n @@ -906,12 +905,12 @@ Non-backwards compatible changes remove : Fin (suc n) → Vector A (suc n) → Vector A n ↦ removeAt : Vector A (suc n) → Fin (suc n) → Vector A n - + updateAt : Fin n → (A → A) → Vector A n → Vector A n ↦ updateAt : Vector A n → Fin n → (A → A) → Vector A n ``` - + * The old names (and the names of all proofs about these functions) have been deprecated appropriately. ### Changes to triple reasoning interface @@ -1656,7 +1655,7 @@ Deprecated names take-drop-id ↦ take++drop≡id map-insert ↦ map-insertAt - + insert-lookup ↦ insertAt-lookup insert-punchIn ↦ insertAt-punchIn remove-PunchOut ↦ removeAt-punchOut @@ -1682,7 +1681,7 @@ Deprecated names updateAt-cong-relative ↦ updateAt-cong-local map-updateAt ↦ map-updateAt-local - + insert-lookup ↦ insertAt-lookup insert-punchIn ↦ insertAt-punchIn remove-punchOut ↦ removeAt-punchOut From d4f2c7903a3d0333b77e8647d58c97064aa90993 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 4 Oct 2023 12:43:08 +0100 Subject: [PATCH 21/33] further revised `CHANGELOG` after merge of #2099; erroneous prior commit msgs refer to 2114 --- CHANGELOG.md | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index cde9dacf58..0d636d5c32 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -822,6 +822,22 @@ 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. + +* NB (issue #2098) the corresponding situation regarding the `flip`ped + relation symbols `_≥_`, `_>_` has not (yet) been addressed. + ### (Issue #1214) Reorganisation of the introduction of negated relation symbols under `Relation.Binary` * Previously, negated relation symbols `_≰_` (for `Poset`) and `_≮_` (`TotalOrder`) @@ -854,22 +870,6 @@ Non-backwards compatible changes symbols `_≥_`, `_>_` (and their negated versions!) has not (yet) been addressed. Ditto. the strict ordering relation `_<_` defined in `Relation.Binary.Properties.Poset`... -### (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. - -* NB (issue #2098) the corresponding situation regarding the `flip`ped - relation symbols `_≥_`, `_>_` has not (yet) been addressed. - ### Standardisation of `insertAt`/`updateAt`/`removeAt` * Previously, the names and argument order of index-based insertion, update and removal functions for From 3a354cf23999d2e0bb2814582bacf4fc9439ed54 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 4 Oct 2023 13:13:39 +0100 Subject: [PATCH 22/33] further revised `CHANGELOG` after merge of #2099 --- CHANGELOG.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 0d636d5c32..325d18e417 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3128,11 +3128,11 @@ Additions to existing modules The following negated relation symbols have now been added, with their (obvious) intended semantics: ```agda - infix 4 _≁_ _≰_ _≮_ - Preorder._≁_ : Rel Carrier _ + infix 4 _⋦_ _≰_ _≮_ + Preorder._⋦_ : Rel Carrier _ StrictPartialOrder._≮_ : Rel Carrier _ ``` - Additionally, `Poset._≰_` is defined by renaming public export of `Preorder._≁_` + Additionally, `Poset._≰_` is defined by renaming public export of `Preorder._⋦_` The corresponding former definitions in `Relation.Binary.Properties.*` have been deprecated. From 6fd62b019d89d980e57155acec802ef5715aae75 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 4 Oct 2023 13:38:39 +0100 Subject: [PATCH 23/33] further revised `CHANGELOG`: fixing notational errors --- CHANGELOG.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 325d18e417..ac32fb9bac 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -3290,9 +3290,9 @@ Additions to existing modules * Added new proofs to `Relation.Binary.Consequences`: ``` - sym⇒¬-sym : Symmetric _∼_ → Symmetric _≁_ - cotrans⇒¬-trans : Cotransitive _∼_ → Transitive _≁_ - irrefl⇒¬-refl : Reflexive _≈_ → Irreflexive _≈_ _∼_ → Reflexive _≁_ + sym⇒¬-sym : Symmetric _∼_ → Symmetric (¬_ ∘₂ _∼_) + cotrans⇒¬-trans : Cotransitive _∼_ → Transitive (¬_ ∘₂ _∼_) + irrefl⇒¬-refl : Reflexive _≈_ → Irreflexive _≈_ _∼_ → Reflexive (¬_ ∘₂ _∼_) mono₂⇒cong₂ : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} → f Preserves₂ ≤₁ ⟶ ≤₁ ⟶ ≤₂ → f Preserves₂ ≈₁ ⟶ ≈₁ ⟶ ≈₂ From 82f00dcf8812f19ddc3775fc84a5dae2df5ea60d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 7 Oct 2023 05:50:25 +0100 Subject: [PATCH 24/33] removed one extraneous `CHANGELOG` note --- CHANGELOG.md | 3 --- 1 file changed, 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8071eef17a..71ffe1aad9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -868,9 +868,6 @@ Non-backwards compatible changes NB `_≮_` is now introduced *earlier* in the hierarchy, at `StrictPartialOrder`, which incurs some rather complicated deprecation gymnastics... -* Accordingly, in fact we now have `_≰_` (in `Poset`) as a renamed `public` re-export - from `_⋦_` in `Preorder`, with `TotalPreorder` inheriting `_⋦_` from `Preorder`. - * As knock-on changes, public re-exports of `Preorder`, `Poset`, `StrictPartialOrder` in derived bundles also now need to re-export the various new symbols accordingly. From 8eb7271a3ba88c547b1c84be70636bb3c05fbe14 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 7 Oct 2023 05:51:42 +0100 Subject: [PATCH 25/33] removed one more extraneous `CHANGELOG` note --- CHANGELOG.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 71ffe1aad9..6018a36175 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -875,10 +875,6 @@ Non-backwards compatible changes corresponding `Relation.Binary.Properties` modules, and the corresponding client client module `import`s being adjusted accordingly. -* Elsewhere under `Relation.Binary.Properties` etc. the use of *explicitly* negated - relation symbols have now been replaced by their definitionally equal counterparts - using the new symbols accordingly. - * NB modules such as `Relation.Binary.Construct.NonStrictToStrict` which operate only on the the underlying `Structures` such as `IsPartialOrder` etc., are unable to make use of the new symbols. From 1aaae22a57495caad2688bca9c7dc642294211df Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 7 Oct 2023 05:52:45 +0100 Subject: [PATCH 26/33] removed one more extraneous `CHANGELOG` note --- CHANGELOG.md | 3 --- 1 file changed, 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6018a36175..ccee10d9e9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -868,9 +868,6 @@ Non-backwards compatible changes NB `_≮_` is now introduced *earlier* in the hierarchy, at `StrictPartialOrder`, which incurs some rather complicated deprecation gymnastics... -* As knock-on changes, public re-exports of `Preorder`, `Poset`, `StrictPartialOrder` - in derived bundles also now need to re-export the various new symbols accordingly. - * Backwards compatibility has been maintained, with deprecated definitions in the corresponding `Relation.Binary.Properties` modules, and the corresponding client client module `import`s being adjusted accordingly. From cf720b3a1e36bbbfb9743159d168f455666185e3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 7 Oct 2023 05:54:05 +0100 Subject: [PATCH 27/33] removed one more extraneous `CHANGELOG` note: forward pointer to #2098 --- CHANGELOG.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index ccee10d9e9..38b95bda67 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -876,10 +876,6 @@ Non-backwards compatible changes only on the the underlying `Structures` such as `IsPartialOrder` etc., are unable to make use of the new symbols. -* NB (issue #2098) the corresponding situation regarding the `flip`ped relation - symbols `_≥_`, `_>_` (and their negated versions!) has not (yet) been addressed. - Ditto. the strict ordering relation `_<_` defined in `Relation.Binary.Properties.Poset`... - ### Standardisation of `insertAt`/`updateAt`/`removeAt` * Previously, the names and argument order of index-based insertion, update and removal functions for From c52034014413188e12ceac31047a639509189303 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 7 Oct 2023 05:54:20 +0100 Subject: [PATCH 28/33] removed one more extraneous `CHANGELOG` note: forward pointer to #2098 --- CHANGELOG.md | 3 --- 1 file changed, 3 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 38b95bda67..6e7854bc19 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -855,9 +855,6 @@ Non-backwards compatible changes Therefore, only _declarations_ of `PartialOrder` records will need their field names updating. -* NB (issue #2098) the corresponding situation regarding the `flip`ped - relation symbols `_≥_`, `_>_` has not (yet) been addressed. - ### (Issue #1214) Reorganisation of the introduction of negated relation symbols under `Relation.Binary` * Previously, negated relation symbols `_≰_` (for `Poset`) and `_≮_` (`TotalOrder`) From dfc76ed25c5ba68dd8a8f2b5413b5967dda75155 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 7 Oct 2023 05:56:09 +0100 Subject: [PATCH 29/33] removed one more extraneous `CHANGELOG` note: NB --- CHANGELOG.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6e7854bc19..3f573c4376 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -869,10 +869,6 @@ Non-backwards compatible changes corresponding `Relation.Binary.Properties` modules, and the corresponding client client module `import`s being adjusted accordingly. -* NB modules such as `Relation.Binary.Construct.NonStrictToStrict` which operate - only on the the underlying `Structures` such as `IsPartialOrder` etc., are unable - to make use of the new symbols. - ### Standardisation of `insertAt`/`updateAt`/`removeAt` * Previously, the names and argument order of index-based insertion, update and removal functions for From c9e7010f11ce06ac6e3f1129fdb568d2e4e6152f Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 7 Oct 2023 06:04:18 +0100 Subject: [PATCH 30/33] removed one more extraneous `CHANGELOG` note: NB; plus relocated text --- CHANGELOG.md | 26 +++++++++----------------- 1 file changed, 9 insertions(+), 17 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3f573c4376..9a9e3869d4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -861,14 +861,20 @@ Non-backwards compatible changes were introduced in the corresponding `Relation.Binary.Properties` modules, for re-export. * Now they are introduced as definitions in the corresponding `Relation.Binary.Bundles`, - together with, for uniformity's sake, an additional negated symbol `_⋦_` for `Preorder`. - NB `_≮_` is now introduced *earlier* in the hierarchy, at `StrictPartialOrder`, which - incurs some rather complicated deprecation gymnastics... + together with, for uniformity's sake, an additional negated symbol `_⋦_` for `Preorder`, + with their (obvious) intended semantics: + ```agda + infix 4 _⋦_ _≰_ _≮_ + Preorder._⋦_ : Rel Carrier _ + StrictPartialOrder._≮_ : Rel Carrier _ + ``` + Additionally, `Poset._≰_` is defined by renaming public export of `Preorder._⋦_` * Backwards compatibility has been maintained, with deprecated definitions in the corresponding `Relation.Binary.Properties` modules, and the corresponding client client module `import`s being adjusted accordingly. + ### Standardisation of `insertAt`/`updateAt`/`removeAt` * Previously, the names and argument order of index-based insertion, update and removal functions for @@ -3162,20 +3168,6 @@ Additions to existing modules prependVLams : List String → Term → Term ``` -* Added new definitions to `Relation.Binary.Bundles`: - - The following negated relation symbols have now been added, with their - (obvious) intended semantics: - ```agda - infix 4 _⋦_ _≰_ _≮_ - Preorder._⋦_ : Rel Carrier _ - StrictPartialOrder._≮_ : Rel Carrier _ - ``` - Additionally, `Poset._≰_` is defined by renaming public export of `Preorder._⋦_` - - The corresponding former definitions in `Relation.Binary.Properties.*` - have been deprecated. - * Added new operations in `Relation.Binary.Construct.Closure.Equivalence`: ``` fold : IsEquivalence _∼_ → _⟶_ ⇒ _∼_ → EqClosure _⟶_ ⇒ _∼_ From 976a1d6747232b5640be0b9e19f3cb44f40404c3 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sat, 7 Oct 2023 06:08:07 +0100 Subject: [PATCH 31/33] removed one more extraneous `CHANGELOG` note: deprecation --- CHANGELOG.md | 5 ----- 1 file changed, 5 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9a9e3869d4..ac64159887 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1757,11 +1757,6 @@ Deprecated names fromForeign ↦ Foreign.Haskell.Coerce.coerce ``` -* In `Relation.Binary.Bundles.Preorder`: - ``` - _∼_ ↦ _≲_ - ``` - * In `Relation.Binary.Indexed.Heterogeneous.Bundles.Preorder`: ``` _∼_ ↦ _≲_ From 47bd7a8b1452211eec8533c71fdc52733fa94fe4 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Tue, 10 Oct 2023 09:03:15 +0900 Subject: [PATCH 32/33] Remove deprecations in Property files --- src/Relation/Binary/Bundles.agda | 36 ++++++++----------- src/Relation/Binary/Properties/Poset.agda | 25 +++---------- .../Binary/Properties/StrictTotalOrder.agda | 19 +--------- .../Binary/Properties/TotalOrder.agda | 23 ++---------- 4 files changed, 23 insertions(+), 80 deletions(-) diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index cba4edce7c..90e3c7e2ac 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -99,8 +99,13 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≳_ _≳_ = flip _≲_ - infix 4 _∼_ -- for deprecation + -- Deprecated. + infix 4 _∼_ _∼_ = _≲_ + {-# WARNING_ON_USAGE _∼_ + "Warning: _∼_ was deprecated in v2.0. + Please use _≲_ instead. " + #-} record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where @@ -118,7 +123,7 @@ record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where preorder = record { isPreorder = isPreorder } open Preorder preorder public - using (module Eq; _≳_) + using (module Eq; _≳_; _⋦_) ------------------------------------------------------------------------ @@ -142,7 +147,8 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where } open Preorder preorder public - using (module Eq) renaming (_⋦_ to _≰_) + using (module Eq) + renaming (_⋦_ to _≰_) record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where @@ -215,7 +221,8 @@ record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂ { isStrictPartialOrder = isStrictPartialOrder } - open StrictPartialOrder strictPartialOrder using (_≮_) + open StrictPartialOrder strictPartialOrder public + using (_≮_) module Eq where @@ -273,14 +280,16 @@ record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where { isTotalOrder = isTotalOrder } - open TotalOrder totalOrder public using (poset; preorder; _≰_) + open TotalOrder totalOrder public + using (poset; preorder; _≰_) decPoset : DecPoset c ℓ₁ ℓ₂ decPoset = record { isDecPartialOrder = isDecPartialOrder } - open DecPoset decPoset public using (module Eq) + open DecPoset decPoset public + using (module Eq) -- Note that these orders are decidable. The current implementation @@ -348,18 +357,3 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w isApartnessRelation : IsApartnessRelation _≈_ _#_ open IsApartnessRelation isApartnessRelation public - - - - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 2.0 - -{-# WARNING_ON_USAGE Preorder._∼_ -"Warning: Preorder._∼_ was deprecated in v2.0. Please use Preorder._≲_ instead. " -#-} diff --git a/src/Relation/Binary/Properties/Poset.agda b/src/Relation/Binary/Properties/Poset.agda index 96cc72398d..beb4ddc8aa 100644 --- a/src/Relation/Binary/Properties/Poset.agda +++ b/src/Relation/Binary/Properties/Poset.agda @@ -21,7 +21,7 @@ open import Relation.Nullary.Negation using (contradiction) module Relation.Binary.Properties.Poset {p₁ p₂ p₃} (P : Poset p₁ p₂ p₃) where -open Poset P renaming (Carrier to A; _≰_ to _≰A_) -- issue #1214 see below +open Poset P renaming (Carrier to A) import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict import Relation.Binary.Properties.Preorder preorder as PreorderProperties @@ -63,10 +63,10 @@ open Poset ≥-poset public ------------------------------------------------------------------------ -- Negated order -≰-respˡ-≈ : _≰A_ Respectsˡ _≈_ +≰-respˡ-≈ : _≰_ Respectsˡ _≈_ ≰-respˡ-≈ x≈y = _∘ ≤-respˡ-≈ (Eq.sym x≈y) -≰-respʳ-≈ : _≰A_ Respectsʳ _≈_ +≰-respʳ-≈ : _≰_ Respectsʳ _≈_ ≰-respʳ-≈ x≈y = _∘ ≤-respʳ-≈ (Eq.sym x≈y) ------------------------------------------------------------------------ @@ -99,7 +99,7 @@ open StrictPartialOrder <-strictPartialOrder public ≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y ≤∧≉⇒< = ToStrict.≤∧≉⇒< -<⇒≱ : ∀ {x y} → x < y → y ≰A x +<⇒≱ : ∀ {x y} → x < y → y ≰ x <⇒≱ = ToStrict.<⇒≱ antisym ≤⇒≯ : ∀ {x y} → x ≤ y → y ≮ x @@ -129,20 +129,3 @@ mono⇒cong = Consequences.mono⇒cong _≈_ _≈_ Eq.sym reflexive antisym antimono⇒cong : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → f Preserves _≈_ ⟶ _≈_ antimono⇒cong = Consequences.antimono⇒cong _≈_ _≈_ Eq.sym reflexive antisym - - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 2.0 - --- issue #1214: locally to this module, we rename the relation _≰_, --- so that we can deprecate it here, yet re-export it elsewhere -infix 4 _≰_ -_≰_ = _≰A_ -{-# WARNING_ON_USAGE _≤_ -"Warning: export of _≰_ from this module was deprecated in v2.0, in favour of a direct public export from Relation.Binary.Bundles.Poset instead" -#-} diff --git a/src/Relation/Binary/Properties/StrictTotalOrder.agda b/src/Relation/Binary/Properties/StrictTotalOrder.agda index 1f5b0fbc1a..e6d34ab8d1 100644 --- a/src/Relation/Binary/Properties/StrictTotalOrder.agda +++ b/src/Relation/Binary/Properties/StrictTotalOrder.agda @@ -12,9 +12,7 @@ module Relation.Binary.Properties.StrictTotalOrder {s₁ s₂ s₃} (STO : StrictTotalOrder s₁ s₂ s₃) where --- issue #1214: locally to this module, we hide the relation _≮_, so --- that we can deprecate its export here, yet re-export it elsewhere -open StrictTotalOrder STO hiding (_≮_) +open StrictTotalOrder STO open import Relation.Binary.Construct.StrictToNonStrict _≈_ _<_ import Relation.Binary.Properties.StrictPartialOrder as SPO open import Relation.Binary.Consequences @@ -28,18 +26,3 @@ decTotalOrder = record } open DecTotalOrder decTotalOrder public - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 2.0 - --- issue #1214: see above -infix 4 _≮_ -_≮_ = StrictTotalOrder._≮_ STO -{-# WARNING_ON_USAGE _≮_ -"Warning: export of _≮_ from this module was deprecated in v2.0, in favour of a direct public export from Relation.Binary.Bundles.StrictPartialOrder instead" -#-} diff --git a/src/Relation/Binary/Properties/TotalOrder.agda b/src/Relation/Binary/Properties/TotalOrder.agda index d8b7853d69..48f788ab7f 100644 --- a/src/Relation/Binary/Properties/TotalOrder.agda +++ b/src/Relation/Binary/Properties/TotalOrder.agda @@ -13,9 +13,7 @@ open import Relation.Binary.Structures using (IsTotalOrder) module Relation.Binary.Properties.TotalOrder {t₁ t₂ t₃} (T : TotalOrder t₁ t₂ t₃) where --- issue #1214: locally to this module, we rename the relation _≰_, so --- that we can deprecate it here, yet re-export it elsewhere -open TotalOrder T renaming (_≰_ to _≰A_) +open TotalOrder T open import Data.Product.Base using (proj₁) open import Data.Sum.Base using (inj₁; inj₂) @@ -96,23 +94,8 @@ open PosetProperties public ; ≰-respˡ-≈ ) -≰⇒> : ∀ {x y} → x ≰A y → y < x +≰⇒> : ∀ {x y} → x ≰ y → y < x ≰⇒> = ToStrict.≰⇒> Eq.sym reflexive total -≰⇒≥ : ∀ {x y} → x ≰A y → y ≤ x +≰⇒≥ : ∀ {x y} → x ≰ y → y ≤ x ≰⇒≥ x≰y = proj₁ (≰⇒> x≰y) - ------------------------------------------------------------------------- --- DEPRECATED ------------------------------------------------------------------------- --- Please use the new names as continuing support for the old names is --- not guaranteed. - --- Version 2.0 - --- issue #1214: see above -infix 4 _≰_ -_≰_ = _≰A_ -{-# WARNING_ON_USAGE _≰_ -"Warning: export of _≰_ from this module was deprecated in v2.0. Please import from Relation.Binary.Bundles.Poset instead" -#-} From 834ed4e8386d1953624ebc4aef397ad3d4b00af2 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Tue, 10 Oct 2023 09:07:26 +0900 Subject: [PATCH 33/33] Fix DecTotalOrder --- src/Relation/Binary/Properties/DecTotalOrder.agda | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/src/Relation/Binary/Properties/DecTotalOrder.agda b/src/Relation/Binary/Properties/DecTotalOrder.agda index ce00a08cad..d7b3c48cd9 100644 --- a/src/Relation/Binary/Properties/DecTotalOrder.agda +++ b/src/Relation/Binary/Properties/DecTotalOrder.agda @@ -14,9 +14,7 @@ open import Relation.Binary.Bundles module Relation.Binary.Properties.DecTotalOrder {d₁ d₂ d₃} (DTO : DecTotalOrder d₁ d₂ d₃) where --- issue #1214: locally to this module, we hide the relation _≰_, so --- that we can deprecate its export here, yet re-export it elsewhere -open DecTotalOrder DTO hiding (trans; _≰_) +open DecTotalOrder DTO hiding (trans) import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict @@ -97,10 +95,3 @@ open TotalOrderProperties public ≮⇒≥ : ∀ {x y} → x ≮ y → y ≤ x ≮⇒≥ = ToStrict.≮⇒≥ Eq.sym _≟_ reflexive total - --- issue #1214: see above -infix 4 _≰_ -_≰_ = DecTotalOrder._≰_ DTO -{-# WARNING_ON_USAGE _≰_ -"Warning: export of _≰_ from this module was deprecated in v2.0, in favour of a direct public export from Relation.Binary.Bundles.Poset instead" -#-}