diff options
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Decidable.v | 6 | ||||
-rw-r--r-- | src/Util/Sum.v | 7 | ||||
-rw-r--r-- | src/Util/Tuple.v | 15 |
3 files changed, 25 insertions, 3 deletions
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index 9ab05699a..c2094c765 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -14,7 +14,7 @@ Ltac destruct_decidable_step := end. Ltac destruct_decidable := repeat destruct_decidable_step. -Local Ltac pre_decide := +Ltac pre_decide := repeat (intros || destruct_decidable || subst @@ -22,13 +22,13 @@ Local Ltac pre_decide := || unfold Decidable in * || hnf ). -Local Ltac solve_decidable_transparent_with tac := +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. +Ltac solve_decidable_transparent := solve_decidable_transparent_with firstorder. Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances. diff --git a/src/Util/Sum.v b/src/Util/Sum.v index 915f58df9..1ee8ea69a 100644 --- a/src/Util/Sum.v +++ b/src/Util/Sum.v @@ -1,5 +1,6 @@ Require Import Coq.Classes.Morphisms. Require Import Relation_Definitions. +Require Import Crypto.Util.Decidable. Definition sumwise {A B} (RA:relation A) (RB : relation B) : relation (A + B) := fun x y => match x, y with @@ -25,3 +26,9 @@ Ltac congruence_sum_step := | [ H : inr _ = inr _ |- _ ] => inversion H; clear H end. Ltac congruence_sum := repeat congruence_sum_step. + +Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances. +Global Instance dec_sumwise {A B RA RB} {HA : DecidableRel RA} {HB : DecidableRel RB} : DecidableRel (@sumwise A B RA RB) | 10. +Proof. + intros [x|x] [y|y]; exact _. +Qed. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 6802a86c3..d08c52c82 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -1,5 +1,6 @@ Require Import Coq.Classes.Morphisms. Require Import Relation_Definitions. +Require Import Crypto.Util.Decidable. Fixpoint tuple' T n : Type := match n with @@ -79,3 +80,17 @@ Qed. Arguments fieldwise' {A B n} _ _ _. Arguments fieldwise {A B n} _ _ _. + +Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances. +Global Instance dec_fieldwise' {A RA} {HA : DecidableRel RA} {n} : DecidableRel (@fieldwise' A A n RA) | 10. +Proof. + induction n; simpl @fieldwise'. + { exact _. } + { intros ??. + exact _. } +Qed. + +Global Instance dec_fieldwise {A RA} {HA : DecidableRel RA} {n} : DecidableRel (@fieldwise A A n RA) | 10. +Proof. + destruct n; unfold fieldwise; exact _. +Qed. |