regression in linear_combination

Stream: mathlib4

[Bhavik Mehta]

The following works in mathlib3, but not in mathlib4:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.LinearCombination

example {s1 s2 s3 c1 c2 c3 : ℝ} (h : s1 + s2 + s3 = 0) (h' : c1 + c2 + c3 = 0)
  (h1 : s1 ^ 2 + c1 ^ 2 = 1) (h2 : s2 ^ 2 + c2 ^ 2 = 1) (h3 : s3 ^ 2 + c3 ^ 2 = 1) :
  s1 * c1 + s2 * c2 + s3 * c3 = 0 :=
by linear_combination
  (-(1 * s1 * c2 * s3) + s2 * c2 * s3 - 1 * s1 * s2 * c3 - 1 * c2 ^ 2 * c3 + s2 * s3 * c3 -
              1 * c2 * c3 ^ 2) *
            h +
          (-(1 * c1 * c2 * s3) + c2 ^ 2 * s3 - 1 * c1 * s2 * c3 + s2 * c2 * c3 + c2 * s3 * c3 +
                s2 * c3 ^ 2 +
              s1) *
            h' +
        (c2 * s3 + s2 * c3) * h1 +
      (-(1 * c2 * s3) + s1 * c3 - 1 * s3 * c3) * h2 +
    (s1 * c2 - 1 * s2 * c2 - 1 * s2 * c3) * h3

[Eric Wieser]

I think this is lean4#2220

[Eric Wieser]

Though macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) doesn't seem to help, even though it does change the statement

[Eric Wieser]

macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) and a syntax fix makes this work

[Bhavik Mehta]

Eric Wieser said:

I think this is lean4#2220

Explicitly saying that all the powers are in nat doesn't fix it

[Eric Wieser]

This works for me:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.LinearCombination

macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)

example {s1 s2 s3 c1 c2 c3 : ℝ} (h : s1 + s2 + s3 = 0) (h' : c1 + c2 + c3 = 0)
  (h1 : s1 ^ 2 + c1 ^ 2 = 1) (h2 : s2 ^ 2 + c2 ^ 2 = 1) (h3 : s3 ^ 2 + c3 ^ 2 = 1) :
  s1 * c1 + s2 * c2 + s3 * c3 = 0 :=
by linear_combination (-(1 * s1 * c2 * s3) + s2 * c2 * s3 - 1 * s1 * s2 * c3 - 1 * c2 ^ 2 * c3 + s2 * s3 * c3 -
              1 * c2 * c3 ^ 2) *
            h +
          (-(1 * c1 * c2 * s3) + c2 ^ 2 * s3 - 1 * c1 * s2 * c3 + s2 * c2 * c3 + c2 * s3 * c3 +
                s2 * c3 ^ 2 +
              s1) *
            h' +
        (c2 * s3 + s2 * c3) * h1 +
      (-(1 * c2 * s3) + s1 * c3 - 1 * s3 * c3) * h2 +
    (s1 * c2 - 1 * s2 * c2 - 1 * s2 * c3) * h3

[Bhavik Mehta]

Oh, never mind, this was me being dumb all along

[Bhavik Mehta]

The syntax was broken in my original example!

[Bhavik Mehta]

So all that's happening is that the syntax for linear_combination in mathlib4 doesn't allow an extra line before the expression, and that's all that confused me

[Mario Carneiro]

It should

[Mario Carneiro]

but the next line cannot be less indented than the word linear_combination, as in your example

[Mario Carneiro]

(which is part of why the style guide prefers to always put by on the previous line)

[Bhavik Mehta]

Hmm, that makes sense, although I got here from polyrith

[Bhavik Mehta]

(in particular, from

    s1 * c1 + s2 * c2 + s3 * c3 = 0 :=
by polyrith

but I suppose that since I should expect this to be a long call, there's no point writing the by as if I'm expecting a one-line proof

[Mario Carneiro]

even for one line proofs like by simp the style guide is to put the by on the previous line (this is different from lean 3)

[Mario Carneiro]

but also, what you describe is a bug in "try this"

[Mario Carneiro]

it should have noticed that polyrith is 3 space indented and apply that to the resulting expression

[Bhavik Mehta]

Mario Carneiro said:

even for one line proofs like by simp the style guide is to put the by on the previous line (this is different from lean 3)

Is this in the style guide? I remember checking before, and I'm just looking now and I don't see it, but I'm under the weather and clearly missing obvious things so I could be wrong

[Mario Carneiro]

it may not be, a lot of the little details are only written in (formatter) code

[Bhavik Mehta]

Oh I guess it's implicit in that by is always meant to be before the first tactic call, even though some one-line examples in the style guide don't have this

[Mario Carneiro]

If the entire theorem (statement and proof) fits on one line then there is no need for the newline, but if you have to break the line never do so between := and by

[Bhavik Mehta]

That makes a lot of sense, thanks

[Mario Carneiro]

(Someday I'll write a proper code formatter, and then it can do all of this stuff. It's just such a big project...)

[Bhavik Mehta]

Soon we'll be able to say "This is correct style because Mario's code formatter says so", in the meantime I can just say "This is correct style because Mario says so" :)

[Gareth Ma]

So the correct format is now

example (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa : ℕ) :
  1 + 0 = 1 := by rw [add_zero]

? I used to write

...
  1 + 0 = 1 :=
by
  rw [add_zero]
``` and it feels clearer to me because I can see where the proof starts easily

[Scott Morrison]

Why don't you just write:

example (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa : ℕ) :
    1 + 0 = 1 := by
  rw [add_zero]

in that case?

[Scott Morrison]

(Note that if the signature needs a linebreak, it must be indented with 4 spaces, not 2 as you have written above.)

[Gareth Ma]

Scott Morrison said:

(Note that if the signature needs a linebreak, it must be indented with 4 spaces, not 2 as you have written above.)

Ohh, that makes the difference then haha

[Mario Carneiro]

my mental style guide says that Scott's version is preferred, but

example (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa : ℕ) :
    1 + 0 = 1 := by rw [add_zero]

is also acceptable (note that it is still 4 space indented)

[Mario Carneiro]

I don't have a strong opinion, but I think the same rule should also apply to axiom and opaque: even though there isn't even a body in this case (the body is optional for opaque), the signature should still be 4 space indented, i.e.

axiom foo (aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa : ℕ) :
    1 + 0 = 1