fix: immediately replace main goal in SPred proof mode tactics (#10571)

This PR ensures that `SPred` proof mode tactics such as `mspec`,
`mintro`, etc. immediately replace the main goal when entering the proof
mode. This prevents `No goals to be solved` errors.

src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean

@@ -48,10 +48,13 @@ def mStartMVar (mvar : MVarId) : MetaM (MVarId × MGoal) := mvar.withContext do
   else
     return (mvar, result.goal)
 
-@[builtin_tactic Lean.Parser.Tactic.mstart]
-def elabMStart : Tactic | _ => do
-  let (mvar, _) ← mStartMVar (← getMainGoal)
+def mStartMainGoal : TacticM (MVarId × MGoal) := do
+  let (mvar, goal) ← mStartMVar (← getMainGoal)
   replaceMainGoal [mvar]
+  return (mvar, goal)
+
+@[builtin_tactic Lean.Parser.Tactic.mstart]
+def elabMStart : Tactic | _ => discard mStartMainGoal
 
 @[builtin_tactic Lean.Parser.Tactic.mstop]
 def elabMStop : Tactic | _ => do

src/Lean/Elab/Tactic/Do/ProofMode/Cases.lean

@@ -191,7 +191,7 @@ private theorem blah3 {σs} {P Q H T : SPred σs}
 def elabMCases : Tactic
   | `(tactic| mcases $hyp:ident with $pat:mcasesPat) => do
     let pat ← liftMacroM <| MCasesPat.parse pat
-    let (mvar, goal) ← mStartMVar (← getMainGoal)
+    let (mvar, goal) ← mStartMainGoal
     mvar.withContext do
 
     let focus ← goal.focusHypWithInfo hyp

src/Lean/Elab/Tactic/Do/ProofMode/Intro.lean

@@ -73,7 +73,7 @@ macro_rules
 @[builtin_tactic Lean.Parser.Tactic.mintro]
 def elabMIntro : Tactic
   | `(tactic| mintro $ident:binderIdent) => do
-    let (mvar, goal) ← mStartMVar (← getMainGoal)
+    let (mvar, goal) ← mStartMainGoal
     mvar.withContext do
     let goals ← IO.mkRef []
     mvar.assign (← mIntro goal ident fun newGoal => do
@@ -82,7 +82,7 @@ def elabMIntro : Tactic
       return m)
     replaceMainGoal (← goals.get)
   | `(tactic| mintro ∀$ident:binderIdent) => do
-    let (mvar, goal) ← mStartMVar (← getMainGoal)
+    let (mvar, goal) ← mStartMainGoal
     mvar.withContext do
     let goals ← IO.mkRef []
     mvar.assign (← mIntroForall goal ident fun newGoal => do

src/Lean/Elab/Tactic/Do/ProofMode/Refine.lean

@@ -70,7 +70,7 @@ partial def mRefineCore (goal : MGoal) (pat : MRefinePat) (k : MGoal → TSyntax
 def elabMRefine : Tactic
   | `(tactic| mrefine $pat:mrefinePat) => do
     let pat ← liftMacroM <| MRefinePat.parse pat
-    let (mvar, goal) ← mStartMVar (← getMainGoal)
+    let (mvar, goal) ← mStartMainGoal
     mvar.withContext do
 
     let goals ← IO.mkRef #[]

src/Lean/Elab/Tactic/Do/ProofMode/RenameI.lean

@@ -21,7 +21,7 @@ partial def mRenameI [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goa
 @[builtin_tactic Lean.Parser.Tactic.mrenameI]
 def elabMRenameI : Tactic
   | `(tactic| mrename_i $idents:binderIdent*) => do
-    let (mvar, goal) ← mStartMVar (← getMainGoal)
+    let (mvar, goal) ← mStartMainGoal
     mvar.withContext do
     let goals ← IO.mkRef []
     mvar.assign (← Prod.snd <$> mRenameI goal idents fun newGoal => do

src/Lean/Elab/Tactic/Do/ProofMode/Revert.lean

@@ -95,7 +95,7 @@ def elabMRevert : Tactic
     return m)
   replaceMainGoal (← goals.get)
   | `(tactic| mrevert ∀ $[$n]?) => do
-  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  let (mvar, goal) ← mStartMainGoal
   mvar.withContext do
   let n := ((·.getNat) <$> n).getD 1
   let goals ← IO.mkRef []

src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean

@@ -88,7 +88,7 @@ def mSpecializeForall (P : Expr) (Ψ : Expr) (arg : TSyntax `term) : OptionT Tac
 @[builtin_tactic Lean.Parser.Tactic.mspecialize]
 def elabMSpecialize : Tactic
   | `(tactic| mspecialize $hyp $args*) => do
-  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  let (mvar, goal) ← mStartMainGoal
   mvar.withContext do
 
   -- Want to prove goal P ⊢ T, where hyp occurs in P.
@@ -133,7 +133,7 @@ def elabMSpecialize : Tactic
 def elabMspecializePure : Tactic
   | `(tactic| mspecialize_pure $head $args* => $hyp) => do
   -- "mspecialize_pure" >> term >> many (ppSpace >> checkColGt "irrelevant" >> termParser (eval_prec max)) >> "as" >> ident
-  let (mvar, goal) ← mStartMVar (← getMainGoal)
+  let (mvar, goal) ← mStartMainGoal
   mvar.withContext do
 
   -- Want to prove goal P ⊢ₛ T. `head` is a pure proof of type `φ` that turns into `⊢ₛ H` via `start_entails`.

src/Lean/Elab/Tactic/Do/Spec.lean

@@ -214,9 +214,9 @@ def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag : Name
 @[builtin_tactic Lean.Parser.Tactic.mspecNoBind]
 def elabMSpecNoBind : Tactic
   | `(tactic| mspec_no_bind $[$spec]?) => do
-    let (mvar, goal) ← mStartMVar (← getMainGoal)
+    let (mvar, goal) ← mStartMainGoal
     mvar.withContext do
-    let (prf, goals) ← collectFreshMVars <| mSpec goal (elabSpec spec) (← getMainTag)
+    let (prf, goals) ← collectFreshMVars <| mSpec goal (elabSpec spec) (← mvar.getTag)
     mvar.assign prf
     replaceMainGoal goals.toList
   | _ => throwUnsupportedSyntax

tests/lean/run/doLogicTests.lean

@@ -292,6 +292,24 @@ theorem fib_correct {n} : (fib_impl n).run = fib_spec n := by
 
 end fib
 
+section regressions
+
+def mySum (l : Array Nat) : Nat := Id.run do
+  let mut out := 0
+  for i in l do
+    out := out + i
+  return out
+
+theorem mySum_correct (l : Array Nat) : mySum l = l.sum := by
+  generalize h : mySum l = x
+  apply Id.of_wp_run_eq h
+  -- This tests that `mspec` properly replaces the main goal.
+  -- Previously, we would get `No goals to be solved` here.
+  mspec
+  all_goals admit
+
+end regressions
+
 section WeNeedAProofMode
 
 abbrev M := StateT Nat (StateT Char (StateT Bool (StateT String Id)))