From b7dfda4f45889b0a57592a628d6a07414182e26f Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Thu, 24 Jul 2025 09:44:06 +0200 Subject: [PATCH] chore: Extract `collectFreshMVars` from `withCollectingNewGoalsFrom` (#9502) --- src/Lean/Elab/Tactic/Do/Spec.lean | 146 +++++++++++++---------------- src/Lean/Elab/Tactic/Do/VCGen.lean | 5 +- src/Lean/Elab/Tactic/ElabTerm.lean | 36 ++++--- 3 files changed, 90 insertions(+), 97 deletions(-) diff --git a/src/Lean/Elab/Tactic/Do/Spec.lean b/src/Lean/Elab/Tactic/Do/Spec.lean index 8ee186bb1c..03735a352d 100644 --- a/src/Lean/Elab/Tactic/Do/Spec.lean +++ b/src/Lean/Elab/Tactic/Do/Spec.lean @@ -136,104 +136,88 @@ def mkPreTag (goalTag : Name) : Name := Id.run do /-- Returns the proof and the list of new unassigned MVars. -/ -def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag : Name) (mkPreTag := mkPreTag) : n (Expr × List MVarId) := do - let mvarCounterSaved := (← liftMetaM getMCtx).mvarCounter +def mSpec (goal : MGoal) (elabSpecAtWP : Expr → n SpecTheorem) (goalTag : Name) (mkPreTag := mkPreTag) : n Expr := do -- First instantiate `fun s => ...` in the target via repeated `mintro ∀s`. - let (_, prf) ← mIntroForallN goal goal.target.consumeMData.getNumHeadLambdas fun goal => do - -- Elaborate the spec for the wp⟦e⟧ app in the target - let T := goal.target.consumeMData - unless T.getAppFn.constName! == ``PredTrans.apply do - liftMetaM (throwError "target not a PredTrans.apply application {indentExpr T}") - let wp := T.getArg! 2 - let specThm ← elabSpecAtWP wp + Prod.snd <$> mIntroForallN goal goal.target.consumeMData.getNumHeadLambdas fun goal => do + -- Elaborate the spec for the wp⟦e⟧ app in the target + let T := goal.target.consumeMData + unless T.getAppFn.constName! == ``PredTrans.apply do + liftMetaM (throwError "target not a PredTrans.apply application {indentExpr T}") + let wp := T.getArg! 2 + let specThm ← elabSpecAtWP wp - -- The precondition of `specThm` might look like `⌜?n = ‹Nat›ₛ ∧ ?m = ‹Bool›ₛ⌝`, which expands to - -- `SVal.curry (fun tuple => ?n = SVal.uncurry (getThe Nat tuple) ∧ ?m = SVal.uncurry (getThe Bool tuple))`. - -- Note that the assignments for `?n` and `?m` depend on the bound variable `tuple`. - -- Here, we further eta expand and simplify according to `etaPotential` so that the solutions for - -- `?n` and `?m` do not depend on `tuple`. - let residualEta := specThm.etaPotential - (T.getAppNumArgs - 4) -- 4 arguments expected for PredTrans.apply - mIntroForallN goal residualEta fun goal => do + -- The precondition of `specThm` might look like `⌜?n = ‹Nat›ₛ ∧ ?m = ‹Bool›ₛ⌝`, which expands to + -- `SVal.curry (fun tuple => ?n = SVal.uncurry (getThe Nat tuple) ∧ ?m = SVal.uncurry (getThe Bool tuple))`. + -- Note that the assignments for `?n` and `?m` depend on the bound variable `tuple`. + -- Here, we further eta expand and simplify according to `etaPotential` so that the solutions for + -- `?n` and `?m` do not depend on `tuple`. + let residualEta := specThm.etaPotential - (T.getAppNumArgs - 4) -- 4 arguments expected for PredTrans.apply + mIntroForallN goal residualEta fun goal => do - -- Compute a frame of `P` that we duplicate into the pure context using `Spec.frame` - -- For now, frame = `P` or nothing at all - mTryFrame goal fun goal => do + -- Compute a frame of `P` that we duplicate into the pure context using `Spec.frame` + -- For now, frame = `P` or nothing at all + mTryFrame goal fun goal => do - -- Fully instantiate the specThm without instantiating its MVars to `wp` yet - let (_, _, spec, specTy) ← specThm.proof.instantiate + -- Fully instantiate the specThm without instantiating its MVars to `wp` yet + let (_, _, spec, specTy) ← specThm.proof.instantiate - -- Apply the spec to the excess arguments of the `wp⟦e⟧ Q` application - let T := goal.target.consumeMData - let args := T.getAppArgs - let Q' := args[3]! - let excessArgs := (args.extract 4 args.size).reverse + -- Apply the spec to the excess arguments of the `wp⟦e⟧ Q` application + let T := goal.target.consumeMData + let args := T.getAppArgs + let Q' := args[3]! + let excessArgs := (args.extract 4 args.size).reverse - -- Actually instantiate the specThm using the expected type computed from `wp`. - let_expr f@Triple m ps instWP α prog P Q := specTy | do liftMetaM (throwError "target not a Triple application {specTy}") - let wp' := mkApp5 (mkConst ``WP.wp f.constLevels!) m ps instWP α prog - unless (← withAssignableSyntheticOpaque <| isDefEq wp wp') do - Term.throwTypeMismatchError none wp wp' spec + -- Actually instantiate the specThm using the expected type computed from `wp`. + let_expr f@Triple m ps instWP α prog P Q := specTy | do liftMetaM (throwError "target not a Triple application {specTy}") + let wp' := mkApp5 (mkConst ``WP.wp f.constLevels!) m ps instWP α prog + unless (← withAssignableSyntheticOpaque <| isDefEq wp wp') do + Term.throwTypeMismatchError none wp wp' spec - let P ← instantiateMVarsIfMVarApp P - let Q ← instantiateMVarsIfMVarApp Q + let P ← instantiateMVarsIfMVarApp P + let Q ← instantiateMVarsIfMVarApp Q - let P := P.betaRev excessArgs - let spec := spec.betaRev excessArgs - let u := goal.u + let P := P.betaRev excessArgs + let spec := spec.betaRev excessArgs + let u := goal.u - -- Often P or Q are schematic (i.e. an MVar app). Try to solve by rfl. - -- We do `fullApproxDefEq` here so that `constApprox` is active; this is useful in - -- `need_const_approx` of `doLogicTests.lean`. - let (HPRfl, QQ'Rfl) ← withAssignableSyntheticOpaque <| fullApproxDefEq <| do - return (← isDefEqGuarded P goal.hyps, ← isDefEqGuarded Q Q') + -- Often P or Q are schematic (i.e. an MVar app). Try to solve by rfl. + -- We do `fullApproxDefEq` here so that `constApprox` is active; this is useful in + -- `need_const_approx` of `doLogicTests.lean`. + let (HPRfl, QQ'Rfl) ← withAssignableSyntheticOpaque <| fullApproxDefEq <| do + return (← isDefEqGuarded P goal.hyps, ← isDefEqGuarded Q Q') - -- Discharge the validity proof for the spec if not rfl - let mut prePrf : Expr → Expr := id - if !HPRfl then - -- let P := (← reduceProjBeta? P).getD P - -- Try to avoid creating a longer name if the postcondition does not need to create a goal - let tag := if !QQ'Rfl then mkPreTag goalTag else goalTag - let HPPrf ← dischargeMGoal { goal with target := P } tag - prePrf := mkApp6 (mkConst ``SPred.entails.trans [u]) goal.σs goal.hyps P goal.target HPPrf + -- Discharge the validity proof for the spec if not rfl + let mut prePrf : Expr → Expr := id + if !HPRfl then + -- let P := (← reduceProjBeta? P).getD P + -- Try to avoid creating a longer name if the postcondition does not need to create a goal + let tag := if !QQ'Rfl then mkPreTag goalTag else goalTag + let HPPrf ← dischargeMGoal { goal with target := P } tag + prePrf := mkApp6 (mkConst ``SPred.entails.trans [u]) goal.σs goal.hyps P goal.target HPPrf - -- Discharge the entailment on postconditions if not rfl - let mut postPrf : Expr → Expr := id - if !QQ'Rfl then - -- Try to avoid creating a longer name if the precondition does not need to create a goal - let tag := if !HPRfl then goalTag ++ `post else goalTag - let wpApplyQ := mkApp4 (mkConst ``PredTrans.apply [u]) ps α wp Q -- wp⟦x⟧.apply Q; that is, T without excess args - let wpApplyQ' := mkApp4 (mkConst ``PredTrans.apply [u]) ps α wp Q' -- wp⟦x⟧.apply Q' - let QQ' ← dischargePostEntails α ps Q Q' tag - let QQ'mono := mkApp6 (mkConst ``PredTrans.mono [u]) ps α wp Q Q' QQ' - postPrf := fun h => - mkApp6 (mkConst ``SPred.entails.trans [u]) goal.σs P (wpApplyQ.betaRev excessArgs) (wpApplyQ'.betaRev excessArgs) - h (QQ'mono.betaRev excessArgs) + -- Discharge the entailment on postconditions if not rfl + let mut postPrf : Expr → Expr := id + if !QQ'Rfl then + -- Try to avoid creating a longer name if the precondition does not need to create a goal + let tag := if !HPRfl then goalTag ++ `post else goalTag + let wpApplyQ := mkApp4 (mkConst ``PredTrans.apply [u]) ps α wp Q -- wp⟦x⟧.apply Q; that is, T without excess args + let wpApplyQ' := mkApp4 (mkConst ``PredTrans.apply [u]) ps α wp Q' -- wp⟦x⟧.apply Q' + let QQ' ← dischargePostEntails α ps Q Q' tag + let QQ'mono := mkApp6 (mkConst ``PredTrans.mono [u]) ps α wp Q Q' QQ' + postPrf := fun h => + mkApp6 (mkConst ``SPred.entails.trans [u]) goal.σs P (wpApplyQ.betaRev excessArgs) (wpApplyQ'.betaRev excessArgs) + h (QQ'mono.betaRev excessArgs) - -- finally build the proof; HPPrf.trans (spec.trans QQ'mono) - let prf := prePrf (postPrf spec) - return ((), prf) - - -- (This is after closing the `mForallIntro` and `mTryFrame` blocks.) - -- Functions like `mkForallFVars` etc. might have instantiated some of the MVar holes and in - -- doing so have introduced new MVars in turn. - -- Thus we try and instantiate all MVars and collect the MVars of the instantiated expressions. - let holes ← getMVarsNoDelayed prf - /- Filter out all mvars that were created prior to `k`. -/ - let holes ← filterOldMVars holes mvarCounterSaved - let holes ← liftMetaM <| sortMVarIdsByIndex holes.toList - return (prf, holes) - -private def addMVar (mvars : IO.Ref (List MVarId)) (goal : Expr) (name : Name) : MetaM Expr := do - let m ← mkFreshExprSyntheticOpaqueMVar goal (tag := name) - mvars.modify (m.mvarId! :: ·) - return m + -- finally build the proof; HPPrf.trans (spec.trans QQ'mono) + let prf := prePrf (postPrf spec) + return ((), prf) @[builtin_tactic Lean.Parser.Tactic.mspecNoBind] def elabMSpecNoBind : Tactic | `(tactic| mspec_no_bind $[$spec]?) => do let (mvar, goal) ← mStartMVar (← getMainGoal) mvar.withContext do - let (prf, goals) ← mSpec goal (elabSpec spec) (← getMainTag) + let (prf, goals) ← collectFreshMVars <| mSpec goal (elabSpec spec) (← getMainTag) mvar.assign prf - replaceMainGoal goals + replaceMainGoal goals.toList | _ => throwUnsupportedSyntax diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean index 65d7051028..0898fc8fcb 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen.lean +++ b/src/Lean/Elab/Tactic/Do/VCGen.lean @@ -352,8 +352,9 @@ where try let specThm ← findSpec ctx.specThms wp trace[Elab.Tactic.Do.vcgen] "Candidate spec for {f.constName!}: {specThm.proof}" - let (prf, specHoles) ← withDefault <| mSpec goal (fun _wp => return specThm) name - assignMVars specHoles + let (prf, specHoles) ← withDefault <| collectFreshMVars <| + mSpec goal (fun _wp => return specThm) name + assignMVars specHoles.toList return prf catch ex => trace[Elab.Tactic.Do.vcgen] "Failed to find spec. Trying simp. Reason: {ex.toMessageData}" diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index 2d8ae05810..1567beb8af 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -109,8 +109,26 @@ def sortMVarIdArrayByIndex [MonadMCtx m] [Monad m] (mvarIds : Array MVarId) : m else Name.quickLt mvarId₁.name mvarId₂.name -def sortMVarIdsByIndex [MonadMCtx m] [Monad m] (mvarIds : List MVarId) : m (List MVarId) := - return (← sortMVarIdArrayByIndex mvarIds.toArray).toList +def sortMVarIdsByIndex [MonadMCtx m] [Monad m] (mvarIds : Array MVarId) : m (Array MVarId) := + return (← sortMVarIdArrayByIndex mvarIds) + +/-- +Execute `k`, and collect any fresh metavariables created during the execution of `k`. +-/ +def collectFreshMVars [Monad m] [MonadLiftT MetaM m] (k : m Expr) : m (Expr × Array MVarId) := do + let mvarCounterSaved := (← liftMetaM getMCtx).mvarCounter + let val ← k + let newMVarIds ← getMVarsNoDelayed val + /- Filter out all mvars that were created prior to `k`. -/ + let newMVarIds ← filterOldMVars newMVarIds mvarCounterSaved + /- + We sort the new metavariable ids by index to ensure the new goals are ordered using the order the metavariables have been created. + See issue #1682. + Potential problem: if elaboration of subterms is delayed the order the new metavariables are created may not match the order they + appear in the `.lean` file. We should tell users to prefer tagged goals. + -/ + let newMVarIds ← liftMetaM <| sortMVarIdsByIndex newMVarIds + return (val, newMVarIds) /-- Execute `k`, and collect new "holes" in the resulting expression. @@ -148,25 +166,15 @@ def withCollectingNewGoalsFrom (k : TacticM Expr) (parentTag : Name) (tagSuffix go where go := do - let mvarCounterSaved := (← getMCtx).mvarCounter - let val ← k - let newMVarIds ← getMVarsNoDelayed val + let (val, newMVarIds) ← collectFreshMVars k /- ignore let-rec auxiliary variables, they are synthesized automatically later -/ let newMVarIds ← newMVarIds.filterM fun mvarId => return !(← Term.isLetRecAuxMVar mvarId) - /- Filter out all mvars that were created prior to `k`. -/ - let newMVarIds ← filterOldMVars newMVarIds mvarCounterSaved /- If `allowNaturalHoles := false`, all natural mvarIds must be assigned. Passing this guard ensures that `newMVarIds` does not contain unassigned natural mvars. -/ unless allowNaturalHoles do let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← mvarId.getKind).isNatural logUnassignedAndAbort naturalMVarIds - /- - We sort the new metavariable ids by index to ensure the new goals are ordered using the order the metavariables have been created. - See issue #1682. - Potential problem: if elaboration of subterms is delayed the order the new metavariables are created may not match the order they - appear in the `.lean` file. We should tell users to prefer tagged goals. - -/ - let newMVarIds ← sortMVarIdsByIndex newMVarIds.toList + let newMVarIds := newMVarIds.toList tagUntaggedGoals parentTag tagSuffix newMVarIds return (val, newMVarIds)