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

CHANGELOG.md

@@ -621,7 +621,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
@@ -842,7 +842,6 @@ 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
@@ -856,9 +855,25 @@ 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.
+### (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`,
+ 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`
 
@@ -879,12 +894,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
@@ -895,12 +910,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
@@ -1658,7 +1673,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
@@ -1684,7 +1699,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
@@ -1742,11 +1757,6 @@ Deprecated names
  fromForeign ↦ Foreign.Haskell.Coerce.coerce
  ```
 
-* In `Relation.Binary.Bundles.Preorder`:
- ```
- _∼_ ↦ _≲_
- ```
-
 * In `Relation.Binary.Indexed.Heterogeneous.Bundles.Preorder`:
  ```
  _∼_ ↦ _≲_
@@ -1758,6 +1768,15 @@ 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._≮_
+
 * In `Relation.Nullary.Decidable.Core`:
  ```
  excluded-middle ↦ ¬¬-excluded-middle
@@ -3300,9 +3319,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₂ ≈₁ ⟶ ≈₁ ⟶ ≈₂

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

@@ -92,11 +92,20 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 
  open Setoid setoid public
 
+ infix 4 _⋦_
+ _⋦_ : Rel Carrier _
+ x ⋦ y = ¬ (x ≲ y)
+
  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
@@ -114,7 +123,7 @@ record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  preorder = record { isPreorder = isPreorder }
 
  open Preorder preorder public
- using (module Eq; _≳_)
+ using (module Eq; _≳_; _⋦_)
 
 
 ------------------------------------------------------------------------
@@ -139,6 +148,7 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 
  open Preorder preorder public
  using (module Eq)
+ renaming (_⋦_ to _≰_)
 
 
 record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -159,7 +169,7 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  }
 
  open Poset poset public
- using (preorder)
+ using (preorder; _≰_)
 
  module Eq where
  decSetoid : DecSetoid c ℓ₁
@@ -189,6 +199,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 _≈_ _<_
@@ -207,6 +221,9 @@ record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂
  { isStrictPartialOrder = isStrictPartialOrder
  }
 
+ open StrictPartialOrder strictPartialOrder public
+ using (_≮_)
+
  module Eq where
 
  decSetoid : DecSetoid c ℓ₁
@@ -238,7 +255,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
@@ -263,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
@@ -295,7 +314,7 @@ record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) wh
  }
 
  open StrictPartialOrder strictPartialOrder public
- using (module Eq)
+ using (module Eq; _≮_)
 
  decSetoid : DecSetoid c ℓ₁
  decSetoid = record
@@ -338,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. "
-#-}

src/Relation/Binary/Properties/DecTotalOrder.agda

@@ -12,9 +12,9 @@ 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)
+open DecTotalOrder DTO hiding (trans)
 
 import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
 import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
@@ -80,19 +80,18 @@ 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

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)
@@ -62,11 +63,6 @@ open Poset ≥-poset public
 ------------------------------------------------------------------------
 -- Negated order
 
-infix 4 _≰_
-
-_≰_ : Rel A p₃
-x ≰ y = ¬ (x ≤ y)
-
 ≰-respˡ-≈ : _≰_ 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 ≰ x
 <⇒≱ = ToStrict.<⇒≱ antisym
 
-≤⇒≯ : ∀ {x y} → x ≤ y → ¬ (y < x)
+≤⇒≯ : ∀ {x y} → x ≤ y → y ≮ x
 ≤⇒≯ = ToStrict.≤⇒≯ antisym
 
 ------------------------------------------------------------------------

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

src/Relation/Binary/Properties/StrictTotalOrder.agda

@@ -18,7 +18,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

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
@@ -90,8 +90,7 @@ open PosetProperties public
 
 open PosetProperties public
  using
- ( _≰_
- ; ≰-respʳ-≈
+ ( ≰-respʳ-≈
  ; ≰-respˡ-≈
  )