naming convention: `symm` in lemmas generated by `@[simps]`

Stream: mathlib4

[Jireh Loreaux]

When @[simps] generates lemmas abut symm it appends symm, as in, foo_symm_apply or foo_symm. However, this essentially treats symm as if it were an infix operator, but it's not. Moreover, when we write lemmas about symm by hand, we (try to) express foo.symm as symm_foo in the declaration name because that's our rule for dot notation.

What do we want to do about this? I think the discrepancy causes inconsistency across the library, even in lemmas named manually, whether they correspond to simps lemmas or not.

[Floris van Doorn]

It is possible to change this in @[simps], with e.g. initialize_simps_projections Equiv (as_prefix symm), so it is purely a question what we want the naming to be.
I write Equiv.symm e usually using projection notation, i.e. e.symm and so far we have not made firm rules whether such names should be written as prefix or as postfix.

[Floris van Doorn]

I must say that I've gotten very used to foo_apply and foo_symm_apply, and that changing it will be a big change.

[Floris van Doorn]

Jireh Loreaux said:

we (try to) express foo.symm as symm_foo in the declaration name because that's our rule for dot notation.

Have we made this into a firm rule by now?

[Jireh Loreaux]

I thought this was pretty much decided, yes.

[Thomas Murrills]

(Note that we could also have @[simps] generate the old naming as an alias and tag it as deprecated in favor of the new naming, so that this change is no worse than deprecating a bunch of lemmas :) )

[Andrew Yang]

I thought this was pretty much decided, yes.

Is this true?

As in, yes in general dot notations do not affect naming conventions but there are some exceptions in practice. In particular, the .symm I see are almost always treated as suffixes. Do we have a consensus in this particular case?

[Eric Wieser]

I think given we have an exception for _injective we could also have one for symm

[Bhavik Mehta]

Note that there are quite a lot of exceptions to "dot notation is prefix" in practice, some because of simps and many predating it, eg Functor.obj and Functor.map are always written "infix". Looking through mathlib, it certainly seems that the vast majority of hand-written lemmas about foo.symm are named foo_symm; and of course the [simps]-generated ones are written this way too, out of the first 50 files which contained "symm_" I looked at, I could only find two where the "prefix rule" was ever followed, and the first 200 searches in loogle for "symm_" are almost all actually using it as a suffix, with symm_mk cases as the only exceptions.

Based on the patterns used in practice in mathlib, and the fact that dot notation is here to stay, I think we should reconsider if prefix-only should really be applied in every case.

[Jireh Loreaux]

I think you'll find that there are a bunch of inconsistencies. In particular, I think that the simp lemmas involving Equiv.toWeakerEquiv.symm are mostly named with prefix notation.

So, my primary issue with making symm an exception is that ... it's an exception. It's one more extra rule to remember. If we had a reasonably reliable automatic declaration naming tool into which we could program all these exceptions, then this wouldn't be so much of a problem, but we don't.

But admittedly, I think symm makes more sense as an exception than injective.

[Bhavik Mehta]

I don't disagree that there are inconsistencies, but I think they are proportionally very rare: every search I can think to do shows overwhelming majority for suffix notation. For instance, lemmas about MulEquiv.symm, especially those coercing to Equiv first, use suffix notation on the whole: https://loogle.lean-lang.org/?q=Equiv.symm%2C+MulEquiv%2C+%22symm%22, whereas looking at a pattern which I think captures what you describe only shows a small number of examples: https://loogle.lean-lang.org/?q=%22.symm_%22%2C+Equiv.symm+_+%3D+_. But maybe I'm misunderstanding what you mean? I'd be very interested to see figures backing up some of these claims.

If we had a reasonably reliable automatic declaration naming tool into which we could program all these exceptions, then this wouldn't be so much of a problem, but we don't.

I would argue that @[simps] is this naming tool!
My preference is that we should name according to the order the pretty-printer displays things, since this is closer to left-to-right, easier for beginners, and closer to what mathlib mostly does already, especially for projections.

[Sébastien Gouëzel]

I think our life would be much simpler if we had no exception. Dot notation is a function application, so I'd put it in the usual way we write function applications, i.e., to the left, with prefix notation. And I'd be very very happy to kill the exceptions we have for monotone, injective and friends, for which I don't see any good reason.

[Kevin Buzzard]

I also think that "I am used to X" is a weak argument for not changing X -- for example I was used to Lean 3's capitalisation conventions but nobody was arguing that we should keep them in mathlib4.

[Jireh Loreaux]

Bhavik, I will certainly admit that postfix symm is more prevalent, especially due to simps. And yes, simps can be used to help with consistency, but it doesn't satisfy my requirements because we still manually name lemmas not generated by it.

But the question is not, "what do we currently do?", it's "what should we do?". And, like Sébastien Gouëzel, I would prefer if we had no exceptions.

