## Stream: general

### Topic: Tutorial

#### 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.

#### Johan Commelin (Oct 04 2018 at 06:59):

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

#### Johan Commelin (Oct 04 2018 at 06:59):

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

#### Johan Commelin (Oct 04 2018 at 07:00):

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

#### 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).

Ok, I'll do that

#### 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.

#### 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 (-;

#### 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

#### 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.

#### 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

#### Johannes Hölzl (Oct 04 2018 at 07:20):

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

#### 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

#### 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

#### Kevin Buzzard (Oct 04 2018 at 09:10):

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

#### 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?

#### Johan Commelin (Oct 05 2018 at 08:07):

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

#### Patrick Massot (Oct 05 2018 at 08:10):

I'll create the branch if you want

#### Bryan Gin-ge Chen (Oct 05 2018 at 08:11):

Sure, that'd be great.

#### Patrick Massot (Oct 05 2018 at 08:11):

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

wait

I messed up

now it's ok

#### Patrick Massot (Oct 05 2018 at 08:23):

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

#### Bryan Gin-ge Chen (Oct 05 2018 at 08:36):

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

Oh, I guess not.

#### Johan Commelin (Oct 05 2018 at 08:40):

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

Done

#### Simon Hudon (Oct 05 2018 at 08:58):

And now, I'm off. Good day!

Sleep tight!

Thanks :) :zzz:

Thanks Simon!

#### 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.

#### 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.

#### Simon Hudon (Oct 05 2018 at 15:07):

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

#### 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.

#### 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.

#### 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

#### Kevin Buzzard (Oct 05 2018 at 15:22):

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

#### 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.

#### Kevin Buzzard (Oct 05 2018 at 15:26):

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

#### 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

#### Kevin Buzzard (Oct 05 2018 at 15:26):

transfer, that's it.

Thanks Simon.

:+1:

#### 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.

#### Simon Hudon (Oct 05 2018 at 15:28):

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

#### 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.

#### Simon Hudon (Oct 05 2018 at 15:28):

Look at trunc.induction_on

#### 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?

#### 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.

#### 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".

#### Kevin Buzzard (Oct 05 2018 at 15:30):

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

#### Kevin Buzzard (Oct 05 2018 at 15:32):

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

#### 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

#### 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.

#### Kevin Buzzard (Oct 05 2018 at 15:34):

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

#### 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.

#### 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.

#### 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

#### 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.

#### Kevin Buzzard (Oct 05 2018 at 15:38):

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

#### 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.

#### 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

#### Simon Hudon (Oct 05 2018 at 15:45):

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

#### Kevin Buzzard (Oct 05 2018 at 16:12):

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

#### 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...

#### Kevin Buzzard (Oct 05 2018 at 16:12):

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

#### 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

#### Kevin Buzzard (Oct 05 2018 at 16:13):

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

#### Kevin Buzzard (Oct 05 2018 at 16:14):

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

#### 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.

#### 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.

#### 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.

#### Kevin Buzzard (Oct 05 2018 at 16:16):

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

#### 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.

#### 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.

#### 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.

#### 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.

#### 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

#### 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.

#### 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?

#### 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 :-)

#### Kevin Buzzard (Oct 05 2018 at 17:08):

I think there's something missing here.

#### Kevin Buzzard (Oct 05 2018 at 17:09):

It's rw for data somehow

#### 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.

#### 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.

#### 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

#### 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?

#### 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).

#### Kevin Buzzard (Oct 05 2018 at 17:18):

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

#### 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.

#### 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

#### Simon Hudon (Oct 05 2018 at 17:25):

Maybe that's what you're looking for?

#### Kevin Buzzard (Oct 05 2018 at 17:37):

I'm looking for magic

#### 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

#### 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.

#### 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.

#### Kevin Buzzard (Oct 05 2018 at 17:39):

Is that magic Simon?

#### Kevin Buzzard (Oct 05 2018 at 17:40):

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

#### 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.

#### 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.

#### Kevin Buzzard (Oct 05 2018 at 17:46):

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

