names distinguished only by case

Stream: mathlib4

[Reid Barton]

We found the following names in mathlib3 that are distinguished only by case:
docs#set docs#Set
docs#seq docs4#Seq (Seq is Lean 4's has_seq)
docs#asymptotics.is_o docs#asymptotics.is_O
docs#bilin_form.is_ortho docs#bilin_form.is_Ortho, also linear_map.
docs#sup_hom docs#Sup_hom, also inf/Inf
docs#cauchy docs#Cauchy
docs#probability_theory.indep docs#probability_theory.Indep, also indep_fun, indep_set

[Reid Barton]

The sup/Sup one we can resolve by using Sup/Sup_whatever.

[Reid Barton]

For others, we might need to invent some new names

[Reid Barton]

cauchy could become filter.cauchy.

[Patrick Massot]

The big O/little o one is a terrible blow for Lean 4's casing convention. Maybe we need to start over with a different convention.

[Rémy Degenne]

The Indep/indep names and variants in probability theory were chosen to follow the example of the set definitions Union/union, Inter/inter, etc.(that is use capital letter for an indexed family, small letter for two arguments). They can be changed to use whatever new convention is chosen to replace Union/union.

[Reid Barton]

And is_ortho too

[Lukas Miaskiwskyi]

Patrick Massot said:

The big O/little o one is a terrible blow for Lean 4's casing convention. Maybe we need to start over with a different convention.

Would "BigO" and "SmallO" be too off-putting? It's more verbose than a single letter, but I feel like that might not be so bad.

[Reid Barton]

There is notation for these already. So it is mainly a question of what appears in lemma names

[Calvin Lee]

submit a new character proposal to the Unicode consortium for an upper-case small letter "o"?

[Reid Barton]

Like ᴏ?

[Reid Barton]

LATIN LETTER SMALL CAPITAL O

[Kyle Miller]

For what it's worth, big-O and little-o are technically actually Ο and ο (big omicron and little omicron), which are at completely different unicode codepoints.

[Calvin Lee]

Reid Barton said:

LATIN LETTER SMALL CAPITAL O

oh right, smallcaps. that would work :smile:

[Patrick Massot]

Lukas Miaskiwskyi said:

Patrick Massot said:

The big O/little o one is a terrible blow for Lean 4's casing convention. Maybe we need to start over with a different convention.

Would "BigO" and "SmallO" be too off-putting? It's more verbose than a single letter, but I feel like that might not be so bad.

Don't worry, we'll find a way. I was joking.

[Eric Wieser]

I'm confused, there is no docs#Seq is there?

[Reid Barton]

No but there is docs4#Seq

[Eric Wieser]

Oh right, the point being that there is no obvious choice of Mathlib4 name for the old seq

[Trebor Huang]

As a tangent: Omicron means "small o", the big O is actually Omega

[Yury G. Kudryashov]

We also have docs#lim and docs#Lim

[Yury G. Kudryashov]

I'm using lim_under and lim for now

[Yury G. Kudryashov]

These defs are very rarely used in mathlib.

[Patrick Massot]

Trebor Huang said:

As a tangent: Omicron means "small o", the big O is actually Omega

No, big O and Omega are different.

[Trebor Huang]

I mean literally interpreting the greek name, not related to the big O notation thing

[Jireh Loreaux]

?? big and little omicron exist (and look like O and o), but the big and little omega are Ω and ω. So I don't understand your claim here.

[Mario Carneiro]

He's saying that omicron means "o micron", that is "small o", and similarly "o mega" means "big o" in greek

[Jireh Loreaux]

Ah, got it.

[Yury G. Kudryashov]

Probably, we should add Coprod to the list of exceptions.

[Thomas Murrills]

I think the weird thing here is that big O and small o are really just standalone “symbols” rather than “spelled” alphanumeric names (that is, their names are given by the glyphs themselves rather than what words those glyphs spell)…so imo they should either

1. be described alphanumerically (BigO and SmallO, as suggested earlier)

2. be referred to as 𝑂 and 𝑜 (to use a glyph that’s distinct from alphanumeric characters)

[Yury G. Kudryashov]

BTW, is it hard not to replace Iic etc with iic etc in lemma names in mathport?

[Yury G. Kudryashov]

When I'm porting a file about intervals, I start with searches like _i -> _I (ask y/n)

[Jireh Loreaux]

Yury, a regexp search and replace does this instantly with no need for yes/no. i\([ico]\)\([ico]\) and just map it to I\1\2. Of course, if mathport can do it easily all the better.

[Jireh Loreaux]

This could have false positives, but I think they are relatively unlikely.

