[ refactor ] introduce revised notation for decidability of Lexicographic orderings, plus knock-ons

CHANGELOG.md

@@ -99,6 +99,28 @@ Deprecated names
   witness   ↦   satisfiable
   ```
 
+* In `Data.List.Relation.Binary.Lex.NonStrict`:
+  ```agda
+  <-decidable    ↦   _<?_
+  ≤-decidable    ↦   _≤?_
+  ```
+
+* In `Data.List.Relation.Binary.Lex.Strict`:
+  ```agda
+  <-decidable    ↦   _<?_
+  ≤-decidable    ↦   _≤?_
+  ```
+
+* In `Data.Product.Relation.Binary.Lex.NonStrict`:
+  ```agda
+  ×-decidable    ↦   ≤ₗₑₓ?
+  ```
+
+* In `Data.Product.Relation.Binary.Lex.Strict`:
+  ```agda
+  ×-decidable    ↦   <ₗₑₓ?
+ ```
+
 * In `Data.Rational.Properties`:
   ```agda
   nonPos*nonPos⇒nonPos  ↦  nonPos*nonPos⇒nonNeg
@@ -109,6 +131,18 @@ Deprecated names
   truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
   ```
 
+* In `Data.Vec.Relation.Binary.Lex.NonStrict`:
+  ```agda
+  <-decidable    ↦   _<?_
+  ≤-decidable    ↦   _≤?_
+  ```
+
+* In `Data.Vec.Relation.Binary.Lex.Strict`:
+  ```agda
+  <-decidable    ↦   _<?_
+  ≤-decidable    ↦   _≤?_
+  ```
+
 * In `Relation.Binary.Construct.Intersection`:
   ```agda
   decidable     ↦   _∩?_

src/Data/List/Relation/Binary/Lex.agda

@@ -16,7 +16,7 @@ open import Data.List.Relation.Binary.Pointwise.Base
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Function.Base using (_∘_; flip; id)
 open import Function.Bundles using (_⇔_; mk⇔)
-open import Level using (_⊔_)
+open import Level using (Level; _⊔_)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Relation.Nullary.Decidable as Dec
   using (Dec; yes; no; _×?_; _⊎?_)
@@ -26,6 +26,14 @@ open import Relation.Binary.Definitions
   using (Symmetric; Transitive; Irreflexive; Asymmetric; Antisymmetric
         ; Decidable; _Respects₂_; _Respects_)
 
+private
+  variable
+    a ℓ₁ ℓ₂ : Level
+    A : Set a
+    x y : A
+    xs ys : List A
+
+
 
 ------------------------------------------------------------------------
 -- Re-exporting the core definitions and properties
@@ -35,20 +43,17 @@ open import Data.List.Relation.Binary.Lex.Core public
 ------------------------------------------------------------------------
 -- Properties
 
-module _ {a ℓ₁ ℓ₂} {A : Set a} {P : Set}
-         {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
+module _ {A : Set a} {P : Set} {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
 
   private
     _≋_ = Pointwise _≈_
     _<_ = Lex P _≈_ _≺_
 
-  ¬≤-this : ∀ {x y xs ys} → ¬ (x ≈ y) → ¬ (x ≺ y) →
-            ¬ (x ∷ xs) < (y ∷ ys)
+  ¬≤-this : ¬ (x ≈ y) → ¬ (x ≺ y) → ¬ (x ∷ xs) < (y ∷ ys)
   ¬≤-this x≉y x≮y (this x≺y)       = x≮y x≺y
   ¬≤-this x≉y x≮y (next x≈y xs<ys) = x≉y x≈y
 
-  ¬≤-next : ∀ {x y xs ys} → ¬ x ≺ y → ¬ xs < ys →
-            ¬ (x ∷ xs) < (y ∷ ys)
+  ¬≤-next : ¬ x ≺ y → ¬ xs < ys → ¬ (x ∷ xs) < (y ∷ ys)
   ¬≤-next x≮y xs≮ys (this x≺y)     = x≮y x≺y
   ¬≤-next x≮y xs≮ys (next _ xs<ys) = xs≮ys xs<ys
 
@@ -63,7 +68,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} {P : Set}
     as (next x≈y xs<ys) (this y≺x)       = contradiction y≺x (ir (sym x≈y))
     as (next x≈y xs<ys) (next y≈x ys<xs) = x≈y ∷ as xs<ys ys<xs
 
-  toSum : ∀ {x y xs ys} → (x ∷ xs) < (y ∷ ys) → (x ≺ y ⊎ (x ≈ y × xs < ys))
+  toSum : (x ∷ xs) < (y ∷ ys) → x ≺ y ⊎ (x ≈ y × xs < ys)
   toSum (this x≺y) = inj₁ x≺y
   toSum (next x≈y xs<ys) = inj₂ (x≈y , xs<ys)
 
@@ -87,25 +92,25 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} {P : Set}
   respects₂ eq (resp₁ , resp₂) = resp¹ , resp²
     where
     open IsEquivalence eq using (sym; trans)
