renaming basic Group(WithZero) lemmas

Stream: mathlib4

[Floris van Doorn]

We have some bad lemma names for Group(WithZero) lemmas.
@Yaël Dillies made a PR in #11530 to improve the situation. I like the logic of the new names, but since it's a pretty big change, I would like to see if someone has another suggestion, and to have some more visibility for this. And e.g. mul_div_cancel will refer to a very different lemma.

From the PR description:
each big row contains the multiplicative statement, then the three rows contain the GroupWithZero lemma name, the Group lemma, the AddGroup lemma name

Statement	New name	Old name
(a * b) / a = b	mul_div_eq_right₀	mul_div_cancel_left
	mul_div_eq_right	mul_div_cancel'''
	add_sub_eq_right	add_sub_cancel'
(a * b) / b = a	mul_div_eq_left₀	mul_div_cancel
	mul_div_eq_left	mul_div_cancel''
	add_sub_eq_left	add_sub_cancel
a / (a * b) = b⁻¹	div_mul_eq_inv_right₀	div_mul_right (roughly)
	div_mul_eq_inv_right	div_mul_cancel''
	sub_add_eq_neg_right	sub_add_cancel'
b / (a * b) = a⁻¹	div_mul_eq_inv_left₀	div_mul_left (roughly)
	div_mul_eq_inv_left	div_mul_cancel'''
	sub_add_eq_neg_left	sub_add_cancel''
a * (b / a) = b	mul_div_cancel₀	mul_div_cancel'
	mul_div_cancel	mul_div_cancel'_right
	add_sub_cancel	add_sub_cancel'_right
(a / b) * b = a	div_mul_cancel₀	div_mul_cancel
	div_mul_cancel	div_mul_cancel'
	sub_add_cancel	sub_add_cancel

[Floris van Doorn]

I am happy with these changes, and I think we should go further in a later PR, unifying the name of e.g. docs#mul_inv_cancel and docs#mul_right_inv

[Ruben Van de Velde]

Getting rid of the triple ticks will definitely be a win

[Damiano Testa]

I am personally happy with these changes.

And not just triple ticks, also double and single ones!

[Yaël Dillies]

Yes, I should add this is a very unambitious PR compared to what could/should be done!

[Yaël Dillies]

Anyway, please offer better naming schemes if you have some. I am mostly unfussed about what the new names should be, so long as

• The triples of lemmas get the same name (up to additivisation and appending of ₀)
• The pairs of triples get the same name (up to swapping left and right or different symbol reading, eg swapping mul and div)
• The names are guessable/symbol-readable

[Richard Copley]

mul_div_cancel is much more suggestive and guessable for (a * b) / b = b (where the multiplication is done first) than for a * (b / a) = b (which should perhaps be div_mul_cancel_left or div_mul_cancel').
If you do change it, it's also worth considering the similarly-named lemmas

#check Nat.mul_div_cancel --  ⋯ → m * n / n = m
#check IsUnit.mul_div_cancel -- ⋯ → a * b / b = a
#check Asymptotics.IsBigO.eventually_mul_div_cancel -- ⋯ → u / v * v =ᶠ[l] u

and the already inconsistent

#check Ordinal.mul_div_cancel -- ⋯ → b * a / b = a

[Thomas Murrills]

This PR seems like a strict improvement on the current state of affairs! It’s unfortunate that mul_div could mean (_ * _) / _ or _ * (_ / _), but I can’t think of a (good) way around it.

[Thomas Murrills]

Likewise the rule for using cancel vs. eq_(left/right) takes seeing one of these tables and thinking about it, I think. It’d be nice if this were either documented somewhere or if we could have a uniform scheme (but again, hard to think of one).

[Thomas Murrills]

(Maybe this is already documented somewhere and I just didn’t scroll far enough through the diff? :sweat_smile:)

[Yaël Dillies]

Thomas Murrills said:

It’s unfortunate that mul_div could mean (_ * _) / _ or _ * (_ / _)

I hate binary operators

[Yaël Dillies]

Richard Copley said:

mul_div_cancel is much more suggestive and guessable for (a * b) / b = a than for a * (b / a) = b

From experience, which one it is much more suggestive and guessable for entirely depends on which one you need at the minute... :upside_down:

[Yaël Dillies]

A problem with mul_div_cancel meaning (a * b) / b = a is that it should then also mean (a * b) / a = b

[Richard Copley]

mul_div_eq_right isn't better in that respect.

[Yaël Dillies]

It is better in that the other one can be mul_div_eq_left!

[Richard Copley]

(Typo: could you fix the a / (a * b) = a⁻¹ in the table please?)

[Yaël Dillies]

(fixed on the PR)

[Floris van Doorn]

(fixed in OP)

[Yaël Dillies]

(you fixed it the wrong way, Floris!)

[Richard Copley]

Yaël Dillies said:

It is better in that the other one can be mul_div_eq_left!

:-1: but never mind. Overall I like the change.

[Thomas Murrills]

Tentative idea which might look bad after I send this message and look at it long enough:

• the inner operator gets to name what is “right” and what is “left”. (Already sort of the case for the proposed eq names.)
• The outer operator refers to which of these it uses as its other argument after its name. For example:

(a * b) / a = b: mul_div_left_eq_right
a * (b / a) = b: mul_right_div_eq_left
a / (b * a) = b ^{-1}: div_right_mul_eq_left_inv
(a / b) * b = a: div_mul_right_eq_left

[Thomas Murrills]

This is still technically ambiguous, but the alternate interpretations are no longer true!

[Thomas Murrills]

Though there is the issue that imo we don’t really call it “left division” and “right division” so this still isn’t that intuitive when div names the arguments. (There’s “numerator” and “denominator”, but what would be the additive analogue? “minuend” and “subtrahend” aren’t exactly widely known terms…)

[Thomas Murrills]

Alternate idea, I guess, just to brainstorm and maybe inspire more ideas:

keep the names in the table above, but replace _cancel with _eq_numerator (and _eq_minuend)

[Richard Copley]

:laughing: dividend, not numerator

[Thomas Murrills]

Oh, yeah, dividend is better. (But not not numerator! :P)

[Thomas Murrills]

(Aside: I’m realizing maybe some people only use “numerator” for natLits…though I’ve always heard it used generically for the top part of \frac, and I assume / is just ASCII art for \frac! :) )

