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...