[Merged by Bors] - fix(Tactic/Polyrith): fix crash when hypotheses are constant polynomials

Mathlib/Tactic/Polyrith.lean

@@ -332,8 +332,6 @@ def polyrith (g : MVarId) (only : Bool) (hyps : Array Expr)
     if hyps'.isEmpty then
       return ← byRing "polyrith did not find any relevant hypotheses"
     let vars := (← get).atoms.size
-    if vars = 0 then
-      return ← byRing "polyrith did not find find any variables"
     match ← sageOutput (createSageArgs traceOnly α vars hyps' tgt) with
     | .ok { trace, data } =>
       if let some trace := trace then logInfo trace

scripts/polyrith_sage.py

@@ -21,11 +21,15 @@ def create_query(type: str, n_vars: int, eq_list, goal_type):
     for a description of this method. """
     var_list = ", ".join([f"var{i}" for i in range(n_vars)])
     query = f'''
-P = PolynomialRing({type_str(type)}, 'var', {n_vars!r})
-[{var_list}] = P.gens()
-gens = {eq_list}
+if {n_vars!r} != 0:
+    P = PolynomialRing({type_str(type)}, 'var', {n_vars!r})
+    [{var_list}] = P.gens()
+else:
+    # workaround for a Sage shortcoming with `n_vars = 0`,
+    # `TypeError: no conversion of this ring to a Singular ring defined`
+    P = PolynomialRing({type_str(type)}, 'var', 1)
 p = P({goal_type})
-I = ideal(gens)
+I = P.ideal({eq_list})
 coeffs = p.lift(I)
 print(serialize_polynomials(coeffs))
 '''

test/polyrith.lean

@@ -433,11 +433,27 @@ A full test suite is provided at the bottom of the file.
 --   "(1 - 2)"]
 --   "linear_combination h1 - h2"
 
+-- example {R} [CommRing R] (x : R) (h2 : (2 : R) = 0) : x + x = 0 :=
+-- by test_polyrith
+--   "{\"data\":[\"(poly.var 0)\"],\"success\":true}"
+--   ["ff",
+--   "R",
+--   "1",
+--   "[(2 - 0)]",
+--   "((var0 + var0) - 0)"]
+--   "linear_combination x * h2"
 
--- We comment the following tests so that we don't overwhelm the SageCell API.
-
-
+-- example {R} [CommRing R] (_x : R) (h : (2 : R) = 4) : (0 : R) = 2 :=
+-- by test_polyrith
+--   "{\"data\":[\"(poly.const 1/1)\"],\"success\":true}"
+--   ["ff",
+--   "R",
+--   "0",
+--   "[(2 - 4)]",
+--   "(0 - 2)"]
+--   "linear_combination h"
 
+-- We comment the following tests so that we don't overwhelm the SageCell API.
 
 /-