Revert "Factor out a common computation to fix n² behavior"

This reverts commit 1d8c074afbd8cee069e80306f9116bcd8c5b3e48.

It doesn't actually make a difference in running time, and it
complicates things a bit.

1 files changed, 9 insertions, 12 deletions

diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v
index 05bd2e83f..59c13e8c5 100644
--- a/src/Experiments/NewPipeline/Arithmetic.v
+++ b/src/Experiments/NewPipeline/Arithmetic.v
@@ -15,7 +15,6 @@ Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Import Crypto.Util.Tactics.RunTacticAsConstr.
 Require Import Crypto.Util.Tactics.Head.
-Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.OptionList.
 Require Import Crypto.Util.Prod.
@@ -2135,13 +2134,13 @@ Module Rows.
           (map weight (seq 0 fuel)).
 
       (* TODO : move sat_reduce and repeat_sat_reduce to Saturated.Associational *)
-      Definition sat_reduce base s s' c (p : list (Z * Z)) :=
+      Definition sat_reduce base s c n (p : list (Z * Z)) :=
+        let '(s', _) := adjust_s (S (S n)) s in
         let lo_hi := Associational.split s' p in
         fst lo_hi ++ (Associational.sat_mul_const base [(1, s'/s)] (Associational.sat_mul_const base c (snd lo_hi))).
 
       Definition repeat_sat_reduce base s c (p : list (Z * Z)) n :=
-        let '(s', _) := adjust_s (S (S n)) s in
-        fold_right (fun _ q => sat_reduce base s s' c q) p (seq 0 n).
+        fold_right (fun _ q => sat_reduce base s c n q) p (seq 0 n).
 
       Definition mulmod base s c n nreductions (p q : list Z) :=
         let p_a := Positional.to_associational weight n p in
@@ -2233,17 +2232,16 @@ Module Rows.
         { break_match; cbn in *; auto. }
       Qed.
 
-      Lemma eval_sat_reduce base s s' c p :
+      Lemma eval_sat_reduce base s c n p :
         base <> 0 -> s - Associational.eval c <> 0 -> s <> 0 ->
-        s' mod s = 0 -> s' <> 0 ->
-        Associational.eval (sat_reduce base s s' c p) mod (s - Associational.eval c)
+        Associational.eval (sat_reduce base s c n p) mod (s - Associational.eval c)
         = Associational.eval p mod (s - Associational.eval c).
       Proof using wprops.
         intros; cbv [sat_reduce].
+        lazymatch goal with |- context[adjust_s ?fuel ?s] => destruct (adjust_s_invariant fuel s ltac:(assumption)) as [Hmod ?] end.
         eta_expand; autorewrite with push_eval zsimplify_const; cbn [fst snd].
         rewrite !Z.mul_assoc, <- (Z.mul_comm (Associational.eval c)), <- !Z.mul_assoc, <-Associational.reduction_rule by auto.
-        autorewrite with zsimplify_const; rewrite !Z.mul_assoc, Z.mul_div_eq_full by auto.
-        rewrite_hyp !*.
+        autorewrite with zsimplify_const; rewrite !Z.mul_assoc, Z.mul_div_eq_full, Hmod by auto.
         autorewrite with zsimplify_const push_eval; trivial.
       Qed.
       Hint Rewrite eval_sat_reduce using auto : push_eval.
@@ -2253,9 +2251,8 @@ Module Rows.
         Associational.eval (repeat_sat_reduce base s c p n) mod (s - Associational.eval c)
         = Associational.eval p mod (s - Associational.eval c).
       Proof using wprops.
-        intros; cbv [repeat_sat_reduce]; eta_expand.
-        apply fold_right_invariant; intros; autorewrite with push_eval; auto;
-          apply adjust_s_invariant; assumption.
+        intros; cbv [repeat_sat_reduce].
+        apply fold_right_invariant; intros; autorewrite with push_eval; auto.
       Qed.
       Hint Rewrite eval_repeat_sat_reduce using auto : push_eval.