diff options
author | Jason Gross <jagro@google.com> | 2016-06-22 12:26:27 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-06-22 13:17:11 -0700 |
commit | 40df85e20678cbed1870ae86054c90bf4cb72879 (patch) | |
tree | 40679883c2f6f550371ccc804e2e05d0541a5da6 /src | |
parent | fd026fcca741364051c4d7a3469896ee04ad67ea (diff) |
Add decidability util file
This will be useful for the Weierstrass curves, which require
case-splitting on field equality.
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/Decidable.v | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v new file mode 100644 index 000000000..f8cf03d6e --- /dev/null +++ b/src/Util/Decidable.v @@ -0,0 +1,61 @@ +(** Typeclass for decidable propositions *) + +Require Import Coq.Logic.Eqdep_dec. + +Local Open Scope type_scope. + +Class Decidable (P : Prop) := dec : {P} + {~P}. + +Notation DecidableRel R := (forall x y, Decidable (R x y)). + +Ltac destruct_decidable_step := + match goal with + | [ H : Decidable _ |- _ ] => destruct H + end. +Ltac destruct_decidable := repeat destruct_decidable_step. + +Local Ltac pre_decide := + repeat (intros + || destruct_decidable + || subst + || split + || unfold Decidable in * + || hnf ). + +Local Ltac solve_decidable_transparent_with tac := + pre_decide; + try solve [ left; abstract tac + | right; abstract tac + | decide equality; eauto with nocore ]. + +Local Ltac solve_decidable_transparent := solve_decidable_transparent_with firstorder. + +Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances. + +Global Instance dec_True : Decidable True := left I. +Global Instance dec_False : Decidable False := right (fun x => x). +Global Instance dec_or {A B} `{Decidable A, Decidable B} : Decidable (A \/ B) := _. +Global Instance dec_and {A B} `{Decidable A, Decidable B} : Decidable (A /\ B) := _. +Global Instance dec_impl {A B} `{Decidable (B \/ ~A)} : Decidable (A -> B) | 3 := _. +Global Instance dec_impl_simple {A B} `{Decidable A, Decidable B} : Decidable (A -> B) := _. +Global Instance dec_iff {A B} `{Decidable A, Decidable B} : Decidable (A <-> B) := _. +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) := _. +Global Instance dec_eq_bool : DecidableRel (@eq bool) := _. +Global Instance dec_eq_Empty_set : DecidableRel (@eq Empty_set) := _. +Global Instance dec_eq_nat : DecidableRel (@eq nat) := _. +Global Instance dec_eq_prod {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A * B)) := _. +Global Instance dec_eq_sum {A B} `{DecidableRel (@eq A), DecidableRel (@eq B)} : DecidableRel (@eq (A + B)) := _. + +Lemma Decidable_respects_iff A B (H : A <-> B) : (Decidable A -> Decidable B) * (Decidable B -> Decidable A). +Proof. solve_decidable_transparent. Defined. + +Lemma Decidable_iff_to_impl A B (H : A <-> B) : Decidable A -> Decidable B. +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. |