From a49d6945893959d894795ce4fcbe6f7238a81ee5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Dec 2018 18:33:06 -0500 Subject: Add ZRange.OperationBounds --- src/Util/ZRange/BasicLemmas.v | 5 ++ src/Util/ZRange/OperationsBounds.v | 95 ++++++++++++++++++++++++++++++++++++++ src/Util/ZUtil/Morphisms.v | 36 +++++++++++++++ 3 files changed, 136 insertions(+) create mode 100644 src/Util/ZRange/OperationsBounds.v (limited to 'src/Util') diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v index 5f434c771..e41657428 100644 --- a/src/Util/ZRange/BasicLemmas.v +++ b/src/Util/ZRange/BasicLemmas.v @@ -177,4 +177,9 @@ Module ZRange. rewrite <- is_bounded_by_bool_opp at 1. rewrite normalize_opp, opp_involutive; reflexivity. Qed. + + Lemma is_tighter_than_bool_constant r v + : is_tighter_than_bool (ZRange.constant v) r + = is_bounded_by_bool v r. + Proof. reflexivity. Qed. End ZRange. diff --git a/src/Util/ZRange/OperationsBounds.v b/src/Util/ZRange/OperationsBounds.v new file mode 100644 index 000000000..d57577210 --- /dev/null +++ b/src/Util/ZRange/OperationsBounds.v @@ -0,0 +1,95 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZRange.Operations. +Require Import Crypto.Util.ZRange.BasicLemmas. +Require Import Crypto.Util.ZRange.CornersMonotoneBounds. +Require Import Crypto.Util.ZRange.LandLorBounds. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Morphisms. +Require Import Crypto.Util.Notations. + +Module ZRange. + Local Ltac t := + lazymatch goal with + | [ |- is_bounded_by_bool (?f _) (ZRange.two_corners ?f _) = true ] + => apply (@ZRange.monotoneb_two_corners_gen f) + | [ |- is_bounded_by_bool (?f _ _) (ZRange.four_corners ?f _ _) = true ] + => apply (@ZRange.monotoneb_four_corners_gen f) + | [ |- is_bounded_by_bool (?f _ _) (ZRange.four_corners_and_zero ?f _ _) = true ] + => apply (@ZRange.monotoneb_four_corners_and_zero_gen f) + end; + eauto with zarith; + repeat match goal with + | [ |- forall x : Z, _ ] => let x := fresh "x" in intro x; destruct x + end; + eauto with zarith. + + Lemma is_bounded_by_bool_log2 + x x_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + : is_bounded_by_bool (Z.log2 x) (ZRange.log2 x_bs) = true. + Proof. t. Qed. + + Lemma is_bounded_by_bool_log2_up + x x_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + : is_bounded_by_bool (Z.log2_up x) (ZRange.log2_up x_bs) = true. + Proof. t. Qed. + + Lemma is_bounded_by_bool_add + x x_bs y y_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + (Hboundedy : is_bounded_by_bool y y_bs = true) + : is_bounded_by_bool (Z.add x y) (ZRange.add x_bs y_bs) = true. + Proof. t. Qed. + + Lemma is_bounded_by_bool_sub + x x_bs y y_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + (Hboundedy : is_bounded_by_bool y y_bs = true) + : is_bounded_by_bool (Z.sub x y) (ZRange.sub x_bs y_bs) = true. + Proof. t. Qed. + + Lemma is_bounded_by_bool_mul + x x_bs y y_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + (Hboundedy : is_bounded_by_bool y y_bs = true) + : is_bounded_by_bool (Z.mul x y) (ZRange.mul x_bs y_bs) = true. + Proof. t. Qed. + + Lemma is_bounded_by_bool_div + x x_bs y y_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + (Hboundedy : is_bounded_by_bool y y_bs = true) + : is_bounded_by_bool (Z.div x y) (ZRange.div x_bs y_bs) = true. + Proof. t. Qed. + + Lemma is_bounded_by_bool_shiftr + x x_bs y y_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + (Hboundedy : is_bounded_by_bool y y_bs = true) + : is_bounded_by_bool (Z.shiftr x y) (ZRange.shiftr x_bs y_bs) = true. + Proof. t. Qed. + + Lemma is_bounded_by_bool_shiftl + x x_bs y y_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + (Hboundedy : is_bounded_by_bool y y_bs = true) + : is_bounded_by_bool (Z.shiftl x y) (ZRange.shiftl x_bs y_bs) = true. + Proof. t. Qed. + + Lemma is_bounded_by_bool_land + x x_bs y y_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + (Hboundedy : is_bounded_by_bool y y_bs = true) + : is_bounded_by_bool (Z.land x y) (ZRange.land x_bs y_bs) = true. + Proof. now apply ZRange.is_bounded_by_bool_land_bounds. Qed. + + Lemma is_bounded_by_bool_lor + x x_bs y y_bs + (Hboundedx : is_bounded_by_bool x x_bs = true) + (Hboundedy : is_bounded_by_bool y y_bs = true) + : is_bounded_by_bool (Z.lor x y) (ZRange.lor x_bs y_bs) = true. + Proof. now apply ZRange.is_bounded_by_bool_lor_bounds. Qed. +End ZRange. diff --git a/src/Util/ZUtil/Morphisms.v b/src/Util/ZUtil/Morphisms.v index 15a9fcf1a..d073e0429 100644 --- a/src/Util/ZUtil/Morphisms.v +++ b/src/Util/ZUtil/Morphisms.v @@ -178,6 +178,12 @@ Module Z. Lemma div_Zneg_Zneg_le_Proper_l p : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.div (Zneg p) (Zneg x)). Proof. div_Proper_t. Qed. Hint Resolve div_Zneg_Zneg_le_Proper_l : zarith. + Lemma div_Z0_Zpos_le_Proper_l : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.div Z0 (Zpos x)). + Proof. div_Proper_t. Qed. + Hint Resolve div_Z0_Zpos_le_Proper_l : zarith. + Lemma div_Z0_Zneg_le_Proper_l : Proper (Pos.le ==> Z.le) (fun x => Z.div Z0 (Zneg x)). + Proof. div_Proper_t. Qed. + Hint Resolve div_Z0_Zneg_le_Proper_l : zarith. Lemma div_Zpos_Zpos_le_Proper_r x : Proper (Pos.le ==> Z.le) (fun p => Z.div (Zpos p) (Zpos x)). Proof. div_Proper_t. Qed. Hint Resolve div_Zpos_Zpos_le_Proper_r : zarith. @@ -190,6 +196,12 @@ Module Z. Lemma div_Zneg_Zneg_le_Proper_r x : Proper (Pos.le ==> Z.le) (fun p => Z.div (Zneg p) (Zneg x)). Proof. div_Proper_t. Qed. Hint Resolve div_Zneg_Zneg_le_Proper_r : zarith. + Lemma div_Zpos_Z0_le_Proper_r : Proper (Pos.le ==> Z.le) (fun p => Z.div (Zpos p) Z0). + Proof. do 3 intro; cbv; congruence. Qed. + Hint Resolve div_Zpos_Z0_le_Proper_r : zarith. + Lemma div_Zneg_Z0_le_Proper_r : Proper (Basics.flip Pos.le ==> Z.le) (fun p => Z.div (Zneg p) Z0). + Proof. do 3 intro; cbv; congruence. Qed. + Hint Resolve div_Zneg_Z0_le_Proper_r : zarith. Local Ltac shift_t := repeat first [ progress intros | progress cbv [Proper respectful Basics.flip] in * @@ -244,6 +256,12 @@ Module Z. Lemma shiftr_Zneg_Zneg_le_Proper_l p : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.shiftr (Zneg p) (Zneg x)). Proof. shift_Proper_t'. Qed. Hint Resolve shiftr_Zneg_Zneg_le_Proper_l : zarith. + Lemma shiftr_Z0_Zpos_le_Proper_l : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.shiftr Z0 (Zpos x)). + Proof. shift_Proper_t'. Qed. + Hint Resolve shiftr_Z0_Zpos_le_Proper_l : zarith. + Lemma shiftr_Z0_Zneg_le_Proper_l : Proper (Pos.le ==> Z.le) (fun x => Z.shiftr Z0 (Zneg x)). + Proof. shift_Proper_t'. Qed. + Hint Resolve shiftr_Z0_Zneg_le_Proper_l : zarith. Lemma shiftr_Zpos_Zpos_le_Proper_r x : Proper (Pos.le ==> Z.le) (fun p => Z.shiftr (Zpos p) (Zpos x)). Proof. shift_Proper_t'. Qed. Hint Resolve shiftr_Zpos_Zpos_le_Proper_r : zarith. @@ -256,6 +274,12 @@ Module Z. Lemma shiftr_Zneg_Zneg_le_Proper_r x : Proper (Basics.flip Pos.le ==> Z.le) (fun p => Z.shiftr (Zneg p) (Zneg x)). Proof. shift_Proper_t'. Qed. Hint Resolve shiftr_Zneg_Zneg_le_Proper_r : zarith. + Lemma shiftr_Zpos_Z0_le_Proper_r : Proper (Pos.le ==> Z.le) (fun p => Z.shiftr (Zpos p) Z0). + Proof. shift_Proper_t'. Qed. + Hint Resolve shiftr_Zpos_Z0_le_Proper_r : zarith. + Lemma shiftr_Zneg_Z0_le_Proper_r : Proper (Basics.flip Pos.le ==> Z.le) (fun p => Z.shiftr (Zneg p) Z0). + Proof. shift_Proper_t'. Qed. + Hint Resolve shiftr_Zneg_Z0_le_Proper_r : zarith. Lemma shiftl_Zpos_Zpos_le_Proper_l p : Proper (Pos.le ==> Z.le) (fun x => Z.shiftl (Zpos p) (Zpos x)). Proof. shift_Proper_t'. Qed. Hint Resolve shiftl_Zpos_Zpos_le_Proper_l : zarith. @@ -268,6 +292,12 @@ Module Z. Lemma shiftl_Zneg_Zneg_le_Proper_l p : Proper (Pos.le ==> Z.le) (fun x => Z.shiftl (Zneg p) (Zneg x)). Proof. shift_Proper_t'. Qed. Hint Resolve shiftl_Zneg_Zneg_le_Proper_l : zarith. + Lemma shiftl_Z0_Zpos_le_Proper_l : Proper (Pos.le ==> Z.le) (fun x => Z.shiftl Z0 (Zpos x)). + Proof. shift_Proper_t'. Qed. + Hint Resolve shiftl_Z0_Zpos_le_Proper_l : zarith. + Lemma shiftl_Z0_Zneg_le_Proper_l : Proper (Basics.flip Pos.le ==> Z.le) (fun x => Z.shiftl Z0 (Zneg x)). + Proof. shift_Proper_t'. Qed. + Hint Resolve shiftl_Z0_Zneg_le_Proper_l : zarith. Lemma shiftl_Zpos_Zpos_le_Proper_r x : Proper (Pos.le ==> Z.le) (fun p => Z.shiftl (Zpos p) (Zpos x)). Proof. shift_Proper_t'. Qed. Hint Resolve shiftl_Zpos_Zpos_le_Proper_r : zarith. @@ -280,6 +310,12 @@ Module Z. Lemma shiftl_Zneg_Zneg_le_Proper_r x : Proper (Basics.flip Pos.le ==> Z.le) (fun p => Z.shiftl (Zneg p) (Zneg x)). Proof. shift_Proper_t'. Qed. Hint Resolve shiftl_Zneg_Zneg_le_Proper_r : zarith. + Lemma shiftl_Zpos_Z0_le_Proper_r : Proper (Pos.le ==> Z.le) (fun p => Z.shiftl (Zpos p) Z0). + Proof. shift_Proper_t'. Qed. + Hint Resolve shiftl_Zpos_Z0_le_Proper_r : zarith. + Lemma shiftl_Zneg_Z0_le_Proper_r : Proper (Basics.flip Pos.le ==> Z.le) (fun p => Z.shiftl (Zneg p) Z0). + Proof. shift_Proper_t'. Qed. + Hint Resolve shiftl_Zneg_Z0_le_Proper_r : zarith. Hint Resolve Z.land_round_Proper_pos_r : zarith. Hint Resolve Z.land_round_Proper_pos_l : zarith. -- cgit v1.2.3