Zulip Chat Archive

Stream: general

Topic: Tutorial


view this post on Zulip Johan Commelin (Oct 04 2018 at 06:58):

@Patrick Massot Would you mind pushing your demo to a new tutorial branch on community fork? Maybe as docs/tutorial/demo.lean.

view this post on Zulip Johan Commelin (Oct 04 2018 at 06:59):

After that we could attempt answering Neil's questions in that branch as well.

view this post on Zulip Johan Commelin (Oct 04 2018 at 06:59):

Q1 and Q2 have been done. They can easily be entered.

view this post on Zulip Johan Commelin (Oct 04 2018 at 07:00):

Q3 shouldn't be hard either. Q4 needs work. Q5 should be rather easy again.

view this post on Zulip Johan Commelin (Oct 04 2018 at 07:01):

The point is that we should write lots of comments in those files. So that people can actually learn a lot of Lean. Instead of learning only a tiny bit of maths (that they actually knew already).

view this post on Zulip Patrick Massot (Oct 04 2018 at 07:01):

Ok, I'll do that

view this post on Zulip Bryan Gin-ge Chen (Oct 04 2018 at 07:04):

If you're looking for help with this, I'd be happy to contribute. I think I should be able to do Q5.

view this post on Zulip Johan Commelin (Oct 04 2018 at 07:05):

Sure! Please contribute!

view this post on Zulip Johan Commelin (Oct 04 2018 at 07:10):

@Patrick Massot Do you have time to do this before the talks start? Otherwise I can start the branch... and you can dump your demo later (-;

view this post on Zulip Patrick Massot (Oct 04 2018 at 07:13):

depends on the RER train. I'm leaving my house, let's see when I'll arrive in Orsay

view this post on Zulip Sean Leather (Oct 04 2018 at 07:13):

I would recommend using a top-level tutorial directory instead of the subdirectory under docs. First, it's more discoverable (easier to find). Second, I think many people expect docs to not be code, which could lead people to not look in there for code.

view this post on Zulip Johan Commelin (Oct 04 2018 at 07:15):

I'm fine with that. It depends on what the powers that be prefer (-; @Mario Carneiro @Johannes Hölzl

view this post on Zulip Johannes Hölzl (Oct 04 2018 at 07:20):

if we add tutorials, I would also prefer tutorial in the top level directory.

view this post on Zulip Johannes Hölzl (Oct 04 2018 at 07:20):

But we could also have a separate repository in leanprover-community then its easier to contribute

view this post on Zulip Johan Commelin (Oct 04 2018 at 07:21):

I think it is best to have this end up in mathlib. Because then we are forced to keep it working. Also: better discoverability

view this post on Zulip Kevin Buzzard (Oct 04 2018 at 09:10):

Stick it in the top level and it can be moved later

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 08:05):

I've made some progress on Q5. Is someone (Patrick? Johan?) planning to make a branch in leanprover-community I can PR to?

view this post on Zulip Johan Commelin (Oct 05 2018 at 08:07):

Sorry, I have to do some other stuff now. Please go ahead and create the branch

view this post on Zulip Patrick Massot (Oct 05 2018 at 08:10):

I'll create the branch if you want

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 08:11):

Sure, that'd be great.

view this post on Zulip Patrick Massot (Oct 05 2018 at 08:11):

https://github.com/leanprover-community/mathlib/tree/tutorials

view this post on Zulip Patrick Massot (Oct 05 2018 at 08:12):

wait

view this post on Zulip Patrick Massot (Oct 05 2018 at 08:12):

I messed up

view this post on Zulip Patrick Massot (Oct 05 2018 at 08:14):

now it's ok

view this post on Zulip Patrick Massot (Oct 05 2018 at 08:23):

Ok, I've pushed my demo file: https://github.com/leanprover-community/mathlib/commit/bf36dd1e66d373c53666ca4579649f767955ed42

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 08:36):

OK, I've PR'd my file for review here.

view this post on Zulip Johan Commelin (Oct 05 2018 at 08:39):

You don't have write access to the community fork?

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 08:39):

Oh, I guess not.

view this post on Zulip Johan Commelin (Oct 05 2018 at 08:40):

@Mario Carneiro @Simon Hudon can one of you fix this?

view this post on Zulip Simon Hudon (Oct 05 2018 at 08:57):

Done

view this post on Zulip Simon Hudon (Oct 05 2018 at 08:58):

And now, I'm off. Good day!

view this post on Zulip Johan Commelin (Oct 05 2018 at 08:58):

Sleep tight!

view this post on Zulip Simon Hudon (Oct 05 2018 at 08:59):

Thanks :) :zzz:

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 13:19):

Thanks Simon!

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 13:27):

I've gone ahead and merged my PR. Here are two specific questions, and I would appreciate any other comments as well:

1) I'm not sure how to finish this proof.

2) The forward and backward directions in the iff.intro here are identical except that the roles of s₁ and s₂ are swapped. Is there a cleaner way to do this? I thought about using wlog but I couldn't figure out how to use it in this case.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:00):

1) I'm not sure how to finish this proof.

Oh I love these questions. Mathematicians don't even give them a second thought. You have two finite types with the same cardinality and and you want to conclude that some operation on the type which only depends on the cardinality (e.g. the cardinality of the number of partitions) is the same for each. This is stupidly hard to do in Lean and it's coming up more and more. The general problem is that if you have two types which are equivalent (i.e. you are given inverse bijections between the types and proofs that the maps are inverse to each other on both sides) then a mathematician instantly identifies the types, and any reasonable theorem or definition constructed with one has an obvious counterpart for the other. Now someone will explain that yeah in theory this can all be done with traversable or transportable or something, but I can't do this because I don't really understand what needs to be done. We've just missed @Simon Hudon but he knows something about this sort of question. My guess is that you need to prove that if the cards are the same then there's an equiv (which might well be there), and then you want to prove that if X equiv Y then partitions X equiv partitions Y (which looks trivial but might involve some actual work) and then you want to prove that partitions X equiv partitions Y then the cards are the same, which might well be there.

view this post on Zulip Simon Hudon (Oct 05 2018 at 15:07):

Thanks for cueing me in @Kevin Buzzard! That is indeed a nice question!

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 15:08):

if the cards are the same then there's an equiv (which might well be there),

Yeah, I was attempting to use fintype.equiv_finfor that but it gives me an equiv wrapped up in trunc... so I gave up and decided to ask for help.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:20):

The example I ran into in around Feb/Mar time was that I had a complex of abelian groups A -> B -> C and an isomorphic (in the obvious sense) complex A' -> B' -> C' and wanted to deduce that these two complexes had isomorphic cohomology -- in fact I had several questions of this nature. I wanted the isomorphism to be explictly built for me by a tactic but in the end I don't think this ever happened.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:21):

People ground out proofs very quickly -- "this is an isomorphism and this is an isomorphism so this map between kernels is an isomorphism, and now this map between images is an isomorphism, and..." but they really had to build them

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:22):

But I want proof by a tactic called mathematical_intuition or transport_de_structure or something

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:25):

and my understanding was that making a tactic would somehow involve having to go through a bunch of Lean theorems or definitions applying to abelian groups, and tagging them with an attribute which is a claim that this function some of whose inputs or outputs are abelian groups "naturally" descends to a function whose inputs and outputs are equivalence classes of abelian groups, where the equivalence is given by group isomorphism.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:26):

And I think the idea was that some of the attribute-tagging could be done automatically.

view this post on Zulip Simon Hudon (Oct 05 2018 at 15:26):

@Kevin Buzzard I did build some isomorphisms with a tactic but I got some push back because transport was seem as redundant with transfer and I didn't take it any further

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:26):

transfer, that's it.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:26):

Thanks Simon.

view this post on Zulip Simon Hudon (Oct 05 2018 at 15:27):

:+1:

view this post on Zulip Simon Hudon (Oct 05 2018 at 15:27):

@Bryan Gin-ge Chen trunc should not deter you. You can unwrap it when you're proving a proposition.

view this post on Zulip Simon Hudon (Oct 05 2018 at 15:28):

It just states that the object exists in a non constructive way

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:28):

This is an important tactic for mathematicians and it isn't there. Bryan's question is a great example of an EIMHIL questions (easy in maths, hard in Lean). The exciting thing about this community is that several times in the past I have explicitly flagged things which were easy in maths but hard in Lean, and other members of the community like Simon, Mario and Johannes sometimes step up and make them easy in Lean. The ring tactic is a great example of this.

view this post on Zulip Simon Hudon (Oct 05 2018 at 15:28):

Look at trunc.induction_on

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:29):

Simon, do you know if is there a relatively easy way to patch up the sorry completely?

view this post on Zulip Simon Hudon (Oct 05 2018 at 15:29):

