too big for `ring`

Stream: maths

[Kevin Buzzard]

(y * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - (3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) * (x * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - ((3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) ^ 2 + E.a1 * (3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) * (2 * y + E.a1 * x + E.a3) - E.a2 * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - 2 * x * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3)))) ^ 2 + (2 * y + E.a1 * x + E.a3) * E.a1 * ((3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) ^ 2 + E.a1 * (3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) * (2 * y + E.a1 * x + E.a3) - E.a2 * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - 2 * x * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3)) * (y * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - (3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) * (x * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - ((3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) ^ 2 + E.a1 * (3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) * (2 * y + E.a1 * x + E.a3) - E.a2 * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - 2 * x * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3)))) + (2 * y + E.a1 * x + E.a3) ^ 3 * E.a3 * (y * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - (3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) * (x * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - ((3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) ^ 2 + E.a1 * (3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) * (2 * y + E.a1 * x + E.a3) - E.a2 * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - 2 * x * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3)))) - (((3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) ^ 2 + E.a1 * (3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) * (2 * y + E.a1 * x + E.a3) - E.a2 * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - 2 * x * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3)) ^ 3 + (2 * y + E.a1 * x + E.a3) ^ 2 * E.a2 * ((3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) ^ 2 + E.a1 * (3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) * (2 * y + E.a1 * x + E.a3) - E.a2 * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - 2 * x * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3)) ^ 2 + (2 * y + E.a1 * x + E.a3) ^ 4 * E.a4 * ((3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) ^ 2 + E.a1 * (3 * x ^ 2 + 2 * E.a2 * x + E.a4 - E.a1 * y) * (2 * y + E.a1 * x + E.a3) - E.a2 * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3) - 2 * x * (2 * y + E.a1 * x + E.a3) * (2 * y + E.a1 * x + E.a3)) + (2 * y + E.a1 * x + E.a3) ^ 6 * E.a6) = (y ^ 2 + E.a1 * x * y + E.a3 * y - (x ^ 3 + E.a2 * x ^ 2 + E.a4 * x + E.a6)) * (64 * y ^ 6 + (192 * E.a1 * x + 192 * E.a3) * y ^ 5 + (240 * E.a1 ^ 2 * x ^ 2 + 480 * E.a1 * E.a3 * x + 240 * E.a3 ^ 2) * y ^ 4 + (160 * E.a1 ^ 3 * x ^ 3 + 480 * E.a1 ^ 2 * E.a3 * x ^ 2 + 480 * E.a1 * E.a3 ^ 2 * x + 160 * E.a3 ^ 3) * y ^ 3 + (60 * E.a1 ^ 4 * x ^ 4 + 240 * E.a1 ^ 3 * E.a3 * x ^ 3 + 360 * E.a1 ^ 2 * E.a3 ^ 2 * x ^ 2 + 240 * E.a1 * E.a3 ^ 3 * x + 60 * E.a3 ^ 4) * y ^ 2 + (12 * E.a1 ^ 5 * x ^ 5 + 60 * E.a1 ^ 4 * E.a3 * x ^ 4 + 120 * E.a1 ^ 3 * E.a3 ^ 2 * x ^ 3 + 120 * E.a1 ^ 2 * E.a3 ^ 3 * x ^ 2 + 60 * E.a1 * E.a3 ^ 4 * x + 12 * E.a3 ^ 5) * y + E.a1 ^ 6 * x ^ 6 + 6 * E.a1 ^ 5 * E.a3 * x ^ 5 + 15 * E.a1 ^ 4 * E.a3 ^ 2 * x ^ 4 + 20 * E.a1 ^ 3 * E.a3 ^ 3 * x ^ 3 + 15 * E.a1 ^ 2 * E.a3 ^ 4 * x ^ 2 + 6 * E.a1 * E.a3 ^ 5 * x + E.a3 ^ 6)

