left and right

Stream: mathlib4

[Aaron Liu]

Sometimes I can't use mathlib without loogle and this is one of the reasons

Stuff that looks to me to be about (_ + ·)

lots

• docs#AddGroup.addLeft_bijective
• docs#AddLECancellable
• docs#AddLECancellable.Injective
• docs#AddLECancellable.add_le_add_iff_left
• docs#AddLECancellable.add_tsub_cancel_left
• docs#AddLECancellable.inj
• docs#AddLECancellable.lt_add_of_tsub_lt_left
• docs#AddLECancellable.lt_tsub_of_add_lt_left
• docs#AddLeftCancelMonoid
• docs#AddLeftCancelSemigroup
• docs#AddLeftMono
• docs#AddLeftReflectLE
• docs#AddLeftReflectLT
• docs#AddLeftStrictMono
• docs#AddUnits.addLeft
• docs#AddUnits.addLeft_bijective
• docs#AddUnits.add_neg_cancel_left
• docs#AddUnits.add_right_inj
• docs#AddUnits.neg_add_cancel_left
• docs#Equiv.addLeft
• docs#IsAddLeftRegular
• docs#IsAddUnit.add_left_cancel
• docs#IsAddUnit.add_neg_cancel_left
• docs#IsAddUnit.add_right_inj
• docs#IsAddUnit.add_right_injective
• docs#IsAddUnit.add_sub_add_left
• docs#IsAddUnit.add_sub_cancel_left
• docs#IsAddUnit.isAddUnit_iff_addLeft_bijective
• docs#IsAddUnit.neg_add_cancel_left
• docs#IsLeftCancelAdd
• docs#add_le_add_iff_left
• docs#add_le_add_left
• docs#add_le_of_le_sub_left
• docs#add_left_cancel
• docs#add_left_cancel''
• docs#add_left_cancel_iff
• docs#add_left_comm
• docs#add_left_surjective
• docs#add_lt_add_left
• docs#add_ne_add_right
• docs#add_neg_cancel_left
• docs#add_right_inj
• docs#add_right_inj_of_comparable
• docs#add_right_injective
• docs#add_right_mono
• docs#add_right_strictMono
• docs#add_sub_add_left_eq_sub
• docs#add_sub_cancel_left
• docs#add_sub_left_comm
• docs#add_tsub_add_eq_tsub_left
• docs#add_tsub_add_le_tsub_left
• docs#add_tsub_cancel_left
• docs#add_tsub_le_left
• docs#cmp_add_left
• docs#comp_add_left
• docs#le_of_add_le_add_left
• docs#le_tsub_of_add_le_left
• docs#leftInverse_add_right_neg_add
• docs#leftInverse_neg_add_add_right
• docs#lt_of_add_lt_add_left
• docs#lt_tsub_iff_left
• docs#lt_tsub_of_add_lt_left
• docs#neg_add_cancel_left
• docs#sub_add_cancel_left
• docs#tsub_le_iff_left

loogle only showed me the first 200 in my search so I don't have any more than this but sometimes it's left (usually it's left) and sometimes it's right so how am I supposed to tell

[Kenny Lau]

@Joachim Breitner maybe can we have a button in loogle to "show 200 more results"?

[David Loeffler]

sometimes it's left (usually it's left) and sometimes it's right so how am I supposed to tell

So your point is that the defs / lemmas involving x ↦ a + x, for a fixed a and x the argument, sometimes have names involving add_left and sometimes add_right?

