Zulip Chat Archive

Stream: mathlib4

Topic: Naming convention


Xavier Roblot (Jan 18 2023 at 15:39):

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 (Jan 18 2023 at 15:44):

Yes, those are correct.

Xavier Roblot (Jan 18 2023 at 15:44):

Ok. Thanks!

Notification Bot (Jan 18 2023 at 15:45):

Xavier Roblot has marked this topic as resolved.

Notification Bot (Jan 19 2023 at 09:33):

Johan Commelin has marked this topic as unresolved.

Johan Commelin (Jan 19 2023 at 09:33):

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 (Jan 19 2023 at 09:33):

Or should it be truncEquivFinOfCardEq?

Alex Keizer (Jan 19 2023 at 14:03):

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

Ruben Van de Velde (Jan 19 2023 at 14:04):

:see_no_evil:

Eric Wieser (Jan 19 2023 at 14:05):

@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 (Jan 19 2023 at 14:06):

@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 (Jan 20 2023 at 10:18):

So, Zmod or ZMod?

Heather Macbeth (Jan 20 2023 at 16:12):

We have Int.ModEq so maybe ZMod for parallelism?

Eric Wieser (Jan 23 2023 at 11:38):

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

zbatt (Jan 24 2023 at 16:42):

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

zbatt (Jan 24 2023 at 16:43):

As in this case here

Reid Barton (Jan 24 2023 at 16:45):

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 (Jan 24 2023 at 16:46):

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

Reid Barton (Jan 24 2023 at 16:49):

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

Reid Barton (Jan 24 2023 at 16:50):

since we're now in namespace Rack

zbatt (Jan 24 2023 at 16:51):

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 (Jan 24 2023 at 16:51):

What is the error?

zbatt (Jan 24 2023 at 16:51):

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

Reid Barton (Jan 24 2023 at 16:52):

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

zbatt (Jan 24 2023 at 16:52):

sorry, my bad

Reid Barton (Jan 24 2023 at 16:55):

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 (Jan 24 2023 at 16:56):

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 (Jan 24 2023 at 16:57):

it can't find it

zbatt (Jan 24 2023 at 16:58):

wait this is strange

zbatt (Jan 24 2023 at 16:59):

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 (Jan 24 2023 at 16:59):

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 (Jan 24 2023 at 17:00):

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

zbatt (Jan 24 2023 at 17:00):

that seems to have worked, thanks!

zbatt (Jan 24 2023 at 17:04):

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

Kyle Miller (Jan 24 2023 at 17:07):

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 (Jan 24 2023 at 17:08):

gotcha

Yaël Dillies (Jan 24 2023 at 17:20):

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 (Jan 24 2023 at 17:20):

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

Yaël Dillies (Jan 24 2023 at 17:24):

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

Kyle Miller (Jan 24 2023 at 17:30):

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 (Jan 24 2023 at 17:31):

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

Jireh Loreaux (Jan 25 2023 at 16:05):

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 (Jan 25 2023 at 16:05):

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

Jireh Loreaux (Jan 25 2023 at 16:08):

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 (Jan 25 2023 at 17:30):

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

Eric Wieser (Jan 25 2023 at 17:31):

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

Reid Barton (Feb 09 2023 at 17:00):

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 (Feb 19 2023 at 21:00):

Should Filter.EventuallyLe be Filter.EventuallyLE?

Yury G. Kudryashov (Feb 21 2023 at 03:35):

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

Yury G. Kudryashov (Feb 21 2023 at 03:35):

We use NNReal and ENNReal for types.

Jireh Loreaux (Feb 21 2023 at 03:38):

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 (Feb 21 2023 at 03:39):

Personally, the latter makes more sense to me.

Eric Wieser (Feb 21 2023 at 11:56):

I prefer the former slightly

Thomas Murrills (Feb 21 2023 at 18:46):

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 (Feb 21 2023 at 19:34):

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 (Feb 21 2023 at 19:37):

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 (Feb 21 2023 at 19:43):

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 (Feb 21 2023 at 19:46):

