feat: cleanup metavars

src/Lean/Meta/Sym/Apply.lean

@@ -44,8 +44,11 @@ first because solving it often solves `?w`.
 def mkResultPos (pattern : Pattern) : List Nat := Id.run do
   let auxPrefix := `_sym_pre
   -- Initialize "found" mask with arguments that can be synthesized by type class resolution.
-  let mut found := pattern.isInstance
   let numArgs := pattern.varTypes.size
+  let mut found := if let some varInfos := pattern.varInfos? then
+     varInfos.argsInfo.map fun info : ProofInstArgInfo => info.isInstance
+  else
+     Array.replicate numArgs false
   let auxVars := pattern.varTypes.mapIdx fun i _ => mkFVar ⟨.num auxPrefix i⟩
   -- Collect arguments that occur in the pattern
   for fvarId in collectFVars {} (pattern.pattern.instantiateRev auxVars) |>.fvarIds do

src/Lean/Meta/Sym/Pattern.lean

@@ -64,7 +64,11 @@ def mkProofInstInfoMapFor (pattern : Expr) : MetaM (AssocList Name ProofInstInfo
 public structure Pattern where
   levelParams    : List Name
   varTypes       : Array Expr
-  isInstance     : Array Bool
+  /--
+  If `some argsInfo`, `argsInfo` stores whether the pattern variables are instances/proofs.
+  It is `none` if no pattern variables are instance/proof.
+  -/
+  varInfos?      : Option ProofInstInfo
   pattern        : Expr
   fnInfos        : AssocList Name ProofInstInfo
   /--
@@ -78,6 +82,16 @@ public structure Pattern where
 
 def uvarPrefix : Name := `_uvar
 
+/-- Returns `true` if the `i`th argument / pattern variable is an instance. -/
+def Pattern.isInstance (p : Pattern) (i : Nat) : Bool := Id.run do
+  let some varInfos := p.varInfos? | return false
+  varInfos.argsInfo[i]!.isInstance
+
+/-- Returns `true` if the `i`th argument / pattern variable is a proof. -/
+def Pattern.isProof (p : Pattern) (i : Nat) : Bool := Id.run do
+  let some varInfos := p.varInfos? | return false
+  varInfos.argsInfo[i]!.isProof
+
 def isUVar? (n : Name) : Option Nat := Id.run do
   let .num p idx := n | return none
   unless p == uvarPrefix do return none
@@ -144,12 +158,13 @@ where
       else
         mask
 
-def mkPatternCore (levelParams : List Name) (varTypes : Array Expr) (isInstance : Array Bool)
-    (pattern : Expr) : MetaM Pattern := do
+def mkPatternCore (type : Expr) (levelParams : List Name) (varTypes : Array Expr) (pattern : Expr) : MetaM Pattern := do
   let fnInfos ← mkProofInstInfoMapFor pattern
   let checkTypeMask := mkCheckTypeMask pattern varTypes.size
   let checkTypeMask? := if checkTypeMask.all (· == false) then none else some checkTypeMask
-  return { levelParams, varTypes, isInstance, pattern, fnInfos, checkTypeMask? }
+  let varInfos? ← forallBoundedTelescope type varTypes.size fun xs _ =>
+    mkProofInstArgInfo? xs
+  return { levelParams, varTypes, pattern, fnInfos, varInfos?, checkTypeMask? }
 
 /--
 Creates a `Pattern` from the type of a theorem.
@@ -168,12 +183,12 @@ public def mkPatternFromDecl (declName : Name) (num? : Option Nat := none) : Met
   let (levelParams, type) ← preprocessPattern declName
   let hugeNumber := 10000000
   let num := num?.getD hugeNumber
-  let rec go (i : Nat) (type : Expr) (varTypes : Array Expr) (isInstance : Array Bool) : MetaM Pattern := do
+  let rec go (i : Nat) (pattern : Expr) (varTypes : Array Expr) : MetaM Pattern := do
     if i < num then
-      if let .forallE _ d b _ := type then
-        return (← go (i+1) b (varTypes.push d) (isInstance.push (isClass? (← getEnv) d).isSome))
-    mkPatternCore levelParams varTypes isInstance type
-  go 0 type #[] #[]
+      if let .forallE _ d b _ := pattern then
+        return (← go (i+1) b (varTypes.push d))
+    mkPatternCore type levelParams varTypes pattern
+  go 0 type #[]
 
 /--
 Creates a `Pattern` from an equational theorem, using the left-hand side of the equation.
