polyrith: a new tactic

Stream: general

[Rob Lewis]

I'm excited to announce a new mathlib tactic, polyrith! #14878 landed last night so this is now live in mathlib.

Sort of like linarith, polyrith works when you have a bunch of equality hypotheses that imply an equality goal, but you don't want to go through annoying calculation steps to explain why.

import tactic.polyrith

example (x y : ℚ) (h1 : x + y = 3) (h2 : 3*x = 7) :
  x*x*y + y*x*y + 6*x = 3*x*y + 14 :=
by polyrith

Unlike linarith, though, polyrith is a self-replacing tactic! When it finds the combination of hypotheses that prove the goal, it will suggest a call to linear_combination. So in this sense, it's kind of like library_search, in that it should never appear in finished code.

This is for a special reason. polyrith works by calling Sage, a computer algebra tool, via its web API. So it requires an active internet connection (support for local Sage coming later), and we don't want to leave these external calls in library code.

I think polyrith is unique among mathlib tactics in calling external processes. You may need to install the Python package requests if you don't have it already. And, while it's been tested on a few different systems, there may be some unforeseen engineering issues, since this is uncharted territory for mathlib. Try it out and let us know if you run into issues!

Many thanks to @Dhruv Bhatia for implementing this! Also to @Eric Wieser for substantial improvements during review, and to @Abby Goldberg for contributing linear_combination, which polyrith depends on.

[Bolton Bailey]

Cool! Does this work over any field, or just fields like \Q or \R?

[Bolton Bailey]

Is this the Gröbner basis tactic I've heard about?

[Bolton Bailey]

(judging by the "groebner" tag, I presume the answer is yes)

[Rob Lewis]

Bolton Bailey said:

Cool! Does this work over any field, or just fields like \Q or \R?

Depends on what exactly you mean by "works" :smile: it will pretend that whatever field you're working over is $\mathbb{Q}$. It uses ring for normalization and we don't have a comparable way to normalize expressions in more specific fields. With some tweaks it could report back coefficients and leave it to you to normalize yourself, but this isn't implemented yet.

[Rob Lewis]

And yes, it uses Singular's Gröbner basis computation (via Sage) to find the coefficients.

[Yaël Dillies]

Let me mention that @Shing Tak Lam has been working on a Gröbner basis implementation within Lean itself.

[Rob Lewis]

Yaël Dillies said:

Let me mention that Shing Tak Lam has been working on a Gröbner basis implementation within Lean itself.

Cool, it would be very interesting to try to hook that up to polyrith when it's ready!

[Shing Tak Lam]

Yaël Dillies said:

Let me mention that Shing Tak Lam has been working on a Gröbner basis implementation within Lean itself.

