diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-10 04:37:44 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-10 04:37:44 -0500 |
| commit | 4758761b669078acb85e9071c05f546e5b2f0f13 (patch) | |
| tree | d266bd0ef0a6d7006420e4084808574aaaef9784 /src/Util/Decidable.v | |
| parent | dbb2aa3df305ef0061ff2efeeb12c51cc1a2ca91 (diff) | |
Fix opacity of dec_Forall, dec_Exists
Diffstat (limited to 'src/Util/Decidable.v')
| -rw-r--r-- | src/Util/Decidable.v | 18 |
1 files changed, 14 insertions, 4 deletions
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))} |