From b81aa3aaa4a4b1cf31a6f03eeb7809012b516240 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 May 2019 09:56:24 +0200
Subject: [PATCH] `RelDecision` instance for `flip`, and make `flip` tc opaque
 to avoid loops due to eager unification.

---
 theories/base.v      | 7 ++++++-
 theories/decidable.v | 6 +++++-
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 86d98c17..4f9c20a6 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -505,7 +505,12 @@ Arguments id _ _ / : assert.
 Arguments compose _ _ _ _ _ _ / : assert.
 Arguments flip _ _ _ _ _ _ / : assert.
 Arguments const _ _ _ _ / : assert.
-Typeclasses Transparent id compose flip const.
+Typeclasses Transparent id compose const.
+
+(** Make sure that [flip] is type class opaque, otherwise one gets loops due to
+instance involving [flip], e.g. [RelDecision R → RelDecision (flip R)] could be
+used indefinitely. *)
+Typeclasses Opaque flip.
 
 Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' :=
   g ∘ h ∘ f.
diff --git a/theories/decidable.v b/theories/decidable.v
index c78d72a6..062dd1dc 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,7 @@ 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] *)
+Instance flip_dec {A} (R : relation A) `{!RelDecision R} :
+  RelDecision (flip R) := λ x y, decide_rel R y x.
-- 
GitLab