## Stream: new members

### Topic: really tedious calculation

#### Alena Gusakov (Jun 24 2020 at 20:08):

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


Is this true?

#### Reid Barton (Jun 24 2020 at 20:13):

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

#### Sebastien Gouezel (Jun 24 2020 at 20:13):

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

#### Reid Barton (Jun 24 2020 at 20:13):

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

#### Kevin Buzzard (Jun 24 2020 at 20:13):

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

#### Kevin Buzzard (Jun 24 2020 at 20:15):

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

#### Kevin Buzzard (Jun 24 2020 at 20:16):

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

#### Alena Gusakov (Jun 24 2020 at 20:17):

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 (Jun 24 2020 at 20:17):

Is there a different way I should've approached it

#### Kevin Buzzard (Jun 24 2020 at 20:18):

I think you shouldn't have used 0

#### Reid Barton (Jun 24 2020 at 20:18):

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 (Jun 24 2020 at 20:18):

You can also do existsi _. Remember that tactic?

#### Reid Barton (Jun 24 2020 at 20:19):

split works instead of those two lines, too

#### Kevin Buzzard (Jun 24 2020 at 20:19):

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

#### Alena Gusakov (Jun 24 2020 at 20:20):

Yeah that was pretty nice, thanks!

#### Kevin Buzzard (Jun 24 2020 at 20:20):

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 (Jun 24 2020 at 20:21):

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 (Jun 24 2020 at 20:21):

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 (Jun 24 2020 at 20:22):

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

#### Alena Gusakov (Jun 24 2020 at 20:22):

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 (Jun 24 2020 at 20:23):

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.

Gotcha. Thanks!!

#### Sebastien Gouezel (Jun 24 2020 at 20:55):

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 (Jun 24 2020 at 21:08):

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

#### Scott Morrison (Jun 25 2020 at 04:30):

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

Last updated: May 14 2021 at 13:24 UTC