I stand corrected, nnreal is consistent.

Johan Commelin (Feb 22 2023 at 03:17):

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 (Feb 22 2023 at 19:23):

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 (Feb 22 2023 at 19:24):

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 (Feb 22 2023 at 19:41):

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ō (Feb 23 2023 at 09:47):

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

Eric Wieser (Feb 23 2023 at 11:06):

Seems reasonable to me

Matthew Ballard (Feb 23 2023 at 14:00):

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 (Feb 23 2023 at 14:03):

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

Adam Topaz (Feb 23 2023 at 14:10):

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

Matthew Ballard (Feb 23 2023 at 14:39):

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

Adam Topaz (Feb 23 2023 at 14:40):

Have you met docs#category_theory.bundled ?

Ruben Van de Velde (Feb 23 2023 at 15:01):

How about Hom as a field for categories?

Adam Topaz (Feb 23 2023 at 15:04):

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

Matthew Ballard (Feb 23 2023 at 15:04):

That at least has Sort v in the signature

Adam Topaz (Feb 23 2023 at 15:04):

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

Kyle Miller (Feb 23 2023 at 15:41):

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 (Feb 23 2023 at 15:42):

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

Adam Topaz (Feb 23 2023 at 15:43):

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

Adam Topaz (Feb 23 2023 at 15:43):

Again, "all the conventions"

Kyle Miller (Feb 23 2023 at 15:47):

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 (Feb 23 2023 at 15:50):

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

Eric Wieser (Feb 23 2023 at 15:51):

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

Eric Wieser (Feb 23 2023 at 15:52):

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

Kyle Miller (Feb 23 2023 at 15:52):

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 (Feb 23 2023 at 15:53):

Because you write p : SomeProp but never b : someBool

Kyle Miller (Feb 23 2023 at 15:55):

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 (Feb 23 2023 at 15:56):

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 (Feb 23 2023 at 16:02):

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 (Feb 23 2023 at 16:03):

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

Mario Carneiro (Feb 23 2023 at 16:04):

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

Mario Carneiro (Feb 23 2023 at 16:04):

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 (Feb 23 2023 at 16:34):

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 (Feb 23 2023 at 16:36):

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 (Feb 23 2023 at 16:52):

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 (Feb 23 2023 at 17:21):

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

Mario Carneiro (Feb 23 2023 at 17:22):

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 (Feb 23 2023 at 17:46):

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 (Feb 23 2023 at 17:46):

How did we port docs4#CategoryTheory.Bundled ?

Eric Wieser (Feb 23 2023 at 17:47):

Oh, it's Greek so I guess not relevant

Matthew Ballard (Feb 23 2023 at 18:47):

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 (Feb 23 2023 at 18:49):

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

Adam Topaz (Feb 23 2023 at 18:52):

apex?!

Adam Topaz (Feb 23 2023 at 18:52):

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

Johan Commelin (Feb 23 2023 at 18:53):

that's true

Johan Commelin (Feb 23 2023 at 18:53):

I guess it would be the coapex?

Johan Commelin (Feb 23 2023 at 18:54):

https://words.bighugelabs.com/antapex

Adam Topaz (Feb 23 2023 at 18:54):

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

Adam Topaz (Feb 23 2023 at 18:55):

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 (Feb 23 2023 at 18:58):

Clearly xepa

Thomas Murrills (Feb 23 2023 at 20:10):

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 (Feb 23 2023 at 20:20):

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

Kyle Miller (Feb 24 2023 at 15:24):

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 (Feb 24 2023 at 15:58):

It looks like pt is it. Incoming soon

Eric Wieser (Feb 24 2023 at 17:40):

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 (Feb 24 2023 at 18:03):

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 (Feb 24 2023 at 18:04):

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

Johan Commelin (Feb 24 2023 at 18:07):

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

