naming conventions

Stream: mathlib4

[Kevin Buzzard]

I've heard a rumour that there is still no final decision made on casing in mathlib4 theorem names. My belief right now is that when we have ported a bunch of these grimy low-level files which have few tactics available then the manual porting job is going to get much easier and in particular more people will be able to get involved, so I see porting these low-level files as a high priority task (in fact there are several reasons why I believe this). Let me talk about the beginning of data.bool.basic, a file so low-level in mathlib3 that it has no imports at all, meaning that you don't even get a tada emoji when you finish a tactic proof, although this is not really an issue because there is only one begin end block in the entire file anyway.

The block below is referring to naming of the first few theorems in data.bool.basic. The format of the block is:

mathlib3_name : mathlib3_statement
mathlib3port auto-gen name
my proposed mathlib4_name : mathlib4_statement

Note that mathlib3's tt : bool is mathlib4's true : Bool, mathlib3's to_bool is mathlib4's decide, mathlib3's coe_sort is mathlib4's CoeSort.coe. Note also that I am not speaking from a position of authority when it comes to mathlib4 naming -- in fact I am speaking from a position of complete cluelessness. On the other hand I'm thoroughly enjoying porting data.bool.basic even though it's turning out to be very hard work (I'm still only a quarter of the way through -- I work on it when I'm on my commute). Any advice as to what these things should be called would be welcome -- even if the advice is "quit changing the mathlib3port names". [note added in proof: I just realised that mathlib3port is not changing the names at all!]

If names get changed, my understanding is that I should do #align mathlib3_name mathlib4_name after the proof of the theorem. Is that right?

theorem coe_sort_tt : coe_sort.{1 1} tt = true :=
coe_sort_tt
theorem CoeSort_coe_true : (↥ true : Prop) = True :=

theorem coe_sort_ff : coe_sort.{1 1} ff = false :=
coe_sort_ff
theorem CoeSort_coe_false : (↥ false : Prop) = False :=

theorem to_bool_true {h} : @to_bool true h = tt :=
to_bool_true
theorem decide_True {h} : @decide True h = true :=

theorem to_bool_false {h} : @to_bool false h = ff :=
to_bool_false
theorem decide_False {h} : @decide False h = false :=

theorem to_bool_coe (b:bool) {h} : @to_bool b h = b :=
to_bool_coe
theorem decide_coe (b : Bool) {h} : @decide b h = b :=

theorem coe_to_bool (p : Prop) [decidable p] : to_bool p ↔ p :=
coe_to_bool
theorem coe_decide (p : Prop) [d : Decidable p] : decide p ↔ p :=

lemma of_to_bool_iff {p : Prop} [decidable p] : to_bool p ↔ p :=
of_to_bool_iff
theorem of_decide_iff {p : Prop} [Decidable p] : decide p ↔ p :=

lemma tt_eq_to_bool_iff {p : Prop} [decidable p] : tt = to_bool p ↔ p :=
tt_eq_to_bool_iff
theorem true_eq_decide_iff {p : Prop} [Decidable p] : true = decide p ↔ p :=

lemma ff_eq_to_bool_iff {p : Prop} [decidable p] : ff = to_bool p ↔ ¬ p :=
ff_eq_to_bool_iff
theorem false_eq_decide_iff {p : Prop} [Decidable p] : false = decide p ↔ ¬p :=

[Mario Carneiro]

theorem CoeSort_coe_true : (↥ true : Prop) = True :=

This one is actually true_eq_true_eq_True if you actually look at the statement:

CoeSort_coe_true : (true = true) = True

Theorems about coercions are going to be misleading like this, and most likely they should just be removed and all applications of the theorem should use something else.

[Mario Carneiro]

The standard way of coercing a bool to a prop is currently b = true, so we should probably come up with some naming convention for this that doesn't require spelling out the eq_true all the time

[Mario Carneiro]

Since coe doesn't actually show up in any of the statements of the lemmas, I would avoid names that contain coe. Other suggestions: to_bool_coe -> decide_bool, coe_to_bool -> decide_eq_true, of_to_bool_iff -> isn't this the same theorem?, tt_eq_to_bool_iff -> true_eq_decide, ff_eq_to_bool_iff -> false_eq_decide

[Yakov Pechersky]

Re mentions of coe, what's the mathlib4 equivalent of a lemma that has the following statement?

theorem cases_on'_none_coe (f : Option α → β) (o : Option α) :
    casesOn' o (f none) (f ∘ coe) = f o := by

What do we put now instead of coe?

[Mario Carneiro]

(↑)

[Yakov Pechersky]

Thanks! Can one do explicit ((a : α) : Option α) as well?

[Kevin Buzzard]

When I tried to use a coercion (in this case \-|u or whatever order you put those three characters in) it was automatically unfolded in the statement I was using it in. Is this normal?

[Mario Carneiro]

yes, this is a significant difference from lean 3

[Mario Carneiro]

The function coe basically never shows up in statements anymore, coercions are now unfolded at elaboration time

[Mario Carneiro]

