Tutorial

Stream: general

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

Ok, I'll do that

[Bryan Gin-ge Chen]

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]

Sure! Please contribute!

[Johan Commelin]

@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]

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

[Sean Leather]

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]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Johan Commelin]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Patrick Massot]

I'll create the branch if you want

[Bryan Gin-ge Chen]

Sure, that'd be great.

[Patrick Massot]

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

[Patrick Massot]

wait

[Patrick Massot]

I messed up

[Patrick Massot]

now it's ok

[Patrick Massot]

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

[Bryan Gin-ge Chen]

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

[Johan Commelin]

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

[Bryan Gin-ge Chen]

Oh, I guess not.

[Johan Commelin]

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

[Simon Hudon]

Done

[Simon Hudon]

And now, I'm off. Good day!

[Johan Commelin]

Sleep tight!

[Simon Hudon]

Thanks :) :zzz:

[Bryan Gin-ge Chen]

Thanks Simon!

[Bryan Gin-ge Chen]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Simon Hudon]

@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]

transfer, that's it.

[Kevin Buzzard]

Thanks Simon.

[Simon Hudon]

:+1:

[Simon Hudon]

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

[Simon Hudon]

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

[Kevin Buzzard]

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]

Look at trunc.induction_on

[Kevin Buzzard]

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

[Simon Hudon]

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

@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]

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

[Kevin Buzzard]

I contributed to some mathoverflow chat about this once

[Kevin Buzzard]

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

[Simon Hudon]

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

I'll look into it

[Kevin Buzzard]

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]

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

[Bryan Gin-ge Chen]

@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]

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]

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]

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

[Kevin Buzzard]

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

[Simon Hudon]

@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]

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]

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

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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]

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

[Simon Hudon]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

@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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

@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]

@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]

@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]

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

I think there's something missing here.

[Kevin Buzzard]

It's rw for data somehow

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Simon Hudon]

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]

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]

Maybe that's what you're looking for?

[Kevin Buzzard]

I'm looking for magic

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Is that magic Simon?

[Kevin Buzzard]

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

[Simon Hudon]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

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

[Scott Morrison]

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

Wow I had not seen that. Thanks.

[Bryan Gin-ge Chen]

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]

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

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

[Simon Hudon]

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

[Simon Hudon]

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]

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

[Simon Hudon]

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]

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]

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

@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]

Sorry about that. You can revert them for now.

[Simon Hudon]

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

[Simon Hudon]

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]

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

[Simon Hudon]

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

[Bryan Gin-ge Chen]

Exactly.

[Bryan Gin-ge Chen]

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]

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]

@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]

@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]

@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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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

[Mario Carneiro]

you should use sets instead

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

@Simon Hudon Do you know this?

[Mario Carneiro]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

@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]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

@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]

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

[Bryan Gin-ge Chen]

@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]

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

[Mario Carneiro]

You can also write this as the range of a function

[Mario Carneiro]

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]

(empty_not_mem_blocks : blocks)

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

but that doesn't fit in this definition of partition

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

yes, that should work

[Bryan Gin-ge Chen]

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]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Bryan Gin-ge Chen]

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]

you can do subst h

[Bryan Gin-ge Chen]

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]

What if you do dsimp at h first?

[Bryan Gin-ge Chen]

Ah, perfect! Thanks so much!

[Simon Hudon]

:+1:

[Bryan Gin-ge Chen]

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]

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]

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]

What's the span of a relation?

[Bryan Gin-ge Chen]

@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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

in this case it's lattice theory

[Mario Carneiro]

but I guess posets are categories, so sure

[Bryan Gin-ge Chen]

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]

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]

Does that make sense?

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Patrick Massot]

(deleted)

[Simon Hudon]

But what about the union?

[Mario Carneiro]

that is the union

[Mario Carneiro]

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

[Mario Carneiro]

similarly for arbitrary union

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

no

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

Ah, OK.

[Mario Carneiro]

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

[Kenny Lau]

are there any sorry that I can fill?

[Bryan Gin-ge Chen]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Kenny Lau]

so I don't really know what I can do

[Kenny Lau]

how do other people work on this branch?

[Kenny Lau]

how does @Simon Hudon work on this branch?

[Bryan Gin-ge Chen]

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

[Kenny Lau]

do you have 24 threads?

[Bryan Gin-ge Chen]

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]

can't you see how many threads you have?

[Kenny Lau]

2018-10-07.png

[Bryan Gin-ge Chen]

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]

I have 2 cores and 4 threads

[Kenny Lau]

I'm on a windows surface

[Bryan Gin-ge Chen]

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]

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]

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

I guess it isn't designed to build lean

[Mario Carneiro]

Yes, an ultrabook is not intended for heavy workstation programming

[Bryan Gin-ge Chen]

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]

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]

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]

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

[Kenny Lau]

you mean rec_on

[Kevin Buzzard]

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]

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]

Kenny you're right

[Kevin Buzzard]

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]

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]

and then the union thing is a triviality

[Kevin Buzzard]

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

[Kevin Buzzard]

