From 4758761b669078acb85e9071c05f546e5b2f0f13 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 10 Nov 2017 04:37:44 -0500 Subject: Fix opacity of dec_Forall, dec_Exists --- src/Util/Decidable.v | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) (limited to 'src/Util/Decidable.v') diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index 482f2c50a..72d94753e 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -115,11 +115,21 @@ Global Instance dec_gt_Z : DecidableRel BinInt.Z.gt := ZArith_dec.Z_gt_dec. Global Instance dec_ge_Z : DecidableRel BinInt.Z.ge := ZArith_dec.Z_ge_dec. Global Instance dec_Forall {A P} {HD : forall x : A, Decidable (P x)} {ls} - : Decidable (Forall P ls) - := @Forall_dec A P HD ls. + : Decidable (Forall P ls) | 10. +Proof. + induction ls as [|x xs IHxs]; [ left | destruct (HD x), IHxs; [ left | right.. ] ]; + [ constructor; assumption | constructor; assumption | intro Hn.. ]; + clear HD; + try abstract (inversion Hn; subst; tauto). +Defined. Global Instance dec_Exists {A P} {HD : forall x : A, Decidable (P x)} {ls} - : Decidable (Exists P ls) - := @Exists_dec A P ls HD. + : Decidable (Exists P ls) | 10. +Proof. + induction ls as [|x xs IHxs]; [ right | destruct (HD x), IHxs; [ left.. | right ] ]; + [ intro Hn | constructor; assumption.. | intro Hn ]; + clear HD; + try abstract (inversion Hn; subst; tauto). +Defined. Global Instance dec_match_pair {A B} {P : A -> B -> Prop} {x : A * B} {HD : Decidable (P (fst x) (snd x))} -- cgit v1.2.3