Reid Barton (Feb 24 2023 at 18:20):

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 (Feb 24 2023 at 18:29):

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

Alex Keizer (Feb 24 2023 at 18:33):

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 (Feb 24 2023 at 18:34):

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 (Feb 24 2023 at 18:38):

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

Reid Barton (Feb 24 2023 at 18:40):

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

Reid Barton (Feb 24 2023 at 18:41):

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

Jireh Loreaux (Feb 24 2023 at 18:48):

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 (Feb 24 2023 at 18:56):

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 (Feb 24 2023 at 19:52):

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

Thomas Murrills (Feb 24 2023 at 20:00):

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 (Feb 24 2023 at 23:22):

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

Kevin Buzzard (Feb 25 2023 at 00:23):

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

Kevin Buzzard (Feb 25 2023 at 00:23):

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

Thomas Murrills (Feb 25 2023 at 00:34):

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 (Feb 25 2023 at 02:25):

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 (Mar 06 2023 at 20:24):

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 (Mar 06 2023 at 20:33):

Those aren't the same though

Eric Wieser (Mar 06 2023 at 20:34):

The first is a Type, the second is a Set

Eric Wieser (Mar 06 2023 at 20:35):

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 (Mar 06 2023 at 20:35):

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

Arien Malec (Mar 06 2023 at 21:00):

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 (Mar 06 2023 at 21:03):

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 (Mar 06 2023 at 21:09):

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 (Mar 06 2023 at 21:10):

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 (Mar 06 2023 at 21:11):

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

Eric Wieser (Mar 06 2023 at 21:17):

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

Eric Wieser (Mar 06 2023 at 21:18):

Arien Malec said:

here we have a function from type to type.

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

Arien Malec (Mar 06 2023 at 21:19):

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 (Mar 06 2023 at 21:19):

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 (Mar 06 2023 at 21:19):

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

Eric Wieser (Mar 06 2023 at 21:20):

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 (Mar 06 2023 at 21:23):

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 (Mar 06 2023 at 21:28):

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 (Mar 06 2023 at 21:33):

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

Jireh Loreaux (Mar 06 2023 at 22:04):

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

Eric Wieser (Mar 16 2023 at 19:01):

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 (Apr 09 2023 at 18:51):

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 (Apr 09 2023 at 19:02):

No, the current name is correct

MonadMaverick (Apr 09 2023 at 19:38):

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 (Apr 09 2023 at 20:02):

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

Eric Wieser (Apr 09 2023 at 20:03):

But your original example is a proof so should be lowerCamel_snake

MonadMaverick (Apr 09 2023 at 20:11):

I see. Thank you!

Kevin Buzzard (Apr 16 2023 at 11:37):

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 (Apr 16 2023 at 11:42):

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

Kevin Buzzard (Apr 16 2023 at 11:44):

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 (Apr 17 2023 at 06:41):

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 (Apr 17 2023 at 06:42):

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

Ruben Van de Velde (Apr 17 2023 at 07:01):

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

Yaël Dillies (Apr 17 2023 at 07:25):

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

Ruben Van de Velde (Apr 17 2023 at 07:29):

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

Yaël Dillies (Apr 24 2023 at 08:24):

Why is it docs4#Localization but docs4#addLocalization ?

Eric Wieser (Apr 24 2023 at 08:29):

It's a mistake for sure

Eric Wieser (Apr 24 2023 at 08:30):

Also, docs4# consuming ? is really annoying

Yaël Dillies (Apr 24 2023 at 08:33):

Not if you're :flag_france: :stuck_out_tongue:

Mario Carneiro (Apr 24 2023 at 08:35):

Eric Wieser said:

Also, docs4# consuming ? is really annoying

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

Eric Wieser (Apr 24 2023 at 08:38):

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

Patrick Massot (Apr 24 2023 at 08:59):

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

Eric Wieser (Apr 24 2023 at 09:02):

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 (Apr 24 2023 at 09:04):

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
x2+xx,\frac{x^2+x}{x,} or worse

