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
```

Mathlib/Algebra/Group/Defs.lean

@@ -88,16 +88,16 @@ infixl:65 " -ᵥ " => VSub.vsub
 infixr:73 " • " => HSMul.hSMul
 
 attribute [to_additive existing] Mul Div HMul instHMul HDiv instHDiv HSMul
-attribute [to_additive (reorder := 1) SMul] Pow
-attribute [to_additive (reorder := 1)] HPow
-attribute [to_additive existing (reorder := 1 5) hSMul] HPow.hPow
-attribute [to_additive existing (reorder := 1 4) smul] Pow.pow
+attribute [to_additive (reorder := 1 2) SMul] Pow
+attribute [to_additive (reorder := 1 2)] HPow
+attribute [to_additive existing (reorder := 1 2, 5 6) hSMul] HPow.hPow
+attribute [to_additive existing (reorder := 1 2, 4 5) smul] Pow.pow
 
 @[to_additive (attr := default_instance)]
 instance instHSMul [SMul α β] : HSMul α β β where
   hSMul := SMul.smul
 
-attribute [to_additive existing (reorder := 1)] instHPow
+attribute [to_additive existing (reorder := 1 2)] instHPow
 
 universe u
 

Mathlib/Algebra/Group/OrderSynonym.lean

@@ -37,12 +37,12 @@ instance [h : Inv α] : Inv αᵒᵈ := h
 @[to_additive]
 instance [h : Div α] : Div αᵒᵈ := h
 
-@[to_additive (attr := to_additive) (reorder := 1) instSMulOrderDual]
+@[to_additive (attr := to_additive) (reorder := 1 2) instSMulOrderDual]
 instance [h : Pow α β] : Pow αᵒᵈ β := h
 #align order_dual.has_pow instPowOrderDual
 #align order_dual.has_smul instSMulOrderDual
 
-@[to_additive (attr := to_additive) (reorder := 1) instSMulOrderDual']
+@[to_additive (attr := to_additive) (reorder := 1 2) instSMulOrderDual']
 instance instPowOrderDual' [h : Pow α β] : Pow α βᵒᵈ := h
 #align order_dual.has_pow' instPowOrderDual'
 #align order_dual.has_smul' instSMulOrderDual'
@@ -140,25 +140,25 @@ theorem ofDual_div [Div α] (a b : αᵒᵈ) : ofDual (a / b) = ofDual a / ofDua
 #align of_dual_div ofDual_div
 #align of_dual_sub ofDual_sub
 
-@[to_additive (attr := simp, to_additive) (reorder := 1 4) toDual_smul]
+@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) toDual_smul]
 theorem toDual_pow [Pow α β] (a : α) (b : β) : toDual (a ^ b) = toDual a ^ b := rfl
 #align to_dual_pow toDual_pow
 #align to_dual_smul toDual_smul
 #align to_dual_vadd toDual_vadd
 
-@[to_additive (attr := simp, to_additive) (reorder := 1 4) ofDual_smul]
+@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) ofDual_smul]
 theorem ofDual_pow [Pow α β] (a : αᵒᵈ) (b : β) : ofDual (a ^ b) = ofDual a ^ b := rfl
 #align of_dual_pow ofDual_pow
 #align of_dual_smul ofDual_smul
 #align of_dual_vadd ofDual_vadd
 
-@[to_additive (attr := simp, to_additive) (reorder := 1 4) toDual_smul']
+@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) toDual_smul']
 theorem pow_toDual [Pow α β] (a : α) (b : β) : a ^ toDual b = a ^ b := rfl
 #align pow_to_dual pow_toDual
 #align to_dual_smul' toDual_smul'
 #align to_dual_vadd' toDual_vadd'
 
-@[to_additive (attr := simp, to_additive) (reorder := 1 4) ofDual_smul']
+@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) ofDual_smul']
 theorem pow_ofDual [Pow α β] (a : α) (b : βᵒᵈ) : a ^ ofDual b = a ^ b := rfl
 #align pow_of_dual pow_ofDual
 #align of_dual_smul' ofDual_smul'
@@ -179,12 +179,12 @@ instance [h : Inv α] : Inv (Lex α) := h
 @[to_additive]
 instance [h : Div α] : Div (Lex α) := h
 
-@[to_additive (attr := to_additive) (reorder := 1) instSMulLex]
+@[to_additive (attr := to_additive) (reorder := 1 2) instSMulLex]
 instance [h : Pow α β] : Pow (Lex α) β := h
 #align lex.has_pow instPowLex
 #align lex.has_smul instSMulLex
 
-@[to_additive (attr := to_additive) (reorder := 1) instSMulLex']
+@[to_additive (attr := to_additive) (reorder := 1 2) instSMulLex']
 instance instPowLex' [h : Pow α β] : Pow α (Lex β) := h
 #align lex.has_pow' instPowLex'
 #align lex.has_smul' instSMulLex'
@@ -280,25 +280,25 @@ theorem ofLex_div [Div α] (a b : Lex α) : ofLex (a / b) = ofLex a / ofLex b :=
 #align of_lex_div ofLex_div
 #align of_lex_sub ofLex_sub
 
-@[to_additive (attr := simp, to_additive) (reorder := 1 4) toLex_smul]
+@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) toLex_smul]
 theorem toLex_pow [Pow α β] (a : α) (b : β) : toLex (a ^ b) = toLex a ^ b := rfl
 #align to_lex_pow toLex_pow
 #align to_lex_smul toLex_smul
 #align to_lex_vadd toLex_vadd
 
-@[to_additive (attr := simp, to_additive) (reorder := 1 4) ofLex_smul]
+@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) ofLex_smul]
 theorem ofLex_pow [Pow α β] (a : Lex α) (b : β) : ofLex (a ^ b) = ofLex a ^ b := rfl
 #align of_lex_pow ofLex_pow
 #align of_lex_smul ofLex_smul
 #align of_lex_vadd ofLex_vadd
 
-@[to_additive (attr := simp, to_additive) (reorder := 1 4) toLex_smul']
+@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) toLex_smul']
 theorem pow_toLex [Pow α β] (a : α) (b : β) : a ^ toLex b = a ^ b := rfl
 #align pow_to_lex pow_toLex
 #align to_lex_smul' toLex_smul'
 #align to_lex_vadd' toLex_vadd'
 
-@[to_additive (attr := simp, to_additive) (reorder := 1 4) ofLex_smul']
+@[to_additive (attr := simp, to_additive) (reorder:= 1 2, 4 5) ofLex_smul']
 theorem pow_ofLex [Pow α β] (a : α) (b : Lex β) : a ^ ofLex b = a ^ b := rfl
 #align pow_of_lex pow_ofLex
 #align of_lex_smul' ofLex_smul'

Mathlib/Algebra/Group/ULift.lean

@@ -89,12 +89,12 @@ theorem smul_down [SMul α β] (a : α) (b : ULift.{v} β) : (a • b).down = a
 #align ulift.smul_down ULift.smul_down
 #align ulift.vadd_down ULift.vadd_down
 
-@[to_additive existing (reorder := 1) smul]
+@[to_additive existing (reorder := 1 2) smul]
 instance pow [Pow α β] : Pow (ULift α) β :=
   ⟨fun x n => up (x.down ^ n)⟩
 #align ulift.has_pow ULift.pow
 
-@[to_additive existing (attr := simp) (reorder := 1) smul_down]
+@[to_additive existing (attr := simp) (reorder := 1 2) smul_down]
 theorem pow_down [Pow α β] (a : ULift.{v} α) (b : β) : (a ^ b).down = a.down ^ b :=
   rfl
 #align ulift.pow_down ULift.pow_down

Mathlib/Algebra/Hom/Group.lean

@@ -444,7 +444,7 @@ theorem map_div [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) :
 #align map_div map_div
 #align map_sub map_sub
 
-@[to_additive (attr := simp) (reorder := 8)]
+@[to_additive (attr := simp) (reorder := 8 9)]
 theorem map_pow [Monoid G] [Monoid H] [MonoidHomClass F G H] (f : F) (a : G) :
   ∀ n : ℕ, f (a ^ n) = f a ^ n
   | 0 => by rw [pow_zero, pow_zero, map_one]
@@ -461,7 +461,7 @@ theorem map_zpow' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H]
 #align map_zsmul' map_zsmul'
 
 /-- Group homomorphisms preserve integer power. -/
-@[to_additive (attr := simp) (reorder := 8)
+@[to_additive (attr := simp) (reorder := 8 9)
 "Additive group homomorphisms preserve integer scaling."]
 theorem map_zpow [Group G] [DivisionMonoid H] [MonoidHomClass F G H]
   (f : F) (g : G) (n : ℤ) : f (g ^ n) = f g ^ n := map_zpow' f (map_inv f) g n

Mathlib/Algebra/Hom/Iterate.lean

@@ -103,14 +103,14 @@ theorem iterate_map_smul (f : M →+ M) (n m : ℕ) (x : M) : (f^[n]) (m • x)
   f.toMultiplicative.iterate_map_pow n x m
 #align add_monoid_hom.iterate_map_smul AddMonoidHom.iterate_map_smul
 
-attribute [to_additive (reorder := 5)] MonoidHom.iterate_map_pow
+attribute [to_additive (reorder := 5 6)] MonoidHom.iterate_map_pow
 #align add_monoid_hom.iterate_map_nsmul AddMonoidHom.iterate_map_nsmul
 
 theorem iterate_map_zsmul (f : G →+ G) (n : ℕ) (m : ℤ) (x : G) : (f^[n]) (m • x) = m • (f^[n]) x :=
   f.toMultiplicative.iterate_map_zpow n x m
 #align add_monoid_hom.iterate_map_zsmul AddMonoidHom.iterate_map_zsmul
 
-attribute [to_additive existing (reorder := 5)] MonoidHom.iterate_map_zpow
+attribute [to_additive existing (reorder := 5 6)] MonoidHom.iterate_map_zpow
 
 end AddMonoidHom
 

Mathlib/Data/Array/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino, Floris van Doorn
 -/
 
-import Std
+import Lean
 
 /-!
 ## Definitions on Arrays
@@ -14,3 +14,19 @@ proofs about these definitions, those are contained in other files in `Mathlib.D
 -/
 
 namespace Array
