## Stream: general

#### Patrick Massot (Apr 21 2018 at 11:46):

Let me share my joy of using @Simon Hudon recent contributions (not yet merged, see https://github.com/PatrickMassot/mathlib/tree/wlog_ext for a version including both relevant PR if you want to play with it).

I defined homeomorphisms between topological spaces X and Y, and the support of a homeomorphism f from X to itself (if you don't know what this means, think homeo X X coerces to invertible functions from X to X and supp f is the set of x in X such that f x ≠ x, that's good enough approximation). I want to prove the trivial yet important fact that two homeos with disjoint support commute. I already had various proofs of that, some versions written with the help of Mario. But I'd like to show what the latest version looks like. So statement is:

example {f g : homeo X X} (H : supp f ∩ supp g = ∅) : f * g = g * f


#### Patrick Massot (Apr 21 2018 at 11:47):

First consider the pen and paper proof: We need to prove f (g x) = g (f x) for all x in X. If x is neither in supp f nor in supp g then it's obvious, so let's discard this case. WLOG x is in supp f since everything is obviously symmetric in f and g. By H, x is not in supp g. Also the support of f is stable under f (because its complement the fixed points set is obviously stable). So f x is also not in supp g. So g x = x and g (f x) = f x and we are done.

#### Patrick Massot (Apr 21 2018 at 11:48):

Simon's work help with the first and third sentences. First "We need to prove f (g x) = g (f x) for all x in X". But actually homeo X X is not quite X → X so we can't do funext x. We only need a extensionality lemma for homeos, and tag it with the [extensionality] attribute to later write ext x in place of funext x. Same would work for sets etc.

Now the third sentence is much more spectacular: "WLOG x is in supp f since everything is obviously symmetric in f and g". I still cannot write this without sweating and thinking: Oh my god, Lean will disagree it's obvious. Simon's tactic turns this into: wlog h : x ∈ supp f using f g. Period. No disagrement. :heart_eyes:

#### Patrick Massot (Apr 21 2018 at 11:48):

Here is what it looks like. Notice also liberal use of the finish tactic.

lemma fundamental' {f g : homeo X X} (H : supp f ∩ supp g = ∅) : f * g = g * f :=
begin
ext x,
by_cases H' : x ∈ supp f ∨ x ∈ supp g,
{ -- Here we assume H' : x ∈ supp f ∨ x ∈ supp g
wlog h : x ∈ supp f using f g,
have x_not_supp_g : x ∉ supp g := (subset_compl_iff_disjoint.2 H) h,
have f_x_supp_f : f x ∈ supp f,
{ have : f x ∈ f '' supp f := mem_image_of_mem f h,
finish [stable_support f] },
have : f x ∉ supp g := (subset_compl_iff_disjoint.2 H) f_x_supp_f,
finish [fix_of_not_in_supp] },
{ -- Now we assume H' : ¬(x ∈ supp f ∨ x ∈ supp g)
rw not_or_distrib at H',
finish [fix_of_not_in_supp] }
end


#### Patrick Massot (Apr 21 2018 at 11:48):

And a calc version for good measure.

lemma fundamental'' {f g : homeo X X} (H : supp f ∩ supp g = ∅) : f * g = g * f :=
begin
ext x,
by_cases H' : x ∈ supp f ∨ x ∈ supp g,
{ -- Here we assume H' : x ∈ supp f ∨ x ∈ supp g
wlog h : x ∈ supp f using f g,
exact calc
(f * g) x = f (g x) : by simp
... = f x     : by { have x_not_supp_g : x ∉ supp g := (subset_compl_iff_disjoint.2 H) h,
finish [fix_of_not_in_supp] }
... = g (f x) : by { have f_x_supp_f : f x ∈ supp f,
{ have : f x ∈ f '' supp f := mem_image_of_mem f h,
finish [stable_support f] },
have : f x ∉ supp g := (subset_compl_iff_disjoint.2 H) f_x_supp_f,
finish [fix_of_not_in_supp] }
... = (g * f) x : by simp },
{ -- Now we assume H' : ¬(x ∈ supp f ∨ x ∈ supp g)
rw not_or_distrib at H',
finish [fix_of_not_in_supp] }
end


#### Patrick Massot (Apr 21 2018 at 11:48):

Term mode people will have a really hard time converting me.

#### Simon Hudon (Apr 21 2018 at 12:00):

What a nice homage! Thank you! I'm so happy that you like those tools :)

#### Kenny Lau (Apr 21 2018 at 12:09):

let's see how long we'll need to wait before they merge the PR

#### Patrick Massot (Apr 21 2018 at 12:19):

What a nice homage! Thank you! I'm so happy that you like those tools :)

I'm not only the annoying user who can't code anything by himself, and keep reminding you to work on these tactics (and write tactic writing tutorials covering pi_instance and wlog). I also love using them, and documenting things.

#### Patrick Massot (Apr 21 2018 at 12:24):

And I think the community is currently working really well. It seems to me we recently went from the pretty horrible situation where the main dev felt harassed by frustrated users to a pretty nice situation. Leo and Sebastian are peacefully working on Lean 4 while everybody else finds some place in the Lean 3 world. Clearly we don't want Leo to spend time writing tactics like wlog. We want power users like Mario, you, Scott... to write these. And then we have dumb users like me who can come up with examples finding bugs, suggests new tactics, write documentation... And everybody has fun, I think. And it seems Lean 4 will expose even more to Lean without touching C++ code or even PRing the main repo, so we are clearly going in the right direction.

#### Patrick Massot (Apr 21 2018 at 12:25):

let's see how long we'll need to wait before they merge the PR

Ok, we still have some frustration...

#### Patrick Massot (Apr 21 2018 at 12:25):

But I'm optimistic anyway.

#### Patrick Massot (Apr 21 2018 at 12:26):

And I hope that writing an example non-trivially using wlog actually helps getting the PR merged more than complaining that reviewing PR takes time.

#### Mario Carneiro (Apr 21 2018 at 12:31):

I always like to see a tool in use, that definitely brings it up the todo list

#### Simon Hudon (Apr 21 2018 at 12:45):

And I think the community is currently working really well.

I've also had a very positive experience in the community with people eager to help and grateful when you give then a nudge. I was surprised and saddened that Leo described his experience as harassment.

#### Simon Hudon (Apr 21 2018 at 12:52):

And then we have dumb users like me who can come up with examples finding bugs, suggests new tactics, write documentation...

Yeah! Darn those dumb users, leeching off the community and only proving important mathematical theorems!

But seriously, I'm really glad you decided to champion the cause of documentation. It's often neglected but it makes such a big difference!

#### Moses Schönfinkel (Apr 21 2018 at 13:11):

Is lack of documentation why Coq hasn't been adopted widespreadly (ok this is not really English) after 30 years?

#### Simon Hudon (Apr 21 2018 at 13:14):

Hard to say. To be fair, I found Coq much harder to pick up than Lean. I never actually ended up applying it to large problems. I think the standard library is ill-organized and much harder to use than Lean's.

#### Moses Schönfinkel (Apr 21 2018 at 13:17):

That's because there is no organisation so to speak; no hierarchy either. You have, for example, two different versions for Z<theroem> and N<theorem>.

#### Simon Hudon (Apr 21 2018 at 13:18):

Maybe you could summarize that as: when you're a beginner, you have to get over a lot humps before you can begin to try stuff on your own. It feels like with Lean, once you installed it, you start hacking and it progressively becomes harder as you get more ambitious

#### Simon Hudon (Apr 21 2018 at 13:19):

Yeah, it looks a bit like a research project that just happened to be useful

#### Simon Hudon (Apr 21 2018 at 13:20):

And I find it doesn't help that the library is built around ML modules more than around type classes. Type classes are really tremendous to make things simple to use.

#### Kevin Buzzard (Apr 21 2018 at 20:59):

My 2 cents: I think that the Coq community, and the automated theorem proving community in general, have done a bad job of advertising to mathematicians. I remember the edition of the Notices of the AMS coming out a few years ago which concentrated on this stuff and wondering if it was the future, but somehow the jewels in the crown at the time were things like "yet another proof of the 4 colour theorem" and maybe this was just after the odd order theorem, which was something mathematicians had long moved on from.

#### Kevin Buzzard (Apr 21 2018 at 20:59):

My gut feeling is that a different approach is needed

#### Kevin Buzzard (Apr 21 2018 at 21:00):

so that's why I'm going to try concentrating on getting undergraduates in mathematics to prove a bunch of basic stuff, because I think it might have a different kind of outcome.

#### Kevin Buzzard (Apr 21 2018 at 21:00):

Maybe a bunch of young people who know about this stuff will somehow integrate it into the maths community in a different way.

#### Kevin Buzzard (Apr 21 2018 at 21:02):

Let me absolutely echo the opinions of the others in this thread -- I've had a really good time learning Lean here, I would never have got anywhere without this group, and now I feel like I actually understand certain aspects of the software well enough to be able to use it without being continually frustrated.

#### Kevin Buzzard (Apr 21 2018 at 21:02):

The strategy of "if you don't get it, find out about it and then write some docs" also works really well for me.

#### Kevin Buzzard (Apr 21 2018 at 21:03):

And also the idea of choosing a non-trivial thing to work on and then just working on it has taught me a huge amount. There are just over 5000 lines of code in the stacks project directory now.

#### Patrick Massot (Apr 21 2018 at 21:08):

Roughly, how many lines are pure commutative algebra and how many use geometric language?

#### Kevin Buzzard (Apr 21 2018 at 21:14):

it wouldn't surprise me if nearly 1000 lines were cut-and-pasted stacks project LaTeX :-)

#### Kevin Buzzard (Apr 21 2018 at 21:15):

I guess it's almost all algebra at the minute

#### Kevin Buzzard (Apr 21 2018 at 21:16):

@Johan Commelin pointed out a typo in my definition of scheme and I told him not to believe my definition until we had some proof of a lemma about schemes which was geometric

#### Kevin Buzzard (Apr 21 2018 at 21:16):

and I am not sure how geometric you think this is

#### Kevin Buzzard (Apr 21 2018 at 21:16):

but he suggested the Spec / Gamma duality, Hom(S,Spec(A)) = Hom(A,Gamma(S))

#### Patrick Massot (Apr 21 2018 at 21:16):

I know the distinction is hard to make (Grothendieck did this on purpose!). Let's say: how many lines not containing "sheaf" or "presheaf"?

#### Kevin Buzzard (Apr 21 2018 at 21:16):

which I think would be a true test

#### Kevin Buzzard (Apr 21 2018 at 21:17):

Oh there are lots and lots of lines proving abstract stuff of the form "if I have a presheaf only defined on a basis of open sets for a topology, but it satisfies the sheaf axiom for a cofinal set of covers, then it extends uniquely to a sheaf on the whole space"

#### Kevin Buzzard (Apr 21 2018 at 21:18):

There's a bunch of lemmas about rings

#### Kevin Buzzard (Apr 21 2018 at 21:18):

and then a bunch of lemmas about presheaves and sheaves

#### Kevin Buzzard (Apr 21 2018 at 21:18):

and then some actual mathematics saying that some sequence of rings is exact

#### Kevin Buzzard (Apr 21 2018 at 21:19):

and I'm just in the process of writing the glue which will glue it all together.

#### Patrick Massot (Apr 21 2018 at 21:19):

Did you try to separate nicely as much sheaf theory from ring theory as possible?

#### Andrew Ashworth (Apr 21 2018 at 21:35):

so would you say it took you about a year of using lean before you felt confident in doing things in it?

#### Andrew Ashworth (Apr 21 2018 at 21:35):

i wonder how much faster your summer undergraduates and fall students will learn lean

#### Patrick Massot (Apr 21 2018 at 21:36):

I think he started less than a year ago

Last July maybe?

#### Patrick Massot (Apr 21 2018 at 21:36):

Maybe even August

#### Andrew Ashworth (Apr 21 2018 at 21:39):

two semesters of focused effort sounds about right though

#### Andrew Ashworth (Apr 21 2018 at 21:40):

coincidentally that's how long it takes to get through software foundations 1-3

#### Andrew Ashworth (Apr 21 2018 at 21:43):

if i had to guess that right there is the reason it never took off in 30 years

#### Andrew Ashworth (Apr 21 2018 at 21:44):

imagine if you had to spend two semesters before you could write latex or use a computer algebra system

#### Patrick Massot (Apr 21 2018 at 21:47):

Also don't forget it's not like Coq was ready on year one and then waited for 30 years

#### Kevin Buzzard (Apr 21 2018 at 23:42):

Yes I started when I was in MSRI in July/August 2017

#### Kevin Buzzard (Apr 21 2018 at 23:42):

but I'm not entirely sure you can call my efforts focussed

#### Kevin Buzzard (Apr 21 2018 at 23:42):

I was teaching a class of 220 students in one of the terms, and being head of pure maths and teaching a graduate course in the other one :-/

#### Kevin Buzzard (Apr 21 2018 at 23:42):

On the other hand I pretty much gave up all of my other hobbies

Last updated: Aug 03 2023 at 10:10 UTC