naming bikeshed: `mkpair`/`unpair`

Stream: mathlib4

[Thomas Murrills]

(See !4#2324) There are currently the names mkpair and unpair in Data.Nat.Pairing. By the naming conventions (and consistency with all other mk* names in lean4, e.g. mkConst, mkAppM, etc.), mkpair should be mkPair. But @Eric Wieser pointed out that mkpair is consistent with unpair, so maybe it was named this way to match.

A blind application of the naming conventions gets us mkPair and unpair, but we should also consider unPair or leaving it as-is. For context, there is no type/declaration Pair—unPair would just be to keep it consistent with mkPair.

[Thomas Murrills]

/poll mkpair/unpair naming bikeshed
mkPair, unPair
mkPair, unpair
mkpair, unpair

[Kyle Miller]

mkpair is short for "make pair" but unpair isn't short for "un??? pair" -- "unpair" is a single word, so I'm not sure what justifies unPair.

[Thomas Murrills]

Right, I think the idea was just to be consistent with mkPair visually even though it doesn't "make sense", since they're more or less inverses and are used close together (e.g. theorems like mkpair_unpair).

[Thomas Murrills]

By the same logic mkpair isn't one word, so we'd be breaking sense somehow either way! :)

[Thomas Murrills]

Ooh, I like pair/unpair. (Was that you who added that just now, @Eric Wieser ?) mk makes me think we're applying a constructor, but there's no type or constructor Pair/pair, so it doesn't really fit with the other mks.

[Kyle Miller]

I think the logic behind mkPair using constructor-like names is that it's the Prod.mk constructor for Nat x Nat, but using a bijection to Nat. (For all you know, Nat x Nat is Nat behind the scenes, so to speak.)

[Thomas Murrills]

Ah, I see! That mks sense. :)

[Thomas Murrills]

Seems like we have a consensus! It does however clash with a couple names in Computability.Primrec, so I had to explicitly use Nat.pair in some places and rename two lemmas (the lemmas were simply named mkpair (namespaced), so I renamed them to nat_pair).

@Mario Carneiro would you like to take a look (!4#2324) to make sure you're ok with that? Feel free to lmk if you'd rather it be different.

[Mario Carneiro]

those namespaced lemmas should be protected

[Thomas Murrills]

The thing is that there are existing lemmas named pair (in the same namespace)

[Thomas Murrills]

So renaming mkpair to pair clashes with those

[Mario Carneiro]

did the other thread decide re: natPair / nat_pair / NatPair / something else?

[Thomas Murrills]

Not afaik; btw another thing that could be done here is to rename the existing one it clashes with (it's actually just one, I renamed the other for consistency)

protected theorem pair : Primrec₂ (@Prod.mk α β) :=
  .pair .fst .snd

[Mario Carneiro]

I would go for natPair then