From 5ba352a350874dd3bdea8b4c8d632bb6442336eb Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 10 May 2019 09:18:00 +0200
Subject: [PATCH] Another attempt at a `RelDecision` instance for `flip`.

Now we follow Coq's stdlib and declare this instance using a `Hint Extern`;
this avoids making `flip` type class opaque.
---
 theories/decidable.v | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/theories/decidable.v b/theories/decidable.v
index c78d72a6..799ab1ba 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -135,7 +135,7 @@ Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
   dexist (`x) p = x.
 Proof. apply dsig_eq; reflexivity. Qed.
 
-(** * Instances of Decision *)
+(** * Instances of [Decision] *)
 (** Instances of [Decision] for operators of propositional logic. *)
 Instance True_dec: Decision True := left I.
 Instance False_dec: Decision False := right (False_rect False).
@@ -192,3 +192,11 @@ Proof. destruct (decide Q); tauto. Qed.
 Program Definition inj_eq_dec `{EqDecision A} {B} (f : B → A)
   `{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
 Solve Obligations with firstorder congruence.
+
+(** * Instances of [RelDecision] *)
+Definition flip_dec {A} (R : relation A) `{!RelDecision R} :
+  RelDecision (flip R) := λ x y, decide_rel R y x.
+(** We do not declare this as an actual instance since Coq can unify [flip ?R]
+with any relation. Coq's standard library is carrying out the same approach for
+the [Reflexive], [Transitive], etc, instance of [flip]. *)
+Hint Extern 3 (RelDecision (flip _)) => apply flip_dec : typeclass_instances.
-- 
GitLab