[Yury G. Kudryashov]

Sometimes there is ici in a word.

[Jireh Loreaux]

Yes, but I think it's easier to just hope and catch the ones that stick out after the fact, because a stray I completely out of place will be easy to catch.

[Jireh Loreaux]

Even icc is possible, just not terribly likely.

[Yury G. Kudryashov]

I prefer to do this search (and some similar searches) in the y/n mode.

[Jireh Loreaux]

Fair enough

[Yury G. Kudryashov]

E.g., sUnion -> union_s, then Union -> union_i (it is not replaced automatically in some dot notation and simp/rw)

[Johan Commelin]

Yury G. Kudryashov said:

BTW, is it hard not to replace Iic etc with iic etc in lemma names in mathport?

We would need to update the decapitalize function in mathport. Shouldn't be too hard.

[Johan Commelin]

I need to give a seminar talk this morning. After lunch I'll be back

[Reid Barton]

I know I've seen this Icc decapitalization happening, but can you point to a specific example?

[Yury G. Kudryashov]

E.g., I fixed a lot of these in !4#1820

[Notification Bot]

Eric Rodriguez has marked this topic as resolved.

[Notification Bot]

Eric Rodriguez has marked this topic as unresolved.

[Eric Rodriguez]

Oops, sorry.

[Reid Barton]

Thanks, I will look into it.

[Reid Barton]

https://github.com/leanprover-community/mathport/pull/225

[Reid Barton]

Here are some more name/name parts that are not necessarily distinguished by capitalization, but were nevertheless capitalized in Lean 3:

• End, as in e.g. docs#module.End_algebra_map_is_unit_inv_apply_eq_iff
• C and X, as in polynomials

[Eric Wieser]

I guess End should be lower-cased for the same reason Int is in docs4#Sum.elim_intCast_intCast

[Eric Wieser]

Or we should move that into the Module.End namespace

[Reid Barton]

FWIW I think the logic behind the Lean 3 name is that, on paper, you would never write $\mathrm{end}$, and you would also never say "end".

[Yury G. Kudryashov]

Isn't end a reserved word? I see, you're talking about parts of larger names.

[Jireh Loreaux]

I'm now porting the asymptotics file, so we need to make decisions regarding is_O and is_o. I like Thomas's suggestions here below, but if I had to choose one I would go for different glyphs. Can we have a brief discussion and then a poll?
Thomas Murrills said:

I think the weird thing here is that big O and small o are really just standalone “symbols” rather than “spelled” alphanumeric names (that is, their names are given by the glyphs themselves rather than what words those glyphs spell)…so imo they should either

1. be described alphanumerically (BigO and SmallO, as suggested earlier)

2. be referred to as 𝑂 and 𝑜 (to use a glyph that’s distinct from alphanumeric characters)

[Jireh Loreaux]

For glyphs that I think would be nice I suggest 𝓞 and 𝓸 (\MCO and \MCo).

[Jeremy Tan]

For ease of typing I'd go for spelling out bigO and littleO (which from my experience on Maths Stack Exchange is more prevalent than smallO)

[Eric Wieser]

I don't think that's a strong argument, we can always make \bigO type whatever glyph we pick

[Jeremy Tan]

The calligraphic Os I equally like though

[Jeremy Tan]

I've sometimes used them in my MSE answers

[Jeremy Tan]

(but usually only if the question also uses the same style for the Os; obviously, that site being TeX-based, and there being no universal formatting style, typing a plain O is much faster than typing \mathcal O)

[Kevin Buzzard]

Note that we're already using 𝓞 in locale number_field to mean "ring of integers". There is a nonzero chance that an analytic number theorist might want to use big-O notation and number fields at some point in the future.

[Jireh Loreaux]

Thanks Kevin, do you have an alternate suggestion for big/little O?

[Jeremy Tan]

Still, my heart is going with spelling the symbols out

[James Gallicchio]

(.. Something about using calligraphic O's for the actual definition names feels .. wrong .. bigO and littleO seems fine for the definitions, and if there's interest in calligraphic O's then we can have them as notation..)

[Jireh Loreaux]

Note, we have docs#mem_ℓp and docs#measure_theory.mem_𝓛p

[James Gallicchio]

my heart still trembles a little at the thought of forgetting which font O means big O :stuck_out_tongue:

[Jireh Loreaux]

That's fixed by just having \bigO for input.

[Jireh Loreaux]

Oh, interestingly Kevin, since this isn't notation it shouldn't actually conflict, but someone tell me if I'm misunderstanding parsing.

[Jireh Loreaux]

(Although I admit it would be confusing.)

[Kevin Buzzard]

Jireh Loreaux said:

Thanks Kevin, do you have an alternate suggestion for big/little O?

I am hoping that this is one of those questions where we can just make some random decision and then if people are annoyed by it we can change it later :-)

