perf: add performance comparison tests for SymM vs MetaM (#11838)

This PR adds performance comparison tests between the new `SymM` monad
and the standard `MetaM` for `intros`/`apply` operations.

The tests solve problems of the form:
```lean
let z := 0; ∀ x, ∃ y, x = z + y ∧ let z := z + x; ∀ x, ∃ y, x = z + y ∧ ... ∧ True
```
using repeated `intros` and `apply` with `Exists.intro`, `And.intro`,
`Eq.refl`, and `True.intro`.

**Results show 10-20x speedup:**

| Size | MetaM | SymM | Speedup |
|------|-------|------|---------|
| 1000 | 226ms | 21ms | 10.8x |
| 2000 | 582ms | 44ms | 13.2x |
| 3000 | 1.08s | 72ms | 15.0x |
| 4000 | 1.72s | 101ms | 17.0x |
| 5000 | 2.49s | 125ms | 19.9x |
| 6000 | 3.45s | 157ms | 22.0x |

Author: leodemoura

tests/lean/sym/perf_meta_apply.lean

@@ -0,0 +1,78 @@
+import Lean.Meta.Tactic
+
+open Lean Meta
+def profileM {α : Type} (k : MetaM α) (msg : String := "experiment") : MetaM α :=
+  profileitM Exception msg ({ : Options }.setBool `profiler true |>.setNat `profiler.threshold 0)  k
+
+def genTerm (n : Nat) : Expr := Id.run do
+  let mut e := mkConst ``True
+  let nat := mkConst ``Nat
+  for _ in 0...n do
+    let eq := mkApp3 (mkConst ``Eq [1]) nat (mkBVar 0) (mkNatAdd (mkBVar 2) (mkBVar 1))
+    e := mkApp2 (mkConst ``And) eq e
+    e := mkApp2 (mkConst ``Exists [1]) nat (mkLambda `y .default nat e)
+    e := mkForall `x .default nat e
+    e := mkLet `z nat (mkNatAdd (mkBVar 1) (mkBVar 0)) e
+  let eq := mkApp3 (mkConst ``Eq [1]) nat (mkBVar 0) (mkNatAdd (mkBVar 2) (mkBVar 1))
+  e := mkApp2 (mkConst ``And) eq e
+  e := mkApp2 (mkConst ``Exists [1]) nat (mkLambda `y .default nat e)
+  e := mkForall `x .default nat e
+  e := mkLet `z nat (mkNatLit 0) e
+  return e
+
+set_option maxRecDepth 10000000
+
+def tryIntros? (goals : List MVarId) : MetaM (Option (List MVarId)) := do
+  let goal :: goals := goals | return none
+  let (fvars, goal') ← goal.intros
+  if fvars.isEmpty then return none
+  return some (goal' :: goals)
+
+def tryApply? (declName : Name) (goals : List MVarId) : MetaM (Option (List MVarId)) := do
+  let goal :: goals := goals | return none
+  try
+    let goals' ← goal.applyConst declName
+    return some (goals' ++ goals)
+  catch _ =>
+    return none
+
+def tryApplyAny? (declNames : List Name) (goals : List MVarId) : MetaM (Option (List MVarId)) := do
+  match declNames with
+  | [] => return none
+  | declName :: declNames =>
+    if let some goals' ← tryApply? declName goals then
+      return some goals'
+    else
+      tryApplyAny? declNames goals
+
+def solve (n : Nat) (type : Expr) : MetaM Unit := profileM (msg := s!"size {n}") do
+  let mvarId := (← mkFreshExprMVar type).mvarId!
+  discard <| go 10000000 [mvarId]
+  return ()
+where
+  go (fuel : Nat) (goals : List MVarId) : MetaM Bool := do
+    let fuel + 1 := fuel | throwError "out of fuel"
+    let goal :: goals' := goals | return true
+    if (← goal.isAssigned) then
+      go fuel goals'
+    else
+      if let some goals' ← tryIntros? goals then
+        go fuel goals'
+      else if let some goals' ← tryApplyAny? [``Exists.intro, ``And.intro, ``Eq.refl, ``True.intro] goals then
+        go fuel goals'
+      else
+        throwError "Stuck at {goal}"
+
+def test (n : Nat) : MetaM Unit := do
+  let e := genTerm n
+  solve n e
+
+-- We are solving problems of the following form
+#eval logInfo (genTerm 2)
+
+#eval test 1000
+#eval test 2000
+#eval test 3000
+#eval test 4000
+#eval test 5000
+#eval test 6000

tests/lean/sym/perf_sym_apply.lean

@@ -0,0 +1,83 @@
+import Lean.Meta.Tactic
+import Lean.Meta.Sym
+
+open Lean Meta Sym
+def profileM {α : Type} (k : MetaM α) (msg : String := "experiment") : MetaM α :=
+  profileitM Exception msg ({ : Options }.setBool `profiler true |>.setNat `profiler.threshold 0)  k
+
+def genTerm (n : Nat) : Expr := Id.run do
+  let mut e := mkConst ``True
+  let nat := mkConst ``Nat
+  for _ in 0...n do
+    let eq := mkApp3 (mkConst ``Eq [1]) nat (mkBVar 0) (mkNatAdd (mkBVar 2) (mkBVar 1))
+    e := mkApp2 (mkConst ``And) eq e
+    e := mkApp2 (mkConst ``Exists [1]) nat (mkLambda `y .default nat e)
+    e := mkForall `x .default nat e
+    e := mkLet `z nat (mkNatAdd (mkBVar 1) (mkBVar 0)) e
+  let eq := mkApp3 (mkConst ``Eq [1]) nat (mkBVar 0) (mkNatAdd (mkBVar 2) (mkBVar 1))
+  e := mkApp2 (mkConst ``And) eq e
+  e := mkApp2 (mkConst ``Exists [1]) nat (mkLambda `y .default nat e)
+  e := mkForall `x .default nat e
+  e := mkLet `z nat (mkNatLit 0) e
+  return e
+
+set_option maxRecDepth 10000000
+
+def tryIntros? (goals : List Goal) : SymM (Option (List Goal)) := do
+  try
+    let goal :: goals := goals | return none
+    let (_, goal') ← intros goal
+    return some (goal' :: goals)
+  catch _ =>
+    return none
+
+def tryApply? (rule : BackwardRule) (goals : List Goal) : SymM (Option (List Goal)) := do
+  let goal :: goals := goals | return none
+  try
+    let goals' ← rule.apply goal
+    return some (goals' ++ goals)
+  catch _ =>
+    return none
+
+def tryApplyAny? (rules : List BackwardRule) (goals : List Goal) : SymM (Option (List Goal)) := do
+  match rules with
+  | [] => return none
+  | rule :: rules =>
+    if let some goals' ← tryApply? rule goals then
+      return some goals'
+    else
+      tryApplyAny? rules goals
+
+def solve (n : Nat) (type : Expr) : MetaM Unit := profileM (msg := s!"size {n}") <| SymM.run' do
+  let mvarId := (← mkFreshExprMVar type).mvarId!
+  let rules ← [``Exists.intro, ``And.intro, ``Eq.refl, ``True.intro].mapM fun declName => mkBackwardRuleFromDecl declName
+  let goal ← mkGoal mvarId
+  discard <| go 10000000 rules [goal]
+  return ()
+where
+  go (fuel : Nat) (rules : List BackwardRule) (goals : List Goal) : SymM Bool := do
+    let fuel + 1 := fuel | throwError "out of fuel"
+    let goal :: goals' := goals | return true
+    if (← goal.mvarId.isAssigned) then
+      go fuel rules goals'
+    else
+      if let some goals' ← tryIntros? goals then
+        go fuel rules goals'
+      else if let some goals' ← tryApplyAny? rules goals then
+        go fuel rules goals'
+      else
+        throwError "Stuck at {goal.mvarId}"
+
+def test (n : Nat) : MetaM Unit := do
+  let e := genTerm n
+  solve n e
+
+-- We are solving problems of the following form
+#eval logInfo (genTerm 2)
+
+#eval test 1000
+#eval test 2000
+#eval test 3000
+#eval test 4000
+#eval test 5000
+#eval test 6000