:D Glad to be helpful. I think Lean won't be as easy as math (!) but there certainly are a lot of low hanging fruits to make it a lot easier to use.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:30):

@Jeremy Avigad I would be really interested to hear your opinion on what a mathematician means when they say that two objects are "canonically isomorphic".

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:30):

This is notion which is somehow still missing in my Lean experience.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:31):

I contributed to some mathoverflow chat about this once

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:32):

https://mathoverflow.net/questions/19644/what-is-the-definition-of-canonical/19663#19663

view this post on Zulip Simon Hudon (Oct 05 2018 at 15:32):

Simon, do you know if is there a relatively easy way to patch up the sorry completely?

I'll look into it

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:33):

Oh I just wondered whether you knew immediately that this would be a relatively straightforward sorry to remove. Like when Patrick asks silly questions about subs on nats not working properly and I know I can prove every one because I just know how they work better than he does in some funny way.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:34):

I think he can do them too, but they just annoy him too much :-)

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 15:34):

@Simon Hudon Ah, thanks! Up to now I've been getting away with just applying lemmas and not really thinking much about how things are actually set up using inductive types and such, but now I should probably turn my brain on.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:34):

but I have no idea whether Bryan's sorry is easy to fill in or not. In some sense Neil Strickland is exhibiting a problem with doing mathematics in Lean here.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:36):

And it's a problem I stumbled upon when doing schemes and so no doubt is looming when the perfectoid project gets really moving again

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:36):

We will need to be replacing complete topological rings with canonically isomorphic complete topological rings left right and centre.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 15:38):

where by canonically isomorphic I mean an explicit equiv of morphisms in the appropriate category.

view this post on Zulip Simon Hudon (Oct 05 2018 at 15:43):

@Bryan Gin-ge Chen It's a common experience I find. E. W. Dijkstra had a nice way to put it: just let the symbols do the work.

view this post on Zulip Simon Hudon (Oct 05 2018 at 15:44):

It's taking me a little bit to boot up my brain but I have my coffee now so I should be able to understand a bit more. But Kevin had the right idea I think: you need a congruence lemma for partition with regards to equiv

view this post on Zulip Simon Hudon (Oct 05 2018 at 15:45):

For the rest, let's see where the symbols take us

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:12):

@Mario Carneiro is that sorry above easy to fill in?

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 16:12):

OK, I think I have a rough idea of what to look at now. It's rather hard to figure out how to use something new, e.g. equiv when there isn't a chapter of TPiL to fall back on. It doesn't help that core lean has has_equiv which is apparently just unrelated notation. At least mathlib itself provides plenty of example code to learn from. Anyways, hopefully these tutorials will help future users...

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:12):

https://github.com/leanprover-community/mathlib/blob/tutorials/tutorials/partitions.lean#L96

view this post on Zulip Simon Hudon (Oct 05 2018 at 16:13):

I'm almost done proving:

lemma card_eq_of_equiv {s : finset α} {t : finset β} (h : s.to_set  t.to_set) :
  s.card = t.card :=  ...

if you want to wait a moment

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:13):

equiv X Y is the best kind of bijection between two types X and Y.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:14):

It's an explicit map from X to Y and an explicit inverse.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:15):

Just saying "there's a map and it's a bijection" is slightly less information in Lean, because they need the computer science version of the axiom of choice (getting data from proofs of existence), so equiv is the important one to focus on.

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 16:15):

@Simon Hudon Cool! I'm still digesting other code so you'll probably finish before I even get close to attempting my own version.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:15):

The problem is that equiv is what mathematicians would think of as a canonical bijection between two sets.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:16):

There are other equivs too -- group isomorphisms, topological space isomorphism etc.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:17):

And then there is a whole bunch of stuff defined on types or groups or whatever, which descends to the equivalence classes under these various equivalence relations.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:18):

And for mathematicians these are all "proof by obvious", so it's clear there's a tactic brewing. But we don't have that tactic yet.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 16:20):

And without it, replacing a topological monoid with a canonically isomorphic topological monoid in a complex of topological monoids and then proving that the cohomology of the complex "hasn't changed" (when Lean actually can see that it _has_ changed in some sense) is going to be hard work I think.

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 16:25):

It's certainly eye-opening (in a good way, probably). I remember having vaguely similar feelings about all the calculus I thought I knew when I took analysis.

view this post on Zulip Simon Hudon (Oct 05 2018 at 16:56):

@Bryan Gin-ge Chen The short answer to your question is: yes it's feasible. You need congruence of partitions with regards to equiv and congruence of card with regards to congruence as well. I'm completing the proof now if you want it. It you want to do it yourself, you can use these three hints:

1. prove congruence of partitions
2. prove congruence of card
3. use trunc.induction_on

view this post on Zulip Bryan Gin-ge Chen (Oct 05 2018 at 17:05):

@Simon Hudon Great, thanks so much! Feel free to push your proofs into the tutorials branch if you'd like. I'll try to study them and add tutorial-style documentation later on.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:07):

@Simon Hudon Great, thanks so much! Feel free to push your proofs into the tutorials branch if you'd like. I'll try to study them and add tutorial-style documentation later on.

This should not be being documented. This should be being hidden by tactics, no?

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:08):

"We now do a big song and dance to replace an object with a canonically isomorphic object". I'm sure the mathematicians would be fascinated :-)

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:08):

I think there's something missing here.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:09):

It's rw for data somehow

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

We want a rw that eats equivs, not equalities and iffs, and works for data in situations where we only care about the answer up to canonical isomorphism.

view this post on Zulip Simon Hudon (Oct 05 2018 at 17:12):

That would be nice. It involves proving congruence about a ton of functions though. The nice thing about = is that every function preserves it.

view this post on Zulip Simon Hudon (Oct 05 2018 at 17:13):

Such a tactic as you're describing is doable. We only need to decide how high it needs to be on the priority list

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

I think we've had this discussion before. Wasn't there some hope that by proving some lemmas about the basic constructors in Lean one could then go on and get a machine to generate all the congruence lemmas automatically?

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:16):

Can the transfer tactic be turned into this mega-rw tactic? Very often in mathematics people only care about the answer up to isomorphism or perhaps a well-defined notion of canonical isomorphism (maybe it's part of the story that the object is unique up to unique isomorphism, for example).

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:18):

we want to be able to rewrite isomorphic perfectoid spaces. Is Lean up to that?

view this post on Zulip Simon Hudon (Oct 05 2018 at 17:22):

I remember building group isomorphism from their underlying type isomorphism but I don't remember the rest of the discussion that you're referring to.

view this post on Zulip Simon Hudon (Oct 05 2018 at 17:23):

But in my libraries, I have some code to construct an isomorphism from an arbitrary type to sums and pairs. With Jeremy, we're talking about adding support for reasoning about W-types which should complete the picture to building isomorphism to canonical type representations

view this post on Zulip Simon Hudon (Oct 05 2018 at 17:25):

Maybe that's what you're looking for?

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:37):

I'm looking for magic

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:37):

example (X Y : Type) (f : Type → Type) (h : equiv X Y) : equiv (f X) (f Y) := by rw h

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:37):

Mario sometimes tells me that this isn't always true, but I'm not sure I've ever seen a mathematical example of it going wrong.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:38):

Here equiv could mean an equiv of structures, and then f is somehow known to preserve all the structure.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:39):

Is that magic Simon?

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:40):

This time round I have a far more mature understanding of what I think is missing.

view this post on Zulip Simon Hudon (Oct 05 2018 at 17:43):

What we probably need is a type class to tell us that f preserves equiv. Then iso_rw h (a tactic we want to build) would know how to build the proof. As it is, rw builds its proofs using congr_arg and congr_fun which needs no assumptions about f. We need basically the same tools for equiv.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:45):

It would be interesting to find out when this is going to bite the perfectoid project and how badly it will bite it. With schemes it bit us when we were doing structure sheaves. Here we only have structure presheaves but who knows.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:46):

In the schemes project I ended up writing some really weird code.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:51):

https://github.com/kbuzzard/lean-stacks-project/blob/53bea440dc519a1f6d023cbecc2dfe270499bbbf/src/tag01HR.lean#L210

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:52):

Over 350 (admittedly very inelegant and much commented) lines of code, to prove something which de Jong dismisses with one throwaway comment.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:55):

"Thus we may apply Algebra, Lemma 10.23.1 to the module MfM_f over RfR_f and the elements g1,,gng_1,\ldots,g_n." Note that Chris had already proved the lemma. The issue was applying it.

view this post on Zulip Kevin Buzzard (Oct 05 2018 at 17:56):

because R[1/f][1/g]R[1/f][1/g] was only canonically isomorphic to R[1/fg]R[1/fg]

view this post on Zulip Scott Morrison (Oct 05 2018 at 21:48):