This says X = Y; an identity in a ring (here k is a field and x,y, E.a1, E.a2, E.a3, E.a4, E.a6 are elements of k and ring in theory solves it). But ring times out. This is the assertion that if P is a point on an elliptic curve, then 2P is also on the curve. Any tips?

[Sebastien Gouezel]

#mwe? :)

[Kevin Buzzard]

0=0

[Sebastien Gouezel]

If you give a self-contained example that Mario can cut and paste, he will find the performance bottleneck in ring for you and solve it in three minutes. If you don't give the self-contained example, you're on your own :-)

[Kevin Buzzard]

aargh

[Kevin Buzzard]

I made a MWE and Lean solves it!

[Kenny Lau]

then why can't you just use the extracted lemma?

[Kevin Buzzard]

no, it's 50-50

import tactic


variables (k : Type) [field k] (a1 a2 a3 a4 a6 x y : k)

example : (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) ^ 2 + (2 * y + a1 * x + a3) * a1 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) * (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) + (2 * y + a1 * x + a3) ^ 3 * a3 * (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) - (((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) ^ 3 + (2 * y + a1 * x + a3) ^ 2 * a2 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) ^ 2 + (2 * y + a1 * x + a3) ^ 4 * a4 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) + (2 * y + a1 * x + a3) ^ 6 * a6) = (y ^ 2 + a1 * x * y + a3 * y - (x ^ 3 + a2 * x ^ 2 + a4 * x + a6)) * (64 * y ^ 6 + (192 * a1 * x + 192 * a3) * y ^ 5 + (240 * a1 ^ 2 * x ^ 2 + 480 * a1 * a3 * x + 240 * a3 ^ 2) * y ^ 4 + (160 * a1 ^ 3 * x ^ 3 + 480 * a1 ^ 2 * a3 * x ^ 2 + 480 * a1 * a3 ^ 2 * x + 160 * a3 ^ 3) * y ^ 3 + (60 * a1 ^ 4 * x ^ 4 + 240 * a1 ^ 3 * a3 * x ^ 3 + 360 * a1 ^ 2 * a3 ^ 2 * x ^ 2 + 240 * a1 * a3 ^ 3 * x + 60 * a3 ^ 4) * y ^ 2 + (12 * a1 ^ 5 * x ^ 5 + 60 * a1 ^ 4 * a3 * x ^ 4 + 120 * a1 ^ 3 * a3 ^ 2 * x ^ 3 + 120 * a1 ^ 2 * a3 ^ 3 * x ^ 2 + 60 * a1 * a3 ^ 4 * x + 12 * a3 ^ 5) * y + a1 ^ 6 * x ^ 6 + 6 * a1 ^ 5 * a3 * x ^ 5 + 15 * a1 ^ 4 * a3 ^ 2 * x ^ 4 + 20 * a1 ^ 3 * a3 ^ 3 * x ^ 3 + 15 * a1 ^ 2 * a3 ^ 4 * x ^ 2 + 6 * a1 * a3 ^ 5 * x + a3 ^ 6)
:= begin
  ring,
end

[Rob Lewis]

I should point out #2672 in case Mario takes a look at this. It could be that in disguise here.

[Rob Lewis]

(I forgot about the issue myself and never looked into it.)

[Kevin Buzzard]

OK so if I cut and paste the above, I get a pretty much guaranteed deterministic time-out. However if I replace ring by sorry and then add ring above, I get "tactic failed: there are no goals to be solved" on the sorry

[Kevin Buzzard]

Deleting the sorry of course makes it time out again :rolling_on_the_floor_laughing:

[Reid Barton]

does that mean ring succeeds but the kernel is timing out typechecking the resulting term?

[Kevin Buzzard]

import tactic


variables (k : Type) [field k] (a1 a2 a3 a4 a6 x y : k)