I raised a very similar point for smulonly a day or two back (here: #mathlib4 > Naming discrepancy: `smulLeft` vs `smulRight`). I'm glad I'm not the only one who considers this sub-optimal.

[Bryan Gin-ge Chen]

I thought we had more specific guidance in our naming conventions but it does look like there's a hole there. It'd be good to settle on something here!

[Kenny Lau]

"left inverse" is an existing term where "y is a left inverse of x" means yx=1, and consequently we also have add_left_inj which means i + k = j + k ↔ i = j which means the function x ↦ x + k is injective, and this is clearly adding on the left

[Kenny Lau]

to make this point clearer, from "y is a left inverse of k" we say "k has a left inverse", where in this case to connect with the function it means that the map x ↦ x * k has 1 in its image (which is usually equivalent to the function being surjective)

[Kenny Lau]

oh boy by this logic the majority of aaron's linked decls are wrong

[Sébastien Gouëzel]

I prefer to avoid left and right precisely because of this ambiguity (are we adding something to the left of x, or is the varying variable on the left of the expression?), and to use const_add and add_const instead.

[Eric Wieser]

Bryan Gin-ge Chen said:

I thought we had more specific guidance in our naming conventions

We have only

An injectivity lemma that uses "left" or "right" should refer to the argument that "changes". For example, a lemma with the statement a - b = a - c ↔ b = c could be called sub_right_inj.

[Bhavik Mehta]

Also

Predicates as suffixes can be preceded by either _left or _right to signify that a binary operation is left- or right-monotone. For example, mul_left_monotone : Monotone (· * a) proves left-monotonicity of multiplication and not monotonicity of left-multiplication.

[Kenny Lau]

which means AddLeftMono is very much wrong

[Aaron Liu]

The theorem docs#add_right_mono uses the typeclass docs#AddLeftMono

[Kenny Lau]

note that my explanation above with left inverse is consistent with these two quoted notes, and is also consistent with the fact that AddLeftMono is wrong

[Kenny Lau]

Aaron Liu said:

The theorem docs#add_right_mono uses the special typeclass docs#AddLeftMono

oh no...

[Weiyi Wang]

That's a refactoring in motion #29396

[Jovan Gerbscheid]

Yes, we are in the process of fixing this, but the left/right refers to the side with the variable argument. So e.g. right monotonicity is monotonicity of c + . for a fixed c.

[Aaron Liu]

That's unfortunately not what I'm used to

[Aaron Liu]

are we really gonna swap add_left_comm and add_right_comm

[Kenny Lau]

that's unfortunate, i guess based on my logic i'll also have to get used to the new left_comm

[Aaron Liu]

Kenny Lau said:

"left inverse" is an existing term where "y is a left inverse of x" means yx=1, and consequently we also have add_left_inj which means i + k = j + k ↔ i = j which means the function x ↦ x + k is injective, and this is clearly adding on the left

I don't buy this logic how did you go from left inverse to add_left_inj

[Aaron Liu]

to me that says "adding on the right by k is injective"

[Kenny Lau]

Aaron Liu said:

Kenny Lau said:

"left inverse" is an existing term where "y is a left inverse of x" means yx=1, and consequently we also have add_left_inj which means i + k = j + k ↔ i = j which means the function x ↦ x + k is injective, and this is clearly adding on the left

I don't buy this logic how did you go from left inverse to add_left_inj

the logic is that everything with "left" in the name is referring to the function x ↦ x op k where op is + or *

[Aaron Liu]

I don't see how that applies to left inverse

[Kenny Lau]

has left inverse says that this function has 1 in the range

[Aaron Liu]

"has left inverse" and "is right inverse" are the same thing

[Aaron Liu]

so I could just as well say this is right

[Kenny Lau]

:thinking:

[Kenny Lau]

i retract my statement

[Johan Commelin]

Sébastien Gouëzel said:

I prefer to avoid left and right precisely because of this ambiguity (are we adding something to the left of x, or is the varying variable on the left of the expression?), and to use const_add and add_const instead.

I like this. What do others in this thread think of this suggestion?

[Johan Commelin]

cc @Yaël Dillies

[Kenny Lau]

ConstAddMono is fine and unambiguous, but what's mul_left_comm?

[Kenny Lau]

I suppose that can be mul_const_comm?

[Eric Wieser]

left_comm is its own atom there, it means op a (op b c) = op b (op a c)

[Eric Wieser]

I supposed you could argue for leftComm, I don't remember what we decided the rule was there

[Eric Wieser]

I'd argue the const terminology only makes sense when there's a lambda involved, to refer to the variable not bound by the lambda

[Kenny Lau]

well AddConstMono can have a lambda

[Eric Wieser]

I guess you could phrase op a (op b c) = op b (op a c) as (fun a b => op a (op b c)) a b = (fun a b => op a (op b c)) b a to justify a const, though then it would be op_op_const_comm

[Yaël Dillies]

I think _leftComm is good, and we are not using it now merely because this is a name coming from mathlib3

[Yaël Dillies]

Johan Commelin said:

Sébastien Gouëzel said:

I prefer to avoid left and right precisely because of this ambiguity (are we adding something to the left of x, or is the varying variable on the left of the expression?), and to use const_add and add_const instead.

I like this. What do others in this thread think of this suggestion?

I am not a big fan, mostly because the location of the const modifier changes between the two lemmas in a pair, and I still believe I can iron out the _left/_right table cloth.

[Aaron Liu]

Eric Wieser said:

left_comm is its own atom there, it means op a (op b c) = op b (op a c)

I thought it was because it's saying (a + ·) ∘ (b + ·) = (b + ·) ∘ (a + ·)

[Sébastien Gouëzel]

Yaël Dillies said:

I am not a big fan, mostly because the location of the const modifier changes between the two lemmas in a pair, and I still believe I can iron out the _left/_right table cloth.

The fact that the location of the const changes is precisely the point, right? The main advantage I see compared to left / right is precisely that there is no ambiguity because the position of the keyword tells everything. With left or right, there is an ambiguity. We could probably choose a convention for left / right once and for all and try to enforce it all over mathlib, but since this would be an arbitrary convention newcomers who are not aware of it will always be confused / make mistakes that we will have to fix. In fact, we have already chosen such a convention (use the side of the varying variable) but it's obscure enough that it's not respected. IMHO, using a phrasing without built-in ambiguity is a clear win here.

[Kenny Lau]

image.png

[Kevin Buzzard]

We can't even be consistent with primed and nonprimed versions of lemmas!

[Yaël Dillies]

The latter is correct: left here refers to a in a * b

[Aaron Liu]

can it be mul_lt_left_iff_lt_one and mul_lt_right_iff_lt_one that's how I would name it

[Yury G. Kudryashov]

@Yaël Dillies I understand that you have a clear idea of what _left/_right at the end of a name means. Many people (incl. myself and most of the new contributors) don't have it and/or don't think that it's important enough to memorize it. If a lemma can be named without _left/_right at the end (e.g., by using const_mul or mul_eq_left_...), I would definitely prefer this name. I'm not sure about lemmas like add_le_add_left (I see that you're swapping left/right for some of these lemmas in a pending PR).

[Kenny Lau]

is a or b the constant in the photo i posted?

[Yaël Dillies]

I don't disagree with you, Yury. I think here Aaron's suggestion is best.

[Yaël Dillies]

I should have said that the second one was more correct

[Yury G. Kudryashov]

I'm sorry if my message did sound offensive. This was not my intention.

[Yaël Dillies]

Nono, it didn't feel offensive at all. I'm just annoyed at myself for having written my above remark in 10s during a lecture and thus forgetting to mention the better alternative :sweat_smile: