diff options
| -rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v | 65 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v | 23 |
2 files changed, 74 insertions, 14 deletions
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v index 39571e9ab..ec1a9cb98 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v @@ -30,6 +30,54 @@ Proof. | word_arith_t ]. Qed. +Local Arguments N.ldiff : simpl never. +Lemma land_abs_bounds a b + : a < 0 \/ b < 0 + -> -(2^(Z.log2_up (Z.max (Z.abs a) (Z.abs b)))) + <= Z.land a b + <= Z.max a b. +Proof. + destruct a, b; simpl Z.abs; split; + try solve [ unfold Z.max; simpl; lia + | unfold Z.max; simpl; apply Z.opp_nonpos_nonneg; auto with zarith + | match goal with + | [ |- - _ <= _ ] + => transitivity 0; + solve [ unfold Z.max; simpl; lia + | unfold Z.max; simpl; apply Z.opp_nonpos_nonneg; auto with zarith ] + | [ |- Z.land (Z.pos _) (Z.pos _) <= Z.max _ _ ] + => apply Z.max_case_strong; intro; + first [ apply Z.land_upper_bound_l + | apply Z.land_upper_bound_r ]; + lia + end ]. + all:simpl. + all:admit. +Admitted. +Local Existing Instances Z.add_le_Proper Z.log2_up_le_Proper Z.pow_Zpos_le_Proper Z.sub_le_eq_Proper. +Lemma lor_abs_bounds a b + : a < 0 \/ b < 0 + -> Z.min a b + <= Z.lor a b + <= 2^(Z.log2_up (Z.max (Z.abs a) (Z.abs b) + 1)) - 1. +Proof. + destruct a, b; simpl Z.abs; split; + try solve [ unfold Z.max, Z.min; simpl; lia + | unfold Z.max, Z.min; simpl; apply Z.opp_nonpos_nonneg; auto with zarith + | match goal with + | [ |- Z.min (Z.pos _) (Z.pos _) <= Z.lor _ _ ] + => apply Z.lor_bounds_gen_lower; lia + end + | apply Z.lor_bounds_upper ]; + repeat first [ rewrite Z.max_r by lia + | rewrite Z.max_l by lia + | rewrite Z.lor_0_l + | rewrite Z.lor_0_r + | omega + | lia + | rewrite <- Z.log2_up_le_full; lia ]. +Admitted. + Local Arguments Z.pow : simpl never. Local Arguments Z.add !_ !_. Local Existing Instances Z.add_le_Proper Z.log2_up_le_Proper Z.pow_Zpos_le_Proper Z.sub_le_eq_Proper. @@ -55,13 +103,14 @@ Proof. { handle_four_corners. } { destruct_head Bounds.t. case_Zvar_nonneg; replace_all_neg_with_pos; handle_shift_neg; - autorewrite with Zshift_to_pow; - rewrite ?Z.div_opp_l_complete by auto with zarith; - autorewrite with Zpow_to_shift. + preprocess_shift_min_max. 16:split_min_max; saturate_with_shift_facts; omega. all:admit. } { destruct_head Bounds.t. - case_Zvar_nonneg; replace_all_neg_with_pos; handle_shift_neg; admit. } + case_Zvar_nonneg; replace_all_neg_with_pos; handle_shift_neg; + preprocess_shift_min_max. + 16:split_min_max; saturate_with_shift_facts; omega. + all:admit. } { repeat first [ progress destruct_head Bounds.t | progress simpl in * | break_t_step @@ -69,8 +118,8 @@ Proof. | rewriter_t | progress replace_all_neg_with_pos | progress saturate_land_lor_facts - | split_min_max; omega ]; - admit. } + | split_min_max; omega ]. + all:admit. } { repeat first [ progress destruct_head Bounds.t | progress simpl in * | break_t_step @@ -79,8 +128,8 @@ Proof. | progress replace_all_neg_with_pos | progress saturate_land_lor_facts | progress Zarith_land_lor_t_step - | solve [ split_min_max; try omega; try Zarith_land_lor_t_step ] ]; - admit. } + | solve [ split_min_max; try omega; try Zarith_land_lor_t_step ] ]. + all:admit. } { repeat first [ progress destruct_head Bounds.t | progress simpl in * | progress split_min_max diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v index 349f1c6ce..57b41cfae 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v @@ -123,10 +123,10 @@ Ltac saturate_with_shift_facts := => unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega) | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?y << ?y'] ] => unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega) - | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?x >> ?x'] ] - => unique assert (x >> x' <= y >> y') by (apply Z.shiftr_le_mono; omega) - | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?y >> ?y'] ] - => unique assert (x >> x' <= y >> y') by (apply Z.shiftr_le_mono; omega) + | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?x >> ?y'] ] + => unique assert (x >> y' <= y >> x') by (Z.shiftr_le_mono; omega) + | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?y >> ?x'] ] + => unique assert (x >> y' <= y >> x') by (apply Z.shiftr_le_mono; omega) end. Ltac saturate_with_all_shift_facts := repeat match goal with @@ -134,8 +134,17 @@ Ltac saturate_with_all_shift_facts := | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[Z.shiftl _ _] ] => unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega) | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[Z.shiftr _ _] ] - => unique assert (x >> x' <= y >> y') by (apply Z.shiftr_le_mono; omega) + => unique assert (x >> y' <= y >> x') by (apply Z.shiftr_le_mono; omega) end. +Ltac preprocess_shift_min_max := + repeat first [ rewrite (Z.min_r (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega) + | rewrite (Z.min_l (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega) + | rewrite (Z.max_r (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega) + | rewrite (Z.max_l (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega) + | rewrite (Z.min_r (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega) + | rewrite (Z.min_l (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega) + | rewrite (Z.max_r (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega) + | rewrite (Z.max_l (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega) ]. Ltac saturate_land_lor_facts := repeat match goal with | [ |- context[Z.land ?x ?y] ] @@ -179,7 +188,9 @@ Ltac replace_all_neg_with_pos := end. Ltac handle_shift_neg := repeat first [ rewrite !Z.shiftr_opp_r - | rewrite !Z.shiftl_opp_r ]. + | rewrite !Z.shiftl_opp_r + | rewrite !Z.shiftr_opp_l + | rewrite !Z.shiftl_opp_l ]. Ltac handle_four_corners_step_fast := first [ progress destruct_head Bounds.t |