Mario Carneiro (Apr 24 2023 at 09:10):

What about docs4#Array.back?

Eric Wieser (Apr 24 2023 at 09:13):

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

Yaël Dillies (Apr 29 2023 at 15:51):

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

Scott Morrison (Apr 29 2023 at 22:40):

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 (Apr 29 2023 at 22:56):

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 (Apr 29 2023 at 22:57):

Is that unicode smallcaps!?

Jireh Loreaux (Apr 30 2023 at 02:15):

Do those work in idents?

Jeremy Tan (Apr 30 2023 at 02:23):

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 (Apr 30 2023 at 03:32):

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 (Apr 30 2023 at 07:59):

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 (Apr 30 2023 at 07:59):

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 (Apr 30 2023 at 08:13):

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 (Apr 30 2023 at 08:36):

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 (Apr 30 2023 at 08:37):

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

Yaël Dillies (Apr 30 2023 at 08:41):

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

Eric Wieser (Apr 30 2023 at 08:48):

It just looked for TitleCase names

Eric Wieser (Apr 30 2023 at 08:49):

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

Yaël Dillies (Apr 30 2023 at 08:49):

Ah right!

Eric Wieser (Apr 30 2023 at 08:50):

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 (Apr 30 2023 at 08:51):

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

Yaël Dillies (Apr 30 2023 at 08:52):

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 (Apr 30 2023 at 08:54):

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

Mario Carneiro (Apr 30 2023 at 08:54):

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

Adam Topaz (Apr 30 2023 at 14:36):

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 (Apr 30 2023 at 14:43):

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 (Apr 30 2023 at 14:45):

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

Adam Topaz (Apr 30 2023 at 14:47):

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 (Apr 30 2023 at 14:47):

Recall that we have this forget_2 class

Yaël Dillies (Apr 30 2023 at 14:54):

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

Adam Topaz (Apr 30 2023 at 14:56):

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 (Apr 30 2023 at 14:59):

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 (Apr 30 2023 at 15:00):

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

Yaël Dillies (Apr 30 2023 at 15:09):

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 (May 01 2023 at 21:34):

Getting back to the actual naming issue for a moment:

Today's porting meeting was initially enthusiastic about just making the change GroupGrp 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 (May 01 2023 at 21:36):

Actually, worse than CommRing is of course just Ring.

Scott Morrison (May 01 2023 at 21:37):

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 (May 01 2023 at 21:38):

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

Scott Morrison (May 01 2023 at 21:39):

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

Yaël Dillies (May 01 2023 at 21:40):

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 (May 01 2023 at 21:42):

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

Scott Morrison (May 01 2023 at 21:42):

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

Yaël Dillies (May 01 2023 at 21:42):

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

Yaël Dillies (May 01 2023 at 21:43):

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

Alex J. Best (May 01 2023 at 21:43):

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

Yaël Dillies (May 01 2023 at 21:43):

BoundedDistribLattice/BoundedDistribLattices however is a mouthful.

Scott Morrison (May 01 2023 at 21:43):

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 (May 01 2023 at 21:44):

BddDistribLat is the alternative Yaël?

Yaël Dillies (May 01 2023 at 21:44):

BddDistLat rather, but yeah close enough.

Mario Carneiro (May 01 2023 at 21:44):

or BddDLat

Yaël Dillies (May 01 2023 at 21:44):

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 (May 01 2023 at 21:45):

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

Scott Morrison (May 01 2023 at 21:45):

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 (May 01 2023 at 21:46):

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 (May 01 2023 at 21:46):

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 (May 01 2023 at 21:48):

I think Yaël's suggestion gives:

  • Lat, Rings, CommRings, Grp, Top

for the examples above?

Yaël Dillies (May 01 2023 at 21:48):

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 (May 01 2023 at 21:49):

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

Scott Morrison (May 01 2023 at 21:50):

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 (May 01 2023 at 21:51):

