Nat.add_sub_cancel' and Nat.add_sub_of_le

Stream: mathlib4

[Richard Osborn]

These two theorems seem to be identical. I noticed that __root__.add_sub_cancel' was deprecated, so I'm assuming Nat.add_sub_cancel' should be deprecated as well?

[Richard Osborn]

Ok, looking at #11530, it seems as the Nat version of these lemmas don't always agree with the Group versions. Nat.add_sub_cancel should be add_sub_cancel_right?

[Yaël Dillies]

There's much more to it, eg all the tsub lemmas. I'm planning on fixing all of this, but juggling the three different repos across which the lemmas are spread is exceeding my pre-exams capacity.

[Yaël Dillies]

Maybe @Kim Morrison can tell us whether renames to align with mathlib naming conventions are welcome to Core/Std.

[Kim Morrison]

Yes, I'm happy to merge renaming PRs within the Nat/Int/List/Array namespaces, as long as there's no bikeshedding in sight and obviously following the conventions as written. :-)

[Kim Morrison]

alias is not available in Lean, so deprecations are usually best done as abbrev X := @Y.

[Richard Osborn]

Ah, I totally missed that these were in Core. I can look into submitting a PR for all the lemmas that don't include m ≤ n hypotheses. Is there a consensus on what the names should be for the lemmas which require m ≤ n? Nat.sub_add_cancel doesn't mention the additional hypothesis whereas Nat.add_sub_of_le and add_tsub_cancel_of_le do mention it.

[Mario Carneiro]

@Kim Morrison said:

alias is not available in Lean, so deprecations are usually best done as abbrev X := @Y.

Can we do something about this? I know that it was skipped during the initial upstreaming due to the iff-handling part, but it is easily possible to just skip that part and only upstream the main command. I think there are many many uses of alias and @[deprecated] alias in lean core and making it easier to deprecate will help core to do it more rather than cold-turkey renames

[Kim Morrison]

This got stuck on the objection that there are too many ways to say the same thing, and we don't want both alias and abbrev, without a clear story to users about when to use each.