Naming convention

Stream: mathlib4

[Xavier Roblot]

I am still a bit confused about some name conventions... For example, are these names (from Algebra.BigOperators.RingEquiv mathlib4#1647) correct: RingEquiv.map_list_prod, RingEquiv.map_multiset_prod?
That is, even though List and Multiset are types, they are not capitalised here because lowerCamelCase(?). I believe they are correct because I found similar examples, see for eg. docs4#map_list_prod.

[Yaël Dillies]

Yes, those are correct.

[Xavier Roblot]

Ok. Thanks!

[Notification Bot]

Xavier Roblot has marked this topic as resolved.

[Notification Bot]

Johan Commelin has marked this topic as unresolved.

[Johan Commelin]

Is this the right name?

def truncEquivFin_of_cardEq [DecidableEq α] {n : ℕ} (h : Fintype.card α = n) : Trunc (α ≃ Fin n) :=
  (truncEquivFin α).map fun e => e.trans (Fin.cast h).toEquiv

[Johan Commelin]

Or should it be truncEquivFinOfCardEq?

[Alex Keizer]

Also, shouldn't it be FinType/FinSet, with the second word capitalized as well?

[Ruben Van de Velde]

:see_no_evil:

[Eric Wieser]

@Alex Keizer, the rule we're using is that if we wrote it as oneword it remains as Oneword, but two_words goes to TwoWords

[Eric Wieser]

@Johan Commelin I think we decided to prefer the Of name in a previous meeting; maybe see if you can find any matches for Of in existing lemma names?

[Ruben Van de Velde]

So, Zmod or ZMod?

[Heather Macbeth]

We have Int.ModEq so maybe ZMod for parallelism?

[Eric Wieser]

Any other thoughts on that? mathlib4#1713 is otherwise ready to go, but currently uses Zmod not ZMod

[zbatt]

Does anyone know how I should handle a case where a class has a field foo but there's also a theorem foo?

[zbatt]

As in this case here

[Reid Barton]

Here they are in different namespaces; is the issue just that you need to use nonrec or _root_, so that Lean doesn't think it's recursive?

[zbatt]

to be honest I'm not entirely sure how nonrec or _root_ work I'll look into it now

[Reid Barton]

Actually since you already wrote Shelf.self_distrib as the proof, it should Just Work with theorem self_distrib [...]

[Reid Barton]

since we're now in namespace Rack

[zbatt]

sorry what goes in the [...]? This currently doesn't work

theorem self_distrib {x y z : R} : x ◃ y ◃ z = (x ◃ y) ◃ x ◃ z :=
  Shelf.self_distrib
#align rack.self_distrib Rack.self_distrib

[Reid Barton]

What is the error?

[zbatt]

invalid declaration name 'Rack.self_distrib', structure 'Rack' has field 'self_distrib'

[Reid Barton]

Oh sorry, that wasn't obvious and I thought the issue was something else.

[zbatt]

sorry, my bad

[Reid Barton]

My impression now is that this theorem is not needed in Lean 4 at all, because of the difference between Lean 3 (new-style!) structures and Lean 4 structures

[Reid Barton]

I would check that the output of #check Rack.self_distrib matches docs#rack.self_distrib, and then #align the latter to the former, and add a porting note

[zbatt]

it can't find it

[zbatt]

wait this is strange

[zbatt]

it was originally complaining that 'Rack' has field 'self_distrib', but if I get rid of the theorem and do #check Rack.self_distrib it tells me its unknown

[Kyle Miller]

I'm trying to remember what the point of rack.self_distrib was. I think it's just meant to be a synonym for shelf.self_distrib but in the rack namespace, since structure extension can't help you with this.

[Kyle Miller]

You might be able to replace it with export Shelf (self_distrib) (if I got that syntax right)

[zbatt]

that seems to have worked, thanks!

[zbatt]

though you run into the same issue with act and you don't seem able to export that in the same way

[Kyle Miller]

It's fine renaming rack.act to Rack.act'. It's not used much, and its main purpose is to be an equivalence version of shelf.act if you need it.

[zbatt]

gotcha

[Yaël Dillies]

Kyle Miller said:

You might be able to replace it with export Shelf (self_distrib) (if I got that syntax right)

Hmm, but we don't want it to be accessible from the root namespace, do we?

[Kyle Miller]

It won't be. In context, that's done within the Rack namespace.

[Yaël Dillies]

Oh, does export know about the namespace it's in? I alwasy it was just stripping away namespaces.

[Kyle Miller]

The export and open commands create aliases (which are not the same sort of thing as what you get from the alias command, confusingly)

namespace A
def x := 37
end A

namespace B
export A (x)
end B

#check x -- unknown identifier
#check B.x -- A.x : Nat

[Kyle Miller]

The difference between export and open is whether these aliases work outside the current namespace.

[Jireh Loreaux]

Why do we have docs4#Set.mem_Icc instead of Set.mem_icc? I don't recall seeing a discussion about this.

[Floris van Doorn]

probably because that is the Lean 3 name. I don't know if that is a good enough reason.

[Jireh Loreaux]

Okay, it would be good to know if we're going to buck the convention on this. It also appears in mathlib4#1754 for the finset version, which is what caused me to notice.

[Eric Wieser]

The new naming convention would also advocate renaming Set.Icc to Set.icc

[Eric Wieser]

So I think the lemma is consistent with the def as is

[Reid Barton]

class AddTorsor (G : outParam (Type _)) (P : Type _) [outParam <| AddGroup G] extends AddAction G P,
  VSub G P where
  [Nonempty : Nonempty P]
  /-- Torsor subtraction and addition with the same element cancels out. -/
  vsub_vadd' : ∀ p1 p2 : P, (p1 -ᵥ p2 : G) +ᵥ p2 = p1
  /-- Torsor addition and subtraction with the same element cancels out. -/
  vadd_vsub' : ∀ (g : G) (p : P), g +ᵥ p -ᵥ p = g

Shouldn't the field name Nonempty be lowercase?

[Ruben Van de Velde]

Should Filter.EventuallyLe be Filter.EventuallyLE?

[Yury G. Kudryashov]

What is the correct Lean 4 name for docs#ennreal.lt_iff_exists_nnreal_btwn?

[Yury G. Kudryashov]

We use NNReal and ENNReal for types.

[Jireh Loreaux]

I think I would follow the "lowercase as a group" convention, and get either ENNReal.lt_iff_exists_nnreal_btwn, or possibly ENNReal.lt_iff_exists_nnReal_btwn

[Jireh Loreaux]

Personally, the latter makes more sense to me.

[Eric Wieser]

I prefer the former slightly

[Thomas Murrills]

I personally prefer the latter but I’m fairly certain the former is what would be consistent with mathlib4 naming, so that’s what I think we should do (an initial group of same-cased letters is (de)capitalized together, with the group taken to be as large as possible)

[Jireh Loreaux]

I don't think "as large as possible" is the correct interpretation. I think it's uppercased letters which are part of a semantic group get lowercased together. For example, if you had something like LEOfFoo (if this were some type) I think it would be camelCased as leOfFoo.

[Jireh Loreaux]

So I picked nnReal because "nonnegative" is a semantic block, whereas "non" isn't, and "nonnegative real" isn't an (atomic) semantic block.

[Thomas Murrills]

That’s my inclination too, but I was told otherwise here. In fact ennReal vs. ennreal was the example being discussed

(I think leOfReal could still be handled differently under this rule because it’s not simply a semantic block but an existing lean name being referenced, and maybe there are component boundaries at name references…either way the rule I gave is indeed not quite correct, though)

[Jireh Loreaux]

I stand corrected, nnreal is consistent.

[Johan Commelin]

We have:

/-- Two elements `x` and `y` are complements of each other if `x ⊔ y = ⊤` and `x ⊓ y = ⊥`. -/
structure IsCompl [PartialOrder α] [BoundedOrder α] (x y : α) : Prop where
  /-- If `x` and `y` are to be complementary in an order, they should be disjoint. -/
  protected Disjoint : Disjoint x y
  /-- If `x` and `y` are to be complementary in an order, they should be codisjoint. -/
  protected Codisjoint : Codisjoint x y

Shouldn't those two fields be lowercase?

[Jireh Loreaux]

the BoundedContinuousFunction file will be available in a while. I propose we take the opporunity while porting to change the name to BoundedContinuousMap. It shortens an already long name, and it agrees with ContinuousMap. Opinions?

[Eric Wieser]

I think it might be easiest to rename it in mathlib 3 where we don't have to replace both the CamelCase and snake_case versions in lemma names

[Jireh Loreaux]

Yeah, there is a slightly tricky bit that it's sometimes abbreviated to bcf, but agreed, easier to make this change in mathlib3

[Pol'tta / Miyahara Kō]

We port linear_independent_theorem to linearIndependent_theorem.
Should we port linear_dependent_theorem to linearDependent_theorem in the same way?

[Eric Wieser]

Seems reasonable to me

[Matthew Ballard]

I couldn't bring myself to do it initially but

structure Cone (F : J ⥤ C) where
  X : C
  π : (const J).obj X ⟶ F
#align category_theory.limits.cone CategoryTheory.Limits.Cone

Should be an x? I was conflicted because (X:C) is everywhere else in the file for a parameter.

[Jireh Loreaux]

IMHO, this is a reasonable place to have an exception to the convention.

[Adam Topaz]

Yeah, I think the upper-case X should remain in this case.

[Matthew Ballard]

One can also complain about the genericity of the field name. Another option is pt

[Adam Topaz]

Have you met docs#category_theory.bundled ?

[Ruben Van de Velde]

How about Hom as a field for categories?

[Adam Topaz]

Hom for cats is a type, so uppercase seems fine to me.

[Matthew Ballard]

That at least has Sort v in the signature

[Adam Topaz]

I don't know... personally I think the new naming convention is not a convention but rather all the conventions

[Kyle Miller]

I don't really understand the rules for Prop-valued fields. According to the wiki, they should be capitalized, but for example docs4#Membership.mem is lower-case.

The wiki's convention leads to the adjacency relation in a simple graph being capitalized like so:

structure SimpleGraph (V : Type u) where
  Adj : V → V → Prop
  symm : Symmetric Adj
  loopless : Irreflexive Adj

What is the justification for this rule?

[Ruben Van de Velde]

I thought props should not be capitalized, as opposed to sorts

[Adam Topaz]

I think if the term has type Sort _ then it's meant to be capitalized, but terms of props are lowercase?

[Adam Topaz]

Again, "all the conventions"

[Kyle Miller]

I was going by item 2 at https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#naming-convention

Would it be OK to make Adj lower-case then?

[Adam Topaz]

Adj x y is a Sort 0, so it should indeed be CamelCase, no?

[Eric Wieser]

Yeah, only things of type p where p : Prop are lowercase

[Eric Wieser]

But indeed Membership.mem doesn't fit this convention, and this has been raised multiple times

[Kyle Miller]

I don't really get why this is how it is for Prop -- if I change Prop to Bool, why should I have to change the capitalization?

[Eric Wieser]

Because you write p : SomeProp but never b : someBool

[Kyle Miller]

That's true, but it doesn't address why that's more important than making Prop and Bool be somewhat interchangeable.

The best justification I can come up with for this is that you're wanting to parallel how it's True <-> true and False <-> false, which is I think a stronger argument than the fact that props have terms.

[Kyle Miller]

But I think it's still a shame that making a change to whether something is a Bool or a Prop entails going through everything and reviewing naming conventions. Hopefully that's relatively rare.

[Mario Carneiro]

Yes, this has also been raised before, and in particular Leo is not interested in changing Membership.mem to match the mathlib4 naming convention for this reason

[Mario Carneiro]

I would just like us to have a convention, I'm not too fussed about the details

[Mario Carneiro]

the compromise proposal was to have structure fields use the lowerSnakeCase convention if they would otherwise be UpperCased for being types

[Mario Carneiro]

The reason this is awkward is that it suggests that a definition wrapping a structure field would be capitalized differently than a structure field directly

[Yaël Dillies]

Eric Wieser said:

Because you write p : SomeProp but never b : someBool

Indeed, but you will most definitely write b : coe_sort someBool at some point.

[Matthew Ballard]

I get value from being able to separate data from proofs from the names themselves. But I am with Mario, in that having a convention with very broad coverage is most beneficial.

[Eric Wieser]

Mario Carneiro said:

the compromise proposal was to have structure fields use the lowerSnakeCase convention if they would otherwise be UpperCased for being types

I'd maybe argue that we don't need to make the compromise, and can just use a different convention in mathlib to what core uses

[Mario Carneiro]

that's also confusing, because people will repeatedly ask this same question

[Mario Carneiro]

it is an option but I'd prefer to have some cohesion here. If we were going to part ways naming convention wise we should have just stuck to snake case everything

[Eric Wieser]

Well, with that compromise you can't know what the name is without first knowing whether it's a projection and therefore knowing the implementation details

[Eric Wieser]

How did we port docs4#CategoryTheory.Bundled ?

[Eric Wieser]

Oh, it's Greek so I guess not relevant

[Matthew Ballard]

Circling back to the concrete question, !4#2337 has its dependencies cleared and should be ready to go except for the naming issue mentioned here.

[Matthew Ballard]

/poll What should the cone point be called?
X
x
pt
other

[Adam Topaz]

apex?!

[Adam Topaz]

apex doesn't really make sense for the cocone point ;)

[Johan Commelin]

that's true

[Johan Commelin]

I guess it would be the coapex?

[Johan Commelin]

https://words.bighugelabs.com/antapex

[Adam Topaz]

whatever name we choose, I think it should be the same for both cones and cocones.

[Adam Topaz]

And my only reasoning for staying with X is muscle memory, which isn't the best argument. I think pt is a very natural choice.

[Matthew Ballard]

Clearly xepa

[Thomas Murrills]

not that it will affect things, but imo being able to read off some basic info from the name itself is great, and the benefit of avoiding capital letters after . seems far less than the benefit of being able to consistently get info about something’s role from its name. conflating terms of types with sort-like terms only when they appear as structure fields is at least a very peculiar rule

[Thomas Murrills]

(but, by my personal preferences, still better than having Props be lowerCamelCase in general)

[Kyle Miller]

Mario Carneiro said:

The reason this is awkward is that it suggests that a definition wrapping a structure field would be capitalized differently than a structure field directly

Speaking of structures, one awkwardness associated to the current naming convention is that there is a difference in capitalization between a term of a type and a term of a type that wraps that type.

For example, with this

structure MyProp where
  P : Prop

you have Q : Prop but q : MyProp. Maybe if there's a coercion from MyProp to Prop you'd still be expected to capitalize Q : MyProp?

[Matthew Ballard]

It looks like pt is it. Incoming soon

[Eric Wieser]

Kyle Miller said:

For example, with this

structure MyProp where
  P : Prop

you have Q : Prop but q : MyProp.

Doesn't this depend whether MyProp : Prop?

[Floris van Doorn]

No, we don't capitalize objects that have a structure as type whether these structures are types or propositions. E.g. we're capitalizing neither docs4#Nonempty.intro nor docs4#Inhabited.default.

[Floris van Doorn]

Oh hey, those linkifiers work! Thanks @Henrik Böving!

[Johan Commelin]

So docs4#IsCompl.Disjoint shouldn't exist, right?

[Reid Barton]

Getting here late but does anyone actually say "point" for this? pt would have been my last choice--ok, it ranks ahead of other.

[Adam Topaz]

I think it's okay ;)
https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/LocallyConstant.20preserves.20colimits/near/236834837

[Alex Keizer]

I wanted to play around with making lints, so I wrote a lint that tries to detect when things are wrongly named (https://github.com/alexkeizer/lean-naming-lint/).

Currently, the output is chock full of definitions like (With all different kind of variations on Ioi, Iio, and some others)

comap_coe_Ioi_nhdsWithin_Ioi

Complaining that Ioi should be lowerCamelCase ioi by the rule that UpperCamelCase names that are part of snake_case names should be spelled as lowerCamelCase.

Is that right, are these names misspelled, or is this an exception?

[Reid Barton]

I was going to say that maybe it makes sense to refer to the extra object of the indexing category as the "cone point", but definitely not its image under the actual functor

[Adam Topaz]

Well, I still think pt is a step up from X.

[Reid Barton]

I mean, statistically the vertex of the cone is more likely to be called $X$ than its "point" :smile:

[Reid Barton]

Anyways, it wouldn't be the first time mathlib makes choices I find strange.

[Jireh Loreaux]

Alex Keizer said:

Is that right, are these names misspelled, or is this an exception?

I think we are keeping Ioi and all its variants capitalized as a special case. So these would need to maybe be added as nolints to whatever linter you are writing.

[Reid Barton]

Reid Barton said:

Getting here late but does anyone actually say "point" for this?

I suggest searching for "_ of the cone" "colimit" for _ = apex, point, tip, vertex

[Yury G. Kudryashov]

Is it true that we use emod for % on integers? If yes, then why?

[Thomas Murrills]

Johan Commelin said:

So docs4#IsCompl.Disjoint shouldn't exist, right?

Looks to me like these fields should have been disjoint and codisjoint under any convention, right? What was the rationale for capitalizing them?

[Eric Wieser]

Should we have a #naming-conventions stream? It looks like there are intermingled discussions here

[Kevin Buzzard]

Probably just a document with explanations, examples and known idiosyncrasies would be good enough

[Kevin Buzzard]

And then when someone asks a question which isn't covered they're encouraged to add to the document

[Thomas Murrills]

We kind of have that on the porting wiki, no? (Maybe it could be more complete, though—and eventually I imagine it should leave the porting wiki anyway.) I think the issue is that there are lots of such questions that keep arising and need to be discussed.

[Mario Carneiro]

Yury G. Kudryashov said:

Is it true that we use emod for % on integers? If yes, then why?

I think this is waiting on the definition change for Int.mod in core

[Arien Malec]

Naming adjudication:

We have an implementation of derangements of a permutation in Combinatorics.Derangements.Basic

mathport ported it as derangements, I overrode to Derangements and Eric's asked me to follow the mathport decision, which follows the strict rules on the wiki. I have no super strong opinion either way, but before I go flip it back, Derangements follows the same naming convention as, for example PNat - it's effectively a hardwired constraint on an existing type, and it's subsequently used "typelike" -- it's functionally a "newtype with constraint"

Compare:

def PNat := { n : ℕ // 0 < n }

def Derangements (α : Type _) : Set (Perm α) :=
  { f : Perm α | ∀ x : α, f x ≠ x }

[Eric Wieser]

Those aren't the same though

[Eric Wieser]

The first is a Type, the second is a Set

[Eric Wieser]

It would be clearer if we'd written def PNat : Type := ... but I guess we didn't do that in mathlib 3 either.

[Eric Wieser]

Are you confusing {x | p x} with {x // p x}?

[Arien Malec]

I understand the difference, but I think of Derangements in this case as being a fixed subtype of Perm -- it's a Set, sure, but the effect is to put a constraint on Perm α

It's also possible I still live in a set theoretical foundations view of the world :-)

[Thomas Murrills]

I think there’s a case to be made for treating sets as types naming-convention-wise, but I also think that would be something we’d want to apply uniformly to all sets (and therefore not a change we’d want to make mid-port at least)

[Arien Malec]

We really get to make this decision once, right? It's going to be a mechanical chore to undo.

If derangements were a function on Perm α, I'd be there, but here we have a function from type to type.

[Thomas Murrills]

Imo the important info you get from the naming convention is the role something can play with respect to other terms. Anything in UpperCamelCase can be on the right side of a : judgment. So the question would be: is ∈ similar enough in role to : to induce similar naming conventions? Do we lose info by enforcing that analogy? And is ∈ prominent enough to warrant a carve-out?

I think these are all questions for after the port and that we shouldn’t make an exception now even for a very Type-like set—because arguably all sets are Type-like in some way :)

[Thomas Murrills]

(I don’t think it’s a function from Type to Type; it’s a function from Type to a Type)

[Eric Wieser]

Right, by this argument Fintype.card should be Fintype.Card, which I've seen no argument for elsewhere

[Eric Wieser]

Arien Malec said:

here we have a function from type to type.

The function from type to type is fun α => coeSort (derangements α)

[Arien Malec]

Thomas Murrills said:

(I don’t think it’s a function from Type to Type; it’s a function from Type to a Type)

derangements it is (again probably a set theoretical bias to see the set of all Perm α such that there are no fixed points as essentially a subtype of Perm α).

[Arien Malec]

Eric Wieser said:

Right, by this argument Fintype.card should be Fintype.Card, which I've seen no argument for elsewhere

That's pretty clearly a function on Fintype :-).

[Eric Wieser]

docs#unitary will fall into a similar naming rule as derangements, I don't know if that's ported yet (docs4#unitary)

[Eric Wieser]

I see where you're coming from with the uppercase, but I think you're really proposing the addition of a special case to the existing convention.

[Thomas Murrills]

Fwiw I do think it’s useful to view it as essentially a subtype in the way you mention, but every set is essentially a subtype of the type used to index it in a similar way, which is why I think there’s some merit to asking whether we want to UpperCamelCase sets—it’s just that this ought to be a general rule instead of an exception for derangements in particular

[Arien Malec]

Eric Wieser said:

I see where you're coming from with the uppercase, but I think you're really proposing the addition of a special case to the existing convention.

That's right -- & we'd have to language lawyer the exact rules.

[Alistair Tucker]

Would it be def Derangement : Perm α → Prop := in uppercase?

[Jireh Loreaux]

Along with docs4#unitary we also have docs4#selfAdjoint I think derangements is the way to go here.

[Eric Wieser]

Matthew Ballard said:

/poll What should the cone point be called?
X
x
pt
other

Is this related to the weirdness in https://github.com/leanprover-community/mathlib4/pull/2931#discussion_r1139150725? Have we accidentally taught mathport to replace all fields named X with pt? cc @Jeremy Tan

[MonadMaverick]

class MeasurableSingletonClass (α : Type _) [MeasurableSpace α] : Prop where
  /-- A singleton is a measurable set. -/
  measurableSet_singleton : ∀ x, MeasurableSet ({x} : Set α)

Should the field be measurable_set_singleton?

[Eric Wieser]

No, the current name is correct

[MonadMaverick]

I guess the reason is that we have "def MeasurableSet [MeasurableSpace α] (s : Set α) : Prop".

But why it's MeasurableSet instead of measurableSet?

def nullMeasurableSet [MeasurableSpace α] (s : Set α)
    (μ : Measure α := by volume_tac) : Prop :=
  @MeasurableSet (NullMeasurableSpace α μ) _ s
#align measure_theory.null_measurable_set MeasureTheory.nullMeasurableSet

def aeDisjoint (s t : Set α) :=
  μ (s ∩ t) = 0
#align measure_theory.ae_disjoint MeasureTheory.aeDisjoint

Should I name them "def NullMeasurableSet ..." and "def AeDisjoint ...."?

The auto translation from mathlib3port did return NullMeasurableSet and AeDisjoint

[Eric Wieser]

Yes, those defs should both be CamelCase because they are Props

[Eric Wieser]

But your original example is a proof so should be lowerCamel_snake

[MonadMaverick]

I see. Thank you!

[Kevin Buzzard]

I am porting a category theory file, and most of the errors made by the autoporter are issues with capitalisation etc coming from the changes in the naming convention. I am fixing them in a mundane way (typically searching for #align's) but this does make me conscious that I really still don't have the first clue about the lean 4 naming convention. Is there a document for dummies which explains it anywhere? (assuming I understand the lean 3 naming convention)

[Mario Carneiro]

https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#naming-convention

[Kevin Buzzard]

Ironically I had just re-read the porting wiki up to not far before that point as preparation for getting back into porting.

[Scott Morrison]

We have decided to keep LE and LT capitalised even in camel case names, right? mathlib4 is currently quite inconsistent, with Le[A-Z] and LE[A-Z] both producing plenty of hits.

[Scott Morrison]

e.g. we have ofMapLEIff (correctly), but linearIndependentFintypeOfLeSpanFintype (incorrect?)

[Ruben Van de Velde]

I think LE/LT was the conclusion, yes, but mathport doesn't know that (yet?)

[Yaël Dillies]

ofMapLEIff looks pretty unreadable, though. Are we sure of that decision?

[Ruben Van de Velde]

I'm not sure if we're sure of anything :)

[Yaël Dillies]

Why is it docs4#Localization but docs4#addLocalization ?

[Eric Wieser]

It's a mistake for sure

[Eric Wieser]

Also, docs4# consuming ? is really annoying

[Yaël Dillies]

Not if you're :flag_france: :stuck_out_tongue:

[Mario Carneiro]

Eric Wieser said:

Also, docs4# consuming ? is really annoying

to be fair, lean identifiers consuming ? is also annoying in many cases

[Eric Wieser]

Changing the linkifier to drop ?s that match \?$ would probably help

[Patrick Massot]

Let's be honest: the English typography idea to remove all spaces before punctuation is just plain wrong.

[Eric Wieser]

Not as bad as the bizarre convention that I refuse to acknowledge with quotes, that "puts a trailing comma here," or a "trailing period."

[Eric Wieser]

I can only hope that the people who think this is a good idea have no intersection with people who add punctuation after equations, to avoid writing
$\frac{x^2+x}{x,}$ or worse

[Mario Carneiro]

What about docs4#Array.back?

[Eric Wieser]

Don't you mean "What about docs4#Array.back??"?

[Yaël Dillies]

For people interested in the names of categories, I have just opened !4#3730 and !4#3731.

[Scott Morrison]

I agree it would be nice to not have unnecessary Cat suffixes, but for now this is what the porting-wiki asks for. Yaël's !4#3730 removes Cat from the end of some order category names, following changes they made in mathlib3 as #18657.

I think it would be good to come up with a consistent rule, and update the decision in the porting-wiki, before proceeding here.

Is "slightly abbreviate the name of the bundled typeclass" enough? e.g.

• the category of bundled Lattices is Lat
• the category of bundled Algebras is Alg

etc. I worry slightly that it is harder for a reader to determine quickly whether they are looking at the unbundled ("we work with elements") or bundled ("we work with morphisms") version, but I think it is okay. I think this naming scheme would be closer to informal conventions.

[Eric Wieser]

I assume using Lᴀᴛᴛɪᴄᴇ (Lᴀᴛᴛɪᴄᴇ for Android users who can't read Unicode in code blocks) as the spelling of the category is a bad idea?

[Scott Morrison]

Is that unicode smallcaps!?

[Jireh Loreaux]

Do those work in idents?

[Jeremy Tan]

Note that not all smallcaps letters are in Unicode, and those that are usually have different styles because they are meant for different purposes. I wouldn't want smallcaps for cat names

[Scott Morrison]

Yes, they render pretty unevenly for me, and are also presumably a pain to type. I would prefer not to use unicode smallcaps!

[Yaël Dillies]

In the case of the order theory category names, the abbreviated names I came up with match what there's on nLab, except Lat which corresponds to our DistLatand Ord which corresponds to our Preord.

[Yaël Dillies]

The "painful to type" can be fixed by adding a \name_of_the_category abbreviation outputting the small caps name for each category we have. But that only fixes it inside VScode, not when looking up lemmas in the docs :sad:

[Mario Carneiro]

yeah I think that the snarky remarks regarding the naming convention will only get worse if a lemma can simultaneously contain upper and lowercase camel case components, snake case, and small caps in the middle, e.g. CategoryTheory.ʟᴀᴛ_dualEquiv_inverse (where of course ʟᴀᴛ is the lowercase small caps form of Lᴀᴛ)

[Joël Riou]

The category of quivers could be named QuiverCat or Quiv, but the current QuivCat is in between, so that changing the name either way would be very much ok for me. As it seems Quiv is in use in the math community, it is probably better. Similarly for other bundled categories, we could see whether there is a very well established category name used by mathematicians, or otherwise fall back to the addition of the suffix Cat to the instance name of the mathematical structure. No fancy Unicode characters please!

[Mario Carneiro]

my guess is that in mathlib3 it was named Quiv and so mathport stuck a Cat on the end

[Yaël Dillies]

Was mathport instructed to add the Cat suffixes? How does it know what's a category and what's not?

[Eric Wieser]

It just looked for TitleCase names

[Eric Wieser]

module.End was auto-translated to Module.EndCat (then fixed manually)

[Yaël Dillies]

Ah right!

[Eric Wieser]

Another hot take; what about calling the category UnbundledTypeclass.Cat, and then having 𝒞 UnbundledTypeclass or similar as notation to refer to the category?

[Yaël Dillies]

That's much longer to type in general. cf the stupidly long category names in LTE.

[Yaël Dillies]

And some categories do not come from bundling typeclasses, so I'm not sure how your approach would handle those. I'm thinking that whether a category comes from a typeclass or not is an implementation detail.

[Mario Carneiro]

actually for bundling typeclasses it would be nice if there was a one-liner to define the category and supporting lemmas

[Mario Carneiro]

I know that there was bundled for doing most of the work but a macro could automate the lemma construction as well

[Adam Topaz]

Mario Carneiro said:

actually for bundling typeclasses it would be nice if there was a one-liner to define the category and supporting lemmas

This should be relatively easy with a macro. I played around with such a thing some time ago. I’ll try to dig it up when I have some computer time.

[Adam Topaz]

A more advanced one liner would also add the various forgetful functors to intermediate bundled categories (like the forgetful functor from Groups to Monoids). I guess for this to be automated one would have to extract some information from the corresponding type class hierarchy. That’s something I haven’t figured out how to do. Mario, do you some feeling for how difficult that would be?

[Yaël Dillies]

What's hard is that we don't want all forgetful functors, but only the direct ones.

[Adam Topaz]

No, I think you want all of them, together with the corresponding lemmas/isoms showing their compatibility w.r.t. compositions of forgetful functors

[Adam Topaz]

Recall that we have this forget_2 class

[Yaël Dillies]

In a hierarchy of $n$ typeclasses, that's $O(n^2)$ forgetful functors and $O(n^3)$ compatibility lemmas. Isn't that too much?

[Adam Topaz]

Ok, maybe not all of them but there should at least be some way of specifying which we want as part of the automation.

[Yaël Dillies]

Yeah that sounds more reasonable. But at least that means we can't hope for the system to come up with them all. We need manual input at some point during the chain.

[Adam Topaz]

Oh yes of course. I was envisioning some command that you have to call manually (with some options)

[Yaël Dillies]

Actually, we might not need those $O(n^3)$ compatibility lemmas if instead we have a tactic that does them all (it basically amount to rewriting with rfl after all).

[Scott Morrison]

Getting back to the actual naming issue for a moment:

Today's porting meeting was initially enthusiastic about just making the change Group → Grp and similarly.

We then worried slightly about what to do with CommRing, with the only viable option seeming to be CRing. (Which is perhaps too short / ambiguous, although I think consistent with the mathematics literature?)

@Alex J. Best then made the very interesting suggestion of just appending an s, hence Groups for the category of bundled Groups, and so on. This matches how mathematics speak these things, although not how they write them. We couldn't think of cases where there is already a trailing s. The fact that there are some categories like Top that we presumably don't want to name this way means that this couldn't be a universal rule.

[Scott Morrison]

Actually, worse than CommRing is of course just Ring.

[Scott Morrison]

I guess Rng is viable, and used in the literature (in fact, GPT4 suggests this when asked "How do mathematicians write the category of rings?" :-)

[Yaël Dillies]

Yeah, I was thinking so too, although we'll need a big warning that its elements do have a unit.

[Scott Morrison]

/poll How to name categories:
Lat, Rng, CRng (CRing?), Grp, Top
Lattices, Rings, CommRings, Groups, (? not sure for Top)

[Yaël Dillies]

I quite like the idea of appending a s, but I would rather do that as a second option after shortening since category names come up in lemma names a lot (at least for my order categories experience of things) and every single character saved here is tens of lines that are saved from the 100 chars limit.

[Scott Morrison]

Do we have an example where appending s would be used, even if shortening was the default?

[Scott Morrison]

@Alex J. Best, in the s scenario, presumably we'd just allow exceptions for e.g. Top?

[Yaël Dillies]

Ring is a good example, if we listen to the non-unital people.

[Yaël Dillies]

In particular, it's not a name that really needs shortening.

[Alex J. Best]

Yeah I'd propose TopSpaces for Top, so indeed some sort of semi-shortened but with the s still

[Yaël Dillies]

BoundedDistribLattice/BoundedDistribLattices however is a mouthful.

[Scott Morrison]

Alex J. Best said:

Yeah I'd propose TopSpaces for Top, so indeed some sort of semi-shortened but with the s still

I'd be a little sad to lose Top, which is pretty ingrained in the literature, I think.

[Jireh Loreaux]

BddDistribLat is the alternative Yaël?

[Yaël Dillies]

BddDistLat rather, but yeah close enough.

[Mario Carneiro]

or BddDLat

[Yaël Dillies]

DistLat has the advantage of already existing in the literature, but I don't feel so strongly about removing the extra three letters.

[Mario Carneiro]

as a metamath aficionado I am an expert at making just barely readable abbreviations for things

[Scott Morrison]

I do prefer Rings over Rng, for sure (even without any regard for the needs of non-unital ring theorists, which I don't actually believe in :-).

[Yaël Dillies]

We should also consider that some category names were already shortened in mathlib, eg docs#NonemptyFinLinOrd (albeit I shortened it, it was already shorter than NonemptyFiniteLinearOrder)

[Alex J. Best]

Scott Morrison said:

Alex J. Best said:

Yeah I'd propose TopSpaces for Top, so indeed some sort of semi-shortened but with the s still

I'd be a little sad to lose Top, which is pretty ingrained in the literature, I think.

Maybe Top could be its own exception indeed then. I'm coming round to Yael's suggestion more. Even in the informal literature we use CGHaus etc.

[Scott Morrison]

I think Yaël's suggestion gives:

• Lat, Rings, CommRings, Grp, Top

for the examples above?

[Yaël Dillies]

I think s for short names that can't meaningfully be shortened does make sense, and for the ones that can be shortened, let's cut them up!

[Yaël Dillies]

Alternatively, CRings or CRing instead of CommRings. Not sure that clashes with anything else.

[Scott Morrison]

I think whatever we do for Ring should be reflected in what we do for CommRing. Hence if Ring becomes Rings, then CommRing must become either CommRings or CRings, but cannot become CRing?

[Yaël Dillies]

Sounds reasonable, yes.

[Scott Morrison]

Okay, if we shorten Comm to C, does that cause problems for $C^*$-rings?

[Scott Morrison]

They will presumably be called CStarRings, so there's no actual clash, just potential difficulty interpreting the C.

[Scott Morrison]

@Kevin Buzzard, do you feel strongly about the difference between CommRings and CRings for the category of commutative rings? (And you aren't allowed to say that we should just drop the C entirely. :-)

[Eric Wieser]

Do people care about the category of CommSemirings?

[Scott Morrison]

I have met a real live person who cared about this category, but it is pretty niche. :-)

[Eric Wieser]

In a more distant hierarchy-builder future, I can imagine also wanting a name for the category of NonUnitalNonAssocSemirings...

[Scott Morrison]

There's a mini industry of trying to do algebraic geometry over (commutative) semirings, hoping to have applications to various positivity questions?

[Kevin Buzzard]

I'm not bothered about any naming conventions, I am happy to just go with anything, I think it's all a bit bikesheddy (just personal opinion)

[Kevin Buzzard]

I'd be happy with GROUP as well

[Jireh Loreaux]

Personally I would keep Comm instead of shortening, just for the sake of clarity.

[Eric Wieser]

One danger with CommRings is it's easy to misread/write as CommRing, which presumably gives confusing errors

[Eric Wieser]

CommRing.s is more visibly different, though also a bit weird

[Scott Morrison]

Clearly we need (X :: C), which asserts that there is a category instance on C available. :-)

[Scott Morrison]

With the possible exception of CommRings, I think we have pretty good agreement that shortening is the preferred default. I will

• go edit the wiki
• merge some of Yael's renaming PRs

[Scott Morrison]

(Now that someone has said the word "bikeshed" we have to stop discussion. :-)

[Yaël Dillies]

We could now discuss specific names. Here are a few I haven't touched in my PRs:

• docs4#MonCat
• docs4#ModuleCat

[Yaël Dillies]

For the first, Mon risks clashing with docs#Mon_, but I guess we had the same clash in mathlib.
For the second, is Mod alright?

[Scott Morrison]

Yes, I think Mon and Mod are great. The clash with Mon_ is "by design", Mon_ C is meant to be read as "monoids in C".

[Scott Morrison]

I think we also have Mod_ A given A : Mon_ C.

[Yaël Dillies]

I cannot find Mod_ but its existence would indeed be a strong proponent for "it's not a bug, it's a feature" (of our naming convention)!

[Scott Morrison]

Maybe that one never made it to a PR, sorry.

[Scott Morrison]

Oh, it is there, but without the _. :-(

[Yaël Dillies]

I will rename it in mathlib, to avoid any porting trouble.

[Scott Morrison]

Oh, I didn't see this.

[Scott Morrison]

#18911

[Yaël Dillies]

Scott Morrison said:

I think Mon and Mod are great.

!4#3730 and !#3731 are now updated to reflect your enthusiasm. But behold of merging both simultaneously because the Mathlib file will conflict, I'm afraid.

[Matthew Ballard]

Anneuax?

[Reid Barton]

If it's not too late to toss in more suggestions: Some books write things like 𝒢roup for the category of groups, etc. I am not a huge fan myself, but it's relatively inoffensive to type at least (and certainly better than unicode small caps)

[Reid Barton]

Isn't Mod the core library name for the class with %?

[Reid Barton]

And similarly for Top? Sorry if these were already pointed out and I missed it

[Jireh Loreaux]

docs4#Mod docs4#Top

[Kevin Buzzard]

TOP? Or is this too Fortran?

[Reid Barton]

It does have a somewhat antique feel but I think it's okay

[Kevin Buzzard]

If we go for TopCat then I will forever think of this

[MonadMaverick]

-- Definition of OuterMeasure
structure OuterMeasure (α : Type _) where
  measure_of : Set α → ℝ≥0∞
  empty : measure_of ∅ = 0
  mono : ∀ {s₁ s₂}, s₁ ⊆ s₂ → measure_of s₁ ≤ measure_of s₂
  unionᵢ_nat : ∀ s : ℕ → Set α, measure_of (⋃ i, s i) ≤ ∑' i, measure_of (s i)

protected def ofFunction : OuterMeasure α := ...
def boundedBy : OuterMeasure α := ...
def inducedOuterMeasure : OuterMeasure α := ...

def infₛGen (m : Set (OuterMeasure α)) (s : Set α) : ℝ≥0∞ := ...

there is no structure or class named OfFunction/BoundedBy/InducedOuterMeasure

Should the name be of_function bounded_by induced_outer_measure?

for infₛGen, the lean 3 name is Inf_gen, should the lean 4 name be infₛ_gen?

[Scott Morrison]

infₛGen is correct. camelCase for defs is the basic rule.

[Scott Morrison]

(The others above are correct as well, inducedOuterMeasure, etc)

[Eric Wieser]

measure_of should be measureOf, right?

[MonadMaverick]

Eric Wieser said:

measure_of should be measureOf, right?

It's measureOf in master. I copied it from my old files.

[Yaël Dillies]

Reid Barton said:

And similarly for Top? Sorry if these were already pointed out and I missed it

So either Tops or maybe Topol?

[Pol'tta / Miyahara Kō]

submodule.fg in Lean 3 is an acronym of "finitely generated", so this should be ported as Submodule.FG following the naming convention.
Indeed, this is ported as Submodule.Fg, and many related definitions like Ideal.Fg are so.
Should we admit Fg as a counter-example of the naming convention?

[Pol'tta / Miyahara Kō]

/poll fg should be ported as
Fg
FG

[Pol'tta / Miyahara Kō]

Henceforth, we port fg to FG. !4#3948

[MonadMaverick]

I am confused about the naming convention.

We changed unionᵢ to iUnion.

Why did we do that?

I think it would be better if we followed the same naming convention as Rust.

In Rust, all structures and classes are PascalCase, and all other identifiers are snake_case.

This would make the code more consistent and easier to read.

Do you think this is a good idea?

[Eric Wieser]

Why did we do that?

See #mathlib4 > sup/Sup. The ᵢ was too hard to distinguish from the subscript s.

[Mario Carneiro]

In Rust, all structures and classes are PascalCase, and all other identifiers are snake_case.

In Lean, local variables and functions are camelCase. Changing this would be a massive refactor at this point

[Eric Wieser]

Do we have a #naming4 yet?

[Jireh Loreaux]

It's on the porting wiki page

[Kevin Buzzard]

Yeah, I think the question was do we have a linkifier to it :-) (it's https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#naming-convention )

[Kevin Buzzard]

I would vote for redirecting #naming . I think Lean 4 is in the lead now. Or maybe we just switch over all the linkifiers at the same time?

[Eric Wieser]

Yeah, I think the question was do we have a linkifier to it

That and promoting it to a more permanent page that isn't just scoped to porting work

[Floris van Doorn]

Shall I make a PR with the following renamings?

infNndist -> infNNDist
infEdist -> infEDist

following the naming convention of ENNReal?

[Chris Hughes]

Does !4#4214 do the right thing. Renaming aemeaurable to aeMeasurable in lemmas?

[Eric Wieser]

Does this mean that lemmas about NNDist should be named things like nnDist_smul?

[Chris Hughes]

I would say so, but maybe I misremembered the convention

[Moritz Doll]

I don't think so, @Jireh Loreaux certainly knows

[Jireh Loreaux]

Uppercased initial collections get lowercased as a group. So SMul becomes smul, and NNDist becomes nndist.

[Eric Wieser]

So to answer @Chris Hughes' question, AEMeasurable becomes aemeasurable not aeMeasurable?

[Floris van Doorn]

Do we agree with the following names?

AEMeasurable
AEStronglyMeasurable
AEStronglyMeasurable.aemeasurable
aestronglyMeasurable_id

There is still an ae_eq in many Lean 4 lemma names. This is a bit of a special case, since ae_eq is not a definition, just notation for filter.eventually_eq, and probably ae_eq is more readable than aeeq inside lemma names...

[Eric Wieser]

aeEq is presumably the other option

[Mario Carneiro]

since ae_eq is not a definition but it is used like one in theorems, I'm also inclined to call it aeEq

[Yaël Dillies]

Yeah, I feel like the cap after the ae shouldn't be lower-cased, so aeEq, aeMeasurable.

[Eric Wieser]

Ah, but the point is that if it were a definition it would be AEEq and so would lowercase as aeeq

[Eric Wieser]

And if we think aeEq is the right name then ENNReal would lowercase to ennReal not ennreal, and SMul to sMul.

[Floris van Doorn]

Eric Wieser said:

Ah, but the point is that if it were a definition it would be AEEq and so would lowercase as aeeq

Yes, that was my thought...

[Mario Carneiro]

I'd prefer not to use this example as motivation to change all the others. frankly having a one off exception sounds better than that, especially if it is in the name of readability

[Mario Carneiro]

I didn't mean that it would be treated as the lowercased version of a definition that doesn't exist, but rather as a non-definition label segment like trans, which could be either snake cased or camel cased

[Yaël Dillies]

I'm with Mario on that one. I see ae as a modifier, just like u, i, c before Icc.

[Eric Wieser]

Well enn is a modifier too...

[Eric Wieser]

The main difference being that uIcc and iUnion etc aren't types, so we don't have to re-case them

[Mario Carneiro]

aeEq isn't a type either IIUC

[Mario Carneiro]

it's just a thing we say on theorems about a.e. equality

[Mario Carneiro]

and I'm also not talking about modifiers like u i which go inside definition names, I mean label fragments that show up in theorem names that are not a symbol reading label, like refl, trans, assoc, comm etc

[Mario Carneiro]

I'm saying we could categorize aeEq as such a label fragment, in which case we have more flexibility on casing it (basically it should consist of 1 or more camel cased components separated by _)

[Jireh Loreaux]

I think we should maintain a list of exceptions to the naming convention, or else write it in the docstring. That way a future person (maybe even one of us) doesn't come along and say: "oh, this is misnamed, PR'd"

[Sebastien Gouezel]

Trying to catch up with the naming convention. Can someone remind me why we have Tendsto with a capital, but interior without a capital?

[Yaël Dillies]

The first is a Sort, the second is not.

[Yury G. Kudryashov]

BTW, should we rename docs#Nat.coprime to Nat.Coprime?

[Ruben Van de Velde]

Wouldn't that mean it's a Sort?

[Kyle Miller]

The rule's not that the constant itself is a Sort, but whether after applying all the arguments you get a Sort

[Kyle Miller]

(and if something is Set-valued, you're supposed to ignore that Set X = X -> Prop, since sets aren't meant to be treated as functions.)

[Yury G. Kudryashov]

E.g., docs#IsOpen is a predicate too.

[Sebastien Gouezel]

I don't really understand how Tendsto is supposed to be a Sort, but I can definitely live with the rule that Prop-valued stuff are capitalized, and Set-valued stuff are not.

[Yaël Dillies]

Tendsto is Prop-valued. Prop = Sort 0. That's all we're saying.

[Kevin Buzzard]

The rule is that types begin with capital letters and terms begin with small letters, apart from functions, where you have to look at the target. Tendsto is a function which takes some inputs and returns a type (or more precisely a Prop) so it's capital.

[Kevin Buzzard]

And the rule doesn't apply for t : Set X because you're not allowed to unfold Set

[Kayla Thomas]

Is this the right document to go by: https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#naming-convention ?
If so, I'm not sure if I follow rule three "Functions are named the same way as their return values (e.g. a function of type A → B → C is named as though it is a term of type C)." in regards to "Tendsto is a function which takes some inputs and returns a type (or more precisely a Prop) so it's capital.". Should the rule read "as though it is type C" instead of "as though it is a term of type C"? For example should I write

def NotFree
  (Γ : List (VarName × MetaVarName))
  (v : VarName) :
  Formula → Prop

or

def not_free
  (Γ : List (VarName × MetaVarName))
  (v : VarName) :
  Formula → Prop

Is there, or is it possible to have, a linter for the naming convention?

[Thomas Murrills]

The first one is right! I think the wording is right too—we want to name NotFree as though it is a term of type Prop, i.e. as though NotFree : Prop. Though, is there a chance the phrase “a is a term of type C” could get interpreted as anything other than a : C? If so maybe we should clarify!

[Kayla Thomas]

If it is a term of type Prop then wouldn't that go to rule 1 "Terms of Props (e.g. proofs, theorem names) are in snake_case."?

[Thomas Murrills]

Hmm, I think that has to do with calling things which have type A simply As. So the phrase “Terms of Props” ~ “Terms of {things a which have type Prop}” ~ “things which have type a, where a has type Prop” ~ “things h where h : a and a : Prop”. Also, in general, “a term of A” means the same as “a term of type A”.

Afaik this lingo is type-theoretically standard but can be confusing…maybe we should stick to a single way to phrase things in the naming conventions/most important docs?

[Thomas Murrills]

(Also, tangent: we should probably move/copy the naming convention into a page called “contribution guidelines” or something like that. I know it’s also in Lean 4 survival guide for Lean 3 users, but this applies to everyone now! :) )

[Kayla Thomas]

Is it possible to make a linter for this?

[Kayla Thomas]

Or to write the guide using some kind of pattern matching on the result of running #check on the expression?

[Thomas Murrills]

A linter would be neat imo! (I’m trying to see if it’s been discussed before…)

[Mario Carneiro]

the logic is already implemented in mathport but not as a linter

[Kayla Thomas]

What would need to be done to turn it into a linter?

[Kayla Thomas]

I should probably learn how to do this kind of programming in Lean.

[Kayla Thomas]

Do I have this right?

lower_snake_case : UpperCamelCase : Prop
lowerCamelCase : UpperCamelCase : Type
UpperCamelCase : A -> B -> Prop
UpperCamelCase : A -> B -> Type

?

[Thomas Murrills]

Yup! :) (And the first two naming conventions there also ignore initial A → B → …’s, as well—e.g. lower_snake_case : A → B → UpperCamelCase, where UpperCamelCase : Prop)

[Kayla Thomas]

Thank you!

[Kayla Thomas]

Ie,

UpperCamelCase : Prop
UpperCamelCase : Type
lower_snake_case : (UpperCamelCase : Prop)
lowerCamelCase : (UpperCamelCase : Type)
UpperCamelCase : A -> B -> Prop
UpperCamelCase : A -> B -> Type
lower_snake_case : A -> B -> (UpperCamelCase : Prop)
lowerCamelCase : A -> B -> (UpperCamelCase : Type)

?

[Thomas Murrills]

Yup! The rule is that h : Foo should always be named the same way as h' : A → Foo, no matter what Foo is. Arguments/hypotheses don’t affect naming.

[Kayla Thomas]

Thank you!

[Jireh Loreaux]

What is the status of the naming convention regarding terms of type List.TFAE? Per the naming convention, I would expect them to be lowercase, but @Anatole Dedecker pointed out that we have both docs#t1Space_TFAE and docs#IsGalois.tfae. Do we have an exception for this, or do we want to make one, or just go with tfae?

[Anatole Dedecker]

(I think currently we even have more instances of TFAE, but that shouldn't have any importance)

[Yaël Dillies]

Surely docs#Filter.limsSup should be Filter.sLimsup? It currently reads as lims + sup.

[Jireh Loreaux]

And leave docs#Filter.limsup alone, correct?

[Yaël Dillies]

Yes. Another option would be to also rename limsup to iLimsup, but I think that's unnecessary.

[Ruben Van de Velde]

Jireh Loreaux said:

What is the status of the naming convention regarding terms of type List.TFAE? Per the naming convention, I would expect them to be lowercase, but Anatole Dedecker pointed out that we have both docs#t1Space_TFAE and docs#IsGalois.tfae. Do we have an exception for this, or do we want to make one, or just go with tfae?

Seems like we have six of one, half a dozen of the other. How about a poll?

[Ruben Van de Velde]

/poll What should the naming convention be?
tfae
TFAE
tFAE

[Kyle Miller]

Doesn't the naming convention indicate that "TFAE" should be capitalized because it's Prop-valued?

[Eric Wieser]

@Kyle Miller, I think the question is how it should be used in lemmas that are of the form theorem foo : List.TFAE [X, Y, Z]. I don't think the proposal is to rename docs#List.TFAE itself.

[Martin Dvořák]

Oh. Then I change my vote to tfae only.

[Ruben Van de Velde]

Exactly, thanks for clarifying Eric

[Yuyang Zhao]

Currently we have docs#SetTheory.PGame.leLfDecidable

def leLfDecidable : ∀ (x y : PGame.{u}) [Short x] [Short y], Decidable (x ≤ y) × Decidable (x ⧏ y)

docs#SetTheory.PGame.Lf should be renamed to SetTheory.PGame.LF, then

[Yuyang Zhao]

/poll leLfDecidable should be renamed to
leLFDecidable
lelfDecidable

[Alistair Tucker]

I want to port my project respecting the new naming conventions but am confused by the example

-- follows rules 2 and 6
class LT (α : Type u) where
  lt : α → α → Prop -- follows rule 4 and 6

where said rules are:
2) Props and Types (or Sort) (inductive types, structures, classes) are in UpperCamelCase.
4) All other terms of Types (basically anything else) are in lowerCamelCase.
6) Acronyms like LE are written upper-/lowercase as a group, depending on what the first character would be.

However there is also rule 3 which should in theory have priority over rule 4?
3) Functions are named the same way as their return values (e.g. a function of type A → B → C is named as though it is a term of type C).

Then

-- follows rules 2 and 6
class LT (α : Type u) where
  LT : α → α → Prop -- follows rule 3 and 6

[Eric Wieser]

This is because LT (and docs#Membership) are in Lean core, and are not subject to mathlib's naming conventions

[Eric Wieser]

Core appears to have it's own "things in a structure / class are never UpperCamelCase" rule that conflicts with mathlib's rules.

[Eric Wieser]

Some previous discussion on that point:

Mario Carneiro said:

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.

Kyle Miller said:

I don't really understand the rules for Prop-valued fields. According to the wiki, they should be capitalized, but for example docs4#Membership.mem is lower-case.

[Alistair Tucker]

Thanks! But even in Mathlib.Logic.Basic we have things like

theorem dec_em' (p : Prop) [Decidable p] : ¬p ∨ p := (dec_em p).symm

Shouldn't p be uppercase here?

[Eric Wieser]

Yes, but I think we're pretty lazy about naming conventions when it comes to naming hypotheses

[Eric Wieser]

I'd be happy to merge a PR that upper-cases all the Prop arguments in that file

[Eric Wieser]

But it's probably not the best use of your time!

[Eric Wieser]

Naming matters most for the things that people need to be able to guess the name of; and you very rarely need to guess the name of a hypothesis.

[Alistair Tucker]

I do think that if LT/lt doesn't actually conform to Mathlib naming conventions then it probably shouldn't be used as an example on the Mathlib naming conventions page!

[Eric Wieser]

A PR to fix that sounds like a much better use of your time!

[Eric Wieser]

Oh no, docs#Dvd.dvd has the same problem... (and isn't in core)

[Jireh Loreaux]

I think there are probably a lot of these discrepancies.

[Mario Carneiro]

I would go so far as to say that local variables in definitions don't follow the usual naming convention for declarations, they have their own thing (mostly TBD). For programming, this basically means using lowercase camel case for variable names

[Mario Carneiro]

but mathlib has a bunch of additional stuff about names of types denoting rings etc

[Eric Wieser]

Do you think docs#Dvd.dvd should be renamed? As it's not in core, we have the power to rename it

[Kevin Buzzard]

Then we'll just have people saying "Why is it Add.add but Dvd.Dvd?" which is probably worse.

[Mario Carneiro]

It would cause naming conflicts with the parent class to have Dvd.Dvd. In the similar case of subset we used HasSubset.Subset to address this

[Mario Carneiro]

Kevin Buzzard said:

Then we'll just have people saying "Why is it Add.add but Dvd.Dvd?" which is probably worse.

At least in this case we have a coherent and documented answer for the 'why' question though

[Kevin Buzzard]

Yeah but it's also a pretty crap answer: why should a mathematician care about what is in core and what is not?

[Mario Carneiro]

no I mean the 'read the naming convention' answer

[Mario Carneiro]

Add.add is following the conventions

[Mario Carneiro]

LE.le and Membership.mem are not

[Mario Carneiro]

because Add.add returns a value in an arbitrary type aka "data", while Dvd.dvd returns a Prop

[Kevin Buzzard]

Oh yes of course!

[Yaël Dillies]

Why not just HasDvd?

[Eric Wieser]

Mario Carneiro said:

It would cause naming conflicts with the parent class to have Dvd.Dvd.

Why is there a conflict?

[Mario Carneiro]

if one of them is open or exported then you can't refer to them separately

[Mario Carneiro]

for notation typeclasses it is not uncommon to export them

[Michael Rothgang]

Should docs#LocalHomeomorph.eq_of_eq_on_source_univ be renamed to eq_of_eqOnSource_univ? Note that the hypothesis includes an EqOnSource hypothesis (it's not an equality of functions on some set).

Same question for docs#LocalEquiv.eq_of_eq_on_source_univ.

[Patrick Massot]

Yes.

[Michael Rothgang]

Will PR later today (unless objections come up).

[Michael Rothgang]

Filed as #8121

[Michael Rothgang]

How to name lemmas containing a hypothesis of the form IsOpen s? Currently, mathlib mixes of_open and of_isOpen; @sgouezel suggested I use the latter in #8057. In my understanding,

• "of_isOpen" matches naming conventions on the nose (the definition is called IsOpen, after all)
• at first sight, "preimage_open_of_open" reads nicer to me than "preimage_isOpen_of_isOpen" (but I certainly can get used to both)

Is a PR to rename all these welcome? (Right now, mathlib has only 47 lemmas named like this, so it wouldn't be a huge PR.)

[Michael Rothgang]

Same question for IsClosed, IsCompact, IsSigmaCompact, IsNowhereDense, etc.

[Ruben Van de Velde]

How many of those other examples? :)

[Michael Rothgang]

Loogle counts 43 hits for "of_closed", at least one false positive, 44 hits for "of_compact" (with some being definitely false positives and fine).
I get 30 hits for "of_bounded" (unverified), IsSigmaCompact is all fine; 3 for "IsNowhereDense".

[Kevin Buzzard]

I think preimage_isOpen_of_isOpen reads very nicely!

[Floris van Doorn]

I am strongly in favor of normalizing all these names to use isOpen. It is super annoying to remember which lemmas are named wrong to shorten them.
The name of something like docs#ContinuousOn.preimage_open_of_open is a mess: it doesn't even mention inter in the name. I would go for ContinuousOn.isOpen_inter_preimage (and only add of_isOpen if needed to disambiguate with another lemma).

[Floris van Doorn]

docs#TopologicalSpace.Closeds.closed should also be renamed to TopologicalSpace.Closeds.isClosed.

[Ruben Van de Velde]

(isOpen certainly reads nicer than is_open would have done)

[Floris van Doorn]

For LFTCM 2024 we should do a name-parsing pubquiz. You get a mathlib lemma name, and you have to guess the statement of the lemma.

[Michael Rothgang]

#8229 does the first ten lemma names for "isOpen" (all about (f)deriv). More to follow tonight.

[Kevin Buzzard]

Floris van Doorn said:

For LFTCM 2024 we should do a name-parsing pubquiz. You get a mathlib lemma name, and you have to guess the statement of the lemma.

I have thought about doing this for my course too. I don't see why it should be LFTCM 2024, I think it should be up on the community website, should be large, and should start with some easy ones and then attempt to teach some principles with later questions. And it should go in both directions: statement -> name and name -> statement. Anyone fancy taking this on?

[Michael Rothgang]

I went over all lemmas with "of_open" in their name and renamed as appropriate. Pushed all of those to #8229. I appreciate ideas on a better name for continuousOn_isOpen_of_generateFrom; I find the current name somewhat confusing.

[Michael Rothgang]

New question: do we prefer "of_open_cover" or "of_openCover"?

[Ruben Van de Velde]

Is it about something called OpenCover?

[Michael Rothgang]

No, docs#T0Space.of_open_cover is not - so it should be "of_open_cover", right?

[Ruben Van de Velde]

Exactly

[Yaël Dillies]

Well, we can make non-definitions be atomic names in the grand (naming) scheme of things. But this decision has to be recorded somewhere in the documentation.

[Michael Rothgang]

#8492 has three more renames

[Ruben Van de Velde]

def addNsmul (δ : α) (n : ℕ) : Icc a b := projIcc a b h (a + n • δ)

Should this be addNSMul?

[Junyan Xu]

Nsmul appears 14 times while NSmul only appears in the definition of the class once
image.png

[Ruben Van de Velde]

Looks like to_additive agrees with the capitals, though

[Junyan Xu]

Sorry, it seems NSMul does appear a lot more times (38):
image.png
image.png
I searched the wrong capitalization NSmul (and there's one result in to_additive)

[Junyan Xu]

Let me fix it in a subsequent PR (about homotopy lifting); it's not very likely it will get used elsewhere soon, so no rush I guess...

[Yury G. Kudryashov]

I found out that we have docs#fkg. IMHO, this (and some other names in that file) contradicts our naming convention. @Yaël Dillies

[Yaël Dillies]

What do you think it should be? The statement is longish.

[Yury G. Kudryashov]

At least, it should be longer than 3 letters.

[Yury G. Kudryashov]

E.g., fortuinKastelynGinibre is better than fkg.

[Yury G. Kudryashov]

BTW, it would be nice to have an explanation why (hμ : ∀ (a b : α), μ a * μ b ≤ μ (a ⊓ b) * μ (a ⊔ b)) is a natural condition and what functions μ satisfy it (other than constants).

UPD: same applies to ∀ (a b : α), f a * g b ≤ f (a ⊓ b) * g (a ⊔ b).

[Yury G. Kudryashov]

At least, fortuinKastelynGinibre is good until you formalize another theorem by the same 3 authors.

[Yury G. Kudryashov]

... and since docs#holley mentions only 1 author, it has chances to hit this condition earlier.

[Damiano Testa]

Should the convention also include that author names are either all capitalized or all non-capitalized? fortuin, Kastelyn, Ginibre seems a little sad for fortuin...

[Eric Wieser]

resultOfFortuinKastelynGinibre?

[Damiano Testa]

Eric Wieser said:

resultOfFortuinKastelynGinibre?

Better.

le_of_FortuinKastelynGinibre :stuck_out_tongue_wink:

[Eric Wieser]

Ah, but you're not allowed to have a capital letter after an underscore

[Damiano Testa]

I like so many things about Lean 4, but I find it very hard to take seriously the capitalization conventions...

[Eric Wieser]

So apparently does lean4 itself, given lean4#1897 :upside_down:

[Damiano Testa]

I think that we should consider porting Lean 4 to lean_four. :lol:

[Kevin Buzzard]

Eric Wieser said:

So apparently does lean4 itself, given lean4#1897 :upside_down:

Did we ever hear an explanation about the related lean4#3155 ?

[Ruben Van de Velde]

leanFour?

[Eric Wieser]

I hadn't noticed lean4#3155 being closed, cc @Mario Carneiro and @Scott Morrison

[Kevin Buzzard]

Re the fkg discussion: I guess what's going on is that humans also have a capital letter convention, and lean's convention goes against it sometimes. However should we really be naming theorems after their authors? I think Fermat and Riemann might already be namechecked in mathlib but it's not clear that this should be scaling...

[Mario Carneiro]

I don't know anything about lean4#3155

[Mario Carneiro]

Is fortuinKastelynGinibre a definition?

[Mario Carneiro]

because if it's a theorem then the naming convention is to use fortuin_kastelyn_ginibre

[Ruben Van de Velde]

Yeah, it's a theorem docs#fkg

[Eric Wieser]

Mario Carneiro said:

because if it's a theorem then the naming convention is to use fortuin_kastelyn_ginibre

I thought this rule only applied if fortuin, kastelyn, and ginibre were separate parts of the theorem

[Eric Wieser]

Because otherwise you pretend that you have FortuinKastelynGinibre : Prop, and so the proof is morally fortuinKastelynGinibre : FortuinKastelynGinibre

[Mario Carneiro]

it also applies if the theorem is not being named using symbol-reading, including things like trans or antisymm but also "named theorems" like banach_tarski

[Mario Carneiro]

I think your rule would only apply if FortuinKastelynGinibre was a literal definition

[Mario Carneiro]

most of our theorems are symbol-reading names so this rule doesn't get a lot of exercise

[Mario Carneiro]

although I think we overdo it in many places

[Eric Wieser]

I think we have a handful of theorem names in mathlib that suggest a def / abbrev literally exists when in fact we are just pretending

[Mario Carneiro]

true, there are "patterns" like 0 <= x that get special names

[Mario Carneiro]

but those are recurring patterns, not named theorems

[Mario Carneiro]

(besides this, using camel case in this situation is clearly the unpopular option so I don't think we should bend over backwards to find an interpretation which requires it)

[Mario Carneiro]

the naming convention is not designed to be obnoxious

[Kim Morrison]

Eric Wieser said:

I hadn't noticed lean4#3155 being closed, cc Mario Carneiro and Scott Morrison

Leo expressed his lack of enthusiasm for that PR: mostly because it was not important, and minorly because he disagreed with the actual change.

[Eric Wieser]

and minorly because he disagreed with the actual change.

Was there any elaboration on this? Can we adjust #naming in a way that aligns with Leo's heuristics for the current names being correct?

[Kim Morrison]

Just that congrArg is atomic: it is not built out of congr and arg.

[Mario Carneiro]

ah, so basically the same argument eric was making above

[Kim Morrison]

Indeed.

[Eric Wieser]

So should we deprecate docs#congr_arg and rename docs#DFunLike.congr_arg ?

[Kim Morrison]

I guess we could!

[Ruben Van de Velde]

And congr_fun? And the ones with \2?

[Eric Wieser]

How does this fit with things like docs#forall_congr_prop ?

[Eric Wieser]

Perhaps arg and fun are special, as they are not symbol reading in the same way that "prop" is

[Damiano Testa]

I feel like this ball is rolling the opposite way that I imagined... :face_palm: :upside_down:

[Yaël Dillies]

I agree. congr_fun really is made of congr and fun ad is not atomic.

[Eric Wieser]

do you have another example where fun is obviously atomic?

[Yaël Dillies]

docs#isEmpty_fun, docs#Nat.card_fun, docs#isOpen_ne_fun

[Damiano Testa]

apply_fun? docs#mem_span_range_iff_exists_fun

[Yaël Dillies]

The tactic? We're looking for lemma names.

[Jireh Loreaux]

I don't see how this could be read as a single atom. There's a theorem called docs#congr, and we specialize to the case when the arguments coincide to get congr_fun (congruence for functions), and we specialize to the case when the functions coincide to get congr_arg (congruence for arguments).

[Jireh Loreaux]

Moreover, I think the time we most frequently abuse the "single atom" rule for lower camel case is where there is an existing def, but some additional information causes it to have a more common name.

[Jireh Loreaux]

That is the case for nonneg (the existing defs are LE.le and Zero.zero), but also for things like docs#LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot' where the Complement but doesn't actually appear in the name of the def. Likewise there was a recent discussion surrounding things like ClosedUnitBall (or variants thereof).

[Kim Morrison]

Consistency is a good thing, but it cuts both ways here. Even if you think congr_arg is consistent with a naming scheme, it seems very likely that the not-downstream-of-Mathlib part of the Lean world will be using congrArg. I think that this sort of consistency is quite important.

[Eric Wieser]

Scott, docs#congr_arg and docs#congr_fun are in Std not Mathlib, so I don't know if that is true; and I don't know if we care much about the not-downstream-of-Std bits of Lean

[Jireh Loreaux]

Scott, I agree that consistency is important, although Eric's comment suggests we already have the issue that non-Mathlib users could potentially be using either spelling.

[Jireh Loreaux]

The issue is that we should at least be consistent in a way that makes sense to the most users, and from what I can tell (at least without an explicit poll), congr_arg makes more sense to people than congrArg, even after the explanation. That being said, maybe I'm wrong (we haven't taken a poll), and core devs can choose to ignore the result either way. I'm just saying that we should support the thing users expect.

[Mario Carneiro]

I definitely don't like the notion that Leo's slight preference should override the community here (assuming that polls or otherwise show it is actually preferred). I'm okay with the BDFL model to some extent but Leo has been very clear about not wanting to create or defend a naming convention and generally avoids such discussions whenever possible, so this isn't an area I think we should defer to him on.

Of course everyone has their aesthetic preferences, but the naming convention is trying to do more than reflect one person's taste, it's also supposed to convey additional information and be a readability and searching aid. My impression has always been that Leo finds naming discussions to be a detractor from more important things, which is why it seems difficult to make progress with those renaming PRs.

[Mauricio Collares]

(Off-topic: PHP's function naming rationale, for people who haven't heard of it: https://news-web.php.net/php.internals/70691)

[Kim Morrison]

A question about naming of eq lemmas. Do we have generic advice (I coudn't see such in #naming) about whether/when the RHS of an eq lemma should be part of the name.

My feeling is "only if needed to disambiguate amongst multiple lemmas with the same LHS, or if the RHS is sufficiently inobvious" which isn't super precise.

But I would still like to decide whether there is a default of "no, if the RHS is obvious and unambiguous".

[Jireh Loreaux]

The closest thing we have in #naming to this is:

Often the name of theorem simply describes the conclusion. If only a prefix of the description is enough to convey the meaning, the name may be made even shorter.

So, I think your interpretation is correct, even up to the default "no, if the RHS is obvious and umambiguous". (Reason: the default is to prefer short names, and if the naming convention allows for it, then we'd prefer the shorter LHS-only, versus the longer LHS_eq_RHS.)

[Eric Wieser]

If the lemma doesn't have an obvious direction, LHS_eq_RHS is often better, since its much easier to find for someone searching for RHS

[Eric Wieser]

(eg sub_eq_iff_eq_add etc)

[Mario Carneiro]

IMO this is a good use for alias

[Michael Rothgang]

Should lemma names use setIntegral_foo_bar or set_integral_foo_bar? (About the objects defined in Mathlib/MeasureTheory/Integral/SetIntegral.lean.) Mathlib currently has both (but mostly the latter).

[Eric Wieser]

Is docs#setIntegral a thing?

[Yury G. Kudryashov]

There is no definition setIntegral but we can put this name on the notation.

[Ruben Van de Velde]

Thoughts?

Complex.re_ofNat (n : ℕ) [inst✝ : Nat.AtLeastTwo n] : (OfNat.ofNat n).re = OfNat.ofNat n
IsROrC.ofNat_re.{u_1} {K : Type u_1} [inst✝ : IsROrC K] (n : ℕ) [inst✝¹ : Nat.AtLeastTwo n] :
  IsROrC.re (OfNat.ofNat n) = OfNat.ofNat n

[Mario Carneiro]

std uses the "prefix convention" (re_ofNat), but this is not universally popular

[Yaël Dillies]

re_ofNat it should be

[Mario Carneiro]

I'm not sure we have anything in the naming convention specifically addressing this issue

[Yaël Dillies]

Use of dot notation should not change the name of a lemma. If it's not yet in #naming, it should be

[Mario Carneiro]

#naming actually contains a counterexample:

theorem MonoidHom.toOneHom_injective [MulOneClass M] [MulOneClass N] :
  Function.Injective (MonoidHom.toOneHom : (M →* N) → OneHom M N) := sorry

[Yaël Dillies]

This falls under a different rule, namely that adjective predicates can be put last

[Mario Carneiro]

As a descriptive matter, I don't think mathlib follows the prefix convention much

[Mario Carneiro]

might be good to get data on this though

[Mario Carneiro]

I think the honest answer is that we are not consistent about it

[Ruben Van de Velde]

I suspected as much

[Ruben Van de Velde]

Mathlib/Algebra/Lie/Submodule.lean:theorem injective_incl : Function.Injective N.incl := Subtype.coe_injective
Mathlib/Algebra/Module/Submodule/LinearMap.lean:theorem injective_subtype : Injective p.subtype :=
Mathlib/Algebra/Tropical/Basic.lean:theorem injective_trop : Function.Injective (trop : R → Tropical R) :=
Mathlib/Analysis/BoxIntegral/Box/Basic.lean:theorem injective_coe : Injective ((↑) : Box ι → Set (ι → ℝ)) := by

[Mario Carneiro]

In the case of re_ofNat, I tend to think that the prefix convention gets the wrong answer, because re is a projection so there is more information being provided by the ofNat part than the re part. In autocomplete it's not that useful to see all of the functions I can take the real part of

[Yaël Dillies]

I think it's particularly useful here in that you don't know whether it will ofNat, nat_cast or natCast

[Ruben Van de Velde]

Would that rule also apply to IsROrC?

[Mario Carneiro]

what I just described is not a rule, it's an observation of a downside of the prefix convention applied to this example, and yes it also applies to IsROrC

[Mario Carneiro]

Yaël Dillies said:

I think it's particularly useful here in that you don't know whether it will ofNat, nat_cast or natCast

Those are different functions though (well the first two at least). 2 and 3 are just another instance of naming inconsistency

[Mario Carneiro]

but you "should" know in advance whether you want ofNat or natCast

[Kim Morrison]

Mario Carneiro said:

In the case of re_ofNat, I tend to think that the prefix convention gets the wrong answer, because re is a projection so there is more information being provided by the ofNat part than the re part. In autocomplete it's not that useful to see all of the functions I can take the real part of

This has always been my complaint about the prefix convention. I would love to get to consistency here, but I'm genuinely unsure which I prefer.

[Eric Wieser]

injective isn't a good example here, because #naming specifically prescribes a set of rules for Function.Injective that go against the usual rules

[Eric Wieser]

Mario Carneiro said:

In autocomplete it's not that useful to see all of the functions I can take the real part of

I don't understand this argument, autocomplete will only tell you this if you start typing re anyway. You can still find the lemma by typing ofNat first:

image.png

[Mario Carneiro]

that's true, but I don't think this was always the case, plus it appears that even in that example prefixes are given precedence over arbitrary substring matches

[Eric Wieser]

In this case the first two prefix lemmas (docs#Complex.ofNat_arg, docs#Complex.ofNat_log) are misnamed anyway

[Eric Wieser]

Complex.ofNat_log isn't even the statement I expected after accounting for that misnaming

[Michael Rothgang]

Today's unexpected naming (to me): why do we have docs#ContMDiff.prod_mk but docs#ContDiff.prod? They seems to be perfectly analogous to me.

[Floris van Doorn]

Yes, this is an inconsistency that should be unified.
This one runs pretty deep, e.g. docs#ContinuousAt.prod vs docs#Continuous.prod_mk.
I personally prefer prod_mk, but I'm also fine with making a poll or going for the one that is used most (I think prod_mk, but I'm not sure). They should definitely all be unified.

[Michael Rothgang]

I just checked: apparently, there are 35 lemmas or theorems named prod_mk and 228 named prod. (Double-checking these numbers now; my methodology is a bit hacky.)

[Michael Rothgang]

Some grepping points in a similar direction: if anything, prod_mk (or even ProdMk) is the minority.

[Yaël Dillies]

I do think it should be prodMk

[Timo Carlin-Burns]

Is the rationale for prodMk that we are referring to the definition Prod.mk and dotted declarations should be referred to by their full name in camelCase?

[Richard Osborn]

There are a lot of lemmas that only refer to an element of the type X×Y instead of the pair (x,y). I would guess those only need prod and not prod_mk.

[Yaël Dillies]

Yes, you are both exactly right

[Michael Rothgang]

I just searched around a bit: the current naming is presumably organically grown, i.e. a slight mess.

• should it be prod, prod_mk or prodMk?
• should it be prod_mk_left or prodMkLeft or inl?

[Michael Rothgang]

(I don't care about the outcome, as long as we find one.)

[Michael Rothgang]

I hear you propose "it should be prod when refererring to an element of type X\times Y, and prod_mk/prodMk when referring to a pair (x,y).

[Yaël Dillies]

• prod or prodMk, depending on whether it's x : α × β or (a, b) : α × β
• prodMkLeft or inl both sound fine ( but the latter could be confused with docs#Sum.inl)

[Michael Rothgang]

So prod_mk is a Lean3-ism and should be renamed away from?

[Yaël Dillies]

Note that we are currently having the same conversation about nat_cast: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/naming.20conventions.3A.20natCast.20vs.20nat_cast

[Michael Rothgang]

Side question: #naming still mentions balland bex- should this be removed, in light of #10816? (Does this need wider consensus first? In any case, there are a few lemmas still using the old convention.)

[Timo Carlin-Burns]

Michael Rothgang said:

• should it be prod_mk_left or prodMkLeft or inl?

In my mind these two have distinct meaning. prodMk_left refers to $x \mapsto (x, y)$ for a constant $y$, whereas inl refers to $x \mapsto (x, 0)$, i.e. the natural inclusion homomorphism into the product docs#AddMonoidHom.inl

[Yaël Dillies]

Yes, please do, Michael

[Yaël Dillies]

Also, what lemmas are you thinking of? I meant to have caught them all

[Michael Rothgang]

Yaël Dillies said:

Also, what lemmas are you thinking of? I meant to have caught them all

#11615 has what are probably the last stragglers. (It's hard to audit all lemmas mentioning "ball" :zany_face:)

[Michael Rothgang]

Submitted https://github.com/leanprover-community/leanprover-community.github.io/pull/455 for the naming convention change; comments welcome.

[Eric Wieser]

Michael Rothgang said:

So prod_mk is a Lean3-ism and should be renamed away from?

There is still a mostly-tied pair of polls in progress about this

[Patrick Massot]

I remember from the sphere eversion project time that those lemma names are a mess. Making them consistent would be really nice. I don’t care which version is chosen.

[Yury G. Kudryashov]

I've just noticed that docs3#list.length_enum became docs#List.enum_length on its way from Mathlib to std4#363. @Scott Morrison Is it intentional?

[Kim Morrison]

This change was wrong, sorry.

[Kim Morrison]

If anyone is feeling authoritative on names, #10098 could do with some advice. The problem here is identifiers ending with _, which wreaks havoc with the "camelCasesDefs" rules. :-)

[Yaël Dillies]

Oh no, I see the issue. Category theory was a mistake.

[Sébastien Gouëzel]

Identifiers ending with _ look like a nightmare for naming convention. Would it make sense to have Mon- instead (or substitute whatever character you like more instead!)

[Eric Wieser]

What's used in literature here?

[Kim Morrison]

\mathsf?

[Kim Morrison]

Either something like Mon C or Mon_C, I guess. This is why we originally went with Mon_ C (and to disambiguate from Monoid, etc, although in this specific case it is fine).

[Eric Wieser]

I assume you mean $\mathsf{Mon}_C$? and not a literal underscore?

[Eric Wieser]

IsCategoryTheory.Monoid along with Mon[C] notation (or similar) remotely reasonable?

[Damiano Testa]

I see the GetElem issue coming back...

[Mitchell Lee]

Here's a theorem that states that the length of a reflection in a Coxeter group is odd. (See #11466.)

example {B : Type*} {W : Type*} [Group W] {M : CoxeterMatrix B}
  {cs : CoxeterSystem M W} {t : W} (ht : cs.IsReflection t) :
  Odd (cs.length t) := by sorry

One reviewer suggested the name CoxeterSystem.IsReflection.odd_length, and another reviewer suggested CoxeterSystem.IsReflection.length_odd. Which better fits with the naming conventions?

[Mitchell Lee]

(Thanks @Johan Commelin and @Ruben Van de Velde for the feedback.)

[Yaël Dillies]

odd_length is slightly better

[Kevin Buzzard]

Isn't there a rule for this? I thought odd_length was canonical.

[Yaël Dillies]

Yes but it conflicts with odd being an adjective prop, meaning it can be used as a suffix (like injective, inj, mono, ...)

[Eric Wieser]

I don't think that adjective rule is written down anywhere?

[Yaël Dillies]

Then we should write it down

[Markus Himmel]

The special case of the adjective rule for injective appears in #naming

[Eric Wieser]

Right: there's no indication this was intended to be a general rule

[Yaël Dillies]

It also applies to mono/monotone however

[Richard Copley]

neg_pos x (for rewriting "negative of x is positive", (· > 0) (- x)) is another example with the adjective on the right.

[Richard Copley]

And lt_zero_neg would be a strange name indeed for its friend neg_lt_zero.

[Ruben Van de Velde]

lt is an infix operator so goes in the middle

[Richard Copley]

It would be a shame to break up the neg_pos, neg_nonpos, neg_lt_zero, neg_nonneg family.

[Daniel Weber]

The name of some polynomial theorems, for example docs#Polynomial.sum_over_range, are a bit strange - I'd expect something like Polynomial.sum_eq_sum_range_coeff. What is the reasoning behind it?

[Ruben Van de Velde]

Not sure there is any; you might look at git blame

[Daniel Weber]

It was added in mathlib#3243 , there's nothing about the name there.

[Riccardo Brasca]

I think it is just a mistake, you probably would spend more time in trying to understand what happened than opening a PR fixing it :smile:

[Jireh Loreaux]

In Lean 3, we had only dot notation (a.k.a. generalized field notation). This meant that sometimes things wouldn't actually get namespaced unless they had an argument with that type. For example, docs#isSelfAdjoint_one. However, in Lean 4, we have the usual dot notation as in Lean 3, but we also have what I'll call the expected type dot notation, where if the expected type is known and matches the namespace of the declaration, you can omit the prefix. So, for instance, if docs#isSelfAdjoint_one were renamed to IsSelfAdjoint.one (and of course, protected), then we could write .one with a goal of IsSelfAdjoint (1 : R).

So, should we do this in general? I'm not proposing to try to find all occurrences of things like this, but should we allow / encourage these kinds of renames?

[Eric Wieser]

I'd be weakly in favor of switching to this kind of naming

[Yaël Dillies]

Same here. I have concerns about discoverability and expectability (I have observed quite a few new potential name clashes if we were to switch over), but it does like a principled approach with clear benefits.

[Jireh Loreaux]

Certainly if we do this we'll need to be careful about protecting appropriate declarations.

[Andrew Yang]

I agree that mathlib is lacking on protecting lemmas. Especially the ones that clash with defs in the root namespace.

[Mario Carneiro]

we could have a linter for that

[Jireh Loreaux]

FYI: I just asked @Damiano Testa to write such a linter earlier today.

[Yaël Dillies]

... and I asked @Alex J. Best to write it several months ago :sweat_smile:

[Jireh Loreaux]

#14211 as an example of this. (if you choose to approve, please delegate instead of merging as it may have a merge conflict with a PR that will land soon.)

[Damiano Testa]

Ok, so, to clarify, the linter should flag all non-protected declarations of the form X.Y, where Y has no "dots" and declaration _root_.Y exists?

[Damiano Testa]

(and X is not empty, I guess...)

[Damiano Testa]

A preliminary script suggests that there are about 7k such non-protected results. Here is a selection:

List.Subperm.trans                                       GaloisConnection.id
Int.lt_of_not_ge                                         EuclideanDomain.gcd_zero_left
ProbabilityTheory.kernel.map_zero                        Bool.false_ne_true
USize.xor                                                Left.inv_le_one_iff
Nat.lt_mul_iff_one_lt_left                               Nat.gcd_dvd_gcd_mul_left
NonUnitalAlgHom.congr_fun                                List.IsRotated.symm
SimpleGraph.Embedding.completeGraph                      Decidable.not_ball
Bool.iff_self_and                                        Polynomial.map_neg
ClosureOperator.IsClosed                                 Orthonormal.inner_sum
IsSymm.symm                                              Submodule.neg_eq_self
UniformAddGroup.uniformContinuous_sub                    CommRingCat.Colimits.Relation.mul_comm
NonUnitalSubring.sum_mem                                 Finset.max_le_iff
Int.le_neg_add_of_add_le                                 Int.dvd_add_right
Linarith.le_of_le_of_eq                                  ENNReal.pow_pos
StrictConcaveOn.congr                                    CategoryTheory.Presheaf.IsLocallyInjective
RingEquiv.map_prod                                       AlgEquiv.isSeparable_iff
LinearOrderedField.div_eq_mul_inv                        NonUnitalSubsemiring.subset_closure
Finset.codisjoint_inf_right                              Rat.add_left_neg
IsOpen.nhdsWithin_eq                                     Nat.eq_zero_or_pos
Even.zpow_nonneg                                         Nat.sub_one_mul
HasGradientWithinAt.congr                                UInt8.lt_irrefl
Iff.trans                                                MonoidHom.map_pow
Function.Embedding                                       Ordinal.dvd_antisymm
Set.Nontrivial                                           NormedAddTorsor.dist_eq_norm'
Trivialization.contMDiff_iff                             Nat.mul_le_mul_right
ENNReal.inv_le_inv'                                      Int.sub_lt_sub_right
Stream'.WSeq.LiftRel.trans                               Nat.dist_self
Option.map_bind                                          IsAddUnit.sub_add_cancel_left
CanonicallyLinearOrderedSemifield.le_of_add_le_add_left  FirstOrder.Language.LHom.funext
Module.zero_smul                                         MeasureTheory.JordanDecomposition.negPart
LinearMap.congr_fun₂                                     AddOpposite.instSemiring
OmegaCompletePartialOrder.Continuous                     Asymptotics.IsLittleO.congr
Even.pow_pos                                             Stream'.WSeq.map_congr
LowerSet.compl_top                                       AddConstMap.id
Nat.le_add_right                                         Filter.nhds_mono
WeierstrassCurve.Jacobian.map_neg                        Commute.sub_dvd_pow_sub_pow
MeasureTheory.Measure.zero_sub                           Equiv.instCommGroupShrink
MonoidHom.map_mul_inv                                    AffineMap.congr_fun
LSeriesHasSum.LSeriesSummable                            Set.ssubset_of_ssubset_of_subset
IsOpen.continuousOn_iff                                  EqvGen.Setoid
Multiset.map_eq_zero                                     LeftCancelSemigroup.mul_left_cancel
SubtractionMonoid.neg_add_rev                            Submonoid.map_iSup
Nat.Prime.one_le                                         AddConGen.Rel.below.trans
Subsemiring.list_prod_mem                                Monotone.eq_of_le_of_le
CategoryTheory.ShortComplex.Homotopy.trans               AddRightCancelMonoid.add_zero
IsConnected.subset_closure                               List.tendsto_nhds
IsIntegralClosure.algebraMap_injective                   Nat.mul_left_cancel
Primrec.cond                                             IsUnit.div_self
InvOneClass.inv_one                                      Nat.le_of_not_gt
UInt8.le_trans                                           Zsqrtd.mul_nonneg
PowerSeries.mul_inv_rev                                  Subalgebra.mul_self
NNReal.tendsto_rpow_atTop                                AddCommGroup.ModEq.add_left_cancel
Equiv.Perm.congr_fun                                     HasDistribNeg.neg_mul
Nat.dvd_mul                                              LipschitzOnWith.norm_sub_le_of_le
Multiset.lcm_dvd                                         MonCat.Colimits.Relation.mul_assoc
LipschitzOnWith.norm_div_le                              Int.le_max_right
Algebra.IsIntegral                                       ENNReal.nhdsWithin_Iio_neBot
AddSubsemigroup.closure_union                            AddEquiv.refl
Int.max_comm                                             IsAddMonoidHom.id
Rat.add_mul                                              SNum.«term_::_»
LieSubmodule.eq_bot_iff                                  EqvGen.symm
AddUnits.eq_neg_of_add_eq_zero_right                     EMetric.tendsto_nhds
Module.add_smul                                          Finset.ssubset_iff_subset_ne
List.Lex                                                 ENNReal.div_le_div_left
Topology.IsUpper.closure_singleton                       Nat.sub_le_sub_iff_right
ProofWidgets.Svg.Action                                  CategoryTheory.DifferentialObject.Hom.comm
MeasureTheory.HasFiniteIntegral.congr                    Nat.sInf_empty
IsUnit.stronglyMeasurable_const_smul_iff                 Equiv.cast
Con.symm                                                 Submodule.map_smul
AddLECancellable.tsub_lt_tsub_iff_right                  Mathlib.Tactic.PushNeg.not_iff
AddUnits.add_neg_eq_zero                                 ProofWidgets.Svg.Frame.height
LinearOrder.max_def                                      IsCoprime.neg_neg
PartENat.ne_top_of_lt                                    CircleDeg1Lift.continuous_pow
Multiset.sub_le_iff_le_add                               Equiv.forall₃_congr
Nat.dvd_refl                                             AntitoneOn.congr
SignType.LE                                              MulLECancellable.mul_le_mul_iff_left
TensorAlgebra.Rel                                        ContinuousMap.congr_fun
Filter.EventuallyLE.mul_le_mul                           EMetric.uniformEmbedding_iff'
AddSubgroup.add_mem_cancel_right                         RingHom.LocalizationPreserves
WithTop.isLUB_sSup                                       LucasLehmer.X.left_distrib
Ne.ite_eq_left_iff                                       Trivialization.smoothWithinAt_iff
FermatLastTheoremForThreeGen.Solution'.multiplicity      WithTop.add_lt_add_left
SModEq.refl                                              IsDedekindDomainInv.inv_mul_eq_one
Int.min_eq_right                                         IsCompl.symm
Equiv.instSemiringShrink                                 FreeLieAlgebra.Rel.leibniz_lie
Padic.AddValuation.map_mul                               Stream'.WSeq.LiftRel.symm
MeasureTheory.VectorMeasure.MutuallySingular.symm        AbsoluteValue.map_neg
Mathlib.Meta.FunProp.LambdaTheoremArgs.id                System.FilePath.normalize
IsSemiringHom.map_add                                    List.instLawfulBEq
IsOpen.exterior_subset_iff                               Commute.exists_add_pow_prime_pow_eq
RightCancelSemigroup.mul_right_cancel                    Subring.multiset_sum_mem
Nat.div_lt_one_iff                                       CategoryTheory.GrothendieckTopology.trivial
ENNReal.mul_lt_mul                                       Right.add_pos_of_pos_of_nonneg
NzsNum.bit0                                              Equiv.Set.congr
Equiv.congr_arg                                          Nat.mul_left_inj
Metric.uniformInducing_iff                               Finset.not_nonempty_empty
AddMonoidHom.id                                          ContinuousMap.HomotopyRel.cast
ClosureOperator.isClosed_closure                         Nat.mul_sub_left_distrib
FirstOrder.Language.Equiv.refl                           Char.lt_trans
Relator.BiTotal.trans                                    CategoryTheory.Functor.map_add
Qq.QuotedDefEq.rfl                                       CategoryTheory.FreeMonoidalCategory.Hom.id
Finset.codisjoint_inf_left                               NzsNum.«term_::_»
ZNum.bit0                                                DistribMulAction.smul_zero
FP.FloatCfg.precMax                                      Asymptotics.SuperpolynomialDecay.congr
LE.le.trans                                              QuadraticForm.Isometry
FirstOrder.Language.IsAlgebraic                          Mathlib.Tactic.Ring.ExProd.cast
InvolutiveNeg.neg_neg                                    IsUnit.div_eq_iff
CategoryTheory.IsSplitEpi.id                             Set.Finite.lowerClosure
IsStrongAntichain.flip                                   IsSeparable.trans
AddConstMap.instPowNat                                   AddLECancellable.le_tsub_iff_left
Derivation.congr_fun                                     FreeGroup.map_one
GradeOrder.grade                                         Nat.Coprime.orderOf_pow
CanonicallyOrderedCommSemiring.npow_zero                 ENNReal.nhds_top
Nat.le_of_not_le                                         SmoothRing.smooth_mul
Int.neg_pos                                              NonUnitalCommSemiring.mul_comm
ONote.zero_add                                           PontryaginDual.map_one
USize.not_le                                             DFinsupp.bot_eq_zero
Ordinal.div_pos                                          Subalgebra.algebraMap_mem
StarSubalgebra.algebraMap_mem                            Set.OrdConnected.apply_covBy_apply_iff
CategoryTheory.Discrete.instSubsingleton

[Damiano Testa]

If I am not mistaken, each declaration above is not protected and the last component of each one of them is a declaration in its own right.

There are many more.

[Yaël Dillies]

Y should be allowed to have dots. Finset.Nat.antidiagonal and Nat.antidiagonal both existing would be bad.

[Yaël Dillies]

Are you sure you are handling export correctly?

[Damiano Testa]

Ok, I think that this is already the case in the list above: CategoryTheory.IsSplitEpi.id is flagged, but because id exists.

[Damiano Testa]

Yaël Dillies said:

Are you sure you are handling export correctly?

How should I handle export? My strategy has been to open Y, scan for resolveConst X and see if X appears.

[Damiano Testa]

(I also checked, antid does not appear as a substring of the output of the code.)

[Damiano Testa]

I spot-checked a few declarations in the output and it does seem that

• the declaration is not protected,
• the last segment is a (fully-qualified) declaration.

[Yaël Dillies]

Unsure! I don't know where export information is

[Yaël Dillies]

GradeOrder.grade is the suspicious exported declaration I was thinking of

[Damiano Testa]

Oh, GradeOrder.order is indeed protected, but there is docs#grade as well.

[Damiano Testa]

/-- An `𝕆`-graded order is an order `α` equipped with a strictly monotone function
`grade 𝕆 : α → 𝕆` which preserves order covering (`CovBy`). -/
class GradeOrder (𝕆 α : Type*) [Preorder 𝕆] [Preorder α] where
  /-- The grading function. -/
  protected grade : α → 𝕆
  /-- `grade` is strictly monotonic. -/
  grade_strictMono : StrictMono grade
  /-- `grade` preserves `CovBy`. -/
  covBy_grade ⦃a b : α⦄ : a ⋖ b → grade a ⋖ grade b

[Damiano Testa]

And #print is aware that GradeOrder.order is protected.

[Damiano Testa]

Ok, with a modification that excludes GradeOrder.grade, I got the list down to 4473 declarations.

[Damiano Testa]

(Btw, there is docs#AddMonoidAlgebra.grade and it is still flagged.)

[Damiano Testa]

The new list is available here.

[Damiano Testa]

Yaël Dillies said:

Y should be allowed to have dots. Finset.Nat.antidiagonal and Nat.antidiagonal both existing would be bad.

Yaël, re-reading this, I realize that I had missed a negation in your statement! You are right, this is not done by the current list, but would be easy to implement.

However, if the current count is about right (~4k declaration that need protecting), then it might be a good gradual process to start with these and then extend the scope to "more dots in Y" are allowed.

[Damiano Testa]

How does the list look like? If there is consensus that protecting those declarations is desired, I can look into automating that.

[Damiano Testa]

import Mathlib

open Lean Elab Command

def isRepeated (n : Name) (dbg? : Bool := false) : CommandElabM Bool := do
  if (← n.isBlackListed) then return false else
  let comps := n.components
  if comps.length ≠ 1 then
    let nm := comps.getLast!
    let ns := comps.dropLast.foldl Name.append default
    let nms ← withScope
      (fun s => {s with openDecls := (.simple ns []) :: s.openDecls })
        do resolveGlobalName nm
    if (nms.map Prod.fst).contains nm && (nms.map Prod.fst).contains n then
      if dbg? then dbg_trace nms
      return true
    else return false
  else return false

elab "#unprotected" : command => do
  let env ← getEnv
  let csts := env.constants
  let fin ← csts.map₁.foldM (init := ({} : HashSet Name)) fun ans n _ => do
    if ← isRepeated n then
      return ans.insert n
    else return ans
  let res := fin.toArray.filter (!#[`Lean, `Batteries, `Std].contains ·.components[0]!)
  logInfo m!"{res.size} declarations that clash as they are unprotected\n\n{res.qsort (·.toString < ·.toString)}"

#unprotected

[Damiano Testa]

Damiano Testa said:

Ok, with a modification that excludes GradeOrder.grade, I got the list down to 4473 declarations.

Today there seem to be 12 more declarations that should have been protected.

[Michael Rothgang]

I'd like to hear the room's opinion on the naming of various linter executables: should it be mk_all or mkAll? lint_style or lintStyle? run_linter or runLinter? Right now, we have

• runLinter defined in batteries and
• mk_all and lint_style defined in mathlib (pretty new)

#naming doesn't really talk about this, but rule 4 suggests mkAll and lintStyle.

[Damiano Testa]

My slight preference for command-line options is to use lowercase and underscores.

[Yaël Dillies]

Oh actually I thought runLinter was a declaration, not an executable, precisely because it is in lowerCamelCase

[Richard Osborn]

CLI interfaces usually just use all lowercase. These are run via lake exe? I would suggest lint and make commands that take options, so lake exe lint --style or lake exe make --all (or just lake exe make and have --all be the default).

[Yaël Dillies]

lake exe make sounds really ambiguous for what it is, though

[Richard Osborn]

So does mkAll, so maybe it needs a new name in general.

[Damiano Testa]

The name is legacy from when there was an all.lean file and you could import all. May not be the best justification for keeping the name, though...

[Damiano Testa]

Or maybe we can rename Mathlib.lean to All.lean!

[Ruben Van de Velde]

Now it "mk"s "all" top-level .lean files

[Kim Morrison]

lake exe make_directory_imports? Or just lake exe directory_imports?

The noun seems more useful in the name than the verb.

[Mario Carneiro]

I think we should actually use kebab case here, CLI tools/options are usually kebab case (e.g. apt-get)

[Damiano Testa]

Would it be possible to have tab-autocompletion for these options? Typing them can be quite tedious. If pressing tab writes them for you, then it is easier!

[Yaël Dillies]

Mario Carneiro said:

I think we should actually use kebab case here, CLI tools/options are usually kebab case (e.g. apt-get)

That's what I tried to do but the [CLI| ... ] macro in Lean doesn't support that

[Mario Carneiro]

why would it care what the name of the executable is?

[Mario Carneiro]

and also, that's dumb

[Mario Carneiro]

does it not work if you use the french quotes?

[Michael Rothgang]

Mario Carneiro said:

does it not work if you use the french quotes?

With options, that certainly fails (that annoyed me today); I didn't test the CLI name.

[Mario Carneiro]

just tested, and you can put "flag-name" : type; "description" in the FLAGS section of [Cli| ... ]

[Michael Rothgang]

I just did a different test in branch#MR-rename-lint-style-wip, renaming the lint_style executable to lint-style: it works!

[Michael Rothgang]

Michael Rothgang said:

I just did a different test in branch#MR-rename-lint-style-wip, renaming the lint_style executable to lint-style: it works!

#14757 will rename lint_style to lint-style. Depends on #14697 (substantial rewrite of the logic, to support auto-updating the exceptions file).

[Richard Osborn]

Is there a reason why you prefer lint-style to lint? Generally, shorter names are preferred for CLI interfaces.

[Michael Rothgang]

The reason is the existence of other linters: there are

• syntax linters (which automatically run on any file, such as the setOption lint)
• environment linters (registered with the env_lint attribute), such as the simpNF or docBlame lint: these are run using the runLinters executable defined in batteries
• mathlib's style linters, which are text-based: they were previously written in Python; I'm gradually porting them to Lean. lint-style only runs the last kind, which is why I prefer to not name it simply lint

[Michael Rothgang]

I would also like to have a lake lint command, with e.g. lake lint --style only running the style lints. As I understand it, that is not too far away... but I'm not sure on the specifics @Kim Morrison

[Richard Osborn]

Agreed. lake lint would be ideal to solve the current fragmentation.

[Kim Morrison]

I would propose that as an initial step to lake lint we ask for something that is parallel to the current lake test implementation: i.e. it lets you point to an executable or script or library to build, but leaves the actual implementation up to the library.

This is easy to implement on the lake side, gives us a path to experimenting in downstream libraries, and later if appropriate adding linter management to lake itself.

[Kim Morrison]

I'm pretty sure Mac has previously discussed doing this, but I don't see an open issue. Would someone like to create an issue along these lines?

[Michael Rothgang]

Kim Morrison said:

lake exe make_directory_imports? Or just lake exe directory_imports?

The noun seems more useful in the name than the verb.

So: what would be a good name for mk_all: any objections to make-directory-imports; other suggestions? If I don't hear any by, say, Monday, I will prepare a PR to rename the script (and leaving a warning on the old one).

[Michael Rothgang]

While we're at it: any objections if I rename checkYaml to check-yaml and add this as a separate rule to #naming? If not, #14892 is a PR doing the former.

[Damiano Testa]

In the absence of Tab-completion, I would prefer a shorter name for mk_all. Otherwise, I'll probably make an alias and then will never remember what the real name is.

[Michael Rothgang]

Richard Osborn said:

Agreed. lake lint would be ideal to solve the current fragmentation.

Today I realised that this already exists; it was added in Lean 4.9. :tada:
Configuring mathlib to enable this could be a next step.

[Ruben Van de Velde]

Should docs#Nat.not_eq_zero_of_lt be Nat.ne_zero_of_lt (see also docs#ne_zero_of_lt)?

[Ruben Van de Velde]

Given

abbrev IsClique (s : Set α) : Prop :=
  s.Pairwise G.Adj

is the field named correctly in

structure IsNClique (n : ℕ) (s : Finset α) : Prop where
  IsClique : G.IsClique s
  card_eq : #s = n

or should it be isClique?

[Eric Wieser]

isClique, because it's not a : Prop

[Ruben Van de Velde]

Is docs#PowerSeries.divided_by_X_pow_order not supposed to be in camel case?

[Anthony DeRossi]

As requested in #20893, statements of the form X = Y ↔ ... are commonly named X_eq_Y or X_eq_Y_iff. #naming says iff is "sometimes omitted". Which should it be?

[Jon Eugster]

personal preference, but I like x_eq_y_iff better. (maybe particularly because th LHS has an eq in there, misleading the reader? :thinking:)

[Jon Eugster]

Also, I interpret "sometimes ommitted" to mean it's the non-standard thing to do, but allowed. As opposed to "usually ommitted".

[Violeta Hernández]

I think it makes sense to expect rw [X_eq_Y] to substitute X for Y, and to expect rw [X_eq_Y_iff] to substitute X = Y for something else.

[Xavier Roblot]

When working with the docs#NumberField.mixedEmbedding.mixedSpace, it is necessary in many
situations to distinguish between the docs#NumberField.InfinitePlace.IsReal and
docs#NumberField.InfinitePlace.IsComplex cases. Thus, many results are duplicated using the ending
of_isReal or of_isComplex in their names. However, this is not consistent since the spelling
ofIsReal or ofIsComplex is also used for some results for no good reason (and I am sure
about that since I wrote this code :sweat_smile: ). In #21629, I am trying to fix that and suggested to use the
following convention:

• If the fact that the infinite place is real or complex comes from an additional hypothesis, use of_isReal/of_isComplex
• If the fact that the infinite place is real or complex comes from a subtype, use ofIsReal/ofIsComplex

As suggested by @Michael Stoll , I am asking here for some feedback about this naming convention.

[Michael Stoll]

It would be good if this question would receive some comments. Here are mine:

• It makes sense to try to distinguish the two variants (hypothesis/subtype) in the declaration name.
• But there should be agreement on how to do this (and it should be compatible with the naming convention).

Does this (i.e., "duplicate" statements that either use a hypothesis or the corresponding subtype) already occur somewhere else in Mathlib?

[Michael Rothgang]

Should docs#ENNReal.toNNReal_nat be called ENNReal.toNNReal_natCast instead? Same question for docs#ENNReal.toReal_nat. (This question came up in #22049, which is otherwise close to landing.) I don't mind either way, but agreeing on one direction would be nice.

[Yaël Dillies]

Yes, they both should. And we should have ofNat versions of both too

[Ruben Van de Velde]

docs#ENNReal.toReal_ofNat exists

[Michael Rothgang]

#22071

[Ben Eltschig]

I just came across Topology.CWComplex.mapsto - that should instead be called Topology.CWComplex.mapsTo, I think?

[Ben Eltschig]

#22106

[Michael Rothgang]

Shoulds docs#Sum.inl_injective be injective_inl instead?

[Ruben Van de Velde]

No, injective is an exception

[Michael Rothgang]

Ah, right: https://leanprover-community.github.io/contribute/naming.html#injectivity. Thanks for clarifying!

[Michael Rothgang]

(and https://leanprover-community.github.io/contribute/naming.html#injectivity)

[Ruben Van de Velde]

(Whether that's a good choice I'll let you decide for yourself, but that's the rule right now)

[Ruben Van de Velde]

theorem surjective_compr₂_of_exists_rightInverse (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ)
   (hf : Surjective f) (hg : ∃ g' : Qₗ →ₗ[R] Pₗ, g.comp g' = LinearMap.id) :

Do we accept rightInverse as a pseudo-identifier when it doesn't refer to docs#Function.RightInverse ?

[Ben Eltschig]

docs#CategoryTheory.Sieve.pullback_eq_top_iff_mem should probably be mem_iff_pullback_eq_top, right? Since that's the direction in which the equivalence is stated

[Kim Morrison]

Yes, please! :-)

[Ben Eltschig]

#22385

[Ruben Van de Velde]

Lower-camel-case of AEStronglyMeasurable: aeStronglyMeasurable or aestronglyMeasurable? We use both, though the latter dominates

[Etienne Marion]

Indeed the latter dominates but I think the convention indicates it should be the former, because "ae" is a group and "strongly" is another one.

[Eric Wieser]

Shouldn't it match how we handle NNReal?

[Etienne Marion]

That’s true. This came up (in a slightly different form) here and we settled for the former option there, which looking at nnreal and aestronglyMeasurable seems to be against how things are usually done in the library. On the other hand my interpretation of the naming convention is that we should go with the former, so I’m a bit confused.

[Michael Rothgang]

LinearEquiv.prod which is Equiv.prodCongr as a linear map. Should we rename one of these?
(There is also LinearMap.prod, presumably we want that to match also.)That one is actually fine.

[Michael Rothgang]

I don't care about this bikeshed's colour, but I have lost a few minutes more than once because of this inconsistency.

[Aaron Liu]

I think they should be LinearEquiv.prodCongr and LinearMap.prodCongr

[Bolton Bailey]

IMHO, in cases of decision points between shorter and longer names, there are a few reasons its better to favor the longer ones:

1. In the past few years Copilot and similar software has made writing long names by typing them out less necessary.
2. Mathlib is large and has many analogous names for similar concepts, longer names decrease the chance of a later collision.
3. Mathlib is "read more than its written", probably moreso than other code due to how necessary it is to consult documentation when writing.

[Eric Wieser]

docs#AddEquiv.prodCongr also matches the suggestion

[Eric Wieser]

I think a lot of the linear map api diverges from the others

[Eric Wieser]

Another example is docs#LinearMap.proj vs docs#Pi.evalRingHom, docs#Pi.evalMonoidHom, etc

[Michael Rothgang]

#24145 renames LInearEquiv.prod

[Michael Rothgang]

How should docs#pullback_snd_iso_of_right_iso be called? #24151 points out that the current name is definitely wrong --- but as the conclusion is IsIso (pullback.fst f g), I'm not convinced that just pullback_fst_iso_of_right_iso is correct. (Perhaps the fix is "don't name the instance".)

[Etienne Marion]

#23500 from @Loïc Simon defines this:

structure MeasureTheory.Measure.SetWhereLE (μ ν : Measure X) (s : Set X) : Prop where
  measurable : MeasurableSet s
  le_on : μ.restrict s ≤ ν.restrict s
  ge_on_compl : ν.restrict sᶜ ≤ μ.restrict sᶜ

Do you think the name is ok? The guideline for structures is not very clear, so I don't know if we should just refer to the general notion as does the name here are try to stick to what is literally written in lean, which I think would give something like RestrictLERestrictOn.

[Eric Wieser]

Is that within the MeasureTheory. namespace?

[Etienne Marion]

Eric Wieser said:

Is that within the MeasureTheory. namespace?

Yes, I edited the code (it's a bit different than the first one I posted but the question is the same).

[Yury G. Kudryashov]

Etienne Marion said:

#23500 from Loïc Simon defines this:

structure MeasureTheory.Measure.SetWhereLE (μ ν : Measure X) (s : Set X) : Prop where
  measurable : MeasurableSet s
  le_on : μ.restrict s ≤ ν.restrict s
  ge_on_compl : ν.restrict sᶜ ≤ μ.restrict sᶜ

Do you think the name is ok? The guideline for structures is not very clear, so I don't know if we should just refer to the general notion as does the name here are try to stick to what is literally written in lean, which I think would give something like RestrictLERestrictOn.

Cf. docs#MeasureTheory.hahn_decomposition.

[Loïc Simon]

Oh, I actually missed the version of Hahn decomposition for positive measures. I was relying on the one on signed measure and kind of showing the unsigned version on my own. That may simplify the overall proof. Thank you @Yury G. Kudryashov .

[Loïc Simon]

[Well, after looking at the proof of hahn_decomposition for positive measure Here I realize, my own proof is actually simpler (because it relies on the SignedMeasure version, that is exists_compl_positive_negative and because I created a couple useful lemmas ). The core of my proof is this lemma.
I wonder if it's not worth keeping my own proof after all. What's your take on this ?

Also, about the naming. I used SetWhereLe \mu \nu S to refer to the set (or class of sets actually) which is sometimes denoted {\mu \le \nu} in the stat folklore. I actually have two versions of this notion (one for positive measures, and one for signed measures). @Yury G. Kudryashov you proposed to rename this notion as IsHahnDecomposition, I kind of agree with you given the content of Measure/Decomposition/Hahn.lean. But to my mind, the Hahn decomposition theorem is classically expressed for signed measures (am I wrong on that ?). Ironically , in mathlib the SignedMeasure version of the Hahn decomposition is named exists_compl_positive_negative. Anyway, I'd be interested in some discussion about the naming.

[EDIT] @Yury G. Kudryashov I've read back again your suggestion on my PR, and I wonder if you recommend to move SetWhereLe and the related results to Measure/Decomposition/Hahn.lean as a mean to simplify the proof of hahn_decomposition.

[Yury G. Kudryashov]

If we introduce this definition (I don't know if we should), then it should happen in Measure/Decomposition/Hahn, because reformulating Hahn decomposition in terms of your definition seems natural.

[Yury G. Kudryashov]

I have no opinion about 2 proofs.

[Christian Merten]

Should docs#LinearEquiv.sumArrowLequivProdArrow be called

• LinearEquiv.sumArrowProdArrow
• or LinearEquiv.sumArrowEquivProdArrow
• or even just LinearEquiv.sumArrow?

For reference, the dependent version is called docs#LinearEquiv.sumPiEquivProdPi`.

I don't understand why there is an L in the name (indicating the linearity I assume), given that it is already in the LinearEquiv namespace.

(I am asking, because I am about to add the AlgEquiv version).

[Jovan Gerbscheid]

Should this be LinearEquiv.sumArrowEquivArrowProd instead? Or should Complex.equivRealProd be called Complex.equivProdReal?

[Robert Maxton]

Michael Rothgang said:

How should docs#pullback_snd_iso_of_right_iso be called? #24151 points out that the current name is definitely wrong --- but as the conclusion is IsIso (pullback.fst f g), I'm not convinced that just pullback_fst_iso_of_right_iso is correct. (Perhaps the fix is "don't name the instance".)

Bumping this, as it seems to have got lost. (My personal preference is that sorting by pullback is more useful when browsing the suggestions list than sorting by isIso)