From fe4b156f34c8a0ac994ff4cdb40755d23bc5e7b9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 5 Sep 2016 11:42:26 -0700 Subject: Add a lemma about semidecidable things to Decidable --- src/Util/Decidable.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'src/Util/Decidable.v') diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index 7b412caf0..cb47a3625 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -100,7 +100,7 @@ Global Instance dec_eq_Z : DecidableRel (@eq Z) | 10 := Z.eq_dec. Lemma not_not P {d:Decidable P} : not (not P) <-> P. Proof. destruct (dec P); intuition. Qed. - + Global Instance dec_ex_forall_not T (P:T->Prop) {d:Decidable (exists b, P b)} : Decidable (forall b, ~ P b). Proof. destruct (dec (~ exists b, P b)) as [Hd|Hd]; [left|right]; @@ -120,6 +120,13 @@ Proof. solve_decidable_transparent. Defined. Lemma Decidable_iff_to_flip_impl A B (H : A <-> B) : Decidable B -> Decidable A. Proof. solve_decidable_transparent. Defined. +Lemma dec_of_semidec {P : Prop} (H : option P) (H_complete : H = None -> ~P) : Decidable P. +Proof. destruct H; [ left; assumption | right; apply H_complete, eq_refl ]. Defined. + +Lemma dec_rel_of_semidec_rel {A} {R : A -> A -> Prop} (H : forall x y, option (R x y)) + (H_complete : forall x y, H x y = None -> ~R x y) : DecidableRel R. +Proof. eauto using dec_of_semidec. 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. -- cgit v1.2.3