From c0d5e8bc2c925bc2b60f18c929acf7d73ea9ecec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Dec 2025 19:45:33 -0800 Subject: [PATCH] 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 | 6 +- src/Lean/Meta/Sym/Intro.lean | 139 +++++++++++++++++++++++++++++++++ src/Lean/Meta/Sym/IsClass.lean | 32 ++++++++ tests/lean/run/sym_intro.lean | 38 +++++++++ 4 files changed, 212 insertions(+), 3 deletions(-) create mode 100644 src/Lean/Meta/Sym/Intro.lean create mode 100644 src/Lean/Meta/Sym/IsClass.lean create mode 100644 tests/lean/run/sym_intro.lean diff --git a/src/Lean/Meta/Sym.lean b/src/Lean/Meta/Sym.lean index 33c54a8a81..4a2db00d8b 100644 --- a/src/Lean/Meta/Sym.lean +++ b/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 diff --git a/src/Lean/Meta/Sym/Intro.lean b/src/Lean/Meta/Sym/Intro.lean new file mode 100644 index 0000000000..4716bf2f7e --- /dev/null +++ b/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 diff --git a/src/Lean/Meta/Sym/IsClass.lean b/src/Lean/Meta/Sym/IsClass.lean new file mode 100644 index 0000000000..ab290469b8 --- /dev/null +++ b/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 diff --git a/tests/lean/run/sym_intro.lean b/tests/lean/run/sym_intro.lean new file mode 100644 index 0000000000..ade7f95055 --- /dev/null +++ b/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