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

Author: jamesmckinna

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
@@ -1659,7 +1674,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
@@ -1685,7 +1700,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
@@ -1743,11 +1758,6 @@ Deprecated names
   fromForeign ↦ Foreign.Haskell.Coerce.coerce
   ```
 
-* In `Relation.Binary.Bundles.Preorder`:
-  ```
-  _∼_  ↦  _≲_
-  ```
-
 * In `Relation.Binary.Indexed.Heterogeneous.Bundles.Preorder`:
   ```
   _∼_  ↦  _≲_
@@ -1759,6 +1769,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
@@ -3301,9 +3320,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ˡ-≈
   )