[ refactor ] v2.4-admissible version of #2952

CHANGELOG.md

@@ -6,6 +6,19 @@ The library has been tested using Agda 2.8.0.
 Highlights
 ----------
 
+* The notation for `Decidable` relations has been (partially) standardised: thus
+  - `_≡?_` (at `infix 4`) for `DecidableEquality`
+  - `_≈?_` (ditto.) for the general `IsDecEquivalence`
+
+  At present, the old fieldname `_≟_` has been retained, in order to avoid
+  a non-backwards compatible/breaking change of fieldname, which will plan
+  to do in Version 3.0, with accompanying deprecation of that name, against
+  its eventual removal in subsequent versions.
+
+  The change leads to a number of (trivial) renamings/deprecations, others more
+  substantive in `Data.{Nat|Fin}.Properties` for the concrete datatypes, which
+  are summarised below, but are not each documented for all affected modules.
+
 Bug-fixes
 ---------
 
@@ -97,6 +110,15 @@ Deprecated names
   ```agda
   ¬∀⟶∃¬-smallest  ↦   ¬∀⇒∃¬-smallest
   ¬∀⟶∃¬-          ↦   ¬∀⇒∃¬
+  _≟_       ↦   _≡?_
+  inj⇒≟     ↦   inj⇒≡?
+  ```
+
+* In `Data.Nat.Properties`:
+  ```agda
+  _≟_     ↦   _≡?_
+  ≟-diag  ↦   ≡?-≡
+  ≟-≡     ↦   ≡?-≢
   ```
 
 * In `Data.Irrelevant`:
@@ -134,21 +156,42 @@ Deprecated names
   truncate-irrelevant  ↦  Relation.Binary.PropositionalEquality.Core.refl
   ```
 
+* In `Effect.Monad.Partiality`:
+  ```agda
+  _≟-Kind_     ↦   _≡?-Kind_
+  ```
+
 * In `Function.Base`:
   ```agda
   λ∙ : (.(x : A) → B x) → ((x : A) → B x)
   ```
 
+* In `Reflection.AST.AlphaEquality`:
+  ```agda
+  ≟⇒α     ↦   ≡?⇒α
+  ```
+
 * In `Relation.Binary.Construct.Intersection`:
   ```agda
   decidable     ↦   _∩?_
   ```
 
+* In `Relation.Binary.PropositionalEquality`:
+  ```agda
+  ≡-≟-identity     ↦   ≡-≡?-identity
+  ≢-≟-identity     ↦   ≢-≡?-identity
+  ```
+
 * In `Relation.Binary.Construct.Union`:
   ```agda
   decidable     ↦   _∪?_
   ```
 
+* In `Relation.Nary`:
+  ```agda
+  ≟-mapₙ     ↦   ≡?-mapₙ
+  ```
+
 * In `Relation.Nullary.Decidable.Core`:
   ```agda
   ⊤-dec     ↦   ⊤?
@@ -323,9 +366,9 @@ Additions to existing modules
 * In `Data.Fin.Properties`:
   ```agda
   ≡-irrelevant : Irrelevant {A = Fin n} _≡_
-  ≟-≡          : (eq : i ≡ j) → (i ≟ j) ≡ yes eq
-  ≟-≡-refl     : (i : Fin n) → (i ≟ i) ≡ yes refl
-  ≟-≢          : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
+  ≡?-≡         : (eq : i ≡ j) → (i ≡? j) ≡ yes eq
+  ≡?-≡-refl    : (i : Fin n) → (i ≡? i) ≡ yes refl
+  ≡?-≢         : (i≢j : i ≢ j) → (i ≡? j) ≡ no i≢j
   inject-<     : inject j < i
 
   record Least⟨_⟩ (P : Pred (Fin n) p) : Set p where
@@ -417,7 +460,7 @@ Additions to existing modules
 
 * In `Data.Nat.Properties`:
   ```agda
-  ≟-≢   : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
+  ≡?-≡-refl : ∀ n  → (n ≡? n) ≡ yes refl
   ∸-suc : .(m ≤ n) → suc n ∸ m ≡ suc (n ∸ m)
   ^-distribʳ-* : ∀ m n o → (n * o) ^ m ≡ n ^ m * o ^ m
   2*suc[n]≡2+n+n : ∀ n → 2 * (suc n) ≡ 2 + (n + n)

