Associativity rules for SMul and VAdd

Stream: mathlib4

[Antoine Chambert-Loir]

Apparently, SMul and VAdd have different associativity rules. This makes it harder to additivize some stuff. But maybe I'm wrong.

import Mathlib.Algebra.Group.Defs

variable {G A X S: Type*} [Mul G] [SMul G X] [Add A] [VAdd A S]
  (g h : G) (a b : A) (x : X) (s : S)

#check g • (h • x) -- g • h • x : X
#check (g * h) • x -- (g * h) • x : X
#check (a + b) +ᵥ s -- a + b +ᵥ s : S
#check a +ᵥ (b +ᵥ s) -- a +ᵥ (b +ᵥ s) : S

[Johan Commelin]

The relevant priorities and associativities are:

@[inherit_doc] infixl:65 " + "   => HAdd.hAdd
@[inherit_doc] infixl:70 " * "   => HMul.hMul

@[inherit_doc] infixl:65 " +ᵥ " => HVAdd.hVAdd
@[inherit_doc] infixr:73 " • " => HSMul.hSMul

[Johan Commelin]

There are indeed some asymmetries here.
I think +ᵥ should associate to the right instead of left.

And we should document our choice of priority and associativity, just like we did for the big operators $\sum$ and $\prod$

[Antoine Chambert-Loir]

I wouldn't dare trying to change the infixl into an infixr here, or conversely, in fear that it breaks everything. Does one know whether this is a deliberate choice or a mere accident of code.

[Johan Commelin]

@Eric Wieser Do you know the reasoning behind these choices?

[Eric Wieser]

I think VAdd is more @Yury G. Kudryashov's domain

[Floris van Doorn]

I feel like the left-associativity of VAdd is just a mistake. a +ᵥ (b +ᵥ s) seems to make sense a lot of the time (only needs one VAdd instance) while (a +ᵥ b) +ᵥ s only rarely makes sense (needs two VAdd instances). But maybe I don't know its uses well enough.

[Eric Wieser]

Antoine Chambert-Loir said:

This makes it harder to additivize some stuff.

I don't think the notation precedence has any effect on to_additive, if that's what you mean

[Floris van Doorn]

Correct, to_additive doesn't care about notation precedences (or even whether you use notation). Reordering the arguments would make it significantly harder to additivize stuff (and so to_additive can only additive a fraction of power-lemmas to smul-lemmas).

[Johan Commelin]

@Floris van Doorn you are saying "would". So that's not the issue here? But notation also isn't the issue...
Do I understand that correctly?

[Antoine Chambert-Loir]

I'm not sure I understand what you mean, @Floris van Doorn. The only thing I can tell is that I had to additivize a lemma by hand (for reasons I don't understand), hence I copy-pasted the proof of the multiplicative case, and this is how I discovered the problem with associativity, because even after changing smul to vadd and similar other modifications, lean wasn't understanding the terms as I expected.

[Floris van Doorn]

If changing the notation means that lemmas are going to state different things (i.e. they are elaborated to different expressions), then sure, that would impact to_additive (and break proof for reasons unrelated to to_additive).

@Antoine Chambert-Loir: is this on a branch of Mathlib? If so, could you link it so that I can take a look?
I can tell you it has nothing to do with the notation, but it could be #10830 or the fact that you are (also) working with an abstract ring in the lemma.

[Antoine Chambert-Loir]

This is either in #19171 or more likely in #12052.

[Antoine Chambert-Loir]