"We now do a big song and dance to replace an object with a canonically isomorphic object". I'm sure the mathematicians would be fascinated :-)

@Kevin Buzzard, have you seen @David Michael Roberts attempt to summarise the latest disagreement between Mochizuki and Scholze? <https://thehighergeometer.files.wordpress.com/2018/09/mochizuki_final1.pdf>. It's very much about whether such replacements were valid or not.

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 00:41):

Wow I had not seen that. Thanks.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 04:49):

Is there an easy proof of this (is it secretly in mathlib)? I did this the hard way with ext and lots of digging back and forth through exists statements:

def embedding_of_finset {β : Type*} (f : α  β) : finset α  finset β :=
⟨λ S, S.map f, by {
  unfold function.injective,
  intros a₁ a₂ h,
  simp [finset.ext] at h ,
  intro x,
  split,
  { intro H,
    have hex := (h (f x)).mp (exists.intro x H, rfl),
    exact exists.elim hex (by { intros y hy,
      have : y = x := f.2 hy.2,
      exact this  hy.1 }) },
  { intro H,
    have hex := (h (f x)).mpr (exists.intro x H, rfl),
    exact exists.elim hex (by { intros y hy,
      have : y = x := f.2 hy.2,
      exact this  hy.1 }) } }

view this post on Zulip Johan Commelin (Oct 06 2018 at 05:05):

"We now do a big song and dance to replace an object with a canonically isomorphic object". I'm sure the mathematicians would be fascinated :-)

@Kevin Buzzard, have you seen @David Michael Roberts attempt to summarise the latest disagreement between Mochizuki and Scholze? <https://thehighergeometer.files.wordpress.com/2018/09/mochizuki_final1.pdf>. It's very much about whether such replacements were valid or not.

@David Michael Roberts Thanks for writing these!

view this post on Zulip Mario Carneiro (Oct 06 2018 at 05:10):

oops... I was too focused on the image properties and forgot about the fact that the function is injective

view this post on Zulip Simon Hudon (Oct 06 2018 at 05:22):

I pushed something like that to tutorial and called it map'

view this post on Zulip Simon Hudon (Oct 06 2018 at 05:24):

Also, I finished the proof of card_partitions_eq_card_partitions_fin in the partition tutorial. It needed much more work than I thought

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 05:24):

Ah, perfect! I was so engrossed in my attempt that I missed your commit.

view this post on Zulip Simon Hudon (Oct 06 2018 at 05:25):

The big changes that I made was using finset.sup in the formulation of partition instead of using multisets which required a few lemmas in finset

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 05:40):

Very nice! Using sup is much cleaner than the hack I was using with multiset.

Here's what I had. Now that I've looked at what you did, I see there's still a ton of stuff needed to fill in the sorry at line 292. In particular I hadn't even started on something like partitions_congr yet and that was definitely also necessary.

view this post on Zulip David Michael Roberts (Oct 06 2018 at 05:48):

"We now do a big song and dance to replace an object with a canonically isomorphic object". I'm sure the mathematicians would be fascinated :-)

@Kevin Buzzard, have you seen @David Michael Roberts attempt to summarise the latest disagreement between Mochizuki and Scholze? <https://thehighergeometer.files.wordpress.com/2018/09/mochizuki_final1.pdf>. It's very much about whether such replacements were valid or not.

@David Michael Roberts Thanks for writing these!

You're welcome!

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 06:16):

@Simon Hudon Just a heads-up, I'm rebuilding tutorial and I think your changes to ext have broken the proofs of various things in category_theory and holor.

view this post on Zulip Simon Hudon (Oct 06 2018 at 06:17):

Sorry about that. You can revert them for now.

view this post on Zulip Simon Hudon (Oct 06 2018 at 06:20):

For the last sorry, do you need the lattice to be different from the lattice on finite sets?

view this post on Zulip Simon Hudon (Oct 06 2018 at 06:22):

Ok, I see your definition of subset. I'll pick it up tomorrow if you haven't managed to solve it

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 06:23):

Yeah, I was thinking of implementing as a bonus the lattice structure described here.

view this post on Zulip Simon Hudon (Oct 06 2018 at 06:25):

Ah! I see! You can somehow decrease a partition by taking one of its parts and splitting it, right?

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 06:25):

Exactly.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 06:30):

I think I could muddle my way through that eventually, though you're definitely welcome to work on it if you want to. I'd also appreciate comments on the other proofs / tutorial text that I've added if you've had a chance to look at them.

view this post on Zulip Mario Carneiro (Oct 06 2018 at 06:45):

If you use equivalence relations instead of partitions, this follows from the fact that equivalence relations have a Moore structure (they are closed under arbitrary intersection), so they have a complete lattice structure

view this post on Zulip Johan Commelin (Oct 06 2018 at 06:49):

@Bryan Gin-ge Chen https://github.com/leanprover-community/mathlib/blob/tutorials/tutorials/partitions.lean#L109 Couldn't you just compare the multiset.join to the multiset that underlies our finset?

view this post on Zulip Johan Commelin (Oct 06 2018 at 06:58):

@Bryan Gin-ge Chen Consider adding an example to https://github.com/leanprover-community/mathlib/blob/tutorials/tutorials/partitions.lean#L193 where the issue is multiplicity > 1.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 07:06):

@Bryan Gin-ge Chen https://github.com/leanprover-community/mathlib/blob/tutorials/tutorials/partitions.lean#L109 Couldn't you just compare the multiset.join to the multiset that underlies our finset?

Thanks for pointing this out. In fact, Simon has created a better solution for this using sup which is used in partition_of_disjoint_union right below. I'll edit...

I've added this example:

#eval (is_partition ({{0}, {1}, {1,3}} : finset (finset (fin 4))) : bool) -- ff

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:08):

I think this file could stand to be generalized quite a bit. I would want to see partitions defined as equivalence relations, forget the finiteness constraint, and forget the finset representatives

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:08):

Then, given this, you can define the Bell numbers by a recurrence (so they compute fast), and prove that the number of partitions on a finite set is a bell number

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:09):

At the same time, you can define an efficiently computable finset representation of a partition by recursion rather than filtering the universe

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:10):

this both proves the recursion scheme for calculating its size, and also gives an efficiently computable partition function on finset

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 07:11):

That sounds cool. Is there a good place to read about this approach?

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:11):

not particularly... basically finsets are bad for proving stuff when you don't need finiteness explicitly

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:12):

you should use sets instead

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:12):

especially since "partition" generalizes so nicely to the infinite case

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:13):

If you need more details about some part about that let me know

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:14):

It would be nice to have the Bell triangle used for calculating and defining the bell numbers

view this post on Zulip Johan Commelin (Oct 06 2018 at 07:23):

I guess Lean automatically memoizes computations? If I define A n k = A (n-1) k + A n (k - 1), and I ask it to compute A 10 5, does that lead to combinatorial explosion? Or will it efficiently remember the terms it computed?

view this post on Zulip Johan Commelin (Oct 06 2018 at 07:23):

@Simon Hudon Do you know this?

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:36):

Just for fun:

def bell_aux₁ :    × list    × list 
| n (r, l) := (r, n :: l)

def bell_triangle :   list    × list 
| n [] := (n, [])
| n (m :: l) := let n' := n + m in bell_aux₁ n' (bell_triangle n' l)

def bell_aux :    × list 
| 0     := (1, [])
| (k+1) := let (n, l) := bell_aux k in bell_aux₁ n (bell_triangle n l)

def bell (n : ) :  := (bell_aux n).1

#eval list.map bell (list.range 20)

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:37):

lean does not memoize things unless you tell it to. This is one of the major shortcomings of lean 3

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 07:47):

Is the efficient partition function on finset that you had in mind one based on the "Combinatorial Interpretation" in the Bell triangle wiki page?

view this post on Zulip Johan Commelin (Oct 06 2018 at 07:47):

Do we have a memoize monad that automagically does that for you?

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:48):

I PR'd one to core back in the day, rejected

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:49):

To do it in pure lean requires explicit maintenance of the accumulator data, in this case the list nat that forms the lines of the triangle as we progress

view this post on Zulip Johan Commelin (Oct 06 2018 at 07:50):

Right, but a pure Lean version might already be nice.

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:50):

@Bryan Gin-ge Chen Yes. That description of how to count partitions is exactly what you need to write a partition generating algorithm that obviously has length B_n

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:51):

Lean can't figure out your accumulator data for you, at least not effectively

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:51):

For example it's not completely obvious that you can calculate fibonacci numbers with a two number sliding window

view this post on Zulip Johan Commelin (Oct 06 2018 at 07:53):

I was thinking about a naive cache that would just remember all Fibonacci numbers. Don't bother about two number sliding windows. Or am I missing something?

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:55):

