prod vs prod_mk

Stream: maths

[Nicolò Cavalleri]

I see that in many parts of Mathlib (especially for more basic stuff, such as topology) lemmas having to do with the function (λ x, (f x, g x)) are named with prod_mk, whereas in some newer part of mathlib they are named with simply prod (for example there istimes_cont_diff.prod instead of times_cont_diff.prod_mk). I guess the reason for the first name was to distinguish it from prod_map((λ x y, (f x, g y))) to avoid ambiguity. Since I am about to PR a lot of lemmas on product manifolds, I was wondering if it may be a good idea to look for uniformity in Mathlib on these names. This firstly for the sake of coherence itself, that is always a good thing and second because there are a lot of lemmas regarding smooth manifolds that have an identical counterpart in topology up to changing continuous with smooth and adding a few model_with_corners here and there and I want to use exactly the same names for these lemmas as in the continuous case because this way one can write a lemma of this kind in topology, copy and paste it in geometry, do just one smart replace, and that's it. Otherwise one has to look names twice and in general think of different processes for what is in the end the same exact proof. I believe @Patrick Massot and @Mario Carneiro used the name prod_mk in topology and @Sebastien Gouezel used the name prod in geometry. If you guys can decide what you like better between these two conventions, I will adapt the library myself accordingly (at least the geometry and topology sections) and name my lemmas accordingly. For what it counts I like prod_mk better because it completely avoids ambiguity with prod_map and prod is a good name for both, but you should decide on your own and I will just update the library

[Mario Carneiro]

I believe the switch to prod by @Sebastien Gouezel was deliberate, there should be a justification here somewhere

[Nicolò Cavalleri]

He wrote this message answering the same thing I wrote here (but in the stream new members) some time ago (when I was writing that code the first time, now I wrote it again here because I want to PR it and I need to sort this out)
Sebastien Gouezel said:

Coherence is definitely a good option. As to whether we should use prod_mk or prod, I don't have a strong opinion, but I think I prefer slightly prod as it is shorter, and not really ambiguous.

[Nicolò Cavalleri]

It was actually him who told me to ask this publicly in order to decide which of the two conventions to choose so I guess he's also open to hear if anybody has a strong opinion for some reason or if it's the same thing for everybody

[Mario Carneiro]

I believe that prod_mk is the more technically correct name, but I have great sympathy for shortening names and name segments when there is no ambiguity

[Mario Carneiro]

I'm not sure it's entirely true that there is no ambiguity though; especially in theorems about the term the name will reappear smashed together with a bunch of other names and it's entirely possible for the type prod to appear in the same "grammatical position" as the function prod_mk

[Yury G. Kudryashov]

While refactoring measure_theory/ I also met src#measure_theory.simple_func.pair

[Nicolò Cavalleri]

When everybody will have agreed on one of these names I will change it in the topology and geometry sections and leave to other people to change it in the other parts of mathlib if they'll believe it is a good thing to adopt the same conventions of the topology section

[Anne Baanen]

My personal vote goes to pair > prod > prod_mk. See also set_theory/zfc.lean:507: def pair (x y : Set.{u}) : Set.{u} := {{x}, {x, y}}.

[Nicolò Cavalleri]

Anne Baanen said:

My personal vote goes to pair > prod > prod_mk. See also set_theory/zfc.lean:507: def pair (x y : Set.{u}) : Set.{u} := {{x}, {x, y}}.

Sorry, I did not understand, from pair > prod > prod_mk I'd guess that pair would be your first choice, but I interpret your second comment as "pair could be confused with set's pair". So is pair your first choice?

[Sebastien Gouezel]

Let me start a poll on this.

[Sebastien Gouezel]

Vote here if you prefer pair.

[Sebastien Gouezel]

Vote here if you prefer prod.

[Sebastien Gouezel]

Vote here if you prefer prod_mk.

[Sebastien Gouezel]

Vote here if you don't care really care, but you think that coherence over mathlib is a good idea.

[Nicolò Cavalleri]

Just out of curiosity, why is pair a good name?

[Anne Baanen]

I prefer pair because it is the constructor of (ordered) pairs.

[Nicolò Cavalleri]

But isn't it the constructor for set pair? I thought the constructor for elements of the product of types is something like prod.mk or something similar (even if I always use langle rangle)

[Anne Baanen]

I agree that the specific function used to construct a pair in the prod type is called prod.mk by Lean, but that is just one implementation of putting things together so we can take them apart later. Another implementation is Set.pair. A third one is sigma.mk. Arguably, and.intro is another. There are also many structures with an addition operator, and I'm happy with using add to refer to any of them, or all of them.

[Anne Baanen]

Anyway, I don't care a lot about the specific name we use in the end so I will try to refrain from commenting so we can just get this bike shed painted :)