@@ -188,14 +203,14 @@ Throws an error if the theorem's conclusion is not an equality.
 -/
 public def mkEqPatternFromDecl (declName : Name) : MetaM (Pattern × Expr) := do
   let (levelParams, type) ← preprocessPattern declName
-  let rec go (type : Expr) (varTypes : Array Expr) (isInstance : Array Bool) : MetaM (Pattern × Expr) := do
-    if let .forallE _ d b _ := type then
-      return (← go b (varTypes.push d) (isInstance.push (isClass? (← getEnv) d).isSome))
+  let rec go (pattern : Expr) (varTypes : Array Expr) : MetaM (Pattern × Expr) := do
+    if let .forallE _ d b _ := pattern then
+      return (← go b (varTypes.push d))
     else
-      let_expr Eq _ lhs rhs := type | throwError "resulting type for `{.ofConstName declName}` is not an equality"
-      let pattern ← mkPatternCore levelParams varTypes isInstance lhs
+      let_expr Eq _ lhs rhs := pattern | throwError "resulting type for `{.ofConstName declName}` is not an equality"
+      let pattern ← mkPatternCore type levelParams varTypes lhs
       return (pattern, rhs)
-  go type #[] #[]
+  go type #[]
 
 structure UnifyM.Context where
   pattern   : Pattern
@@ -799,7 +814,6 @@ def mkPreResult : UnifyM MkPreResultResult := do
     | none => mkFreshLevelMVar
   let pattern := (← read).pattern
   let varTypes := pattern.varTypes
-  let isInstance := pattern.isInstance
   let eAssignment := (← get).eAssignment
   let tPending := (← get).tPending
   let mut args := #[]
@@ -820,7 +834,7 @@ def mkPreResult : UnifyM MkPreResultResult := do
       let type := varTypes[i]!
       let type ← instantiateLevelParamsS type pattern.levelParams us
       let type ← instantiateRevBetaS type args
-      if isInstance[i]! then
+      if pattern.isInstance i then
         if let .some val ← trySynthInstance type then
           args := args.push (← shareCommon val)
           continue

src/Lean/Meta/Sym/ProofInstInfo.lean

@@ -19,6 +19,26 @@ public def preprocessType (type : Expr) : MetaM Expr := do
   let type ← Core.betaReduce type
   zetaReduce type
 
+/--
+Analyzes whether the given free variables (aka arguments) are proofs or instances.
+Returns `none` if no arguments are proofs or instances.
+-/
+public def mkProofInstArgInfo? (xs : Array Expr) : MetaM (Option ProofInstInfo) := do
+  let env ← getEnv
+  let mut argsInfo := #[]
+  let mut found := false
+  for x in xs do
+    let type ← Meta.inferType x
+    let isInstance := isClass? env type |>.isSome
+    let isProof ← isProp type
+    if isInstance || isProof then
+      found := true
+    argsInfo := argsInfo.push { isInstance, isProof }
+  if found then
+    return some { argsInfo }
+  else
+    return none
+
 /--
 Analyzes the type signature of `declName` and returns information about which arguments
 are proofs or instances. Returns `none` if no arguments are proofs or instances.
@@ -26,21 +46,7 @@ are proofs or instances. Returns `none` if no arguments are proofs or instances.
 public def mkProofInstInfo? (declName : Name) : MetaM (Option ProofInstInfo) := do
   let info ← getConstInfo declName
   let type ← preprocessType info.type
-  forallTelescopeReducing type fun xs _ => do
-    let env ← getEnv
-    let mut argsInfo := #[]
-    let mut found := false
-    for x in xs do
-      let type ← Meta.inferType x
-      let isInstance := isClass? env type |>.isSome
-      let isProof ← isProp type
-      if isInstance || isProof then
-        found := true
-      argsInfo := argsInfo.push { isInstance, isProof }
-    if found then
-      return some { argsInfo }
-    else
-      return none
+  forallTelescopeReducing type fun xs _ => mkProofInstArgInfo? xs
 
 /--
 Returns information about the type signature of `declName`. It contains information about which arguments

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

