really tedious calculation

Stream: new members

[Alena Gusakov]

I cannot for the life of me figure out how I should solve this even though it should be really simple

import algebra.group.basic
import data.real.basic

noncomputable theory
open_locale classical


def star_set := set.Ico (0:ℝ) 1

#check star_set


section star_group

def star : ℝ → ℝ → ℝ
| x y := x + y - ⌊ x + y ⌋


notation x`⋆`y := star x y
variables (x y : ℝ) (A : Type*)

#check star_set

lemma star_assoc {a b c : ℝ} (ha : a ∈ star_set) (hb : b ∈ star_set) (hc : c ∈ star_set): (a ⋆ b ⋆ c) = (a ⋆ (b ⋆ c)) :=
begin
    unfold star,
    repeat {rw ← fract},
    rw fract_eq_fract,
    use 0,
    repeat {rw fract},
    --what now??
end

end star_group

[Kevin Buzzard]

Is this true?

[Reid Barton]

I think this needs a bit of high-level strategy.

[Sebastien Gouezel]

This is associativity of addition on $\mathbb{R}/\mathbb{Z}$.

[Reid Barton]

i.e. first start with the math proof, even if it's only one sentence.

[Kevin Buzzard]

ring reduces the goal to ⊢ -↑⌊a + b⌋ + ↑⌊b + c⌋ = ↑0

[Kevin Buzzard]

It's not associativity of addition on R/Z because the star isn't a map from R/Z to R/Z

[Kevin Buzzard]

I guess the lemma is true but the proof has made a wrong turn.

[Alena Gusakov]

Yeah it is true, I've done it by hand. Just the reordering of terms where I was stuck was kind of a nightmare

[Alena Gusakov]

Is there a different way I should've approached it

[Kevin Buzzard]

I think you shouldn't have used 0

[Reid Barton]

here is a weird way to do it

lemma star_assoc {a b c : ℝ} (ha : a ∈ star_set) (hb : b ∈ star_set) (hc : c ∈ star_set): (a ⋆ b ⋆ c) = (a ⋆ (b ⋆ c)) :=
begin
    unfold star,
    repeat {rw ← fract},
    rw fract_eq_fract,
    let z : ℤ := _,
    use z,
    repeat {rw fract},
    ring,
    norm_cast,
end

[Kevin Buzzard]

You can also do existsi _. Remember that tactic?

[Reid Barton]

split works instead of those two lines, too

[Kevin Buzzard]

I think Reid wins Zulip proof of the day for that one

[Alena Gusakov]

Yeah that was pretty nice, thanks!

[Kevin Buzzard]

The point @Alena Gusakov is that which integer you want to use depends on exactly what "carries" occurred when you added a+b and b+c.

[Kevin Buzzard]

You used 0 and that can't be right, because the high-powered ring tactic (which is the tactic you didn't know when you posted the original question) reduced the goal as you had it to (some random integer) = 0.

[Kevin Buzzard]

Reid's clever proof says "instead of using 0, let's use z, where z is an integer I'll specify later when the dust has cleared"

[Reid Barton]

It's one of those proofs that ended before I expected it to.

[Alena Gusakov]

Yeah that makes sense, I knew there were gonna be some issues if 1 < a + b or whatever, I think my plan was to try to split it up into cases again but I guess forgot

[Kevin Buzzard]

so at the end he has two goals:

abc : ℝ
ha : a ∈ star_set
hb : b ∈ star_set
hc : c ∈ star_set
⊢ -↑⌊a + b⌋ + ↑⌊b + c⌋ = ↑?m_1
abc : ℝ
ha : a ∈ star_set
hb : b ∈ star_set
hc : c ∈ star_set
⊢ ℤ

The first goal has a variable in! It's a bit of a silly name, ?m_1, but it's just an integer variable. The second goal is "tell me what that variable is". But if you try and solve the first goal with another tactic (norm_cast), Lean guesses that the variable you want is $-\lfloor a+b\rfloor + \lfloor b+c \rfloor$ and solves everything.

[Alena Gusakov]

Gotcha. Thanks!!

[Sebastien Gouezel]

Also, this proof shows that the assumptions ha, hb and hc are not necessary. You can spot this by typing #lint after the proof, and it will tell you this, among other things.

[Alena Gusakov]

Did not know about #lint! That's super useful, thanks!

[Scott Morrison]

(mathlib PRs will run #lint automatically, and complain about anything it finds, so it's a good habit to run it yourself occasionally)