Zulip Chat Archive

Stream: general

Topic: easy-in-maths union question


view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:07):

import data.set
universe u
example {X Y : Type u} (U : set X) (f : X  set Y) :
( (uu : {x // x  U}), f uu.val) = ⋃₀(f '' U) := sorry

"Two ways of writing a union are the same".

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:08):

This is a joy to prove in tactic mode using set.subset.antisymm

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:08):

is "joy" sarcasm?

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:08):

begin
  apply set.subset.antisymm,
  { intros y Hy,
    cases Hy with V HV,
    cases HV with HV HyV,
    cases HV with uu HuV,
    change V = f (uu.val) at HuV,
    existsi V,
    existsi _,
    exact HyV,
    existsi uu.val,
    exact uu.property,eq.symm HuV
  },
  { intros y Hy,
    cases Hy with V HV,
    cases HV with HV HyV,
    cases HV with u HuV,
    existsi V,
    existsi _,
    exact HyV,
    existsi (u,HuV.1 : {x // x  U}),
    exact eq.symm HuV.2
  }

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:08):

no, not at all

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:09):

I feel like goals like this are ones that I know I can crush

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:09):

so it's a bit like grinding in the early Zeldas

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:09):

you know you can do it and it's quite fun to do

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:09):

But for something of this form which is trivially true in maths

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:10):

my understanding is that one should seek a short "obfuscated" proof

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:10):

i.e. pull a couple of things out the library and you're done

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:10):

so I looked through data.set.lattice

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:10):

and I found

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:10):

open set
#check @sUnion_image
#check @Union_eq_sUnion_image
#check @sUnion_eq_Union
#check @set.sUnion_eq_Union'

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:11):

all of which said "a union equals a union"

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:11):

but I just can't put them all together

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:11):

So I am wondering if this is a hole in the library or if I'm missing a trick

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:11):

I don't know this file very well

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:12):

example {X Y : Type u} (U : set X) (f : X  set Y) :
( (uu : {x // x  U}), f uu.val) = ⋃₀(f '' U) :=
set.ext $ λ z, ⟨λ x1, ⟨⟨x2, H1, H2, H3, x1, x2, H1, H2.symm, H3,
λ x1, x2, H1, H2, H3, x1, ⟨⟨x2, H1, H2.symm, H3⟩⟩

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:12):

I need to be quick because my daughter just woke up (she is sick and off school)

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:13):

but while I'm here let me mention the independent question that I was talking about existsi _ yesterday or so and Mario advised me not to use it, saying it was better to go back and fill it in later.

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:13):

However in my proof above, I used it because the thing that exists is another existsi

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:13):

Aah excellent -- that looks much more like the 2-line obfuscated proof which this result deserves.

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:14):

Should it be in the library?

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:14):

Thanks Kenny.

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:14):

example {X Y : Type u} (U : set X) (f : X  set Y) :
( (uu : {x // x  U}), f uu.val) = ⋃₀(f '' U) :=
by finish [set.set_eq_def]

view this post on Zulip Johannes Hölzl (Apr 17 2018 at 13:15):

the simplifier also works: by simp [set.set_eq_def]

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:15):

now we just switched camps :P

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:16):

Aah! I tried to use simp a lot too, but my simp-fu is weak.

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:16):

Thanks Johannes. How long did it take you to find that?

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:17):

You see, the long tactic mode proof took me a very short time to write, because at each stage I just did the only thing which could be done.

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:17):

I suspect that Kenny had a similar experience with the term proof.

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:17):

But when I tried to find a short proof using library functions, all that happened was that I spent a long time looking through the library and noting down possibly useful functions

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:18):

and then a long time failing to glue them together.

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:18):

I want to get to the stage where if it's easy in maths, I can just nail it in Lean

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:18):

example {X Y : Type u} (U : set X) (f : X → set Y) :
(⋃ (uu : {x // x ∈ U}), f uu.val) = ⋃₀(f '' U) :=
set.ext $ by simp

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:18):

right

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:19):

But this stinks because surely my strategy is basically the same

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:19):

except I split the iff into two distinct implications

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:19):

and then somehow simp failed to deal with either of them

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:20):

simp simplifies iff's and equalities, lol

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:20):

As I said, my simp-fu is weak

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:20):

so that's the trick -- don't break the symmetry.

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 13:20):

Thanks -- that was very instructive!

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:21):

example {X Y : Type u} (U : set X) (f : X  set Y) :
( (uu : {x // x  U}), f uu.val) = ⋃₀(f '' U) :=
set.ext $ λ z, ⟨λ hz, by simpa using hz, λ hz, by simpa using hz

view this post on Zulip Kenny Lau (Apr 17 2018 at 13:21):

splitting into two implications ^

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 17:00):

so to prove X -> Y using simp, you intro h and then simpa using h?

view this post on Zulip Kenny Lau (Apr 17 2018 at 17:03):

right

view this post on Zulip Kevin Buzzard (Apr 17 2018 at 17:10):

This trick is sufficiently important that it should be mentioned in the simp docs.


Last updated: May 15 2021 at 00:39 UTC