Commit 2023-04-28 06:56 bcbd4ec1

perf: improve performance of to_additive (#3632)

• applyReplacementFun now treats applications f x_1 ... x_n as atomic, and recurses directly into f and x_i (before it recursed on the partial appliations f x_1 ... x_j)
• I had to reimplement the way to_additive reorders arguments, so at the same time I also made it more flexible. We can now reorder with an arbitrary permutation, and you have to specify this by providing a permutation using cycle notation (e.g. (reorder := 1 2 3, 8 9) means we're permuting the first three arguments and swapping arguments 8 and 9). This implements the first item of #1074.
• additiveTest now memorizes the test on previously-visited subexpressions. Thanks to @kmill for this suggestion! The performance on (one of) the slowest declaration(s) to additivize (MonoidLocalization.lift) is summarized below (note: dsimp only refers to adding a single dsimp only tactic in the declaration, which was done in #3580)

original: 27400ms
better applyReplacementFun: 1550ms
better applyReplacementFun + better additiveTest: 176ms
dsimp only: 6710ms
better applyReplacementFun + dsimp only: 425ms
better applyReplacementFun + better additiveTest + dsimp only: 128ms