feat: where ... finally section to assign leftover goals (#8723)

This PR implements a `finally` section following a (potentially empty)
`where` block. `where ... finally` opens a tactic sequence block in
which the goals are the unassigned metavariables from the definition
body and its auxiliary definitions that arise from use of `let rec` and
`where`.

This can be useful for discharging multiple proof obligations in the
definition body by a single invocation of a tactic such as `all_goals`:
```lean
example (i j : Nat) (xs : Array Nat) (hi : i < xs.size) (hj: j < xs.size) :=
  match i with
  | 0 => x
  | _ => xs[i]'?_ + xs[j]'?_
where x := 13
finally all_goals assumption
```

---------

Co-authored-by: Sebastian Graf <sg@lean-fro.org>

src/Lean/Elab/Binders.lean

@@ -468,7 +468,8 @@ def elabFunBinders (binders : Array Syntax) (expectedType? : Option Expr) (x : A
 
 def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax :=
   match whereDecls with
-  | `(whereDecls|where $[$decls:letRecDecl];*) => `(let rec $decls:letRecDecl,*; $body)
+  | `(whereDecls|where $[$_:whereFinally]?) => `($body)
+  | `(whereDecls|where $[$decls:letRecDecl];* $[$_:whereFinally]?) => `(let rec $decls:letRecDecl,*; $body)
   | _ => Macro.throwUnsupported
 
 def expandWhereDeclsOpt (whereDeclsOpt : Syntax) (body : Syntax) : MacroM Syntax :=

src/Lean/Elab/LetRec.lean

@@ -9,6 +9,7 @@ import Lean.Elab.Binders
 import Lean.Elab.DeclModifiers
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.DeclarationRange
+import Lean.Elab.MutualDef
 
 namespace Lean.Elab.Term
 open Meta
@@ -18,6 +19,7 @@ structure LetRecDeclView where
   attrs         : Array Attribute
   shortDeclName : Name
   declName      : Name
+  parentName?   : Option Name
   binderIds     : Array Syntax
   type          : Expr
   mvar          : Expr -- auxiliary metavariable used to lift the 'let rec'
@@ -43,8 +45,8 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
       unless declId.isIdent do
         throwErrorAt declId "'let rec' expressions must be named"
       let shortDeclName := declId.getId
-      let currDeclName? ← getDeclName?
-      let declName := currDeclName?.getD Name.anonymous ++ shortDeclName
+      let parentName? ← getDeclName?
+      let declName := parentName?.getD Name.anonymous ++ shortDeclName
       if decls.any fun decl => decl.declName == declName then
         withRef declId do
           throwError "'{declName}' has already been declared"
@@ -67,7 +69,7 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
         liftMacroM <| expandMatchAltsIntoMatch decl decl[3]
       let termination ← elabTerminationHints ⟨attrDeclStx[3]⟩
       decls := decls.push {
-        ref := declId, attrs, shortDeclName, declName,
+        ref := declId, attrs, shortDeclName, declName, parentName?,
         binderIds, type, mvar, valStx, termination
       }
     else
@@ -94,8 +96,8 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) :=
           (mkInfo := (pure <| .inl <| mkBodyInfo view.valStx ·))
           (mkInfoOnError := (pure <| mkBodyInfo view.valStx none))
           do
-             let value ← elabTermEnsuringType view.valStx type
-             mkLambdaFVars xs value
+            let value ← elabTermEnsuringType view.valStx type
+            mkLambdaFVars xs value
 
 private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array Expr) (values : Array Expr) : TermElabM Unit := do
   let letRecsToLiftCurr := (← get).letRecsToLift
@@ -115,13 +117,14 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
       attrs          := view.attrs
       shortDeclName  := view.shortDeclName
       declName       := view.declName
+      parentName?    := view.parentName?
       lctx
       localInstances
       type           := view.type
       val            := value
       mvarId         := view.mvar.mvarId!
-      termination    := termination
-      : LetRecToLift }
+      termination
+    }
   modify fun s => { s with letRecsToLift := toLift.toList ++ s.letRecsToLift }
 
 @[builtin_term_elab «letrec»] def elabLetRec : TermElab := fun stx expectedType? => do

src/Lean/Elab/MutualDef.lean

@@ -16,6 +16,7 @@ import Lean.Elab.Deriving.Basic
 import Lean.Elab.PreDefinition.Main
 import Lean.Elab.PreDefinition.TerminationHint
 import Lean.Elab.DeclarationRange
