From 5914224fe2ea9a329286fb6f0f6216a93dc59f36 Mon Sep 17 00:00:00 2001
From: "G. Allais" <guillaume.allais@ens-lyon.org>
Date: Fri, 13 Apr 2018 11:51:25 +0200
Subject: [PATCH] [ new ] generic "diag" for decidable equality (#266)

---
 CHANGELOG.md                                   |  6 ++++++
 src/Relation/Binary/PropositionalEquality.agda | 15 +++++++++++++++
 2 files changed, 21 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e0870e2d0d..912e93c8d2 100644
--- a/CHANGELOG.md
+++ b/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`.
 
diff --git a/src/Relation/Binary/PropositionalEquality.agda b/src/Relation/Binary/PropositionalEquality.agda
index 0f422e0bad..c909f8b4cf 100644
--- a/src/Relation/Binary/PropositionalEquality.agda
+++ b/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
 ------------------------------------------------------------------------