fix(Tactic/Polyrith): fix crash when hypotheses are constant polynomi…

…als (#7586)

This forward-ports leanprover-community/mathlib3#17142

The tests are commented out because the test framework for polyrith was never ported. You can check out the branch and run polyrith manually to see that everything is ok.

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.
 
 /-