From e76a76c36a1c2792438b62656bb94234bc4e5317 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Fri, 24 May 2024 04:42:29 +0000 Subject: [PATCH] fix: make polyrith succeed when target is identically zero (#13150) The `polyrith` feature that checks for membership in the radical of the ideal fails if the target is 0. (That is, `polyrith` cannot prove `x - x = 0`.) This PR fixes this by checking (in Sage) whether the target is 0, and short circuiting if it is. This example succeeded before #7790, fails after, and now succeeds again. ```lean import Mathlib.Tactic.Polyrith variable {R : Type*} [CommRing R] example {x : R} (H : x = 1) : x = x := by polyrith ``` This PR also renames a misleadingly named variable in the `polyrith` Python script. Co-authored-by: Rob Lewis --- scripts/polyrith_sage.py | 27 +++++++++++++++++---------- 1 file changed, 17 insertions(+), 10 deletions(-) diff --git a/scripts/polyrith_sage.py b/scripts/polyrith_sage.py index f9937c85ba2cd..42f7f58ccc7fd 100644 --- a/scripts/polyrith_sage.py +++ b/scripts/polyrith_sage.py @@ -15,7 +15,7 @@ def type_str(type): return "QQ" -def create_query(type: str, n_vars: int, eq_list, goal_type): +def create_query(type: str, n_vars: int, eq_list, target): """ 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. """ @@ -24,21 +24,28 @@ def create_query(type: str, n_vars: int, eq_list, goal_type): if {n_vars!r} != 0: P = PolynomialRing({type_str(type)}, {var_list}) [{", ".join(var_list)}] = P.gens() - p = P({goal_type}) - gens = {eq_list} + [1 - p*aux] - I = P.ideal(gens) - 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)]] - print(str(power)+';'+serialize_polynomials(coeffs)) + p = P({target}) + if p==0: + # The "radicalization trick" implemented below does not work if the target polynomial p is 0 + # since it requires substituting 1/p. + print('1;'+serialize_polynomials(len({eq_list})*[P(0)])) + else: + # Implements the trick described in 2.2 of arxiv.org/pdf/1007.3615.pdf + # for testing membership in the radical. + gens = {eq_list} + [1 - p*aux] + I = P.ideal(gens) + 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)]] + print(str(power)+';'+serialize_polynomials(coeffs)) else: # workaround for a Sage shortcoming with `n_vars = 0`, # `TypeError: no conversion of this ring to a Singular ring defined` # In this case, there is no need to look for membership in the *radical*; - # we just check for membership in the ideal, and return exponent 1 + # we just check for membership in the ideal, and return exponent 1 # if coefficients are found. P = PolynomialRing({type_str(type)}, 'var', 1) - p = P({goal_type}) + p = P({target}) I = P.ideal({eq_list}) coeffs = p.lift(I) print('1;'+serialize_polynomials(coeffs))