## Stream: general

### Topic: new Lean / mathlib tutorial

#### Jeremy Avigad (May 08 2020 at 14:00):

Kevin Buzzard, Rob Lewis, Patrick Massot, and I have started working on a new tutorial introduction to Lean and mathlib, with help from Gabriel Ebner. It is here: https://github.com/leanprover-community/mathematics_in_lean. The tutorial is meant to supplement other sources, like Kevin's Natural Number game, Patrick's tutorial, and TPIL. There is overlap. The goal is to provide as much useful learning material as possible for people looking to learn how to formalize mathematics and contribute to mathlib.

There is also an online version: https://leanprover-community.github.io/mathematics_in_lean/, but we recommend using the VS Code version. We hope to get some new chapters out quickly over the next few weeks.

In VS Code version, the examples and exercises are opened in an examples folder and you can save your work. Caveat: we don't yet have a good way of updating the tutorial without moving your files and resetting the repository or making a fresh copy. And the infrastructure may get additional bells and whistles. But in the meanwhile, the current version provides some fun exercises for people looking for things to do.

Enjoy!

#### Jean-Philippe Burelle (May 08 2020 at 19:35):

Hi, I have started this tutorial and I think it's great so far. I completed the natural numbers game a few days ago, and have no other experience with lean or any theorem proving software.
I think it would probably be good to say a few words in the first page about the VSCode interface. For instance, how to open the Goals window if you closed it by mistake, and perhaps how to split/switch tabs according to how you expect the user to interact with the tutorials.
I also found a typo in the first exercise of 2.2 : The theorem to prove says (a+b) + -b = 0.
Maybe it's good to leave it there though, it teaches readers that theorem provers can be useful to spot mistakes in theorem statements :laughing:

#### Jeremy Avigad (May 09 2020 at 14:33):

Thanks! I just corrected the exercise in the version I am working on, so it will be fixed next time we put new material online, hopefully within the next couple of days.