Sounds reasonable, yes.

Scott Morrison (May 01 2023 at 21:52):

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

Scott Morrison (May 01 2023 at 21:52):

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

Scott Morrison (May 01 2023 at 21:53):

@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 (May 01 2023 at 21:54):

Do people care about the category of CommSemirings?

Scott Morrison (May 01 2023 at 21:54):

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

Eric Wieser (May 01 2023 at 21:55):

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

Scott Morrison (May 01 2023 at 21:55):

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

Kevin Buzzard (May 01 2023 at 22:01):

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 (May 01 2023 at 22:04):

I'd be happy with GROUP as well

Jireh Loreaux (May 01 2023 at 22:12):

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

Eric Wieser (May 01 2023 at 22:22):

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

Eric Wieser (May 01 2023 at 22:22):

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

Scott Morrison (May 01 2023 at 22:23):

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

Scott Morrison (May 01 2023 at 22:24):

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 (May 01 2023 at 22:25):

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

Yaël Dillies (May 01 2023 at 22:33):

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

Yaël Dillies (May 01 2023 at 22:35):

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 (May 01 2023 at 22:37):

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 (May 01 2023 at 22:38):

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

Yaël Dillies (May 01 2023 at 22:40):

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 (May 01 2023 at 22:40):

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

Scott Morrison (May 01 2023 at 22:41):

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

Yaël Dillies (May 01 2023 at 22:42):

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

Scott Morrison (May 01 2023 at 22:52):

Oh, I didn't see this.

Scott Morrison (May 01 2023 at 22:52):

#18911

Yaël Dillies (May 01 2023 at 22:55):

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 (May 01 2023 at 23:42):

Anneuax?

Reid Barton (May 03 2023 at 13:51):

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 (May 03 2023 at 13:56):

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

Reid Barton (May 03 2023 at 13:57):

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

Jireh Loreaux (May 03 2023 at 14:25):

docs4#Mod docs4#Top

Kevin Buzzard (May 03 2023 at 17:51):

TOP? Or is this too Fortran?

Reid Barton (May 03 2023 at 17:54):

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

Kevin Buzzard (May 03 2023 at 17:59):

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

MonadMaverick (May 04 2023 at 00:25):

-- 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 (May 04 2023 at 01:05):

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

Scott Morrison (May 04 2023 at 01:06):

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

Eric Wieser (May 04 2023 at 01:10):

measure_of should be measureOf, right?

MonadMaverick (May 04 2023 at 01:47):

Eric Wieser said:

measure_of should be measureOf, right?

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

Yaël Dillies (May 04 2023 at 08:02):

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ō (May 11 2023 at 23:00):

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ō (May 11 2023 at 23:01):

/poll fg should be ported as
Fg
FG

Pol'tta / Miyahara Kō (May 12 2023 at 20:05):

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

MonadMaverick (May 17 2023 at 11:53):

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 (May 17 2023 at 11:59):

Why did we do that?

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

Mario Carneiro (May 17 2023 at 14:02):

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 (May 17 2023 at 14:12):

Do we have a #naming4 yet?

Jireh Loreaux (May 17 2023 at 17:04):

It's on the porting wiki page

Kevin Buzzard (May 17 2023 at 17:16):

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 (May 17 2023 at 17:16):

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 (May 17 2023 at 17:33):

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 (May 22 2023 at 15:27):

Shall I make a PR with the following renamings?

infNndist -> infNNDist
infEdist -> infEDist

following the naming convention of ENNReal?

Chris Hughes (May 22 2023 at 16:05):

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

Eric Wieser (May 22 2023 at 16:06):

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

Chris Hughes (May 22 2023 at 16:07):

I would say so, but maybe I misremembered the convention

Moritz Doll (May 22 2023 at 16:32):

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

Jireh Loreaux (May 22 2023 at 16:37):

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

Eric Wieser (May 22 2023 at 17:00):

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

Floris van Doorn (May 22 2023 at 20:14):

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 (May 22 2023 at 20:16):

