From e5d58e8575d25956bd93387c08127b02c86606f3 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 18 Oct 2023 01:20:20 +0000
Subject: [PATCH] fix(Tactic/Polyrith): fix crash when hypotheses are constant
 polynomials (#7586)

This forward-ports leanprover-community/mathlib#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 |  2 --
 scripts/polyrith_sage.py     | 12 ++++++++----
 test/polyrith.lean           | 22 +++++++++++++++++++---
 3 files changed, 27 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Tactic/Polyrith.lean b/Mathlib/Tactic/Polyrith.lean
index 4ee028d7c404a..53d3585e76d8f 100644
--- a/Mathlib/Tactic/Polyrith.lean
+++ b/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
diff --git a/scripts/polyrith_sage.py b/scripts/polyrith_sage.py
index f25beea928b36..0ced1a3ca1064 100644
--- a/scripts/polyrith_sage.py
+++ b/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))
 '''
diff --git a/test/polyrith.lean b/test/polyrith.lean
index 5123abc612765..b941ec56c1d4d 100644
--- a/test/polyrith.lean
+++ b/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.
 
 /-