perf: improve to_additive performance (#1060)

Using
```
def Ones : ℕ → Q(Nat)
| 0     => q(1)
| (n+1) => q($(Ones n) + $(Ones n))
```
The new `to_additive` takes `45ms` on `Ones 500` (higher gives stack overflows)
The old `to_additive` takes `13794ms` on `Ones 17` (exponential in the argument)
There is still one issue workaround by using `transform` in `etaExpand`.

* Remove `replaceRecM` and `replaceRecMeta` that are exponentially slow
* Remove `replaceRecTraversal` because its interface is less convenient than `replaceRec`



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib.lean

@@ -269,6 +269,7 @@ import Mathlib.Init.Data.List.Basic
 import Mathlib.Init.Data.List.Lemmas
 import Mathlib.Init.Data.Nat.Basic
 import Mathlib.Init.Data.Nat.Lemmas
+import Mathlib.Init.Data.Nat.Notation
 import Mathlib.Init.Data.Ordering.Basic
 import Mathlib.Init.Data.Prod
 import Mathlib.Init.Data.Quot

Mathlib/Algebra/GroupPower/Order.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.Order.WithZero
 import Mathlib.Algebra.GroupPower.Ring
 import Mathlib.Data.Set.Intervals.Basic
 import Mathlib.Data.Nat.Basic
+import Mathlib.Init.Data.Nat.Basic
 
 /-!
 # Lemmas about the interaction of power operations with order

Mathlib/Data/Fin/Fin2.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Std.Tactic.NoMatch
-import Mathlib.Init.Data.Nat.Basic
+import Mathlib.Init.Data.Nat.Notation
 
 /-!
 # Inductive type variant of `Fin`

Mathlib/Data/Stream/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Mathlib.Mathport.Rename
-import Mathlib.Init.Data.Nat.Basic
+import Mathlib.Init.Data.Nat.Notation
 /-!
 # Definition of `Stream'` and functions on streams
 

Mathlib/Init/Data/Fin/Basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Mathlib.Init.Data.Nat.Basic
+import Mathlib.Init.Data.Nat.Notation
 import Mathlib.Util.MapsTo
 
 /-!

Mathlib/Init/Data/Int/Basic.lean

@@ -6,7 +6,7 @@ Authors: Jeremy Avigad
 The integers, with addition, multiplication, and subtraction.
 -/
 import Mathlib.Mathport.Rename
-import Mathlib.Init.Data.Nat.Basic
+import Mathlib.Init.Data.Nat.Notation
 import Mathlib.Init.ZeroOne
 import Std.Data.Int.Lemmas
 

Mathlib/Init/Data/List/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Mathlib.Mathport.Rename
-import Mathlib.Init.Data.Nat.Basic
+import Mathlib.Init.Data.Nat.Notation
 import Std.Data.Nat.Lemmas
 import Std.Data.List.Basic
 /-!

Mathlib/Init/Data/List/Lemmas.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 import Mathlib.Mathport.Rename
 import Std.Data.List.Basic
 import Std.Data.List.Lemmas
-import Mathlib.Init.Data.Nat.Basic
+import Mathlib.Init.Data.Nat.Notation
 import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Init.Data.List.Basic
 /-!

Mathlib/Init/Data/Nat/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura
 -/
 import Mathlib.Init.ZeroOne
-notation "ℕ" => Nat
+import Mathlib.Init.Data.Nat.Notation
 
 namespace Nat
 

Mathlib/Init/Data/Nat/Lemmas.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad
 -/
 import Std.Data.Nat.Lemmas
-import Mathlib.Init.Data.Nat.Basic
+import Mathlib.Init.Data.Nat.Notation
 import Mathlib.Init.Algebra.Functions
 
 universe u

Mathlib/Init/Data/Nat/Notation.lean

@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Leonardo de Moura
+-/
+
+/-!
+# Notation `ℕ` for the natural numbers.
+-/
+
+notation "ℕ" => Nat

Mathlib/Lean/Expr/ReplaceRec.lean

@@ -31,42 +31,4 @@ def replaceRec (f? : (Expr → Expr) → Expr → Option Expr) : Expr → Expr :
     | some x => x
     | none   => traverseChildren (M := Id) r e
 
-/-- replaceRec under a monad. -/
-partial def replaceRecM [Monad M] (f? : (Expr → M Expr) → Expr → M (Option Expr)) (e : Expr) :
-    M Expr := do
-  match ← f? (replaceRecM f?) e with
-  | some x => return x
-  | none => traverseChildren (replaceRecM f?) e
-
-/-- Similar to `replaceRecM` except that bound variables are instantiated with free variables
-(like `Lean.Meta.transform`).
-This means that MetaM tactics can be used inside the replacement function.
-
-If you don't need recursive calling,
-you should prefer using `Lean.Meta.transform` because it also caches visits.
- -/
-partial def replaceRecMeta [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M]
-    (f? : (Expr → M Expr) → Expr → M (Option Expr)) (e : Expr) : M Expr := do
-  match ← f? (replaceRecMeta f?) e with
-  | some x => return x
-  | none => Lean.Meta.traverseChildren (replaceRecMeta f?) e
-
-/-- A version of `Expr.replace` where we can use recursive calls even if we replace a subexpression.
-  When reaching a subexpression `e` we call `traversal e` to see if we want to do anything with this
-  expression. If `traversal e = none` we proceed to the children of `e`. If
-  `traversal e = some (#[e₁, ..., eₙ], g)`, we first recursively apply this function to
-  `#[e₁, ..., eₙ]` to get new expressions `#[f₁, ..., fₙ]`.
-  Then we replace `e` by `g [f₁, ..., fₙ]`.
-
-  Important: In order for this function to terminate, the `[e₁, ..., eₙ]` must all be smaller than
-  `e` according to some measure  (and this measure must also be strictly decreasing on the w.r.t.
-  the structural subterm relation).
-  -/
-def replaceRecTraversal (traversal : Expr → Option (Array Expr × (Array Expr → Expr))) :
-    Expr → Expr :=
-  replaceRec fun r e ↦
-    match traversal e with
-    | none => none
-    | some (get, set) => some <| set <| .map r <| get
-
 end Lean.Expr

Mathlib/Tactic/PermuteGoals.lean

@@ -6,7 +6,7 @@ Authors: Arthur Paulino, Mario Carneiro
 
 import Lean
 import Std.Data.List.Basic
-import Mathlib.Init.Data.Nat.Basic
+import Mathlib.Init.Data.Nat.Notation
 
 namespace Mathlib.Tactic
 

Mathlib/Tactic/Simps/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import Mathlib.Init.Data.Nat.Basic
+import Mathlib.Init.Data.Nat.Notation
 import Mathlib.Lean.Message
 import Mathlib.Tactic.ToAdditive
 import Mathlib.Tactic.Simps.NotationClass