Int.coe_natAbs misnomer

Stream: mathlib4

[Thomas Murrills]

I imagine this is very, very low priority, but thought I'd mention: I think Int.coe_natAbs should be Int.coe_nat_abs. Currently coe_natAbs (n : ℕ) : |(n : ℤ)| = n, which involves abs, not natAbs. By the name, I'd expect coe_natAbs to be what Int.natAbs_cast is (natAbs_cast (n : ℕ) : natAbs ↑n = n).

[Floris van Doorn]

nice find! I expect that was an overzealous search+replace of nat_abs to natAbs. If we fix it, our naming scheme pays off my distinguishing the two :-)

[Scott Morrison]

Please PR! :-)

[Yaël Dillies]

coe_natAbs would rather be coe_natAbs (n : ℤ) : (n.nat_abs : ℤ) = |n|.

[Yaël Dillies]

And coe_nat_abs should be abs_coe_nat, so the new naming convention still hasn't helped :stuck_out_tongue:

[Anne Baanen]

Good find, I remember being mislead by this theorem name in mathlib3!

[Yaël Dillies]

#17967, mathlib4#1080

[Thomas Murrills]

I guess this might be a good time to ask: what exactly is the naming scheme that tells us that e.g. abs should come before coe? I sort of get it, but is “how to name a lemma in mathlib4” (in general) written down anywhere? (This would also help me guess the names of lemmas!)

[Yaël Dillies]

It's outermost to innermost application from left to right (with the occasional exception of predicates, which might come last, eg docs#set.nonempty, docs#function.injective). In (n.nat_abs : ℤ), int.coe_nat is outermost, and nat_abs is innermost.

[Thomas Murrills]

I see…it also seems like we omit eq_<rhs> when the rhs is “obvious” somehow?

[Yaël Dillies]

Yes. And we omit _eq/_iff when it's clear it's gonna be an equality/equivalence.

[Thomas Murrills]

Do we still write outermost first even when infix notation is standard? Or is it just eq/iff that get written “in the middle”?

[Yaël Dillies]

No, infix notation takes over the precedence convention. But there's a bit of a grey area on whether dot notation is infix.

[Yaël Dillies]

If there is no notation attached to it, I tend to say no.

[Thomas Murrills]

Neat, ok, thanks! :)

[Yaël Dillies]

But even when there's infix notation, we sometimes act as it if were a regular two arguments function and instead precise the argument using _left/_right.

[Yaël Dillies]

This is particularly useful when several infix notations are mixed and do not associate (we unfortunately don't allow brackets in lemma names :pensive:).

[Yaël Dillies]

Another source of confusion is that x.foo.bar should be called bar_foo/bar_foo_x according to the inner/outermost rule, but foo_bar visually.

[Yaël Dillies]

I strongly prefer the first convention because it does not depend on whether you use dot notation or not.