feat: simplify have blocks in Sym.simp

This PR implements support for simplifying `have` telescopes in
`Sym.simp`.

src/Lean/Meta/Sym/Simp/Main.lean

@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Simp.SimpM
+import Lean.Meta.MonadSimp
+import Lean.Meta.HaveTelescope
 import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.InferType
 import Lean.Meta.Sym.Simp.Result
@@ -15,6 +17,13 @@ import Lean.Meta.Sym.Simp.Funext
 namespace Lean.Meta.Sym.Simp
 open Internal
 
+instance : MonadSimp SimpM where
+  dsimp e := return e
+  withNewLemmas _ k := k
+  simp e := do match (← simp (← share e)) with
+    | .rfl _ => return .rfl
+    | .step e' h _ => return .step e' h
+
 def simpLambda (e : Expr) : SimpM Result := do
   -- **TODO**: Add free variable reuse
   lambdaTelescope e fun xs b => do
@@ -41,9 +50,16 @@ def simpForall (_ : Expr) : SimpM Result := do
   -- **TODO**
   return .rfl
 
-def simpLet (_ : Expr) : SimpM Result := do
-  -- **TODO**
-  return .rfl
+def simpLet (e : Expr) : SimpM Result := do
+  if !e.letNondep! then
+    /-
+    **Note**: We don't do anything if it is a dependent `let`.
+    Users may decide to `zeta`-expand them or apply `letToHave` at `pre`/`post`.
+    -/
+    return .rfl
+  else match (← Meta.simpHaveTelescope e) with
+    | .rfl => return .rfl
+    | .step e' h => return .step (← shareCommon e') h
 
 def simpApp (e : Expr) : SimpM Result := do
   congrArgs e

tests/bench/sym/simp_3.lean

@@ -0,0 +1,75 @@
+import Lean
+open Lean Meta
+opaque f : Nat → Nat
+
+namespace SimpBench
+/-!
+## `SymM` Simplifier benchmarks
+-/
+
+def getProofSize (r : Sym.Simp.Result) : MetaM Nat := do
+  match r with
+  | .rfl _ => return 0
+  | .step _ p _ => (ShareCommon.shareCommon' p).numObjs
+
+def mkSimpMethods : MetaM Sym.Simp.Methods := do
+  let thms : Sym.Simp.Theorems := {}
+  let thms := thms.insert (← Sym.Simp.mkTheoremFromDecl ``Nat.zero_add)
+  let thms := thms.insert (← Sym.Simp.mkTheoremFromDecl ``Nat.add_zero)
+  return { post := thms.rewrite }
+
+def simp (e : Expr) : MetaM (Sym.Simp.Result × Float) := Sym.SymM.run do
+  let e ← Grind.shareCommon e
+  let methods ← mkSimpMethods
+  let startTime ← IO.monoNanosNow
+  let r ← Sym.simp e methods { maxSteps := 100000000 }
+  let endTime ← IO.monoNanosNow
+  -- logInfo e
+  -- match r with
+  -- | .rfl _ => logInfo "rfl"
+  -- | .step e' h _ => logInfo e'; logInfo h; check h
+  let timeMs := (endTime - startTime).toFloat / 1000000.0
+  return (r, timeMs)
+
+def mkLetBench (n : Nat) (includeUnused : Bool) : MetaM Expr := do
+  let zero := mkNatLit 0
+  let one := mkNatLit 1
+  let rec go (n : Nat) (xs : Array Expr) (v : Expr) (e : Expr) : MetaM Expr := do
+    match n with
+    | 0 => mkLetFVars (usedLetOnly := false) (generalizeNondepLet := false) xs e
+    | n+1 =>
+      if includeUnused && n % 2 == 0 then
+        withLetDecl (nondep := true) `x (mkConst ``Nat) (mkNatAdd zero (mkNatAdd v one)) fun x =>
+          go n (xs.push x) x (mkNatAdd zero (mkNatAdd e x))
+      else
+        withLetDecl (nondep := true) `y (mkConst ``Nat) zero fun y =>
+          go n (xs.push y) v (mkNatAdd zero (mkNatAdd e zero))
+  go n #[] zero zero
+
+def benchLet (n : Nat) (includeUnused : Bool) : MetaM Unit := do
+  let e ← mkLetBench n includeUnused
+  let (r, timeMs) ← simp e
+  let proofSize ← getProofSize r
+  IO.println s!"have_{n}: {timeMs}ms, proof_size={proofSize}"
+
+set_option maxRecDepth 100000
+
+/-! ## Run all benchmarks -/
+def runAllBenchmarks : MetaM Unit := do
+  IO.println "=== Simplifier Stress Tests ==="
+  IO.println ""
+
+  IO.println ""
+  IO.println "--- Benchmark 1: have block without unused variables ---"
+  for n in [10, 20, 30, 40, 50, 60, 70, 80, 90, 100, 110, 120, 130, 140, 150, 200, 300, 400, 500,
+    600, 700, 800, 900, 1000, 1200, 1400, 1600, 1800, 2000] do
+    benchLet n false
+
+  IO.println "--- Benchmark 2: have block with unused variables ---"
+  for n in [10, 20, 30, 40, 50, 60, 70, 80, 90, 100, 110, 120, 130, 140, 150, 200, 300, 400, 500,
+    600, 700, 800, 900, 1000, 1200, 1400, 1600, 1800, 2000] do
+    benchLet n true
+
+#eval runAllBenchmarks
+
+end SimpBench