Well, yes that can be done, indeed that's how lean used to work

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:56):

Leo decided that this causes unpredictable performance characteristics (since it depends on how the equation compiler compiles your code)

view this post on Zulip Mario Carneiro (Oct 06 2018 at 07:56):

so now it just follows what you tell it, and if you use a bad algorithm then it's your fault

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2018 at 16:48):

@Simon Hudon I've just pushed a commit that moves the more general lemmas you wrote in partitions to more appropriate places in data.finset, data.fintype and data.equiv.basic. Also, one of the tactic.tfae tests still fails, even after I reverted the tactic.ext change.

For now I think I'll leave the tutorial partitions file alone and see if I can make some progress working on Mario's idea in another file. If that turns out well that we can then decide whether we want to completely replace what we've done or perhaps include both approaches.

view this post on Zulip Simon Hudon (Oct 06 2018 at 22:01):

The tfae problem is separate. Maybe we should just remove it from master while I fix it

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 01:37):

@Mario Carneiro I'm stuck on something dumb:

import data.set.lattice

open function

variable (α : Type*)

/- We define a partition as a family of sets associated to an equivalence relation on a set -/

structure partition :=
(blocks : set (set α))
(empty_not_mem_blocks : blocks)
(blocks_partition :  a,  b, b  blocks  a  b   b'  blocks, b  b'  a  b')

def coe_of_setoid [setoid α] : partition α :=
{ blocks := {t |  (s₁ s₂), s₁  t  s₂  t  s₁  s₂ },
  empty_not_mem_blocks := sorry,
  blocks_partition := sorry }

I can't seem to prove that the empty set isn't contained in blocks. I also tried blocks := {t | ∃ a, s ∈ t → a ≈ s} without success.

view this post on Zulip Mario Carneiro (Oct 07 2018 at 01:39):

blocks := {t | ∃ a, {b | a ≈ b} = t}

view this post on Zulip Mario Carneiro (Oct 07 2018 at 01:39):

You can also write this as the range of a function

view this post on Zulip Mario Carneiro (Oct 07 2018 at 01:41):

blocks := {t | ∃ a, s ∈ t → a ≈ s}

This gives the set of subsets of some equivalence class

blocks := {t | ∀ (s₁ s₂), s₁ ∈ t → s₂ ∈ t → s₁ ≈ s₂ }

This gives the set of unions of equivalence classes

view this post on Zulip Mario Carneiro (Oct 07 2018 at 01:42):

(empty_not_mem_blocks : blocks)

The type on this isn't quite right...

view this post on Zulip Mario Carneiro (Oct 07 2018 at 01:43):

But I don't think you should think much about this definition of partition. As far as possible you should just use equivalence relations

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 01:44):

Ah, thanks! I need to be more careful...

I do have (empty_not_mem_blocks : ∅ ∉ blocks). I think I accidentally deleted it when I was writing my previous message.

view this post on Zulip Mario Carneiro (Oct 07 2018 at 01:45):

I would hope to be able to use quot to talk about equivalence classes, rather than sets

view this post on Zulip Mario Carneiro (Oct 07 2018 at 01:45):

but that doesn't fit in this definition of partition

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 01:49):

OK, so I should just try to define poset / lattice instances on setoid α.

view this post on Zulip Mario Carneiro (Oct 07 2018 at 01:55):

yes, that should work

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 02:56):

This works:

instance : has_subset (setoid α) :=
⟨λ r₁ r₂,  (a : α), let r1 := r₁.r in let r2 := r₂.r in {b | r1 a b}  {b | r2 a b}

This fails:

instance a22 : has_subset (setoid α) :=
⟨λ r₁ r₂,  (a : α), {b | r₁.r a b}  {b | r₂.r a b}
/- invalid field notation, function 'setoid.r' does not have explicit argument with type (setoid ...) -/

Anyone know why?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 03:47):

Usually the simp proves these equalities between structures, but not this time:

theorem setoid_eq_iff_r_eq :  {r₁ r₂ : setoid α}, r₁ = r₂  r₁.r = r₂.r
| r1, e1 r2, e2
:= begin
  simp,
  sorry
end

What's the right way to do this? I don't know how to project out what I want from the equality r₁ = r₂ between setoid structures.

view this post on Zulip Simon Hudon (Oct 07 2018 at 04:02):

You can use cases on r1, r2, split the equivalence and use cases on the equality assumption in both cases.

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 04:10):

Thanks. Did you mean something like this?

theorem eq_iff_r_eq :  {r₁ r₂ : setoid α}, r₁ = r₂  r₁.r = r₂.r
| r1, e1 r2, e2
:= begin
  intros,
  split,
  { intro h,
    cases h, },
  {  }
end

I'm getting a rather unhelpful error: cases tactic failed, unexpected failure when introducing auxiliary equatilies.

view this post on Zulip Simon Hudon (Oct 07 2018 at 04:11):

That's odd. Try injection h, maybe that'll work

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 04:17):

Yep, that worked. I don't know how to use cases in the second case though, since now the equality between structures is now in the goal.

view this post on Zulip Simon Hudon (Oct 07 2018 at 04:18):

you can do subst h

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 04:21):

intro h, subst h gives this error:

subst tactic failed, hypothesis 'h' is not of the form (x = t) or (t = x)
state:
α : Type u_1,
eq_iff_r_eq :  {r₁ r₂ : setoid α}, r₁ = r₂  @r α r₁ = @r α r₂,
r1 : α  α  Prop,
e1 : @equivalence α r1,
r2 : α  α  Prop,
e2 : @equivalence α r2,
h : @r α (@mk α r1 e1) = @r α (@mk α r2 e2)
 @mk α r1 e1 = @mk α r2 e2

view this post on Zulip Simon Hudon (Oct 07 2018 at 04:22):

What if you do dsimp at h first?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 04:22):

Ah, perfect! Thanks so much!

view this post on Zulip Simon Hudon (Oct 07 2018 at 04:24):

:+1:

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 06:20):

Here's the WIP complete lattice instance on setoids. I've completed the poset stuff and inf, top, bot but not much else, so a lot of the theorems are just broken skeletons from e.g. data.set.basic.

Is there a clean way of defining the sup / union / join operation? This boils down to something like two elements a z are equivalent in the transitive closure of r1 and r2 if there exists a finite chain of equivalences r1 a b, r2 b c, r1 c d, ... , r_ y z.

view this post on Zulip Simon Hudon (Oct 07 2018 at 06:25):

Aren't the relations in the setoid equivalences? They should be already transitive, symmetric and reflexive. sup and inf of f : a -> b -> b -> Prop should be λ x y, ∃ i, f i x y and λ x y, ∀ i, f i x y respectively

view this post on Zulip Mario Carneiro (Oct 07 2018 at 06:29):

Note that eqv_gen will allow you to take the "span" of an arbitrary relation, so you can just union up a bunch of things and take the span for the supremum

view this post on Zulip Simon Hudon (Oct 07 2018 at 06:44):

What's the span of a relation?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 06:58):

@Simon Hudon I'm not sure I understand. I guess your f is a family of equivalence relations indexed by a? I think your inf agrees with what I have, but I don't think your sup is the correct one. Consider the following two equivalence relations r1 and r2 on the nats, the equivalence classes of r1 are {0,1}, {2,3}, {4,5}, ... and the equivalence classes of r2 are {0}, {1,2}, {3,4}, {5,6}, .... The sup of r1 and r2 has only one equivalence class equal to nat, so in particular 0 is equivalent to 1000, but you need a very long chain of r1 and r2 relations to witness it.

view this post on Zulip Mario Carneiro (Oct 07 2018 at 06:59):

eqv_gen is the equivalence closure of a relation, this is what Bryan wants

view this post on Zulip Mario Carneiro (Oct 07 2018 at 07:01):

Because equivalence relations are closed under arbitrary intersection, you can construct a generic "span" function that gets the smallest equivalence relation including some specified relation, and eqv_gen is this

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 07:05):

Thanks Mario! eqv_gen looks promising. It will probably take me some time to figure out how to use it though.

view this post on Zulip Mario Carneiro (Oct 07 2018 at 07:08):

In your case I think you want to take the eqv_gen of Simon's relation λ x y, ∃ i, f i x y

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 07:16):

OK great, I think I'm starting to get it. I think I would have never found this definition on my own.

view this post on Zulip Mario Carneiro (Oct 07 2018 at 07:19):

Note that it's not required to use that definition, and indeed there is a more "abstract nonsense" definition that makes the proof obligations easier. Define the intersection of an arbitrary indexed family of equivalence relations using Simon's definition; it is straightforward to show this is an equivalence relation. From this, you can define every other element of the complete lattice structure, the inf, the sup, the Sup, the top and bot

