Add and Mul are associative. Let's make them canonical

[msooseth]

Description

As per @zoep 's idea, Mul is associative. So we should make Mul+Mul canonical. This fixes #408 . That issue also mentions Add. Doing that too.

I added an automated test for the Mul associativity, as that's not obvious I think. Anyway, now it's proven correct.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[zoep]

I am wondering if there is a way to do this only if it is beneficial.

For instance if the initial expression is (Lit 17 + Lit 42) + x then rearranging the expression will miss an opportunity for further simplification.

[msooseth]

Oh wow, good point! I think we should be canonical, so it should eventually always be done. But you are right that here we are very much missing an opportunity. What about this (for both Add and Mul):

    -- Add is associative
    go (Add (Add a b) c) = add a (add b c)
    go (Add (Lit a) (Add (Lit b) x) = add (Lit (a+b) x

Notice that the second Add will always have Lit as 1st argument thanks to canonicalization done by add (in case any of its arguments are a Lit). The above ensures that if eventually somehow, the second Add's any argument becomes a Lit and the 1st Add's 1st argument becomes a Lit then we simplify.

This should work for Mul as well. The only special case there is Mul by Lit 0 and Lit 1, but that work with and 2nd argument, so the 2nd argument can be another Mul.

What do you think?

[zoep]

Yes! I think adding this rule would be great!

[d-xo]

looks good!

[zoep]

Looks great!