Style

Stream: general

[Patrick Massot]

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]

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

[Simon Hudon]

Good idea! How do we pick a winner?

[Kevin Buzzard]

In the best games, everybody wins.

[Kevin Buzzard]

"Everybody has won and all must have prizes."

[Sebastien Gouezel]

What is the recommended spacing in mathlib?

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

or

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

or

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

[Kenny Lau]

second

[Sebastien Gouezel]

Thanks.

[Sebastien Gouezel]

Another one:

⟨begin
  ...
end⟩

or

⟨begin
  ...
end ⟩

or

⟨ begin
  ...
end ⟩

[Johan Commelin]

Here I prefer the first one.

[Kenny Lau]

The first one

[Johannes Hölzl]

I would say

⟨ begin
    ...
  end ⟩

[Sebastien Gouezel]

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]

you an also write

begin
  constructor,
  ...
end

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

[Mario Carneiro]

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]

Are the following acceptable styles?

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

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[snowbunting]

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]

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

[Jan-David Salchow]

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]

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]

Introducing new constants shouldn't be the solution though

[Jan-David Salchow]

Can we alias stuff?

[Mario Carneiro]

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

[Jan-David Salchow]

Is it documented somewhere?

[Mario Carneiro]

There are probably less than 10 restated theorems in mathlib

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Jan-David Salchow]

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]

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

[Jan-David Salchow]

So an alias might really do the trick ...

[Mario Carneiro]

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

[Mario Carneiro]

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]

How about the Cauchy Schwarz inequality?

[Mario Carneiro]

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

[Jan-David Salchow]

Is there a reason not to define an alias?

[Mario Carneiro]

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]

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]

I see your point for finding statements

[Jan-David Salchow]

But in a proof I'd prefer an informative name

[Mario Carneiro]

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

[snowbunting]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

so le_zero isn't an example

[snowbunting]

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]

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

[Mario Carneiro]

import tactic.alias

section end

alias add_comm ← plus_comm

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

because it's uniformly called bot in the library

[snowbunting]

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]

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]

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

[snowbunting]

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]

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]

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

[Mario Carneiro]

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