From 73be1b5ea507db8f6b5d9a5ea8db8b67027088ca Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 8 Apr 2017 15:03:28 -0400 Subject: Add Z.shift{l,r}_opp_l --- src/Util/ZUtil.v | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) (limited to 'src/Util/ZUtil.v') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index acdab1a06..83fe2d493 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1548,6 +1548,32 @@ Module Z. Hint Rewrite Z.div_opp_l_complete using zutil_arith : pull_Zopp. Hint Rewrite Z.div_opp_l_complete' using zutil_arith : push_Zopp. + Lemma shiftl_opp_l a n + : Z.shiftl (-a) n = - Z.shiftl a n - (if Z_zerop (a mod 2 ^ (- n)) then 0 else 1). + Proof. + destruct (Z_dec 0 n) as [ [?|?] | ? ]; + subst; + rewrite ?Z.pow_neg_r by omega; + autorewrite with zsimplify_const; + [ | | simpl; omega ]. + { rewrite !Z.shiftl_mul_pow2 by omega. + nia. } + { rewrite !Z.shiftl_div_pow2 by omega. + rewrite Z.div_opp_l_complete by auto with zarith. + reflexivity. } + Qed. + Hint Rewrite shiftl_opp_l : push_Zshift. + Hint Rewrite <- shiftl_opp_l : pull_Zshift. + + Lemma shiftr_opp_l a n + : Z.shiftr (-a) n = - Z.shiftr a n - (if Z_zerop (a mod 2 ^ n) then 0 else 1). + Proof. + unfold Z.shiftr; rewrite shiftl_opp_l at 1; rewrite Z.opp_involutive. + reflexivity. + Qed. + Hint Rewrite shiftr_opp_l : push_Zshift. + Hint Rewrite <- shiftr_opp_l : pull_Zshift. + Lemma div_opp a : a <> 0 -> -a / a = -1. Proof. intros; autorewrite with pull_Zopp zsimplify; lia. -- cgit v1.2.3