@@ -11,6 +11,7 @@ public import Lean.Meta.Sym.Simp.Theorems
 public import Lean.Meta.Sym.Simp.App
 public import Lean.Meta.Sym.Simp.Discharger
 import Lean.Meta.Sym.InstantiateS
+import Lean.Meta.Sym.InstantiateMVarsS
 import Lean.Meta.Sym.Simp.DiscrTree
 namespace Lean.Meta.Sym.Simp
 open Grind
@@ -20,31 +21,48 @@ Creates proof term for a rewriting step.
 Handles both constant expressions (common case, avoids `instantiateLevelParams`)
 and general expressions.
 -/
-def mkValue (expr : Expr) (pattern : Pattern) (result : MatchUnifyResult) : Expr :=
+def mkValue (expr : Expr) (pattern : Pattern) (us : List Level) (args : Array Expr) : Expr :=
   if let .const declName [] := expr then
-    mkAppN (mkConst declName result.us) result.args
+    mkAppN (mkConst declName us) args
   else
-    mkAppN (expr.instantiateLevelParams pattern.levelParams result.us) result.args
+    mkAppN (expr.instantiateLevelParams pattern.levelParams us) args
 
 /--
 Tries to rewrite `e` using the given theorem.
 -/
-public def Theorem.rewrite (thm : Theorem) (e : Expr) (d : Discharger := dischargeNone) : SimpM Result := do
+public def Theorem.rewrite (thm : Theorem) (e : Expr) (d : Discharger := dischargeNone) : SimpM Result :=
+  /-
+  **Note**: We use `withNewMCtxDepth` to ensure auxiliary metavariables used during the `match?`
+  do not pollute the metavariable context.
+  Thus, we must ensure that all assigned variables have be instantiate.
+  -/
+  withNewMCtxDepth do
   if let some result ← thm.pattern.match? e then
     -- **Note**: Potential optimization: check whether pattern covers all variables.
-    for arg in result.args do
-      let .mvar mvarId := arg | pure ()
-      unless (← mvarId.isAssigned) do
-        let decl ← mvarId.getDecl
-        if let some val ← d decl.type then
-          mvarId.assign val
+    let mut args := result.args.toVector
+    let us ← result.us.mapM instantiateLevelMVars
+    for h : i in *...args.size do
+      let arg := args[i]
+      if let .mvar mvarId := arg then
+        if (← mvarId.isAssigned) then
+          let arg ← instantiateMVarsS arg
+          args := args.set i arg
         else
-          -- **Note**: Failed to discharge hypothesis.
-          return .rfl
-    let proof := mkValue thm.expr thm.pattern result
-    let rhs   := thm.rhs.instantiateLevelParams thm.pattern.levelParams result.us
-    let rhs   ← shareCommonInc rhs
-    let expr  ← instantiateRevBetaS rhs result.args
+          let decl ← mvarId.getDecl
+          if let some val ← d decl.type then
+            let val ← instantiateMVarsS val
+            mvarId.assign val
+            args := args.set i val
+          else
+            -- **Note**: Failed to discharge hypothesis.
+            return .rfl
+      else if arg.hasMVar then
+        let arg ← instantiateMVarsS arg
+        args := args.set i arg
+    let proof := mkValue thm.expr thm.pattern us args.toArray
+    let rhs   := thm.rhs.instantiateLevelParams thm.pattern.levelParams us
+    let rhs   ← share rhs
+    let expr  ← instantiateRevBetaS rhs args.toArray
     if isSameExpr e expr then
       return .rfl
     else

tests/bench/sym/add_sub_cancel.lean

@@ -307,5 +307,7 @@ def solveUsingSym (n : Nat) (check := true) : MetaM Unit := do
   driver n check fun mvarId => SymM.run do solve mvarId
 
 set_option maxRecDepth 100000
-#eval solveUsingSym 40
--- goal_100: 370.033833 ms, kernel: 432.021250 ms
+#eval solveUsingSym 80
+-- goal_40: 49.065042 ms, kernel: 35.214791 ms
+-- goal_80: 157.440000 ms, kernel: 101.177958 ms
+-- goal_100: 236.273125 ms, kernel: 158.136958 ms