(I'm not sure what anagram of those characters you mean, I usually just use \u)

[Kevin Buzzard]

(I was coe'ing to sort)

[Scott Morrison]

So... what is the casing rule for things like

theorem lift_rel_subrelation_lex : Subrelation (LiftRel r s) (Lex r s) := LiftRel.lex

?

1. Leave as is, to avoid having to write lots of #align statements, and potentially do a big rename after the port?
2. Rename to LiftRel_Subrelation_Lex, and add lots of #align statements.

I think I prefer 1., however much that leaves lemma names unpredictable for now.

[Mario Carneiro]

I think it is better to take advantage of our heavy work on tool-assisted renaming now rather than postponing what could be thousands of renames into the future

[Mario Carneiro]

I've been reviewing diffs of lean3port and it's really looking a lot better than before

[Mario Carneiro]

Personally, the way I've been leaning toward combining our snake-casing theorem convention with capitalized definition names is to lowercase the definitions without going full snake case so that name components stay together. So your example would be rendered as liftRel_subrelation_lex

[Mario Carneiro]

Name components in a theorem would only stay capitalized when this is needed to work around a name conflict, as in And_assoc, although even here I'm inclined to use and_assoc for associativity of And and Bool.and_assoc for associativity of and

[Yakov Pechersky]

For this subrel example, we rename explicitly in a manual way in the file correct? Is there any align we need to define here?

[Mario Carneiro]

If the name is not the one that mathport would have already generated, you need to add an #align directive with the original lean 3 name and the new lean 4 name.

[Mario Carneiro]

I suggest putting it immediately after the theorem

[Jannis Limperg]

Mario Carneiro said:

Name components in a theorem would only stay capitalized when this is needed to work around a name conflict, as in And_assoc, although even here I'm inclined to use and_assoc for associativity of And and Bool.and_assoc for associativity of and

If you need so many exceptions (some of which, like this one, are even non-local), isn't that a sign that the naming convention is not good? Throughout all these discussions, I've never understood what's wrong with taking the 'components' of a theorem's type, with whatever case they have, and putting underscores between them. So And_assoc because it's about And, Subrelation because it's about Subrelation.

[Mario Carneiro]

Well, LE_Iff_Eq_Or_LT didn't play well with the focus groups

[Mario Carneiro]

The naming conflict in this case could be solved if and was an export of Bool.and

[Jannis Limperg]

I don't mind LE_Iff_Eq_Or_LT at all and I think people would get used to it very quickly. So if there's still a chance to go in this direction, I think this should be reconsidered. But I realise I'm quite late.

[Mario Carneiro]

Stuff like inv_Eq_Iff_inv_Eq just looks (and is) very random

[Jannis Limperg]

It looks a bit funny maybe, but it's perfectly straightforward and predictable. More so than a convention that requires case-folding with exceptions. And the funny looks are not a long-term concern imo. Two months with any naming convention and it'll feel perfectly natural.

[Mario Carneiro]

well I'm arguing for case folding (almost) without exceptions. I won't say there are no exceptions but honestly I think that a good naming convention should always allow for exceptions lest you get absurd examples. Naming conventions are for humans, not machines.

[Mario Carneiro]

Anyway the naming convention was the source of a long discussion so I don't want to diverge too much from what we are using today

[Jannis Limperg]

All right. Doesn't matter too much at the end of the day.

[Yakov Pechersky]

Not trying to bikeshed, just get clarity on guidelines... for this instance
instance lift_or_get_is_left_id (f : α → α → α) : IsLeftId (Option α) (liftOrGet f) none :=
should that be liftOrGet_isLeftId? Does it not matter because it is an instance?

[Jakob von Raumer]

Wouldn't that be IsLeftId_liftOrGet?

[Scott Morrison]

cf. the example

theorem lift_rel_subrelation_lex : Subrelation (LiftRel r s) (Lex r s) := LiftRel.lex

above, which I think we decided to case as liftRel_subrelation_lex. Each CamelCased chunk had its initial capital lowered when forming the theorem name.

[Jakob von Raumer]

Remind me, why does subrelation go in the middle here? Because we're to imagine it as an infix operator?

[Scott Morrison]

I guess so. I've never had strong opinions about word order in theorem names...

[Jon Eugster]

Is there a file where these naming conventions are written down? Seems like https://github.com/leanprover-community/mathlib4/wiki would be a good place.

[Yakov Pechersky]

Should docs#cmp_le be CmpLe or CmpLE? How should cmp_le_swap be spelled? cmpLe_swap?
Mathlib3:

def cmp_le {α} [has_le α] [@decidable_rel α (≤)] (x y : α) : ordering :=

[Kevin Buzzard]

Yakov Pechersky said:

Not trying to bikeshed, just get clarity on guidelines... for this instance
instance lift_or_get_is_left_id (f : α → α → α) : IsLeftId (Option α) (liftOrGet f) none :=
should that be liftOrGet_isLeftId? Does it not matter because it is an instance?

Did we get to the bottom of this? I think I have a similar question. Is the below code following the naming convention?

-- `ReflGen r`: reflexive closure of `r` -/
#check @ReflGen -- @ReflGen : {α : Type u_1} → (α → α → Prop) → α → α → Prop
theorem refl_gen_iff (r : α → α → Prop) (a b : α) : ReflGen r a b ↔ b = a ∨ r a b := sorry

I'm still very much getting used to the idea that the concept of "ReflGen" might manifest itself as both ReflGen and refl_gen in names of declarations. Or have I misunderstood?

[Eric Wieser]

Mario Carneiro said:

Personally, the way I've been leaning toward combining our snake-casing theorem convention with capitalized definition names is to lowercase the definitions without going full snake case so that name components stay together. So your example would be rendered as liftRel_subrelation_lex

Mario Carneiro said:

Well, LE_Iff_Eq_Or_LT didn't play well with the focus groups

Doesn't your rule above advocate lE_iff_eq_or_lT, which feels worse?

[Kevin Buzzard]

Because you're mentioning focus groups let me stress that I have no opinion about the naming convention; Mario's earlier comment that basically everyone will just learn it and get on with it once it's established struck me as probably the truth. My issue is simply that I currently don't understand the naming convention and so struggle to conform to it!

[Mario Carneiro]

Yakov Pechersky said:

Should docs#cmp_le be CmpLe or CmpLE? How should cmp_le_swap be spelled? cmpLe_swap?
Mathlib3:

def cmp_le {α} [has_le α] [@decidable_rel α (≤)] (x y : α) : ordering :=

For acronym name components, I prefer to capitalize / lowercase them as a group, although I think that this has been used inconsistently for LE. That is, this approach would suggest the names CmpLE and cmpLE_swap. Although, I've already violated this rule it seems...

[Mario Carneiro]

(Another fun thing about this example is that it is exactly the opposite of your example - it derives LE from an Ordering function rather than the other way around.)

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

Well, LE_Iff_Eq_Or_LT didn't play well with the focus groups

Doesn't your rule above advocate lE_iff_eq_or_lT, which feels worse?

As another example, the acronym naming convention would use le_iff_eq_or_lt in this example, this is what I mean by lowercasing as a group.

[Mario Carneiro]

But also, it's totally fine to challenge these conventions! I'm just making stuff up here trying to get something that is mostly deterministic, doesn't look too weird, and still has some room for the author's own tastes

[Mario Carneiro]

Kevin Buzzard said:

Yakov Pechersky said:

Not trying to bikeshed, just get clarity on guidelines... for this instance
instance lift_or_get_is_left_id (f : α → α → α) : IsLeftId (Option α) (liftOrGet f) none :=
should that be liftOrGet_isLeftId? Does it not matter because it is an instance?

Did we get to the bottom of this? I think I have a similar question. Is the below code following the naming convention?

-- `ReflGen r`: reflexive closure of `r` -/
#check @ReflGen -- @ReflGen : {α : Type u_1} → (α → α → Prop) → α → α → Prop
theorem refl_gen_iff (r : α → α → Prop) (a b : α) : ReflGen r a b ↔ b = a ∨ r a b := sorry

I'm still very much getting used to the idea that the concept of "ReflGen" might manifest itself as both ReflGen and refl_gen in names of declarations. Or have I misunderstood?

no, those should be liftOrGet_isLeftId and reflGen_iff respectively

[Yakov Pechersky]

By the way, I've been avoiding this question for instance names by making instances anonymous.

[Yakov Pechersky]

For the cmp_le, I also ended up with CmpLE in my PR, so I think we deterministic-ed in the same way.

[Mario Carneiro]

One thing that I may or may not have mentioned before: I think instances should be named either like theorems, or using something similar to the automatic lean 4 naming system which is basically inst + the conclusion mashed together into one word, at the author's discretion. In particular I don't think we should use Of ever, which mathport sometimes gets wrong

[Mario Carneiro]

When making instances anonymous, make sure to hover on the word "instance" to double check that the autogenerated name is not terribly ambiguous. If the original is named you might also want to #align it (I usually don't align instances unless I think it is being referred to directly for some reason)

[Yakov Pechersky]

For a lot of the base files, it's hard to know if named instances will be referred to, since that reference usually comes much later in the import tree

[Mario Carneiro]

I usually do a text search in mathlib to get a ballpark estimate

[Mario Carneiro]

Some lean 3 instances are named only because the original name was ambiguous and it was causing a duplicate definition error

[Yakov Pechersky]

Would it be alright to defer the aligns until the later files are ported? Because sometimes, names are only used because of shorthand, and in those places, an inferInstanceAs can fill in

[Mario Carneiro]

That sounds fine

[Yakov Pechersky]

Basically, not explicitly naming instances might help with hygiene?

[Mario Carneiro]

Instance names are not hygienic, they used to be but this is actually not as great as it sounds on paper because it totally breaks pp.all reprinting

[Mario Carneiro]

I think it is better to think of them as part of the public surface of the API, even though they are usually heuristically named and usually don't need to be referred to explicitly

[Mario Carneiro]

to_additive does something similar

[Moritz Doll]

I don't get the current naming convention yet, but if I understand this thread and Scott's comment on my PR correctly, then docs4#is_empty_pi should be isEmpty_pi, right? Reason is that I looked at that file and thought I was doing the right thing by not changing the alignment..

[Moritz Doll]

i.e., type names are firstLowerCamelCase if they appear in lemmas

[Scott Morrison]

That's my understanding.

[Scott Morrison]

I think we should be permissive about where it is appropriate to fix naming in earlier files. If you feel like making a separate PR, do that, but I think it's fine to include naming issues in PRs that are mostly about porting a later file.

[Scott Morrison]

This isn't ideal from a history/reviewing point of view, but I think worthwhile for efficiency.

[Moritz Doll]

I can make a PR for renaming the lemmas in that file, mainly as an easy exercise for myself to learn the naming convention.

[Moritz Doll]

I would like to add a section in the wiki for the naming convention.

[Yakov Pechersky]

I thought they are lower_case_snake_case if they are LowerCaseSnakeCase : Prop though.

[Mario Carneiro]

theorems are mostly snake case, but individual name components coming from MyFoo : Prop definitions appear as myFoo_is_bar in theorems, i.e. you don't introduce a _ in the middle of the name

[Andrew Yang]

Is there a written documentation / community wiki on the new naming conventions?

[Moritz Doll]

why do we have has_rightInverse? this should be hasRightInverse or not?

[Moritz Doll]

(deleted)

[Moritz Doll]

oh still wrong - it should be HasRightInverse

[Moritz Doll]

https://github.com/leanprover-community/mathlib4/wiki#naming-convention comments and improvements are very welcome

[Scott Morrison]

We'll get there. :-)

[Andrew Yang]

Why is docs4#Cmp in upper camel case? I think it is defining a term?

[Moritz Doll]

we also have docs4#Set.mem which does also not conform to the convention, before doing more edits I would like to hear from someone with more to say on these matters (aka Mario) that what I wrote is correct and if that is the case then we can go ahead and fix everything we find.

[Moritz Doll]

Also what Yakov mentioned in the morning might become more important: in definition-heavy files the amount of manual aligns is too high and we have to figure out some way to optimize the names that mathport generates. Something along the lines of "get all types of the variables, and if a conversion to snake case matches part of the lemma name then replace that part by camel case".

[Yakov Pechersky]

Regarding Cmp, I totally accept that I could have misunderstood the guidelines for it.

[Mario Carneiro]

Cmp should be cmp, CmpUsing should be cmpUsing, Set.mem should be Set.Mem

[Mario Carneiro]

I think that the type searching heuristic is doable, it just needs some elbow grease

[Jakob von Raumer]

Is there a decision on what to do with the distinction between e.g. inf and Inf?

[Yaël Dillies]

And docs#lattice vs docs#Lattice?

[Mario Carneiro]

well, a Set A is actually a function returning a Prop, so there is an argument to be made that Inf is following the new convention already

[Mario Carneiro]

I'm not sure we came to a final consensus on what to do about functions returning sets

[Mario Carneiro]

If we want to name them as functions I think inf, infi, sInf, bInf is as good as any

[Mario Carneiro]

For lattice vs Lattice the naming convention that mathport implements is to suffix categories with Cat, so they would become Lattice and LatticeCat respectively

[Eric Wieser]

Mario Carneiro said:

well, a Set A is actually a function returning a Prop, so there is an argument to be made that Inf is following the new convention already

Can you make that argument more explicitly please?

[Eric Wieser]

Mario Carneiro said:

If we want to name them as functions I think inf, infi, sInf, bInf is as good as any

docs#infi is already a thing; are you proposing renaming Inf to infi and infi to ...?

[Mario Carneiro]

no I meant keeping infi as is

[Yaël Dillies]

I'm not a big fan of appending 3 letters to the names of the numerous categories we have in order theory. Some lemma names are already stupidly long.

[Mario Carneiro]

Inf would become sInf there

[Mario Carneiro]

:shrug:

[Eric Wieser]

What is the bInf of your proposal?

[Mario Carneiro]

infimum bounded by a set; it isn't an actual definition but it shows up in lots of lemmas

[Eric Wieser]

What we call binfi right now (because it's about infi not Inf)

[Mario Carneiro]

oh, that's a name change I hadn't noticed

[Mario Carneiro]

bInfi works too

[Eric Wieser]

Mario Carneiro said:

I'm not sure we came to a final consensus on what to do about functions returning sets

Maybe you're referring to something else, but Inf isn't a function returning a set, it's a function consuming a set

[Mario Carneiro]

oh right, I was thinking about set big union

[Mario Carneiro]

I think we should go for lowercased names for all of these then

[Yaël Dillies]

We should definitely respect capitalisation between Inf and Union. They are genuinely the same function.

[Eric Wieser]

No they're not, docs#set.Union is docs#infi

[Eric Wieser]

And docs#set.sUnion is docs#Inf

[Eric Wieser]

So I think renaming Inf to sInf is very reasonable (along with cInf to csInf?)

[Yaël Dillies]

Aah, of course I meant sUnion

[Yaël Dillies]

I think cInf can stay as is in this scheme.

[Eric Wieser]

Yaël Dillies said:

They are genuinely the same function.

You mean aside from the fact that the union of no sets is empty and the infimum of no sets is the universe, and the functions are morally opposites?

[Mario Carneiro]

The argument I alluded to before @Eric Wieser is that when determining whether a definition returns "data" or "a proposition", it depends on whether we unfold the type (up to reducibles, up to semireducibles?). In the case of Set A := A -> Prop that would mean that anything that returns a Set A should be cased like a proposition, i.e. capital camel case

[Eric Wieser]

@Mario Carneiro: which in this case doesn't actually apply to Inf due to the confusion above, but does apply to set.sUnion

[Mario Carneiro]

Personally I am not a fan of this, I think we should just take the declaration as is without unfolding and hence something returning Set A "returns data" and hence is lowercased

[Eric Wieser]

It definitely shouldn't include unfolding, because then we have to rename everything if we change Set to a structure

[Yaël Dillies]

Sorry, I meant sUnion and Sup, and sInter and Inf

[Moritz Doll]

Mario Carneiro said:

Yakov Pechersky said:

Should docs#cmp_le be CmpLe or CmpLE? How should cmp_le_swap be spelled? cmpLe_swap?
Mathlib3:

def cmp_le {α} [has_le α] [@decidable_rel α (≤)] (x y : α) : ordering :=

For acronym name components, I prefer to capitalize / lowercase them as a group, although I think that this has been used inconsistently for LE. That is, this approach would suggest the names CmpLE and cmpLE_swap. Although, I've already violated this rule it seems...

I am very sorry for pulling this out again, but I was just trying to port zero_le_one and are we really sure that this file should be named zeroLEOne? It looks wrong to me (I read it as zero_leo_ne) and I then realized that nobody complained that we have (and this is my fault as well and I even took that as an example :silence: ) NeZero..

[Mario Carneiro]

it would be zero_le_one

[Mario Carneiro]

because it combines zero, LE and one and they all get lowercased and snake-case strung together

[Andrew Yang]

Doesn't the current naming convention advocate for NEZero instead, for NE being an acronym?

[Mario Carneiro]

that's a good point

[Moritz Doll]

Mario Carneiro said:

it would be zero_le_one

It is a file

[Mario Carneiro]

I'm inclined to make an exception because Ne already exists in core with that spelling

[Moritz Doll]

Andrew that is exactly my point

[Mario Carneiro]

There's a file called zero_le_one?

[Mario Carneiro]

there is.. what is the world coming to

[Moritz Doll]

algebra.order.zero_le_one

[Mario Carneiro]

ZeroLEOne

[Moritz Doll]

alright. does #align also work for filenames?

[Mario Carneiro]

Unsure

[Mario Carneiro]

probably not

[Mario Carneiro]

there are a few other consumers of the file rename map as well, like leanproject --port-progress, so I think we will have to live with the misalignment

[Moritz Doll]

probably not a big problem, since that file is probably not imported too often

[Andrew Yang]

Now that we are on this, shouldn't docs4#HasSmul be HasSMul or even SMul according to the Lean4 manual?

[Mario Carneiro]

SMul

[Riccardo Brasca]

I've proposed this in mathlib4#606

[Riccardo Brasca]

But feel free to open another PR for that, I can just merge master in my PR

[Yaël Dillies]

I think we can just merge algebra.order.zero_le_one with algebra.order.monoid.defs. None imports one but not the other.

[Moritz Doll]

yes, but let's please do that later. I already have mathlib4#664

[Yaël Dillies]

No need to hasten. We can do things right: #17646

[Arien Malec]

I edited the porting wiki to make the naming rules clearer & added more examples. Please review for accuracy...

[Arien Malec]

While we are on it, I'm not at all clear why Ne is UpperCamelCase and isn't treated like LT -- is this to follow Eq?

[Arien Malec]

nevermind -- I see this discussion above.

[Scott Morrison]

@Moritz Doll, I agree with @Yaël Dillies here that #17646 is worth doing first.

[Scott Morrison]

But we should avoid doing this too much, it is costly in time. However in this case it detangles some imports, and I think is valuable.

[Scott Morrison]

@Yaël Dillies, could you keep an eye on that PR and merge as soon as CI completes? I'm going to be offline for a while.

[Yaël Dillies]

No sorry I locked myself in the library for the next 4 jours :sad:

[Ruben Van de Velde]

CI is broken, in fact, but I can push a fix

[Scott Morrison]

Okay :-)

[Yaël Dillies]

But I welcome anyone to keep an eye on it

[Scott Morrison]

Good luck with exams!!

[Yaël Dillies]

Thanks Ruben!

[Scott Morrison]

@Ruben Van de Velde, I just fixed it, but have limited internet and can't push. :-)

[Scott Morrison]

I seem to be allowed to use http, but not ssh, on this network. What fun.

[Ruben Van de Velde]

Then I guess I unfairly beat you to it :)

[Yaël Dillies]

Exams are far still. The only thing I am preparing to beat up is myself.

[Scott Morrison]

I've added a https remote, and will be ready for the next one. I guess I actually need a VPN.

[Scott Morrison]

@Ruben Van de Velde, could you double check you got the right imports there? I think you imported more than necessary.

[Ruben Van de Velde]

The error was missing linear_ordered_comm_monoid_with_zero, which grep tells me is declared in

src/algebra/order/monoid/with_zero.lean:class linear_ordered_comm_monoid_with_zero (α : Type*)

so I think it's right?

[Scott Morrison]

Oh, hmm. Maybe order.hom.basic is not required now, as it's transitively imported? But that doesn't matter. Sorry for the noise.

[Scott Morrison]

There's another failure now.

[Ruben Van de Velde]

Want me to take a look at this one too?

[Scott Morrison]

Could you? I'm getting confused by not having ssh access and sorting out alternate remotes. :-(

[Ruben Van de Velde]

Sure

[Moritz Doll]

Scott Morrison said:

But we should avoid doing this too much, it is costly in time. However in this case it detangles some imports, and I think is valuable.

I am sorry, I did not look at the PR and thought it was just doing the merging, not the other cleanup.
If the process of untangling imports causes delays in the porting then I am not so sure whether it is a good idea to do it before porting. We have to port all files anyways and moving things around in mathlib3 makes the port only faster if the number of files to port is the bottleneck. Of course these refactors are worthwhile in their own right.

[Jireh Loreaux]

Are we changing coe in names to the name of the function they unfold to?

[Mario Carneiro]

I think we should

[Jireh Loreaux]

that's what I thought, good.

[Mario Carneiro]

I mean, the function itself might be named coe, maybe we should use that name more consistently for coe-registered functions

[Mario Carneiro]

e.g. Nat.cast -> Nat.coe

[Jireh Loreaux]

What about Units.val? Moreover, what if there is more than one coercion on a given type (e.g., ℝ≥0 coerces to both ℝ and ℝ≥0∞)?

[Mario Carneiro]

if the function has a better name then that's fine

[Mario Carneiro]

I would not use the name coe in either of those examples

[Yaël Dillies]

I assume we don't want to write toFun in lemma names.

[Mario Carneiro]

that one does sound like a function we should call coe

[Jireh Loreaux]

Shouldn't docs4#HasSmul just be called Smul?

[Moritz Doll]

there is a PR that does that rename

[Moritz Doll]

mathlib4#606

[Jireh Loreaux]

aha, thanks.

[Ruben Van de Velde]

protected theorem IsBot.is_min (h : IsBot a) : IsMin a := fun b _ => h b

Should this be IsBot.isMin?

[Ruben Van de Velde]

Ruben Van de Velde said:

protected theorem IsBot.is_min (h : IsBot a) : IsMin a := fun b _ => h b

Should this be IsBot.isMin?

https://github.com/leanprover-community/mathlib4/pull/713

[Scott Morrison]

/-- Make a ring homomorphism from an additive group homomorphism from a commutative ring to an
integral domain that commutes with self multiplication, assumes that two is nonzero and `1` is sent
to `1`. -/
def mkRingHomOfMulSelfOfTwoNeZero (h : ∀ x, f (x * x) = f x * f x) (h_two : (2 : α) ≠ 0)
    (h_one : f 1 = 1) : β →+* α :=

Could / should this be mkRingHom_of_mul_self_of_two_ne_zero?

[Scott Morrison]

This is the last question remaining on mathlib4#958, so probably I'll merge as is.

[Winston Yin]

Maybe it’s not aesthetically pleasing, but I don’t see this as any worse than the super long auto generated instance names

[Reid Barton]

Well you're not really supposed to need to refer to instances by name, while you do refer to defs by name.

[Mario Carneiro]

the current naming convention says no, but I am certainly sympathetic to wanting to snake case this

[Mario Carneiro]

but it could also get a shorter name which is less about symbol reading

[Eric Wieser]

I don't think we need to block on this for that PR, I just though I should raise it for future consideration

[Eric Wieser]

Perhaps something like "Switch to snake case for trailing prop arguments"

[Yaël Dillies]

Just found an interesting capitalisation error. docs4#Disjoint.comm should be disjoint.comm because it's a lemma name and dot notation doesn't apply, but clearly the weird name threw off whoever ported it.

[Sky Wilshaw]

Should it not be disjoint_comm to match with things like disjoint_self and disjoint_bot_left?

[Sky Wilshaw]

Presumably this should apply to the original mathlib3 name too.

[Yaël Dillies]

Yes, I am renaming it to disjoint_comm. We could backport the change, but also the #align will take care of it for us so we can avoid the fuss.

[Sky Wilshaw]

Ah, nice.

[Eric Wieser]

I don't think disjoint.commwould be correct

[Sky Wilshaw]

Yeah, there's no disjoint namespace.

[Sky Wilshaw]

Or rather, there shouldn't be.

[Yaël Dillies]

I didn't want to throw people off by suggesting removing the namespace, but I guess we agree :grinning_face_with_smiling_eyes:

[Yaël Dillies]

I guess this is a good reason to get rid of the weird docs#and.comm and friends

[Sky Wilshaw]

The names of those lemmas do look pretty weird.

[Sky Wilshaw]

I wonder if this is a lint that can be made? If there is a definition/theorem where its namespace is capitalised, it must refer to an item in the environment?

[Sky Wilshaw]

...and dot notation should apply.

[Eric Wieser]

Or phrased another way; never have two namespaces which are case-insensitively the same?

[Yaël Dillies]

Ah, in fact this is a much wider problem than I originally thought. There are some predicates that have corresponding namespaces, and all the basic API about them is dumped into that namespace even when there is no dot notation possible.

[Yaël Dillies]

Consider docs4#Commute

[Eric Wieser]

I don't think we need to worry about this too much in the port

[Eric Wieser]

It's already inconsistent in mathlib 3

[Sky Wilshaw]

Eric Wieser said:

Or phrased another way; never have two namespaces which are case-insensitively the same?

This wouldn't fix the original issue, because the namespace was translated to Disjoint.

[Yaël Dillies]

The thing is that our new naming convention makes it matter :frown:

[Eric Wieser]

This wouldn't fix the original issue, because the namespace was translated to Disjoint.

That's correct though?

[Sky Wilshaw]

I think we're talking about different things, I was suggesting that a linter deny the use of the Disjoint namespace when dot notation can't be used, like in Disjoint.comm.

[Sky Wilshaw]

I could very easily be misunderstanding though

[Sky Wilshaw]

Yaël Dillies said:

The thing is that our new naming convention makes it matter :frown:

At least from my perspective it's just making assumptions visible that we didn't realise we were making

[Yaël Dillies]

The thing is that we want to allow lemmas such as docs4#Nat.add_le_add...

[Sky Wilshaw]

That makes sense, so my suggestion for a lint rule would absolutely not work.

[Sky Wilshaw]

But then again, that implies Disjoint.comm is a reasonable spelling.

[Sky Wilshaw]

In this context, disjoint_comm is clearer, but I can't really tell why I think that.

[Yaël Dillies]

I think your linter is reasonable so long as it only runs on namespaces associated to predicates.

[Yaël Dillies]

In fact, this is the same dichotomy I am making to decide whether a given lemma should be protected (see for example #18076)

[Sky Wilshaw]

I think I'd need to see more examples to convince myself it's a good idea.

[Yaël Dillies]

cc @Alex J. Best, because we're talking about the linter I made you write

[Yaël Dillies]

Empirically, we open namespaces associated to structures, and we don't open namespaces associated to predicates.

[Sky Wilshaw]

(ignore)

[Yaël Dillies]

The best dichotomy would be to see whether a given namespace is ever opened, but that sounds like a terrible idea :stuck_out_tongue_closed_eyes:

[Sky Wilshaw]

The problem I see with Disjoint.comm is that

• opening the namespace is bad because you end up with the badly named comm
• not opening the namespace is bad because you have to write Disjoint.comm every time, so you should have named it disjoint_comm instead

[Eric Wieser]

• opening the namespace is bad because you end up with the badly named comm

I don't see how this is any worse than opening the namespace and getting symm

[Sky Wilshaw]

I agree, opening that namespace is just generally bad.

[Eric Wieser]

I think that's true of a very large number of namespaces

[Eric Wieser]

It is definitely annoying that in lean 3 you could try foo_bar.baz and foo_bar_baz when looking for a lemma, but in Lean 4 you have to try FooBar.bar and fooBar_baz which is more than one character different

[Sky Wilshaw]

Is it possible for the LSP to just know that those mean the same thing?

[Eric Wieser]

It could certainly offer to autocorrect the wrong one to the right one

[Eric Wieser]

Am I right in saying that we have a rule that functions in Prop (such as Disjoint) should be UpperCamelCase? If so, why do Nonempty.intro and LE.le not follow this rule?

[Mario Carneiro]

Because it's in core. I had a conversation with Leo about this; one of the points he disagrees with on the current style guide is that structure fields being capitalized is too weird (examples given include Membership.mem and LE.le). I've been putting off what to do about this situation, but there is an open PR lean4#1897 about it. Leo has indicated that he doesn't want to lose hair in naming convention discussions, which I totally understand. I'm not really sure how best to approach the situation, but it would be good if we could find a compromise which isn't just special casing these classes.

[Thomas Murrills]

If we want a compromise rule that includes these cases, how about:

Structure fields which are not exported and which would otherwise be UpperCamelCase are instead lowerCamelCase.

[Thomas Murrills]

The carve-out for exported things makes naming a bit more subtle, but has the benefit of making usage and reading more consistent.

The “real” rule that this implements is just “if it follows a dot, it starts with a lowercase letter” (otherwise it’s named normally)

[Johan Commelin]

I'm still confused. Is this right?

theorem ndinter_eq_zero_iff_disjoint {s t : Multiset α} : ndinter s t = 0 ↔ Disjoint s t

or should disjoint in the name be Disjoint?

[Yaël Dillies]

It should be disjoint because of lowerCamelCase

[Eric Wieser]

What's the lower-cased version of docs4#SMulCommClass ? smulCommClass or sMulCommClass? If you look at the instances we currently have a mixture

[Anne Baanen]

Based on how I pronounce it in my mind, I'd write smulCommClass. (yum!)

[Eric Wieser]

!4#2557

[Jireh Loreaux]

It's smul because of the lowercase as a group rule.

[Siddhartha Gadgil]

Should the square root of -1 be Complex.I or Complex.i? @Eric Wieser suggested Complex.I and in mathlib3 it is complex.I (but mathport used lowercase)

[Scott Morrison]

Let's keep .I.

[Notification Bot]

29 messages were moved from this topic to #mathlib4 > naming conventions: natCast vs nat_cast by Eric Wieser.

[Yury G. Kudryashov]

Hi, why do we drop Is in is_haar_measure etc?

[Eric Wieser]

I also think that's strange. Did a human do that, or did mathport?

[Yury G. Kudryashov]

It was done by @Pol'tta / Miyahara Kō in !4#4496 and approved by @Chris Hughes and @Johan Commelin.

[Heather Macbeth]

This seems like a bad idea given that we need to distinguish docs#measure_theory.measure.is_haar_measure from docs#measure_theory.measure.haar_measure.

[Eric Wieser]

Also IsAddLeftInvariant got renamed to AddLeftInvariant

[Eric Wieser]

@Pol'tta / Miyahara Kō, can you explain why you did this rename?

[Eric Wieser]

Were you confusing Is with Has?

[Yury G. Kudryashov]

Heather Macbeth said:

This seems like a bad idea given that we need to distinguish docs#measure_theory.measure.is_haar_measure from docs#measure_theory.measure.haar_measure.

Now we have HaarMeasure (TC) vs haarMeasure (def)

[Pol'tta / Miyahara Kō]

Sorry, I didn't read the porting wiki well and misunderstood the rule for IsLawfulFoo.

[Pol'tta / Miyahara Kō]

I will make the PR which fix this.

[Yury G. Kudryashov]

Thank you!

[Eric Wieser]

I'm not sure I know what #porting-wiki says there... (edit: what's the linkifier?)

[Pol'tta / Miyahara Kō]

!4#4639 is ready to review.

[Jireh Loreaux]

What is our stance on UpperCamelCase versus lowerCamelCase for things which are technically terms, but which have a CoeSort and we always think of them as types? The example I have in mind because I'm currently porting it is docs#weak_dual.character_space. Technically, this has type (in Lean 4 notation) Set (WeakDual 𝕜 A), but we are always using it as a type. In fact, it being of type Set (WeakDual 𝕜 A) as opposed to being a type synonym for a subtype of WeakDual 𝕜 A is entirely an implementation detail.

[Eric Wieser]

Arguably it's not an implementation detail, because the user has to use coeSort everywhere

[Jireh Loreaux]

Fair enough, for that and other reasons I concede it's not an implementation detail.

[Jireh Loreaux]

So what should I do with the namespace WeakDual.CharacterSpace? Should I call it WeakDual.characterSpace?

[Eric Wieser]

Refactor it in mathlib3 first and make it a subtype!

[Reid Barton]

But technically technically, Set X = X -> Prop so t : Set X is still a type

[Eric Wieser]

Eric Wieser said:

Refactor it in mathlib3 first and make it a subtype!

The other reason to do this is I think it will make dot notation work.

[Eric Wieser]

@Reid Barton, I don't understand that reasoning at all

[Jireh Loreaux]

I am looking at that refactor, however, we would lose the ability to (easily) say things like docs#weak_dual.character_space.union_zero

[Eric Wieser]

You could instead take the range of the coercion to talk about the set

[Jireh Loreaux]

Right, it's just not quite as easy.

[Jireh Loreaux]

It would give us dot notation though. @Frédéric Dupuis I know we discussed this design choice back when you defined the character space. Do you have thoughts on the matter?

[Frédéric Dupuis]

From what I recall, my impression at the time was that using a set as a type worked quite seamlessly, whereas using a subtype as a set was very painful, so we went with a set even though most of the time we want to think of it as a type.

[Frédéric Dupuis]

If the subtype approach turns out to be not so painful after all, I'd be happy with it.

[Jireh Loreaux]

Okay, I'll look into that refactor further.

[Jireh Loreaux]

This seems feasible and not too much of a headache (in some places it's likely nicer), but I don't have a strong reason to do it before the port. We can reconsider after the port whether we want a set with CoeSort or a subtype.

[Johan Commelin]

Eric Wieser said:

Reid Barton, I don't understand that reasoning at all

Is X → Type considered a type? Reid is saying that t : Set X is a family of Props.

[Wojciech Nawrocki]

While porting CategoryTheory.Closed.Cartesian I came across (already ported) names isIso_of_mono_of_isSplitEpi and Adjunction.leftAdjointOfNatIso. There are more names in both styles. I would have expected either the latter to be Adjunction.leftAdjoint_of_natIso, or the former to be isIsoOfMonoOfIsSplitEpi. Is this an inconsistency, or is there a rule?

[Ruben Van de Velde]

There is a rule, and it's whether the result is a Prop or not

[Scott Morrison]

It's not the greatest rule, but it's a rule. :-)

[Yury G. Kudryashov]

Should we translate docs#measure_theory.has_pdf as HasPdf or HasPDF?

[Jireh Loreaux]

HasPDF is the only thing that makes sense to me.

[Jireh Loreaux]

Is there precedent for things like HasPdf?

[Yury G. Kudryashov]

docs4#ENNReal

[Yury G. Kudryashov]

I'll fix !4#4962 later today.

[Jireh Loreaux]

That's not a precedent because the Real part isn't an acronym, whereas PDF is.

[Alex Keizer]

There's MvQPF as a precedent for capitalizing the entire abbreviation.

[Floris van Doorn]

The gamma function in Lean 3 was called complex.Gamma/real.Gamma. In Lean 4, should we keep Gamma capitalized or use the usual capitalization conventions (i.e. lowercase gamma)? (c.f. !4#5042)

[Sebastien Gouezel]

This was already discussed in mathlib 3. We settled on Gamma to avoid confusing it with the gamma constant. I think the same applies in Lean 4.

[Floris van Doorn]

ok!

[Mario Carneiro]

I agree regarding confusion from that clear name clash, but I wonder if we can't use some other mechanism than capitalization, like Complex.gammaF

[Mario Carneiro]

it seems kind of similar to the is_o / is_O thing, we shouldn't be treating notations directly as label names

[Jireh Loreaux]

I know it's longer, but Complex.gammaFun seems even better to me.

[Mario Carneiro]

yeah I am also okay with that but didn't want to be the one to propose it :)

[Trebor Huang]

The mathematica solution is EulerGamma for the constant (although it has different casing conventions)

[Timo Carlin-Burns]

docs3#pgame.domineering.L is uppercase because it's talking about an L-shaped fragment of a chess board. Should this remain uppercase in mathlib4 despite not being a type?

Edit: I think uppercase. Hopefully my PR reviewer agrees

[Yuyang Zhao]

Are names like docs#AdjoinRoot.Minpoly.toAdjoin and docs#SetCoe.forall appropriate? docs#AdjoinRoot.Minpoly.toAdjoin references docs#minpoly. SetCoe in docs#SetCoe.forall is not even a name.

[Yuyang Zhao]

In general, what should we do when a non-UpperCamelCase name comes before the dot?

[Anatole Dedecker]

SetCoe is just the name of a namespace, like Metric in Metric.ball, so I think this one is fine (although, for consistency, we should decide whether to move all Subtype. that are really about sets in the SetCoe namespace)

[Ruben Van de Velde]

Should docs#IsFreeGroup.MulEquiv really start with a capital M?

[Jireh Loreaux]

No