[fixes #1214] Add negated ordering relation symbols systematically to Relation.Binary.*

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,6 +762,41 @@ 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 `_≮_` (`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`.
+  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`.
+
+* 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.
+
+* 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 (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`...
 
 ### Other
 
@@ -928,6 +963,7 @@ Non-backwards compatible changes
     lookup : All P xs → (∀ {x} → x ∈ₚ xs → P x)
     lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x)
     ```
+
   * `excluded-middle` in `Relation.Nullary.Decidable.Core` has been renamed to
     `¬¬-excluded-middle`.
 
@@ -1498,6 +1534,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
@@ -2253,7 +2299,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)
@@ -2804,6 +2850,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 _⟶_ ⇒ _∼_

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<s; s<s)
+open import Data.Nat.Base using (_<_; _>_; z<s; s<s)
 open import Data.Nat.Induction
 open import Data.Nat.Properties using (m<n⇒m<1+n)
 open import Data.Product.Base as Prod using (_,_)
@@ -36,7 +36,7 @@ open DecTotalOrder O renaming (Carrier to A)
 
 open import Data.List.Sort.Base totalOrder
 open import Data.List.Relation.Unary.Sorted.TotalOrder totalOrder hiding (head)
-open import Relation.Binary.Properties.DecTotalOrder O using (_≰_; ≰⇒≥; ≰-respˡ-≈)
+open import Relation.Binary.Properties.DecTotalOrder O using (≰⇒≥; ≰-respˡ-≈)
 
 open PermutationReasoning
 

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 _≈_ _≲_
@@ -107,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 _⋦_)
 
 
 ------------------------------------------------------------------------
@@ -131,7 +134,7 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     }
 
   open Preorder preorder public
-    using (module Eq)
+    using (module Eq) renaming (_≁_ to _≰_)
 
 
 record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -152,7 +155,7 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     }
 
   open Poset poset public
-    using (preorder)
+    using (preorder; _≰_)
 
   module Eq where
     decSetoid : DecSetoid c ℓ₁
@@ -182,6 +185,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 _≈_ _<_
@@ -200,6 +207,8 @@ record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂
     { isStrictPartialOrder = isStrictPartialOrder
     }
 
+  open StrictPartialOrder strictPartialOrder using (_≮_)
+
   module Eq where
 
     decSetoid : DecSetoid c ℓ₁
@@ -231,7 +240,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
@@ -256,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
@@ -288,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

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
@@ -80,19 +82,25 @@ open TotalOrderProperties public
   }
 
 open StrictTotalOrder <-strictTotalOrder public
-  using () renaming (compare to <-compare)
+  using (_≮_) renaming (compare to <-compare)
 
 ------------------------------------------------------------------------
 -- _≰_ - the negated order
 
 open TotalOrderProperties public
   using
-  ( _≰_
-  ; ≰-respʳ-≈
+  ( ≰-respʳ-≈
   ; ≰-respˡ-≈
   ; ≰⇒>
   ; ≰⇒≥
   )
 
-≮⇒≥ : ∀ {x y} → ¬ (x < y) → y ≤ x
+≮⇒≥ : ∀ {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"
+#-}

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)
@@ -20,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)
+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
@@ -62,15 +63,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)
 
 ------------------------------------------------------------------------
@@ -90,7 +86,7 @@ _<_ = ToStrict._<_
   }
 
 open StrictPartialOrder <-strictPartialOrder public
-  using ( <-resp-≈; <-respʳ-≈; <-respˡ-≈)
+  using (_≮_; <-resp-≈; <-respʳ-≈; <-respˡ-≈)
   renaming
   ( irrefl to <-irrefl
   ; asym   to <-asym
@@ -103,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
 
 ------------------------------------------------------------------------
@@ -133,3 +129,20 @@ 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"
+#-}

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