Add dec_of_bool_dec

1 files changed, 10 insertions, 1 deletions

diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
index 2703ef108..cc144f062 100644
--- a/src/Util/Decidable.v
+++ b/src/Util/Decidable.v
@@ -152,6 +152,15 @@ Lemma dec_rel_of_semidec_rel {A} {R : A -> A -> Prop} (H : forall x y, option (R
       (H_complete : forall x y, H x y = None -> ~R x y) : DecidableRel R.
 Proof. eauto using dec_of_semidec. Defined.
 
+Lemma dec_of_bool_dec {P : Prop} (b : bool) (Hbl : b = true -> P) (Hlb : P -> b = true)
+  : Decidable P.
+Proof. destruct b; [ left; apply Hbl; reflexivity | right; intro p; apply Bool.diff_false_true, Hlb, p ]. Defined.
+
+Lemma dec_rel_of_bool_dec_rel {A} {R : A -> A -> Prop} (b : A -> A -> bool)
+      (Hbl : forall x y, b x y = true -> R x y) (Hlb : forall x y, R x y -> b x y = true)
+  : DecidableRel R.
+Proof. eauto using dec_of_bool_dec. Defined.
+
 Lemma dec_bool : forall {P} {Pdec:Decidable P}, (if dec P then true else false) = true -> P.
 Proof. intros. destruct dec; solve [ auto | discriminate ]. Qed.
 
@@ -175,4 +184,4 @@ Lemma cast_if_eq_refl {T H P} t v : @cast_if_eq T H P t t v = Some v.
 Proof.
   compute; clear; destruct (H t t) as [ [] |e];
     [ reflexivity | destruct (e eq_refl) ].
-Qed.
\ No newline at end of file
+Qed.