Rename Bounds to ZRange, use Prop, not bool

As per @andres-erbsen's comments at
https://github.com/mit-plv/fiat-crypto/commit/ba864554da71ebe20b2494b1e8adf04779cd904b#commitcomment-21565223,
https://github.com/mit-plv/fiat-crypto/commit/ba864554da71ebe20b2494b1e8adf04779cd904b#commitcomment-21565200

3 files changed, 66 insertions, 69 deletions

diff --git a/src/Reflection/Z/BoundsInterpretations.v b/src/Reflection/Z/BoundsInterpretations.v
index 928402473..8e90213b6 100644
--- a/src/Reflection/Z/BoundsInterpretations.v
+++ b/src/Reflection/Z/BoundsInterpretations.v
@@ -5,7 +5,7 @@ Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
-Require Import Crypto.Util.Bounds.
+Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.Tactics.DestructHead.
 Export Reflection.Syntax.Notations.
 
@@ -13,6 +13,9 @@ Local Notation eta x := (fst x, snd x).
 Local Notation eta3 x := (eta (fst x), snd x).
 Local Notation eta4 x := (eta3 (fst x), snd x).
 
+Notation bounds := zrange.
+Delimit Scope bounds_scope with bounds.
+
 Module Import Bounds.
   Definition t := option bounds. (* TODO?: Separate out the bounds computation from the overflow computation? e.g., have [safety := in_bounds | overflow] and [t := bounds * safety]? *)
   Bind Scope bounds_scope with t.
@@ -32,7 +35,7 @@ Module Import Bounds.
       := match x with
          | Some x
            => match f x with
-              | Build_bounds l u
+              | {| lower := l ; upper := u |}
                 => SmartBuildBounds l u
               end
          | _ => None
@@ -41,7 +44,7 @@ Module Import Bounds.
       := match x, y with
          | Some x, Some y
            => match f x y with
-              | Build_bounds l u
+              | {| lower := l ; upper := u |}
                 => SmartBuildBounds l u
               end
          | _, _ => None
@@ -50,7 +53,7 @@ Module Import Bounds.
       := match x, y, z, w with
          | Some x, Some y, Some z, Some w
            => match f x y z w with
-              | Build_bounds l u
+              | {| lower := l ; upper := u |}
                 => SmartBuildBounds l u
               end
          | _, _, _, _ => None
@@ -102,7 +105,7 @@ Module Import Bounds.
   End with_bitwidth.
 
   Module Export Notations.
-    Export Util.Bounds.Notations.
+    Export Util.ZRange.Notations.
     Infix "+" := (add _) : bounds_scope.
     Infix "-" := (sub _) : bounds_scope.
     Infix "*" := (mul _) : bounds_scope.
@@ -136,10 +139,10 @@ Module Import Bounds.
        | Cast _ T => fun x => SmartRebuildBounds (bit_width_of_base_type T) x
        end%bounds.
 
-  Definition of_Z (z : Z) : t := Some (ZToBounds z).
+  Definition of_Z (z : Z) : t := Some (ZToZRange z).
 
   Definition of_interp t (z : Syntax.interp_base_type t) : interp_base_type t
