diff options
Diffstat (limited to 'src/Util/Decidable.v')
| -rw-r--r-- | src/Util/Decidable.v | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index e7e8ce471..2703ef108 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -11,7 +11,6 @@ Local Open Scope type_scope. Class Decidable (P : Prop) := dec : {P} + {~P}. Arguments dec _%type_scope {_}. - Notation DecidableRel R := (forall x y, Decidable (R x y)). Global Instance hprop_eq_dec {A} `{DecidableRel (@eq A)} : IsHPropRel (@eq A) | 10. @@ -85,7 +84,6 @@ Lemma dec_not {A} `{Decidable A} : Decidable (~A). Proof. solve_decidable_transparent. Defined. (** Disallow infinite loops of dec_not *) Hint Extern 0 (Decidable (~?A)) => apply (@dec_not A) : typeclass_instances. - Global Instance dec_eq_unit : DecidableRel (@eq unit) | 10. exact _. Defined. Global Instance dec_eq_bool : DecidableRel (@eq bool) | 10. exact _. Defined. Global Instance dec_eq_Empty_set : DecidableRel (@eq Empty_set) | 10. exact _. Defined. @@ -110,8 +108,6 @@ Global Instance dec_le_Z : DecidableRel BinInt.Z.le := ZArith_dec.Z_le_dec. 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_eq_positive : DecidableRel (@eq BinNums.positive) | 10 := BinPos.Pos.eq_dec. - Global Instance dec_match_pair {A B} {P : A -> B -> Prop} {x : A * B} {HD : Decidable (P (fst x) (snd x))} : Decidable (let '(a, b) := x in P a b) | 1. @@ -139,6 +135,16 @@ 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. +Global Instance dec_eq_positive : DecidableRel (@eq BinNums.positive) | 10 := BinPos.Pos.eq_dec. +Global Instance dec_lt_positive : DecidableRel BinPos.Pos.lt. +Proof. eauto using Decidable_iff_to_impl, Pos.ltb_lt with typeclass_instances. Defined. +Global Instance dec_le_positive : DecidableRel BinPos.Pos.le. +Proof. eauto using Decidable_iff_to_impl, Pos.leb_le with typeclass_instances. Defined. +Global Instance dec_gt_positive : DecidableRel BinPos.Pos.gt. +Proof. eauto using Decidable_iff_to_flip_impl, Pos.gt_lt_iff with typeclass_instances. Defined. +Global Instance dec_ge_positive : DecidableRel BinPos.Pos.ge. +Proof. eauto using Decidable_iff_to_flip_impl, Pos.ge_le_iff with typeclass_instances. 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. @@ -169,4 +175,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. +Qed.
\ No newline at end of file |