view this post on Zulip Simon Hudon (Oct 07 2018 at 07:20):

Do you use "abstract nonsense" interchangeably with category theory?

view this post on Zulip Mario Carneiro (Oct 07 2018 at 07:23):

in this case it's lattice theory

view this post on Zulip Mario Carneiro (Oct 07 2018 at 07:24):

but I guess posets are categories, so sure

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 07:25):

So I see that the intersection works, but how do I get the union from it? Would I have to define it using the finite chains of relations manually?

view this post on Zulip Simon Hudon (Oct 07 2018 at 07:46):

I haven't looked at that function too closely but I think you could take the union as I defined it and take its transitive, symmetric, reflexive closure

view this post on Zulip Simon Hudon (Oct 07 2018 at 07:46):

Does that make sense?

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

Do you use "abstract nonsense" interchangeably with category theory?

This is the most common usage of the phrase "abstract nonsense" when you see it in the mathematical literature, but the category theory in question can range from a simple diagram chase to the adjoint functor theorem and possibly beyond.

view this post on Zulip Mario Carneiro (Oct 07 2018 at 08:20):

You don't need to take any reflexive symmetric closures with the approach I suggested

view this post on Zulip Mario Carneiro (Oct 07 2018 at 08:20):

Given an intersection construction, you can define the supremum as the intersection of all equivalence classes containing the inputs

view this post on Zulip Patrick Massot (Oct 07 2018 at 08:21):

(deleted)

view this post on Zulip Simon Hudon (Oct 07 2018 at 08:24):

But what about the union?

view this post on Zulip Mario Carneiro (Oct 07 2018 at 08:24):

that is the union

view this post on Zulip Mario Carneiro (Oct 07 2018 at 08:24):

i.e. a \sqcup b = Inf {s | a <= s /\ b <= s}

view this post on Zulip Mario Carneiro (Oct 07 2018 at 08:25):

similarly for arbitrary union

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 08:25):

Given an intersection construction, you can define the supremum as the intersection of all equivalence classes containing the inputs

Typo here? Should the supremum be defined in terms of the union of [...]

view this post on Zulip Mario Carneiro (Oct 07 2018 at 08:25):

no

view this post on Zulip Mario Carneiro (Oct 07 2018 at 08:25):

Think of it as an approximation of the union "from above"

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 08:26):

Ah, OK.

view this post on Zulip Mario Carneiro (Oct 07 2018 at 08:26):

the union is the LEAST upper bound, so you can just take the infimum of upper bounds

view this post on Zulip Kenny Lau (Oct 07 2018 at 08:28):

are there any sorry that I can fill?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 08:31):

Feel free to consider any broken proof in my files as a sorry. I'm not actively working on it at the moment.

view this post on Zulip Kenny Lau (Oct 07 2018 at 08:34):

do I need to compile for 1 hour to find out which proof is broken?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 08:37):

Ah, OK. Well inter_subset_right, inter_subset_left, subset_inter are broken but the statements should be right. You can just delete their proofs and fill them in. Let me see if there are others.

view this post on Zulip Kenny Lau (Oct 07 2018 at 08:37):

again, I need to compile for 1 hour to build this branch

view this post on Zulip Kenny Lau (Oct 07 2018 at 08:37):

so I don't really know what I can do

view this post on Zulip Kenny Lau (Oct 07 2018 at 08:37):

how do other people work on this branch?

view this post on Zulip Kenny Lau (Oct 07 2018 at 08:38):

how does @Simon Hudon work on this branch?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 08:40):

I guess we've all got faster computers? It takes my computer about 10 minutes to compile mathlib.

view this post on Zulip Kenny Lau (Oct 07 2018 at 08:41):

do you have 24 threads?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 08:43):

The Activity monitor says lean is using 14 right now. I just started another build after switching branches. Let's see how long it takes.

view this post on Zulip Kenny Lau (Oct 07 2018 at 08:43):

can't you see how many threads you have?

view this post on Zulip Kenny Lau (Oct 07 2018 at 08:48):

2018-10-07.png

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 08:48):

Do you mean threads across all processes? It's something like 1800 threads and 360 processes. I'm on a 6 core macbook pro.

view this post on Zulip Kenny Lau (Oct 07 2018 at 08:49):

I have 2 cores and 4 threads

view this post on Zulip Kenny Lau (Oct 07 2018 at 08:49):

I'm on a windows surface

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 08:54):

That's really amazing. I'm sure the surface has its advantages.

Oh yeah, you can now bind a key to toggle the infoview live updating in the VS code extension, in case you want to pause the tactic state while lean is busy. It's lean.infoview.toggleUpdating in the keyboard shortcuts.

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 08:55):

This branch seems to be all kinds of screwed up. There's something wrong in data.finset that I have to look at.

view this post on Zulip Kenny Lau (Oct 07 2018 at 08:57):

That's really amazing. I'm sure the surface has its advantages.

I guess it isn't designed to build lean

view this post on Zulip Mario Carneiro (Oct 07 2018 at 09:11):

Yes, an ultrabook is not intended for heavy workstation programming

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 09:25):

tutorial should now build properly. order.partitions is also filled out with sorries, so it should be more clear what's missing.

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 17:32):

Here's my definition for union using eqv_gen (is this right?). Now this is what I need to show union_subset (forgive any typos introduced by my manual prettifying...):

α : Type u_1,
r₁ r₂ r₃ : setoid α,
a : α,
r1 : α  α  Prop :=
  @eqv_gen α (λ (s₁ s₂ : α), @r α r₁ s₁ s₂  @r α r₂ s₁ s₂),
r2 : α  α  Prop := @r α r₃,
x : α,
a_1 : r1 a x,
h23 :  (y : α), @r α r₂ a y  r2 a y,
h13 :  (y : α), @r α r₁ a y  r2 a y
 r2 a x

Here's a very informal argument: a_1 tells us that there's some finite chain of r₁ and r₂ equivalences between a and x, and and we then repeatedly apply h13 and h23 to each of the links of that chain to win. How do I do this?

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 20:56):

I have only half-been paying attention to this thread (and indeed Zulip) but I have a little time before bed. You're trying to prove that if r,s,t are three equivalence relations on a set, and both s and t are subsets of r, then the equivalence relation generated by s and t is a subset of r, right? Do you have that if x is a random relation contained in an equivalence relation r then the equivalence relation generated by x is also contained in r? It's trivial from this, right?

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 20:57):

I'm asking if we have the universal property of "equivalence relation generated by".

view this post on Zulip Kenny Lau (Oct 07 2018 at 20:59):

you mean rec_on

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 20:59):

This would be trivial if you knew that the equivalence relation generated by an arbitrary relation was equal to the intersection of all the equivalence relations containing this relation. Sorry I'm late to the party; there's a lot of other noise in this thread too.

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 21:02):

I think I can do what I want with relation.eqv_gen_mono. That might be the same thing that you're saying.

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:02):

Kenny you're right

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:03):

Is the question "how do I fill in the sorry here: https://github.com/leanprover-community/mathlib/blob/1030f5324363a9213cf4b68f834fad0d124b8a13/order/partitions.lean#L110 "?

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:04):

If so, I am suggesting that you first prove that for an arbitrary relation x and an equiv reln r, x is a subset of r iff the equiv reln generated by x is a subset of r

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:04):

and then the union thing is a triviality

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:05):

and Kenny is suggesting that that the universal property of the relation is just the recursor

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:05):

so this should be hopefully straightforward.

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:05):

Do you want me to try or am I answering the wrong question @Bryan Gin-ge Chen ?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 21:09):

Yes, that was the question. I think I've solved it just now though:

theorem union_subset {r₁ r₂ r₃ : setoid α} (h13 : r₁  r₃) (h23 : r₂  r₃) : r₁  r₂  r₃ :=
begin
  rw [subset_def] at h13 h23 ,
  simp only [set.subset_def, set.mem_set_of_eq] at h13 h23 ,
  rw [union_def, rel_union],
  intros,
  have hor :  a x, @r α r₁ a x  @r α r₂ a x  @r α r₃ a x := by { intros a x h,
    exact or.elim h (h13 a x) (h23 a x) },
  have H := relation.eqv_gen_mono hor a_1,
  have h := (@relation.eqv_gen_iff_of_equivalence _ r₃.r a x r₃.2).mp,
  exact h H
end

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 21:11):

I think relation.eqv_gen_mono is this property you are describing. And it does appear to me to be proved in the way you guys are suggesting. Thanks for the explanation though, without it, I was probably just going to go on not really understanding what was happening under the hood here!

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:31):

@Kenny Lau why did this come out so horrible:

lemma sub_of_gen_sub (x : α  α  Prop) (s : setoid α) (H :  a b : α, x a b  @setoid.r _ s a b) :
 a b : α, (eqv_gen x) a b  @setoid.r _ s a b :=
