From 27aa3a1e358ca9281721e3a3f4137979d16aab7e Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Mon, 27 Jun 2016 11:44:39 -0700
Subject: Add decidable instances for sumwise and fieldwise

---
 src/Util/Tuple.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'src/Util/Tuple.v')

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.
-- 
cgit v1.2.3