[Jireh Loreaux]

But to give an example of what I meant: we have docs#ContinuousLinearEquiv.toLinearEquiv_symm and docs#ContinuousLinearEquiv.symm_toLinearEquiv which are the exact same statement but the latter is deprecated.

[Jireh Loreaux]

And I think this is a perfect example of why there should be no exception. If you create an exception for symm would to also want it for toLinearEquiv? And if not, what is the correct name of the lemma above?

[Jireh Loreaux]

We decided to use prefix for dot notation (even specifically in reference to symm!) in the thread where we decided the simp normal form for these kinds of lemmas (i.e., whether the symm moves inside or outside).

[Bhavik Mehta]

My argument is as follows:

• The convention that I'm in favour of is "read left-to-right of what the pretty-printer says". Currently symm as prefix is an exception to this, and I'm arguing that this exception should be removed, for exactly the reasons described above.
• The proposed alternative convention "function application order" already has an exception for infix notation, so it would end up with more exceptions than the reading order convention.
• Changing mathlib lemmas to be "function application order" convention would involve _massive_ amounts of deprecation, particularly in category theory where the left-to-right convention is used almost exclusively.
• The left-to-right convention is easier for beginners to read, since it's trivial to read off from a human-written or Lean pretty-printed declaration.

It's clear I'm outvoted here, so I won't press on this much further, but I'm really struggling to parse the arguments I'm being presented with.
If the argument is "there shouldn't be exceptions", it seems to me that the clear winner is "left-to-right" rather than "suffixes except when it's an infix notation", especially since notation can be scoped.
If the argument is that "we shouldn't change things", the only explicitly written rule in the mathlib convention is that infix notation is named infix, that predicates are written prefix, and that some dot-notation predicates are written suffix. All of these are consistent with the "left-to-right" convention, and become justified. The rule used in practice in mathlib, as I mentioned above, is more commonly to use left-to-right rather than to special-case dot notation to be written as prefix. This applies even to the case that Jireh mentions, where symm is special-cased in the minority of cases to be prefixed, and I think this prefix special case is what we should eliminate. And this applies especially in category theory, where things like Functor.obj is never written as a prefix.

[Aaron Liu]

Bhavik Mehta said:

• The left-to-right convention is easier for beginners to read, since it's trivial to read off from a human-written or Lean pretty-printed declaration.

The pretty printer doesn't always agree with what the human writes though

[Bhavik Mehta]

That's fair, but in the vast majority of cases it does, and the convention is still unambiguous.

[Aaron Liu]

I don't know about that

[Aaron Liu]

the pretty printer isn't exactly something I would call consistent

[Sébastien Gouëzel]

@Bhavik Mehta, how would you call the following lemma?

import Mathlib

lemma foo (m n : ℕ) : Nat.factorial (m + n) = 0 := sorry

It pretty-prints as (m + n).factorial = 0, so should it be add_factorial? And then when you open Nat it pretty-prints as (m+n) ! = 0, and then there's no way to know if factorial is prefix or postfix. I'd say that factorial_add is better, whatever the pretty-printer says, because it's the function factorial applied to an addition.

[Bhavik Mehta]

I would name it add_factorial, which is consistent with what the pretty printer says in both scopes.

[Bhavik Mehta]

In particular, I think the rule "functions are prefix, except for infix notation which is infix" is an exception which we don't need to have, and complicates things.

[Weiyi Wang]

I remember opening a thread the other day about naming for dot notation and the consensus there was always writing as prefix regardless how it is pretty printed. Let me find it...

[Bhavik Mehta]

I realise my opinion may be a minority one, so I won't block things. But the new convention being proposed here has quite a few more exceptions, requires parsing the statement, and will require thousands of deprecations, and it's not clear to me that all of these are worth it.

[Sébastien Gouëzel]

For another somewhat artifical example, mixing usual functions and dot notation,

lemma foo (m n : ℕ) : Nat.log 2 ((m + n) !) ≤ m + n := sorry

It would feel very strange to me to name this log_add_factorial_le_add and not log_factorial_add_le_add.

[Jireh Loreaux]

Bhavik, I'm not sure whether yours in the minority opinion or not. It's simply not clear to me. And even if it is the minority opinion, I still (even especially) want to hear it from you.

Bhavik Mehta said:

• The proposed alternative convention "function application order" already has an exception for infix notation, so it would end up with more exceptions than the reading order convention.

The difference with infix notation, in my opinion, is that there is essentially no easy way to write it in prefix notation. E.g., to write a + b, you would have to know that + is not just add or even Add.add, but docs#HAdd.hAdd, and so I consider this an implementation detail. In contrast, Equiv.symm f, f.symm and, if the expected type is known, .symm f are all valid spellings, even if the f.symm is the most commonly used.

[Weiyi Wang]