λ a b H2, eqv_gen.rec_on H2 H
  (@setoid.iseqv α s).1
  (λ x y _ H3, (@setoid.iseqv α s).2.1 H3)
  (λ x y z _ _ H4 H5,(@setoid.iseqv α s).2.2 H4 H5)

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:31):

Oh it's because I should be using a typeclass

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:31):

what do you mean by terrible?

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:31):

oh

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:32):

I didn't use typeclasses because I could see I'd have two equiv relns on alpha

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:32):

well it's a lemma

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:32):

the typeclass is local

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:34):

lemma sub_of_gen_sub {α : Type*} (x : α  α  Prop) [setoid α] (H :  a b : α, x a b  a  b) :
 a b : α, (eqv_gen x) a b  a  b :=
λ a b H2, eqv_gen.rec_on H2 H
  setoid.refl
  (λ _ _ _, setoid.symm)
  (λ _ _ _ _ _, setoid.trans)

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:34):

@Bryan Gin-ge Chen it's not mono, this is a slightly longer way around isn't it? Mono says if x sub y then the equiv reln gen by x is a subset of the equiv reln generated by y. To get the universal property from that you also need that the equiv reln generated by an equiv reln is itself, which is another lemma

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:34):

inb4 galois insertion

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:35):

rofl

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:35):

I can quite believe it.

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 21:35):

Right, you can see I had to use relation.eqv_gen_iff_of_equivalence.

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:35):

although it might be a coinsertion

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:36):

With sub_of_gen_sub (which is a relatively straightforward consequence of the recursor) the proof is simpler.

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:36):

The lemma reduces you to checking that if X and Y are subsets of Z then so is X union Y, which will be in the library

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:38):

I don't really understand

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:38):

It wouldn't surprise me if sub_of_gen_sub is already in the library, perhaps under a better name.

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:38):

this is just the preimage of the canonical embedding from the set of equivalence relations on A to P(A x A)

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:38):

yes

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:39):

Bryan is using subset notation in exactly this way

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:39):

but he's not proving things this way

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 21:39):

I did a search for eqv_gen in mathlib and it only showed up in logic.relation and Kenny's free group file.

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:40):

Kenny I'm sure both Bryan and I would be interested if you were to blow his code out of the water using a more high-powered way of thinking about this question.

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:41):

blow his code out of the water?

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:41):

Bryan, do you know what a Galois insertion is?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 21:42):

I'm about to have dinner, so I'll push what I have. Feel free to make arbitrary changes if you're willing to deal with the compile times.

I was just about to ask whether I ought to know about Galois (co)insertions...

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:42):

So the idea is that the construction sending a random relation to an equivalence relation is an adjoint to the forgetful functor sending an equivalence relation to the underlying relation

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:42):

Kenny I'm sure both Bryan and I would be interested if you were to blow his code out of the water using a more high-powered way of thinking about this question.

I still don't know what the question is

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:42):

https://github.com/leanprover-community/mathlib/blob/1030f5324363a9213cf4b68f834fad0d124b8a13/order/partitions.lean

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:43):

Prove all the lemmas there but in a much better way

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:43):

That's the question

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:43):

I think

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:44):

But the point is that you have something else here too -- these aren't just a pair of adjoint functors, because these are on posets (ordered by inclusion) and not just categories.

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:44):

well give me an hour to compile the mathlib first...

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:44):

I've changed some of the files

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:44):

So there's a special name for this situation, called a Galois insertion.

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:45):

so every time I change some files I need to spend one hour compiling the files

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:45):

And there's a bunch of lemmas proved about Galois insertions which might make these sorts of arguments easier.

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:45):

and in this hour my CPU will be fully used

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:45):

and the computer will be mostly unusable

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:45):

Kenny if you are only working on one branch which isn't master

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:45):

then you should just commit the olean files to master :P

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:45):

then whenever you checkout master again, the olean files will reappear

view this post on Zulip Patrick Massot (Oct 07 2018 at 21:46):

Kenny and Kevin, you should pay attention to what Simon is writing in the nextdoor thread

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:47):

Kenny should -- I can compile mathlib in 10 minutes and I never fiddle with it anyway ;-)

view this post on Zulip Kevin Buzzard (Oct 07 2018 at 21:47):

well...hardly ever

view this post on Zulip Kenny Lau (Oct 07 2018 at 21:53):

do all of you have like 30 cores?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 22:23):

And there's a bunch of lemmas proved about Galois insertions which might make these sorts of arguments easier.

Are these lemmas in mathlib? There doesn't seem to be anything named galois*.

view this post on Zulip Kenny Lau (Oct 07 2018 at 22:23):

galois.*?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 22:23):

Oh oops, I was trying to search the community fork.

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 22:28):

I remember reading about Galois connections whenever I learned about covering spaces. I don't remember insertions and coinsertions but the lean file seems clear enough.

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 22:57):

OK, I see the point now! The smart way to do all of this is to just use lift_complete_lattice on the complete lattice instance on subsets. Presumably that's what Kenny is up to now that an hour has passed. :)

view this post on Zulip Kenny Lau (Oct 07 2018 at 22:59):

oh well I proved this

view this post on Zulip Kenny Lau (Oct 07 2018 at 22:59):

import order.complete_lattice data.fintype

open lattice

instance bounded_lattice.of_fintype_inhabited_lattice
  (α : Type*) [fintype α] [inhabited α] [lattice α] :
  bounded_lattice α :=
{ top := finset.fold () (default α) id finset.univ,
  le_top := begin
    suffices :  a  finset.univ, a  finset.fold () (default α) id finset.univ,
      from λ x, this x (finset.mem_univ x),
    generalize : finset.univ = U,
    cases U with U hu1,
    induction U using quot.ind with L,
    induction L with hd tl ih,
    { exact λ _, false.elim },
    intros x hx,
    rcases hx with rfl | hx,
    { exact le_sup_left },
    transitivity,
    { exact ih (list.nodup_of_nodup_cons hu1) x hx },
    { exact le_sup_right }
  end,
  bot := finset.fold () (default α) id finset.univ,
  bot_le := begin
    suffices :  a  finset.univ, finset.fold () (default α) id finset.univ  a,
      from λ x, this x (finset.mem_univ x),
    generalize : finset.univ = U,
    cases U with U hu1,
    induction U using quot.ind with L,
    induction L with hd tl ih,
    { exact λ _, false.elim },
    intros x hx,
    rcases hx with rfl | hx,
    { exact inf_le_left },
    transitivity,
    { exact inf_le_right },
    { exact ih (list.nodup_of_nodup_cons hu1) x hx }
  end,
  .. (infer_instance : lattice α) }

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:00):

and realized that proving it is a complete lattice is impossible

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 23:01):

Oh are you working on tutorial/partitions.lean or order/partitions.lean?

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:02):

what is the difference?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 23:03):

tutorial/partitions.lean was my first try on finite sets. Mario told me I should do stuff with general sets and then specialize, so I made order/partitions.lean.

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 23:04):

Is the issue with finite partitions that Sup and Inf need to use set?

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:07):

I think we should have an instance of \Pi [fintype \a], bounded_lattice (finset \a)

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:14):

Is the issue with finite partitions that Sup and Inf need to use set?

yes

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 23:16):

That's unfortunate. There should be a version of complete_lattice that works for finsets. Is that what your instance above does?

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:17):

no, that's bounded_lattice

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:17):

I don't think you can prove complete_lattice.

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 23:21):

Partitions of finite sets have a complete lattice structure just as much as partitions of arbitrary sets do, so we should add complete_lattice_finset.

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:22):

I don't think so.

view this post on Zulip Jeremy Avigad (Oct 07 2018 at 23:23):

@Kevin Buzzard I am sorry to be slow to respond to your ping, but I have thought about it and I don't have any great insights here. I don't think the notion of a canonical isomorphism is a sharp concept, and your post gives as good a working definition as any. It would be nice to have automation the finds/constructs them for you.

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 23:26):

@Kenny Lau Why not?

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:26):

because given an arbitrary set of partitions I don't see how you can find its supremum.

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:27):

let's just say our set is A = {0,1}

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:27):

I give you a set S of partitions of A

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:27):

how do you find the supremum of S?

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:28):

let's say S is {{{0},{1}}} if Goldbach conjecture is true and and {} otherwise.

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 23:30):

OK, but for finite partitions I only care about finsets of partitions which can't be that gross, right?

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:31):

but if you want to have a complete_lattice instance then you need to find the supremum for arbitrary sets

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 23:32):

So you're saying that there's not even complete_lattice on setoid, as I was aiming to prove in order/partitions.lean...

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:32):

you can always make a noncomputable def :)

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:32):

(don't make it an instance!)

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 23:40):

