Zulip Chat Archive

Stream: new members

Topic: question about field_simp


view this post on Zulip Jz Pan (Dec 23 2020 at 12:03):

I'd like to prove the following result (this is the discriminant of an elliptic curve with j-invariant equal to j):

example (j : ) (h0 : j  0) (h1728 : j-1728  0) :
((-36) / (j - 1728)) ^ 2 - (-1) / (j - 1728) - 8 * (2 * ((-36) / (j - 1728))) ^ 3 - 27 * (4 * ((-1) / (j - 1728))) ^ 2 + 9 * (2 * ((-36) / (j - 1728))) * (4 * ((-1) / (j - 1728)))  0 :=
begin
  calc ((-36) / (j - 1728)) ^ 2 - (-1) / (j - 1728) - 8 * (2 * ((-36) / (j - 1728))) ^ 3 - 27 * (4 * ((-1) / (j - 1728))) ^ 2 + 9 * (2 * ((-36) / (j - 1728))) * (4 * ((-1) / (j - 1728)))
  = j^2 / (j-1728)^3 : by {
    field_simp [h1728],
    sorry,
  }
  ...  0 : by {
    field_simp [h1728, h0],
  },
end

but the first field_simp seems not work. Any suggestions?

view this post on Zulip Johan Commelin (Dec 23 2020 at 12:23):

the goal is changing before and after the first field_simp, right?

view this post on Zulip Eric Wieser (Dec 23 2020 at 12:25):

Yes, field_simp seems to be doing it's job

view this post on Zulip Eric Wieser (Dec 23 2020 at 12:25):

You can close that sorry with ring_exp, ring

view this post on Zulip Sebastien Gouezel (Dec 23 2020 at 12:25):

ring is enough.

view this post on Zulip Sebastien Gouezel (Dec 23 2020 at 12:26):

Is that a ring_exp bug that it doesn't close this goal, by the way?

view this post on Zulip Johan Commelin (Dec 23 2020 at 12:26):

Eric Wieser said:

Yes, field_simp seems to be doing it's job

Well, it didn't clear all denominators.

view this post on Zulip Johan Commelin (Dec 23 2020 at 12:26):

field_simp [pow_succ, h1728] does clear all denoms.

view this post on Zulip Sebastien Gouezel (Dec 23 2020 at 12:27):

Here, it does close all denominators.

view this post on Zulip Kevin Buzzard (Dec 23 2020 at 12:28):

You were fiddling with attributes the other day though

view this post on Zulip Johan Commelin (Dec 23 2020 at 12:29):

ooh, maybe I'm on a mathlib that's too old

view this post on Zulip Jz Pan (Dec 23 2020 at 12:39):

Thanks, I confirm that

  = j^2 / (j-1728)^3 : by {
    field_simp [pow_succ, h1728],
    ring,
  }

works. Maybe I'm using an old version of mathlib, who knows. Anyway I already fixed it by using another elliptic curve whose a1 a2 a3 a4 a6 have no denominators (using a linear change of variable to eliminate all its denominators) :smile:

view this post on Zulip Kevin Buzzard (Dec 23 2020 at 13:29):

I tried to prove the group law was associative for the general a1 a2...a6 form and lean got bogged down in the algebra. I am running a student project on elliptic curves next term and I was tempted to just stick to x^3+Ax+B.

view this post on Zulip Jz Pan (Dec 24 2020 at 05:58):

Interesting. I heard that somebody already implemented the group law for general Weierstrass form.

view this post on Zulip Johan Commelin (Dec 24 2020 at 06:00):

I think that was Kevin, together with John Cremona. But I'm not sure if they finished it in the end. Kevin's comment above sounds like they didn't...

view this post on Zulip Kevin Buzzard (Dec 24 2020 at 09:58):

Oh I'm sure this has been done in other provers. Cremona and I have some work we were doing for fun at LFTCM

view this post on Zulip Jz Pan (Dec 25 2020 at 08:19):

Oops, when I upgrade the mathlib my old file breaks, which complains with 'unknown identifier field_simp'. The last version I used is around 12-02.

view this post on Zulip Ruben Van de Velde (Dec 25 2020 at 08:45):

Try adding import tactic.field_simp?

view this post on Zulip Jz Pan (Dec 25 2020 at 09:12):

And then it doesn't solve the goal anymore :neutral:

view this post on Zulip Eric Wieser (Dec 25 2020 at 09:12):

How close does it get?

view this post on Zulip Jz Pan (Dec 25 2020 at 09:17):

How close does it get?

I forgot; I have already revert the mathlib version :|

view this post on Zulip Johan Commelin (Dec 25 2020 at 09:45):

field_simp became more powerful... so if it stopped closing a goal, we would be interested to know what it looks like...

view this post on Zulip Jz Pan (Dec 26 2020 at 07:21):

You can go to https://gitee.com/acmepjz/my-lean-test/tree/master/tests/gtm106 for my test codes. Current I'm using mathlib version 1f1ba587f272d203a40801c6b21af453f7de6ee3 2020-11-29 and all of my code works.


Last updated: May 08 2021 at 18:17 UTC