diff options
-rw-r--r-- | _CoqProject | 3 | ||||
-rw-r--r-- | src/Compilers/Z/Bounds/Interpretation.v | 28 | ||||
-rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v | 252 | ||||
-rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v | 44 | ||||
-rw-r--r-- | src/Util/ZRange/BasicLemmas.v | 37 | ||||
-rw-r--r-- | src/Util/ZRange/CornersMonotoneBounds.v | 248 | ||||
-rw-r--r-- | src/Util/ZRange/Operations.v | 30 | ||||
-rw-r--r-- | src/Util/ZUtil/Tactics/SplitMinMax.v | 42 |
8 files changed, 377 insertions, 307 deletions
diff --git a/_CoqProject b/_CoqProject index fa0dcff31..41790980e 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6543,6 +6543,8 @@ src/Util/Tactics/UnfoldArg.v src/Util/Tactics/UnifyAbstractReflexivity.v src/Util/Tactics/UniquePose.v src/Util/Tactics/VM.v +src/Util/ZRange/BasicLemmas.v +src/Util/ZRange/CornersMonotoneBounds.v src/Util/ZRange/Operations.v src/Util/ZUtil/AddGetCarry.v src/Util/ZUtil/CPS.v @@ -6583,6 +6585,7 @@ src/Util/ZUtil/Tactics/PullPush.v src/Util/ZUtil/Tactics/ReplaceNegWithPos.v src/Util/ZUtil/Tactics/RewriteModSmall.v src/Util/ZUtil/Tactics/SimplifyFractionsLe.v +src/Util/ZUtil/Tactics/SplitMinMax.v src/Util/ZUtil/Tactics/ZeroBounds.v src/Util/ZUtil/Tactics/Ztestbit.v src/Util/ZUtil/Tactics/PullPush/Modulo.v diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v index 11539d014..e37b64a09 100644 --- a/src/Compilers/Z/Bounds/Interpretation.v +++ b/src/Compilers/Z/Bounds/Interpretation.v @@ -6,6 +6,7 @@ Require Import Crypto.Compilers.Relations. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.Tactics.DestructHead. Export Compilers.Syntax.Notations. @@ -26,31 +27,12 @@ Module Import Bounds. Section ops. (** Generic helper definitions *) - Definition two_corners (f : Z -> Z) : t -> t - := fun x - => let (lx, ux) := x in - {| lower := Z.min (f lx) (f ux); - upper := Z.max (f lx) (f ux) |}. - Definition four_corners (f : Z -> Z -> Z) : t -> t -> t - := fun x y - => let (lx, ux) := x in - let (lfl, ufl) := two_corners (f lx) y in - let (lfu, ufu) := two_corners (f ux) y in - {| lower := Z.min lfl lfu; - upper := Z.max ufl ufu |}. - Definition eight_corners (f : Z -> Z -> Z -> Z) : t -> t -> t -> t - := fun x y z - => let (lx, ux) := x in - let (lfl, ufl) := four_corners (f lx) y z in - let (lfu, ufu) := four_corners (f ux) y z in - {| lower := Z.min lfl lfu; - upper := Z.max ufl ufu |}. Definition t_map1 (f : Z -> Z) : t -> t - := fun x => two_corners f x. + := fun x => ZRange.two_corners f x. Definition t_map2 (f : Z -> Z -> Z) : t -> t -> t - := fun x y => four_corners f x y. + := fun x y => ZRange.four_corners f x y. Definition t_map3 (f : Z -> Z -> Z -> Z) : t -> t -> t -> t - := fun x y z => eight_corners f x y z. + := fun x y z => ZRange.eight_corners f x y z. (** Definitions of the actual bounds propogation *) (** Rules for adding new operations: @@ -64,7 +46,7 @@ Module Import Bounds. Definition shl : t -> t -> t := t_map2 Z.shiftl. Definition shr : t -> t -> t := t_map2 Z.shiftr. Definition max_abs_bound (x : t) : Z - := Z.max (Z.abs (lower x)) (Z.abs (upper x)). + := upper (ZRange.abs x). Definition upper_lor_and_bounds (x y : Z) : Z := 2^(1 + Z.log2_up (Z.max x y)). Definition extreme_lor_land_bounds (x y : t) : t diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v index 0c709abe9..ba0582827 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v @@ -7,6 +7,7 @@ Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.Z.Bounds.Interpretation. Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics. Require Import Crypto.Compilers.SmartMap. +Require Import Crypto.Util.ZRange.CornersMonotoneBounds. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ZUtil.Stabilization. Require Import Crypto.Util.ZUtil.MulSplit. @@ -17,6 +18,7 @@ Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax. Local Open Scope Z_scope. @@ -46,230 +48,6 @@ Proof. subst; eauto. 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 (Bounds.two_corners f x_bs) (f x). -Proof. - unfold ZRange.is_bounded_by' in *; split; trivial. - destruct x_bs as [lx ux]; simpl in *. - destruct Hboundedx as [Hboundedx _]. - destruct_head'_ex. - repeat match goal with - | [ H : Proper (R ?b ==> Z.le) f |- _ ] - => 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; split_min_max; omega. -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 (Bounds.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) - (R := if b then Z.le else Basics.flip Z.le) - (Hmonotone : Proper (R ==> Z.le) f) - x_bs x - (Hboundedx : ZRange.is_bounded_by' None x_bs x) - : ZRange.is_bounded_by' None (Bounds.two_corners f x_bs) (f x). -Proof. - apply monotone_two_corners_genb; auto; subst R; - exists b. - 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 : ZRange.is_bounded_by' None x_bs x) - (Hboundedy : ZRange.is_bounded_by' None y_bs y) - : ZRange.is_bounded_by' None (Bounds.four_corners f x_bs y_bs) (f x y). -Proof. - destruct x_bs as [lx ux], y_bs as [ly uy]. - unfold Bounds.four_corners. - 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[Bounds.two_corners ?x ?y] ] - => let l := fresh "lf" in - let u := fresh "uf" in - generalize dependent (Bounds.two_corners x y); intros [l u]; intros - end. - unfold ZRange.is_bounded_by' 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; split_min_max; omega. -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 (Bounds.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 (Bounds.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) - (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)) - (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 (Bounds.eight_corners f x_bs y_bs z_bs) (f x y z). -Proof. - destruct x_bs as [lx ux], y_bs as [ly uy], z_bs as [lz uz]. - unfold Bounds.eight_corners. - 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[Bounds.four_corners ?x ?y ?z] ] - => let l := fresh "lf" in - let u := fresh "uf" in - generalize dependent (Bounds.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; 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 (Bounds.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. } -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 (Bounds.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) - : ZRange.is_bounded_by' - None - {| ZRange.lower := -upper (Bounds.max_abs_bound xb) (Bounds.max_abs_bound yb); - ZRange.upper := upper (Bounds.max_abs_bound xb) (Bounds.max_abs_bound yb) |} - (f x y). -Proof. - split; [ | exact I ]; simpl. - apply Z.abs_le. - destruct Hboundedx as [Hx _], Hboundedy as [Hy _]. - etransitivity; [ apply Hbounded | ]. - apply Hupper_monotone; - unfold Bounds.max_abs_bound; - repeat (apply Z.max_case_strong || apply Zabs_ind); omega. -Qed. - Local Existing Instances Z.log2_up_le_Proper Z.add_le_Proper Z.sub_with_borrow_le_Proper. Lemma land_upper_lor_land_bounds a b : Z.abs (Z.land a b) <= Bounds.upper_lor_and_bounds (Z.abs a) (Z.abs b). @@ -305,7 +83,7 @@ Lemma land_bounds_extreme xb yb x y (Hy : ZRange.is_bounded_by' None yb y) : ZRange.is_bounded_by' None (Bounds.extreme_lor_land_bounds xb yb) (Z.land x y). Proof. - apply monotonify2; auto; + apply ZRange.monotonify2; auto; unfold Bounds.extreme_lor_land_bounds; [ apply land_upper_lor_land_bounds | apply upper_lor_and_bounds_Proper ]. @@ -315,7 +93,7 @@ Lemma lor_bounds_extreme xb yb x y (Hy : ZRange.is_bounded_by' None yb y) : ZRange.is_bounded_by' None (Bounds.extreme_lor_land_bounds xb yb) (Z.lor x y). Proof. - apply monotonify2; auto; + apply ZRange.monotonify2; auto; unfold Bounds.extreme_lor_land_bounds; [ apply lor_upper_lor_land_bounds | apply upper_lor_and_bounds_Proper ]. @@ -341,7 +119,7 @@ Local Ltac apply_is_bounded_by_truncation_bounds := => apply is_bounded_by_truncation_bounds' end. Local Ltac handle_mul := - apply monotone_four_corners_genb; try (split; auto); + apply ZRange.monotone_four_corners_genb; try (split; auto); unfold Basics.flip; let x := fresh "x" in intro x; @@ -383,13 +161,13 @@ Proof. => generalize dependent (interpToZ x); clear x; intros | [ |- _ /\ True ] => split; [ | tauto ] end ]. - { apply (@monotone_four_corners true true _ _); split; auto. } - { apply (@monotone_four_corners true false _ _); split; auto. } + { apply (@ZRange.monotone_four_corners true true _ _); split; auto. } + { apply (@ZRange.monotone_four_corners true false _ _); split; auto. } { handle_mul. } - { apply monotone_four_corners_genb; try (split; auto); + { apply ZRange.monotone_four_corners_genb; try (split; auto); [ eexists; apply Z.shiftl_le_Proper1 | exists true; apply Z.shiftl_le_Proper2 ]. } - { apply monotone_four_corners_genb; try (split; auto); + { apply ZRange.monotone_four_corners_genb; try (split; auto); [ eexists; apply Z.shiftr_le_Proper1 | exists true; apply Z.shiftr_le_Proper2 ]. } { cbv [Bounds.land Bounds.extremization_bounds]; break_innermost_match; @@ -419,14 +197,14 @@ Proof. { apply Z.mod_bound_min_max; auto. } { handle_mul. } { auto with zarith. } - { apply (@monotone_eight_corners true true true _ _ _); split; auto. } - { apply (@monotone_eight_corners true true true _ _ _); split; auto. } + { apply (@ZRange.monotone_eight_corners true true true _ _ _); split; auto. } + { apply (@ZRange.monotone_eight_corners true true true _ _ _); split; auto. } { apply Z.mod_bound_min_max; auto. } - { apply (@monotone_eight_corners true true true _ _ _); split; auto. } + { apply (@ZRange.monotone_eight_corners true true true _ _ _); split; auto. } { auto with zarith. } - { apply (@monotone_eight_corners false true false _ _ _); split; auto. } - { apply (@monotone_eight_corners false true false _ _ _); split; auto. } + { apply (@ZRange.monotone_eight_corners false true false _ _ _); split; auto. } + { apply (@ZRange.monotone_eight_corners false true false _ _ _); split; auto. } { apply Z.mod_bound_min_max; auto. } - { apply (@monotone_eight_corners false true false _ _ _); split; auto. } + { apply (@ZRange.monotone_eight_corners false true false _ _ _); split; auto. } { auto with zarith. } Qed. diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v index 51c105186..71f4b758b 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v @@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Psatz. Require Import Crypto.Compilers.Z.Bounds.Interpretation. Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.Bool. Require Import Crypto.Util.FixedWordSizesEquality. Require Import Crypto.Util.Option. @@ -10,6 +11,7 @@ Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.UniquePose. +Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax. Local Open Scope Z_scope. @@ -54,44 +56,6 @@ Ltac word_arith_t := => clear; pose proof (@wordToZ_range logsz w); autorewrite with push_Zof_nat zsimplify_const in *; try omega end. -Ltac revert_min_max := - repeat match goal with - | [ H : context[Z.min _ _] |- _ ] => revert H - | [ H : context[Z.max _ _] |- _ ] => revert H - end. -Ltac rewrite_min_max_step_fast := - match goal with - | [ H : (?a <= ?b)%Z |- context[Z.max ?a ?b] ] - => rewrite (Z.max_r a b) by assumption - | [ H : (?b <= ?a)%Z |- context[Z.max ?a ?b] ] - => rewrite (Z.max_l a b) by assumption - | [ H : (?a <= ?b)%Z |- context[Z.min ?a ?b] ] - => rewrite (Z.min_l a b) by assumption - | [ H : (?b <= ?a)%Z |- context[Z.min ?a ?b] ] - => rewrite (Z.min_r a b) by assumption - end. -Ltac rewrite_min_max_step := - match goal with - | _ => rewrite_min_max_step_fast - | [ |- context[Z.max ?a ?b] ] - => first [ rewrite (Z.max_l a b) by omega - | rewrite (Z.max_r a b) by omega ] - | [ |- context[Z.min ?a ?b] ] - => first [ rewrite (Z.min_l a b) by omega - | rewrite (Z.min_r a b) by omega ] - end. -Ltac only_split_min_max_step := - match goal with - | _ => revert_min_max; progress repeat apply Z.min_case_strong; intros - | _ => revert_min_max; progress repeat apply Z.max_case_strong; intros - end. -Ltac split_min_max_step := - match goal with - | _ => rewrite_min_max_step - | _ => only_split_min_max_step - end. -Ltac split_min_max := repeat split_min_max_step. - Ltac case_Zvar_nonneg_on x := is_var x; lazymatch type of x with @@ -191,7 +155,7 @@ Ltac handle_shift_neg := Ltac handle_four_corners_step_fast := first [ progress destruct_head Bounds.t - | progress cbv [Bounds.four_corners] in * + | progress cbv [ZRange.four_corners] in * | progress subst | Zarith_t_step | progress split_min_max @@ -202,7 +166,7 @@ Ltac handle_four_corners_step := | remove_binary_operation_le_hyps_step ]. Ltac handle_four_corners := lazymatch goal with - | [ |- (ZRange.lower (Bounds.four_corners _ _ _) <= _ <= _)%Z ] + | [ |- (ZRange.lower (ZRange.four_corners _ _ _) <= _ <= _)%Z ] => idtac end; repeat handle_four_corners_step. diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v new file mode 100644 index 000000000..c5dcaa3d4 --- /dev/null +++ b/src/Util/ZRange/BasicLemmas.v @@ -0,0 +1,37 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZRange.Operations. +Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Tactics.DestructHead. + +Module ZRange. + Import Operations.ZRange. + Local Open Scope zrange_scope. + + Local Notation eta v := r[ lower v ~> upper v ]. + + Local Ltac t := + repeat first [ reflexivity + | progress destruct_head' zrange + | progress cbv -[Z.min Z.max Z.le Z.lt Z.ge Z.gt] + | progress split_min_max + | match goal with + | [ |- _ = _ :> zrange ] => apply f_equal2 + end + | omega + | solve [ auto ] ]. + + + Lemma flip_flip v : flip (flip v) = v. + Proof. destruct v; reflexivity. Qed. + + Lemma normalize_flip v : normalize (flip v) = normalize v. + Proof. t. Qed. + + Lemma normalize_idempotent v : normalize (normalize v) = normalize v. + Proof. t. Qed. + + Definition normalize_or v : normalize v = v \/ normalize v = flip v. + Proof. t. Qed. +End ZRange. diff --git a/src/Util/ZRange/CornersMonotoneBounds.v b/src/Util/ZRange/CornersMonotoneBounds.v new file mode 100644 index 000000000..f41c712ed --- /dev/null +++ b/src/Util/ZRange/CornersMonotoneBounds.v @@ -0,0 +1,248 @@ +Require Import Coq.Classes.Morphisms. +Require Import Coq.ZArith.ZArith. +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.PointedProp. +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.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.UniquePose. +Require Import Crypto.Util.Tactics.SpecializeBy. + +Local Open Scope Z_scope. + +Module ZRange. + Import Operations.ZRange. + Local Arguments is_bounded_by' !_ _ _ / . + + 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. + split; trivial. + destruct x_bs as [lx ux]; simpl in *. + destruct Hboundedx as [Hboundedx _]. + destruct_head'_ex. + repeat match goal with + | [ H : Proper (R ?b ==> Z.le) f |- _ ] + => 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; split_min_max; omega. + 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) + (R := if b then Z.le else Basics.flip Z.le) + (Hmonotone : Proper (R ==> 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; subst R; + exists b. + 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 : 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]. + 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; split_min_max; omega. + 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) + (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)) + (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 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; 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. } + 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 ZRange. diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index 7d9b24c40..c73b991e8 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -7,21 +7,38 @@ Module ZRange. Local Notation eta v := r[ lower v ~> upper v ]. + Definition flip (v : zrange) : zrange + := r[ upper v ~> lower v ]. + + Definition union (x y : zrange) : zrange + := let (lx, ux) := eta x in + let (ly, uy) := eta y in + r[ Z.min lx ly ~> Z.max ux uy ]. + Definition normalize (v : zrange) : zrange - := r[ Z.min (lower v) (upper v) ~> Z.max (lower v) (upper v) ]. + := r[ Z.min (lower v) (upper v) ~> Z.max (upper v) (lower v) ]. + + Definition normalize' (v : zrange) : zrange + := union v (flip v). + + Lemma normalize'_eq : normalize = normalize'. Proof. reflexivity. Defined. Definition abs (v : zrange) : zrange := let (l, u) := eta v in r[ 0 ~> Z.max (Z.abs l) (Z.abs u) ]. + Definition map (f : Z -> Z) (v : zrange) : zrange + := let (l, u) := eta v in + r[ f l ~> f u ]. + Definition two_corners (f : Z -> Z) (v : zrange) : zrange := let (l, u) := eta v in - r[ Z.min (f l) (f u) ~> Z.max (f l) (f u) ]. + r[ Z.min (f l) (f u) ~> Z.max (f u) (f l) ]. - Definition union (x y : zrange) : zrange - := let (lx, ux) := eta x in - let (ly, uy) := eta y in - r[ Z.min lx ly ~> Z.max ux uy ]. + Definition two_corners' (f : Z -> Z) (v : zrange) : zrange + := normalize' (map f v). + + Lemma two_corners'_eq : two_corners = two_corners'. Proof. reflexivity. Defined. Definition four_corners (f : Z -> Z -> Z) (x y : zrange) : zrange := let (lx, ux) := eta x in @@ -32,5 +49,4 @@ Module ZRange. := let (lx, ux) := eta x in union (four_corners (f lx) y z) (four_corners (f ux) y z). - End ZRange. diff --git a/src/Util/ZUtil/Tactics/SplitMinMax.v b/src/Util/ZUtil/Tactics/SplitMinMax.v new file mode 100644 index 000000000..901cfde88 --- /dev/null +++ b/src/Util/ZUtil/Tactics/SplitMinMax.v @@ -0,0 +1,42 @@ +Require Import Coq.omega.Omega. +Require Import Coq.ZArith.BinInt. + +Ltac rewrite_min_max_side_condition_t := omega. + +Ltac revert_min_max := + repeat match goal with + | [ H : context[Z.min _ _] |- _ ] => revert H + | [ H : context[Z.max _ _] |- _ ] => revert H + end. +Ltac rewrite_min_max_step_fast := + match goal with + | [ H : (?a <= ?b)%Z |- context[Z.max ?a ?b] ] + => rewrite (Z.max_r a b) by assumption + | [ H : (?b <= ?a)%Z |- context[Z.max ?a ?b] ] + => rewrite (Z.max_l a b) by assumption + | [ H : (?a <= ?b)%Z |- context[Z.min ?a ?b] ] + => rewrite (Z.min_l a b) by assumption + | [ H : (?b <= ?a)%Z |- context[Z.min ?a ?b] ] + => rewrite (Z.min_r a b) by assumption + end. +Ltac rewrite_min_max_step := + match goal with + | _ => rewrite_min_max_step_fast + | [ |- context[Z.max ?a ?b] ] + => first [ rewrite (Z.max_l a b) by rewrite_min_max_side_condition_t + | rewrite (Z.max_r a b) by rewrite_min_max_side_condition_t ] + | [ |- context[Z.min ?a ?b] ] + => first [ rewrite (Z.min_l a b) by rewrite_min_max_side_condition_t + | rewrite (Z.min_r a b) by rewrite_min_max_side_condition_t ] + end. +Ltac only_split_min_max_step := + match goal with + | _ => revert_min_max; progress repeat apply Z.min_case_strong; intros + | _ => revert_min_max; progress repeat apply Z.max_case_strong; intros + end. +Ltac split_min_max_step := + match goal with + | _ => rewrite_min_max_step + | _ => only_split_min_max_step + end. +Ltac split_min_max := repeat split_min_max_step. |