[ new ] add _<_ for chars and deprecate non-propositional equality (#1343)

Author: gallais

CHANGELOG.md

@@ -37,6 +37,12 @@ Non-backwards compatible changes
 * The module `Algebra.Construct.Zero` and `Algebra.Module.Construct.Zero`
   are now level-polymorphic, each taking two implicit level parameters.
 
+* The orders on strings are now using propositional equality as the notion
+  of equivalence on characters rather than the equivalent but less inference-friendly
+  variant defined by conversion of characters to natural numbers.
+  This is in line with our effort to deprecate this badly-behaved equivalence
+  relation on characters.
+
 * Previously `_⊖_` in `Data.Integer.Base` was defined inductively as:
   ```agda
   _⊖_ : ℕ → ℕ → ℤ
@@ -112,6 +118,10 @@ Deprecated names
   Plus′ ↦ TransClosure
   ```
 
+* In `Data.Char.Properties`, deprecated all of the `_≈_`-related content: this
+  relation is equivalent to propositional equality but has worse inference. So
+  we are moving towards not using it anymore.
+
 * In `Data.List.Relation.Binary.Subset.Propositional.Properties`:
   ```agda
   mono            ↦ Any-resp-⊆
@@ -371,6 +381,33 @@ Other minor additions
   +-*-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
   ```
 
+* Added new definition to `Data.Char.Base`:
+  ```agda
+  _≉_ : Rel Char zero
+  _≤_ : Rel Char zero
+  ```
+
+* Added proofs to `Data.Char.Properties`:
+  ```agda
+  ≉⇒≢ : _≉_ → x ≢ y
+
+  <-trans : Transitive _<_
+  <-asym  : Asymmetric _<_
+  <-cmp   : Trichotomous _≡_ _<_
+
+  _≤?_                : Decidable _≤_
+  ≤-reflexive         : _≡_ ⇒ _≤_
+  ≤-trans             : Transitive _≤_
+  ≤-antisym           : Antisymmetric _≡_ _≤_
+  ≤-isPreorder        : IsPreorder _≡_ _≤_
+  ≤-isPartialOrder    : IsPartialOrder _≡_ _≤_
+  ≤-isDecPartialOrder : IsDecPartialOrder _≡_ _≤_
+
+  ≤-preorder : Preorder _ _ _
+  ≤-poset    : Poset _ _ _
+  ≤-decPoset : DecPoset _ _ _
+  ```
+
 * Added infix declarations to `Data.Product.∃-syntax` and `Data.Product.∄-syntax`.
 
 * Added new function to `Data.List.Base`:

README/Data/Trie/NonDependent.agda

@@ -65,7 +65,7 @@ open import Relation.Nary
 open import Relation.Binary using (Rel)
 open import Relation.Nullary.Negation using (¬?)
 
-open import Data.Trie Char.<-strictTotalOrder-≈
+open import Data.Trie Char.<-strictTotalOrder
 open import Data.Tree.AVL.Value
 
 ------------------------------------------------------------------------

src/Data/Char.agda

@@ -12,4 +12,5 @@ module Data.Char where
 -- Re-export base definitions and decidability of equality
 
 open import Data.Char.Base public
-open import Data.Char.Properties using (_≈?_; _≟_; _<?_; _==_) public
+open import Data.Char.Properties
+  using (_≈?_; _≟_; _<?_; _≤?_; _==_) public

src/Data/Char/Base.agda

@@ -13,6 +13,7 @@ import Data.Nat.Base as ℕ
 open import Function
 open import Relation.Binary using (Rel)
 open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Construct.Closure.Reflexive
 
 ------------------------------------------------------------------------
 -- Re-export the type, and renamed primitives
@@ -39,14 +40,21 @@ open import Agda.Builtin.Char public using ( Char )
 open import Agda.Builtin.String public using ()
   renaming ( primShowChar to show )
 
-infix 4 _≈_
+infix 4 _≈_ _≉_
 _≈_ : Rel Char zero
 _≈_ = _≡_ on toℕ
 
+_≉_ : Rel Char zero
+_≉_ = _≢_ on toℕ
+
 infix 4 _<_
 _<_ : Rel Char zero
 _<_ = ℕ._<_ on toℕ
 
+infix 4 _≤_
+_≤_ : Rel Char zero
+_≤_ = ReflClosure _<_
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

src/Data/Char/Instances.agda

@@ -9,8 +9,6 @@
 module Data.Char.Instances where
 
 open import Data.Char.Properties
-open import Relation.Binary.PropositionalEquality.Properties
-  using (isDecEquivalence)
 
 instance
-  Char-≡-isDecEquivalence = isDecEquivalence _≟_
+  Char-≡-isDecEquivalence = isDecEquivalence