[Richard Copley]

Statement type	New base name
(a * b) / a = b	div_cancels_left_mul
(a * b) / b = a	div_cancels_right_mul
a / (a * b) = b⁻¹	div_right_mul_eq_inv ??
a / (b * a) = b⁻¹	div_left_mul_eq_inv ??
b * (a / b) = a	left_mul_cancels_div
(a / b) * b = a	right_mul_cancels_div

Semiseriously. With all new names, deprecation becomes a possibility.

[Eric Wieser]

Yaël Dillies said:

A problem with mul_div_cancel meaning (a * b) / b = a is that it should then also mean (a * b) / a = b

Another way out is to always give the simpler name to the lemma that doesn't need commutativity, which means the first one wins here

[Mario Carneiro]

I don't understand the logic here regarding whether cancel should be used or not. AFAICT these should all be "cancel" lemmas? (The characteristic property of a cancel lemma is that the lhs contains two occurrences of a variable where the rhs has 0)

[Mario Carneiro]

I also what to put a vote in the "actually, ' isn't so bad" bucket: it's nice if symbol reading takes you to the whole cluster of lemmas, i.e. I see a * (b / a) and say "uh... mul div cancel" cause it's cancelling and has mul and div in that order, and then I get a list of lemmas that are also cancellation lemmas with mul and div in that order like (a * b) / a or (a * b) / b and I pick the right one by looking at it in autocomplete. If the names are all completely different then I really have to understand the logic of the naming because if I search for the wrong one then my lemma won't show up.

[Mario Carneiro]

(note, it's fine to use suffixes other than ' for this purpose, like mul_div_cancel_right; I'm just worried about us breaking up the group so that they don't share a prefix anymore.)

[Floris van Doorn]

Based on Mario's suggestion, this is a possible naming scheme:

Statement type	New name
(a * b) / a = b	mul_div_cancel_left(₀)
(a * b) / b = a	mul_div_cancel_right(₀)
a / (a * b) = b⁻¹	div_mul_cancel_left(₀)
a / (b * a) = b⁻¹	div_mul_cancel_right(₀)
b * (a / b) = a	mul_div_cancel(₀)
(a / b) * b = a	div_mul_cancel(₀)

[Yaël Dillies]

You have the same typo as before in your statements

[Floris van Doorn]

I think I just interchanged a and b?

[Yaël Dillies]

Oh right

[Yaël Dillies]

I quite like this naming scheme

[Thomas Browning]

Per Eric's suggestion, would it make sense to give (a * b) / b = a the shorter name, rather than b * (a / b) = a?

[Floris van Doorn]

Eric Wieser said:

Another way out is to always give the simpler name to the lemma that doesn't need commutativity, which means the first one wins here

This is a possible heuristic, but not one we actually use in Mathlib, I think. Compare docs#mul_inv and docs#mul_inv_rev.

[Yaël Dillies]

Thomas Browning said:

Per Eric's suggestion, would it make sense to give (a * b) / b = a the shorter name, rather than b * (a / b) = a?

I think that's worse because of the symmetry issues.

[Filippo A. E. Nuccio]

Yaël Dillies said:

I quite like this naming scheme

Me too!

[Yaël Dillies]

PR updated!

[Antoine Chambert-Loir]

I feel div_mul_cancel should be a / (a * b) = 1 / b rather than … = b⁻¹.
(This latter lemma could be called div_mul_eq_inv_left.)

[Yaël Dillies]

We decided long ago that lemmas should use x⁻¹, not 1 / x, the same way that we use -x, not 0 - x.