## Stream: general

### Topic: Style

#### Patrick Massot (Apr 08 2018 at 20:51):

Let's play a new game: each time someone opens a PR and is asked for style corrections, we check whether https://github.com/leanprover/mathlib/blob/master/docs/style.md and https://github.com/leanprover/mathlib/blob/master/docs/naming.md already have them. If not we open something like https://github.com/leanprover/mathlib/pull/95

#### Patrick Massot (Apr 08 2018 at 20:54):

Everybody can play, and make contributing to, and maintaining, mathlib slightly easier

#### Simon Hudon (Apr 08 2018 at 21:57):

Good idea! How do we pick a winner?

#### Kevin Buzzard (Apr 08 2018 at 22:38):

In the best games, everybody wins.

#### Kevin Buzzard (Apr 08 2018 at 22:39):

"Everybody has won and all must have prizes."

#### Sebastien Gouezel (Mar 29 2019 at 13:35):

What is the recommended spacing in mathlib?

  { ...
split,
{ ... },
{ ... }}


or

  { ...
split,
{ ... },
{ ... } }


or

  { ...
split,
{ ... },
{ ... }
}


second

Thanks.

#### Sebastien Gouezel (Mar 29 2019 at 13:41):

Another one:

⟨begin
...
end⟩


or

⟨begin
...
end ⟩


or

⟨ begin
...
end ⟩


#### Johan Commelin (Mar 29 2019 at 13:42):

Here I prefer the first one.

The first one

#### Johannes Hölzl (Mar 29 2019 at 16:29):

I would say

⟨ begin
...
end ⟩


#### Sebastien Gouezel (Mar 29 2019 at 17:57):

Ah. I would say your suggestion is more readable, but it has the drawback of shifting the proof by 4 characters to the right (instead of two characters for the more condensed version).

#### Johannes Hölzl (Mar 29 2019 at 18:07):

you an also write

begin
constructor,
...
end


In many cases a refine inside of the tactic block might be necessary anyway.

#### Mario Carneiro (Mar 29 2019 at 18:14):

If there is only one case I would prefer option 1. If it's multiple cases I would use

begin
refine <bla _ _, foo _ _>,
{ ... },
{ ... }
end


#### Floris van Doorn (Mar 29 2019 at 18:52):

Are the following acceptable styles?

begin
have h : ...,
{ ... },
...
end

begin
split,
{ ... },
...
end


#### Mario Carneiro (Mar 29 2019 at 18:53):

I prefer to bracket both cases in the second example, but the first one is common

#### Mario Carneiro (Mar 29 2019 at 18:54):

If one subgoal is much shorter than the other, then you should arrange it so that the short goal comes first and then you can skip the second brackets

#### Patrick Massot (Mar 29 2019 at 19:02):

Who wants to update the style guide to record all that?

#### snowbunting (Mar 31 2019 at 08:28):

What are the thoughts in the Lean community about multiple synonym/names for a certain theorem? Are there any strategies on how to do that or do people have concerns against doing that?

For example, I was looking for something like "submodule.le_zero" and I wouldn't want to have to dig into lattices and their \bot element, just to get that.

namespace submodule
universes u v
variables {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M]
lemma le_zero (N: submodule R M): (0: submodule R M) ≤ N :=
lattice.bot_le
end namespace


Same goes with theorems that have very common names - again from my first "exercise" - e.g. I would want to find Nakayama's lemma preferable formulated in about 5 equivalent ways as something like nakayama, nakayama_rephrased_1, nakayama_rephrased_2 or something along those lines, certainly not exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul.

#### Mario Carneiro (Mar 31 2019 at 08:46):

The le_zero example is not recommended because that's not how we write the zero submodule

#### Jan-David Salchow (Mar 31 2019 at 08:46):

I also have the feeling that the mathlib conventions deserve some updating on this issue. This is not only about finding statements, but also about readability of proofs.

#### Mario Carneiro (Mar 31 2019 at 08:47):

It is important to stick to a single expression consistently because that's the common language for all the simp lemmas and such

#### Jan-David Salchow (Mar 31 2019 at 08:47):

Introducing new constants shouldn't be the solution though

#### Jan-David Salchow (Mar 31 2019 at 08:47):

Can we alias stuff?

#### Mario Carneiro (Mar 31 2019 at 08:47):

There is an alias command for exactly that, but it is not much used

#### Jan-David Salchow (Mar 31 2019 at 08:48):

Is it documented somewhere?

#### Mario Carneiro (Mar 31 2019 at 08:48):

There are probably less than 10 restated theorems in mathlib

#### Mario Carneiro (Mar 31 2019 at 08:48):

and they are mostly because I thought that core had a dumb name for something

#### Mario Carneiro (Mar 31 2019 at 08:49):

I agree that famous theorems should use famous names, especially if the symbol reading name is unenlightening or very long

#### Mario Carneiro (Mar 31 2019 at 08:50):

The convention for restatements would be to use postfix ' or \1, \2 etc

#### Jan-David Salchow (Mar 31 2019 at 08:50):

There are also boundary cases, e.g. Johannes asked me to rename homogeneous to norm_smul in https://github.com/leanprover-community/mathlib/pull/680#discussion_r253305420

#### Jan-David Salchow (Mar 31 2019 at 08:50):

I'm not claiming that homogeneous is the best name ever, but it would be nicer in some proofs

#### Jan-David Salchow (Mar 31 2019 at 08:51):

So an alias might really do the trick ...