#### Kevin Buzzard (Oct 05 2018 at 17:51):

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

#### 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.

#### Kevin Buzzard (Oct 05 2018 at 17:55):

"Thus we may apply Algebra, Lemma 10.23.1 to the module $M_f$ over $R_f$ and the elements $g_1,\ldots,g_n$." Note that Chris had already proved the lemma. The issue was applying it.

#### Kevin Buzzard (Oct 05 2018 at 17:56):

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

#### 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.

#### Kevin Buzzard (Oct 06 2018 at 00:41):

Wow I had not seen that. Thanks.

#### 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 }) } }⟩


#### 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!

#### 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

#### Simon Hudon (Oct 06 2018 at 05:22):

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

#### 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

#### Bryan Gin-ge Chen (Oct 06 2018 at 05:24):

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

#### 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

#### 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.

#### 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!

#### 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.

#### Simon Hudon (Oct 06 2018 at 06:17):

Sorry about that. You can revert them for now.

#### 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?

#### 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

#### Bryan Gin-ge Chen (Oct 06 2018 at 06:23):

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

#### 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?

Exactly.

#### 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.

#### 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

#### 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?

#### 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.

#### 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...

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


#### 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

#### 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

#### 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

#### 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

#### Mario Carneiro (Oct 06 2018 at 07:11):

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

#### Mario Carneiro (Oct 06 2018 at 07:12):

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

#### Mario Carneiro (Oct 06 2018 at 07:13):

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

#### 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

#### 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?

#### Johan Commelin (Oct 06 2018 at 07:23):

@Simon Hudon Do you know this?

#### 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)


#### 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

#### 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?

#### Johan Commelin (Oct 06 2018 at 07:47):

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

#### Mario Carneiro (Oct 06 2018 at 07:48):

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

#### 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

#### Johan Commelin (Oct 06 2018 at 07:50):

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

#### 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

#### Mario Carneiro (Oct 06 2018 at 07:51):

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

#### 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

#### 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?

#### Mario Carneiro (Oct 06 2018 at 07:55):

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

#### 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)

#### 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

#### 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.

#### 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

#### 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.

#### Mario Carneiro (Oct 07 2018 at 01:39):

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

#### Mario Carneiro (Oct 07 2018 at 01:39):

You can also write this as the range of a function

#### 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

#### Mario Carneiro (Oct 07 2018 at 01:42):

(empty_not_mem_blocks : blocks)

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

#### 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

#### 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.

#### 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

#### Mario Carneiro (Oct 07 2018 at 01:45):

but that doesn't fit in this definition of partition

#### Bryan Gin-ge Chen (Oct 07 2018 at 01:49):

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

#### Mario Carneiro (Oct 07 2018 at 01:55):

yes, that should work

#### 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?

#### 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.

#### 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.

#### 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.

#### Simon Hudon (Oct 07 2018 at 04:11):

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

#### 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.

#### Simon Hudon (Oct 07 2018 at 04:18):

you can do subst h

#### 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


#### Simon Hudon (Oct 07 2018 at 04:22):

What if you do dsimp at h first?

#### Bryan Gin-ge Chen (Oct 07 2018 at 04:22):

Ah, perfect! Thanks so much!

:+1:

#### 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.

#### 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

#### 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

#### Simon Hudon (Oct 07 2018 at 06:44):

What's the span of a relation?

#### 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.

#### Mario Carneiro (Oct 07 2018 at 06:59):

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

#### 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

#### 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.

#### 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

#### 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.

#### 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

#### Simon Hudon (Oct 07 2018 at 07:20):

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

#### Mario Carneiro (Oct 07 2018 at 07:23):

in this case it's lattice theory

#### Mario Carneiro (Oct 07 2018 at 07:24):

but I guess posets are categories, so sure

#### 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?

#### 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

#### Simon Hudon (Oct 07 2018 at 07:46):

Does that make sense?

#### 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.

#### Mario Carneiro (Oct 07 2018 at 08:20):

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

#### 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

(deleted)

#### Mario Carneiro (Oct 07 2018 at 08:24):

