Add ZRange.OperationBounds

3 files changed, 136 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.
diff --git a/src/Util/ZUtil/Morphisms.v b/src/Util/ZUtil/Morphisms.v
index 15a9fcf1a..d073e0429 100644
--- a/src/Util/ZUtil/Morphisms.v
+++ b/src/Util/ZUtil/Morphisms.v
@@ -178,6 +178,12 @@ Module Z.
   Lemma div_Zneg_Zneg_le_Proper_l p : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.div (Zneg p) (Zneg x)).
   Proof. div_Proper_t. Qed.
   Hint Resolve div_Zneg_Zneg_le_Proper_l : zarith.
+  Lemma div_Z0_Zpos_le_Proper_l : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.div Z0 (Zpos x)).
+  Proof. div_Proper_t. Qed.
+  Hint Resolve div_Z0_Zpos_le_Proper_l : zarith.
+  Lemma div_Z0_Zneg_le_Proper_l : Proper (Pos.le ==> Z.le) (fun x => Z.div Z0 (Zneg x)).
+  Proof. div_Proper_t. Qed.
+  Hint Resolve div_Z0_Zneg_le_Proper_l : zarith.
   Lemma div_Zpos_Zpos_le_Proper_r x : Proper (Pos.le ==> Z.le) (fun p => Z.div (Zpos p) (Zpos x)).
   Proof. div_Proper_t. Qed.
   Hint Resolve div_Zpos_Zpos_le_Proper_r : zarith.
@@ -190,6 +196,12 @@ Module Z.
   Lemma div_Zneg_Zneg_le_Proper_r x : Proper (Pos.le ==> Z.le) (fun p => Z.div (Zneg p) (Zneg x)).
   Proof. div_Proper_t. Qed.
   Hint Resolve div_Zneg_Zneg_le_Proper_r : zarith.
+  Lemma div_Zpos_Z0_le_Proper_r : Proper (Pos.le ==> Z.le) (fun p => Z.div (Zpos p) Z0).
+  Proof. do 3 intro; cbv; congruence. Qed.
+  Hint Resolve div_Zpos_Z0_le_Proper_r : zarith.
+  Lemma div_Zneg_Z0_le_Proper_r : Proper (Basics.flip Pos.le ==> Z.le) (fun p => Z.div (Zneg p) Z0).
+  Proof. do 3 intro; cbv; congruence. Qed.
+  Hint Resolve div_Zneg_Z0_le_Proper_r : zarith.
   Local Ltac shift_t :=
     repeat first [ progress intros
                  | progress cbv [Proper respectful Basics.flip] in *
@@ -244,6 +256,12 @@ Module Z.
   Lemma shiftr_Zneg_Zneg_le_Proper_l p : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.shiftr (Zneg p) (Zneg x)).
   Proof. shift_Proper_t'. Qed.
   Hint Resolve shiftr_Zneg_Zneg_le_Proper_l : zarith.
+  Lemma shiftr_Z0_Zpos_le_Proper_l : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.shiftr Z0 (Zpos x)).
+  Proof. shift_Proper_t'. Qed.
+  Hint Resolve shiftr_Z0_Zpos_le_Proper_l : zarith.
+  Lemma shiftr_Z0_Zneg_le_Proper_l : Proper (Pos.le ==> Z.le) (fun x => Z.shiftr Z0 (Zneg x)).
+  Proof. shift_Proper_t'. Qed.
+  Hint Resolve shiftr_Z0_Zneg_le_Proper_l : zarith.
   Lemma shiftr_Zpos_Zpos_le_Proper_r x : Proper (Pos.le ==> Z.le) (fun p => Z.shiftr (Zpos p) (Zpos x)).
   Proof. shift_Proper_t'. Qed.
   Hint Resolve shiftr_Zpos_Zpos_le_Proper_r : zarith.
@@ -256,6 +274,12 @@ Module Z.
   Lemma shiftr_Zneg_Zneg_le_Proper_r x : Proper (Basics.flip Pos.le ==> Z.le) (fun p => Z.shiftr (Zneg p) (Zneg x)).
   Proof. shift_Proper_t'. Qed.
   Hint Resolve shiftr_Zneg_Zneg_le_Proper_r : zarith.
+  Lemma shiftr_Zpos_Z0_le_Proper_r : Proper (Pos.le ==> Z.le) (fun p => Z.shiftr (Zpos p) Z0).
+  Proof. shift_Proper_t'. Qed.
+  Hint Resolve shiftr_Zpos_Z0_le_Proper_r : zarith.
+  Lemma shiftr_Zneg_Z0_le_Proper_r : Proper (Basics.flip Pos.le ==> Z.le) (fun p => Z.shiftr (Zneg p) Z0).
+  Proof. shift_Proper_t'. Qed.
+  Hint Resolve shiftr_Zneg_Z0_le_Proper_r : zarith.
   Lemma shiftl_Zpos_Zpos_le_Proper_l p : Proper (Pos.le ==> Z.le) (fun x => Z.shiftl (Zpos p) (Zpos x)).
   Proof. shift_Proper_t'. Qed.
   Hint Resolve shiftl_Zpos_Zpos_le_Proper_l : zarith.
@@ -268,6 +292,12 @@ Module Z.
   Lemma shiftl_Zneg_Zneg_le_Proper_l p : Proper (Pos.le ==> Z.le) (fun x => Z.shiftl (Zneg p) (Zneg x)).
   Proof. shift_Proper_t'. Qed.
   Hint Resolve shiftl_Zneg_Zneg_le_Proper_l : zarith.
+  Lemma shiftl_Z0_Zpos_le_Proper_l : Proper (Pos.le ==> Z.le) (fun x => Z.shiftl Z0 (Zpos x)).
+  Proof. shift_Proper_t'. Qed.
+  Hint Resolve shiftl_Z0_Zpos_le_Proper_l : zarith.
+  Lemma shiftl_Z0_Zneg_le_Proper_l : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.shiftl Z0 (Zneg x)).
+  Proof. shift_Proper_t'. Qed.
+  Hint Resolve shiftl_Z0_Zneg_le_Proper_l : zarith.
   Lemma shiftl_Zpos_Zpos_le_Proper_r x : Proper (Pos.le ==> Z.le) (fun p => Z.shiftl (Zpos p) (Zpos x)).
   Proof. shift_Proper_t'. Qed.
   Hint Resolve shiftl_Zpos_Zpos_le_Proper_r : zarith.
@@ -280,6 +310,12 @@ Module Z.
   Lemma shiftl_Zneg_Zneg_le_Proper_r x : Proper (Basics.flip Pos.le ==> Z.le) (fun p => Z.shiftl (Zneg p) (Zneg x)).
   Proof. shift_Proper_t'. Qed.
   Hint Resolve shiftl_Zneg_Zneg_le_Proper_r : zarith.
+  Lemma shiftl_Zpos_Z0_le_Proper_r : Proper (Pos.le ==> Z.le) (fun p => Z.shiftl (Zpos p) Z0).
+  Proof. shift_Proper_t'. Qed.
+  Hint Resolve shiftl_Zpos_Z0_le_Proper_r : zarith.
+  Lemma shiftl_Zneg_Z0_le_Proper_r : Proper (Basics.flip Pos.le ==> Z.le) (fun p => Z.shiftl (Zneg p) Z0).
+  Proof. shift_Proper_t'. Qed.
+  Hint Resolve shiftl_Zneg_Z0_le_Proper_r : zarith.
 
   Hint Resolve Z.land_round_Proper_pos_r : zarith.
   Hint Resolve Z.land_round_Proper_pos_l : zarith.