Zulip Chat Archive

Stream: maths

Topic: set union equality


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

example (X : Type) (R : Type) (D : R → set X) (γ : Type) (f : γ → R) : ⋃₀(D '' set.range f) = ⋃ (i : γ), D (f i) := sorry

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

I was rather hoping simp would do this one...

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

is there some lemma?

view this post on Zulip Kevin Buzzard (Apr 25 2018 at 18:01):

or do I stick with my 25 line tactic proof :-/

view this post on Zulip Mario Carneiro (Apr 25 2018 at 18:03):

use D '' range f = range (D o f) and then hopefully U range f = U i, f i is a theorem

view this post on Zulip Kenny Lau (Apr 25 2018 at 18:06):

import data.set

example (X : Type) (R : Type) (D : R  set X) (γ : Type) (f : γ  R) :
  ⋃₀(D '' set.range f) =  (i : γ), D (f i) :=
set.ext $ λ z, ⟨λ x1, ⟨⟨x2, x3, h1, h2, h3⟩⟩, x1, x3, h2  h1  rfl, h3,
λ x1, x2, h1, h3, x1, f x2, x2, rfl, h1.symm, h3⟩⟩

view this post on Zulip Kevin Buzzard (Apr 25 2018 at 18:08):

That's my 25 line tactic proof!

view this post on Zulip Kenny Lau (Apr 25 2018 at 18:08):

interesting

view this post on Zulip Kevin Buzzard (Apr 25 2018 at 18:08):

begin
  apply set.ext,
  intro x,
  split,
  intro H,
  cases H with V HV,
  cases HV with HV HX,
  cases HV with r HR,
  cases HR.1 with i Hi,
  existsi V,
  existsi _,
  assumption,
  simp,
  existsi i,
  rw Hi,rw HR.2,

  intro H,
  cases H with V HV,
  cases HV with HV Hx,
  cases HV with i Hi,
  existsi V,
  existsi _,
  assumption,
  existsi (f i),
  split,
  simp,
  existsi i,
  refl,
  rw Hi,
end

view this post on Zulip Kenny Lau (Apr 25 2018 at 18:08):

use rcases :P

view this post on Zulip Kevin Buzzard (Apr 25 2018 at 18:08):

It must be, because we both start with the same line and then do nothing

view this post on Zulip Kevin Buzzard (Apr 25 2018 at 18:09):

other than following our nose

view this post on Zulip Kevin Buzzard (Apr 25 2018 at 18:42):

example (X : Type) (R : Type) (D : R  set X) (γ : Type) (f : γ  R) :
  ⋃₀(D '' set.range f) =  (i : γ), D (f i) :=
  begin
  rw [set.image_univ,set.image_comp],
  show ⋃₀(D  f '' set.univ) =  (i : γ), (D  f) i,
  simp [set.Union_eq_sUnion_image],
  end

view this post on Zulip Kevin Buzzard (Apr 25 2018 at 18:44):

don't even need the show

view this post on Zulip Kevin Buzzard (Apr 25 2018 at 18:45):

Mario's insight is that we reduce the number of functions from 2 to 1 and then simp can handle it

view this post on Zulip Kenny Lau (Apr 25 2018 at 18:50):

import data.set

example (X : Type) (R : Type) (D : R  set X) (γ : Type) (f : γ  R) :
  ⋃₀(D '' set.range f) =  (i : γ), D (f i) :=
by rw [set.Union_eq_sUnion_image,  set.range_comp]

view this post on Zulip Kenny Lau (Apr 25 2018 at 18:50):

do I win?

view this post on Zulip Kevin Buzzard (Apr 25 2018 at 18:59):

IMG_20180425_113712650.jpg

view this post on Zulip Kevin Buzzard (Apr 25 2018 at 18:59):

saw that on the way in today and thought of you

view this post on Zulip Scott Morrison (Apr 25 2018 at 23:06):

@Kevin Buzzard your 25 line tactic proof doesn't seem to work (fails at cases H with V HV,). I was curious how my tactics cope with this one. :-)

view this post on Zulip Mario Carneiro (Apr 25 2018 at 23:11):

works for me

view this post on Zulip Mario Carneiro (Apr 25 2018 at 23:12):

import data.set.lattice

example (X : Type) (R : Type) (D : R → set X) (γ : Type) (f : γ → R) :
  ⋃₀(D '' set.range f) = ⋃ (i : γ), D (f i) :=
begin
  apply set.ext,
  ... +25 lines
end

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:34):

Simon's code in the cases thread didn't work for me without a minor fix

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:34):

I wonder whether we are using different versions of Lean

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:35):

I'm running 04-20 now, along with the latest mathlib. Are you?

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:35):

