question about field_simp

Stream: new members

[Jz Pan]

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?

[Johan Commelin]

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

[Eric Wieser]

Yes, field_simp seems to be doing it's job

[Eric Wieser]

You can close that sorry with ring_exp, ring

[Sebastien Gouezel]

ring is enough.

[Sebastien Gouezel]

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

[Johan Commelin]

Eric Wieser said:

Yes, field_simp seems to be doing it's job

Well, it didn't clear all denominators.

[Johan Commelin]

field_simp [pow_succ, h1728] does clear all denoms.

[Sebastien Gouezel]

Here, it does close all denominators.

[Kevin Buzzard]

You were fiddling with attributes the other day though

[Johan Commelin]

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

[Jz Pan]

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:

[Kevin Buzzard]

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.

[Jz Pan]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Jz Pan]

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.

[Ruben Van de Velde]

Try adding import tactic.field_simp?

[Jz Pan]

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

[Eric Wieser]

How close does it get?

[Jz Pan]

How close does it get?

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

[Johan Commelin]

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

[Jz Pan]

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.