-    resp¹ : ∀ {xs} → Lex P _≈_ _≺_ xs Respects _≋_
+    resp¹ : Lex P _≈_ _≺_ xs Respects _≋_
     resp¹ []            xs<[]            = xs<[]
     resp¹ (_   ∷ _)     halt             = halt
     resp¹ (x≈y ∷ _)     (this z≺x)       = this (resp₁ x≈y z≺x)
     resp¹ (x≈y ∷ xs≋ys) (next z≈x zs<xs) =
       next (trans z≈x x≈y) (resp¹ xs≋ys zs<xs)
 
-    resp² : ∀ {ys} → flip (Lex P _≈_ _≺_) ys Respects _≋_
+    resp² : flip (Lex P _≈_ _≺_) ys Respects _≋_
     resp² []            []<ys            = []<ys
     resp² (x≈z ∷ _)     (this x≺y)       = this (resp₂ x≈z x≺y)
     resp² (x≈z ∷ xs≋zs) (next x≈y xs<ys) =
       next (trans (sym x≈z) x≈y) (resp² xs≋zs xs<ys)
 
 
   []<[]-⇔ : P ⇔ [] < []
-  []<[]-⇔ = mk⇔ base (λ { (base p) → p })
+  []<[]-⇔ = mk⇔ base λ { (base p) → p }
 
 
-  ∷<∷-⇔ : ∀ {x y xs ys} → (x ≺ y ⊎ (x ≈ y × xs < ys)) ⇔ (x ∷ xs) < (y ∷ ys)
+  ∷<∷-⇔ : (x ≺ y ⊎ (x ≈ y × xs < ys)) ⇔ (x ∷ xs) < (y ∷ ys)
   ∷<∷-⇔ = mk⇔ [ this , uncurry next ] toSum
 
   module _ (dec-P : Dec P) (dec-≈ : Decidable _≈_) (dec-≺ : Decidable _≺_)

src/Data/List/Relation/Binary/Lex/NonStrict.agda

@@ -19,7 +19,7 @@ open import Function.Base using (const; id)
 import Data.List.Relation.Binary.Lex.Strict as Strict
 open import Level using (Level; _⊔_)
 open import Relation.Nullary.Negation.Core using (¬_)
-open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Decidable.Core using (yes; no)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles
 open import Relation.Binary.Structures
@@ -86,8 +86,8 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     <-compare sym _≟_ antisym tot =
       Strict.<-compare sym (Conv.<-trichotomous _ _ sym _≟_ antisym tot)
 
-    <-decidable : Decidable _≈_ → Decidable _≼_ → Decidable _<_
-    <-decidable _≟_ _≼?_ =
+    _<?_ : Decidable _≈_ → Decidable _≼_ → Decidable _<_
+    _<?_ _≟_ _≼?_ =
       Core.decidable (no id) _≟_ (Conv.<-decidable _ _ _≟_ _≼?_)
 
     <-isStrictPartialOrder : IsPartialOrder _≈_ _≼_ →