+
+/-- Permute the array using a sequence of indices defining a cyclic permutation.
+  If the list of indices `l = [i₁, i₂, ..., iₙ]` are all distinct then
+  `(cyclicPermute! a l)[iₖ₊₁] = a[iₖ]` and `(cyclicPermute! a l)[i₀] = a[iₙ]` -/
+def cyclicPermute! [Inhabited α] : Array α → List Nat → Array α
+| a, []      => a
+| a, i :: is => cyclicPermuteAux a is a[i]! i
+where cyclicPermuteAux : Array α → List Nat → α → Nat → Array α
+| a, [], x, i0 => a.set! i0 x
+| a, i :: is, x, i0 =>
+  let (y, a) := a.swapAt! i x
+  cyclicPermuteAux a is y i0
+
+/-- Permute the array using a list of cycles. -/
+def permute! [Inhabited α] (a : Array α) (ls : List (List Nat)) : Array α :=
+ls.foldl (init := a) (·.cyclicPermute! ·)

Mathlib/Data/Pi/Algebra.lean

@@ -117,28 +117,28 @@ instance instSMul [∀ i, SMul α <| f i] : SMul α (∀ i : I, f i) :=
 instance instPow [∀ i, Pow (f i) β] : Pow (∀ i, f i) β :=
   ⟨fun x b i => x i ^ b⟩
 
