feat(tactic/polyrith): solve more problems by testing for membership in the radical

scripts/polyrith_sage.py

@@ -19,16 +19,19 @@ def create_query(type: str, n_vars: int, eq_list, goal_type):
     """ Create a query to invoke Sage's `MPolynomial_libsingular.lift`. See
     https://github.com/sagemath/sage/blob/f8df80820dc7321dc9b18c9644c3b8315999670b/src/sage/rings/polynomial/multi_polynomial_libsingular.pyx#L4472-L4518
     for a description of this method. """
-    var_list = ", ".join([f"var{i}" for i in range(n_vars)])
+    var_list = [f"var{i}" for i in range(n_vars)] + ['aux']
     query = f'''
 import json
-P = PolynomialRing({type_str(type)}, 'var', {n_vars!r})
-[{var_list}] = P.gens()
-gens = {eq_list}
+P = {type_str(type)}{var_list}
+[{", ".join(var_list)}] = P.gens()
 p = P({goal_type})
+gens = {eq_list} + [1 - p*aux]
 I = ideal(gens)
-coeffs = p.lift(I)
-print(json.dumps([polynomial_to_string(c) for c in coeffs]))
+coeffs = P(1).lift(I)
+power = max(cf.degree(aux) for cf in coeffs)
+coeffs = [P(cf.subs(aux = 1/p)*p^power) for cf in coeffs[:int(-1)]]
+js = {{'power': power, 'coeffs': [polynomial_to_string(c) for c in coeffs]}}
+print(json.dumps(js))
 '''
     return query
 

src/tactic/linear_combination.lean

@@ -435,7 +435,7 @@ meta def _root_.tactic.interactive.linear_combination
   (input : parse (as_linear_combo ff [] <$> texpr)?)
   (_ : parse (tk "with")?)
   (config : linear_combination_config := {})
-  : tactic unit :=
+  : tactic unit := do
 let (h_eqs_names, coeffs) := list.unzip (input.get_or_else []) in
 linear_combination h_eqs_names coeffs config
 

src/tactic/polyrith.lean

@@ -300,12 +300,18 @@ meta instance : non_null_json_serializable poly :=
     | sum.inr p := pure p
     end}
 
+/-- A schema for the data reported by the Sage calculation -/
+@[derive [non_null_json_serializable, inhabited]]
+structure sage_json_coeffs_and_power :=
+(coeffs : list poly)
+(power  : ℕ)
+
 /-- A schema for success messages from the python script -/
 @[derive [non_null_json_serializable, inhabited]]
 structure sage_json_success :=
 (success : {b : bool // b = tt})
 (trace : option string := none)
-(data : option (list poly) := none)
+(data : option sage_json_coeffs_and_power := none)
 
 /-- A schema for failure messages from the python script -/
 @[derive [non_null_json_serializable, inhabited]]
@@ -316,7 +322,7 @@ structure sage_json_failure :=
 
 /-- Parse the json output from `scripts/polyrith.py` into either an error message, a list of `poly`
 objects, or `none` if only trace output was requested. -/
-meta def convert_sage_output (j : json) : tactic (option (list poly)) :=
+meta def convert_sage_output (j : json) : tactic (option (ℕ × list poly)) :=
 do
   r : sage_json_success ⊕ sage_json_failure ← decorate_ex "internal json error: "
     -- try the error format first, so that if both fail we get the message from the success parser
@@ -326,7 +332,7 @@ do
       fail!"polyrith failed to retrieve a solution from Sage! {f.error_name}: {f.error_value}"
   | sum.inl s := do
       s.trace.mmap trace,
-      pure s.data
+      pure $ s.data.map $ λ sd, (sd.power, sd.coeffs)
   end
 
 /-!
@@ -484,18 +490,21 @@ a call to `linear_combination`.
 -/
 meta def process_output (eq_names : list expr) (m : list expr) (R : expr) (sage_out : json) :
   tactic format := focus1 $ do
-  some coeffs_as_poly ← convert_sage_output sage_out | fail!"internal error: No output available",
+  some (power, coeffs_as_poly) ← convert_sage_output sage_out
+    | fail!"internal error: No output available",
   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 {exponent := power},
   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 lc_fmt : format := "linear_combination " ++ format.nest 2 (format.group expr_string),
+  let lc_exp : format := if power = 1 then "" else format!" with {{exponent := {power}}}",
+  let lc_fmt : format := "linear_combination " ++
+    format.nest 2 (format.group expr_string ++ lc_exp),
   done <|>
     fail!"polyrith found the following certificate, but it failed to close the goal:\n{lc_fmt}",
-  return $ "linear_combination " ++ format.nest 2 (format.group expr_string)
+  return lc_fmt
 
 /-- Tactic for the special case when no hypotheses are available. -/
 meta def no_hypotheses_case : tactic (option format) :=