that is the union

#### Mario Carneiro (Oct 07 2018 at 08:24):

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

#### Mario Carneiro (Oct 07 2018 at 08:25):

similarly for arbitrary union

#### 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 [...]

no

#### Mario Carneiro (Oct 07 2018 at 08:25):

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

Ah, OK.

#### 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

#### Kenny Lau (Oct 07 2018 at 08:28):

are there any sorry that I can fill?

#### 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.

#### Kenny Lau (Oct 07 2018 at 08:34):

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

#### 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.

#### Kenny Lau (Oct 07 2018 at 08:37):

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

#### Kenny Lau (Oct 07 2018 at 08:37):

so I don't really know what I can do

#### Kenny Lau (Oct 07 2018 at 08:37):

how do other people work on this branch?

#### Kenny Lau (Oct 07 2018 at 08:38):

how does @Simon Hudon work on this branch?

#### 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.

#### 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.

#### Kenny Lau (Oct 07 2018 at 08:43):

can't you see how many threads you have?

2018-10-07.png

#### 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.

#### Kenny Lau (Oct 07 2018 at 08:49):

I have 2 cores and 4 threads

#### Kenny Lau (Oct 07 2018 at 08:49):

I'm on a windows surface

#### 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.

#### 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.

#### 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

#### Mario Carneiro (Oct 07 2018 at 09:11):

Yes, an ultrabook is not intended for heavy workstation programming

#### 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.

#### 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?

#### 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?

#### Kevin Buzzard (Oct 07 2018 at 20:57):

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

#### Kenny Lau (Oct 07 2018 at 20:59):

you mean rec_on

#### 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.

#### 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.

#### Kevin Buzzard (Oct 07 2018 at 21:02):

Kenny you're right

#### 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 "?

#### 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

#### Kevin Buzzard (Oct 07 2018 at 21:04):

and then the union thing is a triviality

#### Kevin Buzzard (Oct 07 2018 at 21:05):

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

#### Kevin Buzzard (Oct 07 2018 at 21:05):

so this should be hopefully straightforward.

#### 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 ?

#### 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


#### 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!

#### 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)


#### Kevin Buzzard (Oct 07 2018 at 21:31):

Oh it's because I should be using a typeclass

#### Kenny Lau (Oct 07 2018 at 21:31):

what do you mean by terrible?

oh

#### 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

#### Kenny Lau (Oct 07 2018 at 21:32):

well it's a lemma

#### Kenny Lau (Oct 07 2018 at 21:32):

the typeclass is local

#### 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)


#### 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

#### Kenny Lau (Oct 07 2018 at 21:34):

inb4 galois insertion

rofl

#### Kevin Buzzard (Oct 07 2018 at 21:35):

I can quite believe it.

#### Bryan Gin-ge Chen (Oct 07 2018 at 21:35):

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

#### Kevin Buzzard (Oct 07 2018 at 21:35):

although it might be a coinsertion

#### 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.

#### 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

#### Kenny Lau (Oct 07 2018 at 21:38):

I don't really understand

#### 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.

#### 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)

yes

#### Kevin Buzzard (Oct 07 2018 at 21:39):

Bryan is using subset notation in exactly this way

#### Kenny Lau (Oct 07 2018 at 21:39):

but he's not proving things this way

#### 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.

#### 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.

#### Kenny Lau (Oct 07 2018 at 21:41):

blow his code out of the water?

#### Kevin Buzzard (Oct 07 2018 at 21:41):

Bryan, do you know what a Galois insertion is?

#### 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.

#### 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

#### 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

#### Kevin Buzzard (Oct 07 2018 at 21:43):

Prove all the lemmas there but in a much better way

#### Kevin Buzzard (Oct 07 2018 at 21:43):

That's the question

I think

#### 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.

#### Kenny Lau (Oct 07 2018 at 21:44):

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

#### Kenny Lau (Oct 07 2018 at 21:44):

I've changed some of the files

#### Kevin Buzzard (Oct 07 2018 at 21:44):

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

