Zulip Chat Archive

Stream: general

Topic: Style


view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 08 2018 at 20:54):

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

view this post on Zulip Simon Hudon (Apr 08 2018 at 21:57):

Good idea! How do we pick a winner?

view this post on Zulip Kevin Buzzard (Apr 08 2018 at 22:38):

In the best games, everybody wins.

view this post on Zulip Kevin Buzzard (Apr 08 2018 at 22:39):

"Everybody has won and all must have prizes."

view this post on Zulip Sebastien Gouezel (Mar 29 2019 at 13:35):

What is the recommended spacing in mathlib?

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

or

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

or

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

view this post on Zulip Kenny Lau (Mar 29 2019 at 13:36):

second

view this post on Zulip Sebastien Gouezel (Mar 29 2019 at 13:39):

Thanks.

view this post on Zulip Sebastien Gouezel (Mar 29 2019 at 13:41):

Another one:

begin
  ...
end

or

begin
  ...
end 

or

 begin
  ...
end 

view this post on Zulip Johan Commelin (Mar 29 2019 at 13:42):

Here I prefer the first one.

view this post on Zulip Kenny Lau (Mar 29 2019 at 13:55):

The first one

view this post on Zulip Johannes Hölzl (Mar 29 2019 at 16:29):

I would say

 begin
    ...
  end 

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Floris van Doorn (Mar 29 2019 at 18:52):

Are the following acceptable styles?

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

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

view this post on Zulip Mario Carneiro (Mar 29 2019 at 18:53):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 29 2019 at 19:02):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Jan-David Salchow (Mar 31 2019 at 08:47):

Introducing new constants shouldn't be the solution though

view this post on Zulip Jan-David Salchow (Mar 31 2019 at 08:47):

Can we alias stuff?

view this post on Zulip Mario Carneiro (Mar 31 2019 at 08:47):

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

view this post on Zulip Jan-David Salchow (Mar 31 2019 at 08:48):

Is it documented somewhere?

view this post on Zulip Mario Carneiro (Mar 31 2019 at 08:48):

There are probably less than 10 restated theorems in mathlib

view this post on Zulip Mario Carneiro (Mar 31 2019 at 08:48):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 08:50):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jan-David Salchow (Mar 31 2019 at 08:51):

So an alias might really do the trick ...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jan-David Salchow (Mar 31 2019 at 08:54):

How about the Cauchy Schwarz inequality?

view this post on Zulip 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

view this post on Zulip Jan-David Salchow (Mar 31 2019 at 08:55):

Is there a reason not to define an alias?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Jan-David Salchow (Mar 31 2019 at 08:58):

I see your point for finding statements

view this post on Zulip Jan-David Salchow (Mar 31 2019 at 08:58):

But in a proof I'd prefer an informative name

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 09:00):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 09:03):

so le_zero isn't an example

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Mar 31 2019 at 09:09):

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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 09:11):

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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 09:12):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 31 2019 at 09:14):

because it's uniformly called bot in the library

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 31 2019 at 09:43):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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