Add ZRange.OperationBounds

2 files changed, 100 insertions, 0 deletions

diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v
index 5f434c771..e41657428 100644
--- a/src/Util/ZRange/BasicLemmas.v
+++ b/src/Util/ZRange/BasicLemmas.v
@@ -177,4 +177,9 @@ Module ZRange.
     rewrite <- is_bounded_by_bool_opp at 1.
     rewrite normalize_opp, opp_involutive; reflexivity.
   Qed.
+
+  Lemma is_tighter_than_bool_constant r v
+    : is_tighter_than_bool (ZRange.constant v) r
+      = is_bounded_by_bool v r.
+  Proof. reflexivity. Qed.
 End ZRange.
diff --git a/src/Util/ZRange/OperationsBounds.v b/src/Util/ZRange/OperationsBounds.v
new file mode 100644
index 000000000..d57577210
--- /dev/null
+++ b/src/Util/ZRange/OperationsBounds.v
@@ -0,0 +1,95 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Classes.Morphisms.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZRange.Operations.
+Require Import Crypto.Util.ZRange.BasicLemmas.
+Require Import Crypto.Util.ZRange.CornersMonotoneBounds.
+Require Import Crypto.Util.ZRange.LandLorBounds.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.Morphisms.
+Require Import Crypto.Util.Notations.
+
+Module ZRange.
+  Local Ltac t :=
+    lazymatch goal with
+    | [ |- is_bounded_by_bool (?f _) (ZRange.two_corners ?f _) = true ]
+      => apply (@ZRange.monotoneb_two_corners_gen f)
+    | [ |- is_bounded_by_bool (?f _ _) (ZRange.four_corners ?f _ _) = true ]
+      => apply (@ZRange.monotoneb_four_corners_gen f)
+    | [ |- is_bounded_by_bool (?f _ _) (ZRange.four_corners_and_zero ?f _ _) = true ]
+      => apply (@ZRange.monotoneb_four_corners_and_zero_gen f)
+    end;
+    eauto with zarith;
+    repeat match goal with
+           | [ |- forall x : Z, _ ] => let x := fresh "x" in intro x; destruct x
+           end;
+    eauto with zarith.
+
+  Lemma is_bounded_by_bool_log2
+        x x_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+  : is_bounded_by_bool (Z.log2 x) (ZRange.log2 x_bs) = true.
+  Proof. t. Qed.
+
+  Lemma is_bounded_by_bool_log2_up
+        x x_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+  : is_bounded_by_bool (Z.log2_up x) (ZRange.log2_up x_bs) = true.
+  Proof. t. Qed.
+
+  Lemma is_bounded_by_bool_add
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+        (Hboundedy : is_bounded_by_bool y y_bs = true)
+  : is_bounded_by_bool (Z.add x y) (ZRange.add x_bs y_bs) = true.
+  Proof. t. Qed.
+
+  Lemma is_bounded_by_bool_sub
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+        (Hboundedy : is_bounded_by_bool y y_bs = true)
+  : is_bounded_by_bool (Z.sub x y) (ZRange.sub x_bs y_bs) = true.
+  Proof. t. Qed.
+
+  Lemma is_bounded_by_bool_mul
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+        (Hboundedy : is_bounded_by_bool y y_bs = true)
+  : is_bounded_by_bool (Z.mul x y) (ZRange.mul x_bs y_bs) = true.
+  Proof. t. Qed.
+
+  Lemma is_bounded_by_bool_div
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+        (Hboundedy : is_bounded_by_bool y y_bs = true)
+  : is_bounded_by_bool (Z.div x y) (ZRange.div x_bs y_bs) = true.
+  Proof. t. Qed.
+
+  Lemma is_bounded_by_bool_shiftr
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+        (Hboundedy : is_bounded_by_bool y y_bs = true)
+  : is_bounded_by_bool (Z.shiftr x y) (ZRange.shiftr x_bs y_bs) = true.
+  Proof. t. Qed.
+
+  Lemma is_bounded_by_bool_shiftl
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+        (Hboundedy : is_bounded_by_bool y y_bs = true)
+  : is_bounded_by_bool (Z.shiftl x y) (ZRange.shiftl x_bs y_bs) = true.
+  Proof. t. Qed.
+
+  Lemma is_bounded_by_bool_land
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+        (Hboundedy : is_bounded_by_bool y y_bs = true)
+  : is_bounded_by_bool (Z.land x y) (ZRange.land x_bs y_bs) = true.
+  Proof. now apply ZRange.is_bounded_by_bool_land_bounds. Qed.
+
+  Lemma is_bounded_by_bool_lor
+        x x_bs y y_bs
+        (Hboundedx : is_bounded_by_bool x x_bs = true)
+        (Hboundedy : is_bounded_by_bool y y_bs = true)
+  : is_bounded_by_bool (Z.lor x y) (ZRange.lor x_bs y_bs) = true.
+  Proof. now apply ZRange.is_bounded_by_bool_lor_bounds. Qed.
+End ZRange.