Private definitions and lemmas

Stream: mathlib4

[Emilie (Shad Amethyst)]

I'm unsure what the current stance is on private definitions and lemmas; I'm thinking of marking a few things in my formalization of Rubin's theorem as private, because to me they're just implementation detail, namely:

• defining an intermediary function before proving it is bijective and using Equiv.ofBijective — the function is only really exposed if one unfolds the generated Equiv, and I have a theorem that makes this result public already (example snippet from my branch)
• wrappers around Exists.choose and Exists.choose_spec — I have to apply Exists.choose inside of a biInter, and I haven't found a better way to do this without making the proof next to unreadable (example snippet from my branch)
• in general, one-time-use lemmas that are very unlikely to see any use outside of one or two upcoming theorem
• strictly weaker statements, like proving ≤ before proving = from le_antisymm

The big issue I am seeing with private definitions is that you cannot unfold them, but in a perfect world unfold-ing shouldn't be necessary outside of the module proving theorems about the definition.

[Moritz Doll]

Mathlib generally avoids private and instead uses names like foo_aux instead, see docs#ContinuousLinearMap.adjointAux for example

[Ruben Van de Velde]

I think there were implementation issues with private in lean 3 but they may be solved in lean 4, so I don't think there's a strong reason to avoid it on that account. It may make it harder to prove new API lemmas elsewhere though, for example in preparation for upstreaming

[Yaël Dillies]

I agree with your use cases. I mark definitions private when they fulfill one of your requirements.

[Yaël Dillies]

And I believe the pattern Moritz is referring to should be stopped

[Eric Wieser]

Maybe the rule should be that if you put aux in the name, it should also be private? I think keeping the aux in private names is fine, as it avoids local naming conflicts

[Yaël Dillies]

Yeah sure (and I've mostly been doing that). private names don't really matter, so you do you

[Mario Carneiro]

I think for definitions we should still avoid private. For theorems it's mostly fine

[Mario Carneiro]

but the argument that you never know when someone will want to prove more things about that definition you made and thought was only relevant for two theorems still applies in mathlib itself

[Damiano Testa]

I personally do not really like private, but I like the idea of some flagging of definitions that are intended as stepping stones. So, personally, I find the aux naming a good practice.

[Damiano Testa]

My view is that private is a good way of avoiding downstream use of the declaration. This makes perfect sense for a programming language developper that wants to have some internals, but only worry about not changing the outward-facing programs.

In Mathlib, the subject is... mathematics! Everyone should have access to whatever they want!

[Mario Carneiro]

well there is still the issue of backward compatibility and migration, which makes it useful to have a notion of "these things you can count on, those things are refactored frequently and you should coordinate with X and Y if you want to use them"

[Mario Carneiro]

I'm not sure private is exactly the right mechanism for this though

[Martin Dvořák]

In my projects, almost everything is private. It sometimes leads to a clash of opinions when I end up contributing my results to Mathlib. Namely #9705 ...

[Mario Carneiro]

these are mathlib wide design decisions, I would advise you to go with the prevailing style and separately pursue changing that style if you want

[Martin Dvořák]

Yeah, I usually aim to accommodate my work the the Mathlib ways. Sometimes it is hard tho, because this design decision raises the bar for how well my implementation details have to be handled. Hence my PR is currently in the "awaiting author" state.

[Mario Carneiro]

I'm not sure what that means, the bar is the same either way

[Mario Carneiro]

an *Aux function can be written in a way which is convenient for the known use cases just like a private function

[Yaël Dillies]

Mario Carneiro said:

but the argument that you never know when someone will want to prove more things about that definition you made and thought was only relevant for two theorems still applies in mathlib itself

It definitely doesn't apply to the things I mark private in Bhavik and I's formalisation of combinatorics where concepts do not correspond to a single general theorem but rather to a collection of analogous statements with varying asymptotic behavior depending on the application.

[Mario Carneiro]

I don't know what that means

[Junyan Xu]

Emilie (Shad Amethyst) said:

• wrappers around Exists.choose and Exists.choose_spec — I have to apply Exists.choose inside of a biInter, and I haven't found a better way to do this without making the proof next to unreadable (example snippet from my branch)

This seems to be a combination of docs#Finite.to_properlyDiscontinuousSMul and this lemma I proved.

Also,

lemma _root_.OrderEmbedding.injective {α β : Type*} [PartialOrder α] [Preorder β] (f : α ↪o β) :
    Function.Injective f := f.inj'

should work

[Emilie (Shad Amethyst)]

Yeah I figured in the meantime this lemma could go, I was focused on something else when I wrote this :)

[Eric Wieser]

Mario Carneiro said:

but the argument that you never know when someone will want to prove more things about that definition you made and thought was only relevant for two theorems still applies in mathlib itself

If this happens, then arguably this definition is worthy of an aux-less name; but I guess the difference is that it's easier for downstream users to work around a weird name than it is to direct them to import private or whatever the command is

[Junyan Xu]

This seems to be a combination of docs#Finite.to_properlyDiscontinuousSMul and this lemma I proved.

I see that my version doesn't subsume yours because your code doesn't mention compactness and allows for a set s not necessarily equal to the whole group. Nevertheless I think the statements are similar in spirit so I hope my code could help you simplify yours :)

[Emilie (Shad Amethyst)]

I'd have to ponder this a bit more, I don't see immediately how I can use your theorem, since I don't think I can get to a ProperlyDiscontinuousSMul from my context

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

but the argument that you never know when someone will want to prove more things about that definition you made and thought was only relevant for two theorems still applies in mathlib itself

If this happens, then arguably this definition is worthy of an aux-less name; but I guess the difference is that it's easier for downstream users to work around a weird name than it is to direct them to import private or whatever the command is

I don't think this follows. You can have a function which is intended as a building block for another function, which has complex arguments, which nevertheless has useful lemmas about it. It doesn't become any easier to name as a result

[Mario Carneiro]

A lot of the List functions are like that

[Mario Carneiro]

List.reverseAux actually gets used quite a lot in mathlib because it has really nice defeqs