doc/README/Data/List/Membership.agda

@@ -34,7 +34,7 @@ import Data.List.Membership.DecPropositional as DecPropMembership
 -- propositional equality over `ℕ` and it is also decidable. Therefore
 -- the module `DecPropMembership` should be opened as follows:
 
-open DecPropMembership ℕ._≟_
+open DecPropMembership ℕ._≡?_
 
 -- As membership is just an instance of `Any` we also need to import
 -- the constructors `here` and `there`. (See issue #553 on Github for
@@ -66,7 +66,7 @@ import Data.List.Membership.Propositional.Properties as PropProperties
 -- following the first `∈` refers to lists of type `List ℕ` whereas
 -- the second `∈` refers to lists of type `List Char`.
 
-open DecPropMembership Char._≟_ renaming (_∈_ to _∈ᶜ_)
+open DecPropMembership Char._≡?_ renaming (_∈_ to _∈ᶜ_)
 open SetoidProperties using (∈-map⁺)
 
 lem₂ : {v : ℕ} {xs : List ℕ} → v ∈ xs → fromℕ v ∈ᶜ map fromℕ xs

doc/README/Data/List/Relation/Binary/Subset.agda

@@ -22,10 +22,10 @@ module README.Data.List.Relation.Binary.Subset where
 
 -- Decidable equality over Strings
 open import Data.String.Base using (String)
-open import Data.String.Properties using (_≟_)
+open import Data.String.Properties using (_≡?_)
 
 -- Open the decidable membership module using Decidable ≡ over Strings
-open import Data.List.Membership.DecPropositional _≟_
+open import Data.List.Membership.DecPropositional _≡?_
 
 
 -- Simple cases are inductive proofs

doc/README/Data/Record.agda

@@ -21,7 +21,7 @@ import Data.Record as Record
 
 -- Let us use strings as labels.
 
-open Record String _≟_
+open Record String _≡?_
 
 -- Partial equivalence relations.
 

doc/README/Data/Trie/NonDependent.agda

@@ -83,7 +83,7 @@ record Lexer t : Set (suc t) where
 
   -- Two keywords are considered distinct if the strings are not equal
   Distinct : Rel Keyword 0ℓ
-  Distinct a b = ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋
+  Distinct a b = ⌊ ¬? ((proj₁ a) String.≡? (proj₁ b)) ⌋
 
   field
 
@@ -175,7 +175,7 @@ module LetIn where
     LPAR RPAR : TOK
     ID : String → TOK
 
-  keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≟ (proj₁ b)) ⌋)
+  keywords : List# (String × TOK) (λ a b → ⌊ ¬? ((proj₁ a) String.≡? (proj₁ b)) ⌋)
   keywords =  ("let" , LET)
            ∷# ("="   , EQ)
            ∷# ("in"  , IN)

doc/README/Design/Decidability.agda

@@ -24,21 +24,21 @@ open import Relation.Nary
 
 open import Relation.Nullary.Reflects
 
-infix 4 _≟₀_ _≟₁_ _≟₂_
+infix 4 _≡?₀_ _≡?₁_ _≡?₂_
 
 -- A proof of `Reflects P b` shows that a proposition `P` has the truth value of
 -- the boolean `b`. A proof of `Reflects P true` amounts to a proof of `P`, and
 -- a proof of `Reflects P false` amounts to a refutation of `P`.
 
 ex₀ : (n : ℕ) → Reflects (n ≡ n) true
-ex₀ n = ofʸ refl
+ex₀ n = of refl
 
 ex₁ : (n : ℕ) → Reflects (zero ≡ suc n) false
-ex₁ n = ofⁿ λ ()
+ex₁ n = of λ()
 
 ex₂ : (b : Bool) → Reflects (T b) b
-ex₂ false = ofⁿ id
-ex₂ true  = ofʸ tt
+ex₂ false = of id
+ex₂ true  = of tt
 
 ------------------------------------------------------------------------
 -- Dec
@@ -64,71 +64,71 @@ ex₄ n = no λ ()
 -- only the `yes` and `no` patterns. The following procedure decides whether two
 -- given natural numbers are equal.
 
