[Merged by Bors] - feat: improve `polyrith` by testing for membership in the radical #7790

robertylewis · 2023-10-20T03:39:17Z

In @hrmacbeth 's tutorial on polyrith, there were examples of problems that it could almost solve, but failed. The goal was not expressible as a linear combination of the hypotheses but a power of the goal was.

example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 :=
sorry

Mathematically, x+y*z is in the radical of the ideal generated by x-y, x*y. There's a "standard trick" for testing membership in the radical without a search for the proper exponent: see e.g. section 2.2 of arxiv.org/pdf/1007.3615.pdf or 4.2 Prop 8 of Cox, Little, O'Shea.

This PR implements the trick in the Sage call made by polyrith. When the power returned is n > 1, we use linear_combination (exp := n) to check the certificate (#7789 ).

The polyrith test infrastructure still needs to be ported from mathlib3. All tests in the test file succeed when they are uncommented. A future PR will restore the old test suite.

Mathlib/Tactic/Polyrith.lean

digama0 · 2023-10-21T21:32:29Z

Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause lake clean to delete your mathlib folder! If you need to do so, make sure to delete lakefile.olean manually before running any lake commands.

adomani · 2023-10-26T06:52:42Z

The code is above what I actually feel that I understand, but is this testing membership in the radical or whether some explicit power of the element lies in the ideal? More explicitly, could it not be the case that a larger power than what is being used would work?

As I said, I do not really understand the code, so I hope that this question is not just noise!

robertylewis · 2023-10-26T14:40:10Z

It tests for membership in the radical.

To start, the goal is H₁ = 0, ..., Hₙ = 0 ⊢ P = 0. This follows if we can find Qᵢ and r such that Pʳ = Q₁H₁ + ... + QₙHₙ, i.e. P is in the radical of <Hᵢ>.

In Sage: introduce a new variable z and use a Grobner basis algorithm to compute hᵢ such that 1 = h₁H₁ + ... + hₙHₙ + h(1 - zP).

Take r to be the maximum power of z that appears in the hᵢs. Substitute 1/P (formally) for z and multiply 1 = h₁H₁ + ... + hₙHₙ + h(1 - zP) by Pʳ to get our desired equation: the coeffs are Qᵢ = Pʳhᵢ[z ← 1/P].

So the Grobner basis computation produces r without a search. In principle, if there is an r that works, this should find it. Of course it may be computationally infeasible.

I'm not sure that this procedure makes any claim about finding a minimal r. This must depend on the details of the Grobner basis algorithm. In practice, on all the polyrith tests, it correctly finds r = 1 (and finds a minimal r > 1 on the new tests).

adomani · 2023-10-26T14:52:14Z

Robert, thank you for the explanation! I had missed that there was a first Gröbner basis computation and then you used the degrees of the elements of that basis to get the bound on r: this clears my doubts!

In terms of improving feasibility, it may be good to have an option to ask Sage to check if the given element is a member of the ideal itself or whether it is contained in the radical: I expect these two computations to perform differently (where testing for membership in the ideal is likely often faster) and you may be satisfied with the answer to one of the two questions. I am thinking of something in the style of

polyrith -- check membership in the ideal;
polyrith! -- check membership in the radical.

Anyway, this is just a suggestion: I am very happy that polyrith even exists!

robertylewis · 2023-10-26T15:06:17Z

I thought about the two versions, but decided against it for a few reasons:

It's confusing for newcomers/people who don't want to think about how polyrith works, which is probably most people. They just want to know whether the goal is provable.
polyrith is self-replacing, so minor slowdowns don't matter nearly as much as for tactics that will remain source code.
It's not even clear to me that the radical problem is significantly slower on average. The computation has one more variable and similar degree. Grobner basis algorithms are fickle and adding an option to use a different term order would probably help a lot more than falling back to the original non-radical check.
Some non-scientific testing at the end of feat(tactic/polyrith): solve more problems by testing for membership in the radical mathlib3#15425 indicated that there's not much/any slowdown, although this isn't a strong data point!

adomani · 2023-10-26T15:17:04Z

Rob, thanks for the further comments! I agree that specifying term orders normally has a much larger impact on feasibility of a Gröbner basis computation!

Thanks for taking the time to explain: it turns out that my comments were indeed noise, but I am grateful for the explanations, since they taught me something!

alexjbest · 2023-11-03T13:03:45Z

scripts/polyrith_sage.py

+    [{", ".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))


I don't really understand why this is done with this trick of checking if 1 is in the ideal <hyps, 1/goal>, I would expect singular/sage has a way to ask for a lift to the radical ideal directly which I would hope would be easier to maintain in the long run (especially if we have aspirations of making this work for non-char 0 rings properly). Did you consider this approach?
I'm not completely against merging this, but the whole thing is starting to look a bit scary ;)

After experimenting a bit I believe that using the builtin radical support, while probably a better algorithm underneath, is not very convenient to use with the way things are set up here, so I'm happy with this I guess

Yeah, I remember looking for this when I first implemented this (granted, a year and a half ago) and not turning up anything useful. Sage/Singular will check for membership in the radical just fine but extracting the power and coefficient is a pain. My impression is that what I do in this PR is a "standard" approach and that a native Sage implementation would do roughly the same, although I'm somewhat out of my element here.

When I read the sage docstring for radical earlier it said:

From the Singular manual: A combination of the algorithms of Krick/Logar and Kemper is used. Works also in positive characteristic (Kempers algorithm).

but I have no idea how accurate that is!

Right -- but there's space between the membership check $p \in \sqrt{\langle H_1, \ldots, H_n \rangle}$, and explicitly producing $k$ and $Q_i$ such that $p^k = \sum Q_iH_i$. Sage's radical makes the former easy, but I don't see how to get from there to the latter. Maybe there's a way, I'd love to hear it.

(It sounds like you came to a similar conclusion, just leaving this comment for reference later!)

scripts/polyrith_sage.py

alexjbest · 2023-11-03T18:27:23Z

maintainer merge

github-actions · 2023-11-03T18:27:35Z

🚀 Pull request has been placed on the maintainer queue by alexjbest.

robertylewis · 2023-11-07T17:37:14Z

bors merge

@hrmacbeth

) In @hrmacbeth 's tutorial on `polyrith`, there were examples of problems that it could almost solve, but failed. The goal was not expressible as a linear combination of the hypotheses but a power of the goal was. ```lean example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 := sorry ``` Mathematically, `x+y*z` is in the radical of the ideal generated by `x-y, x*y`. There's a "standard trick" for testing membership in the radical without a search for the proper exponent: see e.g. section 2.2 of [arxiv.org/pdf/1007.3615.pdf](https://arxiv.org/pdf/1007.3615.pdf) or 4.2 Prop 8 of Cox, Little, O'Shea. This PR implements the trick in the Sage call made by `polyrith`. When the power returned is `n > 1`, we use `linear_combination (exp := n)` to check the certificate (#7789 ). The `polyrith` test infrastructure still needs to be ported from mathlib3. All tests in the test file succeed when they are uncommented. A future PR will restore the old test suite. Co-authored-by: Rob Lewis <[email protected]> Co-authored-by: Mario Carneiro <[email protected]>

mathlib-bors · 2023-11-07T18:02:34Z

Pull request successfully merged into master.

Build succeeded:

@hrmacbeth

) In @hrmacbeth 's tutorial on `polyrith`, there were examples of problems that it could almost solve, but failed. The goal was not expressible as a linear combination of the hypotheses but a power of the goal was. ```lean example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 := sorry ``` Mathematically, `x+y*z` is in the radical of the ideal generated by `x-y, x*y`. There's a "standard trick" for testing membership in the radical without a search for the proper exponent: see e.g. section 2.2 of [arxiv.org/pdf/1007.3615.pdf](https://arxiv.org/pdf/1007.3615.pdf) or 4.2 Prop 8 of Cox, Little, O'Shea. This PR implements the trick in the Sage call made by `polyrith`. When the power returned is `n > 1`, we use `linear_combination (exp := n)` to check the certificate (#7789 ). The `polyrith` test infrastructure still needs to be ported from mathlib3. All tests in the test file succeed when they are uncommented. A future PR will restore the old test suite. Co-authored-by: Rob Lewis <[email protected]> Co-authored-by: Mario Carneiro <[email protected]>

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 <[email protected]>

robertylewis added 7 commits October 19, 2023 21:43

remove unused config object

67e53ae

add exp option to linear_combination

acbdf91

fix style lint

4006550

update docs

5278e4d

start on extending polyrith

74c822d

wip

93445f9

complete and add tests

8d7e896

robertylewis added the t-meta Tactics, attributes or user commands label Oct 20, 2023

Merge branch 'master' into polyrith-radical

e4685b3

leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Oct 20, 2023

Merge branch 'master' into polyrith-radical

1a199f9

robertylewis added the awaiting-review label Oct 20, 2023

robertylewis commented Oct 20, 2023

View reviewed changes

Mathlib/Tactic/Polyrith.lean Show resolved Hide resolved

Mathlib/Tactic/Polyrith.lean Show resolved Hide resolved

robertylewis and others added 3 commits October 20, 2023 09:01

Apply suggestions from code review

c30c045

docs

bc33e63

chore: bump lean toolchain

d8873f0

robertylewis added 2 commits October 22, 2023 08:48

Merge branch 'master' into polyrith-radical

0a410d0

remove debug code

bbcb66d

alexjbest reviewed Nov 3, 2023

View reviewed changes

eric-wieser reviewed Nov 3, 2023

View reviewed changes

scripts/polyrith_sage.py Show resolved Hide resolved

expand comment about workaround case

677d35e

sgouezel added this pull request to the merge queue Nov 7, 2023

github-merge-queue bot removed this pull request from the merge queue due to no response for status checks Nov 7, 2023

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 7, 2023

mathlib-bors bot changed the title ~~feat: improve polyrith by testing for membership in the radical~~ [Merged by Bors] - feat: improve polyrith by testing for membership in the radical Nov 7, 2023

mathlib-bors bot closed this Nov 7, 2023

mathlib-bors bot deleted the polyrith-radical branch November 7, 2023 18:02

eric-wieser mentioned this pull request Mar 23, 2024

feat(tactic/polyrith): solve more problems by testing for membership in the radical leanprover-community/mathlib3#15425

Closed

1 task

robertylewis mentioned this pull request May 23, 2024

[Merged by Bors] - fix: make polyrith succeed when target is identically zero #13150

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: improve `polyrith` by testing for membership in the radical #7790

[Merged by Bors] - feat: improve `polyrith` by testing for membership in the radical #7790

robertylewis commented Oct 20, 2023 •

edited by sgouezel

Loading

digama0 commented Oct 21, 2023

adomani commented Oct 26, 2023 •

edited

Loading

robertylewis commented Oct 26, 2023

adomani commented Oct 26, 2023 •

edited

Loading

robertylewis commented Oct 26, 2023 •

edited

Loading

adomani commented Oct 26, 2023

alexjbest Nov 3, 2023 •

edited

Loading

alexjbest Nov 3, 2023

robertylewis Nov 3, 2023

alexjbest Nov 3, 2023

robertylewis Nov 4, 2023

alexjbest commented Nov 3, 2023

github-actions bot commented Nov 3, 2023

robertylewis commented Nov 7, 2023

mathlib-bors bot commented Nov 7, 2023

[Merged by Bors] - feat: improve polyrith by testing for membership in the radical #7790

[Merged by Bors] - feat: improve polyrith by testing for membership in the radical #7790

Conversation

robertylewis commented Oct 20, 2023 • edited by sgouezel Loading

digama0 commented Oct 21, 2023

adomani commented Oct 26, 2023 • edited Loading

robertylewis commented Oct 26, 2023

adomani commented Oct 26, 2023 • edited Loading

robertylewis commented Oct 26, 2023 • edited Loading

adomani commented Oct 26, 2023

alexjbest Nov 3, 2023 • edited Loading

Choose a reason for hiding this comment

alexjbest Nov 3, 2023

Choose a reason for hiding this comment

robertylewis Nov 3, 2023

Choose a reason for hiding this comment

alexjbest Nov 3, 2023

Choose a reason for hiding this comment

robertylewis Nov 4, 2023

Choose a reason for hiding this comment

alexjbest commented Nov 3, 2023

github-actions bot commented Nov 3, 2023

robertylewis commented Nov 7, 2023

mathlib-bors bot commented Nov 7, 2023

[Merged by Bors] - feat: improve `polyrith` by testing for membership in the radical #7790

[Merged by Bors] - feat: improve `polyrith` by testing for membership in the radical #7790

robertylewis commented Oct 20, 2023 •

edited by sgouezel

Loading

adomani commented Oct 26, 2023 •

edited

Loading

adomani commented Oct 26, 2023 •

edited

Loading

robertylewis commented Oct 26, 2023 •

edited

Loading

alexjbest Nov 3, 2023 •

edited

Loading