Naming convention: f (k + 1) <= f k + 1

Stream: lean4

[Siddharth Bhat]

Consider the theorem:

theorem foo {k : Nat} {f : Nat → Nat} : f (k + 1) ≤ f k + 1 := sorry

What's the name of this theorem supposed to be? As far as I can tell, the "naming algorithm" says f_succ_le_f_succ, which is a bit nonsensical :)

[Floris van Doorn]

I assume you're asking this in the case that f is a specific function/declaration? Yes, our naming convention would indeed prescribe the name you suggest, but there is some flexibility. It would be easier if there is a mathematical term for this behavior "f - id is non-increasing", and then just use that term (in the same way, add_comm is not called add_eq_add).

[Sabbir Rahman]

That will probably be named f_succ_le_succ_f since in rhs, the succ happens after applying f.

[Ruben Van de Velde]

Sounds more like f_add_one_le_f_add_one

[Kim Morrison]

Yes, despite their persistence in names, I'd encourage everyone to avoid using succ to mean plus one. Only use it when you are really talking about the inductive definition of Nat.

[Martin Dvořák]

You mean use add_one instead of succ in the names of constants? Or avoid calling .succ in the code?

[Ruben Van de Velde]

Why not both :)

[Yury G. Kudryashov]

Kim meant "use succ in the name only if you use Nat.succ in the code". But the normal form is n + 1.