-_≟₀_ : (m n : ℕ) → Dec (m ≡ n)
-zero  ≟₀ zero  = yes refl
-zero  ≟₀ suc n = no λ ()
-suc m ≟₀ zero  = no λ ()
-suc m ≟₀ suc n with m ≟₀ n
+_≡?₀_ : (m n : ℕ) → Dec (m ≡ n)
+zero  ≡?₀ zero  = yes refl
+zero  ≡?₀ suc n = no λ()
+suc m ≡?₀ zero  = no λ()
+suc m ≡?₀ suc n with m ≡?₀ n
 ... | yes p = yes (cong suc p)
 ... | no ¬p = no (¬p ∘ suc-injective)
 
--- In this case, we can see that `does (suc m ≟ suc n)` should be equal to
--- `does (m ≟ n)`, because a `yes` from `m ≟ n` gives rise to a `yes` from the
+-- In this case, we can see that `does (suc m ≡? suc n)` should be equal to
+-- `does (m ≡? n)`, because a `yes` from `m ≡? n` gives rise to a `yes` from the
 -- result, and similarly for `no`. However, in the above definition, this
 -- equality does not hold definitionally, because we always do a case split
 -- before returning a result. To avoid this, we can return the `does` part
 -- separately, before any pattern matching.
 
-_≟₁_ : (m n : ℕ) → Dec (m ≡ n)
-zero  ≟₁ zero  = yes refl
-zero  ≟₁ suc n = no λ ()
-suc m ≟₁ zero  = no λ ()
-does  (suc m ≟₁ suc n) = does (m ≟₁ n)
-proof (suc m ≟₁ suc n) with m ≟₁ n
-... | yes p = ofʸ (cong suc p)
-... | no ¬p = ofⁿ (¬p ∘ suc-injective)
+_≡?₁_ : (m n : ℕ) → Dec (m ≡ n)
+zero  ≡?₁ zero  = yes refl
+zero  ≡?₁ suc n = no λ()
+suc m ≡?₁ zero  = no λ()
+does  (suc m ≡?₁ suc n) = does (m ≡?₁ n)
+proof (suc m ≡?₁ suc n) with m ≡?₁ n
+... | yes p = of (cong suc p)
+... | no ¬p = of (¬p ∘ suc-injective)
 
 -- We now get definitional equalities such as the following.
 
-_ : (m n : ℕ) → does (5 + m ≟₁ 3 + n) ≡ does (2 + m ≟₁ n)
+_ : (m n : ℕ) → does (5 + m ≡?₁ 3 + n) ≡ does (2 + m ≡?₁ n)
 _ = λ m n → refl
 
 -- Even better, from a maintainability point of view, is to use `map` or `map′`,
 -- both of which capture the pattern of the `does` field remaining the same, but
 -- the `proof` field being updated.
 
-_≟₂_ : (m n : ℕ) → Dec (m ≡ n)
-zero  ≟₂ zero  = yes refl
-zero  ≟₂ suc n = no λ ()
-suc m ≟₂ zero  = no λ ()
-suc m ≟₂ suc n = map′ (cong suc) suc-injective (m ≟₂ n)
+_≡?₂_ : (m n : ℕ) → Dec (m ≡ n)
+zero  ≡?₂ zero  = yes refl
+zero  ≡?₂ suc n = no λ()
+suc m ≡?₂ zero  = no λ()
+suc m ≡?₂ suc n = map′ (cong suc) suc-injective (m ≡?₂ n)
 
-_ : (m n : ℕ) → does (5 + m ≟₂ 3 + n) ≡ does (2 + m ≟₂ n)
+_ : (m n : ℕ) → does (5 + m ≡?₂ 3 + n) ≡ does (2 + m ≡?₂ n)
 _ = λ m n → refl
 
 -- `map′` can be used in conjunction with combinators such as `_⊎?_` and
 -- `_×?_` to build complex (simply typed) decision procedures.
 
-module ListDecEq₀ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) where
+module ListDecEq₀ {a} {A : Set a} (_≡?ᴬ_ : (x y : A) → Dec (x ≡ y)) where
 