#### Mario Carneiro (Mar 31 2019 at 08:51):

If it is some kind of f(g x) = g (f x) statement I would definitely prefer the symbol reading name

#### Mario Carneiro (Mar 31 2019 at 08:52):

If it is \ex x, foo x /\ \all y, bar x <= f x + g y then I would prefer a more informative name

#### Jan-David Salchow (Mar 31 2019 at 08:54):

How about the Cauchy Schwarz inequality?

#### Mario Carneiro (Mar 31 2019 at 08:55):

I could see a case for either, but I'd err on the side of symbol reading name

#### Jan-David Salchow (Mar 31 2019 at 08:55):

Is there a reason not to define an alias?

#### Mario Carneiro (Mar 31 2019 at 08:55):

the problem is that these theorems often have a few forms, and if they are algebraic manipulation lemmas then it's easier to get at them by the symbol reading name

#### Mario Carneiro (Mar 31 2019 at 08:57):

The alias command still leaves some to be desired. I would like it if it was possible to have forwarding links, i.e. you type in cauchy_s... in autocomplete and norm_mul_le pops up (with an indication that it is redirecting from cauchy_schwarz)

#### Jan-David Salchow (Mar 31 2019 at 08:58):

I see your point for finding statements

#### Jan-David Salchow (Mar 31 2019 at 08:58):

But in a proof I'd prefer an informative name

#### Mario Carneiro (Mar 31 2019 at 08:59):

I suppose you could also do it the other way around, seeing as the main reason for the symbol reading names is searchability

#### snowbunting (Mar 31 2019 at 09:00):

So how would that alias work? I see

/ -- doc string - /
alias my_theorem ← alias1 alias2 ...


or

alias A_iff_B ↔ B_of_A A_of_B


in the comments, but alias submodule.le_zero ← lattice.bot_le does not work.

What is the bad thing of doing

lemma le_zerro: ... :=
lattice.bot_le


#### Mario Carneiro (Mar 31 2019 at 09:00):

you have to import the tactic, I don't think it's in the default set

#### Mario Carneiro (Mar 31 2019 at 09:01):

The tactic does basically the same thing as that, except it also gives it a nice docstring and attributes and stuff

#### Mario Carneiro (Mar 31 2019 at 09:02):

alias is a good way to document your intent about it too (otherwise people might just remove it to eliminate duplication)

#### Mario Carneiro (Mar 31 2019 at 09:02):

Of course, alias is only for exact duplicates. If you want to change the statement it's not an alias

#### Mario Carneiro (Mar 31 2019 at 09:03):

so le_zero isn't an example

#### snowbunting (Mar 31 2019 at 09:06):

would you mind pointing me to a minimal working example? Also didn't see any documentation about docstrings yet, is there any tutorial/document where to read that stuff?

Yes it is not, but since I could replace my submodule.le_zero in the proof with lattice.bot_le, it would be functionally an alias, wouldn't it? (I mean I only did write the lemma because I needed this fact in the proof and couldn't find it)

#### Mario Carneiro (Mar 31 2019 at 09:09):

Just try it and see, it's not a particularly complicated tactic

#### Mario Carneiro (Mar 31 2019 at 09:11):

import tactic.alias

section end

#print plus_comm -- mouse over this, the docstring is "**Alias** of add_comm"
-- @[alias]
-- theorem plus_comm : ∀ {α : Type u} [_inst_1 : add_comm_semigroup α] (a b : α), a + b = b + a :=


#### Mario Carneiro (Mar 31 2019 at 09:12):

By the way, that theorem would be called zero_le not le_zero anyway

#### Mario Carneiro (Mar 31 2019 at 09:13):

and that already exists and might even apply if you can prove submodules have the right structure

#### Mario Carneiro (Mar 31 2019 at 09:14):

but like I said, I strongly recommend against adding that theorem, because it will make you want to use 0 for the zero submodule, and you will be frustrated six more times for lack of other theorems talking about this submodule

#### Mario Carneiro (Mar 31 2019 at 09:14):

because it's uniformly called bot in the library

#### snowbunting (Mar 31 2019 at 09:41):

thank you!

I'm not going to make any pull request to the library, I am merely trying to figure out how things work, so the example here is rather a theoretical one. But I think it is good to know the options available for giving nicer, shorter notations to things, as this seems to be im my opinion quite important for the usability.

I agree with you that I should use \bot to match the library style, and also that I messed up the name there (I had first "ge_zero", then I changed the sign later).

#### Scott Morrison (Mar 31 2019 at 09:43):

Naming things is hard. It took me a long time to get over the fact that mathlib people were telling me the property that functors have is called map_comp, rather than functoriality.

#### Scott Morrison (Mar 31 2019 at 09:43):

I have grudgingly accepted their point, I think. :-)

#### snowbunting (Mar 31 2019 at 09:46):

absolutely, and it makes sense for searching when you can type something like eq_of... and it gives you all the options, so I generally like the naming style.

#### Mario Carneiro (Mar 31 2019 at 09:48):

By the way, I've tried this kind of naming in the past. In the long term, you get confused by your own naming system, because it is difficult to name everything consistently this way and you have to look a lot more up

#### Mario Carneiro (Mar 31 2019 at 09:48):

you end up with ad hoc extensions to the naming system all over the place and it becomes a mess

#### Mario Carneiro (Mar 31 2019 at 09:50):

there just isn't enough creativity in the mathematical lexicon to name all the thousands of piddly lemmas that demand names

Last updated: May 11 2021 at 13:22 UTC