#### Kenny Lau (Oct 07 2018 at 21:45):

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

#### 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.

#### Kenny Lau (Oct 07 2018 at 21:45):

and in this hour my CPU will be fully used

#### Kenny Lau (Oct 07 2018 at 21:45):

and the computer will be mostly unusable

#### Kevin Buzzard (Oct 07 2018 at 21:45):

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

#### Kevin Buzzard (Oct 07 2018 at 21:45):

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

#### Kevin Buzzard (Oct 07 2018 at 21:45):

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

#### Patrick Massot (Oct 07 2018 at 21:46):

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

#### Kevin Buzzard (Oct 07 2018 at 21:47):

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

#### Kevin Buzzard (Oct 07 2018 at 21:47):

well...hardly ever

#### Kenny Lau (Oct 07 2018 at 21:53):

do all of you have like 30 cores?

#### 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*.

#### Kenny Lau (Oct 07 2018 at 22:23):

galois.*?

#### Bryan Gin-ge Chen (Oct 07 2018 at 22:23):

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

#### 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.

#### 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. :)

#### Kenny Lau (Oct 07 2018 at 22:59):

oh well I proved this

#### 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 α) }


#### Kenny Lau (Oct 07 2018 at 23:00):

and realized that proving it is a complete lattice is impossible

#### Bryan Gin-ge Chen (Oct 07 2018 at 23:01):

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

#### Kenny Lau (Oct 07 2018 at 23:02):

what is the difference?

#### 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.

#### Bryan Gin-ge Chen (Oct 07 2018 at 23:04):

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

#### Kenny Lau (Oct 07 2018 at 23:07):

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

#### Kenny Lau (Oct 07 2018 at 23:14):

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

yes

#### 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?

#### Kenny Lau (Oct 07 2018 at 23:17):

no, that's bounded_lattice

#### Kenny Lau (Oct 07 2018 at 23:17):

I don't think you can prove complete_lattice.

#### 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.

#### Kenny Lau (Oct 07 2018 at 23:22):

I don't think so.

#### 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.

#### Bryan Gin-ge Chen (Oct 07 2018 at 23:26):

@Kenny Lau Why not?

#### 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.

#### Kenny Lau (Oct 07 2018 at 23:27):

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

#### Kenny Lau (Oct 07 2018 at 23:27):

I give you a set S of partitions of A

#### Kenny Lau (Oct 07 2018 at 23:27):

how do you find the supremum of S?

#### Kenny Lau (Oct 07 2018 at 23:28):

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

#### 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?

#### 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

#### 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...

#### Kenny Lau (Oct 07 2018 at 23:32):

you can always make a noncomputable def :)

#### Kenny Lau (Oct 07 2018 at 23:32):

