Zulip Chat Archive

Stream: general

Topic: lemma naming


view this post on Zulip Rob Lewis (Sep 30 2020 at 09:01):

The problem to me is consistency. To find a named theorem you have to know the name and know it's important enough to use the name instead of the standard scheme. The good thing about following the standard scheme is that it's mostly thoughtless: you guess what the beginning should be and try tab complete. Inserting a disjunction in there makes things harder.

view this post on Zulip Rob Lewis (Sep 30 2020 at 09:02):

It's also much easier to grep for a "traditional" name in a doc string than to grep for a standard scheme name in a doc string, if people even bothered to put those in (which they wouldn't).

view this post on Zulip Johan Commelin (Sep 30 2020 at 09:05):

I strongly agree with both arguments that Rob made

view this post on Zulip Rob Lewis (Sep 30 2020 at 09:11):

Kevin Buzzard said:

Here's a funny idea. For people who are expecting things like binomial_theorem or pythagorean_theorem we could capitalise and define the term to mean the statement of the theorem

About Kevin's suggestion here, I don't really see the point. This would just be noise in the library. We shouldn't prove theorem add_sq_eq_sq : Pythagorean_Theorem or whatever. This just adds a useless layer of indirection, makes things hard for any metaprograms that work at the syntactic eq level, etc. So def Pythagorean_Theorem : Prop := a^2 + b^2 = c^2 would never be used in the library.

view this post on Zulip Johan Commelin (Sep 30 2020 at 09:12):

I think Kevin doesn't want to use it. But just have it as a nice trophy on a wall.

view this post on Zulip Johan Commelin (Sep 30 2020 at 09:13):

we could have hall_of_fame.lean:

import all

theorem pythagoras_holds : Pythagorean_Theorem := add_sq_eq_sq

...

or something similar.

view this post on Zulip Johan Commelin (Sep 30 2020 at 09:14):

But at that point it becomes very similar to overview.yaml, I guess

view this post on Zulip Rob Lewis (Sep 30 2020 at 09:16):

Yeah, this is yet another list that won't get updated and will probably be contained in the Freek list, the undergrad list, and the overview.


Last updated: May 14 2021 at 14:20 UTC