I think I'm starting to get it. Do you happen to know which part of the galois insertion between the partial order on equivalence relations and that on subsets of α×α\alpha \times \alpha is noncomputable?

view this post on Zulip Bryan Gin-ge Chen (Oct 07 2018 at 23:41):

@Mario Carneiro What do you think about having a complete_lattice_finset?

view this post on Zulip Kenny Lau (Oct 07 2018 at 23:41):

none of the parts

view this post on Zulip Mario Carneiro (Oct 08 2018 at 00:22):

@Kenny Lau Sup and Inf are inherently noncomputable, just from their types: set A -> A

view this post on Zulip Mario Carneiro (Oct 08 2018 at 00:22):

This means that they take in no data and produce data

view this post on Zulip Kenny Lau (Oct 08 2018 at 00:23):

well set (set A) -> set A is computable though

view this post on Zulip Mario Carneiro (Oct 08 2018 at 00:23):

pointlessly so

view this post on Zulip Mario Carneiro (Oct 08 2018 at 00:23):

you can computabilize any definition of that type

view this post on Zulip Kenny Lau (Oct 08 2018 at 00:23):

aha

view this post on Zulip Kenny Lau (Oct 08 2018 at 00:23):

thanks

view this post on Zulip Johan Commelin (Oct 09 2018 at 06:53):

@Scott Morrison Do you know if Neil got Lean working in the end?

view this post on Zulip Johan Commelin (Oct 09 2018 at 06:53):

@Neil Strickland Aah, you're on this Zulip. Can you confirm?

view this post on Zulip Johan Commelin (Oct 09 2018 at 06:56):

I'm looking at the first "challenge", namely: prove 2 + 2 = 4. Your goal with this challenge is

Key points: basic boilerplate at the top of the file, basic grammar of stating and proving, how to interact with the proof assistant.

But in Lean you won't learn that from 2 + 2 = 4. In idiomatic Lean, a file dedicated to that lemma would contain 1 line:

lemma two_add_two : 2 + 2 = 4 := rfl

No imports, no boiler plate, no interactions, no nothing.

view this post on Zulip Scott Morrison (Oct 09 2018 at 06:56):

I'm not really sure what state we left him in. At Dagstuhl he definitely had a working copy on the laptop he had with him, but that might not still be the case.

view this post on Zulip Johan Commelin (Oct 09 2018 at 06:57):

I think the "Key points" deserve to be in a dedicated tutorial file. But I'm not sure if 2 + 2 = 4 is the right "goal" of that file.

view this post on Zulip Scott Morrison (Oct 09 2018 at 06:58):

Well -- even that file teaches you a few things: the lemma keyword, colon, colon-equals. You could also explain the red and green underlines, and the fact that the absence of these shows Lean approves. (Or ... is just not even running...)

view this post on Zulip Tobias Grosser (Oct 09 2018 at 07:38):

(deleted)

view this post on Zulip Tobias Grosser (Oct 09 2018 at 07:39):

do all of you have like 30 cores?

@Kenny Lau , any reason you don't compile on a proper server?

view this post on Zulip Tobias Grosser (Oct 09 2018 at 07:40):

If you don't have one available, I suggest you get an account at the GCC compile farm: "https://cfarm.tetaneutral.net"

view this post on Zulip Tobias Grosser (Oct 09 2018 at 07:41):

They give accounts to open source contributors and have some servers that are commonly not too busy

view this post on Zulip Tobias Grosser (Oct 09 2018 at 07:41):

gcc20 22, 443 Dual Xeon x86_64 Intel(R) Xeon(R) CPU X5670 @ 2.93GHz 2 CPU
12 cores 24 threads 24105 MB 825.0 GB Debian 7.11 wheezy
3.2.0-4-amd64 1090 days INRIA Rocquencourt France

view this post on Zulip Tobias Grosser (Oct 09 2018 at 07:41):

Is mostly idle today.

view this post on Zulip Tobias Grosser (Oct 09 2018 at 07:42):

If you can get lean compiled on powerpc hardware you can run on IBM Power8 with 160 CPUs

view this post on Zulip Tobias Grosser (Oct 09 2018 at 07:43):

It's also at 99% idle ATM.

view this post on Zulip Mario Carneiro (Oct 09 2018 at 07:46):

I've never heard of this option

view this post on Zulip Mario Carneiro (Oct 09 2018 at 07:46):

Maybe there is a possibility we can set up Jenkins on it as an alternative to Travis?

view this post on Zulip Johan Commelin (Oct 09 2018 at 07:57):

Here is what I just pushed for Challenge 1.
https://github.com/leanprover-community/mathlib/blob/tutorials/tutorials/two_add_two.lean

view this post on Zulip Johan Commelin (Oct 09 2018 at 07:58):

I didn't do any tactics yet. So that should be done in Challenge 2 "Infinitude of primes".

view this post on Zulip Johan Commelin (Oct 09 2018 at 08:07):

@Neil Strickland Would you mind adding a link to https://github.com/leanprover-community/mathlib/tree/tutorials/tutorials in you post on MO? Or is it ok with you if we edit the post while writing tutorials on the 5 challenges that you suggested?

view this post on Zulip Johan Commelin (Oct 09 2018 at 08:11):

General question @Mario Carneiro @Bryan Gin-ge Chen should we leave active #eval and #print statements in these tutorials? Or should they be commented out, so that they don't spam ordinary mathlib-builds. I suppose it is easy enough for the user to uncomment them.

view this post on Zulip Mario Carneiro (Oct 09 2018 at 08:12):

I'm not sure mathlib is the best place for them

view this post on Zulip Johan Commelin (Oct 09 2018 at 08:12):

them what?

view this post on Zulip Mario Carneiro (Oct 09 2018 at 08:13):

the tutorials

view this post on Zulip Johan Commelin (Oct 09 2018 at 08:13):

I think it is

view this post on Zulip Mario Carneiro (Oct 09 2018 at 08:13):

Especially if it is an interactive walkthrough

view this post on Zulip Johan Commelin (Oct 09 2018 at 08:13):

Because it forces us to make sure they compile

view this post on Zulip Mario Carneiro (Oct 09 2018 at 08:14):

I don't know, I mean TPIL has code snippets and they only break occasionally, and it is reported and fixed

view this post on Zulip Mario Carneiro (Oct 09 2018 at 08:15):

It's not like they are going to be based on really complicated things

view this post on Zulip Johan Commelin (Oct 09 2018 at 08:15):

It's not like they are going to be based on really complicated things

One of the challenges is on nilpotent ideals... it would break helplessly by your module refactor.

view this post on Zulip Mario Carneiro (Oct 09 2018 at 08:16):

They could just as easily be in a separate project. Even better, if a user downloads the tutorial project depending on mathlib then they are already in the right place to do work of their own

view this post on Zulip Kenny Lau (Oct 09 2018 at 08:16):

One of the challenges is on nilpotent ideals... it would break helplessly by your module refactor.

what do you mean?

view this post on Zulip Mario Carneiro (Oct 09 2018 at 08:16):

I'm not saying they never change, but they won't change often

view this post on Zulip Johan Commelin (Oct 09 2018 at 08:17):

@Kenny Lau https://mathoverflow.net/a/311159/21815

view this post on Zulip Kenny Lau (Oct 09 2018 at 08:18):

yes?

view this post on Zulip Johan Commelin (Oct 09 2018 at 08:18):

That's homework for us (-;

view this post on Zulip Scott Morrison (Oct 09 2018 at 09:19):

I'd be pretty happy to see tutorials embedded in mathlib for now. Anything to avoid useful stuff bit-rotting away. :-)

view this post on Zulip Sean Leather (Oct 09 2018 at 09:31):

I agree that tutorials should go into in mathlib. I think that, as long as the plan is to keep mathlib monolithic (which seems to be working out for the most part), it should include tutorials. A reasonable alternative is to build a tutorial repository during mathlib's CI test phase.

view this post on Zulip Mario Carneiro (Oct 09 2018 at 09:39):

I still think it is a good idea to have a "scratch" repo that newbies can get to have a working setup in vscode with mathlib already hooked in, since this is the recommended use

view this post on Zulip Johan Commelin (Oct 09 2018 at 09:39):

What do you mean with "recommended use"?

view this post on Zulip Mario Carneiro (Oct 09 2018 at 09:39):

I mean this is the way third parties use mathlib

view this post on Zulip Mario Carneiro (Oct 09 2018 at 09:40):

you have a project, and this project imports mathlib

view this post on Zulip Mario Carneiro (Oct 09 2018 at 09:40):

this is the format vscode is expecting

view this post on Zulip Mario Carneiro (Oct 09 2018 at 09:40):

You can have mathlib as a global install and work with loose files, but I think this approach is less robust

