assoc

Stream: general

[Chris Hughes]

Is there a good reason why add_assoc is a + b + c = a + (b + c) and not a + (b + c) = a + b + c? It makes expressions very hard to read after simp [add_assoc]

[Kevin Buzzard]

I asked this once and my impression was that @Mario Carneiro seemed to have some kind of argument as to why this was sensible

[Mario Carneiro]

Does simp work as well with left associated lists as it does right associated lists? At the very least simp only [add_assoc, add_right_comm, add_comm] needs to be able to prove all AC goals

[Gabriel Ebner]

I don't see any reason why it shouldn't work with right-associative lists.
Some proofs using by simp [add_assoc, add_left_comm, add_comm, neg_add_cancel_left] would likely break if switched to left though because with right the summands are shuffled around, and neg_add_cancel_left has more chance of applying.

[Chris Hughes]

There's a simp loop if you go the other way round. To get around this the simplify would have to start putting the longest expressions first after simp [add_comm] instead of the shortest.

0. [simplify.rewrite] [add_comm]: a + -b + -c ==> -c + (a + -b)
0. [simplify.rewrite] [add_assoc]: -c + (a + -b) ==> -c + a + -b
0. [simplify.rewrite] [add_right_comm]: a + -c + -b ==> a + -b + -c