From eaf7fba1612c8ba2987b40bafc6b4e20a5f0be0b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 10 Apr 2017 18:34:36 -0400 Subject: Add dec_of_bool_dec --- src/Util/Decidable.v | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'src/Util/Decidable.v') 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. -- cgit v1.2.3