Is "nat.eq_zero_of_add_eq_zero_right" misnamed?

Stream: new members

[Kent Van Vels]

I am wondering if the nat.eq_zero_of_add_eq_zero_right (link) and nat.eq_zero_of_add_eq_zero_left (link) should have their names swapped. Since I am new, I am posting here, but if there a better place for me to post this, please let me know.

I would be happy to make the change if it is needed, I didn't see it on the issues list on the repo. Thanks.

[Martin Dvořák]

Yeah, the names are weird. But also, why is exactly one of them written as implication?

[Martin Dvořák]

Ah, only the first one is proved using pattern matching. Still, don't we want to make them look the same?

[Damiano Testa]

These lemmas are not in mathlib, right?

I think that changing them in favour of a convention that is not so well-established may be more work than is worth.

Still, if someone else feel strongly about this, feel free to say so!

[Damiano Testa]

You can also take a look at what injectivity a add_left_cancel_semigroup to see some more confusing left/right lemmas.

[Martin Dvořák]

What do you mean by "not in mathlib" please?

[Damiano Testa]

Isn't the lemma in core? The location is not src/..., right?

[Martin Dvořák]

Oh! You are right!
lean/library/init/data/nat/lemmas.lean

[Damiano Testa]

Yes, so this is a lemma that comes with Lean, even if you do not want to use mathlib. It can still be changed, but the procedure is different than opening a PR for mathlib.

[Damiano Testa]

Honestly, if I need one of these lemmas, I look them up, read the statements via autocompleting eq_zero_of_add_eq_zero, type enter when I see the one I want and not even look at whether it is left or right! :shrug:

[Damiano Testa]

Two more minor comments.

@Kent Van Vels you can link Lean declarations typing docs#nat.eq_zero_of_add_eq_zero_right (I literally typed what you see) and the link is automatically created.

@Martin Dvořák while the statements look different, I think that internally Lean converts them to similar shape. You can see this as follows:

#check @nat.eq_zero_of_add_eq_zero_left
-- nat.eq_zero_of_add_eq_zero_left : ∀ {n m : ℕ}, n + m = 0 → m = 0

#check @nat.eq_zero_of_add_eq_zero_right
-- nat.eq_zero_of_add_eq_zero_right : ∀ {n m : ℕ}, n + m = 0 → n = 0

The difference in the automatically generated documentation is probably a consequence of the fact that the parsing relies more on the actual lean file than on the internal representation of the declarations. I do not actually know how the documentation works, so I may be wrong about this.

[Alex J. Best]

I think the doc is generated from the internal representation and pretty printed rather than the source, so I'm not sure what causes lean to show them differently in this case.

[Damiano Testa]

Alex, thanks for the information!