`RelDecision` instance for `flip`, and make `flip` tc opaque to avoid loops...

`RelDecision` instance for `flip`, and make `flip` tc opaque to avoid loops due to eager unification.

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.

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.