(One complicated issue in #12052 is that one defines a Group of additive automorphisms in the context of AddGroup, but @[to_additive] should not make this group an AddGroup. Because of that, possibly, one has to do the things by hand.)

[Antoine Chambert-Loir]

(line 279 of Mathlib/GroupTheory/GroupAction/Blocks.lean)

[Floris van Doorn]

Antoine Chambert-Loir said:

(One complicated issue in #12052 is that one defines a Group of additive automorphisms in the context of AddGroup, but @[to_additive] should not make this group an AddGroup. Because of that, possibly, one has to do the things by hand.)

Yes, that was indeed the problem. #19297 adds a new attribute for to_additive that says that operations on that type should not be additivized. Beware: you will have to specify the name manually if you want to keep a multiplicative name.

[Yury G. Kudryashov]

Eric Wieser said:

I think VAdd is more Yury G. Kudryashov's domain

@Joseph Myers added AddTorsors in !3#2720

[Joseph Myers]

When I defined +ᵥ I took the priority and use of infix from + (Lean 3 subsequently changed + from infix to infixl, not sure what semantic difference, if any, that involved).

It was subsequently decided that +ᵥ should act with the vector on the left rather than the right, so I made the corresponding change to that PR. I didn't think at the time to reverse associativity when reversing which side the action was on, but maybe that was when it should have changed.

[Joseph Myers]

If we do change associativity, I hope we have tools to verify that all lemma types are syntactically equal before and after the change: that the change doesn't result in any unintentional changes to what is proved.

[Eric Wieser]

Sadly I don't think we have those tools right now

[Eric Wieser]

leaff might have been up to the job, but it wouldn't surprise me if its stuck on an old lean version

[Johan Commelin]

@Joseph Myers Thanks for clearing up the history of how this came to be.

[Johan Commelin]

There are 141 lines in mathlib that contain more than one occurence of +ᵥ. Not all of them are assocs, some of them occur on different sides of =. But there might be assoc situations that span multiple lines.

Anyway, I think the best we can do is to just change the associativity, and take a very careful look at all 500+ lines where +ᵥ shows up.

[Johan Commelin]

Well, we can do better. Even if we don't have leaff we can ask Lean to print a list of all declarations where assoc plays a role.

[Johan Commelin]

@Eric Wieser That shouldn't be too hard, right?

[Johan Commelin]

Do I understand correctly that

-- Mathlib/Algebra/Group/Action/Opposite.lean -- L94,99
scoped notation3:74 r:75 " +ᵥ> " m:74 => r +ᵥ m
scoped notation3:73 m:73 " <+ᵥ " r:74 => AddOpposite.op r +ᵥ m

have their associativities set as intended?

I would expect both lines to use the same numbers....

[Johan Commelin]

Hmmm, and also that they would be much closer to the 65 that +ᵥ uses

[Johan Commelin]

#19321 (+41/-38)

[Damiano Testa]

The question here is to look for all HVAdd.hVAdd applications that have an HVAdd.hVAdd application inside them in all theorem statements, right?

[Damiano Testa]

(And this may still be too many, but would not miss any possibility.)

[Yaël Dillies]

Johan Commelin said:

Do I understand correctly that

-- Mathlib/Algebra/Group/Action/Opposite.lean -- L94,99
scoped notation3:74 r:75 " +ᵥ> " m:74 => r +ᵥ m
scoped notation3:73 m:73 " <+ᵥ " r:74 => AddOpposite.op r +ᵥ m

have their associativities set as intended?

I would expect both lines to use the same numbers....

Yes, it is so that a +ᵥ> b <+ᵥ c means (a +ᵥ> b) <+ᵥ c, not a +ᵥ> (b <+ᵥ c)

[Johan Commelin]

I feel like in such situations I would prefer if a +ᵥ> b <+ᵥ c would give an "Ambiguous parsing error", and would force us to add parens.

[Eric Wieser]

Hasn't that ship sailed with a + b + c?

[Johan Commelin]

Nah, I think we can distinguish between "well-known" operators and "not so well-known".

[Johan Commelin]

Also, that's twice the same operator. And + is usually associative.

[Johan Commelin]

Maybe you say that a +ᵥ> b <+ᵥ c is evil if there is no VAddAssoc instance floating around? I could live with that.

[Eric Wieser]

In the same way as a * b * c is evil if multiplication is not associative

[Yaël Dillies]

Johan Commelin said:

Maybe you say that a +ᵥ> b <+ᵥ c is evil if there is no VAddAssoc instance floating around?

VAddCommClass actually, but yeah

[Johan Commelin]

I would be very happy if a * b * c printed with parens in the non-associative case.
I will confess that I'm not often working with non-associative *.

[Johan Commelin]

Maybe more importantly, I would really like our source files to contain parens in those cases.

[Johan Commelin]

Anyway, what do people think of

chore: change associativity of +ᵥ and -ᵥ from infixl to infixr #19321

[Johan Commelin]

Should we change the priority of -ᵥ to remove half of the parens again?

[Eric Wieser]

I've just noticed that this now fails with a very confusing error:

import Mathlib.Algebra.AddTorsor

variable {V P : Type*} [AddCommGroup V] [AddTorsor V P] (a b c : P)
def foo := b -ᵥ a +ᵥ c

[Eric Wieser]

I would guess this is because you can't have two notations with the same precedence where one is infixr but the other is infixl?