[Eric Wieser]

I agree with Jireh, I don't expect there to actually be a conflict

[Eric Wieser]

Kevin Buzzard said:

There is a nonzero chance that an analytic number theorist might want to use big-O notation and number fields at some point in the future.

To such a theorist, are both symbols "big O"?

[Jeremy Tan]

I always type the ring of integers in LaTeX as O_K

[Jeremy Tan]

So for me, it is not true that both symbols are \mathcal O

[James Gallicchio]

one other small point of contention for including symbols in definition names: docgen search doesn't know of the equivalence of "big O" and \bigO, and it seems very complicated to support

[Jireh Loreaux]

I get around that input problem with m17n-lean, but I understand it isn't for everyone.

[Yaël Dillies]

James Gallicchio said:

bigO and littleO seems fine for the definitions

I think this is the best suggestion so far.

[Kevin Buzzard]

I think the reason we're not using $\mathcal{O}_K$ in Lean number theory to mean the integers of $K$ is simply that we were unable to make this notation work. In algebraic geometry we also use $\mathcal{O}_X$ to mean the structure sheaf of the scheme $X$, and when I was doing some sheaves of modules stuff in my alg geom graduate lectures I used

notation `𝓞_ ` X := λ (U : (opens (X : TOP))ᵒᵖ), X.presheaf.obj U

so I could at least write 𝓞_ X. Eric, regarding analytic number theorists interested in number fields -- I would imagine that the context always made things completely clear in practice.

[Jeremy Tan]

The only conceivable theorem I can conceive regarding analytic num-theorists working on number fields is Chebotarev's density theorem

[Thomas Murrills]

for my two cents, I think it would be much nicer to use glyphs! it’s easier to read—less visual clutter, closer to what you’d expect in math—and about as easy to type.

I also think Unicode mathematical italic O might be worth revisiting; using $O$ for big O notation is at least as common as (or more common than?) using $\mathcal{O}$, in my experience, and it’s surprisingly distinctive (at least to my eye) among monospace characters (foo bar 𝑂 (n^2 + 50) a x 𝑜 n).

I don’t have a strong notion of whether it should be the actual identifier or notation, though. Notation would solve the docs problem, but at the cost of essentially two identifiers for the same thing. But as a mathematician, my personal preference would be for it to at least be a glyph in one way or another. :)

[Jireh Loreaux]

Thomas, I didn't choose those because they aren't valid tokens (according to my Lean setup).

[Thomas Murrills]

Oh, that’s strange.

[Eric Wieser]

To be clear, we're talking about is_𝒪 not 𝒪 by itself, right?

[Jireh Loreaux]

Right, it should be is𝓞 because it's a Prop.

[Eric Wieser]

So I don't think it makes sense to make it notation

[Jireh Loreaux]

Well, we do have notation for it too.

[Eric Wieser]

Although we also have =O[f] notation somewhere, right?

[Eric Wieser]

Regarding the docs; in mathlib3, the doc search looks in docstrings, so that should find "big O"

[Jireh Loreaux]

f =O[l] g means is𝓞 l f g

[Jireh Loreaux]

Of course, we could change the glyphs in the notation too, but this isn't as pressing.

[Eric Wieser]

Perhaps the existence of notation is an argument against using the short names

[Eric Wieser]

We could have had a lemma «+» _comm but we decided to call it add_comm instead

[Thomas Murrills]

Tangent, but…why isn’t e.g. 𝑜 a valid token? Wouldn’t we expect it to be? (Maybe this should be a new thread…)

[James Gallicchio]

It works fine as notation, interestingly. Not sure what characters are allowed in identifiers.

[Thomas Murrills]

Poked around a bit—I guess it’s simply not in the Unicode blocks specified in src/Init/Meta.lean. (Its exclusion doesn’t seem accidental since adjacent blocks are included, so I figure a conscious decision was made at some point.)

[Jireh Loreaux]

/poll naming for is_O, is_o and is_O_with
Is𝓞, Is𝓸, Is𝓞With
IsBigO, IsLittleO, IsBigOWIth

[Jireh Loreaux]

Note that the above poll is just for naming not for notation. If we want to consider any changes in notation that can be a separate poll (but there is no need for new notation currently).

[Jireh Loreaux]

The poll seems a little one-sided :sweat_smile:, so I've pushed to !4#3393 with the changes. It's ready for review.