example : (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) ^ 2 + (2 * y + a1 * x + a3) * a1 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) * (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) + (2 * y + a1 * x + a3) ^ 3 * a3 * (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) - (((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) ^ 3 + (2 * y + a1 * x + a3) ^ 2 * a2 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) ^ 2 + (2 * y + a1 * x + a3) ^ 4 * a4 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) + (2 * y + a1 * x + a3) ^ 6 * a6) = (y ^ 2 + a1 * x * y + a3 * y - (x ^ 3 + a2 * x ^ 2 + a4 * x + a6)) * (64 * y ^ 6 + (192 * a1 * x + 192 * a3) * y ^ 5 + (240 * a1 ^ 2 * x ^ 2 + 480 * a1 * a3 * x + 240 * a3 ^ 2) * y ^ 4 + (160 * a1 ^ 3 * x ^ 3 + 480 * a1 ^ 2 * a3 * x ^ 2 + 480 * a1 * a3 ^ 2 * x + 160 * a3 ^ 3) * y ^ 3 + (60 * a1 ^ 4 * x ^ 4 + 240 * a1 ^ 3 * a3 * x ^ 3 + 360 * a1 ^ 2 * a3 ^ 2 * x ^ 2 + 240 * a1 * a3 ^ 3 * x + 60 * a3 ^ 4) * y ^ 2 + (12 * a1 ^ 5 * x ^ 5 + 60 * a1 ^ 4 * a3 * x ^ 4 + 120 * a1 ^ 3 * a3 ^ 2 * x ^ 3 + 120 * a1 ^ 2 * a3 ^ 3 * x ^ 2 + 60 * a1 * a3 ^ 4 * x + 12 * a3 ^ 5) * y + a1 ^ 6 * x ^ 6 + 6 * a1 ^ 5 * a3 * x ^ 5 + 15 * a1 ^ 4 * a3 ^ 2 * x ^ 4 + 20 * a1 ^ 3 * a3 ^ 3 * x ^ 3 + 15 * a1 ^ 2 * a3 ^ 4 * x ^ 2 + 6 * a1 * a3 ^ 5 * x + a3 ^ 6)
:= begin
  ring,
  sorry, -- tactic failed, there are no goals to be solved
end

Lean challenge -- remove the sorry

[Sebastien Gouezel]

It works on my computer. More precisely,

import tactic

set_option profiler true

variables (k : Type) [field k] (a1 a2 a3 a4 a6 x y : k)

lemma foo :
  (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) ^ 2 + (2 * y + a1 * x + a3) * a1 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) * (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) + (2 * y + a1 * x + a3) ^ 3 * a3 * (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) - (((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) ^ 3 + (2 * y + a1 * x + a3) ^ 2 * a2 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) ^ 2 + (2 * y + a1 * x + a3) ^ 4 * a4 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) + (2 * y + a1 * x + a3) ^ 6 * a6) = (y ^ 2 + a1 * x * y + a3 * y - (x ^ 3 + a2 * x ^ 2 + a4 * x + a6)) * (64 * y ^ 6 + (192 * a1 * x + 192 * a3) * y ^ 5 + (240 * a1 ^ 2 * x ^ 2 + 480 * a1 * a3 * x + 240 * a3 ^ 2) * y ^ 4 + (160 * a1 ^ 3 * x ^ 3 + 480 * a1 ^ 2 * a3 * x ^ 2 + 480 * a1 * a3 ^ 2 * x + 160 * a3 ^ 3) * y ^ 3 + (60 * a1 ^ 4 * x ^ 4 + 240 * a1 ^ 3 * a3 * x ^ 3 + 360 * a1 ^ 2 * a3 ^ 2 * x ^ 2 + 240 * a1 * a3 ^ 3 * x + 60 * a3 ^ 4) * y ^ 2 + (12 * a1 ^ 5 * x ^ 5 + 60 * a1 ^ 4 * a3 * x ^ 4 + 120 * a1 ^ 3 * a3 ^ 2 * x ^ 3 + 120 * a1 ^ 2 * a3 ^ 3 * x ^ 2 + 60 * a1 * a3 ^ 4 * x + 12 * a3 ^ 5) * y + a1 ^ 6 * x ^ 6 + 6 * a1 ^ 5 * a3 * x ^ 5 + 15 * a1 ^ 4 * a3 ^ 2 * x ^ 4 + 20 * a1 ^ 3 * a3 ^ 3 * x ^ 3 + 15 * a1 ^ 2 * a3 ^ 4 * x ^ 2 + 6 * a1 * a3 ^ 5 * x + a3 ^ 6)
