From 8926b3f6b2aa1fe0f8d3f65f1966f60402cad4b9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 13 Aug 2018 23:58:49 -0400 Subject: Prove monotonicity properties about zrange --- src/Util/Bool.v | 5 + src/Util/ZRange/CornersMonotoneBounds.v | 838 ++++++++++++++++++++++---------- src/Util/ZRange/Operations.v | 49 ++ 3 files changed, 625 insertions(+), 267 deletions(-) (limited to 'src') diff --git a/src/Util/Bool.v b/src/Util/Bool.v index fe6ae64e4..fb2038de5 100644 --- a/src/Util/Bool.v +++ b/src/Util/Bool.v @@ -103,3 +103,8 @@ Ltac split_andb_in_context := repeat split_andb_in_context_step. Lemma if_const A (b : bool) (x : A) : (if b then x else x) = x. Proof. case b; reflexivity. Qed. + +Lemma ex_bool_iff_or P : @ex bool P <-> (or (P true) (P false)). +Proof. + split; [ intros [ [] ? ] | intros [?|?]; eexists ]; eauto. +Qed. diff --git a/src/Util/ZRange/CornersMonotoneBounds.v b/src/Util/ZRange/CornersMonotoneBounds.v index 5edeee5e8..9cea5c376 100644 --- a/src/Util/ZRange/CornersMonotoneBounds.v +++ b/src/Util/ZRange/CornersMonotoneBounds.v @@ -10,7 +10,9 @@ Require Import Crypto.Util.Bool. Require Import Crypto.Util.ZRange. Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.ZRange.BasicLemmas. +Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.SpecializeAllWays. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.SpecializeBy. @@ -22,332 +24,634 @@ Module ZRange. Local Arguments is_bounded_by' !_ _ _ / . Local Coercion is_true : bool >-> Sortclass. - (*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 : 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). + Fixpoint app' {A B} {n : nat} : nary_T A B (S n) -> tuple' A n -> B + := match n with + | O => fun f x => f x + | S n => fun f '(xs, x) => @app' A B n (f x) xs + end. + Definition app {A B} {n : nat} : nary_T A B n -> tuple A n -> B + := match n with + | O => fun x _ => x + | S n => @app' A B n + end. + + Local Notation R b := (match b with true => Z.le | false => Basics.flip Z.le end). + + Local Notation Rp b := (match b with true => Pos.le | false => Basics.flip Pos.le end). + + Fixpoint is_monotone_on_projections {n : nat} : nary_T Z Z n -> Prop + := match n with + | O => fun _ => True + | S n' => fun f + => (forall x, is_monotone_on_projections (f x)) + /\ (forall args, exists b, Proper (R b ==> Z.le) (fun x => app (f x) args)) + end. + + Fixpoint is_piecewise_monotone_on_projections {n : nat} : nary_T Z Z n -> Prop + := match n with + | O => fun _ => True + | S n' + => fun f + => (forall x, is_piecewise_monotone_on_projections (f x)) + /\ (forall args, exists b, Proper (Rp b ==> Z.le) (fun x => app (f (Zpos x)) args)) + /\ (forall args, exists b, Proper (Rp b ==> Z.le) (fun x => app (f (Zneg x)) args)) + end. + + Definition all_are_bounded_by_bool {n} (v : tuple Z n) (v_bs : tuple zrange n) : bool + := Tuple.fieldwiseb is_bounded_by_bool v v_bs. + + Local Ltac fast_split_min_max := rewrite ?Z.min_le_iff, ?Z.max_le_iff. + + Local Ltac t_fin_common_step := + first [ progress cbv [all_are_bounded_by_bool is_bounded_by_bool is_monotone_on_projections is_true is_tighter_than_bool] in * + | progress cbv [Proper respectful Basics.flip] in * + | progress cbn in * + | progress rewrite ?Bool.orb_true_iff, ?Bool.orb_false_iff, ?Bool.andb_true_iff, ?Z.leb_le, ?Z.ltb_lt in * + | progress Z.ltb_to_lt + | progress fast_split_min_max + | progress destruct_head'_and + | progress destruct_head'_prod + | progress destruct_head'_ex + | progress specialize_by exact tt + | progress specialize_by exact I + | progress destruct_head' zrange + | solve [ auto using or_introl, or_intror, Z.le_refl ] + | match goal with + | [ H : _ -> True |- _ ] => clear H + | [ H : ?x <= ?x |- _ ] => clear H + | [ H : ?x \/ ?x |- _ ] => assert x by (destruct H; assumption); clear H + | [ H : ?x < ?x |- _ ] => exfalso; clear -H; lia + | [ H : 0 <= Z.pos _ |- _ ] => clear H + | [ H : 0 < Z.pos _ |- _ ] => clear H + | [ H : Z.neg _ <= 0 |- _ ] => clear H + | [ H : Z.neg _ < 0 |- _ ] => clear H + | [ H : Z.pos _ <= Z.neg _ |- _ ] => exfalso; clear -H; lia + | [ H : Z.pos _ <= 0 |- _ ] => exfalso; clear -H; lia + | [ H : 0 <= Z.neg _ |- _ ] => exfalso; clear -H; lia + | [ H : Z.pos _ < 0 |- _ ] => exfalso; clear -H; lia + | [ |- context[Z.max 1 (Z.pos ?x)] ] => rewrite (Z.max_r 1 (Zpos x)) by (clear; lia) + | [ |- context[Z.min 1 (Z.pos ?x)] ] => rewrite (Z.min_l 1 (Zpos x)) by (clear; lia) + | [ H : ?x > ?y |- _ ] => assert (y < x) by (clear -H; lia); clear H + | [ H : ?x >= ?y |- _ ] => assert (y <= x) by (clear -H; lia); clear H + | [ |- context[Z.max (Z.neg ?x) (-1)] ] => rewrite (Z.max_r (Zneg x) (-1)) by (clear; lia) + | [ |- context[Z.min (Z.neg ?x) (-1)] ] => rewrite (Z.min_l (Zneg x) (-1)) by (clear; lia) + end ]. + Local Ltac t_fin_saturate_step := + first [ progress destruct_head'_bool + | match goal with + | [ H : forall (x : Z) (y : Z), _ <= _ -> _ <= _, v : Z |- _ ] + => unique pose proof (H v v ltac:(reflexivity)) + | [ H : forall (x : Z) (y : Z), _ <= _ -> _ <= _, v : Z, v' : Z |- _ ] + => unique pose proof (H v v' ltac:(auto || reflexivity)) + end + | apply conj ]. + Local Ltac t_fin_specific_pos_step := + first [ match goal with + | [ H : _ \/ _ |- _ ] => destruct H as [H|H]; try (exfalso; clear -H; lia); [] + | [ H : Z.pos _ <= ?v |- _ ] => is_var v; destruct v as [|v|v]; try (exfalso; clear -H; lia) + | [ H : ?v <= Z.neg _ |- _ ] => is_var v; destruct v as [|v|v]; try (exfalso; clear -H; lia) + | [ H : 0 <= ?v |- _ ] => is_var v; destruct v as [|v|v]; try (exfalso; clear -H; lia) + | [ H : ?v <= 0 |- _ ] => is_var v; destruct v as [|v|v]; try (exfalso; clear -H; lia) + | [ H : 0 < ?v |- _ ] => is_var v; destruct v as [|v|v]; try (exfalso; clear -H; lia) + | [ H : ?v < 0 |- _ ] => is_var v; destruct v as [|v|v]; try (exfalso; clear -H; lia) + end + | break_innermost_match_step + | progress destruct_head'_bool + | match goal with + | [ H' : Z.le (?f ?p) (?g ?q) |- _ ] + => first [ unique assert (Pos.le p q) by (clear -H'; lia) + | unique assert (Pos.le q p) by (clear -H'; lia) ] + | [ H : forall x y, Pos.le _ _ -> _ <= _, H' : Pos.le _ _ |- _ ] + => unique pose proof (H _ _ H') + | [ H : forall x y, Pos.le x _ -> _ <= _, v : positive |- _ ] + => unique pose proof (H 1%positive v ltac:(clear; lia)) + | [ H : forall x y, Pos.le _ x -> _ <= _, v : positive |- _ ] + => unique pose proof (H v 1%positive ltac:(clear; lia)) + end + | apply conj + | progress destruct_head' Z ]. + Local Ltac t_fin := + repeat first [ t_fin_common_step + | t_fin_saturate_step ]. + Local Ltac t_fin_pos := + repeat first [ t_fin_common_step + | t_fin_specific_pos_step ]. + + Lemma pull_union_under_args2 A n f g bs + : @app' A _ n (under_args2 union f g) bs + = union (app' f bs) (app' g bs). + Proof. induction n; t_fin. Qed. + + Lemma monotone_n_corners_genb + n f + (Hmonotone : @is_monotone_on_projections n f) + v v_bs + (Hboundedx : @all_are_bounded_by_bool n v v_bs) + : is_bounded_by_bool (app f v) (app (n_corners f) v_bs). Proof. - destruct x_bs as [lx ux]; simpl in *. - 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 ==> _) _ |- _ ] - => 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; repeat apply conj; eauto with omega) - end. - destruct_head' and. - repeat match goal with - | [ H : Proper (R ?b ==> _) _, H' : R ?b _ _ |- _ ] - => unique pose proof (H _ _ H') - end. - destruct_head bool; split_andb; Z.ltb_to_lt; split_min_max; omega. + destruct n as [|n]. + { cbv [all_are_bounded_by_bool is_bounded_by_bool is_monotone_on_projections is_true] in *; cbn in *. + rewrite Bool.andb_true_iff, Z.leb_le; split; reflexivity. } + cbv [app tuple all_are_bounded_by_bool fieldwiseb] in *. + induction n as [|n IHn]. + { t_fin. } + { destruct v_bs as [ v_bs [l u] ], v as [vs v]; cbn [lower upper] in *. + cbn [fieldwiseb' fst snd] in Hboundedx. + cbv [is_true] in *. + rewrite Bool.andb_true_iff in Hboundedx. + destruct Hboundedx as [Hboundedx0 Hboundedx1]. + destruct Hmonotone as [Hmonotone0 Hmonotone1]. + specialize (fun x => IHn (f x) (Hmonotone0 _) vs v_bs Hboundedx0). + cbn [app']. + set (Sn := S n) in *. + cbn [n_corners]. + set (f' := fun x => @n_corners Sn (f x)). + lazymatch type of IHn with + | forall x, is_bounded_by_bool (@?B x) (app' _ ?v_bs) = true + => change (forall x, is_bounded_by_bool (B x) (app' (f' x) v_bs) = true) in IHn + end; cbv beta in *. + clearbody f'. + cbn -[Sn] in *. + rewrite pull_union_under_args2. + cbv [is_bounded_by_bool app] in *. + unfold Sn in Hmonotone1. + setoid_rewrite Bool.andb_true_iff in IHn. + rewrite ?Bool.andb_true_iff in *. + setoid_rewrite Z.leb_le in IHn. + rewrite !Z.leb_le in *. + specialize (Hmonotone1 vs). + destruct Hmonotone1 as [? Hmonotone1]. + clear -IHn Hboundedx1 Hmonotone1. + cbn [lower upper] in *. + destruct_head'_bool. + all: split; etransitivity; [ | eapply Hmonotone1, Hboundedx1 | eapply Hmonotone1, Hboundedx1 | ]. + all: first [ etransitivity; [ eapply IHn | ] | etransitivity; [ | eapply IHn ] ]. + all: clear; t_fin. } 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). + Lemma monotone_n_corners_and_zero_genb + n f + (Hmonotone : @is_piecewise_monotone_on_projections n f) + v v_bs + (Hboundedx : @all_are_bounded_by_bool n v v_bs) + : is_bounded_by_bool (app f v) (app (n_corners_and_zero f) v_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. + destruct n as [|n]. + { cbv [all_are_bounded_by_bool is_bounded_by_bool is_piecewise_monotone_on_projections is_true] in *; cbn in *. + rewrite Bool.andb_true_iff, Z.leb_le; split; reflexivity. } + cbv [app tuple all_are_bounded_by_bool fieldwiseb] in *. + induction n as [|n IHn]. + { t_fin_pos. } + { destruct v_bs as [ v_bs [l u] ], v as [vs v]; cbn [lower upper] in *. + cbn [fieldwiseb' fst snd] in Hboundedx. + cbv [is_true] in *. + rewrite Bool.andb_true_iff in Hboundedx. + destruct Hboundedx as [Hboundedx0 Hboundedx1]. + destruct Hmonotone as [Hmonotone0 [Hmonotone1 Hmonotone2] ]. + specialize (fun f pf => IHn f pf vs v_bs Hboundedx0). + specialize (fun x => IHn (f x) (Hmonotone0 _)). + cbn [app']. + set (Sn := S n) in *. + cbn [n_corners_and_zero]. + set (f' := fun x => @n_corners_and_zero Sn (f x)). + lazymatch type of IHn with + | forall x, is_bounded_by_bool (@?B x) (app' _ ?v_bs) = true + => change (forall x, is_bounded_by_bool (B x) (app' (f' x) v_bs) = true) in IHn + end; cbv beta in *. + clearbody f'. + cbn -[Sn] in *. + cbv [is_bounded_by_bool app] in *. + unfold Sn in Hmonotone1, Hmonotone2. + setoid_rewrite Bool.andb_true_iff in IHn. + rewrite ?Bool.andb_true_iff in *. + setoid_rewrite Z.leb_le in IHn. + rewrite !Z.leb_le in *. + specialize (Hmonotone1 vs). + specialize (Hmonotone2 vs). + destruct Hmonotone1 as [? Hmonotone1]. + destruct Hmonotone2 as [? Hmonotone2]. + clear -IHn Hboundedx1 Hmonotone1 Hmonotone2. + cbn [lower upper] in *. + destruct l as [|l|l], u as [|u|u], v as [|v|v]. + all: try (exfalso; clear -Hboundedx1; lia). + all: cbn -[Sn] in *. + all: rewrite !pull_union_under_args2. + all: cbv [union]; cbn [lower upper]. + all: repeat match goal with + | [ H : context[Zpos ?p <= Zpos ?q] |- _ ] + => unique assert (Pos.le p q) by lia + | [ H : context[Zneg ?p <= Zneg ?q] |- _ ] + => unique assert (Pos.le q p) by lia + end. + all: destruct_head'_bool. + all: first [ split; etransitivity; + [ | first [ eapply Hmonotone1 | eapply Hmonotone2 ]; + first [ eassumption | eapply Pos.le_1_l ] + | first [ eapply Hmonotone1 | eapply Hmonotone2 ]; + first [ eassumption | eapply Pos.le_1_l ] | ] + | split ]. + all: first [ etransitivity; [ eapply IHn | ] | etransitivity; [ | eapply IHn ] ]. + all: fast_split_min_max. + all: auto using Z.le_refl. + all: repeat t_fin_common_step. } 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. + exact (@monotone_n_corners_genb 1 f (ltac:(repeat split; auto)) x x_bs Hboundedx). Qed. - Lemma monotone_two_corners_genb + Lemma monotone_two_corners_and_zero_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) + (Hmonotonep : exists b, Proper (Rp b ==> Z.le) (fun x => f (Zpos x))) + (Hmonotonen : exists b, Proper (Rp b ==> Z.le) (fun x => f (Zneg x))) 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) + : is_tighter_than_bool (constant (f x)) (two_corners_and_zero f x_bs). 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. + unshelve eapply (@monotone_n_corners_and_zero_genb 1 f _ x x_bs Hboundedx). + repeat split; auto. Qed. - Lemma monotone_two_corners_gen + Lemma monotoneb_two_corners_gen (f : Z -> Z) (Hmonotone : Proper (Z.le ==> Z.le) f \/ Proper (Basics.flip Z.le ==> Z.le) f) x_bs x - (Hboundedx : ZRange.is_bounded_by' None x_bs x) - : ZRange.is_bounded_by' None (ZRange.two_corners f x_bs) (f x). + (Hboundedx : ZRange.is_bounded_by_bool x x_bs = true) + : ZRange.is_bounded_by_bool (f x) (ZRange.two_corners f x_bs) = true. Proof. - eapply monotone_two_corners_genb; auto. - destruct Hmonotone; [ exists true | exists false ]; assumption. + apply (fun pf => monotone_two_corners_genb' f pf _ _ Hboundedx). + rewrite Bool.ex_bool_iff_or; auto. Qed. - Lemma monotone_two_corners - (b : bool) + + Lemma monotoneb_two_corners_and_zero_gen (f : Z -> Z) - (R := if b then Z.le else Basics.flip Z.le) - (Hmonotone : Proper (R ==> Z.le) f) + (Hmonotonep : Proper (Pos.le ==> Z.le) (fun x => f (Zpos x)) \/ Proper (Basics.flip Pos.le ==> Z.le) (fun x => f (Zpos x))) + (Hmonotonen : Proper (Pos.le ==> Z.le) (fun x => f (Zneg x)) \/ Proper (Basics.flip Pos.le ==> Z.le) (fun x => f (Zneg x))) x_bs x - (Hboundedx : ZRange.is_bounded_by' None x_bs x) - : ZRange.is_bounded_by' None (ZRange.two_corners f x_bs) (f x). + (Hboundedx : ZRange.is_bounded_by_bool x x_bs = true) + : ZRange.is_bounded_by_bool (f x) (ZRange.two_corners_and_zero f x_bs) = true. Proof. - apply monotone_two_corners_genb; auto; subst R; - exists b. - intros ???; apply Hmonotone; auto. + apply (fun pf1 pf2 => monotone_two_corners_and_zero_genb' f pf1 pf2 _ _ Hboundedx). + all: rewrite Bool.ex_bool_iff_or; auto. Qed. - (* + Local Ltac t_fill := + intros; rewrite ?Bool.ex_bool_iff_or; auto; + cbn in *; cbv [is_true] in *; rewrite ?Bool.andb_true_iff; intuition eauto. + + Local Ltac t_red := + cbv [eight_corners_and_zero four_corners_and_zero two_corners_and_zero n_corners_and_zero apply_to_split_range apply_to_split_range_under_args apply_to_each_split_range apply_to_each_split_range_under_args under_args2 apply_to_range apply_to_range_under_args]. + + Lemma two_corners_and_zero_eq f x + : two_corners_and_zero f x = @n_corners_and_zero 1 f x. + Proof. reflexivity. 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)) + (Hmonotone1 : forall x, exists b, Proper (R b ==> Z.le) (fun y => f x y)) (Hmonotone2 : forall y, exists b, Proper (R b ==> Z.le) (fun x => f x y)) - x_bs y_bs x y + x x_bs y y_bs (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]. + apply (fun pf => @monotone_n_corners_genb 2 f pf (y, x) (y_bs, x_bs)). + all: t_fill. + Qed. - Qed.*) + Lemma four_corners_and_zero_eq f x y + : four_corners_and_zero f x y = @n_corners_and_zero 2 f x y. + Proof. + set (n:=1%nat). + cbv [four_corners_and_zero]. + cbn [n_corners_and_zero]. + generalize (fun x => two_corners_and_zero_eq (f x)). + subst n. + generalize (@two_corners_and_zero) (@n_corners_and_zero 1). + t_red. + break_innermost_match; intros ?? H; rewrite ?H; reflexivity. + Qed. - Lemma monotone_four_corners_genb + Lemma monotone_four_corners_and_zero_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 : ZRange.is_bounded_by' None x_bs x) - (Hboundedy : ZRange.is_bounded_by' None y_bs y) - : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y). + (Hmonotone1p : forall x, exists b, Proper (Rp b ==> Z.le) (fun y => f x (Zpos y))) + (Hmonotone1n : forall x, exists b, Proper (Rp b ==> Z.le) (fun y => f x (Zneg y))) + (Hmonotone2p : forall y, exists b, Proper (Rp b ==> Z.le) (fun x => f (Zpos x) y)) + (Hmonotone2n : forall y, exists b, Proper (Rp b ==> Z.le) (fun x => f (Zneg x) y)) + x x_bs y y_bs + (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_and_zero f x_bs y_bs). Proof. - destruct x_bs as [lx ux]. - cbn [ZRange.four_corners lower upper]. - pose proof (monotone_two_corners_genb (f lx) (Hmonotone1 _) _ _ Hboundedy) as Hmono_fl. - pose proof (monotone_two_corners_genb (f ux) (Hmonotone1 _) _ _ Hboundedy) as Hmono_fu. - repeat match goal with - | [ |- context[ZRange.two_corners ?x ?y] ] - => let l := fresh "lf" in - let u := fresh "uf" in - generalize dependent (ZRange.two_corners x y); intros [l u]; intros - end. - unfold ZRange.is_bounded_by', union in *; simpl in *; split; trivial. - destruct_head'_and; destruct_head' True. - pose proof (Hmonotone2 y). - destruct_head'_ex. - repeat match goal with - | [ H : Proper (R ?b ==> Z.le) (f _) |- _ ] - => unique assert (R b (if b then ly else y) (if b then y else ly) - /\ R b (if b then y else uy) (if b then uy else y)) - by (unfold R, Basics.flip; destruct b; omega) - | [ H : Proper (R ?b ==> Z.le) (fun x => f x _) |- _ ] - => 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) - end. - destruct_head' and. - repeat match goal with - | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ] - => unique pose proof (H _ _ H') - end; cbv beta in *. - 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. + rewrite four_corners_and_zero_eq. + exact (@monotone_n_corners_and_zero_genb 2 f ltac:(t_fill) (y, x) (y_bs, x_bs) ltac:(t_fill)). Qed. - Lemma monotone_four_corners_gen + Lemma monotoneb_four_corners_gen (f : Z -> Z -> Z) - (Hmonotone1 : forall x, Proper (Z.le ==> Z.le) (f x) \/ Proper (Basics.flip Z.le ==> Z.le) (f x)) - (Hmonotone2 : forall y, Proper (Z.le ==> Z.le) (fun x => f x y) \/ Proper (Basics.flip Z.le ==> Z.le) (fun x => f x y)) - x_bs y_bs x y - (Hboundedx : ZRange.is_bounded_by' None x_bs x) - (Hboundedy : ZRange.is_bounded_by' None y_bs y) - : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y). + (Hmonotone1 : forall x, Proper (R true ==> Z.le) (fun y => f x y) \/ Proper (R false ==> Z.le) (fun y => f x y)) + (Hmonotone2 : forall y, Proper (R true ==> Z.le) (fun x => f x y) \/ Proper (R false ==> Z.le) (fun x => f x y)) + x x_bs y y_bs + (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. - eapply monotone_four_corners_genb; auto. - { intro x'; destruct (Hmonotone1 x'); [ exists true | exists false ]; assumption. } - { intro x'; destruct (Hmonotone2 x'); [ exists true | exists false ]; assumption. } + apply monotone_four_corners_genb'; t_fill. Qed. - Lemma monotone_four_corners - (b1 b2 : bool) + + Lemma monotoneb_four_corners_and_zero_gen (f : Z -> Z -> Z) - (R1 := if b1 then Z.le else Basics.flip Z.le) (R2 := if b2 then Z.le else Basics.flip Z.le) - (Hmonotone : Proper (R1 ==> R2 ==> Z.le) f) - x_bs y_bs x y - (Hboundedx : ZRange.is_bounded_by' None x_bs x) - (Hboundedy : ZRange.is_bounded_by' None y_bs y) - : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y). + (Hmonotone1p : forall x, Proper (Rp true ==> Z.le) (fun y => f x (Zpos y)) \/ Proper (Rp false ==> Z.le) (fun y => f x (Zpos y))) + (Hmonotone1n : forall x, Proper (Rp true ==> Z.le) (fun y => f x (Zneg y)) \/ Proper (Rp false ==> Z.le) (fun y => f x (Zneg y))) + (Hmonotone2p : forall y, Proper (Rp true ==> Z.le) (fun x => f (Zpos x) y) \/ Proper (Rp false ==> Z.le) (fun x => f (Zpos x) y)) + (Hmonotone2n : forall y, Proper (Rp true ==> Z.le) (fun x => f (Zneg x) y) \/ Proper (Rp false ==> Z.le) (fun x => f (Zneg x) y)) + x x_bs y y_bs + (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_and_zero f x_bs y_bs). Proof. - apply monotone_four_corners_genb; auto; intro x'; subst R1 R2; - [ exists b2 | exists b1 ]; - [ eapply (Hmonotone x' x'); destruct b1; reflexivity - | intros ???; apply Hmonotone; auto; destruct b2; reflexivity ]. + apply monotone_four_corners_and_zero_genb'; t_fill. Qed. - Lemma monotone_eight_corners_genb + + Lemma monotone_eight_corners_genb' (f : Z -> Z -> Z -> Z) - (R := fun b : bool => if b then Z.le else Basics.flip Z.le) - (Hmonotone1 : forall x y, exists b, Proper (R b ==> Z.le) (f x y)) + (Hmonotone1 : forall x y, exists b, Proper (R b ==> Z.le) (fun z => f x y z)) (Hmonotone2 : forall x z, exists b, Proper (R b ==> Z.le) (fun y => f x y z)) (Hmonotone3 : forall y z, exists b, Proper (R b ==> 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). + x x_bs y y_bs z z_bs + (Hboundedx : is_bounded_by_bool x x_bs) + (Hboundedy : is_bounded_by_bool y y_bs) + (Hboundedz : is_bounded_by_bool z z_bs) + : is_tighter_than_bool (constant (f x y z)) (eight_corners f x_bs y_bs z_bs). + Proof. + apply (fun pf => @monotone_n_corners_genb 3 f pf (z, y, x) (z_bs, y_bs, x_bs)). + all: t_fill. + Qed. + + Lemma eight_corners_and_zero_eq f x y z + : eight_corners_and_zero f x y z = @n_corners_and_zero 3 f x y z. Proof. - destruct x_bs as [lx ux]. - unfold ZRange.eight_corners; cbn [lower upper]. - pose proof (monotone_four_corners_genb (f lx) (Hmonotone1 _) (Hmonotone2 _) _ _ _ _ Hboundedy Hboundedz) as Hmono_fl. - pose proof (monotone_four_corners_genb (f ux) (Hmonotone1 _) (Hmonotone2 _) _ _ _ _ Hboundedy Hboundedz) as Hmono_fu. - repeat match goal with - | [ |- context[ZRange.four_corners ?x ?y ?z] ] - => let l := fresh "lf" in - let u := fresh "uf" in - generalize dependent (ZRange.four_corners x y z); intros [l u]; intros - end. - unfold ZRange.is_bounded_by' in *; simpl in *; split; trivial. - destruct_head'_and; destruct_head' True. - pose proof (Hmonotone3 y z). - destruct_head'_ex. - repeat match goal with - | [ H : Proper (R ?b ==> Z.le) (f _ _) |- _ ] - => unique assert (R b (if b then lz else z) (if b then z else lz) - /\ R b (if b then z else uz) (if b then uz else z)) - by (unfold R, Basics.flip; destruct b; omega) - | [ H : Proper (R ?b ==> Z.le) (fun y' => f _ y' _) |- _ ] - => unique assert (R b (if b then ly else y) (if b then y else ly) - /\ R b (if b then y else uy) (if b then uy else y)) - by (unfold R, Basics.flip; destruct b; omega) - | [ H : Proper (R ?b ==> Z.le) (fun x' => f x' _ _) |- _ ] - => 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) - end. - destruct_head' and. - repeat match goal with - | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ] - => unique pose proof (H _ _ H') - end. - 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. + set (n:=2%nat). + cbv [eight_corners_and_zero]. + cbn [n_corners_and_zero]. + generalize (fun x => four_corners_and_zero_eq (f x)). + subst n. + generalize (@four_corners_and_zero) (@n_corners_and_zero 2). + t_red. + break_innermost_match; intros ?? H; rewrite ?H; reflexivity. Qed. - Lemma monotone_eight_corners - (b1 b2 b3 : bool) + + Lemma monotone_eight_corners_and_zero_genb' (f : Z -> Z -> Z -> Z) - (R1 := if b1 then Z.le else Basics.flip Z.le) - (R2 := if b2 then Z.le else Basics.flip Z.le) - (R3 := if b3 then Z.le else Basics.flip Z.le) - (Hmonotone : Proper (R1 ==> R2 ==> R3 ==> Z.le) f) - 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). + (Hmonotone1p : forall x y, exists b, Proper (Rp b ==> Z.le) (fun z => f x y (Zpos z))) + (Hmonotone1n : forall x y, exists b, Proper (Rp b ==> Z.le) (fun z => f x y (Zneg z))) + (Hmonotone2p : forall x z, exists b, Proper (Rp b ==> Z.le) (fun y => f x (Zpos y) z)) + (Hmonotone2n : forall x z, exists b, Proper (Rp b ==> Z.le) (fun y => f x (Zneg y) z)) + (Hmonotone3p : forall y z, exists b, Proper (Rp b ==> Z.le) (fun x => f (Zpos x) y z)) + (Hmonotone3n : forall y z, exists b, Proper (Rp b ==> Z.le) (fun x => f (Zneg x) y z)) + x x_bs y y_bs z z_bs + (Hboundedx : is_bounded_by_bool x x_bs) + (Hboundedy : is_bounded_by_bool y y_bs) + (Hboundedz : is_bounded_by_bool z z_bs) + : is_tighter_than_bool (constant (f x y z)) (eight_corners_and_zero f x_bs y_bs z_bs). Proof. - apply monotone_eight_corners_genb; auto; intro x'; subst R1 R2 R3; - [ exists b3 | exists b2 | exists b1 ]; - intros ???; apply Hmonotone; break_innermost_match; try reflexivity; trivial. + rewrite eight_corners_and_zero_eq. + exact (@monotone_n_corners_and_zero_genb 3 f ltac:(t_fill) (z, y, x) (z_bs, y_bs, x_bs) ltac:(t_fill)). Qed. - Lemma monotonify2 (f : Z -> Z -> Z) (upper : Z -> Z -> Z) - (Hbounded : forall a b, Z.abs (f a b) <= upper (Z.abs a) (Z.abs b)) - (Hupper_monotone : Proper (Z.le ==> Z.le ==> Z.le) upper) - {xb yb x y} - (Hboundedx : ZRange.is_bounded_by' None xb x) - (Hboundedy : ZRange.is_bounded_by' None yb y) - (abs_x := ZRange.upper (ZRange.abs xb)) - (abs_y := ZRange.upper (ZRange.abs yb)) - : ZRange.is_bounded_by' - None - {| ZRange.lower := -upper abs_x abs_y; - ZRange.upper := upper abs_x abs_y |} - (f x y). + Lemma monotoneb_eight_corners_gen + (f : Z -> Z -> Z -> Z) + (Hmonotone1 : forall x y, Proper (R true ==> Z.le) (fun z => f x y z) \/ Proper (R false ==> Z.le) (fun z => f x y z)) + (Hmonotone2 : forall x z, Proper (R true ==> Z.le) (fun y => f x y z) \/ Proper (R false ==> Z.le) (fun y => f x y z)) + (Hmonotone3 : forall y z, Proper (R true ==> Z.le) (fun x => f x y z) \/ Proper (R false ==> Z.le) (fun x => f x y z)) + x x_bs y y_bs z z_bs + (Hboundedx : is_bounded_by_bool x x_bs) + (Hboundedy : is_bounded_by_bool y y_bs) + (Hboundedz : is_bounded_by_bool z z_bs) + : is_tighter_than_bool (constant (f x y z)) (eight_corners f x_bs y_bs z_bs). Proof. - split; [ | exact I ]; subst abs_x abs_y; simpl. - apply Z.abs_le. - destruct Hboundedx as [Hx _], Hboundedy as [Hy _]. - etransitivity; [ apply Hbounded | ]. - apply Hupper_monotone; - unfold ZRange.abs; - repeat (apply Z.max_case_strong || apply Zabs_ind); omega. + apply monotone_eight_corners_genb'; t_fill. Qed. + + Lemma monotoneb_eight_corners_and_zero_gen + (f : Z -> Z -> Z -> Z) + (Hmonotone1p : forall x y, Proper (Rp true ==> Z.le) (fun z => f x y (Zpos z)) \/ Proper (Rp false ==> Z.le) (fun z => f x y (Zpos z))) + (Hmonotone1n : forall x y, Proper (Rp true ==> Z.le) (fun z => f x y (Zneg z)) \/ Proper (Rp false ==> Z.le) (fun z => f x y (Zneg z))) + (Hmonotone2p : forall x z, Proper (Rp true ==> Z.le) (fun y => f x (Zpos y) z) \/ Proper (Rp false ==> Z.le) (fun y => f x (Zpos y) z)) + (Hmonotone2n : forall x z, Proper (Rp true ==> Z.le) (fun y => f x (Zneg y) z) \/ Proper (Rp false ==> Z.le) (fun y => f x (Zneg y) z)) + (Hmonotone3p : forall y z, Proper (Rp true ==> Z.le) (fun x => f (Zpos x) y z) \/ Proper (Rp false ==> Z.le) (fun x => f (Zpos x) y z)) + (Hmonotone3n : forall y z, Proper (Rp true ==> Z.le) (fun x => f (Zneg x) y z) \/ Proper (Rp false ==> Z.le) (fun x => f (Zneg x) y z)) + x x_bs y y_bs z z_bs + (Hboundedx : is_bounded_by_bool x x_bs) + (Hboundedy : is_bounded_by_bool y y_bs) + (Hboundedz : is_bounded_by_bool z z_bs) + : is_tighter_than_bool (constant (f x y z)) (eight_corners_and_zero f x_bs y_bs z_bs). + Proof. + apply monotone_eight_corners_and_zero_genb'; t_fill. + Qed. + + Section legacy. + (** TODO: When we move to the new pipeline, remove this *) + Lemma monotone_two_corners_genb + (f : Z -> Z) + (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 + (f : Z -> Z) + (Hmonotone : Proper (Z.le ==> Z.le) f \/ Proper (Basics.flip Z.le ==> Z.le) f) + x_bs x + (Hboundedx : ZRange.is_bounded_by' None x_bs x) + : ZRange.is_bounded_by' None (ZRange.two_corners f x_bs) (f x). + Proof. + eapply monotone_two_corners_genb; auto. + destruct Hmonotone; [ exists true | exists false ]; assumption. + Qed. + + Lemma monotone_two_corners + (b : bool) + (f : Z -> Z) + (Hmonotone : Proper (R b ==> Z.le) f) + x_bs x + (Hboundedx : ZRange.is_bounded_by' None x_bs x) + : ZRange.is_bounded_by' None (ZRange.two_corners f x_bs) (f x). + Proof. + apply monotone_two_corners_genb; auto; + exists b. + intros ???; apply Hmonotone; auto. + Qed. + + Lemma monotone_four_corners_genb + (f : Z -> Z -> Z) + (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 : ZRange.is_bounded_by' None x_bs x) + (Hboundedy : ZRange.is_bounded_by' None y_bs y) + : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y). + Proof. + destruct x_bs as [lx ux]. + pose proof (monotone_two_corners_genb (f lx) (Hmonotone1 _) _ _ Hboundedy) as Hmono_fl. + pose proof (monotone_two_corners_genb (f ux) (Hmonotone1 _) _ _ Hboundedy) as Hmono_fu. + unfold ZRange.is_bounded_by', union in *; simpl in *; split; trivial. + destruct_head'_and; destruct_head' True. + pose proof (Hmonotone2 y). + destruct_head'_ex. + repeat match goal with + | [ H : Proper (R ?b ==> Z.le) (f _) |- _ ] + => unique assert (R b (if b then ly else y) (if b then y else ly) + /\ R b (if b then y else uy) (if b then uy else y)) + by (unfold Basics.flip; destruct b; omega) + | [ H : Proper (R ?b ==> Z.le) (fun x => f x _) |- _ ] + => 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 Basics.flip; destruct b; omega) + end. + destruct_head' and. + repeat match goal with + | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ] + => unique pose proof (H _ _ H') + end; cbv beta in *. + 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 + (f : Z -> Z -> Z) + (Hmonotone1 : forall x, Proper (Z.le ==> Z.le) (f x) \/ Proper (Basics.flip Z.le ==> Z.le) (f x)) + (Hmonotone2 : forall y, Proper (Z.le ==> Z.le) (fun x => f x y) \/ Proper (Basics.flip Z.le ==> Z.le) (fun x => f x y)) + x_bs y_bs x y + (Hboundedx : ZRange.is_bounded_by' None x_bs x) + (Hboundedy : ZRange.is_bounded_by' None y_bs y) + : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y). + Proof. + eapply monotone_four_corners_genb; auto. + { intro x'; destruct (Hmonotone1 x'); [ exists true | exists false ]; assumption. } + { intro x'; destruct (Hmonotone2 x'); [ exists true | exists false ]; assumption. } + Qed. + Lemma monotone_four_corners + (b1 b2 : bool) + (f : Z -> Z -> Z) + (R1 := if b1 then Z.le else Basics.flip Z.le) (R2 := if b2 then Z.le else Basics.flip Z.le) + (Hmonotone : Proper (R1 ==> R2 ==> Z.le) f) + x_bs y_bs x y + (Hboundedx : ZRange.is_bounded_by' None x_bs x) + (Hboundedy : ZRange.is_bounded_by' None y_bs y) + : ZRange.is_bounded_by' None (ZRange.four_corners f x_bs y_bs) (f x y). + Proof. + apply monotone_four_corners_genb; auto; intro x'; subst R1 R2; + [ exists b2 | exists b1 ]; + [ eapply (Hmonotone x' x'); destruct b1; reflexivity + | intros ???; apply Hmonotone; auto; destruct b2; reflexivity ]. + Qed. + + Lemma monotone_eight_corners_genb + (f : Z -> Z -> Z -> Z) + (Hmonotone1 : forall x y, exists b, Proper (R b ==> Z.le) (f x y)) + (Hmonotone2 : forall x z, exists b, Proper (R b ==> Z.le) (fun y => f x y z)) + (Hmonotone3 : forall y z, exists b, Proper (R b ==> 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. + destruct x_bs as [lx ux]. + unfold ZRange.eight_corners; cbn [lower upper]. + pose proof (monotone_four_corners_genb (f lx) (Hmonotone1 _) (Hmonotone2 _) _ _ _ _ Hboundedy Hboundedz) as Hmono_fl. + pose proof (monotone_four_corners_genb (f ux) (Hmonotone1 _) (Hmonotone2 _) _ _ _ _ Hboundedy Hboundedz) as Hmono_fu. + repeat match goal with + | [ |- context[ZRange.four_corners ?x ?y ?z] ] + => let l := fresh "lf" in + let u := fresh "uf" in + generalize dependent (ZRange.four_corners x y z); intros [l u]; intros + end. + unfold ZRange.is_bounded_by' in *; simpl in *; split; trivial. + destruct_head'_and; destruct_head' True. + pose proof (Hmonotone3 y z). + destruct_head'_ex. + repeat match goal with + | [ H : Proper (R ?b ==> Z.le) (f _ _) |- _ ] + => unique assert (R b (if b then lz else z) (if b then z else lz) + /\ R b (if b then z else uz) (if b then uz else z)) + by (unfold Basics.flip; destruct b; omega) + | [ H : Proper (R ?b ==> Z.le) (fun y' => f _ y' _) |- _ ] + => unique assert (R b (if b then ly else y) (if b then y else ly) + /\ R b (if b then y else uy) (if b then uy else y)) + by (unfold Basics.flip; destruct b; omega) + | [ H : Proper (R ?b ==> Z.le) (fun x' => f x' _ _) |- _ ] + => 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 Basics.flip; destruct b; omega) + end. + destruct_head' and. + repeat match goal with + | [ H : Proper (R ?b ==> Z.le) _, H' : R ?b _ _ |- _ ] + => unique pose proof (H _ _ H') + end. + 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) + (f : Z -> Z -> Z -> Z) + (R1 := if b1 then Z.le else Basics.flip Z.le) + (R2 := if b2 then Z.le else Basics.flip Z.le) + (R3 := if b3 then Z.le else Basics.flip Z.le) + (Hmonotone : Proper (R1 ==> R2 ==> R3 ==> Z.le) f) + 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. + apply monotone_eight_corners_genb; auto; intro x'; subst R1 R2 R3; + [ exists b3 | exists b2 | exists b1 ]; + intros ???; apply Hmonotone; break_innermost_match; try reflexivity; trivial. + Qed. + + Lemma monotonify2 (f : Z -> Z -> Z) (upper : Z -> Z -> Z) + (Hbounded : forall a b, Z.abs (f a b) <= upper (Z.abs a) (Z.abs b)) + (Hupper_monotone : Proper (Z.le ==> Z.le ==> Z.le) upper) + {xb yb x y} + (Hboundedx : ZRange.is_bounded_by' None xb x) + (Hboundedy : ZRange.is_bounded_by' None yb y) + (abs_x := ZRange.upper (ZRange.abs xb)) + (abs_y := ZRange.upper (ZRange.abs yb)) + : ZRange.is_bounded_by' + None + {| ZRange.lower := -upper abs_x abs_y; + ZRange.upper := upper abs_x abs_y |} + (f x y). + Proof. + split; [ | exact I ]; subst abs_x abs_y; simpl. + apply Z.abs_le. + destruct Hboundedx as [Hx _], Hboundedy as [Hy _]. + etransitivity; [ apply Hbounded | ]. + apply Hupper_monotone; + unfold ZRange.abs; + repeat (apply Z.max_case_strong || apply Zabs_ind); omega. + Qed. + End legacy. End ZRange. diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index 32af62ee5..c8db4adf0 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -72,6 +72,55 @@ Module ZRange. Definition constant (v : Z) : zrange := r[v ~> v]. + Fixpoint nary_T (A B : Type) (n : nat) := + match n with + | O => B + | S n => A -> nary_T A B n + end. + + Fixpoint under_args {A B B'} (F : B -> B') {n : nat} : nary_T A B n -> nary_T A B' n + := match n with + | O => F + | S n => fun f x => @under_args A B B' F n (f x) + end. + + Fixpoint under_args2 {A B B' B''} (F : B -> B' -> B'') {n : nat} : nary_T A B n -> nary_T A B' n -> nary_T A B'' n + := match n with + | O => F + | S n => fun f g x => @under_args2 A B B' B'' F n (f x) (g x) + end. + + Definition apply_to_range_under_args {A} {n} (f : Z -> nary_T A zrange n) (v : zrange) : nary_T A zrange n + := let (l, u) := eta v in + under_args2 union (f l) (f u). + + Definition apply_to_split_range_under_args {A} {n} (f : zrange -> nary_T A zrange n) (v : zrange) : nary_T A zrange n + := match split_range_at_0 v with + | (Some n, Some z, Some p) => under_args2 union (under_args2 union (f n) (f p)) (f z) + | (Some v1, Some v2, None) | (Some v1, None, Some v2) | (None, Some v1, Some v2) => under_args2 union (f v1) (f v2) + | (Some v, None, None) | (None, Some v, None) | (None, None, Some v) => f v + | (None, None, None) => f v + end. + + Definition apply_to_each_split_range_under_args {A} {n} (f : BinInt.Z -> nary_T A zrange n) (v : zrange) : nary_T A zrange n + := apply_to_split_range_under_args (apply_to_range_under_args f) v. + + Fixpoint n_corners {n : nat} : nary_T Z Z n -> nary_T zrange zrange n + := match n with + | O => constant + | S n + => fun (f : Z -> nary_T Z Z n) (v : zrange) + => apply_to_range_under_args (fun x => n_corners (f x)) v + end. + + Fixpoint n_corners_and_zero {n : nat} : nary_T Z Z n -> nary_T zrange zrange n + := match n with + | O => constant + | S n + => fun (f : Z -> nary_T Z Z n) (v : zrange) + => apply_to_each_split_range_under_args (fun x => n_corners_and_zero (f x)) v + end. + 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 -- cgit v1.2.3