Naming conventions for `Prop`-valued defs and classes

Stream: mathlib4

[Markus Himmel]

I'm sure that this has been discussed numerous times here, but my searching skills are failing me today. My question is: what are the rules that are applied in mathlib to decide if a prop-valued def or class should receive an Is prefix or not?

My gut feeling is: almost all of them should receive the prefix, and most of the counterexamples in mathlib (of which there are many) exist for historical reasons. There are some cases where the Is prefix is obviously nonsensical, like docs#List.Forall or docs#CategoryTheory.Limits.HasLimits.

Has anyone (perhaps one of our naming experts like @Yaël Dillies ) thought about this in more detail and would be able put their thoughts into words?

[Yaël Dillies]

I think you are mostly right, but I would add that when the predicate is clearly an adjective, one can skip the Is prefix. Eg docs#Subgroup.Normal is fine in my book

[Markus Himmel]

Aha, that indeed covers many of the cases in mathlib where there is no Is. But there are also numerous examples where we have the Is before an adjective, so mathlib is very inconsistent in this situation.

[Yaël Dillies]

My opinion about adjectives is not universal within the community and we've got some strong "All Is" proponents

[Markus Himmel]

Yes, I'm not saying that there is a problem here.

[Kyle Miller]

The HasLimits example I think is following a version of the convention, where you name the predicate using a predicate.

I think I remember some discussion that went in the direction of saying it is OK to use an adjective on its own if the word isn't also a noun.

[Winston Yin (尹維晨)]

I’m guessing IsClosed violates this to preserve parity with IsOpen, where Is is necessary.

[Kevin Buzzard]

In algebra I think that names like TopologicalRing are downright confusing.

[Christian Merten]

My favourite is docs#Algebra.Presentation and docs#Algebra.FinitePresentation :)

[Junyan Xu]

Let me remark that CategoryTheory.Limits.IsLimit is not (yet) a Prop. I think it would be nice to add a Nonempty wrapper around it, as has been done for CategoryTheory.Limits.PreservesLimit etc. (I see that Markus actually reviewed #19206)

[Bolton Bailey]

I would like an infix is operator as an alias for |> (only slightly a joke).

[Eric Wieser]

Regarding Is vs Has, I think roughly this corresponds to arity, as IsFoo Foo vs HasBar Foo Bar

[Yaël Dillies]

Shouldn't that rather be Is vs Are? eg #20911

[Kevin Buzzard]

Comments on #21472 would be very much welcome! It changes Topological(Add)Group to IsTopological(Add)Group and Topological(Semi)Ring to IsTopological(Semi)Ring.

[Peter Nelson]

If a 'MyNoun' predicate is renamed to IsMyNoun, then does lemma exists_myNoun : ∃ x, MyNoun x get renamed to lemma exists_isMyNoun : ∃ x, IsMyNoun x?

'Exists is' doesn't exactly roll off the tongue.

But like so many of these things, I mostly just want to be told what to do.

[Ruben Van de Velde]

Yes, keep the "is"

[Jon Eugster]

Kevin Buzzard said:

Comments on #21472 would be very much welcome! It changes Topological(Add)Group to IsTopological(Add)Group and Topological(Semi)Ring to IsTopological(Semi)Ring.

while I think this change looks reasonable, I would like to reiterate that in my opinion the right thing to do is to first PR any new rule to the contribution guide (source file "naming convention") and then create PRs to implement this rule. Otherwise we might run into the danger of people changing things in opposite directions in different areas. (or at different times)

[Kevin Buzzard]

Will do when I get to a computer

[Kevin Buzzard]

https://github.com/leanprover-community/leanprover-community.github.io/pull/592

Discussions very welcome! It's about time we had some kind of a convention for this. I would particularly welcome more examples of Prop-valued classes (coming for example from topology and category theory).

[Michael Stoll]

I'm in favor of adding Is or Has (as appropriate) to the names of all Prop-valued classes.

But I find it even more important to have a clearly defined convention that Mathlib follows consistently.

[Markus Himmel]

For reference, here is how the corresponding section of the naming convention for the standard library currently looks:

When defining a predicate, prefix the name by Is, like in List.IsPrefix. The Is prefix may be omitted if

• the resulting name would be ungrammatical, or
• the predicate depends on additional data in a way where the Is prefix would be confusing (like List.Pairwise), or
• the name is an adjective (like Std.Time.Month.Ordinal.Valid)

I think there are examples like docs#Specializes and docs#CategoryTheory.Limits.PreservesFiniteLimits which aren't adjectives but where Is or Has would sound really strange. docs#Specializes is interesting because Is or Has somehow (to me) suggests that the type class describes a property of a single thing, which is not the case there (though I guess you could rename it to IsSpecialization). (Nevermind, Specializes isn't a class)

[Kevin Buzzard]

Christian Merten said:

My favourite is docs#Algebra.Presentation and docs#Algebra.FinitePresentation :)

My favourite is now docs#Subgroup.Normal and docs#CategoryTheory.Subgroupoid.IsNormal (both Props)

[Riccardo Brasca]

@Kevin Buzzard I am going to do the same for docs#UniformAddGroup and friends. Do you have any tips to make the job not too painful?

[Kevin Buzzard]

I just used case-sensitive search and replace. Don't forget to deprecate the old names (I forgot this). You don't need to deprecate instance names.

[Michael Rothgang]

There's the scripts/add_depreations.sh script which should help with the second part.

[Johan Commelin]

scripts/add_deprecations.sh -- mini-typo

[Riccardo Brasca]

Thanks for the pointers. Let's see.

[Riccardo Brasca]

#23345. We only have UniformGroup and UniformAddGroup so it's not hard.

[Riccardo Brasca]

We have files like Mathlib.Topology.Algebra.UniformRing (but note that there is no class called UniformRing). Do we want to rename the file?

[Michael Rothgang]

Good question! My first instinct is "yes", but then I'm not sure what to rename it to... Is there a natural name? If not, the current name might be good enough.

[David Loeffler]

Riccardo Brasca said:

We have files like Mathlib.Topology.Algebra.UniformRing (but note that there is no class called UniformRing). Do we want to rename the file?

This file is actually all about completions of rings, so perhaps Mathlib.Topology.Algebra.RingCompletion is a better name?

[Filippo A. E. Nuccio]

(https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20conventions.20for.20.60Prop.60-valued.20defs.20and.20classes/near/507991630):

Kevin Buzzard I am going to do the same for docs#UniformAddGroup and friends. Do you have any tips to make the job not too painful?

I have a WIP PR where I am doing this, it is #23350 for @Riccardo Brasca