fix(tactic/polyrith): fix crash when hypotheses are constant polynomials

scripts/polyrith_sage.py

@@ -22,9 +22,14 @@ def create_query(type: str, n_vars: int, eq_list, goal_type):
     var_list = ", ".join([f"var{i}" for i in range(n_vars)])
     query = f'''
 import json
-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 bug
+    P = PolynomialRing({type_str(type)}, 'var', 1)
+# ensure that the equalities are cast to polynomials
+gens = [P() + eq for eq in {eq_list}]
 p = P({goal_type})
 I = ideal(gens)
 coeffs = p.lift(I)

src/tactic/polyrith.lean

@@ -502,11 +502,6 @@ meta def no_hypotheses_case : tactic (option format) :=
 (do `[ring], return $ some "ring") <|>
   fail "polyrith did not find any relevant hypotheses and the goal is not provable by ring"
 
-/-- Tactic for the special case when there are no variables. -/
-meta def no_variables_case : tactic (option format) :=
-(do `[ring], return $ some "ring") <|>
-  fail "polyrith did not find any variables and the goal is not provable by ring"
-
 /--
 This is the main body of the `polyrith` tactic. It takes in the following inputs:
 * `(only_on : bool)` - This represents whether the user used the key word "only"
@@ -535,8 +530,7 @@ meta def _root_.tactic.polyrith (only_on : bool) (hyps : list pexpr) : tactic (o
 do
   sleep 10, -- otherwise can lead to weird errors when actively editing code with polyrith calls
   (eq_names, m, R, args) ← create_args only_on hyps,
-  if eq_names.length = 0 then no_hypotheses_case else
-  if m.length = 0 then no_variables_case else do
+  if eq_names.length = 0 then no_hypotheses_case else do
   sage_out ← sage_output args,
   if is_trace_enabled_for `polyrith then do
     convert_sage_output sage_out,

test/polyrith.lean

@@ -435,11 +435,27 @@ by test_polyrith
   "(1 - 2)"]
   "linear_combination h1 - h2"
 
+example {R} [comm_ring 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} [comm_ring 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.
 
 
 /-