+import Lean.Elab.WhereFinally
 
 namespace Lean.Elab
 open Lean.Parser.Term
@@ -402,6 +403,17 @@ private def declValToTerminationHint (declVal : Syntax) : TermElabM TerminationH
   else
     return .none
 
+/-- Builds the view of a `where ... finally` section in a `declVal` syntax. -/
+private def declValToWhereFinally (declVal : Syntax) : TermElabM WhereFinallyView := withRef declVal do
+  if declVal.isOfKind ``Parser.Command.declValSimple then
+    mkWhereFinallyView ⟨declVal[3][0]⟩
+  else if declVal.isOfKind ``Parser.Command.declValEqns then
+    mkWhereFinallyView ⟨declVal[0][2][0]⟩
+  else if declVal.isOfKind ``Parser.Command.whereStructInst then
+    mkWhereFinallyView ⟨declVal[2][0]⟩
+  else
+    return .none
+
 /--
 Runs `k` with a restricted local context where only section variables from `vars` are included that
 * are directly referenced in any `headers`,
@@ -608,6 +620,39 @@ private def checkLetRecsToLiftTypes (funVars : Array Expr) (letRecsToLift : List
       let fnName ← getFunName fvarId letRecsToLift
       throwErrorAt toLift.ref "invalid type in 'let rec', it uses '{fnName}' which is being defined simultaneously"
 
+private structure ExprWithHoles where
+  ref : Syntax
+  expr : Expr
+
+private def ExprWithHoles.getHoles (e : ExprWithHoles) : TermElabM (Array MVarId) := withRef e.ref do
+  -- We do not want to see delayed assignments
+  let goals ← getMVarsNoDelayed e.expr
+  -- We only want synthetic opaque metavariables
+  let goals ← goals.filterM (MetavarKind.isSyntheticOpaque <$> ·.getKind)
+  -- Do not include metavariables generated by letrec lifting; these will be solved while lifting
+  let goals ← goals.filterM (not <$> isLetRecAuxMVar ·)
+  -- We want goals to appear in a deterministic order, so we sort by mvar index
+  let goals ← goals.mapM fun goal => return ((← goal.getDecl).index, goal)
+  return goals.insertionSort (·.fst < ·.fst) |>.map (·.snd)
+
+private def fillHolesFromWhereFinally (name : Name) (es : Array ExprWithHoles) (whereFinally : WhereFinallyView) : TermElabM PUnit := do
+  if whereFinally.isNone then return
+  let goals := (← es.mapM fun e => e.getHoles).flatten
+  Lean.Elab.Term.TermElabM.run' do
+  Term.withDeclName name do
+  withRef whereFinally.ref do
+    unless goals.isEmpty do
+      -- make info from `runTactic` available
+      goals.forM fun goal => pushInfoTree (.hole goal)
+      -- assign goals
+      let remainingGoals ← Tactic.run goals[0]! do
+        Tactic.setGoals goals.toList
+        Tactic.withTacticInfoContext whereFinally.ref do
+          Tactic.evalTactic whereFinally.tactic
+      -- complain if any goals remain
+      unless remainingGoals.isEmpty do
+        Term.reportUnsolvedGoals remainingGoals
+
 namespace MutualClosure
 
 /-- A mapping from FVarId to Set of FVarIds. -/
@@ -1196,11 +1241,28 @@ where
     let letRecsToLift ← getLetRecsToLift
     let letRecsToLift ← letRecsToLift.mapM instantiateMVarsAtLetRecToLift
     checkLetRecsToLiftTypes funFVars letRecsToLift
+    -- At this point, all metavariables except for letrec auxiliary variables and `?hole`s
+    -- introduced by the user should be assigned.
+    -- Hence we solve the remaining ones using `where ... finally`.
+    let exprsWithHoles := letRecsToLift.foldl (init := Std.HashMap.emptyWithCapacity headers.size) fun acc l =>
+      let ewh : ExprWithHoles := { ref := l.ref, expr := l.val }
+      if let some parentName := l.parentName? then
+        acc.alter parentName (fun | none => some #[ewh] | some ewhs => some (ewhs.push ewh))
+      else -- no parentName => no holes filled
+        acc
+    for header in headers, value in values do
+      let whereFinally ← declValToWhereFinally header.value
+      let exprsWithHoles := (exprsWithHoles.getD header.declName #[]).push { ref := header.ref, expr := value }
+      fillHolesFromWhereFinally header.declName exprsWithHoles whereFinally
     (if headers.all (·.kind.isTheorem) && !deprecated.oldSectionVars.get (← getOptions) then
        -- do not repeat checks already done in `elabFunValues`
        withHeaderSecVars (check := false) vars sc headers
      else withUsed vars headers values letRecsToLift) fun vars => do
       let preDefs ← MutualClosure.main vars headers funFVars values letRecsToLift
+      -- If there are any unassigned mvars left, they are errors. Check in `addPreDefinitions`.
+      -- Be aware that delayed assignments `?m := fun ... f => ?n ... f` in a let-recs `f` are even
+      -- ill-scoped after lifting `f` to a constant! Any attempt to interact with `?m` likely results
+      -- in `unknown free variable '...'` errors.
       checkAllDeclNamesDistinct preDefs
       for preDef in preDefs do
         trace[Elab.definition] "{preDef.declName} : {preDef.type} :=\n{preDef.value}"

src/Lean/Elab/Term.lean

@@ -15,6 +15,7 @@ import Lean.Elab.Level
 import Lean.Elab.DeclModifiers
 import Lean.Elab.PreDefinition.TerminationHint
 import Lean.Elab.DeclarationRange
+import Lean.Elab.WhereFinally
 import Lean.Language.Basic
 import Lean.Elab.InfoTree.InlayHints
 
@@ -139,6 +140,7 @@ structure LetRecToLift where
   attrs          : Array Attribute
   shortDeclName  : Name
   declName       : Name
+  parentName?    : Option Name
   lctx           : LocalContext
   localInstances : LocalInstances
   type           : Expr

src/Lean/Elab/WhereFinally.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2025 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf
+-/
+prelude
+import Lean.Parser.Term
+
+namespace Lean.Elab
+
+structure WhereFinallyView where
+  ref       : Syntax
+  tactic    : TSyntax ``Lean.Parser.Tactic.tacticSeq
+  deriving Inhabited
+
+def WhereFinallyView.none : WhereFinallyView := { ref := .missing, tactic := ⟨.missing⟩ }
+
+def WhereFinallyView.isNone (o : WhereFinallyView) : Bool := o.ref.isMissing && o.tactic.raw.isMissing
+
+/-- Creates a view of the `finally` section of a `whereDecls` syntax object -/
+def mkWhereFinallyView {m} [Monad m] [MonadError m] (stx : TSyntax ``Parser.Term.whereDecls) : m WhereFinallyView := do
+  -- Fail gracefully upon partial parses/missing where or finally sections
+  let whereFinally := stx.raw[2][0]
+  if whereFinally.isMissing then
+    return { ref := stx, tactic := ⟨.missing⟩ }
+  if !whereFinally[2][0].isMissing then
+    throwErrorAt stx "`where ... finally` does not currently support any named sub-sections `| sectionName => ...`"
+  let tactic := ⟨whereFinally[1]⟩
+  return { ref := whereFinally, tactic }

src/Lean/MetavarContext.lean

@@ -100,7 +100,7 @@ the requirements imposed by these modules.
      assigned by `isDefEq`.
 
   3. SyntheticOpaque metavariables are never assigned by `isDefEq`.
-     That is, the constraint `?n =?= Nat.succ Nat.zero` always fail
+     That is, the constraint `?n =?= Nat.succ Nat.zero` will always fail
      if `?n` is a syntheticOpaque metavariable. This kind of metavariable
      is created by tactics such as `intro`. Reason: in the tactic framework,
      subgoals as represented as metavariables, and a subgoal `?n` is considered

src/Lean/Parser/Term.lean

@@ -822,9 +822,22 @@ def «letrec» := leading_parser:leadPrec
   withPosition (group ("let " >> nonReservedSymbol "rec ") >> letRecDecls) >>
   optSemicolon termParser
 
+/--
+A named subsection of `where ... finally`. In the future, sections such as `decreasing_by` might become
+syntactic sugar for an `where ... finally` subsection `| decreasing => ...`.
+-/
+def whereFinallySubsection := leading_parser
+  ppLine >> "| " >> ident >> darrow >> Tactic.tacticSeq
+
+/--
+The `finally` section trailing a `where` opens a tactic block to fill in `?hole`s in the definition body.
+-/
+@[builtin_doc] def whereFinally := leading_parser
+  ppDedent ppLine >> "finally " >> optional Tactic.tacticSeqIndentGt >> manyIndent whereFinallySubsection
+
 @[run_builtin_parser_attribute_hooks]
 def whereDecls := leading_parser
-  ppDedent ppLine >> "where" >> sepBy1Indent (ppGroup letRecDecl) "; " (allowTrailingSep := true)
+  ppDedent ppLine >> "where" >> sepByIndent (ppGroup letRecDecl) "; " (allowTrailingSep := true) >> optional whereFinally
 
 @[run_builtin_parser_attribute_hooks]
 def matchAltsWhereDecls := leading_parser

tests/lean/run/whereFinally.lean

@@ -0,0 +1,115 @@
+example (i j : Nat) (xs : Array Nat) (hi : i < xs.size) (hj: j < xs.size) :=
+  match i with
+  | 0 => x
+  | _ => xs[i]'?_ + xs[j]'?_
+where x := 13
+finally all_goals assumption
+
+def hole_in_def_body (i : Nat) (xs : Array Nat) (h : i < xs.size) : Nat :=
+  xs[i]'?hole
+where finally
+  case hole => exact h
+
+def hole_in_def_match (i : Nat) (xs : Array Nat) (h : i < xs.size) : Bool → Nat
+  | true => xs[i]'?hole
+  | false => i
+where finally
+  case hole => exact h
+
+def hole_in_def_let_rhs (i : Nat) (xs : Array Nat) (h : i < xs.size) : Nat :=
+  let f (_ : Nat) := xs[i]'?hole
+  f i
+where finally
+  case hole => exact h
+
+def hole_in_rec_def_body (n : Nat) (xs : Array Nat) (h : n < xs.size) : Nat :=
+  match n with
+  | 0 => xs[0]'?hole
+  | n + 1 => hole_in_rec_def_body n xs (by omega)
+where finally
+  case hole => exact h
+
+def hole_in_rec_let_rhs (i : Nat) (xs : Array Nat) (h : i < xs.size) : Nat :=
+  let rec f (x : Nat) :=
+    if x = 0 then xs[i]'?hole else f (x-1)
+  f i
+  where finally
+    case hole => exact h
+
+theorem hole_in_thm_body (i : Nat) (xs : Array Nat) (h : i < xs.size) : True :=
+  let _x := xs[i]'?hole
+  True.intro
+where finally
+  case hole => exact h
+
+set_option pp.rawOnError true in
+def hole_in_def_match_where (i : Nat) (xs : Array Nat) (h : i < xs.size) :=
+  match i with
+  | 0 => x
+  | _ => xs[i]'?hole
+where x := 13
+finally case hole => assumption
+
+def hole_in_rec_let_rhs_match (i : Nat) (xs : Array Nat) (h : i < xs.size) : Nat :=
+  let rec f (x : Nat) :=
+    match x with
+    | 0 => xs[i]'?hole
+    | x + 1 => x
+  f i
+  where finally case hole => exact h
+
+def hole_in_rec_let_and_def (i : Nat) (xs : Array Nat) (h : i < xs.size) : Nat :=
+  let rec f (x : Nat) :=
+    match x with
+    | 0 => xs[i]'?hole
+    | x + 1 => x
+  f i + xs[i]'?hole₂
+where finally
+  case hole => exact h
+  case hole₂ => exact h
+
+namespace hole_in_mutual_def
+mutual
+  def even : Nat → Bool
+    | 0 => ?zeroEven
+    | n + 1 => odd n
+  where finally
+    case zeroEven => exact true
+  def odd : Nat → Bool
+    | 0 => ?zeroOdd
+    | n + 1 => even n
+  where finally
+    case zeroOdd => exact false
+end
+
+mutual
+  def even' (n : Nat) : Bool :=
+    let rec go : Nat → Bool
+      | 0 => ?zeroEven
+      | n + 1 => not (go n)
+    go n
+  where finally
+    case zeroEven => exact true
+  def odd' n := not (even' n)
+end
+end hole_in_mutual_def
+
+structure S where
+  a : Nat
+  b : Nat
+
+def hole_in_struct_def : S where
+  a := ?hole
+  b := ?hole₂
+where finally
+  all_goals exact 42
+
+/--
+error: `where ... finally` does not currently support any named sub-sections `| sectionName => ...`
+-/
+#guard_msgs in
+def hole_decreasing_does_not_exist (i : Nat) (xs : Array Nat) (h : i < xs.size) : Nat :=
+  xs[i]'?hole
+where finally
+  case hole => exact h
+| decreasing => skip