[ new ] generic "diag" for decidable equality (#266)

CHANGELOG.md

@@ -249,6 +249,12 @@ Backwards compatible changes
   trans∧tri⟶respˡ≈ : Transitive _<_ → Trichotomous _≈_ _<_ → _<_ Respectsˡ _≈_
   ```
 
+* Added new proof to `Relation.Binary.PropositionalEquality`:
+  ```agda
+  ≡-≟-identity : (eq : a ≡ b) → a ≟ b ≡ yes eq
+  ≢-≟-identity : a ≢ b → ∃ λ ¬eq → a ≟ b ≡ no ¬eq
+  ```
+
 * The types `Maximum` and `Minimum` are now exported by `Relation.Binary` as well
   as `Relation.Binary.Lattice`.
 

src/Relation/Binary/PropositionalEquality.agda

@@ -9,6 +9,9 @@ module Relation.Binary.PropositionalEquality where
 open import Function
 open import Function.Equality using (Π; _⟶_; ≡-setoid)
 open import Level
+open import Data.Empty
+open import Data.Product
+open import Relation.Nullary using (yes ; no)
 open import Relation.Unary using (Pred)
 open import Relation.Binary
 import Relation.Binary.Indexed as I
@@ -191,6 +194,18 @@ IrrelevantRel _~_ = ∀ {x y} → isPropositional (x ~ y)
 ≡-irrelevance : ∀ {a} {A : Set a} → IrrelevantRel (_≡_ {A = A})
 ≡-irrelevance refl refl = refl
 
+module _ {a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A})) {a b : A} where
+
+  ≡-≟-identity : (eq : a ≡ b) → a ≟ b ≡ yes eq
+  ≡-≟-identity eq with a ≟ b
+  ... | yes p = cong yes (≡-irrelevance p eq)
+  ... | no ¬p = ⊥-elim (¬p eq)
+
+  ≢-≟-identity : a ≢ b → ∃ λ ¬eq → a ≟ b ≡ no ¬eq
+  ≢-≟-identity ¬eq with a ≟ b
+  ... | yes p = ⊥-elim (¬eq p)
+  ... | no ¬p = ¬p , refl
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------