josdejong
Allow tentative/bidirectional simplify rules
With the leafCount function provided by the resolution #2389, it would now make sense to allow simiplification rules to specify that they only apply if they ultimately lead to a lower-complexity (as measured by leafCount) expression, or to allow rules that will apply in either direction (and which will take the ultimate result with the lowest complexity). In both cases, there needs to be a way to specify whether (or in which direction) the rule applies if the complexity is a tie between multiple alternatives.
This was initially proposed in conjunction with simplification of array expressions, so it might be best to add this facility prior to addressing #2390. On the other hand, it would be good to have at least one use case for this feature in place before implementing it, so perhaps it is best to address #927 at least partially first, and then use this feature for the phi^2 <-> phi+1 rule mentioned there.
I can indeed imagine that implementing #2390 before implementing complexity rules would result in extra refactoring later on. If you are convinced that this would require a lot of extra work later on, let's please first implement these complexity rules. If the amount of refactoring later on is not that large, I would prefer focusing on #2390 first, because that brings a lot of value right now, and the complexity rules are at this point experimental (at least in my head).