you are no doubt bleeding edge, I am enjoying the stability of 4-06

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:35):

Upgrading is such a chore

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:35):

I need to do it on three machines

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:35):

and make all the olean files

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:35):

and I just want to concentrate on getting schemes done

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:36):

Everything is taking longer than expected

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:36):

because I have a bunch of commutative diagrams / exact sequences

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:36):

and I continually want to replace an object with a canonically isomorphic object

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:36):

and claim that everything is still commutative / exact

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:37):

I hate computers

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:37):

In maths you just say it works and nobody even notices

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:38):

My instinct always says there's a proof architectural solution to such problems

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:39):

but sometimes you just have to do it the long way a few times before you can see the pattern

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:39):

but once you identify the pattern, it's a short hop to formalized patterns and then lemmas that save you the boilerplate work

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:48):

It is that way of thinking which led me to all this "unique-R-algebra-hom" stuff

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:49):

The proofs that the diagrams commute are just "this is a map with a property, so it's the only map with the property, so it's equal to the map we want"

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:49):

I think a mathematician would instinctively prove commutativity using a diagram chase

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:49):

"where does this element go? This way it goes here, that way it goes there, oh look they're the same"

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:50):

but seeing as I have a pathological fear of quotient types I had to find another way

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:50):

I think that was a good idea on your part

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:50):

I don't think my universal property methods are much quicker

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:50):

in the sense that if I asked Kenny to prove the diagrams commute he would just do the chase

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:50):

and the proof would be about as long, I suspect

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:51):

but my methods are easier to explain

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:51):

I think Kenny is good at getting to the end, but he needs to work on his long game

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 07:51):

they just involve setting type class inference resolution depth to 93 occasionally ;-)

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:52):

there is a lot more possibility for "golfing" at the large scale, planning out the right lemmas that give you the most bang for the buck

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:53):

and that's where stuff like is_unique_R_hom come in

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:54):

I think the difference between Kenny's and my answer to your union-image-range question demonstrate this well

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:55):

on the one hand you can use matches and rfl and anonymous instances to just write out the whole thing from first principles, it's not so hard

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:55):

and on the other you could chain together two lemmas that were written exactly for the purpose

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:57):

I think it's a bit unfortunate that proofs from lemmas lose a lot relative to proofs using basic dependent type theory simply because they have names (and lean's naming convention averages 20 characters or so)

view this post on Zulip Mario Carneiro (Apr 26 2018 at 07:58):

which is a bit misleading since something like λ ⟨a, b⟩, is actually quite a bit more complicated under the hood than it looks

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:04):

In practice, my current problem is that I now know enough about the system to be able to prove these things from first principles, I know that ideally this is not what I should be doing, but I do not have an encyclopedic knowledge of the lemmas which are there and to be honest I am unclear about the roadmap for getting this knowledge.

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:04):

I am not even sure this qualifies as a "problem"

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:04):

but we saw it twice yesterday

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:05):

My ability to retain information is not what it was; I can read the source code and think "oh that is cool" but then not remember everything that is there, unlike when I was in my 20s

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:06):

I need to develop (as Kenny once pointed out) a good feeling for "what _should_ be there"

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:06):

and then simply check that it is

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:06):

Having said all that, I would rather be here than where I was 6 months ago

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:06):

where I had to ask because I simply had no idea how to prove what I needed

view this post on Zulip Mario Carneiro (Apr 26 2018 at 08:10):

I agree with kenny's quote. I certainly don't remember all the lemmas in mathlib, I just think about the things that should exist and make sure they are actually there. Your question about the union-image-range seems like a step in the right direction, you are getting the sense for what form the lemmas should take, but in that case union-image-range is three things and I like lemmas to talk about two things

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:11):

One thing that has helped me terrifically is trying to use Kenny's localization work, because it was written in a completely different style to mathlib. Rather than being written by someone who knew everything and wanted to write an interface, it was written by someone who knew nothing and was learning the material.

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:12):

In practice I said to Kenny "can you please give me a function which given a ring R and a multiplicative subset S, returns the ring R[1/S]"

view this post on Zulip Mario Carneiro (Apr 26 2018 at 08:12):

As far as what you should learn by reading printouts, I would say focus on definitions, that's the core around which the lemmas are built

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:12):

and he said "sure" and a day or so later I had that ring

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:12):

and then I realised I could do nothing with it

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

so I kept asking for more and he kept making it (basically by return of post)

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

and by the end of it I had a feeling for what it meant to build a mathlib file

view this post on Zulip Mario Carneiro (Apr 26 2018 at 08:14):

writing for others is definitely harder than writing for yourself

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:14):

focus on definitions -- thanks for the tip!

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:14):

