Zulip Chat Archive

Stream: maths

Topic: euclidean names


view this post on Zulip Johan Commelin (Sep 11 2020 at 12:53):

@Joseph Myers I'm a bit worried that the long names in euclidean/* are hampering readability, because things now often wrap to multiple lines. What do you think of the following renamings (also on all other names that contain these substrings):

  • orthogonalortho
  • projectionproj
  • circumcenterccenter
  • circumradiuscradius

Maybe there are other options out there as well.

view this post on Zulip Reid Barton (Sep 11 2020 at 12:56):

Out of context, I'm not a fan.
What are some problematic lines?

view this post on Zulip Johan Commelin (Sep 11 2020 at 12:59):

https://github.com/leanprover-community/mathlib/pull/4087/files#diff-db3e8bc3ecf028041f199be03f316f16R645
random example

view this post on Zulip Reid Barton (Sep 11 2020 at 13:30):

In this case, maybe orthogonal_projection could just be projection?

view this post on Zulip Johan Commelin (Sep 11 2020 at 13:31):

I don't have a strong opinion on exactly what changes. But I think that these wrapping lines are a bit problematic

view this post on Zulip Reid Barton (Sep 11 2020 at 13:47):

Is it too crazy to use O as a name component for circumcenter, H for orthocenter, etc.?

view this post on Zulip Johan Commelin (Sep 11 2020 at 13:48):

I think it's worth having a poll on that.

view this post on Zulip Kenny Lau (Sep 11 2020 at 13:53):

why O and H?

view this post on Zulip Reid Barton (Sep 11 2020 at 13:55):

These are the traditional letters used for the points: https://en.wikipedia.org/wiki/Triangle_center#Classical_triangle_centers

view this post on Zulip Reid Barton (Sep 11 2020 at 13:59):

another possible compression from that line is square -> sq--mathlib seems to use both and I can't think of another possible meaning of sq

view this post on Zulip Reid Barton (Sep 11 2020 at 14:00):

(sq is also used to abbreviate commutative square in the category theory library, but it's still a square)

view this post on Zulip Joseph Myers (Sep 11 2020 at 14:02):

Would you also use those names in the definitions themselves, or only for lemmas, and would G be used for centroid not just in the Euclidean context? For example, would circumcenter_eq_centroid (this is in namespace affine.simplex) end up as

/-- The circumcenter of a 1-simplex equals its centroid. -/
lemma O_eq_G (s : simplex  P 1) :
  s.O = finset.univ.G  s.points :=

or would only the name of the lemma change?

view this post on Zulip Johan Commelin (Sep 11 2020 at 14:02):

Everything is open for debate (-;

view this post on Zulip Reid Barton (Sep 11 2020 at 14:03):

I was thinking only the lemma names would change, but I don't feel strongly about this

view this post on Zulip Johan Commelin (Sep 11 2020 at 14:03):

I think with good docstrings, and namespaced definitions, we could even have 1-letter definitions in this part of mathlib.

view this post on Zulip Kevin Buzzard (Sep 11 2020 at 14:09):

standard_symbol.O

view this post on Zulip Kevin Buzzard (Sep 11 2020 at 14:09):

Oh, simplex.O even better!

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

standard_symbol.O is already taken by orthogonal matrices

view this post on Zulip Patrick Massot (Sep 11 2020 at 14:33):

I think the issue is only in lemma names, because they use several def names. But of course changing the name from def to lemma is inconsistent :sad:.

view this post on Zulip Mario Carneiro (Sep 11 2020 at 14:51):

Yep, this is why definition names should be short

view this post on Zulip Eric Wieser (Sep 11 2020 at 15:36):

On the subject of long expressions, is there a sensible way to abbreviate terms like dist p₁ s.circumcenter * dist p₁ s.circumcenter? let d = dist p₁ s.circumcenter in d * d? Does mathlib have a square function?

view this post on Zulip Mario Carneiro (Sep 11 2020 at 15:36):

d ^ 2?

view this post on Zulip Eric Wieser (Sep 11 2020 at 15:39):

That then needs an extra lemma to work with, right? pow_2_eq_mul or something

view this post on Zulip Mario Carneiro (Sep 11 2020 at 16:03):

so?

view this post on Zulip Mario Carneiro (Sep 11 2020 at 16:04):

I would put more emphasis on keeping theorem statement size down rather than not ever needing to rewrite

view this post on Zulip Johan Commelin (Sep 12 2020 at 05:44):

So... shall we use H and O? I like the idea. (I'm fine with making those names protected, if people fear name clashes otherwise.)

view this post on Zulip Johan Commelin (Sep 24 2020 at 14:00):

:ping_pong:

view this post on Zulip Johan Commelin (Oct 05 2020 at 07:33):

/poll short euclidean names
Let's keep orthogonal_projection, circumcenter, and monge_point, etc...
Let's change to euclidean.H, euclidean.O, and proj, etc... (with long names in the docstrings)

view this post on Zulip Johan Commelin (Oct 05 2020 at 07:36):

@Joseph Myers @Mario Carneiro @Reid Barton you've participated in the above discussion. Please join the vote. (Others are welcome too!)

view this post on Zulip Yury G. Kudryashov (Oct 05 2020 at 08:29):

E.g., triangle can have many one-letter defs in its namespace.

view this post on Zulip Johan Commelin (Oct 05 2020 at 11:03):

I think that most of these names are already in very sensible namespaces. That alone will not solve the issue of having lemma names that are > 50 chars.

view this post on Zulip Gabriel Ebner (Oct 05 2020 at 11:17):

euclidean_projection.orthogonal_projection is definitely not in a useful namespace

view this post on Zulip Johan Commelin (Oct 05 2020 at 11:28):

Sure, that's true.
But I do think that this is orthogonal to getting shorter lemma names by having shorter definition names.

view this post on Zulip Johan Commelin (Oct 05 2020 at 11:29):

Also, not that for bundled morphisms, dot notation doesn't help.


Last updated: May 12 2021 at 08:14 UTC