-@[to_additive (attr := simp, to_additive) (reorder := 5) smul_apply]
+@[to_additive (attr := simp, to_additive) (reorder := 5 6) smul_apply]
 theorem pow_apply [∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) (i : I) : (x ^ b) i = x i ^ b :=
   rfl
 #align pi.pow_apply Pi.pow_apply
 #align pi.smul_apply Pi.smul_apply
 #align pi.vadd_apply Pi.vadd_apply
 
-@[to_additive (attr := to_additive) (reorder := 5) smul_def]
+@[to_additive (attr := to_additive) (reorder := 5 6) smul_def]
 theorem pow_def [∀ i, Pow (f i) β] (x : ∀ i, f i) (b : β) : x ^ b = fun i => x i ^ b :=
   rfl
 #align pi.pow_def Pi.pow_def
 #align pi.smul_def Pi.smul_def
 #align pi.vadd_def Pi.vadd_def
 
-@[to_additive (attr := simp, to_additive) (reorder := 2 5) smul_const]
+@[to_additive (attr := simp, to_additive) (reorder:= 2 3, 5 6) smul_const]
 theorem const_pow [Pow α β] (a : α) (b : β) : const I a ^ b = const I (a ^ b) :=
   rfl
 #align pi.const_pow Pi.const_pow
 #align pi.smul_const Pi.smul_const
 #align pi.vadd_const Pi.vadd_const
 