:= begin
  ring,
end

works, and the profiler says

parsing took 10.3ms
local_homeomorph.lean:16:6
type checking of foo took 0.565ms
local_homeomorph.lean:16:6
decl post-processing of foo took 0.0029ms
local_homeomorph.lean:16:6
elaboration of foo took 9.51s

but once the profiler message appears, there are still 40s more before the orange bar disappears.

[Kevin Buzzard]

Oh maybe I need to change my timeoutometer

[Sebastien Gouezel]

The timeout is set in my vscode to 300000.

[Kevin Buzzard]

mine to 100000

[Mario Carneiro]

you know there are line length limits ;P

[Mario Carneiro]

it would be great if this example was minimized

[Sebastien Gouezel]

Don't you think it's just the size of the question that it problematic, and that this will be hard to minimize without killing the issue?

[Mario Carneiro]

Unlikely. The time to run ring should be the majority of the time, if all goes well

[Sebastien Gouezel]

The output of #print foo is very cute, but unfortunately it's too long so it's truncated and I can't try to feed it directly as a proof term, to see if the problem comes from the kernel checking the term. Is there a way to get the untruncated term?

[Rob Lewis]

It is indeed something going wrong at QED time. The following works fine, using ring to prove the goal and confirming that the proof type checks.

import tactic

open tactic
meta def type_check_proof : tactic unit :=
do t ← target,
   (_, pf) ← solve_aux t `[ring],
    type_check pf,
   trace "good"

variables (k : Type) [field k] (a1 a2 a3 a4 a6 x y : k)


lemma foo :
  (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) ^ 2 + (2 * y + a1 * x + a3) * a1 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) * (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) + (2 * y + a1 * x + a3) ^ 3 * a3 * (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) - (((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) ^ 3 + (2 * y + a1 * x + a3) ^ 2 * a2 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) ^ 2 + (2 * y + a1 * x + a3) ^ 4 * a4 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) + (2 * y + a1 * x + a3) ^ 6 * a6) = (y ^ 2 + a1 * x * y + a3 * y - (x ^ 3 + a2 * x ^ 2 + a4 * x + a6)) * (64 * y ^ 6 + (192 * a1 * x + 192 * a3) * y ^ 5 + (240 * a1 ^ 2 * x ^ 2 + 480 * a1 * a3 * x + 240 * a3 ^ 2) * y ^ 4 + (160 * a1 ^ 3 * x ^ 3 + 480 * a1 ^ 2 * a3 * x ^ 2 + 480 * a1 * a3 ^ 2 * x + 160 * a3 ^ 3) * y ^ 3 + (60 * a1 ^ 4 * x ^ 4 + 240 * a1 ^ 3 * a3 * x ^ 3 + 360 * a1 ^ 2 * a3 ^ 2 * x ^ 2 + 240 * a1 * a3 ^ 3 * x + 60 * a3 ^ 4) * y ^ 2 + (12 * a1 ^ 5 * x ^ 5 + 60 * a1 ^ 4 * a3 * x ^ 4 + 120 * a1 ^ 3 * a3 ^ 2 * x ^ 3 + 120 * a1 ^ 2 * a3 ^ 3 * x ^ 2 + 60 * a1 * a3 ^ 4 * x + 12 * a3 ^ 5) * y + a1 ^ 6 * x ^ 6 + 6 * a1 ^ 5 * a3 * x ^ 5 + 15 * a1 ^ 4 * a3 ^ 2 * x ^ 4 + 20 * a1 ^ 3 * a3 ^ 3 * x ^ 3 + 15 * a1 ^ 2 * a3 ^ 4 * x ^ 2 + 6 * a1 * a3 ^ 5 * x + a3 ^ 6)
:= begin
   type_check_proof,
end

[Mario Carneiro]

does it work if you try to create an auxiliary definition using the term that ring creates (e.g. using abstract)?

[Rob Lewis]

@Sebastien Gouezel you can trace pf in the code I wrote above to see the full proof term.

[Rob Lewis]

Indeed, this works (slowly).

import tactic

open tactic
meta def type_check_proof : tactic unit :=
do t ← target,
   (_, pf) ← solve_aux t `[ring],
    type_check pf,
    tp ← infer_type pf,
    trace tp,
    is_def_eq tp t,
   abstract (exact pf),
   trace "good"


