Zulip Chat Archive

Stream: maths

Topic: too big for `ring`


view this post on Zulip Kevin Buzzard (Jul 14 2020 at 11:46):

(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?

view this post on Zulip Sebastien Gouezel (Jul 14 2020 at 11:47):

#mwe? :)

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 11:47):

0=0

view this post on Zulip Sebastien Gouezel (Jul 14 2020 at 11:48):

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

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 11:49):

aargh

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 11:49):

I made a MWE and Lean solves it!

view this post on Zulip Kenny Lau (Jul 14 2020 at 11:50):

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

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 11:50):

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

view this post on Zulip Rob Lewis (Jul 14 2020 at 11:50):

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

view this post on Zulip Rob Lewis (Jul 14 2020 at 11:50):

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

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 11:52):

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

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 11:53):

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

view this post on Zulip Reid Barton (Jul 14 2020 at 11:54):

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

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 11:54):

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

view this post on Zulip Sebastien Gouezel (Jul 14 2020 at 12:03):

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.

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 12:03):

Oh maybe I need to change my timeoutometer

view this post on Zulip Sebastien Gouezel (Jul 14 2020 at 12:04):

The timeout is set in my vscode to 300000.

view this post on Zulip Kevin Buzzard (Jul 14 2020 at 12:04):

mine to 100000

view this post on Zulip Mario Carneiro (Jul 14 2020 at 12:08):

you know there are line length limits ;P

view this post on Zulip Mario Carneiro (Jul 14 2020 at 12:09):

it would be great if this example was minimized

view this post on Zulip Sebastien Gouezel (Jul 14 2020 at 12:10):

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?

view this post on Zulip Mario Carneiro (Jul 14 2020 at 12:11):

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

view this post on Zulip Sebastien Gouezel (Jul 14 2020 at 12:14):

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?

view this post on Zulip Rob Lewis (Jul 14 2020 at 12:16):

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

view this post on Zulip Mario Carneiro (Jul 14 2020 at 12:17):

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

view this post on Zulip Rob Lewis (Jul 14 2020 at 12:17):

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

view this post on Zulip Rob Lewis (Jul 14 2020 at 12:20):

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

view this post on Zulip Sebastien Gouezel (Jul 14 2020 at 12:20):

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

           )
         y
         1
         )
      
      
      
      
      )).trans

view this post on Zulip Rob Lewis (Jul 14 2020 at 12:21):

Oh. set_option pp.max_depth 10000 or something?

view this post on Zulip Sebastien Gouezel (Jul 14 2020 at 12:31):

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

view this post on Zulip Mario Carneiro (Jul 14 2020 at 13:01):

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

view this post on Zulip Reid Barton (Jul 14 2020 at 13:31):

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,

Last updated: May 14 2021 at 19:21 UTC