(The other thread I had https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Naming.20convention.3A.20function.20application/with/533593944)

[Jireh Loreaux]

Factorial is a bit of an odd beast because it's one of the few postfix notations. However, unlike ⁻¹, which has the same issues the infix notations, it's just scoped notation, so I think it makes sense to refer to it in prefix form (although I can sympathize with people reading it at the end and then putting it there).

[Jireh Loreaux]

Interestingly, we have star which is one of the few "notation typeclasses" without any associated notation, even though normally on paper it receives a postfix notation. As a result, we refer to it in prefix notation in declaration names.

[Bhavik Mehta]

Jireh Loreaux said:

The difference with infix notation, in my opinion, is that there is essentially no easy way to write it in prefix notation. E.g., to write a + b, you would have to know that + is not just add or even Add.add, but docs#HAdd.hAdd, and so I consider this an implementation detail. In contrast, Equiv.symm f, f.symm and, if the expected type is known, .symm f are all valid spellings, even if the f.symm is the most commonly used.

I'm not sure this pattern applies in every case: HAdd.hAdd a b vs a + b seems about the same compared to Functor.obj F X vs F.obj X, and as you say the dot-notation one is used far more often in practice. And for many infix notations, particularly those not powered by notation typeclasses, the difference seems even smaller to me, eg Matrix.mulVec. Note that the same "easy way to write it" discussion was mentioned last time: #mathlib4 > Naming convention for structure projections and dot notation @ 💬; although the definition of Functor has changed since then, so it's not clear if my counterargument is as strong

[Jireh Loreaux]

If nothing else, this entire discussion has convinced me that we don't follow any of our own rules! This is somewhat tongue-in-cheek, of course.

[Andrew Yang]

Can I propose the rule to be "function composition order unless clearly documented in the docstring to be otherwise", at least for now? This should be far easier to achieve (requiring way less renames) and is already substantially better than the status quo.

[Bhavik Mehta]

Does that mean adding this documentation to (almost) all the projections currently fed into simps? I agree this requires way less renames, but it's still not a small or local change, there's still quite a lot of things to adjust.

[Andrew Yang]

Or perhaps we could do "function composition order except structure projections unless clearly documented in the docstring to be otherwise".
My point is I that I haven't seen a universal convention that is satisfying (to me) in this thread and it seems quite likely to me that this conversation will die down before such an ideal convention is reached. So to me it seems more useful to think instead about whether there are (perhaps suboptimal) rules that people can agree to easily and is easily enforceable and can drastically improve the status quo already.

[Christian Merten]

It seems to me that at least we have general consensus on removing the exceptions for the prominent violations of Andrew's suggested rule: The suffixing of _injective, _surjective, _montone, etc. that are documented in https://leanprover-community.github.io/contribute/naming.html#predicates-as-suffixes. Is this correct?

[Kenny Lau]

what is function composition order?

[Jireh Loreaux]

@Christian Merten I will have a detailed proposal tomorrow.

[Jireh Loreaux]

For anyone who hasn't read #mathlib4 > Naming convention for structure projections and dot notation @ 💬 which is a recent, but older thread on essentially the same topic, please do so.

Yesterday I had a bit of a back-and-forth with Bhavik about this. By the end of it, I think I/we managed to come up with a set of guidelines which we might be able to canonize in the naming conventions on the website, if there is consensus here.

The suggested convention

Functions, whether structure projections, expressed as dot notation, or otherwise, are included in declaration names in prefix form subject to the following exceptions regarding notation.

1. Globally available infix/postfix notations are written in infix/postfix form in declaration names. Common examples include + or ⁻¹.
2. Scoped infix/postfix notations are written in infix/postfix form if and only if the docstring for the declaration (and also the notation) explicitly specifies this.
3. Local infix/postfix notations are always written in prefix form, so this is not an exception to the rule.

The purpose of the rule for scoped notations is to strike a balance between the following competing interests:

• some declarations (e.g., Matrix.mulVec) are almost never written without their (scoped) notation, and so it would be counterintuitive to write them in prefix form.
• in an ideal world, whether or not a given scope is open shouldn't dictate naming conventions, especially since newcomers may not even know about the existence of such a scope.

In addition, by requiring scoped notations to opt-in to being written in infix/postfix form in declaration names, it allows for community discussion (in the form of the PR review process) about whether any particular notation should be granted that status.

Finally, the opt-in requirement prevents the necessity of renaming thousands of lemmas only to introduce some new scoped infix/postfix notation for something with a large existing API. For example, suppose that at some point we introduce some scoped notation for star. We could choose not to opt-in to naming it with postfix form, and thereby not need to rename all existing lemmas about star (which currently use it in prefix form because it has no scoped or global notation).

Some potential issues

Infix operators without notation

Bhavik Mehta said:

What happens for operators which are used as infix, but without notation, such as docs#Nat.choose, or docs#Finset.image? In other words, these are often written as n.choose m or s.image f. My worry with this direction is that we end up with a ton of exceptions.

The other issue I have with this is that names end up longer, because of _left _right showing up, eg (a+b).choose a and c.choose (a+b) would be choose_add_left and choose_add_right, instead of add_choose vs choose_add

The answer here is that we don't make exceptions for things like docs#Nat.choose, but optionally, one could introduce scoped notation for Nat.choose, and then opt-in to writing it in infix form in docstrings.

Thousands of deprecations

As has been pointed out earlier in this thread, making a change of this sort would lead to hundreds or maybe even thousands of deprecations (e.g., fixing all the symm lemmas generated by simps). While this is a real cost, I think at some point we'll have to pay it in the name of consistency (for whatever direction we end up choosing).

Postfix, and at least one existing exception

While Bhavik and I mostly agreed on the above ideas for infix notation, we thought that postfix notations might be a bit different (despite the fact that in the proposal above I included them). For instance, ⁻¹/inv is always postfix in naming, but ᶜ/compl is often prefix in naming, despite the fact that it is globally available. Likewise, I'm not sure whether we refer to ˣ/units as prefix or postfix in naming. I think that it doesn't actually arise that often because the type is implicit / unnamed. Postfix notations are much less common, so we could opt not to specify their behavior, but I think this is just a recipe for inconsistency, which is why I included them in the proposal above.

[Jireh Loreaux]

One note: personally, I would prefer if we could abolish the existing explicit exceptions to the prefix rule, namely, injective, inj, surjective, bijective, monotone, mono, strictMono, antitone, strictAnti. However, we could also choose to leave these in place (or at least defer abolishing them to a later date).

[Sébastien Gouëzel]

Could you say explicitely what the proposed convention says about symm or toLinearEquiv or things like that? They're not notation, so maybe they're just not in the scope of the proposal?

[Andrew Yang]

I believe this falls in the "Infix operators without notation" category? But I agree less with this decision (in an otherwise great proposal!). I think it is useful to allow the same flexibility as scoped notations here.

[Jireh Loreaux]

That's handled in the first sentence: they get prefix naming.

[Yakov Pechersky]

I am not trying to bikeshed with the following comment, rather, provide context. If I recall correctly, one reason that we had the postfix use of injective etc is so that completion assistance (from the editor) provides a way to see what types of declarations are available for some construction/definition. If I have a frobinate function, typing frobin... gives completion suggestions which help with discoverability of the API landscape. Specifically, characterizations of a function's injectivity etc are such basic elements of the API that discoverability via completion is a boon.

That being said, one can make the argument that prefix naming consistency would also achieve discoverability by the virtue of: if frobinate is injective, you can be sure it is declared as injective_frobinate.

[Jireh Loreaux]

The only way to get an exception to the prefix rule under the proposal is to have an associated notation which is either globally available, or scoped and opted-in

[Yakov Pechersky]

Yes, I was just trying to explain my understanding of the history of how we got to the current exceptions.

[Jireh Loreaux]

Sorry, I was still answering Sébastien's question

[Yakov Pechersky]

Symm does have a postfix notation, when considering automorphisms

[Jireh Loreaux]

That's not literally notation for symm though, butinv, right?

[Bhavik Mehta]

While I don't think this is the optimal convention (eg it doesn't address the salience/discoverability points made by Yakov and Johan), it's certainly better than what we currently have, so thanks for writing it up! And I think it's clearly better to have something agreed upon than nothing at all.

My only comment is on

making a change of this sort would lead to hundreds or maybe even thousands of deprecations (e.g., fixing all the symm lemmas generated by simps). While this is a real cost, I think at some point we'll have to pay it in the name of consistency (for whatever direction we end up choosing).

where I think it's worth noting that this is very easily in the thousands, since just the two data fields for CategoryTheory.Functor together give 4000 deprecations: https://loogle.lean-lang.org/?q=%22_obj%22%2C+CategoryTheory.Functor.obj; https://loogle.lean-lang.org/?q=%22_map%22%2C+CategoryTheory.Functor.map. As such, I'd be interested to hear from some of the current frequent users of the category theory library on this change.

[Robin Carlier]

Note that the issues in CategoryTheory goes beyond just Functor. The fields of eg Iso and NatTrans, and many other structures that appears in this part of the library are usually written as postfix in declaration names (partly because we rely extremely heavily on [simps], and I imagine try to be consistent with what it generates).

At this point, we're probably talking about deprecating almost all of the names in that part of the library.

[Floris van Doorn]

Prod.fst and Prod.snd have no special notation, although it feels like they do, since they're most commonly written as .1 and .2. Do we want to keep naming these two declarations with the postfix naming scheme? (I hope yes.)