variables (k : Type) [field k] (a1 a2 a3 a4 a6 x y : k)

lemma foo :
  (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) ^ 2 + (2 * y + a1 * x + a3) * a1 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) * (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) + (2 * y + a1 * x + a3) ^ 3 * a3 * (y * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)))) - (((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) ^ 3 + (2 * y + a1 * x + a3) ^ 2 * a2 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) ^ 2 + (2 * y + a1 * x + a3) ^ 4 * a4 * ((3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) ^ 2 + a1 * (3 * x ^ 2 + 2 * a2 * x + a4 - a1 * y) * (2 * y + a1 * x + a3) - a2 * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3) - 2 * x * (2 * y + a1 * x + a3) * (2 * y + a1 * x + a3)) + (2 * y + a1 * x + a3) ^ 6 * a6) = (y ^ 2 + a1 * x * y + a3 * y - (x ^ 3 + a2 * x ^ 2 + a4 * x + a6)) * (64 * y ^ 6 + (192 * a1 * x + 192 * a3) * y ^ 5 + (240 * a1 ^ 2 * x ^ 2 + 480 * a1 * a3 * x + 240 * a3 ^ 2) * y ^ 4 + (160 * a1 ^ 3 * x ^ 3 + 480 * a1 ^ 2 * a3 * x ^ 2 + 480 * a1 * a3 ^ 2 * x + 160 * a3 ^ 3) * y ^ 3 + (60 * a1 ^ 4 * x ^ 4 + 240 * a1 ^ 3 * a3 * x ^ 3 + 360 * a1 ^ 2 * a3 ^ 2 * x ^ 2 + 240 * a1 * a3 ^ 3 * x + 60 * a3 ^ 4) * y ^ 2 + (12 * a1 ^ 5 * x ^ 5 + 60 * a1 ^ 4 * a3 * x ^ 4 + 120 * a1 ^ 3 * a3 ^ 2 * x ^ 3 + 120 * a1 ^ 2 * a3 ^ 3 * x ^ 2 + 60 * a1 * a3 ^ 4 * x + 12 * a3 ^ 5) * y + a1 ^ 6 * x ^ 6 + 6 * a1 ^ 5 * a3 * x ^ 5 + 15 * a1 ^ 4 * a3 ^ 2 * x ^ 4 + 20 * a1 ^ 3 * a3 ^ 3 * x ^ 3 + 15 * a1 ^ 2 * a3 ^ 4 * x ^ 2 + 6 * a1 * a3 ^ 5 * x + a3 ^ 6)
:= begin
  type_check_proof,
end

[Sebastien Gouezel]

Yes, but the output I get when adding the line trace pf is truncated, ending with

           …)
         y
         1
         …)
      …
      …
      …
      …
      …)).trans

[Rob Lewis]

Oh. set_option pp.max_depth 10000 or something?

[Sebastien Gouezel]

Thanks. It turned out to be pp.max_steps. But the term is just too big (I just got excessive memory consumption, that I hadn't seen in a long time since I have reasonable defaults)...

[Mario Carneiro]

So the title should be "ring too big for lean" instead?

[Reid Barton]

one cheap way to "minimize" is stuff like

  have : a1 = 0 := sorry,
  subst a1,
  simp only [add_zero, zero_add, mul_zero, zero_mul],
  ring,