Add type of bounded Z

1 files changed, 124 insertions, 0 deletions

diff --git a/src/Util/ZBounded.v b/src/Util/ZBounded.v
new file mode 100644
index 000000000..365076189
--- /dev/null
+++ b/src/Util/ZBounded.v
@@ -0,0 +1,124 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.Bool.IsTrue.
+Require Import Crypto.Util.Bool.
+Require Import Crypto.Util.HProp.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Notations.
+
+Delimit Scope zbounded_scope with zbounded.
+Local Open Scope Z_scope.
+Local Set Primitive Projections.
+Record zbounded {r : zrange}
+  := { value :> Z ;
+       value_bounded : is_true ((lower r <=? value) && (value <=? upper r)) }.
+Bind Scope zbounded_scope with zbounded.
+Global Arguments Build_zbounded {r} value {_}, {r} value _, r value _.
+Global Arguments zbounded r : clear implicits.
+
+Definition adjust_zbounded {r} (v : zbounded r) : zbounded r
+  := {| value := value v ;
+        value_bounded := adjust_is_true (value_bounded v) |}.
+
+(** ** Equality for [zbounded] *)
+Section eq.
+  Definition value_path {r} {u v : zbounded r} (p : u = v)
+  : value u = value v
+    := f_equal (@value _) p.
+
+  Definition value_bounded_path {r} {u v : zbounded r} (p : u = v)
+    : eq_rect
+        _ (fun v => is_true ((lower r <=? v) && (v <=? upper r)))
+        (value_bounded u) _ (value_path p)
+      = value_bounded v.
+  Proof.
+    destruct p; reflexivity.
+  Defined.
+
+  Definition path_zbounded_full {r} (u v : zbounded r)
+             (p : value u = value v)
+             (q : eq_rect
+                    _ (fun v => is_true ((lower r <=? v) && (v <=? upper r)))
+                    (value_bounded u) _ p
+                  = value_bounded v)
+    : u = v.
+  Proof.
+    destruct u as [u1 u2], v as [v1 v2]; simpl in *; subst v1 v2; reflexivity.
+  Defined.
+
+  Definition path_zbounded {r} (u v : zbounded r)
+             (p : value u = value v)
+    : u = v.
+  Proof.
+    apply (path_zbounded_full u v p).
+    destruct u as [u1 u2], v as [v1 v2]; simpl in *; subst v1; simpl.
+    generalize dependent ((lower r <=? u1) && (u1 <=? upper r))%bool.
+    compute; intros b p q; clear.
+    transitivity (adjust_is_true q); clear; subst; reflexivity.
+  Defined.
+
+  Definition path_zbounded_rect_full {r} {u v : zbounded r} (Q : u = v -> Type)
+             (f : forall p q, Q (path_zbounded_full u v p q))
+    : forall p, Q p.
+  Proof.
+    intro p; specialize (f (value_path p) (value_bounded_path p));
+      destruct u as [u0 u1], p; exact f.
+  Defined.
+  Definition path_zbounded_rec_full {r u v} (Q : u = v :> zbounded r -> Set) := path_zbounded_rect_full Q.
+  Definition path_zbounded_ind_full {r u v} (Q : u = v :> zbounded r -> Prop) := path_zbounded_rec_full Q.
+
+  Definition path_zbounded_rect {r} {u v : zbounded r} (Q : u = v -> Type)
+             (f : forall p, Q (path_zbounded u v p))
+    : forall p, Q p.
+  Proof.
+    intro p; specialize (f (value_path p));
+      destruct u as [u0 u1], p.
+    simpl in *.
+    generalize dependent (@Build_zbounded r u0); intros.
+    generalize dependent ((lower r <=? u0) && (u0 <=? upper r))%bool; intros.
+    unfold is_true in *.
+    subst.
+    exact f.
+  Defined.
+  Definition path_zbounded_rec {r u v} (Q : u = v :> zbounded r -> Set) := path_zbounded_rect Q.
+  Definition path_zbounded_ind {r u v} (Q : u = v :> zbounded r -> Prop) := path_zbounded_rec Q.
+
+  (** *** η Principle for [zbounded] *)
+  Definition sigT_eta {r} (p : zbounded r)
+    : p = {| value := value p ; value_bounded := value_bounded p |}
+    := eq_refl.
+End eq.
+
+Ltac induction_zbounded_in_as_using H H0 H1 rect :=
+  induction H as [H0 H1] using (rect _ _ _);
+  cbn [value value_bounded] in H0, H1.
+Ltac induction_zbounded_in_using H rect :=
+  let H0 := fresh H in
+  let H1 := fresh H in
+  induction_zbounded_in_as_using H H0 H1 rect.
+Ltac inversion_zbounded_step :=
+  match goal with
+  | [ H : _ = @Build_zbounded _ _ _ |- _ ]
+    => induction_zbounded_in_using H @path_zbounded_rect_full
+  | [ H : @Build_zbounded _ _ _ = _ |- _ ]
+    => induction_zbounded_in_using H @path_zbounded_rect_full
+  end.
+Ltac inversion_zbounded := repeat inversion_zbounded_step.
+
+Lemma is_bounded_by'_zbounded {r} (v : zbounded r) : is_bounded_by' None r v.
+Proof.
+  destruct v as [v H]; cbv [is_bounded_by']; simpl.
+  unfold is_true in *; split_andb; Z.ltb_to_lt.
+  repeat apply conj; trivial.
+Qed.
+
+Global Instance dec_eq_zrange {r} : DecidableRel (@eq (zbounded r)) | 10.
+Proof.
+  intros [x ?] [y ?].
+  destruct (dec (x = y));
+    [ left; apply path_zbounded; assumption
+    | abstract (right; intro H; inversion_zbounded; tauto) ].
+Defined.