blob: 7ca7b1f3ed48692d9388adefa0ea9b1290b03e8d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
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.
|