so this should be hopefully straightforward.

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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]

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]

@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]

Oh it's because I should be using a typeclass

[Kenny Lau]

what do you mean by terrible?

[Kenny Lau]

oh

[Kevin Buzzard]

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

[Kenny Lau]

well it's a lemma

[Kenny Lau]

the typeclass is local

[Kenny Lau]

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]

@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]

inb4 galois insertion

[Kevin Buzzard]

rofl

[Kevin Buzzard]

I can quite believe it.

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

although it might be a coinsertion

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

I don't really understand

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

yes

[Kevin Buzzard]

Bryan is using subset notation in exactly this way

[Kenny Lau]

but he's not proving things this way

[Bryan Gin-ge Chen]

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]

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]

blow his code out of the water?

[Kevin Buzzard]

Bryan, do you know what a Galois insertion is?

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

Prove all the lemmas there but in a much better way

[Kevin Buzzard]

That's the question

[Kevin Buzzard]

I think

[Kevin Buzzard]

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]

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

[Kenny Lau]

I've changed some of the files

[Kevin Buzzard]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

and in this hour my CPU will be fully used

[Kenny Lau]

and the computer will be mostly unusable

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

well...hardly ever

[Kenny Lau]

do all of you have like 30 cores?

[Bryan Gin-ge Chen]

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]

galois.*?

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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]

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]

oh well I proved this

[Kenny Lau]

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]

and realized that proving it is a complete lattice is impossible

[Bryan Gin-ge Chen]

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

[Kenny Lau]

what is the difference?

[Bryan Gin-ge Chen]

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]

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

[Kenny Lau]

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

[Kenny Lau]

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

yes

[Bryan Gin-ge Chen]

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

[Kenny Lau]

no, that's bounded_lattice

[Kenny Lau]

I don't think you can prove complete_lattice.

[Bryan Gin-ge Chen]

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]

I don't think so.

[Jeremy Avigad]

@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]

@Kenny Lau Why not?

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

I give you a set S of partitions of A

[Kenny Lau]

how do you find the supremum of S?

[Kenny Lau]

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

[Bryan Gin-ge Chen]

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

[Kenny Lau]

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

[Bryan Gin-ge Chen]

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]

you can always make a noncomputable def :)

[Kenny Lau]

(don't make it an instance!)

[Bryan Gin-ge Chen]

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]

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

[Kenny Lau]

none of the parts

[Mario Carneiro]

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

[Mario Carneiro]

This means that they take in no data and produce data

[Kenny Lau]

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

[Mario Carneiro]

pointlessly so

[Mario Carneiro]

you can computabilize any definition of that type

[Kenny Lau]

aha

[Kenny Lau]

thanks

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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]

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

[Tobias Grosser]

(deleted)

[Tobias Grosser]

do all of you have like 30 cores?

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

[Tobias Grosser]

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

[Tobias Grosser]

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

[Tobias Grosser]

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]

Is mostly idle today.

[Tobias Grosser]

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

[Tobias Grosser]

It's also at 99% idle ATM.

[Mario Carneiro]

I've never heard of this option

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

@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]

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]

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

[Johan Commelin]

them what?

[Mario Carneiro]

the tutorials

[Johan Commelin]

I think it is

[Mario Carneiro]

Especially if it is an interactive walkthrough

[Johan Commelin]

Because it forces us to make sure they compile

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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]

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]

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

what do you mean?

[Mario Carneiro]

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

[Johan Commelin]

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

[Kenny Lau]

yes?

[Johan Commelin]

That's homework for us (-;

[Scott Morrison]

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

[Sean Leather]

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]

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]

What do you mean with "recommended use"?

[Mario Carneiro]

I mean this is the way third parties use mathlib

[Mario Carneiro]

you have a project, and this project imports mathlib

[Mario Carneiro]

this is the format vscode is expecting

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

contributing to mathlib is another thing altogether

[Johan Commelin]

So they will end up hacking on the community fork asap

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Scott Morrison]

A scratch project is a good idea.

[Johan Commelin]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Mario Carneiro]

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]

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

[Scott Morrison]

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

[Johan Commelin]

Why?

[Johan Commelin]

I thought we wanted to be a massive monolith

[Scott Morrison]

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

[Sean Leather]

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]

@Scott Morrison But why not do maths inside mathlib?

[Scott Morrison]

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]

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

[Scott Morrison]

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]

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]

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]

@Sean Leather I think we can have both

[Sean Leather]

@Johan Commelin Yep, we probably should.

[Kevin Buzzard]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Sebastien Gouezel]

s/le_antisym/le_antisymm on L104

[Johan Commelin]

s/coutable/countable/ on L396

[Mario Carneiro]

s/infimums/infima/

[Sebastien Gouezel]

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]

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

[Patrick Massot]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

although I don't think the hyphens are common

[Kevin Buzzard]

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

[Kenny Lau]

it's actually a three-line proof

[Kenny Lau]

or "a proof that is three lines long"

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

*allows

[Johan Commelin]

Sorry, typo. I meant "languages"