Try out stronger land, lor bounds

2 files changed, 191 insertions, 69 deletions

diff --git a/src/Util/ZRange/CornersMonotoneBounds.v b/src/Util/ZRange/CornersMonotoneBounds.v
index f41c712ed..5edeee5e8 100644
--- a/src/Util/ZRange/CornersMonotoneBounds.v
+++ b/src/Util/ZRange/CornersMonotoneBounds.v
@@ -4,6 +4,7 @@ Require Import Coq.micromega.Psatz.
 Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
 Require Import Crypto.Util.ZUtil.Stabilization.
 Require Import Crypto.Util.ZUtil.MulSplit.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.ZRange.
@@ -19,31 +20,89 @@ Local Open Scope Z_scope.
 Module ZRange.
   Import Operations.ZRange.
   Local Arguments is_bounded_by' !_ _ _ / .
+  Local Coercion is_true : bool >-> Sortclass.
 
-  Lemma monotone_two_corners_genb
-        (f : Z -> Z)
-        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
-        (Hmonotone : exists b, Proper (R b ==> Z.le) f)
+  (*Definition extremes_at_boundaries
+             (f : Z -> Z)
+             x_bs
+    : forall x, is_bounded_by_bool x x_bs -> is_bounded_by_bool*)
+
+  Lemma monotone_apply_to_range_genbP
+        (P : Z -> Prop)
+        (f : Z -> zrange)
+        (R := fun b : bool => fun x y => P x /\ P y /\ if b then Z.le x y else Basics.flip Z.le x y)
+        (Hmonotonel : exists b, Proper (R b ==> Z.le) (fun v => lower (f v)))
+        (Hmonotoneu : exists b, Proper (R b ==> Z.le) (fun v => upper (f v)))
         x_bs x
-        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-    : ZRange.is_bounded_by' None (two_corners f x_bs) (f x).
+        (Hboundedx : is_bounded_by_bool x x_bs)
+        (x_bs_ok : forall xv, is_bounded_by_bool xv x_bs -> P xv)
+    : is_tighter_than_bool (f x) (apply_to_range f x_bs).
   Proof.
-    split; trivial.
     destruct x_bs as [lx ux]; simpl in *.
-    destruct Hboundedx as [Hboundedx _].
+    cbv [is_bounded_by_bool is_true is_tighter_than_bool] in *.
+    cbn [lower upper] in *.
+    rewrite !Bool.andb_true_iff, !Z.leb_le_iff in *.
+    setoid_rewrite Bool.andb_true_iff in x_bs_ok.
+    repeat setoid_rewrite Z.leb_le_iff in x_bs_ok.
     destruct_head'_ex.
     repeat match goal with
-           | [ H : Proper (R ?b ==> Z.le) f |- _ ]
+           | [ H : Proper (R ?b ==> _) _ |- _ ]
              => unique assert (R b (if b then lx else x) (if b then x else lx)
-                               /\ R b (if b then x else ux) (if b then ux else x))
-               by (unfold R, Basics.flip; destruct b; omega)
+                              /\ R b (if b then x else ux) (if b then ux else x))
+               by (unfold R, Basics.flip; destruct b; repeat apply conj; eauto with omega)
            end.
     destruct_head' and.
     repeat match goal with