aeEq is presumably the other option

Mario Carneiro (May 22 2023 at 20:30):

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 (May 22 2023 at 20:31):

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

Eric Wieser (May 22 2023 at 20:42):

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

Eric Wieser (May 22 2023 at 20:56):

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

Floris van Doorn (May 22 2023 at 20:58):

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 (May 22 2023 at 21:04):

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 (May 22 2023 at 21:07):

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 (May 22 2023 at 21:14):

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

Eric Wieser (May 22 2023 at 21:26):

Well enn is a modifier too...

Eric Wieser (May 22 2023 at 21:27):

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

Mario Carneiro (May 22 2023 at 21:30):

aeEq isn't a type either IIUC

Mario Carneiro (May 22 2023 at 21:31):

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

Mario Carneiro (May 22 2023 at 21:33):

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 (May 22 2023 at 21:34):

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 (May 22 2023 at 22:10):

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 (Jul 11 2023 at 14:05):

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 (Jul 11 2023 at 14:05):

The first is a Sort, the second is not.

Yury G. Kudryashov (Jul 11 2023 at 15:00):

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

Ruben Van de Velde (Jul 11 2023 at 15:08):

Wouldn't that mean it's a Sort?

Kyle Miller (Jul 11 2023 at 15:10):

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

Kyle Miller (Jul 11 2023 at 15:11):

