Topic: lemma naming
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.
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).
Johan Commelin (Sep 30 2020 at 09:05):
I strongly agree with both arguments that Rob made
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.
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.
Johan Commelin (Sep 30 2020 at 09:13):
we could have
import all theorem pythagoras_holds : Pythagorean_Theorem := add_sq_eq_sq ...
or something similar.
Johan Commelin (Sep 30 2020 at 09:14):
But at that point it becomes very similar to
overview.yaml, I guess
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