-           | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
+           | [ H : Proper (R ?b ==> _) _, H' : R ?b _ _ |- _ ]
              => unique pose proof (H _ _ H')
            end.
-    destruct_head bool; split_min_max; omega.
+    destruct_head bool; split_andb; Z.ltb_to_lt; split_min_max; omega.
+  Qed.
+
+  Lemma monotone_apply_to_range_genb
+        (f : Z -> zrange)
+        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
+        (Hmonotonel : exists b, Proper (R b ==> Z.le) (fun v => lower (f v)))
+        (Hmonotoneu : exists b, Proper (R b ==> Z.le) (fun v => upper (f v)))
+        x_bs x
+        (Hboundedx : is_bounded_by_bool x x_bs)
+    : is_tighter_than_bool (f x) (apply_to_range f x_bs).
+  Proof.
+    apply (monotone_apply_to_range_genbP (fun _ => True)); cbv [Proper respectful] in *; eauto;
+      destruct_head'_ex;
+      match goal with
+      | [ b : bool |- _ ] => exists b; destruct b; solve [ intuition eauto ]
+      end.
+  Qed.
+
+  Lemma monotone_two_corners_genb'
+        (f : Z -> Z)
+        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
+        (Hmonotone : exists b, Proper (R b ==> Z.le) f)
+        x_bs x
+        (Hboundedx : is_bounded_by_bool x x_bs)
+    : is_tighter_than_bool (constant (f x)) (two_corners f x_bs).
+  Proof.
+    cbv [two_corners].
+    lazymatch goal with
+    | [ |- context[apply_to_range ?f ?x_bs] ]
+      => apply (monotone_apply_to_range_genb f); auto
+    end.
+  Qed.
+
+  Lemma monotone_two_corners_genb
+        (f : Z -> Z)
+        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
+        (Hmonotone : exists b, Proper (R b ==> Z.le) f)
+        x_bs x
+        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
+    : ZRange.is_bounded_by' None (two_corners f x_bs) (f x).
+  Proof.
+    pose proof (monotone_two_corners_genb' f Hmonotone x_bs x) as H.
+    cbv [constant is_bounded_by' is_bounded_by_bool is_true is_tighter_than_bool] in *.
+    cbn [upper lower] in *.
+    rewrite ?Bool.andb_true_iff, ?Z.leb_le_iff in *.
+    tauto.
   Qed.
 
   Lemma monotone_two_corners_gen
@@ -70,6 +129,63 @@ Module ZRange.
     intros ???; apply Hmonotone; auto.
   Qed.
 
+  (*
+  Lemma monotone_four_corners_genb'
+        (f : Z -> Z -> Z)
+        (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
+        (Hmonotone1 : forall x, exists b, Proper (R b ==> Z.le) (f x))
+        (Hmonotone2 : forall y, exists b, Proper (R b ==> Z.le) (fun x => f x y))
+        x_bs y_bs x y
+        (Hboundedx : is_bounded_by_bool x x_bs)
+        (Hboundedy : is_bounded_by_bool y y_bs)
+    : is_tighter_than_bool (constant (f x y)) (four_corners f x_bs y_bs).
+  Proof.
+    cbv [four_corners].
+    etransitivity;
+      [ apply monotone_two_corners_genb'; solve [ eauto ]
+      | ].
+    cbv [apply_to_range union two_corners constant is_bounded_by_bool is_tighter_than_bool]; cbn [lower upper] in *.
+      | lazymatch goal with
+        | [ |- context[apply_to_range ?f ?x_bs] ]
+          => apply (monotone_apply_to_range_genb f); [ | | eassumption ]
+        end ];
+      auto.
+    { cbv [two_corners constant apply_to_range union flip].
+      cbn [lower upper].
+      subst R.
+      cbv [is_bounded_by_bool is_true] in *; split_andb; Z.ltb_to_lt.
+      assert (Hx_good : lower x_bs <= upper x_bs) by omega.
+      assert (Hy_good : lower y_bs <= upper y_bs) by omega.
+      pose proof (Hmonotone2 (lower y_bs)).
+      pose proof (Hmonotone2 (upper y_bs)).
+      destruct_head'_ex; destruct_head'_bool; [ exists true | | | exists false ];
+        try intros ?? Hc;
+        repeat match goal with
+               | [ H : Proper _ _ |- _ ] => specialize (H _ _ Hc)
+               end;
+        split_min_max; cbn beta in *; try omega.
+      all: pose proof (Hmonotone1 (lower x_bs)).
+      all: pose proof (Hmonotone1 (upper x_bs)).
+      all: destruct_head'_ex.
+      all: destruct_head'_bool.
+      all: repeat match goal with
+                  | [ H : Proper _ (fun x => ?f x _) |- _ ]
+                    => unique pose proof (H _ _ Hx_good)
+                  | [ H : Proper _ (?f _) |- _ ]
+                    => unique pose proof (H _ _ Hy_good)
+                  end;
+        cbn beta in *.
+      cbv [Basics.flip] in *.
+      all:try omega.
+
+      repeat match goal with
+             | [
+      { exists true.
+
+    cbv [two_corners].
+
+  Qed.*)
+
   Lemma monotone_four_corners_genb
         (f : Z -> Z -> Z)
         (R := fun b : bool => if b then Z.le else Basics.flip Z.le)
@@ -109,7 +225,10 @@ Module ZRange.
            | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
              => unique pose proof (H _ _ H')
            end; cbv beta in *.
-    destruct_head bool; split_min_max; omega.
+    destruct_head bool.
+    all: revert_min_max; intros.
+    all: (split; [ repeat (etransitivity; [ | eassumption ]) | repeat (etransitivity; [ eassumption | ]) ]).
+    all: auto using Z.le_min_l, Z.le_min_r, Z.le_max_l, Z.le_max_r.
   Qed.
 
   Lemma monotone_four_corners_gen
@@ -186,24 +305,10 @@ Module ZRange.
            | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ]
              => unique pose proof (H _ _ H')
            end.
-    destruct_head bool; split_min_max; omega.
-  Qed.
-
-  Lemma monotone_eight_corners_gen
-        (f : Z -> Z -> Z -> Z)
-        (Hmonotone1 : forall x y, Proper (Z.le ==> Z.le) (f x y) \/ Proper (Basics.flip Z.le ==> Z.le) (f x y))
-        (Hmonotone2 : forall x z, Proper (Z.le ==> Z.le) (fun y => f x y z) \/ Proper (Basics.flip Z.le ==> Z.le) (fun y => f x y z))
-        (Hmonotone3 : forall y z, Proper (Z.le ==> Z.le) (fun x => f x y z) \/ Proper (Basics.flip Z.le ==> Z.le) (fun x => f x y z))
-        x_bs y_bs z_bs x y z
-        (Hboundedx : ZRange.is_bounded_by' None x_bs x)
-        (Hboundedy : ZRange.is_bounded_by' None y_bs y)
-        (Hboundedz : ZRange.is_bounded_by' None z_bs z)
-    : ZRange.is_bounded_by' None (ZRange.eight_corners f x_bs y_bs z_bs) (f x y z).
-  Proof.
-    eapply monotone_eight_corners_genb; auto.
-    { intros x' y'; destruct (Hmonotone1 x' y'); [ exists true | exists false ]; assumption. }
-    { intros x' y'; destruct (Hmonotone2 x' y'); [ exists true | exists false ]; assumption. }
-    { intros x' y'; destruct (Hmonotone3 x' y'); [ exists true | exists false ]; assumption. }
+    destruct_head bool.
+    all: revert_min_max; intros.
+    all: (split; [ repeat (etransitivity; [ | eassumption ]) | repeat (etransitivity; [ eassumption | ]) ]).
+    all: auto using Z.le_min_l, Z.le_min_r, Z.le_max_l, Z.le_max_r.
   Qed.
   Lemma monotone_eight_corners
         (b1 b2 b3 : bool)
diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v
index d17785f77..07e330a4a 100644
--- a/src/Util/ZRange/Operations.v
+++ b/src/Util/ZRange/Operations.v
@@ -1,5 +1,7 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZUtil.Definitions.
+
 Require Import Crypto.Util.Notations.
 
 Module ZRange.
@@ -41,49 +43,64 @@ Module ZRange.
     := let (l, u) := eta v in
        r[ f l ~> f u ].
 
-  Definition two_corners (f : Z -> Z) (v : zrange) : zrange
+  Definition split_range_at_0 (x : zrange) : option zrange (* < 0 *) * option zrange (* >= 0 *)
+    := let (l, u) := eta x in
+       (if (0 <=? l)%Z
+        then None
+        else Some r[l ~> Z.min u (-1)],
+        if (0 <=? u)%Z
+        then Some r[Z.max 0 l ~> u]
+        else None).
+
+  Definition apply_to_split_range (f : zrange -> zrange) (v : zrange) : zrange
+    := match split_range_at_0 v with
+       | (Some n, Some p) => union (f n) (f p)
+       | (Some v, None) | (None, Some v) => f v
+       | (None, None) => f v
+       end.
+
+  Definition apply_to_range (f : BinInt.Z -> zrange) (v : zrange) : zrange
     := let (l, u) := eta v in
-       r[ Z.min (f l) (f u) ~> Z.max (f u) (f l) ].
+       union (f l) (f u).
 
-  Definition two_corners' (f : Z -> Z) (v : zrange) : zrange
-    := normalize' (map f v).
+  Definition apply_to_each_split_range (f : BinInt.Z -> zrange) (v : zrange) : zrange
+    := apply_to_split_range (apply_to_range f) v.
 
-  Lemma two_corners'_eq : two_corners = two_corners'. Proof. reflexivity. Defined.
+  Definition constant (v : Z) : zrange := r[v ~> v].
 
+  Definition two_corners (f : Z -> Z) (v : zrange) : zrange
+    := apply_to_range (fun x => constant (f x)) v.
   Definition four_corners (f : Z -> Z -> Z) (x y : zrange) : zrange
-    := let (lx, ux) := eta x in
-       union (two_corners (f lx) y)
-             (two_corners (f ux) y).
-
+    := apply_to_range (fun x => two_corners (f x) y) x.
   Definition eight_corners (f : Z -> Z -> Z -> Z) (x y z : zrange) : zrange
-    := let (lx, ux) := eta x in
-       union (four_corners (f lx) y z)
-             (four_corners (f ux) y z).
-
-  Definition upper_lor_land_bounds (x y : BinInt.Z) : BinInt.Z
-    := 2^(1 + Z.log2_up (Z.max x y)).
-  Definition extreme_lor_land_bounds (x y : zrange) : zrange
-    := let mx := ZRange.upper (ZRange.abs x) in
-       let my := ZRange.upper (ZRange.abs y) in
-       {| lower := -upper_lor_land_bounds mx my ; upper := upper_lor_land_bounds mx my |}.
-  Definition extremization_bounds (f : zrange -> zrange -> zrange) (x y : zrange) : zrange
-    := let (lx, ux) := x in
-       let (ly, uy) := y in
-       if ((lx <? 0) || (ly <? 0))%Z%bool
-       then extreme_lor_land_bounds x y
-       else f x y.
-  Definition land_bounds : zrange -> zrange -> zrange
-    := extremization_bounds
-         (fun x y
-          => let (lx, ux) := x in
-             let (ly, uy) := y in
-             {| lower := Z.min 0 (Z.min lx ly) ; upper := Z.max 0 (Z.min ux uy) |}).
-  Definition lor_bounds : zrange -> zrange -> zrange
-    := extremization_bounds
-         (fun x y
-          => let (lx, ux) := x in
-             let (ly, uy) := y in
-             {| lower := Z.max lx ly ; upper := upper_lor_land_bounds ux uy |}).
+    := apply_to_range (fun x => four_corners (f x) y z) x.
+
+  Definition two_corners_and_zero (f : Z -> Z) (v : zrange) : zrange
+    := apply_to_each_split_range (fun x => constant (f x)) v.
+  Definition four_corners_and_zero (f : Z -> Z -> Z) (x y : zrange) : zrange
+    := apply_to_split_range (apply_to_range (fun x => two_corners_and_zero (f x) y)) x.
+  Definition eight_corners_and_zero (f : Z -> Z -> Z -> Z) (x y z : zrange) : zrange
+    := apply_to_split_range (apply_to_range (fun x => four_corners_and_zero (f x) y z)) x.
+
+  Definition two_corners' (f : Z -> Z) (v : zrange) : zrange
+    := normalize' (map f v).
+
+  Lemma two_corners'_eq x y : two_corners x y = two_corners' x y.
+  Proof.
+    cbv [two_corners two_corners' normalize' map union apply_to_range constant flip].
+    cbn [lower upper].
+    rewrite Z.max_comm; reflexivity.
+  Qed.
+
+  (** if positive, round up to 2^k-1 (0b11111....); if negative, round down to -2^k (0b...111000000...) *)
+  Definition round_lor_land_bound (x : BinInt.Z) : BinInt.Z
+    := if (0 <=? x)%Z
+       then 2^(Z.log2_up (x+1))-1
+       else -2^(Z.log2_up (-x)).
+  Definition land_lor_bounds (f : BinInt.Z -> BinInt.Z -> BinInt.Z) (x y : zrange) : zrange
+    := four_corners_and_zero (fun x y => f (round_lor_land_bound x) (round_lor_land_bound y)) x y.
+  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 :=
     if upper r <? split_at