euclidean names

Stream: maths

[Johan Commelin]

@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):

• orthogonal → ortho
• projection → proj
• circumcenter → ccenter
• circumradius → cradius

Maybe there are other options out there as well.

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

In this case, maybe orthogonal_projection could just be projection?

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

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

[Kenny Lau]

why O and H?

[Reid Barton]

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

[Reid Barton]

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]

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

[Joseph Myers]

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]

Everything is open for debate (-;

[Reid Barton]

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

[Johan Commelin]

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

[Kevin Buzzard]

standard_symbol.O

[Kevin Buzzard]

Oh, simplex.O even better!

[Johan Commelin]

standard_symbol.O is already taken by orthogonal matrices

[Patrick Massot]

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]

Yep, this is why definition names should be short

[Eric Wieser]

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]

d ^ 2?

[Eric Wieser]

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

[Mario Carneiro]

so?

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

:ping_pong:

[Johan Commelin]

/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]

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

[Yury G. Kudryashov]

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

[Johan Commelin]

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]

euclidean_projection.orthogonal_projection is definitely not in a useful namespace

[Johan Commelin]

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

[Johan Commelin]

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