Add UniformWeightInstances

1 files changed, 34 insertions, 0 deletions

diff --git a/src/Arithmetic/Saturated/UniformWeightInstances.v b/src/Arithmetic/Saturated/UniformWeightInstances.v
new file mode 100644
index 000000000..7ca7b1f3e
--- /dev/null
+++ b/src/Arithmetic/Saturated/UniformWeightInstances.v
@@ -0,0 +1,34 @@
+Require Import Coq.ZArith.BinInt.
+Require Import Crypto.Arithmetic.Saturated.UniformWeight.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Tactics.DestructHead.
+
+Fixpoint small_Decidable' {bound n} : forall (p : Tuple.tuple' Z n), Decidable (small (n:=S n) bound p).
+Proof.
+  refine match n as n return forall p : Tuple.tuple' Z n, id (Decidable (small (n:=S n) bound p)) with
+         | 0
+           => fun p : Z
+              => if dec (0 <= p < bound)%Z then left _ else right _
+         | S n'
+           => fun p : Tuple.tuple' Z n' * Z
+              => if dec (0 <= snd p < bound)%Z
+                 then if dec (small (n:=S n') bound (fst p))%Z
+                      then left _
+                      else right _
+                 else right _
+         end;
+    unfold id, small in *; simpl in *;
+      [ clear small_Decidable' n
+      | clear small_Decidable' n
+      | clear small_Decidable'; simpl in *.. ];
+      [ abstract (simpl in *; intros; destruct_head'_or; subst; auto; exfalso; assumption)
+      | abstract (simpl in *; intros; destruct_head'_or; subst; auto; exfalso; assumption)
+      | abstract (destruct p; simpl in *; intros; destruct_head'_or; subst; auto).. ].
+Defined.
+
+Global Instance small_Decidable {bound n} : forall (p : Tuple.tuple Z n), Decidable (small bound p).
+Proof.
+  destruct n; simpl; [ left | apply small_Decidable' ].
+  intros ??; exfalso; assumption.
+Defined.