Naming convention: function application

Stream: mathlib4

[Weiyi Wang]

Recently when making PR and reading other PR, I found it unclear on the naming of theorems like the following

theorem foo_bar (a : T) : foo (bar a) = stuff := sorry

The question is whether this should be foo_bar or bar_foo. The naming convention doc doesn't seem to mention this. On the surface, it seems that it should be foo_var just as how it appears in the statement. However, consider the following

theorem foo_bar (a : T) : a.bar.foo = stuff := sorry

where the functions are defined under namespaces like T.bar: T → U and U.foo and are invoked using the dot syntax. bar and foo now appears in the reverse order in the statement, but still represents the same application order as the previous version. Should the name be kept as foo_bar?

Existing theorems in the library seem to give contradictory answers, such as Path.refl_symm and Path.symm_cast which I found when reading #27261. There are also HahnSeries.mul_coeff which is deprecated in favor of HahnSeries.coeff_mul, suggesting the foo_bar style is preferred regardless of the dot. Could we add this to the naming convention to clarify it?

[Robin Arnez]

The Lean core naming convention is a bit more precise about this: https://github.com/leanprover/lean4/blob/master/doc/std/naming.md; I guess most of what's written there applies to mathlib similarly, so yeah foo_bar regardless of dot notation.

[Robin Arnez]

But it would probably be good to make this clear in https://leanprover-community.github.io/contribute/naming.html as well

[Eric Wieser]

Does the latter link the former anywhere?

[Weiyi Wang]

:joy: I didn't know the existence of the core naming convention doc

[Eric Wieser]

I don't know if we want to commit to something as strong as the core guidelines taking precedence, but we could add a sentence like "if your question isn't covered here, look at the core guidelines"

[Robin Arnez]

Eric Wieser schrieb:

Does the latter link the former anywhere?

I don't think so, I believe the core naming convention doc got written later

[Yaël Dillies]

The core naming convention is (more or less) the understanding of the mathlib naming convention by the core devs

[Yaël Dillies]

This means that the mathlib naming convention takes precedence AND pushes the core naming convention to adapt (with someone from core approving the change, obviously)

[Yaël Dillies]

Note: I am not a core Lean dev, but I've been through several iterations of the above process

[Kim Morrison]

Certainly the Mathlib naming conventions take precedence for Mathlib, and the core naming conventions take precedence for core. But we would like these to be in sync as much as possible! It makes life easier for everyone.