@@ -149,9 +149,9 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     ≤-resp₂ : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ → _≤_ Respects₂ _≋_
     ≤-resp₂ eq resp = Core.respects₂ eq (Conv.<-resp-≈ _ _ eq resp)
 
-    ≤-decidable : Decidable _≈_ → Decidable _≼_ → Decidable _≤_
-    ≤-decidable _≟_ _≼?_ =
-      Core.decidable (yes tt) _≟_ (Conv.<-decidable _ _ _≟_ _≼?_)
+    _≤?_ : Decidable _≈_ → Decidable _≼_ → Decidable _≤_
+    _≤?_ _≟_ _≼?_ =
+      Core.decidable (yes _) _≟_ (Conv.<-decidable _ _ _≟_ _≼?_)
 
     ≤-total : Symmetric _≈_ → Decidable _≈_ → Antisymmetric _≈_ _≼_ →
               Total _≼_ → Total _≤_
@@ -197,3 +197,24 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
 ≤-decTotalOrder dtot = record
   { isDecTotalOrder = ≤-isDecTotalOrder isDecTotalOrder
   } where open DecTotalOrder dtot
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+<-decidable = _<?_
+{-# WARNING_ON_USAGE <-decidable
+"Warning: <-decidable was deprecated in v2.4.
+Please use _<?_ instead."
+#-}
+
+≤-decidable = _≤?_
+{-# WARNING_ON_USAGE ≤-decidable
+"Warning: ≤-decidable was deprecated in v2.4.
+Please use _≤?_ instead."
+#-}

src/Data/List/Relation/Binary/Lex/Strict.agda

@@ -100,8 +100,8 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     ...   | tri> xs≮ys xs≉ys ys<xs =
             tri> (¬≤-next x≮y xs≮ys) (xs≉ys ∘ tail) (next (sym x≈y) ys<xs)
 
-    <-decidable : Decidable _≈_ → Decidable _≺_ → Decidable _<_
-    <-decidable = Core.decidable (no id)
+    _<?_ : Decidable _≈_ → Decidable _≺_ → Decidable _<_
+    _<?_ = Core.decidable (no id)
 
     <-respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                   _<_ Respects₂ _≋_
@@ -176,8 +176,8 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     ...   | inj₁ xs≲ys = inj₁ (next      x≈y  xs≲ys)
     ...   | inj₂ ys≲xs = inj₂ (next (sym x≈y) ys≲xs)
 
-    ≤-decidable : Decidable _≈_ → Decidable _≺_ → Decidable _≤_
-    ≤-decidable = Core.decidable (yes _)
+    _≤?_ : Decidable _≈_ → Decidable _≺_ → Decidable _≤_
+    _≤?_ = Core.decidable (yes _)
 
     ≤-respects₂ : IsEquivalence _≈_ → _≺_ Respects₂ _≈_ →
                   _≤_ Respects₂ _≋_
@@ -202,10 +202,10 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
     ≤-isDecPartialOrder : IsStrictTotalOrder _≈_ _≺_ →
                           IsDecPartialOrder _≋_ _≤_
     ≤-isDecPartialOrder sto = record
-      { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
-      ; _≟_            = Pointwise.decidable _≟_
-      ; _≤?_           = ≤-decidable _≟_ _<?_
-      } where open IsStrictTotalOrder sto
+      { isPartialOrder = ≤-isPartialOrder O.isStrictPartialOrder
+      ; _≟_            = Pointwise.decidable O._≟_
+      ; _≤?_           = O._≟_ ≤?  O._<?_
+      } where module O = IsStrictTotalOrder sto
 
     ≤-isTotalOrder : IsStrictTotalOrder _≈_ _≺_ → IsTotalOrder _≋_ _≤_
     ≤-isTotalOrder sto = record
@@ -218,10 +218,10 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
                         IsDecTotalOrder _≋_ _≤_
     ≤-isDecTotalOrder sto = record
       { isTotalOrder = ≤-isTotalOrder sto
-      ; _≟_          = Pointwise.decidable _≟_
-      ; _≤?_         = ≤-decidable _≟_ _<?_
+      ; _≟_          = Pointwise.decidable O._≟_
+      ; _≤?_         = O._≟_ ≤?  O._<?_
       }
-      where open IsStrictTotalOrder sto
+      where module O = IsStrictTotalOrder sto
 
 ≤-preorder : ∀ {a ℓ₁ ℓ₂} → Preorder a ℓ₁ ℓ₂ → Preorder _ _ _
 ≤-preorder pre = record
@@ -245,3 +245,24 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
 ≤-decTotalOrder sto = record
   { isDecTotalOrder = ≤-isDecTotalOrder isStrictTotalOrder
   } where open StrictTotalOrder sto
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+<-decidable = _<?_
+{-# WARNING_ON_USAGE <-decidable
+"Warning: <-decidable was deprecated in v2.4.
+Please use _<?_ instead."
+#-}
+
+≤-decidable = _≤?_
+{-# WARNING_ON_USAGE ≤-decidable
+"Warning: ≤-decidable was deprecated in v2.4.
+Please use _≤?_ instead."
+#-}

src/Data/Product/Relation/Binary/Lex/NonStrict.agda

@@ -82,11 +82,10 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂} {_≤₂_ : Rel B 
     ...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁ , x₂≤y₂))
     ...   | inj₂ x₂≥y₂ = inj₂ (inj₂ (sym₁ x₁≈y₁ , x₂≥y₂))
 
-  ×-decidable : Decidable _≈₁_ → Decidable _≤₁_ → Decidable _≤₂_ →
+  ≤ₗₑₓ? : Decidable _≈₁_ → Decidable _≤₁_ → Decidable _≤₂_ →
                 Decidable _≤ₗₑₓ_
-  ×-decidable dec-≈₁ dec-≤₁ dec-≤₂ =
-    Strict.×-decidable dec-≈₁ (Conv.<-decidable _ _ dec-≈₁ dec-≤₁)
-                       dec-≤₂
+  ≤ₗₑₓ? ≈?₁ ≤?₁ ≤?₂ =
+    Strict.<ₗₑₓ? ≈?₁ (Conv.<-decidable _ _ ≈?₁ ≤?₁) ≤?₂
 
 module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
          {_≈₂_ : Rel B ℓ₃} {_≤₂_ : Rel B ℓ₄}
@@ -158,7 +157,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
                                     (isTotalOrder to₁)
                                     (isTotalOrder to₂)
     ; _≟_          = Pointwise.×-decidable (_≟_ to₁) (_≟_ to₂)
-    ; _≤?_         = ×-decidable (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
+    ; _≤?_         = ≤ₗₑₓ? (_≟_ to₁) (_≤?_ to₁) (_≤?_ to₂)
     }
     where open IsDecTotalOrder
 
@@ -183,3 +182,18 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
 ×-decTotalOrder t₁ t₂ = record
   { isDecTotalOrder = ×-isDecTotalOrder O₁.isDecTotalOrder O₂.isDecTotalOrder
   } where module O₁ = DecTotalOrder t₁; module O₂ = DecTotalOrder t₂
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+×-decidable = ≤ₗₑₓ?
+{-# WARNING_ON_USAGE ×-decidable
+"Warning: ×-decidable was deprecated in v2.4.
+Please use ≤ₗₑₓ? instead."
+#-}

src/Data/Product/Relation/Binary/Lex/Strict.agda

@@ -107,9 +107,9 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} {_<₂_ : Rel B ℓ
   ...   | inj₁ x₂≤y₂ = inj₁ (inj₂ (x₁≈y₁     , x₂≤y₂))
   ...   | inj₂ y₂≤x₂ = inj₂ (inj₂ (sym x₁≈y₁ , y₂≤x₂))
 
-  ×-decidable : Decidable _≈₁_ → Decidable _<₁_ → Decidable _<₂_ →
+  <ₗₑₓ? : Decidable _≈₁_ → Decidable _<₁_ → Decidable _<₂_ →
                 Decidable _<ₗₑₓ_
-  ×-decidable _≈₁?_ _<₁?_ _<₂?_ x y =
+  <ₗₑₓ? _≈₁?_ _<₁?_ _<₂?_ x y =
     proj₁ x <₁? proj₁ y
       ⊎?
     (proj₁ x ≈₁? proj₁ y
@@ -304,3 +304,18 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂}
   { isStrictTotalOrder = ×-isStrictTotalOrder
       (isStrictTotalOrder s₁) (isStrictTotalOrder s₂)
   } where open StrictTotalOrder
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+×-decidable = <ₗₑₓ?
+{-# WARNING_ON_USAGE ×-decidable
+"Warning: ×-decidable was deprecated in v2.4.
+Please use <ₗₑₓ? instead."
+#-}

src/Data/String/Properties.agda

@@ -105,7 +105,7 @@ x ≟ y = map′ ≈⇒≡ ≈-reflexive $ x ≈? y
 
 infix 4 _<?_
 _<?_ : Decidable _<_
-x <? y = StrictLex.<-decidable Char._≟_ Char._<?_ (toList x) (toList y)
+x <? y = StrictLex._<?_ Char._≟_ Char._<?_ (toList x) (toList y)
 
 <-isStrictPartialOrder-≈ : IsStrictPartialOrder _≈_ _<_
 <-isStrictPartialOrder-≈ =

src/Data/Vec/Relation/Binary/Lex/NonStrict.agda

@@ -103,8 +103,8 @@ module _ {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂} where
   <-cmp ≈-sym _≟_ ≼-antisym ≼-total = Strict.<-cmp ≈-sym
     (Conv.<-trichotomous _ _ ≈-sym _≟_ ≼-antisym ≼-total)
 
-  <-dec : Decidable _≈_ → Decidable _≼_ → ∀ {m n} → Decidable (_<_ {m} {n})
-  <-dec _≟_ _≼?_ = Core.decidable (no id) _≟_
+  _<?_ : Decidable _≈_ → Decidable _≼_ → ∀ {m n} → Decidable (_<_ {m} {n})
+  _<?_ _≟_ _≼?_ = Core.decidable (no id) _≟_
     (Conv.<-decidable _ _ _≟_ _≼?_)
 
 ------------------------------------------------------------------------
@@ -189,9 +189,9 @@ module _ {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂} where
   ≤-total ≈-sym _≟_ ≼-antisym ≼-total = Strict.≤-total ≈-sym
     (Conv.<-trichotomous _ _ ≈-sym _≟_ ≼-antisym ≼-total)
 
-  ≤-dec : Decidable _≈_ → Decidable _≼_ →
+  _≤?_ : Decidable _≈_ → Decidable _≼_ →
           ∀ {m n} → Decidable (_≤_ {m} {n})
-  ≤-dec _≟_ _≼?_ = Core.decidable (yes tt) _≟_
+  _≤?_ _≟_ _≼?_ = Core.decidable (yes tt) _≟_
     (Conv.<-decidable _ _ _≟_ _≼?_)
 
   ≤-resp₂ : IsEquivalence _≈_ → _≼_ Respects₂ _≈_ →
@@ -272,3 +272,24 @@ module ≤-Reasoning  {_≈_ : Rel A ℓ₁} {_≼_ : Rel A ℓ₂}
     (<-transˡ ≼-po)
     (<-transʳ ≼-po)
     public
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.4
+
+<-dec = _<?_
+{-# WARNING_ON_USAGE <-dec
+"Warning: <-dec was deprecated in v2.4.
+Please use _<?_ instead."
+#-}
+
+≤-dec = _≤?_
+{-# WARNING_ON_USAGE ≤-dec
+"Warning: ≤-dec was deprecated in v2.4.
+Please use _≤?_ instead."
+#-}