More shift lemmas

After    | File Name                                       | Before   || Change
----------------------------------------------------------------------------------
2m20.11s | Total                                           | 2m11.90s || +0m08.20s
----------------------------------------------------------------------------------
0m09.76s | Testbit                                         | 0m08.74s || +0m01.01s
0m05.19s | ModularArithmetic/BarrettReduction/ZHandbook    | 0m03.57s || +0m01.62s
0m04.49s | ModularArithmetic/BarrettReduction/ZGeneralized | 0m02.86s || +0m01.63s
0m17.23s | ModularArithmetic/ModularBaseSystemProofs       | 0m17.30s || -0m00.07s
0m16.16s | Specific/GF25519                                | 0m16.25s || -0m00.08s
0m14.09s | Experiments/SpecEd25519                         | 0m13.78s || +0m00.31s
0m13.35s | ModularArithmetic/Pow2BaseProofs                | 0m12.62s || +0m00.73s
0m09.25s | ModularArithmetic/Montgomery/ZProofs            | 0m08.38s || +0m00.86s
0m09.06s | Util/ZUtil                                      | 0m09.15s || -0m00.08s
0m03.89s | BaseSystemProofs                                | 0m03.99s || -0m00.10s
0m03.74s | ModularArithmetic/ModularArithmeticTheorems     | 0m02.77s || +0m00.97s
0m03.66s | ModularArithmetic/Tutorial                      | 0m03.64s || +0m00.02s
0m03.40s | Experiments/SpecificCurve25519                  | 0m03.42s || -0m00.02s
0m02.62s | Specific/GF1305                                 | 0m02.58s || +0m00.04s
0m02.22s | ModularArithmetic/BarrettReduction/ZBounded     | 0m02.34s || -0m00.11s
0m01.97s | ModularArithmetic/ModularBaseSystemOpt          | 0m02.05s || -0m00.07s
0m01.63s | Encoding/PointEncodingPre                       | 0m01.51s || +0m00.11s
0m01.56s | ModularArithmetic/BarrettReduction/Z            | 0m01.50s || +0m00.06s
0m01.23s | BaseSystem                                      | 0m01.21s || +0m00.02s
0m01.23s | ModularArithmetic/Montgomery/ZBounded           | 0m00.80s || +0m00.42s
0m01.18s | ModularArithmetic/ExtendedBaseVector            | 0m01.23s || -0m00.05s
0m01.15s | Util/NumTheoryUtil                              | 0m00.99s || +0m00.15s
0m01.06s | ModularArithmetic/PrimeFieldTheorems            | 0m01.07s || -0m00.01s
0m00.93s | Experiments/DerivationsOptionRectLetInEncoding  | 0m00.94s || -0m00.00s
0m00.92s | Encoding/ModularWordEncodingPre                 | 0m00.69s || +0m00.23s
0m00.89s | ModularArithmetic/ModularBaseSystemList         | 0m00.66s || +0m00.23s
0m00.89s | ModularArithmetic/ModularBaseSystemField        | 0m00.95s || -0m00.05s
0m00.88s | Spec/ModularWordEncoding                        | 0m00.57s || +0m00.31s
0m00.87s | ModularArithmetic/ModularBaseSystemListProofs   | 0m00.83s || +0m00.04s
0m00.83s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.87s || -0m00.04s
0m00.73s | Encoding/ModularWordEncodingTheorems            | 0m00.66s || +0m00.06s
0m00.72s | ModularArithmetic/ExtPow2BaseMulProofs          | 0m00.74s || -0m00.02s
0m00.59s | ModularArithmetic/ModularBaseSystem             | 0m00.62s || -0m00.03s
0m00.54s | Spec/ModularArithmetic                          | 0m00.36s || +0m00.18s
0m00.51s | ModularArithmetic/Pre                           | 0m00.56s || -0m00.05s
0m00.47s | ModularArithmetic/ZBounded                      | 0m00.48s || -0m00.01s
0m00.43s | ModularArithmetic/Pow2Base                      | 0m00.43s || +0m00.00s
0m00.40s | ModularArithmetic/Montgomery/Z                  | 0m00.39s || +0m00.01s
0m00.39s | ModularArithmetic/PseudoMersenneBaseParams      | 0m00.41s || -0m00.01s

1 files changed, 20 insertions, 0 deletions

diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index e4bb5b4ca..9552ee582 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1560,6 +1560,26 @@ Module Z.
   Proof. destruct (x >? y + x) eqn:?, (0 >? y) eqn:?; ltb_to_lt; try reflexivity; omega. Qed.
   Hint Rewrite gtb_add_same : zsimplify.
 
+  Lemma shiftl_add x y z : 0 <= z -> (x + y) << z = (x << z) + (y << z).
+  Proof. intros; autorewrite with Zshift_to_pow; lia. Qed.
+  Hint Rewrite shiftl_add using zutil_arith : push_Zshift.
+  Hint Rewrite <- shiftl_add using zutil_arith : pull_Zshift.
+
+  Lemma shiftr_add x y z : z <= 0 -> (x + y) >> z = (x >> z) + (y >> z).
+  Proof. intros; autorewrite with Zshift_to_pow; lia. Qed.
+  Hint Rewrite shiftr_add using zutil_arith : push_Zshift.
+  Hint Rewrite <- shiftr_add using zutil_arith : pull_Zshift.
+
+  Lemma shiftl_sub x y z : 0 <= z -> (x - y) << z = (x << z) - (y << z).
+  Proof. intros; autorewrite with Zshift_to_pow; lia. Qed.
+  Hint Rewrite shiftl_sub using zutil_arith : push_Zshift.
+  Hint Rewrite <- shiftl_sub using zutil_arith : pull_Zshift.
+
+  Lemma shiftr_sub x y z : z <= 0 -> (x - y) >> z = (x >> z) - (y >> z).
+  Proof. intros; autorewrite with Zshift_to_pow; lia. Qed.
+  Hint Rewrite shiftr_sub using zutil_arith : push_Zshift.
+  Hint Rewrite <- shiftr_sub using zutil_arith : pull_Zshift.
+
   Lemma simplify_twice_sub_sub x y : 2 * x - (x - y) = x + y.
   Proof. lia. Qed.
   Hint Rewrite simplify_twice_sub_sub : zsimplify.