chore: Extract collectFreshMVars from withCollectingNewGoalsFrom (#9502)
This commit is contained in:
Sebastian Graf
GitHub
parent
45514a955e
commit
b7dfda4f45
3 changed files with 90 additions and 97 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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}"
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue