feat(tactic/polyrith): solve more problems by testing for membership in the radical

[robertylewis]

In @hrmacbeth 's tutorial, there were examples of problems that polyrith 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. Sage can compute the radical and test for membership. Once it's confirmed that some power of the goal is in the ideal, we can count up until we find which power it is. The certificate returned is an application of pow_eq_zero with this power, then a call to linear_combination like normal.

example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 :=
begin
  refine pow_eq_zero' 2 _; -- goal: (x + y*z)^2 = 0
  linear_combination ((-1) * y * z ^ 2 + 1 * x) * h + (1 * z ^ 2 + 2 * z + 1) * h2
end

There's an open question here: instead of a boolean test for membership in the radical, then naively testing every power for membership in the original ideal, is there a way to extract the power more efficiently during the computation of the radical? This is both a mathematical question and a Sage/Singular API question.

But in any case, the naive approach works on small enough problems (the degree 6 example from Heather's tutorial spends 400ms calling Sage including the communcation overhead), and should have no effect on performance in the cases polyrith already solves.

---

• depends on: [Merged by Bors] - feat(tactic/linear_combination): allow linear_combination with { exponent := n } #15428

Tests do not build yet. #15292 also affects the tests output. I'll update this one when that one is merged, or stack them if/when I have the energy.

[erdOne]

I might not know what I am talking about, but it might be possible to perform some kind of binary search on the exponent in the range of say 1~64 if you have 7 queries available and testing for large polynomials isn't that much more costly than small ones?

[robertylewis]

I might not know what I am talking about, but it might be possible to perform some kind of binary search on the exponent in the range of say 1~64 if you have 7 queries available and testing for large polynomials isn't that much more costly than small ones?

Interesting thought! This assumes that 64 (or whatever we choose) is high enough for most of the problems we see and that the exponents are approximately uniformly distributed in that range. I'd guess (without any evidence) that in typical problems, very low exponents will be more common. But this is really just a gut feeling and I have no test suite of typical problems to check. I'd also have to think about how the ideal membership test scales with the exponent. There is a cost there but I don't know how severe.

[tb65536]

If you're going to binary search, would it make more sense to just repeatedly double the exponent?

[robertylewis]

It turns out there's a "standard trick" for doing this without search: see e.g. section 2.2 of https://arxiv.org/pdf/1007.3615.pdf . I'll investigate whether Sage/Singular supports this trick out of the box or if we need to implement it ourselves. Marking this PR as WIP for now.

[tb65536]

It turns out there's a "standard trick" for doing this without search: see e.g. section 2.2 of https://arxiv.org/pdf/1007.3615.pdf . I'll investigate whether Sage/Singular supports this trick out of the box or if we need to implement it ourselves. Marking this PR as WIP for now.

Ooh, that's clever!

[robertylewis]

Note to self, the json changes here will need to be adapted when #15429 lands.

[robertylewis]

I've implemented the "standard trick" (see also 4.2 Prop 8 of Cox, Little, O'Shea). This is still pending docs, test updates, and #15428 (which I think is ready to go).

While this approach is clearly better overall than the old "search up" approach, there's one downside, namely, it doesn't fall back to the old behavior in the common case where the exponent is 1. Instead we solve a more general problem and deduce from that that n = 1. I don't know how bad of a performance hit this is -- grobner basis computations are hard to predict. The alternative is to keep polyrith using the old behavior and add polyrith! for the new fancy version.

[eric-wieser]

It looks like you've accidentally rebased master on top of your branch, as there are 170 commits now!

[robertylewis]

Yes, there were merge conflicts with #15429 and I didn't resolve cleanly, apparently. This is effectively a reset of the PR -- the new implementation is unrelated to the old. I'll squash and force push before cleaning up the rest.

cd8620d is the relevant commit.

[robertylewis]

And I've marked this awaiting-review mostly for comments on:

While this approach is clearly better overall than the old "search up" approach, there's one downside, namely, it doesn't fall back to the old behavior in the common case where the exponent is 1. Instead we solve a more general problem and deduce from that that n = 1. I don't know how bad of a performance hit this is -- grobner basis computations are hard to predict. The alternative is to keep polyrith using the old behavior and add polyrith! for the new fancy version.

[miguelmarco]

There's an open question here: instead of a boolean test for membership in the radical, then naively testing every power for membership in the original ideal, is there a way to extract the power more efficiently during the computation of the radical? This is both a mathematical question and a Sage/Singular API question.

One possible way is to use the saturation method to get the needed exponent.

[miguelmarco]

Also, you could include a proof of this result:

example {F : Type} [field F] (c : F) (f : polynomial F) (rel : f * (c • X -1) = 1)  : c = 0 

and ask sage for a lift to the ideal generated by the hypothesis plus c*X - 1 (being X an extra variable). Then you can use sage's answer to create a proof of the needed hypothesis, and apply it.

[miguelmarco]

While this approach is clearly better overall than the old "search up" approach, there's one downside, namely, it doesn't fall back to the old behavior in the common case where the exponent is 1. Instead we solve a more general problem and deduce from that that n = 1. I don't know how bad of a performance hit this is -- grobner basis computations are hard to predict. The alternative is to keep polyrith using the old behavior and add polyrith! for the new fancy version.

I have done some simple benchmarking with five variables, and it doesn't seem to be a problem. When the previous method was fast (say, in the order of few seconds or less), the new method was also fast. In fact, in many instances it even happens that the new method is (way) faster!

So it is perfectly possible that the new behaviour would be preferable for the speed boost alone.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(tactic/linear_combination): allow linear_combination with { exponent := n } #15428
  By Dependent Issues (🤖). Happy coding!

[eric-wieser]

Closing, since this was implemented in leanprover-community/mathlib4#7790