feat: intro tactic for SymM (#11803)

This PR implements `intro` (and its variants) for `SymM`. These versions
do not use reduction or infer types, and ensure expressions are
maximally shared.

src/Lean/Meta/Sym.lean

@@ -12,6 +12,8 @@ public import Lean.Meta.Sym.MaxFVar
 public import Lean.Meta.Sym.ReplaceS
 public import Lean.Meta.Sym.LooseBVarsS
 public import Lean.Meta.Sym.InstantiateS
+public import Lean.Meta.Sym.IsClass
+public import Lean.Meta.Sym.Intro
 
 /-!
 # Symbolic simulation support.
@@ -48,9 +50,7 @@ of `lctx₂`, we only need to verify that `lctx₂` contains the maximal free va
 means `x` is the free variable with maximal index occurring in `e`. When assigning `?m := e`, we check
 whether `maxFVar[e]` is in `?m.lctx` — a single hash lookup, O(1).
 
-**Maintaining `maxFVar`:** The mapping is updated during `intro`. The default `intro` in `MetaM` uses
-`instantiate` to replace `Expr.bvar` with `Expr.fvar`, using `looseBVarRange` to skip subexpressions
-without relevant bound variables. The `SymM` version piggybacks on this traversal to update `maxFVar`.
+**Maintaining `maxFVar`:** The mapping is automatically updated when we use `getMaxFVar?`.
 
 ### Skipping type checks on assignment
 

src/Lean/Meta/Sym/Intro.lean

@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2025 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.SymM
+import Lean.Meta.Sym.InstantiateS
+import Lean.Meta.Sym.IsClass
+import Lean.Meta.Tactic.Grind.AlphaShareBuilder
+namespace Lean.Meta.Sym
+
+/--
+Efficient `intro` for symbolic simulation.
+-/
+def introCore (goal : Goal) (max : Nat) (names : Array Name) : SymM (Array FVarId × Goal) := do
+  if max == 0 then return (#[], goal)
+  let env ← getEnv
+  let mvarId := goal.mvarId
+  let mvarDecl ← mvarId.getDecl
+  /-
+  Helper function for constructing a value to assign to `mvarId`. We don't need max sharing here.
+  -/
+  let rec mkValueLoop (i : Nat) (type : Expr) (body : Expr) : Expr :=
+    if i >= max then
+      body
+    else match type with
+      | .mdata _ type => mkValueLoop i type body
+      | .forallE name domain type bi =>
+         mkLambda name bi domain (mkValueLoop (i+1) type body)
+      | .letE name valType value type c =>
+        mkLet name valType value (mkValueLoop (i+1) type body) c
+      | _ => body
+  /-
+  Constructs `e #(n-1) ... #0`. This is helper function for constructing a value to assign to `mvarId`.
+  -/
+  let rec mkAppBVars (e : Expr) (n : Nat) : Expr :=
+    match n with
+    | 0 => e
+    | n+1 => mkAppBVars (mkApp e (mkBVar n)) n
+  /-
+  Constructs a value to assign to `mvarId` using `mkValueLoop` and `mkAppBVars`.
+  -/
+  let mkValueAndAssign (fvars : Array Expr) (mvarId' : MVarId) : MetaM Unit := do
+    let auxMVar ← mkFreshExprMVarAt mvarDecl.lctx mvarDecl.localInstances mvarDecl.type .syntheticOpaque
+    let val := mkAppBVars auxMVar fvars.size
+    let val := mkValueLoop 0 mvarDecl.type val
+    assignDelayedMVar auxMVar.mvarId! fvars mvarId'
+    mvarId.assign val
+  let finalize (lctx : LocalContext) (localInsts : LocalInstances) (fvars : Array Expr) (type : Expr) : SymM (Array Expr × MVarId) := do
+    let type ← instantiateRevS type fvars
+    let mvar' ← mkFreshExprMVarAt lctx localInsts type .syntheticOpaque mvarDecl.userName
+    let mvarId' := mvar'.mvarId!
+    mkValueAndAssign fvars mvarId'
+    return (fvars, mvarId')
+  let mkName (binderName : Name) (i : Nat) : MetaM Name := do
+    if h : i < names.size then
+      return names[i]
+    else
+      mkFreshUserName binderName
+  let updateLocalInsts (localInsts : LocalInstances) (fvar : Expr) (type : Expr) : LocalInstances :=
+    if let some className := isClass? env type then
+      localInsts.push { fvar, className }
+    else
+      localInsts
+  let rec visit (i : Nat) (lctx : LocalContext) (localInsts : LocalInstances) (fvars : Array Expr) (type : Expr) : SymM (Array Expr × MVarId) := do
+    if i >= max then
+      finalize lctx localInsts fvars type
+    else match type with
+    | .mdata _ type => visit i lctx localInsts fvars type
+    | .forallE n type body bi =>
+      let type       ← instantiateRevS type fvars
+      let fvarId     ← mkFreshFVarId
+      let lctx       := lctx.mkLocalDecl fvarId (← mkName n i) type bi
+      let fvar       ← Grind.mkFVarS fvarId
+      let fvars      := fvars.push fvar
+      let localInsts := updateLocalInsts localInsts fvar type
+      visit (i+1) lctx localInsts fvars body
+    | .letE n type value body nondep =>
+      let type       ← instantiateRevS type fvars
+      let value      ← instantiateRevS value fvars
+      let fvarId     ← mkFreshFVarId
+      let lctx       := lctx.mkLetDecl fvarId (← mkName n i) type value nondep
+      let fvar       ← Grind.mkFVarS fvarId
+      let fvars      := fvars.push fvar
+      let localInsts := updateLocalInsts localInsts fvar type
+      visit (i+1) lctx localInsts fvars body
+    | _ => finalize lctx localInsts fvars type
+  let (fvars, mvarId') ← visit 0 mvarDecl.lctx mvarDecl.localInstances #[] mvarDecl.type
+  return (fvars.map (·.fvarId!), { goal with mvarId := mvarId' })
+
+def hugeNat := 1000000
+
+/--
+Introduces leading binders (universal quantifiers and let-expressions) from the goal's target type.
+
+If `names` is non-empty, introduces (at most) `names.size` binders using the provided names.
+If `names` is empty, introduces all leading binders using inaccessible names.
+
+Returns the introduced free variable Ids and the updated goal.
+
+Throws an error if the target type does not have a leading binder.
+-/
+public def intros (goal : Goal) (names : Array Name := #[]) : SymM (Array FVarId × Goal) := do
+  let result ← if names.isEmpty then
+    introCore goal hugeNat #[]
+  else
+    introCore goal names.size names
+  if result.1.isEmpty then
+    throwError "`intros` failed, binder expected"
+  return result
+
+/--
+Introduces a single binder from the goal's target type with the given name.
+
+Returns the introduced free variable ID and the updated goal.
+Throws an error if the target type does not have a leading binder.
+-/
+public def intro (goal : Goal) (name : Name) : SymM (FVarId × Goal) := do
+  let (fvarIds, goal') ← introCore goal 1 #[name]
+  if h : 0 < fvarIds.size then
+    return (fvarIds[0], goal)
+  else
+    throwError "`intro` failed, binder expected"
+
+/--
+Introduces exactly `num` binders from the goal's target type.
+
+Returns the introduced free variable IDs and the updated goal.
+Throws an error if the target type has fewer than `num` leading binders.
+-/
+public def introN (goal : Goal) (num : Nat) : SymM (Array FVarId × Goal) := do
+  let result ← introCore goal num #[]
+  unless result.1.size == num do
+    throwError "`introN` failed, insufficient number of binders"
+  return result
+
+end Lean.Meta.Sym

src/Lean/Meta/Sym/IsClass.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2025 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.SymM
+namespace Lean.Meta.Sym
+
+/--
+Efficient version of `Meta.isClass?` for symbolic simulation. It does not use
+reduction nor instantiates metavariables.
+-/
+public def isClass? (env : Environment) (type : Expr) : Option Name :=
+  go type
+where
+  go : Expr → Option Name
+  | .bvar ..         => none
+  | .lit ..          => none
+  | .fvar ..         => none
+  | .sort ..         => none
+  | .lam ..          => none
+  | .proj ..         => none
+  | .mvar ..         => none
+  | .letE _ _ _ b _  => go b
+  | .forallE _ _ b _ => go b
+  | .mdata _ b       => go b
+  | .const n _       => if isClass env n then some n else none
+  | .app f _         => go f
+
+end Lean.Meta.Sym

tests/lean/run/sym_intro.lean

@@ -0,0 +1,38 @@
+import Lean.Meta.Sym
+
+macro "gen_term" n:num : term => do
+  let mut stx ← `(True)
+  for _ in 0...n.getNat do
+    stx := ← `(let z : Nat := x + y; let y := y + 1; have : y >= 0 := Nat.zero_le y; forall x : Nat, $stx)
+  `(let z : Nat := 0 ; forall x : Nat, forall y : Nat, $stx)
+
+open Lean Meta Sym Elab Tactic
+
+def test (mvarId : MVarId) : MetaM MVarId := do
+  SymM.run' do
+    let goal ← mkGoal mvarId
+    let (_, goal) ← intros goal
+    return goal.mvarId
+
+/--
+trace: z✝² : Nat := 0
+x✝² y✝² : Nat
+z✝¹ : Nat := x✝² + y✝²
+y✝¹ : Nat := y✝² + 1
+this✝¹ : y✝¹ ≥ 0
+x✝¹ : Nat
+z✝ : Nat := x✝¹ + y✝¹
+y✝ : Nat := y✝¹ + 1
+this✝ : y✝ ≥ 0
+x✝ : Nat
+⊢ True
+-/
+#guard_msgs in
+example : gen_term 2 := by
+  run_tac liftMetaTactic1 fun mvarId => test mvarId
+  trace_state
+  constructor
+
+example : gen_term 70 := by
+  run_tac liftMetaTactic1 fun mvarId => test mvarId
+  constructor