view this post on Zulip Johan Commelin (Oct 09 2018 at 09:41):

Right, but I'm more thinking about mathematicians that want to contribute to mathlib

view this post on Zulip Mario Carneiro (Oct 09 2018 at 09:41):

contributing to mathlib is another thing altogether

view this post on Zulip Johan Commelin (Oct 09 2018 at 09:42):

So they will end up hacking on the community fork asap

view this post on Zulip Mario Carneiro (Oct 09 2018 at 09:42):

sure, in that case they are working on mathlib itself so there is already a project

view this post on Zulip Mario Carneiro (Oct 09 2018 at 09:42):

I mean for new leaners, like the kids in Kevin's classes

view this post on Zulip Johan Commelin (Oct 09 2018 at 09:42):

Right, and they get to know that project by looking in tutorials/

view this post on Zulip Scott Morrison (Oct 09 2018 at 09:43):

A scratch project is a good idea.

view this post on Zulip Johan Commelin (Oct 09 2018 at 09:43):

I see. Well, I was more thinking about people like Neil.

view this post on Zulip Mario Carneiro (Oct 09 2018 at 09:43):

I don't think Neil was ready to be a contributor

view this post on Zulip Scott Morrison (Oct 09 2018 at 09:43):

Just the bare minimum setup, with perhaps a file that reminds them where to go for more help.

view this post on Zulip Mario Carneiro (Oct 09 2018 at 09:43):

I assume people start out with projects on their own for a while, and then move to contribution if they are so inclined

view this post on Zulip Johan Commelin (Oct 09 2018 at 09:43):

https://github.com/leanprover-community/hello-world

view this post on Zulip Scott Morrison (Oct 09 2018 at 09:44):

And as Lean/mathlib improves, we actually hope a larger and larger fraction of the community are _not_ hacking on mathlib!

view this post on Zulip Johan Commelin (Oct 09 2018 at 09:44):

Why?

view this post on Zulip Johan Commelin (Oct 09 2018 at 09:44):

I thought we wanted to be a massive monolith

view this post on Zulip Scott Morrison (Oct 09 2018 at 09:45):

(because they're actually doing maths, rather than filling in all the gaps before they can actually get started)

view this post on Zulip Sean Leather (Oct 09 2018 at 09:45):

There's ambiguity in the word “tutorial.” I was thinking of something more like a walkthrough of various features of mathlib. But a scratch/hello-world repository would also be useful.

view this post on Zulip Johan Commelin (Oct 09 2018 at 09:45):

@Scott Morrison But why not do maths inside mathlib?

view this post on Zulip Scott Morrison (Oct 09 2018 at 09:45):

If I'm going to formalise a bunch of the boring-but-technical lemmas in my research paper, they don't belong in mathlib.

view this post on Zulip Mario Carneiro (Oct 09 2018 at 09:45):

@Sean Leather I guess Kevin's mathlib docs pages already do that?

view this post on Zulip Scott Morrison (Oct 09 2018 at 09:47):

or because they're working out the lemmas for their research project. They don't belong in mathlib because they've got no idea if they're the right lemmas yet. But this is all dreaming. For the next couple of decades, I agree, all in mathlib. :-)

view this post on Zulip Sean Leather (Oct 09 2018 at 09:49):

I guess Kevin's mathlib docs pages already do that?

Not in the sense that you can see examples in Lean of what is provable and how with mathlib.

view this post on Zulip Sean Leather (Oct 09 2018 at 09:51):

Perhaps I'm off-topic here with my own definition of tutorial — I'm not sure — but I was thinking of something that demonstrated usage of mathlib with proofs and words, not just words.

view this post on Zulip Johan Commelin (Oct 09 2018 at 10:23):

@Sean Leather I think we can have both

view this post on Zulip Sean Leather (Oct 09 2018 at 10:24):

@Johan Commelin Yep, we probably should.

view this post on Zulip Kevin Buzzard (Oct 09 2018 at 16:48):

The Xena.zip file which I was going to use with my 1st years this year (until ICT delivered something much better) -- that was precisely what Mario was describing above. The way this seems to work is that once a year I am allowed to update what the Imperial College undergraduates see by default when they open up VS Code. This year they see a project with one file test.lean containing import data.int.basic theorem 2+2=4:=rfl and then all the lean and olean files for mathlib and lean (with mathlib as a dependency). This is what I would now call "the bare minimum for mathematicians who are interested". But it sounds like the community might be able to make a much better variant of this, which we could just generally advertise on GH. I think it's worth stressing that win10 users have no git and no command line, and I've met plenty of people who just want to get going. We make a better repo, and we replace Xena.zip with this repo and I document it on the installation page and people will be happier.

view this post on Zulip Patrick Massot (May 27 2019 at 22:42):

On the plane to Edinburgh, and then in my hotel room, I tried to write a tutorial/show case that we could show to people asking how it feels to use Lean and mathlib (among participants to this conference or other people). The first draft is at https://gist.github.com/PatrickMassot/79d7f53b3777c48e0910e131aedff7ea. Comments are welcome. Maybe we could put it inside our almost empty tutorial folder, or create a tutorial repository. Of course you need a recent mathlib to run it.

view this post on Zulip Johan Commelin (May 28 2019 at 07:08):

Nice work Patrick! The comment on line 57 doesn't typecheck: https://gist.github.com/PatrickMassot/79d7f53b3777c48e0910e131aedff7ea#file-proof_tutorial-lean-L57

view this post on Zulip Johan Commelin (May 28 2019 at 07:10):

s/there/they/ on L97
https://gist.github.com/PatrickMassot/79d7f53b3777c48e0910e131aedff7ea#file-proof_tutorial-lean-L97

view this post on Zulip Johan Commelin (May 28 2019 at 07:14):

s/use/prove/ on L179 https://gist.github.com/PatrickMassot/79d7f53b3777c48e0910e131aedff7ea#file-proof_tutorial-lean-L179

view this post on Zulip Johan Commelin (May 28 2019 at 07:16):

s/re-enter/re-enters/ on L210

view this post on Zulip Johan Commelin (May 28 2019 at 07:21):

@Patrick Massot I really like how you very naturally introduce contrapose, linarith, library_search, and norm_cast. Very good job!

view this post on Zulip Sebastien Gouezel (May 28 2019 at 07:26):

s/le_antisym/le_antisymm on L104

view this post on Zulip Johan Commelin (May 28 2019 at 07:28):

s/coutable/countable/ on L396

view this post on Zulip Mario Carneiro (May 28 2019 at 07:31):

s/infimums/infima/

view this post on Zulip Sebastien Gouezel (May 28 2019 at 07:32):

Missing know on L313. I find this sentence not very clear: I would add "asserting that the inverse of a positive number is positive" after "relevant lemma".

view this post on Zulip Adrian Chu (May 28 2019 at 11:06):

Thank you very much! I enjoy it and find it helpful.

view this post on Zulip Patrick Massot (May 28 2019 at 15:15):

Thanks everybody, I updated the gist. What should we do now? Putting it inside mathlib/docs/tutorial is easy, but maybe creating a Lean tutorial repository containing a Lean project depending on mathlib would be easier to use for people who want to interact with the code. If a beginner follow instructions to start a new project then mathlib/docs/tutorial is hidden in _target/deps

view this post on Zulip Kevin Buzzard (May 28 2019 at 15:30):

One could argue a three lines long proof of this lemma is still two lines too long.

I don't understand my own language, but for some reason it definitely should be "a three line long proof"

view this post on Zulip Sebastien Gouezel (May 28 2019 at 15:38):

Your language is really weird (contrary to French which is always completely logical :)

view this post on Zulip Mario Carneiro (May 28 2019 at 15:43):

I think there is no plural because it is "three-line-long proof"

view this post on Zulip Mario Carneiro (May 28 2019 at 15:43):

although I don't think the hyphens are common

view this post on Zulip Kevin Buzzard (May 28 2019 at 18:07):

I was going to mention hyphens but I couldn't figure out where to put them

view this post on Zulip Kenny Lau (May 28 2019 at 18:09):

it's actually a three-line proof

view this post on Zulip Kenny Lau (May 28 2019 at 18:11):

or "a proof that is three lines long"

view this post on Zulip Johan Commelin (May 28 2019 at 19:31):

I think Patrick just wanted to say that it's a long-proof :oops:

view this post on Zulip Johan Commelin (May 28 2019 at 19:42):

Proper languages just allow you to chain words together whenever that's useful... :grinning_face_with_smiling_eyes:

view this post on Zulip Mario Carneiro (May 28 2019 at 19:44):

*allows

view this post on Zulip Johan Commelin (May 28 2019 at 19:46):

Sorry, typo. I meant "languages"


Last updated: May 17 2021 at 21:12 UTC