(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 (Jul 11 2023 at 15:24):

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

Sebastien Gouezel (Jul 11 2023 at 15:47):

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 (Jul 11 2023 at 15:52):

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

Kevin Buzzard (Jul 12 2023 at 09:35):

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 (Jul 12 2023 at 09:35):

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

Kayla Thomas (Aug 06 2023 at 18:54):

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 (Aug 06 2023 at 19:04):

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 (Aug 06 2023 at 19:06):

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 (Aug 06 2023 at 19:14):

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 (Aug 06 2023 at 19:16):

(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 (Aug 06 2023 at 19:20):

Is it possible to make a linter for this?

Kayla Thomas (Aug 06 2023 at 19:24):

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

Thomas Murrills (Aug 06 2023 at 19:31):

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

Mario Carneiro (Aug 06 2023 at 19:56):

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

Kayla Thomas (Aug 06 2023 at 21:39):

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

Kayla Thomas (Aug 06 2023 at 21:44):

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

Kayla Thomas (Aug 06 2023 at 22:19):

Do I have this right?

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

?

Thomas Murrills (Aug 06 2023 at 22:23):

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 (Aug 06 2023 at 22:27):

Thank you!

Kayla Thomas (Aug 06 2023 at 22:36):

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 (Aug 06 2023 at 22:55):

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 (Aug 06 2023 at 22:57):

Thank you!

Jireh Loreaux (Aug 09 2023 at 17:41):

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 (Aug 09 2023 at 17:44):

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

Yaël Dillies (Aug 29 2023 at 14:50):

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

Jireh Loreaux (Aug 29 2023 at 15:16):

And leave docs#Filter.limsup alone, correct?

Yaël Dillies (Aug 29 2023 at 15:28):

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

Ruben Van de Velde (Sep 13 2023 at 12:59):

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 (Sep 13 2023 at 12:59):

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

Kyle Miller (Sep 13 2023 at 13:41):

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

Eric Wieser (Sep 13 2023 at 13:49):

@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 (Sep 13 2023 at 13:52):

Oh. Then I change my vote to tfae only.

Ruben Van de Velde (Sep 13 2023 at 13:53):

Exactly, thanks for clarifying Eric

Yuyang Zhao (Sep 15 2023 at 06:04):

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 (Sep 15 2023 at 06:04):

/poll leLfDecidable should be renamed to
leLFDecidable
lelfDecidable

Alistair Tucker (Oct 09 2023 at 13:21):

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 (Oct 09 2023 at 13:23):

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

Eric Wieser (Oct 09 2023 at 13:23):

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

Eric Wieser (Oct 09 2023 at 13:25):

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 (Oct 09 2023 at 13:26):

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 (Oct 09 2023 at 13:28):

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

Eric Wieser (Oct 09 2023 at 13:29):

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

Eric Wieser (Oct 09 2023 at 13:29):

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

Eric Wieser (Oct 09 2023 at 13:29):

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 (Oct 09 2023 at 13:31):

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 (Oct 09 2023 at 13:33):

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

Eric Wieser (Oct 09 2023 at 13:34):

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

Jireh Loreaux (Oct 09 2023 at 15:53):

I think there are probably a lot of these discrepancies.

Mario Carneiro (Oct 09 2023 at 16:07):

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 (Oct 09 2023 at 16:08):

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

Eric Wieser (Oct 09 2023 at 16:29):

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

Kevin Buzzard (Oct 09 2023 at 16:34):

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

Mario Carneiro (Oct 09 2023 at 16:35):

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 (Oct 09 2023 at 16:37):

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 (Oct 09 2023 at 16:39):

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 (Oct 09 2023 at 16:41):

no I mean the 'read the naming convention' answer

Mario Carneiro (Oct 09 2023 at 16:41):

Add.add is following the conventions

Mario Carneiro (Oct 09 2023 at 16:42):

LE.le and Membership.mem are not

Mario Carneiro (Oct 09 2023 at 16:43):

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

Kevin Buzzard (Oct 09 2023 at 17:02):

Oh yes of course!

Yaël Dillies (Oct 09 2023 at 18:09):

Why not just HasDvd?

Eric Wieser (Oct 09 2023 at 18:11):

Mario Carneiro said:

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

Why is there a conflict?

Mario Carneiro (Oct 09 2023 at 18:12):

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

Mario Carneiro (Oct 09 2023 at 18:12):

for notation typeclasses it is not uncommon to export them

Michael Rothgang (Nov 02 2023 at 14:32):

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 (Nov 02 2023 at 14:34):

Yes.

Michael Rothgang (Nov 02 2023 at 14:34):

Will PR later today (unless objections come up).

Michael Rothgang (Nov 02 2023 at 15:03):

Filed as #8121

Michael Rothgang (Nov 17 2023 at 11:03):

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 (Nov 17 2023 at 11:03):

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

Ruben Van de Velde (Nov 17 2023 at 11:06):

How many of those other examples? :)

Michael Rothgang (Nov 17 2023 at 11:44):

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 (Nov 17 2023 at 13:45):

I think preimage_isOpen_of_isOpen reads very nicely!

Floris van Doorn (Nov 17 2023 at 13:45):

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 (Nov 17 2023 at 13:46):

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

Ruben Van de Velde (Nov 17 2023 at 13:54):

(isOpen certainly reads nicer than is_open would have done)

Floris van Doorn (Nov 17 2023 at 14:00):

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 (Nov 17 2023 at 14:04):

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

Kevin Buzzard (Nov 17 2023 at 14:33):

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 (Nov 17 2023 at 19:04):

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 (Nov 17 2023 at 19:05):

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

Ruben Van de Velde (Nov 17 2023 at 19:06):

Is it about something called OpenCover?

Michael Rothgang (Nov 17 2023 at 19:46):

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

Ruben Van de Velde (Nov 17 2023 at 20:00):

Exactly

Yaël Dillies (Nov 17 2023 at 22:26):

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 (Nov 18 2023 at 13:45):

#8492 has three more renames

Ruben Van de Velde (Nov 30 2023 at 16:17):

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

Should this be addNSMul?

Junyan Xu (Nov 30 2023 at 16:26):

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

Ruben Van de Velde (Nov 30 2023 at 16:30):

Looks like to_additive agrees with the capitals, though

Junyan Xu (Nov 30 2023 at 16:40):

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 (Nov 30 2023 at 16:57):

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


Last updated: Dec 20 2023 at 11:08 UTC