## Stream: maths

### Topic: euclidean names

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

#### Reid Barton (Sep 11 2020 at 12:56):

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

#### Reid Barton (Sep 11 2020 at 13:30):

In this case, maybe orthogonal_projection could just be projection?

#### 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

#### 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.?

#### Johan Commelin (Sep 11 2020 at 13:48):

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

#### Kenny Lau (Sep 11 2020 at 13:53):

why O and H?

#### 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

#### 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

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

#### 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?

#### Johan Commelin (Sep 11 2020 at 14:02):

Everything is open for debate (-;

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

#### Kevin Buzzard (Sep 11 2020 at 14:09):

standard_symbol.O

#### Kevin Buzzard (Sep 11 2020 at 14:09):

Oh, simplex.O even better!

#### Johan Commelin (Sep 11 2020 at 14:09):

standard_symbol.O is already taken by orthogonal matrices

#### 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:.

#### Mario Carneiro (Sep 11 2020 at 14:51):

Yep, this is why definition names should be short

#### 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?

#### Mario Carneiro (Sep 11 2020 at 15:36):

d ^ 2?

#### Eric Wieser (Sep 11 2020 at 15:39):

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

so?

#### 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

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

:ping_pong:

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

#### 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!)

#### Yury G. Kudryashov (Oct 05 2020 at 08:29):

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

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

#### Gabriel Ebner (Oct 05 2020 at 11:17):

euclidean_projection.orthogonal_projection is definitely not in a useful namespace

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

#### 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