Zulip Chat Archive

Stream: new members

Topic: Is "nat.eq_zero_of_add_eq_zero_right" misnamed?


Kent Van Vels (Sep 15 2022 at 19:25):

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 (Sep 15 2022 at 19:38):

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

Martin Dvořák (Sep 15 2022 at 19:44):

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

Damiano Testa (Sep 15 2022 at 20:12):

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 (Sep 15 2022 at 20:13):

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 (Sep 15 2022 at 20:17):

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

Damiano Testa (Sep 15 2022 at 20:19):

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

Martin Dvořák (Sep 15 2022 at 20:23):

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

Damiano Testa (Sep 15 2022 at 20:26):

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 (Sep 15 2022 at 20:29):

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 (Sep 16 2022 at 05:17):

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 (Sep 16 2022 at 09:39):

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 (Sep 16 2022 at 10:36):

Alex, thanks for the information!


Last updated: Dec 20 2023 at 11:08 UTC