(I have an implementation in Lean 4 here which just has a basic implementation of Buchberger's algorithm. I've had a look at doing it using mathlib's mv_polynomials, but nothing so far.)

[Wrenna Robson]

Rob Lewis said:

I'm excited to announce a new mathlib tactic, polyrith! #14878 landed last night so this is now live in mathlib.

Sort of like linarith, polyrith works when you have a bunch of equality hypotheses that imply an equality goal, but you don't want to go through annoying calculation steps to explain why.

import tactic.polyrith

example (x y : ℚ) (h1 : x + y = 3) (h2 : 3*x = 7) :
  x*x*y + y*x*y + 6*x = 3*x*y + 14 :=
by polyrith

Unlike linarith, though, polyrith is a self-replacing tactic! When it finds the combination of hypotheses that prove the goal, it will suggest a call to linear_combination. So in this sense, it's kind of like library_search, in that it should never appear in finished code.

This is for a special reason. polyrith works by calling Sage, a computer algebra tool, via its web API. So it requires an active internet connection (support for local Sage coming later), and we don't want to leave these external calls in library code.

I think polyrith is unique among mathlib tactics in calling external processes. You may need to install the Python package requests if you don't have it already. And, while it's been tested on a few different systems, there may be some unforeseen engineering issues, since this is uncharted territory for mathlib. Try it out and let us know if you run into issues!

Many thanks to Dhruv Bhatia for implementing this! Also to Eric Wieser for substantial improvements during review, and to Abby Goldberg for contributing linear_combination, which polyrith depends on.

This is extremely cool.

[Bolton Bailey]

I tried to use this to prove Pascal's Hexagon theorem from the 100 theorems list, but got a server error :frown:

import tactic.polyrith
import data.real.basic

def collinear (x1 y1 x2 y2 x3 y3 : ℚ) := (x2 - x1) * (y3 - y1) = (x3 - x1) * (y2 - y1)

theorem pascal_hexagon (a b c d e f x1 y1 x2 y2 x3 y3 x4 y4 x5 y5 x6 y6 x7 y7 x8 y8 x9 y9 : ℚ)
  (h1 : a * x1 ^ 2 + b * x1 * y1 + c * y1^2 + d * x1 + e * y1 + f = 0)
  (h2 : a * x2 ^ 2 + b * x2 * y2 + c * y2^2 + d * x2 + e * y2 + f = 0)
  (h3 : a * x3 ^ 2 + b * x3 * y3 + c * y3^2 + d * x3 + e * y3 + f = 0)
  (h4 : a * x4 ^ 2 + b * x4 * y4 + c * y4^2 + d * x4 + e * y4 + f = 0)
  (h5 : a * x5 ^ 2 + b * x5 * y5 + c * y5^2 + d * x5 + e * y5 + f = 0)
  (h6 : a * x6 ^ 2 + b * x6 * y6 + c * y6^2 + d * x6 + e * y6 + f = 0)
  (h12 : collinear x1 y1 x2 y2 x7 y7)
  (h23 : collinear x2 y2 x3 y3 x8 y8)
  (h34 : collinear x3 y3 x4 y4 x9 y9)
  (h45 : collinear x4 y4 x5 y5 x7 y7)
  (h56 : collinear x5 y5 x6 y6 x8 y8)
  (h61 : collinear x6 y6 x1 y1 x9 y9) :
  collinear x7 y7 x8 y8 x9 y9 :=
begin
  unfold collinear at *,
  polyrith,
end

[Bolton Bailey]

From the end of the Lean: Server Error output:

Traceback (most recent call last):
  File "/Users/boltonbailey/Desktop/mathlibcontribution/mathlib/src/../scripts/polyrith_sage.py", line 84, in <module>
    main()
  File "/Users/boltonbailey/Desktop/mathlibcontribution/mathlib/src/../scripts/polyrith_sage.py", line 77, in main
    output = dict(success=True, data=evaluate_in_sage(final_query))
  File "/Users/boltonbailey/Desktop/mathlibcontribution/mathlib/src/../scripts/polyrith_sage.py", line 51, in evaluate_in_sage
    raise Exception(response)
Exception: {'success': False}

[Rob Lewis]

Noted, we definitely need to work on error reporting. This problem seems to be too big (or false) for Sage, at least through its web API. This is the Sage code generated for your example:

import json
P = PolynomialRing(QQ, 'var', 24)
[var0, var1, var2, var3, var4, var5, var6, var7, var8, var9, var10, var11, var12, var13, var14, var15, var16, var17, var18, var19, var20, var21, var22, var23] = P.gens()
gens = [(((((((var6 * (var7 ^ 2)) + ((var8 * var7) * var9)) + (var10 * (var9 ^ 2))) + (var11 * var7)) + (var12 * var9)) + var13) - 0), (((((((var6 * (var14 ^ 2)) + ((var8 * var14) * var15)) + (var10 * (var15 ^ 2))) + (var11 * var14)) + (var12 * var15)) + var13) - 0), (((((((var6 * (var16 ^ 2)) + ((var8 * var16) * var17)) + (var10 * (var17 ^ 2))) + (var11 * var16)) + (var12 * var17)) + var13) - 0), (((((((var6 * (var18 ^ 2)) + ((var8 * var18) * var19)) + (var10 * (var19 ^ 2))) + (var11 * var18)) + (var12 * var19)) + var13) - 0), (((((((var6 * (var20 ^ 2)) + ((var8 * var20) * var21)) + (var10 * (var21 ^ 2))) + (var11 * var20)) + (var12 * var21)) + var13) - 0), (((((((var6 * (var22 ^ 2)) + ((var8 * var22) * var23)) + (var10 * (var23 ^ 2))) + (var11 * var22)) + (var12 * var23)) + var13) - 0), (((var14 - var7) * (var3 - var9)) - ((var1 - var7) * (var15 - var9))), (((var16 - var14) * (var5 - var15)) - ((var0 - var14) * (var17 - var15))), (((var18 - var16) * (var2 - var17)) - ((var4 - var16) * (var19 - var17))), (((var20 - var18) * (var3 - var19)) - ((var1 - var18) * (var21 - var19))), (((var22 - var20) * (var5 - var21)) - ((var0 - var20) * (var23 - var21))), (((var7 - var22) * (var2 - var23)) - ((var4 - var22) * (var9 - var23)))]
p = P((((var0 - var1) * (var2 - var3)) - ((var4 - var1) * (var5 - var3))))
I = ideal(gens)
coeffs = p.lift(I)
print(json.dumps([polynomial_to_string(c) for c in coeffs]))

and pasting that into https://sagecell.sagemath.org/ times out.

[Anatole Dedecker]

For people not at ICERM, you can have a look at https://hrmacbeth.github.io/computations_in_lean/index.html

[Rob Lewis]

Anatole Dedecker said:

For people not at ICERM, you can have a look at https://hrmacbeth.github.io/computations_in_lean/index.html

Highly recommended reading! Thanks @Heather Macbeth (and @Anatole Dedecker for proofreading :smile: )

[Rob Lewis]

Rob Lewis said:

Noted, we definitely need to work on error reporting. This problem seems to be too big (or false) for Sage, at least through its web API. This is the Sage code generated for your example:

import json
P = PolynomialRing(QQ, 'var', 24)
[var0, var1, var2, var3, var4, var5, var6, var7, var8, var9, var10, var11, var12, var13, var14, var15, var16, var17, var18, var19, var20, var21, var22, var23] = P.gens()
gens = [(((((((var6 * (var7 ^ 2)) + ((var8 * var7) * var9)) + (var10 * (var9 ^ 2))) + (var11 * var7)) + (var12 * var9)) + var13) - 0), (((((((var6 * (var14 ^ 2)) + ((var8 * var14) * var15)) + (var10 * (var15 ^ 2))) + (var11 * var14)) + (var12 * var15)) + var13) - 0), (((((((var6 * (var16 ^ 2)) + ((var8 * var16) * var17)) + (var10 * (var17 ^ 2))) + (var11 * var16)) + (var12 * var17)) + var13) - 0), (((((((var6 * (var18 ^ 2)) + ((var8 * var18) * var19)) + (var10 * (var19 ^ 2))) + (var11 * var18)) + (var12 * var19)) + var13) - 0), (((((((var6 * (var20 ^ 2)) + ((var8 * var20) * var21)) + (var10 * (var21 ^ 2))) + (var11 * var20)) + (var12 * var21)) + var13) - 0), (((((((var6 * (var22 ^ 2)) + ((var8 * var22) * var23)) + (var10 * (var23 ^ 2))) + (var11 * var22)) + (var12 * var23)) + var13) - 0), (((var14 - var7) * (var3 - var9)) - ((var1 - var7) * (var15 - var9))), (((var16 - var14) * (var5 - var15)) - ((var0 - var14) * (var17 - var15))), (((var18 - var16) * (var2 - var17)) - ((var4 - var16) * (var19 - var17))), (((var20 - var18) * (var3 - var19)) - ((var1 - var18) * (var21 - var19))), (((var22 - var20) * (var5 - var21)) - ((var0 - var20) * (var23 - var21))), (((var7 - var22) * (var2 - var23)) - ((var4 - var22) * (var9 - var23)))]
p = P((((var0 - var1) * (var2 - var3)) - ((var4 - var1) * (var5 - var3))))
I = ideal(gens)
coeffs = p.lift(I)
print(json.dumps([polynomial_to_string(c) for c in coeffs]))

and pasting that into https://sagecell.sagemath.org/ times out.

Note: I extracted this using set_option trace.polyrith true. Also on the to-do list is better tracing support.

[Bolton Bailey]

or false

Indeed the issue might be that I need to rule out points being on top of one another

[Eric Wieser]

Where did the quaternion_simps come from in that tutorial?

[Rob Lewis]

Eric Wieser said:

Where did the quaternion_simps come from in that tutorial?

https://github.com/hrmacbeth/computations_in_lean/blob/main/src/02_Using_Polyrith/03_double_cover.lean#L15

[Eric Wieser]

Huh, I guess github search failed me

[Praneeth Kolichala]

We can get polyrith to work with negations of equalities as well if we add the following lemma:

lemma mul_inv_one_of_ne {k : Type*} [field k] {a b : k} (h : a ≠ b) : (a - b) * (a - b)⁻¹ = 1 :=
by simp [sub_ne_zero_of_ne h]

Then, we just need to preprocess all the parameters by applying this lemma if the argument is of the form $a \neq b$ instead of $a = b$. Is anyone working on this?

If we add this, we can do some more cool things. Here is the fact that at most one line of the form $ax + b$ goes through two distinct points proved automatically using polyrith (after unfolding definitions):

structure line := (a : ℝ) (b : ℝ)
def line.contains (l : line) (p : ℝ × ℝ) : Prop :=
p.snd = l.a * p.fst + l.b

example {x₀ x₁ y₀ y₁ : ℝ} (h : x₀ ≠ x₁) : set.subsingleton {l : line | l.contains (x₀, y₀) ∧ l.contains (x₁, y₁) } :=
by { rintros ⟨a, b⟩ ⟨H₁, H₂⟩ ⟨a', b'⟩ ⟨H₁', H₂'⟩, simp [line.contains] at *, split; polyrith [mul_inv_one_of_ne h], }

(Crucially, this relies on the fact that the x-values are different).

We could also extend it to proving goals of the form $a \neq b$ by introducing $a = b$ as a hypothesis and trying to prove $1 = 0$ (the same strategy works for proving false, although you'd have to guess what the field/ring is).

[Kevin Buzzard]

Nice! polyrith is one of those tactics which is more useful than you might expect! (modulo Heather's talk where she explained loads of uses so I should up my expectations!). I've used it several times with undergraduates in the past couple of weeks

[Rob Lewis]

@Praneeth Kolichala Cool! I have a couple WIP pull requests for polyrith and linear_combination. @Heather Macbeth and I were discussing syntax for "contraposed" linear combinations, with one disequality hypothesis and a disequality goal. I'm overcommitted and travelilng right now so don't expect much movement from me in the next week or two. But if you have ideas for how to integrate this into polyrith and want to work on it, definitely go ahead!

[Miguel Marco]

Hi,

I already wrote this in a github issue, but I am not sure if that is the right place to comment it, so just in case, i will include it here too:

to cover the case where your goal is not really in the ideal generated by your hypothesis, but in its radical, you can either use Sage's saturationmethod (which will give you the needed exponent), or write a proof for this:

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

and ask Sage for a lift of 1 to the ideal generated by your hypothesis and c*X - 1 (being c what you want to prove, and X a new variable). Then you can use Sage's answer to write the needed hypothesis (as a linear combination) and apply it.

I have a (probably suboptimal) proof of that result if you need it.

[Miguel Marco]

The second approach only needs one call to Sage, but the resulting proof might be not so clear.

[Mario Carneiro]

I'm working on polyrith now BTW. I don't really know how to implement what you suggested

[Heather Macbeth]

Hi @Miguel Marco, I think this was already implemented in the PR #15425, right?

[Heather Macbeth]

Hi @Miguel Marco, I think this was already implemented in the PR #15425, right?

[Heather Macbeth]

See this comment:
https://github.com/leanprover-community/mathlib/pull/15425#issuecomment-1201895845

[Heather Macbeth]

It's a shame the PR hasn't been merged, we don't have many people who can review meta code.

[Miguel Marco]

Let me give an example.

Say you want to prove this:

example (a b c : ℚ) (h1 : b^4  + b^2*c = 2*a*b*c^2) (h2 : b^2*c^2  + b^2 = 2*a*b*c) (h3:  c^3 = b^2) (h4:  a^2 = b^2) : a*c = b

then you rewrite your equations as polynomials being equal to zero, and send the following code to Sage:

R.<a,b,c,X> = QQ[]
I = R.ideal([b^4 - 2*a*b*c^2 + b^2*c, b^2*c^2 - 2*a*b*c + b^2, c^3 - b^2, a^2 - b^2, (a*c - b) * X -1 ])
R.one().lift(I)

and you get

[0, X^2, 0, c^2*X^2, -a*c*X + b*X - 1]

which means that

0*(b^4 - 2*a*b*c^2 + b^2*c)+X^2*(b^2*c^2 - 2*a*b*c + b^2)+0*( c^3 - b^2)+c^2*X^2*(c^3 - b^2, a^2 - b^2)+(-a*c*X + b*X - 1)*( (a*c - b) * X -1)= 1

it could be easily checked with a ring, linear_combination or similar.

Then you rewrite your starting hypothesis, and it should simplify to

(-a*c*X + b*X - 1)*( (a*c - b) * X -1)

then you apply the lemma I posted before (being f=(-a*c*X + b*X - 1) ) to conclude that (a*c - b) = 0.

[Miguel Marco]

Heather Macbeth said:

Hi Miguel Marco, I think this was already implemented in the PR #15425, right?

If I am understanding well the code in that PR, it checks if a specific power of the goal is in the idea. The advantage of the method I propose is that it proves that some power is in the ideal (and hence, it should be equal to zero modulo the hypothesis), without knowing which power.

[Heather Macbeth]

No, that was an earlier implementation (as described in the first message on the PR) -- as of the comment I linked to, the "standard trick" (which I believe is what you describe) is used.

[Heather Macbeth]

Or, perhaps indeed I'm misremembering, @Rob Lewis can confirm whether he actually implemented it or just intended to! Note the PR is currently blocked by #15428 (hint to meta code reviewers ...)

[Heather Macbeth]

Ah yes, see a later comment:

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).

[Heather Macbeth]

@Miguel Marco Are you able to review Lean meta code? Maybe you can help us get #15428 and #15425 merged!

[Heather Macbeth]

By the way, @Mario Carneiro, it seems like it would be a shame to lose this work of Rob's, which has been awaiting review since September (and which makes polyrith much more powerful). Is there any chance you could incorporate it into your polyrith port?

[Miguel Marco]

Heather Macbeth said:

No, that was an earlier implementation (as described in the first message on the PR) -- as of the comment I linked to, the "standard trick" (which I believe is what you describe) is used.

I see. Yes, it is the same idea. Although, if you are not interested in the exponent, and just want to prove that the result must be zero, you don't need to do this part:

power = max(cf.degree(aux) for cf in coeffs)
coeffs = [P(cf.subs(aux = 1/p)*p^power) for cf in coeffs[:int(-1)]]

and just apply the lemma i mentioned. However, it might be a good idea to get the exponent, since it is quite straightforward to compute, and gives you a more readable proof. It was a nice exercise to prove the lemma though :laughing:

[Miguel Marco]

Heather Macbeth said:

Miguel Marco Are you able to review Lean meta code? Maybe you can help us get #15428 and #15425 merged!

I can try to give it a look.... but have absolutely no experience with meta code. So I wouldn't trust my review, at least for the moment.

[Mario Carneiro]

Heather Macbeth said:

By the way, Mario Carneiro, it seems like it would be a shame to lose this work of Rob's, which has been awaiting review since September (and which makes polyrith much more powerful). Is there any chance you could incorporate it into your polyrith port?

Sure, but it won't make it to V1

[Miguel Marco]

I can help with the Sage/Singular side if you want though. I would be specially interested in using a local instance instead of relying on an online service.

[Eric Wieser]

Relatedly, there's another polyrith patch at #17142

[Eric Wieser]

#15428 LGTM, just needs some documentation fixes. I think I missed Rob's comment that it was ready for another round of review.

[Eric Wieser]

I can review the meta code in #15425, but if you have expertise in SageMath then your review would definitely be appreciated @Miguel Marco!

[Mario Carneiro]

Well the initial version is up at mathlib4#942. Didn't know all these extensions would come out of the woodwork today