From f6893ac2202c4eb83f5998f995209e82fddccf9d Mon Sep 17 00:00:00 2001
From: Rob Lewis <rob.y.lewis@gmail.com>
Date: Sat, 16 Jul 2022 13:00:24 -0400
Subject: [PATCH] use linear_combination with exponent

---
 scripts/polyrith_sage.py |  2 +-
 src/tactic/polyrith.lean | 13 ++++---------
 2 files changed, 5 insertions(+), 10 deletions(-)

diff --git a/scripts/polyrith_sage.py b/scripts/polyrith_sage.py
index 83af919edc083..c7b329615ee05 100644
--- a/scripts/polyrith_sage.py
+++ b/scripts/polyrith_sage.py
@@ -35,7 +35,7 @@ def create_query(type: str, n_vars: int, eq_list, goal_type):
         raise e
     n = naive_power_search(p, I)
     coeffs = (p^n).lift(I)
-print(json.dumps({{'exponent': n, "coeffs": [polynomial_to_string(c) for c in coeffs]}}))
+print(json.dumps({{'exponent': int(n), "coeffs": [polynomial_to_string(c) for c in coeffs]}}))
 '''
     return query
 
diff --git a/src/tactic/polyrith.lean b/src/tactic/polyrith.lean
index 868d60969a589..ef1915eb9261e 100644
--- a/src/tactic/polyrith.lean
+++ b/src/tactic/polyrith.lean
@@ -57,10 +57,6 @@ remember to force recompilation of any files that call `polyrith`.
 
 open tactic native
 
-lemma pow_eq_zero' {M : Type*} [monoid_with_zero M] [no_zero_divisors M] {x : M} (n : ℕ) :
-  x ^ n = 0 → x = 0 :=
-pow_eq_zero
-
 namespace polyrith
 
 /-! # Poly Datatype -/
@@ -471,18 +467,17 @@ meta def process_output (eq_names : list expr) (m : list expr) (R : expr) (sage_
   tactic format := do
   some (exp, coeffs_as_poly) ← convert_sage_output sage_out
     | fail!"internal error: No output available",
-  when (exp ≠ 1) $ refine ``(pow_eq_zero' %%`(exp) _),
   coeffs_as_pexpr ← coeffs_as_poly.mmap (poly.to_pexpr m),
   let eq_names_pexpr := eq_names.map to_pexpr,
   coeffs_as_expr ← coeffs_as_pexpr.mmap $ λ e, to_expr ``(%%e : %%R),
-  linear_combo.linear_combination eq_names_pexpr coeffs_as_pexpr,
+  linear_combo.linear_combination eq_names_pexpr coeffs_as_pexpr
+    (if exp ≠ 1 then some exp else none),
   let components := (eq_names.zip coeffs_as_expr).filter
     $ λ pr, bnot $ pr.2.is_app_of `has_zero.zero,
   expr_string ← components_to_lc_format components,
-  let refn : format :=
-    if exp ≠ 1 then format!"refine pow_eq_zero' {exp} _;" ++ format.line else "",
   let lc : format := "linear_combination " ++ format.group expr_string,
-  return $ format.nest 2 $ refn ++ lc
+  let lc := if exp ≠ 1 then lc ++ format!" with exponent {exp}" else lc,
+  return $ format.nest 2 lc
 
 /-- Tactic for the special case when no hypotheses are available. -/
 meta def no_hypotheses_case : tactic (option format) :=