From 34a28d5226491db66984d9f234204ca3d87e5ff7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 9 Oct 2017 02:07:30 -0400 Subject: Add UniformWeightInstances --- src/Arithmetic/Saturated/UniformWeightInstances.v | 34 +++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 src/Arithmetic/Saturated/UniformWeightInstances.v (limited to 'src/Arithmetic') 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. -- cgit v1.2.3