Zulip Chat Archive

Stream: new members

Topic: really tedious calculation


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 20:13):

Is this true?

view this post on Zulip Reid Barton (Jun 24 2020 at 20:13):

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

view this post on Zulip Sebastien Gouezel (Jun 24 2020 at 20:13):

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

view this post on Zulip Reid Barton (Jun 24 2020 at 20:13):

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

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 20:13):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 20:16):

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

view this post on Zulip 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

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:17):

Is there a different way I should've approached it

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 20:18):

I think you shouldn't have used 0

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 20:18):

You can also do existsi _. Remember that tactic?

view this post on Zulip Reid Barton (Jun 24 2020 at 20:19):

split works instead of those two lines, too

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 20:19):

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

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:20):

Yeah that was pretty nice, thanks!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Reid Barton (Jun 24 2020 at 20:22):

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

view this post on Zulip 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

view this post on Zulip 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 a+b+b+c-\lfloor a+b\rfloor + \lfloor b+c \rfloor and solves everything.

view this post on Zulip Alena Gusakov (Jun 24 2020 at 20:25):

Gotcha. Thanks!!

view this post on Zulip 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.

view this post on Zulip Alena Gusakov (Jun 24 2020 at 21:08):

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

view this post on Zulip 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