Zulip Chat Archive

Stream: general

Topic: assoc


Chris Hughes (Jun 08 2020 at 16:19):

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 (Jun 08 2020 at 17:58):

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 (Jun 09 2020 at 04:30):

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 (Jun 09 2020 at 08:32):

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 (Jun 11 2020 at 14:26):

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

Last updated: Dec 20 2023 at 11:08 UTC