feat: add simpTelescope simproc for simplifying binders before intro (#12154)

This PR adds `simpTelescope`, a simproc that simplifies telescope
binders (`have`-expression values and arrow hypotheses) but not the
final body. This is useful for simplifying targets before introducing
hypotheses.

src/Lean/Meta/Sym/Simp.lean

@@ -22,3 +22,4 @@ public import Lean.Meta.Sym.Simp.EvalGround
 public import Lean.Meta.Sym.Simp.Discharger
 public import Lean.Meta.Sym.Simp.ControlFlow
 public import Lean.Meta.Sym.Simp.Goal
+public import Lean.Meta.Sym.Simp.Telescope

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

@@ -94,17 +94,17 @@ Returns the simplified result paired with the remaining `ArrowInfo` list. When a
 collapses (e.g., to `True`), the returned `infos` list is empty, signaling to `toForall`
 that no reconstruction is needed.
 -/
-partial def simpArrows (e : Expr) (infos : List ArrowInfo) : SimpM (Result × List ArrowInfo) := do
+partial def simpArrows (e : Expr) (infos : List ArrowInfo) (simpBody : Simproc) : SimpM (Result × List ArrowInfo) := do
   match infos with
-  | [] => return ((← simp e), [])
+  | [] => return ((← simpBody e), [])
   | info :: infos' =>
-    let_expr f@Arrow p q := e | return ((← simp e), infos)
+    let_expr f@Arrow p q := e | return ((← simpBody e), infos)
     let p_r ← simp p
     if (← isFalseExpr (p_r.getResultExpr p)) && info.v.isZero then
       match p_r with
       | .rfl _ => return (.step (← getTrueExpr) (mkApp (mkConst ``false_arrow) q), [])
       | .step _ h _ => return (.step (← getTrueExpr) (mkApp3 (mkConst ``false_arrow_congr) p q h), [])
-    let (q_r, infos') ← simpArrows q infos'
+    let (q_r, infos') ← simpArrows q infos' simpBody
     if (← isTrueExpr (q_r.getResultExpr q)) then
       match q_r with
       | .rfl _ => return (.step (← getTrueExpr) (mkApp (mkConst ``arrow_true [info.u]) p), [])
@@ -157,10 +157,10 @@ a chance to apply `post` methods to the intermediate arrow `p → p`.
 Thus, this is a simproc that is meant to be used as a pre-method and marks the
 result as fully simplified to prevent `simpArrow` from being applied.
 -/
-public def simpArrowTelescope : Simproc := fun e => do
+public def simpArrowTelescope (simpBody : Simproc := simp) : Simproc := fun e => do
   unless e.isArrow do return .rfl -- not applicable
   let { arrow, infos, v } ← toArrow e
-  let (.step arrow' h _, infos) ← simpArrows arrow infos | return .rfl (done := true)
+  let (.step arrow' h _, infos) ← simpArrows arrow infos simpBody | return .rfl (done := true)
   let e' ← toForall arrow' infos
   let α := mkSort v
   let v1 := v.succ
@@ -190,7 +190,7 @@ public def simpArrow (e : Expr) : SimpM Result := do
     let e' ← e.updateForallS! p' q'
     return .step e' <| mkApp6 (mkConst ``implies_congr [u, v]) p p' q q' h₁ h₂
 
-public def simpForall (e : Expr) : SimpM Result := do
+public def simpForall' (simpArrow : Simproc) (simpBody : Simproc) (e : Expr) : SimpM Result := do
   if e.isArrow then
     simpArrow e
   else if (← isProp e) then
@@ -201,7 +201,7 @@ public def simpForall (e : Expr) : SimpM Result := do
     return .rfl
 where
   main (xs : Array Expr) (b : Expr) : SimpM Result := do
-    match (← simp b) with
+    match (← simpBody b) with
     | .rfl _ => return .rfl
     | .step b' h _ =>
       let h ← mkLambdaFVars xs h
@@ -216,4 +216,7 @@ where
     | .forallE _ _ b _ => if b.hasLooseBVar 0 then getForallTelescopeSize b (n+1) else n
     | _ => n
 
+public def simpForall : Simproc :=
+  simpForall' simpArrow simp
+
 end Lean.Meta.Sym.Simp

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

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.Simp.SimpM
-import Lean.Meta.Sym.Simp.Lambda
+public import Lean.Meta.Sym.Simp.Lambda
 import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.InstantiateS
 import Lean.Meta.Sym.ReplaceS
@@ -316,7 +316,8 @@ For each application `f a`:
 - If only `a` changed: use `congrArg : a = a' → f a = f a'`
 - If neither changed: return `.rfl`
 -/
-def simpBetaApp (e : Expr) (fType : Expr) (fnUnivs argUnivs : Array Level) : SimpM Result := do
+def simpBetaApp (e : Expr) (fType : Expr) (fnUnivs argUnivs : Array Level)
+    (simpBody : Simproc) : SimpM Result := do
   return (← go e 0).1
 where
   go (e : Expr) (i : Nat) : SimpM (Result × Expr) := do
@@ -339,7 +340,7 @@ where
           let h := mkApp6 (← mkCongrPrefix ``congr fType i) f f' a a' hf ha
           pure <| .step e' h
       return (r, fType.bindingBody!)
-    | .lam .. => return (← simpLambda e, fType)
+    | .lam .. => return (← simpBody e, fType)
     | _ => unreachable!
 
   mkCongrPrefix (declName : Name) (fType : Expr) (i : Nat) : SymM Expr := do
@@ -375,12 +376,12 @@ e₃ = e₄    (by rfl, definitional equality from toHave)
 e₁ = e₄    (by transitivity)
 ```
 -/
-def simpHaveCore (e : Expr) : SimpM SimpHaveResult := do
+def simpHaveCore (e : Expr) (simpBody : Simproc) : SimpM SimpHaveResult := do
   let e₁ := e
   let r ← toBetaApp e₁
   let e₂ := r.e
   let { fnUnivs, argUnivs } ← getUnivs r.fType
-  match (← simpBetaApp e₂ r.fType fnUnivs argUnivs) with
+  match (← simpBetaApp e₂ r.fType fnUnivs argUnivs simpBody) with
   | .rfl _ => return { result := .rfl, α := r.α, u := r.u }
   | .step e₃ h _ =>
     let h₁ := mkApp6 (mkConst ``Eq.trans [r.u]) r.α e₁ e₂ e₃ r.h h
@@ -397,8 +398,8 @@ Simplify a `have`-telescope.
 This is the main entry point for `have`-telescope simplification in `Sym.simp`.
 See module documentation for the algorithm overview.
 -/
-public def simpHave (e : Expr) : SimpM Result := do
-  return (← simpHaveCore e).result
+public def simpHave (e : Expr) (simpBody : Simproc) : SimpM Result := do
+  return (← simpHaveCore e simpBody).result
 
 /--
 Simplify a `have`-telescope and eliminate unused bindings.
@@ -406,8 +407,8 @@ Simplify a `have`-telescope and eliminate unused bindings.
 This combines simplification with dead variable elimination in a single pass,
 avoiding quadratic behavior from multiple passes.
 -/
-public def simpHaveAndZetaUnused (e₁ : Expr) : SimpM Result := do
-  let r ← simpHaveCore e₁
+public def simpHaveAndZetaUnused (e₁ : Expr) (simpBody : Simproc) : SimpM Result := do
+  let r ← simpHaveCore e₁ simpBody
   match r.result with
   | .rfl _ =>
     let e₂ ← zetaUnused e₁
@@ -425,7 +426,7 @@ public def simpHaveAndZetaUnused (e₁ : Expr) : SimpM Result := do
         (mkApp2 (mkConst ``Eq.refl [r.u]) r.α e₃)
       return .step e₃ h
 
-public def simpLet (e : Expr) : SimpM Result := do
+public def simpLet' (simpBody : Simproc) (e : Expr) : SimpM Result := do
   if !e.letNondep! then
     /-
     **Note**: We don't do anything if it is a dependent `let`.
@@ -433,6 +434,9 @@ public def simpLet (e : Expr) : SimpM Result := do
     -/
     return .rfl
   else
-    simpHaveAndZetaUnused e
+    simpHaveAndZetaUnused e simpBody
+
+public def simpLet : Simproc :=
+  simpLet' simpLambda
 
 end Lean.Meta.Sym.Simp

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

@@ -46,12 +46,12 @@ def mkFunextFor (xs : Array Expr) (β : Expr) : MetaM Expr := do
   let result ← mkLambdaFVars #[f, g, h] result
   return result
 
-public def simpLambda (e : Expr) : SimpM Result := do
+public def simpLambda' (simpBody : Simproc) (e : Expr) : SimpM Result := do
   lambdaTelescope e fun xs b => withoutModifyingCacheIfNotWellBehaved do
     main xs (← shareCommon b)
 where
   main (xs : Array Expr) (b : Expr) : SimpM Result := do
-    match (← simp b) with
+    match (← simpBody b) with
     | .rfl _ => return .rfl
     | .step b' h _ =>
       let h ← mkLambdaFVars xs h
@@ -69,4 +69,7 @@ where
       modify fun s => { s with funext := s.funext.insert { expr := key } h }
       return h
 
+public def simpLambda : Simproc :=
+  simpLambda' simp
+
 end Lean.Meta.Sym.Simp

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

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2026 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.Simp.SimpM
+import Lean.Meta.Sym.Simp.Have
+import Lean.Meta.Sym.Simp.Forall
+namespace Lean.Meta.Sym.Simp
+/--
+Simplify telescope binders (`have`-expression values, and arrow hypotheses)
+but not the final body. This simproc is useful to simplify target before
+introducing.
+-/
+public partial def simpTelescope : Simproc := fun e => do
+  match e with
+  | .letE .. =>
+    simpLet' (simpLambda' simpTelescope) e
+  | .forallE .. =>
+    simpForall' (simpArrow := simpArrowTelescope simpTelescope) (simpBody := simpLambda' simpTelescope) e
+  | _ => return .rfl
+
+end Lean.Meta.Sym.Simp

tests/lean/run/sym_simp_5.lean

@@ -0,0 +1,33 @@
+import Lean
+open Lean Meta Elab Tactic
+
+elab "sym_simp" "[" declNames:ident,* "]" : tactic => do
+  let rewrite ← Sym.mkSimprocFor (← declNames.getElems.mapM fun s => realizeGlobalConstNoOverload s.raw) Sym.Simp.dischargeSimpSelf
+  let methods : Sym.Simp.Methods := {
+    pre  := Sym.Simp.simpTelescope
+    post := Sym.Simp.evalGround.andThen rewrite
+  }
+  liftMetaTactic1 fun mvarId => Sym.SymM.run do
+    let mvarId ← Sym.preprocessMVar mvarId
+    (← Sym.simpGoal mvarId methods).toOption
+
+set_option warn.sorry false
+
+/-!
+Recall that `simpTelescope` does not simplify the body of a telescope.
+This is why `0 + x = 0 + id x` is not simplified in the following example.
+-/
+/--
+trace: p q : Prop
+⊢ q →
+    ∀ (x : Nat),
+      p →
+        have x := x;
+        have y := x;
+        x = y → 0 + x = 0 + id x
+-/
+#guard_msgs in
+example (p q : Prop) : q → ∀ x : Nat, p ∧ True → have x := 0 + x; have y := x; True → x = 0 + 0 + id y → 0 + x = 0 + id x := by
+  sym_simp [and_true, Nat.zero_add, id_eq]
+  trace_state
+  admit