Naming: nmem vs not_mem

Stream: mathlib4

[Yury G. Kudryashov]

Should we use nmem or not_mem for "not a member"? Currently, not_mem is about 8x more popular, but it should be easy to switch either way.

[Bhavik Mehta]

Relatedly, should it be zero_not_mem or not_zero_mem, if the second is picked.

[Jovan Gerbscheid]

If we accept nmem for not_mem, then why not nle and nlt for not_le and not_lt?

[Kevin Buzzard]

This convention makes lemmas less human-readable.

[Jovan Gerbscheid]

Bhavik Mehta said:

Relatedly, should it be zero_not_mem or not_zero_mem, if the second is picked.

not_zero_mem seems more technically correct, but zero_not_mem sound much more natural. I guess not_mem behaves like a single atom in that regard, which is also reinforced by the notation.

[Eric Wieser]

That would suggest nmem could be an atom too

[Sébastien Gouëzel]

Notationwise, this appears as ∉, so it looks like an atom, which shouldn't have an underscore in it. So nmem is justified. Still, I agree that it is hard to guess or to understand if one is not already aware of it, so personally I would slightly prefer not_mem. The important thing is that we make a choice, whatever it is, and then fix the library and add something about this to the naming conventions file.

[Sébastien Gouëzel]

It turns out that there is a recommendation, in core:

/-- `a ∉ b` is negated elementhood. It is notation for `¬ (a ∈ b)`. -/
notation:50 a:50 " ∉ " b:50 => ¬ (a ∈ b)

recommended_spelling "not_mem" for "∉" in [«term_∉_»]