(don't make it an instance!)

#### 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?

#### Bryan Gin-ge Chen (Oct 07 2018 at 23:41):

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

#### Kenny Lau (Oct 07 2018 at 23:41):

none of the parts

#### Mario Carneiro (Oct 08 2018 at 00:22):

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

#### Mario Carneiro (Oct 08 2018 at 00:22):

This means that they take in no data and produce data

#### Kenny Lau (Oct 08 2018 at 00:23):

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

pointlessly so

#### Mario Carneiro (Oct 08 2018 at 00:23):

you can computabilize any definition of that type

aha

thanks

#### Johan Commelin (Oct 09 2018 at 06:53):

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

#### Johan Commelin (Oct 09 2018 at 06:53):

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

#### 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.

#### 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.

#### 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.

#### 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...)

(deleted)

#### 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?

#### 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"

#### 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

#### 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

#### Tobias Grosser (Oct 09 2018 at 07:41):

Is mostly idle today.

#### 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

#### Tobias Grosser (Oct 09 2018 at 07:43):

It's also at 99% idle ATM.

#### Mario Carneiro (Oct 09 2018 at 07:46):

I've never heard of this option

#### 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?

#### Johan Commelin (Oct 09 2018 at 07:57):

Here is what I just pushed for Challenge 1.

#### 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".

#### 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?

#### 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.

#### Mario Carneiro (Oct 09 2018 at 08:12):

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

them what?

the tutorials

I think it is

#### Mario Carneiro (Oct 09 2018 at 08:13):

Especially if it is an interactive walkthrough

#### Johan Commelin (Oct 09 2018 at 08:13):

Because it forces us to make sure they compile

#### 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

#### Mario Carneiro (Oct 09 2018 at 08:15):

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

#### 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.

#### 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

#### 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?

#### Mario Carneiro (Oct 09 2018 at 08:16):

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

#### Johan Commelin (Oct 09 2018 at 08:17):

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

yes?

#### Johan Commelin (Oct 09 2018 at 08:18):

That's homework for us (-;

#### 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. :-)

#### 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.

#### 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

#### Johan Commelin (Oct 09 2018 at 09:39):

What do you mean with "recommended use"?

#### Mario Carneiro (Oct 09 2018 at 09:39):

I mean this is the way third parties use mathlib

#### Mario Carneiro (Oct 09 2018 at 09:40):

you have a project, and this project imports mathlib

#### Mario Carneiro (Oct 09 2018 at 09:40):

this is the format vscode is expecting

#### 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

#### Johan Commelin (Oct 09 2018 at 09:41):

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

#### Mario Carneiro (Oct 09 2018 at 09:41):

contributing to mathlib is another thing altogether

#### Johan Commelin (Oct 09 2018 at 09:42):

So they will end up hacking on the community fork asap

#### Mario Carneiro (Oct 09 2018 at 09:42):

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

#### Mario Carneiro (Oct 09 2018 at 09:42):

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

#### Johan Commelin (Oct 09 2018 at 09:42):

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

#### Scott Morrison (Oct 09 2018 at 09:43):

A scratch project is a good idea.

#### Johan Commelin (Oct 09 2018 at 09:43):

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

#### Mario Carneiro (Oct 09 2018 at 09:43):

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

#### 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.

#### 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

#### Johan Commelin (Oct 09 2018 at 09:43):

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

#### 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!

Why?

#### Johan Commelin (Oct 09 2018 at 09:44):

I thought we wanted to be a massive monolith

#### 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)

#### 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.

#### Johan Commelin (Oct 09 2018 at 09:45):

@Scott Morrison But why not do maths inside mathlib?

#### 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.

#### Mario Carneiro (Oct 09 2018 at 09:45):

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

#### 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. :-)

#### 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.

#### 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.

#### Johan Commelin (Oct 09 2018 at 10:23):

@Sean Leather I think we can have both

#### Sean Leather (Oct 09 2018 at 10:24):

@Johan Commelin Yep, we probably should.

#### 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.

#### 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.

#### 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

#### Johan Commelin (May 28 2019 at 07:10):

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

#### Johan Commelin (May 28 2019 at 07:14):

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

#### Johan Commelin (May 28 2019 at 07:16):

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

#### 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!

#### Sebastien Gouezel (May 28 2019 at 07:26):

s/le_antisym/le_antisymm on L104

#### Johan Commelin (May 28 2019 at 07:28):

s/coutable/countable/ on L396

#### Mario Carneiro (May 28 2019 at 07:31):

s/infimums/infima/

#### 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".

#### Adrian Chu (May 28 2019 at 11:06):

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

#### 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

#### 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"

#### Sebastien Gouezel (May 28 2019 at 15:38):

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

#### Mario Carneiro (May 28 2019 at 15:43):

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

#### Mario Carneiro (May 28 2019 at 15:43):

although I don't think the hyphens are common

#### Kevin Buzzard (May 28 2019 at 18:07):

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

#### Kenny Lau (May 28 2019 at 18:09):

it's actually a three-line proof

#### Kenny Lau (May 28 2019 at 18:11):

or "a proof that is three lines long"

#### Johan Commelin (May 28 2019 at 19:31):

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

#### 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:

*allows

#### Johan Commelin (May 28 2019 at 19:46):

Sorry, typo. I meant "languages"

Last updated: May 17 2021 at 21:12 UTC