diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-08-13 16:46:28 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-08-13 16:46:38 -0400 |
| commit | 5da42750e1349ce761107902ef3039195adac62c (patch) | |
| tree | 3bcf37d626161e07fc8a6e5a37ca3f421e23dccf /src/Util/Decidable.v | |
| parent | 01373db10fe1fdc698731c2aad35952f9cf31292 (diff) | |
Add decidable equality with nil
Diffstat (limited to 'src/Util/Decidable.v')
| -rw-r--r-- | src/Util/Decidable.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index 014af738f..b68d799b3 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -90,6 +90,10 @@ Global Instance dec_eq_Empty_set : DecidableRel (@eq Empty_set) | 10. exact _. D Global Instance dec_eq_prod {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A * B)) | 10. exact _. Defined. Global Instance dec_eq_option {A} `{DecidableRel (@eq A)} : DecidableRel (@eq (option A)) | 10. exact _. Defined. Global Instance dec_eq_list {A} `{DecidableRel (@eq A)} : DecidableRel (@eq (list A)) | 10. exact _. Defined. +Global Instance dec_eq_list_nil_r {A} {ls} : Decidable (ls = @nil A) | 10. +Proof. destruct ls; [ left; reflexivity | right; abstract congruence ]. Defined. +Global Instance dec_eq_list_nil_l {A} {ls} : Decidable (@nil A = ls) | 10. +Proof. destruct ls; [ left; reflexivity | right; abstract congruence ]. Defined. Global Instance dec_eq_sum {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A + B)) | 10. exact _. Defined. Global Instance dec_eq_sigT_hprop {A P} `{DecidableRel (@eq A), forall a : A, IsHProp (P a)} : DecidableRel (@eq (@sigT A P)) | 10. exact _. Defined. Global Instance dec_eq_sig_hprop {A} {P : A -> Prop} `{DecidableRel (@eq A), forall a : A, IsHProp (P a)} : DecidableRel (@eq (@sig A P)) | 10. exact _. Defined. |