fix: prune goals assigned by isDefEq in sym => mode

This PR fixes a bug in `sym =>` interactive mode where goals whose
metavariable was assigned by `isDefEq` (e.g. via `apply Eq.refl`) were
not pruned. `pruneSolvedGoals` previously only filtered out goals
flagged as inconsistent, so an already-assigned goal would linger as an
unsolved goal. It now also removes goals whose metavariable is already
assigned.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

.github/workflows/ci.yml

@@ -279,7 +279,8 @@ jobs:
                 "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
-                "check-stage3": level >= 2,
+                // Done as part of test-bench
+                //"check-stage3": level >= 2,
                 "test": true,
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
                 "test-bench": large && level >= 2,
@@ -291,7 +292,8 @@ jobs:
                 "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
-                "check-stage3": level >= 2,
+                // Done as part of test-bench
+                //"check-stage3": level >= 2,
                 "test": true,
                 "secondary": true,
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -68,7 +68,10 @@ def setGoals (goals : List Goal) : GrindTacticM Unit :=
 
 def pruneSolvedGoals : GrindTacticM Unit := do
   let gs ← getGoals
-  let gs := gs.filter fun g => !g.inconsistent
+  let gs ← gs.filterM fun g => do
+    if g.inconsistent then return false
+    -- The metavariable may have been assigned by `isDefEq`
+    return !(← g.mvarId.isAssigned)
   setGoals gs
 
 def getUnsolvedGoals : GrindTacticM (List Goal) := do
@@ -329,13 +332,19 @@ def liftGoalM (k : GoalM α) : GrindTacticM α := do
   replaceMainGoal [goal]
   return a
 
-def liftAction (a : Action) : GrindTacticM Unit := do
+inductive LiftActionCoreResult where
+  | closed | subgoals
+
+def liftActionCore (a : Action) : GrindTacticM LiftActionCoreResult := do
   let goal ← getMainGoal
   let ka := fun _ => throwError "tactic is not applicable"
   let kp := fun goal => return .stuck [goal]
   match (← liftGrindM <| a goal ka kp) with
-  | .closed _ => replaceMainGoal []
-  | .stuck gs => replaceMainGoal gs
+  | .closed _ => replaceMainGoal []; return .closed
+  | .stuck gs => replaceMainGoal gs; return .subgoals
+
+def liftAction (a : Action) : GrindTacticM Unit := do
+  discard <| liftActionCore a
 
 def done : GrindTacticM Unit := do
   pruneSolvedGoals

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -111,7 +111,9 @@ def evalCheck (tacticName : Name) (k : GoalM Bool)
      This matches the behavior of these tactics in default tactic mode
      where `lia` can close `x > 1 → x + y + z > 0` directly. -/
   if (← read).sym then
-    liftAction <| Action.intros 0 >> Action.assertAll
+    match (← liftActionCore <| Action.intros 0 >> Action.assertAll) with
+    | .closed   => return () -- closed the goal
+    | .subgoals => pure () -- continue
   let recover := (← read).recover
   liftGoalM do
     let progress ← k

tests/bench/build/run_bench.sh

@@ -23,6 +23,8 @@ echo ">"
 echo "> Building $STAGE_NEXT..."
 echo ">"
 
+make -C "$BUILD_NEXT" clean-stdlib
+
 LAKE_OVERRIDE_LEAN=true LEAN="$(realpath fake_root/bin/lean)" \
 WRAPPER_PREFIX="$(realpath fake_root)" WRAPPER_OUT="$OUT" \
   lakeprof record -- \

tests/bench/sym/simp_1.lean

@@ -10,7 +10,9 @@ namespace SimpBench
 def getProofSize (r : Sym.Simp.Result) : MetaM Nat :=
   match r with
   | .rfl _ _ => return 0
-  | .step _ p _ _ => p.numObjs
+  | .step _ p _ _ =>
+    let p := ShareCommon.shareCommon' p
+    p.numObjs
 
 def checkWithKernel (r : Sym.Simp.Result) : MetaM Float := do
   match r with

tests/elab/sym_interactive_bugs.lean

@@ -0,0 +1,21 @@
+
+example (p q : Prop) : p → q → p ∧ q := by
+  sym =>
+    intro hp hq
+    apply And.intro
+    apply hp
+    apply hq
+
+register_sym_simp chainSimp where
+  post := ground >> rewrite [Nat.add_zero, Nat.zero_add]
+
+example (x y : Nat) (h : x ≤ y) : (1 - 1) + x  ≤ y + (1 + 0) := by
+  sym =>
+    simp chainSimp
+    -- In the following tactic the goal is closed while preprocessing the target
+    lia
+
+example : ∃ x, x = a := by
+  sym =>
+    apply Exists.intro
+    apply Eq.refl

tests/elab/sym_simp_3.lean

@@ -5,7 +5,7 @@ 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.simpControl
-    post := Sym.Simp.evalGround.andThen rewrite
+    post := Sym.Simp.evalGround >> rewrite
   }
   liftMetaTactic1 fun mvarId => Sym.SymM.run do
     let mvarId ← Sym.preprocessMVar mvarId