-  _≟ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys)
-  []       ≟ᴸᴬ []       = yes refl
-  []       ≟ᴸᴬ (y ∷ ys) = no λ ()
-  (x ∷ xs) ≟ᴸᴬ []       = no λ ()
-  (x ∷ xs) ≟ᴸᴬ (y ∷ ys) =
-    map′ (uncurry (cong₂ _∷_)) ∷-injective (x ≟ᴬ y ×? xs ≟ᴸᴬ ys)
+  _≡?ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys)
+  []       ≡?ᴸᴬ []       = yes refl
+  []       ≡?ᴸᴬ (y ∷ ys) = no λ()
+  (x ∷ xs) ≡?ᴸᴬ []       = no λ()
+  (x ∷ xs) ≡?ᴸᴬ (y ∷ ys) =
+    map′ (uncurry (cong₂ _∷_)) ∷-injective (x ≡?ᴬ y ×? xs ≡?ᴸᴬ ys)
 
 -- The final case says that `x ∷ xs ≡ y ∷ ys` exactly when `x ≡ y` *and*
 -- `xs ≡ ys`. The proofs are updated by the first two arguments to `map′`.
 
 -- In the case of ≡-equality tests, the pattern
--- `map′ (congₙ c) c-injective (x₀ ≟ y₀ ×? ... ×? xₙ₋₁ ≟ yₙ₋₁)`
--- is captured by `≟-mapₙ n c c-injective (x₀ ≟ y₀) ... (xₙ₋₁ ≟ yₙ₋₁)`.
+-- `map′ (congₙ c) c-injective (x₀ ≡? y₀ ×? ... ×? xₙ₋₁ ≡? yₙ₋₁)`
+-- is captured by `≡?-mapₙ n c c-injective (x₀ ≡? y₀) ... (xₙ₋₁ ≡? yₙ₋₁)`.
 
-module ListDecEq₁ {a} {A : Set a} (_≟ᴬ_ : (x y : A) → Dec (x ≡ y)) where
+module ListDecEq₁ {a} {A : Set a} (_≡?ᴬ_ : (x y : A) → Dec (x ≡ y)) where
 
-  _≟ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys)
-  []       ≟ᴸᴬ []       = yes refl
-  []       ≟ᴸᴬ (y ∷ ys) = no λ ()
-  (x ∷ xs) ≟ᴸᴬ []       = no λ ()
-  (x ∷ xs) ≟ᴸᴬ (y ∷ ys) = ≟-mapₙ 2 _∷_ ∷-injective (x ≟ᴬ y) (xs ≟ᴸᴬ ys)
+  _≡?ᴸᴬ_ : (xs ys : List A) → Dec (xs ≡ ys)
+  []       ≡?ᴸᴬ []       = yes refl
+  []       ≡?ᴸᴬ (y ∷ ys) = no λ()
+  (x ∷ xs) ≡?ᴸᴬ []       = no λ()
+  (x ∷ xs) ≡?ᴸᴬ (y ∷ ys) = ≡?-mapₙ 2 _∷_ ∷-injective (x ≡?ᴬ y) (xs ≡?ᴸᴬ ys)

doc/README/Foreign/Haskell.agda

@@ -92,12 +92,12 @@ main = run $ do
   content ← readFiniteFile "README/Foreign/Haskell.agda"
   let chars = toList content
   let cleanup = catMaybes ∘ List.map (λ c → if testChar c then just c else nothing)
-  let cleaned = dropWhile ('\n' ≟_) $ cleanup chars
+  let cleaned = dropWhile ('\n' ≡?_) $ cleanup chars
   case uncons cleaned of λ where
     nothing         → putStrLn "I cannot believe this file is filed with dashes only!"
     (just (c , cs)) → putStrLn $ unlines
                     $ ("First (non dash) character: " ++ Char.show c)
-                    ∷ ("Rest (dash free) of the line: " ++ fromList (takeWhile (¬? ∘ ('\n' ≟_)) cs))
+                    ∷ ("Rest (dash free) of the line: " ++ fromList (takeWhile (¬? ∘ ('\n' ≡?_)) cs))
                     ∷ []
 
 -- You can compile and run this test by writing:

doc/README/Function/Reasoning.agda

@@ -57,7 +57,7 @@ subpalindromes str = let Chars = List Char in
   |> filter (λ cs → 2 ≤? length cs)        ∶ List Chars
   -- only keep the ones that are palindromes
   |> map < fromList , fromList ∘ reverse > ∶ List (String × String)