-    := Some (ZToBounds (match t return Syntax.interp_base_type t -> Z with
+    := Some (ZToZRange (match t return Syntax.interp_base_type t -> Z with
                         | TZ => fun z => z
                         | TWord logsz => fun z => z (*FixedWordSizes.wordToZ*)
                         end z)).
@@ -175,20 +178,16 @@ Module Import Bounds.
   Definition bounds_are_good : forall {t}, interp_flat_type interp_base_type t -> Prop
     := (@interp_flat_type_rel_pointwise1 _ _ bound_is_good).
 
-  Definition is_bounded_byb {T} : Syntax.interp_base_type T -> interp_base_type T -> bool
+  Definition is_bounded_by' {T} : Syntax.interp_base_type T -> interp_base_type T -> Prop
     := fun val bound
        => match bound with
           | Some bounds'
-            => Util.Bounds.is_bounded_byb (bit_width_of_base_type T) bounds' val
-          | None => true
-          end%bool%Z.
-  Definition is_bounded_by' {T} : Syntax.interp_base_type T -> interp_base_type T -> Prop
-    := fun val bound => is_bounded_byb val bound = true.
+            => is_bounded_by' (bit_width_of_base_type T) bounds' val
+          | None => True
+          end.
 
   Definition is_bounded_by {T} : interp_flat_type Syntax.interp_base_type T -> interp_flat_type interp_base_type T -> Prop
     := interp_flat_type_rel_pointwise (@is_bounded_by').
-  Definition is_bounded_by_bool {T} : interp_flat_type Syntax.interp_base_type T -> interp_flat_type interp_base_type T -> bool
-    := interp_flat_type_relb_pointwise (@is_bounded_byb).
 
   Local Arguments interp_base_type !_ / .
   Global Instance dec_eq_interp_flat_type {T} : DecidableRel (@eq (interp_flat_type interp_base_type T)) | 10.
diff --git a/src/Util/Bounds.v b/src/Util/Bounds.v
deleted file mode 100644
index 86a94ef60..000000000
--- a/src/Util/Bounds.v
+++ /dev/null
@@ -1,54 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.Decidable.
-Require Import Crypto.Util.Notations.
-
-Delimit Scope bounds_scope with bounds.
-Record bounds := { lower : Z ; upper : Z }.
-Bind Scope bounds_scope with bounds.
-Local Open Scope Z_scope.
-
-Definition ZToBounds (z : Z) : bounds := {| lower := z ; upper := z |}.
-
-Ltac inversion_bounds :=
-  let lower := (eval cbv [lower] in (fun x => lower x)) in
-  let upper := (eval cbv [upper] in (fun y => upper y)) in
-  repeat match goal with
-         | [ H : _ = _ :> bounds |- _ ]
-           => pose proof (f_equal lower H); pose proof (f_equal upper H); clear H;
-              cbv beta iota in *
-         end.
-
-(** All of the boundedness properties take an optional bitwidth, and
-    enforce the condition that the bounds are within 0 and 2^bitwidth,
-    if given. *)
-Section with_bitwidth.
-  Context (bitwidth : option Z).
-
-  Definition is_bounded_byb : bounds -> Z -> bool
-    := fun bound val
-       => (((lower bound <=? val) && (val <=? upper bound))
-             && (match bitwidth with
-                 | Some sz => (0 <=? lower bound) && (upper bound <? 2^sz)
-                 | None => true
-                 end))%bool%Z.
-  Definition is_bounded_by' : bounds -> Z -> Prop
-    := fun bound val => is_bounded_byb bound val = true.
-
-  Definition is_bounded_by {n} : Tuple.tuple bounds n -> Tuple.tuple Z n -> Prop
-    := Tuple.pointwise2 is_bounded_by'.
-End with_bitwidth.
-
-Global Instance dec_eq_bounds : DecidableRel (@eq bounds) | 10.
-Proof.
-  intros [lx ux] [ly uy].
-  destruct (dec (lx = ly)), (dec (ux = uy));
-    [ left; apply f_equal2; assumption
-    | abstract (right; intro H; inversion_bounds; tauto).. ].
-Defined.
-
-Module Export Notations.
-  Delimit Scope bounds_scope with bounds.
-  Notation "b[ l ~> u ]" := {| lower := l ; upper := u |}
-                              (format "b[ l  ~>  u ]") : bounds_scope.
-End Notations.
diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v
new file mode 100644
index 000000000..f68b3e5ff
--- /dev/null
+++ b/src/Util/ZRange.v
@@ -0,0 +1,52 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.Notations.
+
+Delimit Scope zrange_scope with zrange.
+Record zrange := { lower : Z ; upper : Z }.
+Bind Scope zrange_scope with zrange.
+Local Open Scope Z_scope.
+
+Definition ZToZRange (z : Z) : zrange := {| lower := z ; upper := z |}.
+
+Ltac inversion_zrange :=
+  let lower := (eval cbv [lower] in (fun x => lower x)) in
+  let upper := (eval cbv [upper] in (fun y => upper y)) in
+  repeat match goal with
+         | [ H : _ = _ :> zrange |- _ ]
+           => pose proof (f_equal lower H); pose proof (f_equal upper H); clear H;
+              cbv beta iota in *
+         end.
+
+(** All of the boundedness properties take an optional bitwidth, and
+    enforce the condition that the range is within 0 and 2^bitwidth,
+    if given. *)
+Section with_bitwidth.
+  Context (bitwidth : option Z).
+
+  Definition is_bounded_by' : zrange -> Z -> Prop
+    := fun bound val
+       => lower bound <= val <= upper bound
+          /\ match bitwidth with
+             | Some sz => 0 <= lower bound /\ upper bound < 2^sz
+             | None => True
+             end.
+
+  Definition is_bounded_by {n} : Tuple.tuple zrange n -> Tuple.tuple Z n -> Prop
+    := Tuple.pointwise2 is_bounded_by'.
+End with_bitwidth.
+
+Global Instance dec_eq_zrange : DecidableRel (@eq zrange) | 10.
+Proof.
+  intros [lx ux] [ly uy].
+  destruct (dec (lx = ly)), (dec (ux = uy));
+    [ left; apply f_equal2; assumption
+    | abstract (right; intro H; inversion_zrange; tauto).. ].
+Defined.
+
+Module Export Notations.
+  Delimit Scope zrange_scope with zrange.
+  Notation "b[ l ~> u ]" := {| lower := l ; upper := u |}
+                              (format "b[ l  ~>  u ]") : zrange_scope.
+End Notations.