(I didn't even know about recommended_spelling!)

[Kevin Buzzard]

is someone brave enough to look at the recommended spellings of the things we've been using for years?

[Yury G. Kudryashov]

git log says that recommended_spelling was added in February 2025.

[Yury G. Kudryashov]

I fixed spelling for Ne in #24408

[Robin Arnez]

Table of all recommended spellings in core:

Declaration name	Notation	Recommended spelling
List.nil	[]	nil
List.cons	[a]	singleton
Functor.mapRev	<&>	mapRev
orM	<||>	orM
andM	<&&>	andM
Bind.kleisliRight	>=>	kleisliRight
Bind.kleisliLeft	<=<	kleisliLeft
Bind.bindLeft	=<<	bindLeft
GetElem.getElem	xs[i]	getElem
GetElem?.getElem?	xs[i]?	getElem?
GetElem?.getElem!	xs[i]!	getElem!
Iff	↔, <->	iff
HasEquiv.Equiv	≈	equiv
Subset	⊆	subset
SSubset	⊂	ssubset
Superset	⊇	superset
SSuperset	⊃	ssuperset
Union.union	∪	union
Inter.inter	∩	inter
SDiff.sdiff	\	sdiff
EmptyCollection.emptyCollection	∅, {}	empty
bne	!=	bne
Ne	≠	ne
xor	^^	xor
singleton	{x}	singleton
Prod.mk	(a, b)	mk
Function.comp	∘	comp
Prod	×	Prod
PProd	×'	PProd
HOr.hOr	|||	or
HXor.hXor	^^^	xor
HAnd.hAnd	&&&	and
HAdd.hAdd	+	add
HSub.hSub	-	sub
HMul.hMul	*	mul
HDiv.hDiv	/	div
HMod.hMod	%	mod
HPow.hPow	^	pow
HAppend.hAppend	++	append
Neg.neg	-	neg
Dvd.dvd	∣	dvd
HShiftLeft.hShiftLeft	<<<	shiftLeft
HShiftRight.hShiftRight	>>>	shiftRight
Complement.complement	~~~	not
LE.le	≤, <=	le
LT.lt	<	lt
GT.gt	>	gt
GE.ge	≥, >=	ge
Eq	=	eq
BEq	==	beq
And	∧, /\	and
Or	∨, \/	or
Not	¬	not
and	&&	and
or	||	or
not	!	not
Membership.mem	∈	mem
N/A	∉	not_mem
List.cons	::	cons
Functor.map	<$>	map
Bind.bind	>>=	bind
HOrElse.hOrElse	<|>	orElse
HAndThen.hAndThen	>>	andThen
Seq.seq	<*>	seq
SeqLeft.seqLeft	<*	seqLeft
SeqRight.seqRight	*>	seqRight
Subtype	{ x // p x}	subtype
Vector.mk	#v[]	empty
Vector.mk	#v[x]	singleton
BitVec.ofNat	0#n	zero
BitVec.ofNat	1#n	one
List.IsPrefix	<+:	prefix
List.IsSuffix	<:+	suffix
List.IsInfix	<:+:	infix
List.toArray	#[]	empty
List.toArray	#[x]	singleton

[Yury G. Kudryashov]

I'm working on nmem

[Yury G. Kudryashov]

I don't like that the recommended spelling for List.IsPrefix is prefix instead of isPrefix and similarly for IsSuffix/IsInfix, otherwise looks reasonable to me.

[Yury G. Kudryashov]

For nmem: #24409 (search&replace with confirmation + add_deprecations.sh, didn't proofread it myself yet)

[Eric Wieser]

Sébastien Gouëzel said:

It turns out that there is a recommendation, in core:

I think it's been discussed previously that various core naming conventions are actually a best effort to record the status quo in mathlib; not every one of them is a definitive ruling by core that this is the preferred choice. Would a non-binding vote between the two options be sensible?

[Yaël Dillies]

Yury G. Kudryashov said:

I don't like that the recommended spelling for List.IsPrefix is prefix instead of isPrefix and similarly for IsSuffix/IsInfix, otherwise looks reasonable to me.

If you look at the original PR adding those recommended spellings, I complained about precisely this, but my complaint was dismissed :sad:

[Yury G. Kudryashov]

Saving others some searches: it was lean#6886

[Yury G. Kudryashov]

CC: @Markus Himmel. Yael is not the only one who isn't happy about prefix vs isPrefix. For me, it's "I mildly prefer isPrefix, I would be ready to prepare a PR renaming lots of lemmas, but I don't think that it's important enough to argue about this".

[Jovan Gerbscheid]

I'd be happier with the prefix naming if the constant itself was named Prefix :)

[Markus Himmel]

A while ago there was some discussion among the standard library maintainers and we decided that we would like to

• rename Sublist to IsSublist
• scope the notations <+: etc
• use isSublist/isPrefix/... in identifiers

but we haven't had time to make this change yet. PRs to core are welcome (please request a review from me).

[Yury G. Kudryashov]

I'm going to be very busy at my day job for the next 2 weeks (and I'll be away from my desktop that can build Lean in a reasonable amount of time). If no one picks this up before than, I'll prepare a PR when I come back.

[Yury G. Kudryashov]

@Johan Commelin delegated #24409 (nmem -> not_mem) while @Eric Wieser suggests to vote about this. What should I do?

I have no strong opinion on "nmem or not_mem" but I have an opinion on "one of these everywhere vs random choice every time".

[Yaël Dillies]

not_mem is quite clearly the correct name IMO, so I am not sure it's worth voting on the issue

[Johan Commelin]

Yury G. Kudryashov said:

Johan Commelin delegated #24409 (nmem -> not_mem) while Eric Wieser suggests to vote about this. What should I do?

I have no strong opinion on "nmem or not_mem" but I have an opinion on "one of these everywhere vs random choice every time".

Sorry, I missed Eric's request. And I think his remark is very sensible. That recommended_spelling is in this case probably a best-effort attempt to document what mathlib does.

So I'm happy to vote about this.

Yaël Dillies said:

not_mem is quite clearly the correct name IMO, so I am not sure it's worth voting on the issue

Could you please layout why it is quite clear to you?

(For me: since ∉ is a single symbol, I find it quite reasonable to have an atomic naming component for it, without an embedded _.)

[Jovan Gerbscheid]

Have we considdered the fact that "nonmember" is an English word? We could introduce nonmem as the preferred spelling.

[Edward van de Meent]

xkcd 927 irl :looking:

[Yaël Dillies]

Johan Commelin said:

Yaël Dillies said:

not_mem is quite clearly the correct name IMO, so I am not sure it's worth voting on the issue

Could you please layout why it is quite clear to you?

Bhavik made it clear that I wasn't clear. I do not mean to make not_mem a single token. I mean for foo ∉ bar to be called not_foo_mem_bar, not foo_not_mem_bar

[Yaël Dillies]

Johan Commelin said:

(For me: since ∉ is a single symbol, I find it quite reasonable to have an atomic naming component for it, without an embedded _.)

"If you want it to be a single token, then make it a single token", is what I would say

[Yaël Dillies]

Of course, this disagrees with the naming of eg Fintype.sum for ∑ _, _ (as the special case ∑ _ ∈ univ, _ of the general notation), so I am happy to be swayed

[Yaël Dillies]

My order of preference would be:

1. Statu quo, no extra rule: not_foo_mem_bar
2. Extra rule that ∉ is a single token and should be named as such: foo_nmem_bar or foo_notMem_bar
3. Extra rule that ∉ is a single token made of two tokens (??): foo_not_mem_bar

[Bhavik Mehta]

In the cases where 1 and 3 differ, the PR #24409 opts for 3, which is also my preference.

[Sébastien Gouëzel]

The statu quo is 3 rather than 1, I think.

[Yaël Dillies]

Really? I've been naming all my lemmas according to 1, at least

[Filippo A. E. Nuccio]

Yaël Dillies said:

not_mem is quite clearly the correct name IMO, so I am not sure it's worth voting on the issue

In general, I find that as soon as there are more than 3 informed people with different opinions it is always worth voting.

[Yury G. Kudryashov]

Yaël Dillies said:

Really? I've been naming all my lemmas according to 1, at least

Loogle says that there are 719 theorems with not_mem and 790 with both not_ and _mem, which gives an upper estimate of 71 theorems named according to 1.

[Yury G. Kudryashov]

Though in some cases 1 and 3 give the same result, so :up: is wrong.

[Sébastien Gouëzel]

Looks like we have to vote.

[Sébastien Gouëzel]

/poll If a lemma says that 0 does not belong to foo, 0 ∉ foo, how should we name it?
zero_nmem_foo
not_zero_mem_foo
zero_not_mem_foo
zero notMem_foo

[Johan Commelin]

The space in the last option should also be _, right?

[Sébastien Gouëzel]

Yes, sorry. Looks like I can't edit, though.

[Floris van Doorn]

My preference is for nmem: if we have a notation for it, I'm happy to treat it as a declaration for naming purposes.
I like zero_not_mem_foo least out of all options so far: it treats the symbol as having the name not_mem, which would violate the fact that single components shouldn't have an underscore in their name.
(I would like to add half a vote to zero_notMem_foo.)

[Patrick Massot]

My strongest feeling is that I want uniformity here. But I also guess very few people would feel not_zero_mem_foo is natural. Breaking the ∉ feels really weird.

[Floris van Doorn]

When changing these names, please also add in the docstring of the ∉ what the preferred name for this symbol is. We should add this information to every notation that doesn't immediately correspond to a declaration (with a custom name), e.g. also for the notations for a.e.-filters which also have custom (but not consistent) names.

[Sébastien Gouëzel]

There is already recommended_spelling which shows the recommended spelling of lemmas involving the symbol when hovering. The recommended spelling is in core, though -- is it something that core would agree to amend, since apparently this was designed to follow mathlib best practices?

[Kim Morrison]

I'm a bit skeptical of this vote: I think that it artificially splits the opposition to _nmem_. But I'm saying that mostly because I really don't like _nmem_. :-)

[Yury G. Kudryashov]

It's a pity we can't easily run something like ranked choice vote here.

[Mario Carneiro]

this is approval voting though

[Yury G. Kudryashov]

It doesn't differentiate between "strong yes" and "I can tolerate that" though

[Eric Wieser]

You can edit your vote once the two are tied to express preference, but maybe that's not stable

[Markus Himmel]

Sébastien Gouëzel said:

There is already recommended_spelling which shows the recommended spelling of lemmas involving the symbol when hovering. The recommended spelling is in core, though -- is it something that core would agree to amend, since apparently this was designed to follow mathlib best practices?

Yes, core will update the recommended spelling to match the outcome of the vote here. If there is ever a disagreement (which I hope we can avoid) or any other reason for mathlib to amend the recommended spelling, it is possible to have multiple recommended spellings for the same symbol/parser and it is also possible to add a clarifying comment to a recommended spelling. So mathlib can add additional recommended spellings for notations defined in core.

[Sébastien Gouëzel]

Kim Morrison said:

I'm a bit skeptical of this vote: I think that it artificially splits the opposition to _nmem_. But I'm saying that mostly because I really don't like _nmem_. :-)

I agree that notMem is clearly better than nmem: one understands readily what notMem means (once one knows what mem is, which is easy because it's everywhere throughout the library), while nmem is barely shorter and much more cryptic. Still, in the end, we will have to follow the vote of the majority. Let's still wait 24h to give reasonable people the time to change their minds :-), and then we will proceed.

[Sébastien Gouëzel]

Kim Morrison said:

I'm a bit skeptical of this vote: I think that it artificially splits the opposition to _nmem_. But I'm saying that mostly because I really don't like _nmem_. :-)

I don't think it splits the opposition, because one can vote for several options.

[Damiano Testa]

Sébastien, you've convinced me to change my vote!