Commit 2023-04-28 06:56 bcbd4ec1
View on Github →perf: improve performance of to_additive
(#3632)
applyReplacementFun
now treats applicationsf x_1 ... x_n
as atomic, and recurses directly intof
andx_i
(before it recursed on the partial appliationsf 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 singledsimp 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