-@[to_additive (attr := to_additive) (reorder := 6) smul_comp]
+@[to_additive (attr := to_additive) (reorder := 6 7) smul_comp]
 theorem pow_comp [Pow γ α] (x : β → γ) (a : α) (y : I → β) : (x ^ a) ∘ y = x ∘ y ^ a :=
   rfl
 #align pi.pow_comp Pi.pow_comp

Mathlib/GroupTheory/GroupAction/Prod.lean

@@ -89,30 +89,30 @@ instance pow : Pow (α × β) E where pow p c := (p.1 ^ c, p.2 ^ c)
 #align prod.has_pow Prod.pow
 #align prod.has_smul Prod.smul
 
-@[to_additive existing (attr := simp) (reorder := 6) smul_fst]
+@[to_additive existing (attr := simp) (reorder := 6 7) smul_fst]
 theorem pow_fst (p : α × β) (c : E) : (p ^ c).fst = p.fst ^ c :=
   rfl
 #align prod.pow_fst Prod.pow_fst
 
-@[to_additive existing (attr := simp) (reorder := 6) smul_snd]
+@[to_additive existing (attr := simp) (reorder := 6 7) smul_snd]
 theorem pow_snd (p : α × β) (c : E) : (p ^ c).snd = p.snd ^ c :=
   rfl
 #align prod.pow_snd Prod.pow_snd
 
 /- Note that the `c` arguments to this lemmas cannot be in the more natural right-most positions due
 to limitations in `to_additive` and `to_additive_reorder`, which will silently fail to reorder more
 than two adjacent arguments -/
-@[to_additive existing (attr := simp) (reorder := 6) smul_mk]
+@[to_additive existing (attr := simp) (reorder := 6 7) smul_mk]
 theorem pow_mk (c : E) (a : α) (b : β) : Prod.mk a b ^ c = Prod.mk (a ^ c) (b ^ c) :=
   rfl
 #align prod.pow_mk Prod.pow_mk
 
-@[to_additive existing (reorder := 6) smul_def]
+@[to_additive existing (reorder := 6 7) smul_def]
 theorem pow_def (p : α × β) (c : E) : p ^ c = (p.1 ^ c, p.2 ^ c) :=
   rfl
 #align prod.pow_def Prod.pow_def
 
-@[to_additive existing (attr := simp) (reorder := 6) smul_swap]
+@[to_additive existing (attr := simp) (reorder := 6 7) smul_swap]
 theorem pow_swap (p : α × β) (c : E) : (p ^ c).swap = p.swap ^ c :=
   rfl
 #align prod.pow_swap Prod.pow_swap