lemma naming

Stream: general

[Rob Lewis]

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.

[Rob Lewis]

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).

[Johan Commelin]

I strongly agree with both arguments that Rob made

[Rob Lewis]

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.

[Johan Commelin]

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

[Johan Commelin]

we could have hall_of_fame.lean:

import all

theorem pythagoras_holds : Pythagorean_Theorem := add_sq_eq_sq

...

or something similar.

[Johan Commelin]

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

[Rob Lewis]

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.