Pull out *2 in square, don't turn *2 into <<1

2 files changed, 8 insertions, 7 deletions

diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v
index dfd00c943..3ab5a5e09 100644
--- a/src/Experiments/NewPipeline/Arithmetic.v
+++ b/src/Experiments/NewPipeline/Arithmetic.v
@@ -75,14 +75,15 @@ Module Associational.
       _
       nil
       (fun t ts acc
-       => ((fst t * fst t, snd t * snd t)
-             :: (map (fun t'
-                      => (fst t * fst t', 2 * snd t * snd t'))
-                     ts))
+       => (dlet two_t2 := 2 * snd t in
+               (fst t * fst t, snd t * snd t)
+                 :: (map (fun t'
+                          => (fst t * fst t', two_t2 * snd t'))
+                         ts))
             ++ acc)
       p.
   Lemma eval_square p : eval (square p) = eval p * eval p.
-  Proof. induction p; cbn [square list_rect]; push; nsatz.    Qed.
+  Proof. induction p; cbv [square list_rect Let_In]; push; nsatz. Qed.
   Hint Rewrite eval_square : push_eval.
 
   Definition negate_snd (p:list (Z*Z)) : list (Z*Z) :=
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index 1d0354713..ec9e36c67 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -1296,8 +1296,8 @@ In the RHS, the follow notation applies:
                 ; make_rewrite ((-??{ℤ}) *   ??{ℤ} ) (fun x y => -(x * y))
                 ; make_rewrite (  ??{ℤ}  * (-??{ℤ})) (fun x y => -(x * y))
 
-                ; make_rewrite (??{ℤ} * #?ℤ) (fun x y => x << ##(Z.log2 y)  when  Z.eqb y (2^Z.log2 y))
-                ; make_rewrite (#?ℤ * ??{ℤ}) (fun y x => x << ##(Z.log2 y)  when  Z.eqb y (2^Z.log2 y))
+                ; make_rewrite (??{ℤ} * #?ℤ) (fun x y => x << ##(Z.log2 y)  when  (y =? (2^Z.log2 y)) && (negb (y =? 2)))
+                ; make_rewrite (#?ℤ * ??{ℤ}) (fun y x => x << ##(Z.log2 y)  when  (y =? (2^Z.log2 y)) && (negb (y =? 2)))
                 ; make_rewrite (??{ℤ} / #?ℤ) (fun x y => x >> ##(Z.log2 y)  when  Z.eqb y (2^Z.log2 y))
                 ; make_rewrite (??{ℤ} mod #?ℤ) (fun x y =>  x &' ##(y-1)%Z  when  Z.eqb y (2^Z.log2 y))
                 ; make_rewrite (-(-??{ℤ})) (fun v => v)