From cf527e05bdcbb1c0f98459cd7e18fb99cb3e4d86 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 20 Jun 2025 17:51:28 +0200 Subject: [PATCH] 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 --- src/Lean/Elab/Binders.lean | 3 +- src/Lean/Elab/LetRec.lean | 17 +++-- src/Lean/Elab/MutualDef.lean | 62 +++++++++++++++++ src/Lean/Elab/Term.lean | 2 + src/Lean/Elab/WhereFinally.lean | 29 ++++++++ src/Lean/MetavarContext.lean | 2 +- src/Lean/Parser/Term.lean | 15 +++- tests/lean/run/whereFinally.lean | 115 +++++++++++++++++++++++++++++++ 8 files changed, 235 insertions(+), 10 deletions(-) create mode 100644 src/Lean/Elab/WhereFinally.lean create mode 100644 tests/lean/run/whereFinally.lean diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index e8414abdde..46e4b43175 100644 --- a/src/Lean/Elab/Binders.lean +++ b/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 := diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean index 63dd0114a1..9f0b19a063 100644 --- a/src/Lean/Elab/LetRec.lean +++ b/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 diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 1919b60f10..9699dfe2c9 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/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}" diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 8e8b20c908..446ee9da0d 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/src/Lean/Elab/WhereFinally.lean b/src/Lean/Elab/WhereFinally.lean new file mode 100644 index 0000000000..4a18f151be --- /dev/null +++ b/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 } diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index a2f03ffc12..82a5db59e2 100644 --- a/src/Lean/MetavarContext.lean +++ b/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 diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index a85de6ccc7..69044c3c2b 100644 --- a/src/Lean/Parser/Term.lean +++ b/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 diff --git a/tests/lean/run/whereFinally.lean b/tests/lean/run/whereFinally.lean new file mode 100644 index 0000000000..7835adee8e --- /dev/null +++ b/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