-  |> filter (uncurry String._≟_)           ∶ List (String × String)
+  |> filter (uncurry String._≡?_)           ∶ List (String × String)
   |> map proj₁                             ∶ List String
 
 -- Test cases

doc/README/Nary.agda

@@ -338,14 +338,14 @@ exist₁ = 19 , 793 , 3059 , 10 , refl
 -- ∀[_] P = ∀ {a₁} → ⋯ → ∀ {aₙ} → P a₁ ⋯ aₙ
 
 all₁ : ∀[ (λ (a₁ a₂ : ℕ) → Dec (a₁ ≡ a₂)) ]
-all₁ {a₁} {a₂} = a₁ ≟ a₂
+all₁ {a₁} {a₂} = a₁ ≡? a₂
 
 ------------------------------------------------------------------------
 -- Π : (A₁ → ⋯ → Aₙ → Set r) → Set _
 -- Π P = ∀ a₁ → ⋯ → ∀ aₙ → P a₁ ⋯ aₙ
 
 all₂ : Π[ (λ (a₁ a₂ : ℕ) → Dec (a₁ ≡ a₂)) ]
-all₂ = _≟_
+all₂ = _≡?_
 
 ------------------------------------------------------------------------
 -- _⇒_ : (A₁ → ⋯ → Aₙ → Set r) → (A₁ → ⋯ → Aₙ → Set s) → (A₁ → ⋯ → Aₙ → Set _)

doc/style-guide.md

@@ -586,6 +586,12 @@ word within a compound word is capitalized except for the first word.
   converse relations are systematically introduced, eg `≥` as `\ge`
   and `≱` as `\gen`.
 
+* Decidable predicates and relations should typically be written as `R?`,
+  where `R` is the underlying property being asserted to be `Decidable`,
+  moreover typically sharing the same fixity and precedence as `R`: thus
+  - `_≡?_` (at `infix 4`) for `DecidableEquality`
+  - `_≈?_` (ditto.) for the name of the general `IsDecEquivalence`
+
 * Any exceptions to these conventions should be flagged on the GitHub
   `agda-stdlib` issue tracker in the usual way.
 

src/Algebra/Construct/LexProduct.agda

@@ -21,7 +21,7 @@ import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 module Algebra.Construct.LexProduct
   {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (M : Magma ℓ₁ ℓ₂) (N : Magma ℓ₃ ℓ₄)
-  (_≟₁_ : Decidable (Magma._≈_ M))
+  (_≈₁?_ : Decidable (Magma._≈_ M))
   where
 
 open Magma M using (_∙_ ; ∙-cong)
@@ -39,7 +39,7 @@ open Magma N using ()
   ; refl    to ≈₂-refl
   )
 
-import Algebra.Construct.LexProduct.Inner M N _≟₁_ as InnerLex
+import Algebra.Construct.LexProduct.Inner M N _≈₁?_ as InnerLex
 
 private
   infix 4 _≋_
@@ -53,7 +53,7 @@ private
 -- Definition
 ------------------------------------------------------------------------
 
-open import Algebra.Construct.LexProduct.Base _∙_ _◦_ _≟₁_ public
+open import Algebra.Construct.LexProduct.Base _∙_ _◦_ _≈₁?_ public
   renaming (lex to _⊕_)
 
 ------------------------------------------------------------------------
@@ -103,7 +103,7 @@ identityʳ : ∀ {e f} → RightIdentity _≈₁_ e _∙_ → RightIdentity _≈
 identityʳ id₁ id₂ (x , a) = id₁ x , InnerLex.identityʳ id₁ id₂
 
 sel : Selective _≈₁_ _∙_ → Selective _≈₂_ _◦_ → Selective _≋_ _⊕_
-sel ∙-sel ◦-sel (a , x) (b , y) with (a ∙ b) ≟₁ a | (a ∙ b) ≟₁ b
+sel ∙-sel ◦-sel (a , x) (b , y) with (a ∙ b) ≈₁? a | (a ∙ b) ≈₁? b
 ... | no  ab≉a | no  ab≉b  = contradiction₂ (∙-sel a b) ab≉a ab≉b
 ... | yes ab≈a | no  _     = inj₁ (ab≈a , ≈₂-refl)
 ... | no  _    | yes ab≈b  = inj₂ (ab≈b , ≈₂-refl)