Fix split_bounds, prove it correct

4 files changed, 26 insertions, 1 deletions

diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v
index 8da5e69d7..6b5a430c4 100644
--- a/src/Util/ZRange/BasicLemmas.v
+++ b/src/Util/ZRange/BasicLemmas.v
@@ -8,6 +8,7 @@ Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.SpecializeAllWays.
+Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Tactics.DestructHead.
 
@@ -97,4 +98,12 @@ Module ZRange.
       intros; Bool.split_andb; rewrite Bool.andb_true_iff; split; Z.ltb_to_lt; cbn [lower upper] in *; split_min_max.
     all: lia.
   Qed.
+
+  Lemma is_bounded_by_bool_opp x r : is_bounded_by_bool (Z.opp x) (ZRange.opp r) = is_bounded_by_bool x r.
+  Proof.
+    cbv [is_bounded_by_bool andb opp]; cbn [lower upper]; break_match; Z.ltb_to_lt; break_match; Z.ltb_to_lt;
+      try (symmetry; progress Z.ltb_to_lt);
+      try reflexivity;
+      try lia.
+  Qed.
 End ZRange.
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v
index 07e330a4a..95f32869c 100644
--- a/src/Util/ZRange/Operations.v
+++ b/src/Util/ZRange/Operations.v
@@ -102,7 +102,7 @@ Module ZRange.
   Definition land_bounds : zrange -> zrange -> zrange := land_lor_bounds Z.land.
   Definition lor_bounds : zrange -> zrange -> zrange := land_lor_bounds Z.lor.
 
-  Definition split_bounds (r : zrange) (split_at : BinInt.Z) : zrange * zrange :=
+  Definition split_bounds_pos (r : zrange) (split_at : BinInt.Z) : zrange * zrange :=
     if upper r <? split_at
     then if (0 <=? lower r)%Z
          then (r, {| lower := 0; upper := 0 |})
@@ -110,6 +110,13 @@ Module ZRange.
                 {| lower := lower r / split_at; upper := (upper r / split_at) |} )
     else ( {| lower := 0; upper := split_at - 1 |},
            {| lower := lower r / split_at; upper := (upper r / split_at) |} ).
+  Definition split_bounds (r : zrange) (split_at : BinInt.Z) : zrange * zrange :=
+    if (0 <? split_at)%Z
+    then split_bounds_pos r split_at
+    else if (split_at =? 0)%Z
+         then ({| lower := 0; upper := 0 |}, {| lower := 0 ; upper := 0 |})
+         else let '(q, r) := split_bounds_pos (opp r) (-split_at) in
+              (opp q, r).
 
   Definition good (r : zrange) : Prop
     := lower r <= upper r.
diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v
index a9fc4aae0..5ae17ad1a 100644
--- a/src/Util/ZUtil/Div.v
+++ b/src/Util/ZUtil/Div.v
@@ -258,4 +258,8 @@ Module Z.
     intros; subst; auto with zarith.
   Qed.
   Hint Resolve div_same' : zarith.
+
+  Lemma div_opp_r a b : a / (-b) = ((-a) / b).
+  Proof. Z.div_mod_to_quot_rem; nia. Qed.
+  Hint Resolve div_opp_r : zarith.
 End Z.
diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v
index 8dea71870..84917a454 100644
--- a/src/Util/ZUtil/Modulo.v
+++ b/src/Util/ZUtil/Modulo.v
@@ -4,6 +4,7 @@ Require Import Crypto.Util.ZUtil.ZSimplify.Core.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos.
+Require Import Crypto.Util.ZUtil.Div.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
 Local Open Scope Z_scope.
@@ -282,4 +283,8 @@ Module Z.
     autorewrite with zsimplify_const.
     reflexivity.
   Qed.
+
+  Lemma mod_opp_r a b : a mod (-b) = -((-a) mod b).
+  Proof. pose proof (Z.div_opp_r a b); Z.div_mod_to_quot_rem; nia. Qed.
+  Hint Resolve mod_opp_r : zarith.
 End Z.