writing for others -- Kenny and I have worked really well as a team, I knew the maths and he did the dirty work

view this post on Zulip Mario Carneiro (Apr 26 2018 at 08:14):

you can look at the lemmas, but your reaction to them should be "oh, well of course"

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

and the really cool thing about the localization stuff was once he'd done the really primitive dirty work of proving that some map had some universal property, all the other universal properties which people used in practice could be deduced from Kenny's, and I could write that code myself

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

you have probably seen this phenomenon before

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

technical code full of [[ ]] and quot.sound or whatever to get stuff off the ground

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

but then the proofs get more conceptual after a while

view this post on Zulip Mario Carneiro (Apr 26 2018 at 08:17):

oh yes

view this post on Zulip Mario Carneiro (Apr 26 2018 at 08:18):

I expect that outside the free_group file we will never see list (A x bool)

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 08:18):

it's been a fascinating learning experience.

view this post on Zulip Scott Morrison (Apr 26 2018 at 11:14):

example (X : Type) (R : Type) (D : R  set X) (γ : Type) (f : γ  R) :
  ⋃₀(D '' set.range f) =  (i : γ), D (f i) := by obviously

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 16:53):

Well it does look obvious to me.

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 16:53):

I think we are probably a long way from a tactic which will be able to prove everything which looks obvious to me

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 16:53):

but I want to start along down that road.

view this post on Zulip Patrick Massot (Apr 26 2018 at 16:54):

Kevin, you may have missed the point

view this post on Zulip Patrick Massot (Apr 26 2018 at 16:54):

Scott does have a tactic called obviously which does the job here

view this post on Zulip Patrick Massot (Apr 26 2018 at 16:55):

https://github.com/semorrison/lean-tidy/blob/f2303e5376c3520d4432fd073fdb1fd0dfb1f8a8/examples/20180426-kbuzzard.lean

view this post on Zulip Patrick Massot (Apr 26 2018 at 16:55):

https://github.com/semorrison/lean-tidy/blob/b8c6661d4ea74d5e8b5df25b2225f4353e5c6bf5/src/tidy/tidy.lean#L136

view this post on Zulip Kevin Buzzard (Apr 26 2018 at 16:59):

right

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

but unfortunately I suspect that it will not prove _everything_ which is obvious

view this post on Zulip Patrick Massot (Apr 26 2018 at 17:00):

He's working on it

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

In particular I bet it won't prove that if there exists a,b,c,d nats with a^2+b^2+c^2+d^2 = 2n then there exists w x y z nats with w^2+x^2+y^2+z^2=2n and w^2+x^2 even

view this post on Zulip Scott Morrison (Apr 27 2018 at 00:13):

It would be nice to have a better name than obviously. Suggestions welcome. follow_your_nose is a a possibility :-)

view this post on Zulip Scott Morrison (Apr 27 2018 at 00:15):

I think your a^2+b^2+c^2+d^2 = 2n is far from "obvious" in this sense. I mean, it's easy, but I don't think "let's think about the parity of the numbers, and the multiplicities of the parities, and solve the problem merely by permuting" counts as "following your nose".

view this post on Zulip Simon Hudon (Apr 27 2018 at 00:23):

left_as_an_exercise_to_the_reader

view this post on Zulip Simon Hudon (Apr 27 2018 at 00:24):

Or beside_the_point

view this post on Zulip Simon Hudon (Apr 27 2018 at 00:25):

or omitted

view this post on Zulip Mario Carneiro (Apr 27 2018 at 00:37):

I think by beside_the_point is a hilarious substitute for sorry

view this post on Zulip Mario Carneiro (Apr 27 2018 at 00:38):

but none of those suggest that the proof is actually done automatically

view this post on Zulip Simon Hudon (Apr 27 2018 at 00:38):

How about magic or automagic? :D

view this post on Zulip Simon Hudon (Apr 27 2018 at 00:40):

I think I might like chocolate even better, since Uncyclopedia mentions it's a respectable proof technique:

http://uncyclopedia.wikia.com/wiki/Proof

view this post on Zulip Mario Carneiro (Apr 27 2018 at 01:10):

Here's a nice proof of that statement: Given any three numbers a b c, I claim that the sum of two of them is even. If a+b is odd, and a+c is odd, and b+c is odd, then (a+b)+(a+c)+(b+c)=2*(a+b+c) is odd, a contradiction.

view this post on Zulip Mario Carneiro (Apr 27 2018 at 01:12):

To do this formally you only need to know that every number is even or odd and apply it three times, and then do some simple algebra at the end

view this post on Zulip Mario Carneiro (Apr 27 2018 at 01:12):

also you have to know parity rules for adding even and odd


Last updated: May 10 2021 at 07:15 UTC