Add decidable instances for sumwise and fieldwise

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.