From 174d4398c5198a3fae5b1ece9df58edb17ded679 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 27 Jun 2018 19:37:10 -0400 Subject: Try out stronger land, lor bounds --- src/Util/ZRange/CornersMonotoneBounds.v | 169 ++++++++++++++++++++++++++------ src/Util/ZRange/Operations.v | 91 ++++++++++------- 2 files changed, 191 insertions(+), 69 deletions(-) (limited to 'src/Util/ZRange') 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 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