As to adding more information about VS Code, from my experience writing documentation, it is a bad idea to mix purposes. Information then become fragmented, outdated, etc. I think it makes more sense to have a stand-alone markdown document with information about the VS Code interface and FAQs in the mathlib documentation folder (https://github.com/leanprover-community/mathlib/tree/master/docs). Or maybe such a thing already exists somewhere? I'd be happy to link to it from the text if someone writes it.

#### Jean-Philippe Burelle (May 11 2020 at 15:03):

Another small typo : at the end of 2.2, in the "group theory" block, I suspect the one_mul theorem should be mul_one, since the other one is an axiom.

#### Johan Commelin (May 11 2020 at 15:04):

@Jean-Philippe Burelle one_mul : 1 * a = a, and mul_one : a * 1 = a.

#### Johan Commelin (May 11 2020 at 15:04):

Because for the first it is "one mul something" and for the other, "something mul one"

#### Jean-Philippe Burelle (May 11 2020 at 15:07):

Yes, exactly, that's what I think it should say, but not what it currently says

#### Shing Tak Lam (May 11 2020 at 15:14):

I think what @Jean-Philippe Burelle is saying is that the exercise

theorem one_mul (a : G) : 1 * a = a :=
sorry


should be

theorem mul_one (a : G) :  a * 1 = a :=
sorry


since one_mul is true by definition of a group

#### Johan Commelin (May 11 2020 at 15:22):

@Jean-Philippe Burelle sorry, I'm dense :oops:

#### Jeremy Avigad (May 11 2020 at 15:52):

Thanks! I just fixed in my copy. It will be online within the next day or two. Also, the name of the theorem after that should have been mul_right_inv. We have a tool that checks the snippets to make sure they compile, but we don't have a tool to check the exercises to make sure that they make sense.

#### Kevin Buzzard (May 11 2020 at 16:26):

Yeah we do, it's called Zulip :-)

#### Kevin Buzzard (May 11 2020 at 16:27):

It should be called "the authors" but one of them is far more concerned with marking right now :-/

#### Johan Commelin (May 12 2020 at 11:46):

@Jeremy Avigad and others, on my 12 inch laptop, the documentation opened on the right hand side of the split, and therefore hid the "Lean Goal" window. After clicking "Try it", I had to manually switch to the "Lean Goal" tab.
For people who don't know that the "Lean Goal" tab/window exists, you might want to mention it.

#### Johan Commelin (May 12 2020 at 11:51):

This sentence towards the end of the intro also seems slightly crippled:

But be forewarned: interactive theorem prover will challenge you to think about mathematics and mathematical reasoning in fundamentally new ways.

I guess making that "an interactive theorem prover" would already fix it.

Or "proving"

#### Johan Commelin (May 12 2020 at 12:34):

@Jeremy Avigad Another note. calc in tactic mode is now refine calc, and not exact calc. Just a minor point, but you might want to be aware of it (-;

(deleted)

#### Jeremy Avigad (May 12 2020 at 19:16):

Thanks! We'll mention the tab, and also modify the statement about calc so that it is not outright false.

#### Jean-Philippe Burelle (May 13 2020 at 13:44):

In section 2.5 : The second "absorption" exercise has a typo (sup instead of inf).

I also have a very basic question, which perhaps should go in "new members", but since I'm working through the tutorial I thought the context would be clearer if I ask here. I was working on the distributivity exercises, and my goal was in the following state : a ⊓ c ⊔ c ⊓ b = a ⊓ c ⊔ b ⊓ c .
I want to rw inf_comm on the pair c ⊓ b, but the proposition inf_comm uses the curly braces "implicit variables" so I get an error if I write rw inf_comm c b. I can get around this by adding an intermediate goal "have c ⊓ b = b ⊓ c" but this can't be the right way to do it... How do I specify where to substitute when a proposition has variables in curly braces ? I didn't have this problem with add_comm.

#### Patrick Massot (May 13 2020 at 13:46):

https://leanprover.github.io/reference/expressions.html#implicit-arguments

#### Johan Commelin (May 13 2020 at 13:46):

@Jean-Philippe Burelle I think typo is already fixed. (But maybe not yet live)

#### Patrick Massot (May 13 2020 at 13:47):

So you can use rw @inf_comm _ _ c b,

#### Patrick Massot (May 13 2020 at 13:48):

This is a general answer, but not what is expected here

#### Patrick Massot (May 13 2020 at 13:48):

Another general trick is to use

  congr' 1,
rw inf_comm ,


#### Patrick Massot (May 13 2020 at 13:49):

But again this is probably not what Jeremy had in mind at this stage

#### Patrick Massot (May 13 2020 at 13:51):

Ok, I've reread the context, and I can do the exercises using only the surrounding lemmas

#### Patrick Massot (May 13 2020 at 13:51):

So no need for my general tricks

#### Patrick Massot (May 13 2020 at 13:52):

But it's a bit unfortunate that the obvious proof hits this implicit argument issue

#### Jean-Philippe Burelle (May 13 2020 at 13:56):

Yes, especially since it seems inconsistent with the way the previous section on rings worked (where this issue didn't arise) and the text states things like : "mul_comm a matches any pattern of the form a * ? and rewrites it to ? * a"

#### Patrick Massot (May 13 2020 at 14:03):

I think the good answer is that inf_comm should have explicit arguments. Feel free to open your first mathlib PR! (Maybe first check that @Mario Carneiro wouldn't complain)

#### Bryan Gin-ge Chen (May 13 2020 at 14:09):

Indeed, it looks like a lot of identities in order.lattice should have explicit arguments.

#### Jean-Philippe Burelle (May 13 2020 at 14:10):

What is the general philosophy for having implicit vs explicit arguments ?

#### Bryan Gin-ge Chen (May 13 2020 at 14:12):

The rule I've always followed is that an argument should be implicit iff it can be inferred from later explicit arguments.

#### Bryan Gin-ge Chen (May 13 2020 at 14:13):

For instance, if you have a lemma that depends on a : nat and ha : a > 0, then a can be implicit, since Lean will be able to infer it when you provide ha.

#### Bryan Gin-ge Chen (May 13 2020 at 14:16):

I'm trying to remember where I learned this and I guess it must be from the discussion in 4.1 of TPiL.

#### Patrick Massot (May 13 2020 at 14:19):

We also tend to use implicit arguments for iff statements when an object appears on both sides.

#### Mario Carneiro (May 13 2020 at 16:23):

@Patrick Massot I'm okay with this change. There are a number of definitions in lattices and topology written by Johannes in 2017 that use too many implicits. I'm not sure if it is a difference of style or if it is simply because of the variables {a b : A} at the top of the file causing this to be the default.

#### Jean-Philippe Burelle (May 19 2020 at 14:13):

I finished the exercises now.
A few more issues that I noticed at the end of Chapter 2 :

• The first ordered ring exercise is a ≤ b ↔ 0 ≤ b - a, and I think this is the first time the reader is asked to prove an equivalence. I had to use the "split" and "intro" tactics which I learned from the NNG but were not introduced yet in the book.
• For a few proofs in this section I wanted to replace "a - b" with "a + (-b)" and even though it's mentioned that "refl" works for goals of this type (and that this is the definition of "-"), I don't know which tactic to use to just replace one with the other in a more complicated goal. I managed to avoid having to do it in all cases but it's frustrating to know it's the right thing and not be able to do it.
• The mul_nonneg lemma in ordered_ring.lean is stated in terms of ≥ instead of ≤ for some reason, which does not match the book.

#### Kevin Buzzard (May 19 2020 at 14:21):

Many thanks for this!

#### Reid Barton (May 19 2020 at 14:22):

For your own information, you can achieve the second item using the change or show tactics, which are mostly overlapping in functionality.

#### Bhavik Mehta (May 19 2020 at 14:32):

I find change much easier to use in practice than show - in particular if I've made a type error in my new goal show will just say failed, but change gives me a more useful error message

#### Reid Barton (May 19 2020 at 14:37):

Oh interesting---I only ever use change really. I guess show's goal selection functionality prevents it from giving good error messages.

#### Kevin Buzzard (May 19 2020 at 15:41):

I tell students to use change because it works on hypotheses too

#### Jeremy Avigad (May 19 2020 at 21:25):

Oh! I thought show was syntactic sugar for change. In the early chapters, should I rely exclusively on change, or show readers both?

#### Jeremy Avigad (May 19 2020 at 21:26):

@Jean-Philippe Burelle You can rewrite a - b to a + -b with sub_eq_add_neg.

#### Jeremy Avigad (May 19 2020 at 21:29):

We'll fix the ring exercise. We are thinking of renaming the first chapter "Equality and Order" or something like that (because "basic skills" is so vague). Any thoughts there?

#### Bhavik Mehta (May 19 2020 at 21:29):

I personally don't see the advantage of show - change has the additional advantage of being able to modify subexpressions as well

#### Jeremy Avigad (May 19 2020 at 21:32):

O.k., Iets go with change.

#### Sebastien Gouezel (May 19 2020 at 21:38):

show is useful to treat the goals in any order. If you have a tactic that will spit several goals in an unpredictable order, it is really useful.

#### Jeremy Avigad (May 19 2020 at 21:42):

Yeah, I know. I'll go back and take a look at the text. Maybe we'll introduce them both at once, or maybe we'll start with change and use show later, when it is useful.

#### Bhavik Mehta (May 19 2020 at 21:43):

Sebastien Gouezel said:

show is useful to treat the goals in any order. If you have a tactic that will spit several goals in an unpredictable order, it is really useful.

Good to know, thanks!

#### Mario Carneiro (May 19 2020 at 22:04):

I think you can also use show to change the type to a defeq type like change. It would be nice if when it fails it gives the error for the first goal though, so that you get something more informative like change

#### Bhavik Mehta (May 19 2020 at 22:21):

Yeah, with show (even with one goal) if I give a badly-formed type I think the error message is 'failed' which is the same as if I give a well-formed type which isn't defeq to the goal

#### Kevin Buzzard (May 19 2020 at 22:41):

Yes. If I get failed with show then I usually change it to let foo := ... to see if what I wrote actually made syntactic sense and typechecked

#### Reid Barton (May 20 2020 at 00:46):

You should probably just change it to change instead though?

#### Reid Barton (May 20 2020 at 00:46):

assuming it's the current goal you want to change

#### Aniruddh Agarwal (May 20 2020 at 01:54):

Found a typo in section 2.1:

In response to the command #check mul_comm a b, Lean reports that mul_comm a b is a proof of the fact a + b = b + a.

should be

In response to the command #check mul_comm a b, Lean reports that mul_comm a b is a proof of the fact a * b = b * a.

#### Jeremy Avigad (May 20 2020 at 02:04):

@Jean-Philippe Burelle Thanks very much for the feedback. I left show in Chapter 2 but we mention changein the next chapter. We don't say much about either, but it's hard to decide what it is most important to convey early on, without subjecting the reader to information overload. We'll probably end up cycling back and saying more as they come up in more examples. I also fixed the exercise you mentioned, replacing the "iff" with two implications.

A draft of the next chapter is here: https://avigad.github.io/mathematics_in_lean/. We'll add sections on "not", "or", "and", and "iff" before the "convergent sequences" section, and hopefully have it out within a week or so.

@Aniruddh Agarwal Thanks for the correction! I just fixed it in the draft, so it will hopefully go online soon.

#### Aniruddh Agarwal (May 20 2020 at 04:20):

I'm not sure if this is a typo or not, but in the code block right at the beginning of section 2.2 supposed to begin with:

variables (R : Type*) [ring R]


Right now, it begins with

variables (R : Type*) [comm_ring R]


but the discussion around it is about non-necessarily commutative rings.

#### Jean-Philippe Burelle (May 20 2020 at 14:50):

@Patrick Massot I made a new fork and tried turning all the identities in lattices.lean to explicit variables, but this breaks a lot of things in mathlib. What's the best way when making such a change to track everything that broke in an organized way ?
In particular, after making the change, when trying to open some files (like things in topology/metric spaces) in VSCode I would get "ran out of memory" errors, I assume because so many things couldn't compile. This isn't very helpful to finding where the lemmas that I changed were used.

#### Johan Commelin (May 20 2020 at 14:51):

If you have the energy for this, that would be awesome!

#### Johan Commelin (May 20 2020 at 14:51):

Run leanpkg build in a terminal, and hit Ctrl-C as soon as you see the first error message

#### Johan Commelin (May 20 2020 at 14:51):

See which file it complains about, and open it in VScode.

#### Patrick Massot (May 20 2020 at 14:51):

There is a better way, hold on.

#### Johan Commelin (May 20 2020 at 14:51):

Fix it. Close the project in VScode.

Ooh, ok

#### Johan Commelin (May 20 2020 at 14:52):

/me is curious, about to learn how I should have done my refactors in the past.

#### Jeremy Avigad (May 20 2020 at 16:05):

@Aniruddh Agarwal Indeed, it should be ring. I'll fix it. Thanks!

#### Patrick Massot (May 20 2020 at 16:50):

@Jean-Philippe Burelle sorry for disappearing. I'm ready to answer questions now. Which declarations did you change?

#### Patrick Massot (May 20 2020 at 16:53):

Using leancrawler, you can type things like:

In [28]: [(name, lib[name].filename, lib[name].line_nb) for name in G.successors('inf_comm')]
Out[28]:
[('compl_inf_eq_bot',
'/home/pmassot/lean/mathlib/src/order/boolean_algebra.lean',
33),
('inf_infi',
'/home/pmassot/lean/mathlib/src/order/complete_lattice.lean',
476),
('mem_closure_iff_ultrafilter',
'/home/pmassot/lean/mathlib/src/topology/basic.lean',
533),
('Sup_inf_eq',
'/home/pmassot/lean/mathlib/src/order/complete_boolean_algebra.lean',
43),
('compact.image_of_continuous_on',
'/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
391),
('inf_left_comm', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 265),
('multiset.inter_comm',
'/home/pmassot/lean/mathlib/src/data/multiset.lean',
1290),
('inf_sup_right', '/home/pmassot/lean/mathlib/src/order/lattice.lean', 363),
('inf_is_commutative',
'/home/pmassot/lean/mathlib/src/order/lattice.lean',
252),
'/home/pmassot/lean/mathlib/src/ring_theory/power_series.lean',
1369),
('is_compl.symm',
'/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
861),
('compact_of_finite_subfamily_closed',
'/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
199),
("filter.push_pull'",
'/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
1424),
('disjoint.comm',
'/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
817),
("filter.prod_comm'",
'/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
1836),
('inf_eq_bot_iff_le_compl',
'/home/pmassot/lean/mathlib/src/order/bounded_lattice.lean',
279),
('cauchy_prod',
'/home/pmassot/lean/mathlib/src/topology/uniform_space/cauchy.lean',
202),
('nhds_order_unbounded',
'/home/pmassot/lean/mathlib/src/topology/algebra/ordered.lean',
404),
('filter.inf_ne_bot_iff_frequently_right',
'/home/pmassot/lean/mathlib/src/order/filter/basic.lean',
964),
('compact.inter_right',
'/home/pmassot/lean/mathlib/src/topology/subset_properties.lean',
43)]


#### Jean-Philippe Burelle (May 20 2020 at 17:07):

That seems useful! I changed all identities that had implicit variables to explicit, so le_sup_left, le_sup_right, sup_idem, sup_comm, and all their inf counterparts.

#### Jeremy Avigad (May 29 2020 at 21:17):

The next chapter of the new Lean / mathlib tutorial is now live:
https://leanprover-community.github.io/mathematics_in_lean/

#### Yury G. Kudryashov (May 29 2020 at 21:20):

Where is the source?

no

#### Patrick Massot (May 29 2020 at 21:24):

We use mathematics_in_lean for the repository that users can fetch for the local VS Code version. But we also deploy the online version there, so we have the nicer url.