refactor: lift pure preconditions as soon as they arise

The solver lifts a pure precondition unconditionally when it sees one, as in #13978: an embedded `⌜φ⌝` before state-argument introduction, a bare proposition on the `Prop` lattice right after it. The lifted hypothesis is cached in `Scope.lastLiftedPre?`, and the targeted assumption step closes subsequent handoff VCs against it with a single defeq check, so no spec-rule sensitivity is needed; the rule construction returns to producing plain backward rules and the duplication guards before splits disappear.

Co-authored-by: volodeyka <vovaglad00@gmail.com>

Author: sgraf812

src/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean

@@ -136,19 +136,20 @@ public structure VCGen.Scope where
   specs : SpecTheorems
   /-- `__do_jp` fvars currently in scope. -/
   jps : FVarIdMap JumpSiteInfo := {}
+  /-- The most recently lifted pure precondition. `tryLiftedHyp` closes handoff VCs against
+  it without walking the local context. -/
+  lastLiftedPre? : Option FVarId := none
   /-- Index of the next local declaration to consider for local specs. -/
   nextDeclIdx : Nat := 0
   deriving Inhabited
 
 public structure VCGen.State where
   /--
-  A cache mapping registered SpecThms to their backward rule to apply, paired with whether
-  the rule has a premise besides the precondition VC that mentions parts of the program (in
-  which case the caller lifts a pure goal precondition before applying the rule). The
-  particular rule depends on the theorem name, the `WPMonad` instance and the number of
+  A cache mapping registered SpecThms to their backward rule to apply.
+  The particular rule depends on the theorem name, the `WPMonad` instance and the number of
   excess state arguments that the weakest precondition target is applied to.
   -/
-  specBackwardRuleCache : Std.HashMap (Name × Expr × Nat) (BackwardRule × Bool) := {}
+  specBackwardRuleCache : Std.HashMap (Name × Expr × Nat) BackwardRule := {}
   /--
   A cache mapping matchers to their splitting backward rule to apply.
   The particular rule depends on the matcher name, the monad and the number of excess state

src/Lean/Elab/Tactic/Do/Internal/VCGen/Entails.lean

@@ -42,13 +42,17 @@ public def introStateArgs (preIsTop : Bool) (goal : MVarId) : VCGenM MVarId := d
   introsExcessArgs rule goal
 
 /-- Introduce a pure precondition into the local context, leaving `⊤` as the residual
-precondition. `ofProp` selects the embedded form `⌜p⌝ ⊑ rhs` over the bare `Prop` form. -/
-public def introPre (ofProp : Bool) (goal : MVarId) : VCGenM MVarId := do
+precondition. `ofProp` selects the embedded form `⌜p⌝ ⊑ rhs` over the bare `Prop` form.
+Returns the new goal and the introduced hypothesis. -/
+public def introPre (ofProp : Bool) (goal : MVarId) : VCGenM (MVarId × FVarId) := do
   let rules := (← read).introRules
   let rule := if ofProp then rules.ofPropPreIntro else rules.propPreIntro
   let .goals [goal] ← rule.applyChecked goal
     | throwError "Failed to apply precondition intro rule to {goal}"
-  introsHygienic goal
+  let goal ← introsHygienic goal
+  let some decl := (← goal.withContext getLCtx).lastDecl
+    | throwError "Failed to intro the lifted precondition of {goal}"
+  return (goal, decl.fvarId)
 
 /--
 Reduce an `EPost.Cons.head` projection on the RHS of `pre ⊑ rhs` to the underlying component:

src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleCache.lean

@@ -35,13 +35,13 @@ specs must check that their equation type is definitionally equal to `m α`.
 Cache key: `(proof key, instWP, excessArgs.size)`.
 -/
 public def mkBackwardRuleFromSpecCached (specThm : SpecTheorem) (info : WPInfo) :
-    OptionT VCGenM (BackwardRule × Bool) := do
+    OptionT VCGenM BackwardRule := do
   let key := (specThm.proof.key, info.instWP, info.excessArgs.size)
   let s := (← get).specBackwardRuleCache
   if let some rule := s[key]? then return rule
   let some rule ← withNewMCtxDepth <| match specThm.kind with
       | .triple => tryMkBackwardRuleFromSpec specThm info |>.run
-      | .simp _ => ((·, false)) <$> tryMkBackwardRuleFromSimp specThm info |>.run
+      | .simp _ => tryMkBackwardRuleFromSimp specThm info |>.run
     | failure
   modify fun st => { st with specBackwardRuleCache := st.specBackwardRuleCache.insert key rule }
   return rule

src/Lean/Elab/Tactic/Do/Internal/VCGen/RuleConstruction.lean

@@ -368,7 +368,7 @@ prf : ∀ (pre : Prop) (α : Type) (x : StateT Nat Id α) (β : Type)
 -/
 private def mkSpecBackwardProof
     (pre prog postSpec epostSpec specProof EPred : Expr) (ss ssTypes : Array Expr)
-    (stateArgNames : Array Name := #[]) : SymM (AbstractMVarsResult × Bool) := do
+    (stateArgNames : Array Name := #[]) : SymM AbstractMVarsResult := do
   /- we start with `pre ⊑ wp prog post epost` where
   1. `pre` represents the Lean expression for `pre`
   2. `prog`, `postSpec`, and `epostSpec` are the selected arguments of the spec's `wp` RHS
@@ -378,11 +378,9 @@ private def mkSpecBackwardProof
   let mut postAbstract := postSpec.consumeMData
   let mut epostAbstract := epostSpec.consumeMData
   let mut specApplied := specProof
-  let mut hasContinuationVC := false
 
   /- abstract concrete `post` if it is not already abstract -/
   unless postAbstract.isMVar do
-    hasContinuationVC := true
     /- `α → Pred`: type of `post` -/
     let postTy ← Sym.inferType postSpec
     /- mvar `postAbstract` for new abstract `post` -/
@@ -421,7 +419,6 @@ private def mkSpecBackwardProof
         This proof DOES NOT have a `?epostImpl` premise -/
       specApplied ← mkAppM ``WPMonad.wp_econs_bot_le #[prog, postAbstract, epostAbstract, specApplied]
     else
-      hasContinuationVC := true
       /- Decompose `epostSpec ⊑ epostAbstract` into per-component proofs
         using `EPost.Cons.mk_le` and `EPost.Nil.le` -/
       let hepost ← decomposeEPostRel EPred epostSpec epostAbstract stateArgNames
@@ -450,7 +447,7 @@ private def mkSpecBackwardProof
   /- use `PartialOrder.rel_trans` to compose the abstracted `pre` and the proof of the original theorem -/
   specApplied ← mkAppM ``PartialOrder.rel_trans #[specAbstract, specApplied]
 
-  return (← abstractMVars specApplied, hasContinuationVC)
+  abstractMVars specApplied
 
 /--
 Try to build a backward rule from a single spec theorem in `⊑` form.
@@ -464,7 +461,7 @@ Given a spec `pre ⊑ wp prog post epost` where the lattice type is
   `info.Pred = σ1 → ... → σn → Prop`
 -/
 public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPInfo)
-    (stateArgNames : Array Name := #[]) : OptionT SymM (BackwardRule × Bool) := do
+    (stateArgNames : Array Name := #[]) : OptionT SymM BackwardRule := do
   -- Instantiate the spec theorem, creating metavars for all universally quantified params
   let (_xs, _bs, specProof, specType) ← specThm.instantiate
   let_expr PartialOrder.rel Pred' _cl' pre rhs := specType
@@ -481,12 +478,8 @@ public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPInfo)
     let ty ← Sym.inferType info.excessArgs[i]
     ssTypes := ssTypes.push ty
     ss := ss.push <| ← mkFreshExprMVar (userName := stateArgNames[i]?.getD `s) ty
-  let (res, hasContinuationVC) ← mkSpecBackwardProof pre prog postSpec epostSpec specProof info.EPred ss ssTypes stateArgNames
-  let rule ← mkBackwardRuleFromExpr res.expr res.paramNames.toList
-  -- The post and epost VCs never see the goal's precondition. When the rule has one, the
-  -- caller lifts a pure goal precondition into the local context first; `tryLiftedHyp`
-  -- closes the resulting handoff VCs against the lifted hypothesis.
-  return (rule, hasContinuationVC)
+  let res ← mkSpecBackwardProof pre prog postSpec epostSpec specProof info.EPred ss ssTypes stateArgNames
+  mkBackwardRuleFromExpr res.expr res.paramNames.toList
 
 /-! ## Equality spec rules
 

src/Lean/Elab/Tactic/Do/Internal/VCGen/Solve.lean

@@ -122,20 +122,18 @@ private def tryRfl (goal : MVarId) (target pre rhs : Expr) : VCGenM (Option (Lis
   goal.assign (mkApp3 refl relArgs[0]! relArgs[1]! pre)
   return some []
 
-/-- Strategy 5: close `pre ⊑ rhs` against the newest pure hypothesis in the local context,
-which is typically the precondition lifted just before the current spec rule was applied.
-This is one defeq check against one hypothesis, not an assumption search.
+/-- Strategy 5: close `pre ⊑ rhs` against the most recently lifted pure precondition,
+cached in `Scope.lastLiftedPre?`. This is one defeq check against one hypothesis, not an
+assumption search.
 
 Goals whose RHS contains metavariables are skipped: the defeq check could otherwise assign
 a post abstraction from an unrelated hypothesis. -/
-private def tryLiftedHyp (goal : MVarId) (α pre rhs : Expr) : VCGenM (Option (List MVarId)) :=
+private def tryLiftedHyp (scope : VCGen.Scope) (goal : MVarId) (α pre rhs : Expr) :
+    VCGenM (Option (List MVarId)) :=
   goal.withContext do
     if rhs.hasExprMVar then return none
-    let some hyp ← (← getLCtx).findDeclRevM? (fun decl => do
-        if decl.isImplementationDetail then return none
-        else if ← Meta.isProp decl.type then return some decl
-        else return none)
-      | return none
+    let some fvarId := scope.lastLiftedPre? | return none
+    let some hyp := (← getLCtx).find? fvarId | return none
     let proof? ← match_expr rhs with
       | CompleteLattice.ofProp _l _inst φ => do
         if ← isDefEqS φ hyp.type then
@@ -155,25 +153,17 @@ private def tryLiftedHyp (goal : MVarId) (α pre rhs : Expr) : VCGenM (Option (L
     goal.assign proof
     return some []
 
-/--
-Lift a non-trivial embedded pure precondition `⌜φ⌝` into the local context, leaving `⊤`
-as the residual precondition. Used before a decomposition step that would duplicate the
-precondition into several subgoals (a `⊓` or match split), and before applying a spec whose own
-precondition is `⊤` (whose precondition VC would otherwise discard the fact). Returns `none` when
-the precondition is not such a `⌜φ⌝`.
--/
-private def liftPurePre? (goal : MVarId) (pre : Expr) : VCGenM (Option MVarId) := do
+/-- Strategy 6: lift an embedded pure precondition `⌜φ⌝` into the local context, leaving `⊤`
+as the residual precondition. Runs before state-argument introduction, which would otherwise
+leave `⌜φ⌝` applied to the introduced arguments. Returns the new goal and the hypothesis. -/
+private def tryOfPropPreIntro (goal : MVarId) (pre : Expr) : VCGenM (Option (MVarId × FVarId)) := do
   let_expr CompleteLattice.ofProp _l _inst φ := pre | return none
   if φ.isTrue then return none
   return some (← introPre (ofProp := true) goal)
 
-/-- Strategy 6: decompose a supported lattice connective on the RHS, lifting a pure
-precondition first when the connective is `⊓` (which duplicates the precondition). -/
-private def tryLattice (goal : MVarId) (target pre rhs : Expr) (preIsTop : Bool) :
+/-- Strategy 8: decompose a supported lattice connective on the RHS. -/
+private def tryLattice (goal : MVarId) (target rhs : Expr) (preIsTop : Bool) :
     VCGenM (Option (List MVarId)) := do
-  if rhs.isAppOf ``meet then
-    if let some g ← liftPurePre? goal pre then
-      return some [g]
   solveLatticeConnective? goal target rhs preIsTop
 
 /-- Replace the program in `goal`'s target with `prog` (which must be definitionally equal). -/
@@ -213,16 +203,14 @@ private def tryWPLet (goal : MVarId) (target : Expr) (info : WPInfo) : VCGenM (O
   return some (← substOrHoistLet goal target info name type val body nondep
     info.prog.getAppRevArgs)
 
-/-- Strategy 7b: split an `ite`/`dite`/match program (or iota-reduce a matcher with a concrete
-discriminant), lifting a pure precondition first since the split duplicates it into the alts. -/
-private def tryWPMatch (goal : MVarId) (target pre : Expr) (info : WPInfo) :
+/-- Strategy 7b: split an `ite`/`dite`/match program, or iota-reduce a matcher with a concrete
+discriminant. -/
+private def tryWPMatch (goal : MVarId) (target : Expr) (info : WPInfo) :
     VCGenM (Option (List MVarId)) := do
   let some splitInfo ← liftMetaM <| Lean.Elab.Tactic.Do.getSplitInfo? info.prog | return none
   if splitInfo matches .matcher .. then
     if let some prog ← liftMetaM <| withReducible <| reduceRecMatcher? info.prog then
       return some [← replaceProgDefEq goal target info (← shareCommonInc prog)]
-  if let some g ← liftPurePre? goal pre then
-    return some [g]
   let rule ← mkBackwardRuleForSplitCached splitInfo info
   let .goals goals ← rule.applyChecked goal m!"split rule for{indentExpr info.prog}"
     | throwError "Failed to apply split rule for {indentExpr info.prog}"
@@ -255,19 +243,15 @@ private def tryWPHeadReduce (goal : MVarId) (target : Expr) (info : WPInfo) :
   return some (← replaceProgDefEq goal target info prog)
 
 /-- Strategy 7e: look up a registered `@[spec]` theorem (triple or simp) for the program head
-and apply its cached backward rule.
-
-When the rule has a premise besides the precondition VC that mentions parts of the program,
-a pure goal precondition is lifted into the local context first. Such premises never see the
-goal's precondition, so the lift is what keeps the fact available in them. -/
-private def applySpec (scope : VCGen.Scope) (goal : MVarId) (target pre α : Expr)
-    (preIsTop : Bool) (info : WPInfo) : VCGenM SolveResult := do
+and apply its cached backward rule. -/
+private def applySpec (scope : VCGen.Scope) (goal : MVarId) (target : Expr) (info : WPInfo) :
+    VCGenM SolveResult := do
   trace[Elab.Tactic.Do.vcgen] "Applying a spec for {info.prog}. Excess args: {info.excessArgs}"
   match ← SpecTheorems.findSpecs scope.specs info.prog with
   | .error thms => return .noSpecFoundForProgram info.prog info.m thms
   | .ok thm =>
   trace[Elab.Tactic.Do.vcgen] "Spec for {info.prog}: {thm.proof}"
-  let some (rule, needsPureLift) ←
+  let some rule ←
     try
       mkBackwardRuleFromSpecCached thm info |>.run
     catch ex =>
@@ -277,11 +261,6 @@ private def applySpec (scope : VCGen.Scope) (goal : MVarId) (target pre α : Exp
         Pred:{indentExpr info.Pred}\n\
         excessArgs: {info.excessArgs}"
     | return .noSpecFoundForProgram info.prog info.m #[thm]
-  if needsPureLift && !preIsTop then
-    if let some g ← liftPurePre? goal pre then
-      return .goals scope [g]
-    if α.isProp then
-      return .goals scope [← introPre (ofProp := false) goal]
   let .goals goals ← rule.applyChecked goal m!"spec rule for{indentExpr info.prog}"
     | do
       let ruleType ← Meta.inferType rule.expr
@@ -314,23 +293,23 @@ The function performs the following steps in order:
 2. **Target-let handling**: zeta-substitute duplicable top-level lets, otherwise introduce them.
 3. **Triple unfolding**: If the target is `⦃P⦄ x ⦃Q; E⦄`, unfold into `P ⊑ wp x Q E`.
 4. **Syntactic rfl**: close `pre ⊑ rhs` by `PartialOrder.rel_refl` when both sides unify.
-5. **Lifted-hypothesis discharge**: close `pre ⊑ rhs` with the newest pure hypothesis,
-   typically the precondition lifted before the previous spec application.
-6. **State-argument introduction**: If the lattice carrier is a function type
+5. **Lifted-hypothesis discharge**: close `pre ⊑ rhs` against the most recently lifted
+   precondition, cached in `Scope.lastLiftedPre?`.
+6. **Embedded pure precondition introduction**: lift a `⌜φ⌝` precondition into the local
+   context, before state-argument introduction would apply it to the introduced arguments.
+7. **State-argument introduction**: If the lattice carrier is a function type
    `σ₁ → ... → σₙ → Base`, introduce all excess state arguments.
-7. **EPost projection reduction**: reduce an `EPost.Cons.head` RHS to the projected component.
-8. **Lattice decomposition**: decompose `⊓`, `⇨`, `⌜p⌝` and `⊤` RHS connectives.
-9. **WP decomposition**: when the RHS is `wp e post epost s₁ ... sₙ`, in order:
-   hoist/zeta program-head lets, split `ite`/`dite`/match, zeta-unfold fvar program heads,
-   reduce projection heads, and finally apply a registered `@[spec]` theorem.
-10. **Pure precondition introduction** (last resort): introduce a bare pure precondition (on
-    the `Prop` lattice) so the residual VC has the form `⊤ ⊑ φ`.
-
-Pure preconditions are deliberately introduced *late* (step 10, and inside steps 8/9 right
-before a `⊓` or match split duplicates them, or before a spec rule with a post or epost VC
-loses them): introducing them eagerly would turn reflexivity-closable verification conditions
-such as `Q x ⊑ wp (pure x) Q E` into goals that need an assumption search. The lifted fact is
-handed back to the handoff VCs by step 5.
+8. **Bare pure precondition introduction**: on the `Prop` lattice, lift a non-`⊤`
+   precondition into the local context.
+9. **EPost projection reduction**: reduce an `EPost.Cons.head` RHS to the projected component.
+10. **Lattice decomposition**: decompose `⊓`, `⇨`, `⌜p⌝` and `⊤` RHS connectives.
+11. **WP decomposition**: when the RHS is `wp e post epost s₁ ... sₙ`, in order:
+    hoist/zeta program-head lets, split `ite`/`dite`/match, zeta-unfold fvar program heads,
+    reduce projection heads, and finally apply a registered `@[spec]` theorem.
+
+Pure preconditions are lifted as soon as they arise (steps 6 and 8). The lifted hypothesis is
+cached in `Scope.lastLiftedPre?`, and step 5 closes the handoff VCs of subsequent spec
+applications against it with a single defeq check.
 -/
 public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := goal.withContext do
   if ← outOfFuel then return .stop
@@ -354,19 +333,25 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
   let preIsTop := pre.isAppOf ``Lean.Order.top && pre.getAppNumArgs == 2
 
   if let some gs ← tryRfl goal target pre rhs then return .goals scope gs
-  if let some gs ← tryLiftedHyp goal α pre rhs then return .goals scope gs
+  if let some gs ← tryLiftedHyp scope goal α pre rhs then return .goals scope gs
 
-  -- Phase 2: introduce excess state arguments and reduce EPost projections, so that the RHS
-  -- exposes either a lattice connective or a `wp` application.
+  -- Phase 2: lift pure preconditions as they arise, introduce excess state arguments, and
+  -- reduce EPost projections, so that the RHS exposes a lattice connective or a `wp`
+  -- application over a `⊤` precondition.
+  if let some (g, h) ← tryOfPropPreIntro goal pre then
+    return .goals { scope with lastLiftedPre? := some h } [g]
   if α.isForall then return .goals scope [← introStateArgs preIsTop goal]
+  if !preIsTop && α.isProp then
+    let (g, h) ← introPre (ofProp := false) goal
+    return .goals { scope with lastLiftedPre? := some h } [g]
   if let some g ← reduceEPostHead? goal target α inst pre rhs then return .goals scope [g]
 
   -- Collect new local specs before any strategy that may emit multiple subgoals
   -- (`tryWPMatch`, `tryLattice`) or apply a registered spec (`applySpec`).
   let scope ← scope.collectLocalSpecs goal
 
   -- Phase 3: lattice connective decomposition.
-  if let some gs ← tryLattice goal target pre rhs preIsTop then return .goals scope gs
+  if let some gs ← tryLattice goal target rhs preIsTop then return .goals scope gs
 
   -- Phase 4: wp decomposition. The program-shape steps below all consume one unit of fuel
   -- (the `stepLimit` config option) when they make progress.
@@ -375,7 +360,7 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
     if let some g ← tryWPLet goal target info then
       VCGen.burnOne
       return .goals scope [g]
-    if let some gs ← tryWPMatch goal target pre info then
+    if let some gs ← tryWPMatch goal target info then
       VCGen.burnOne
       return .goals scope gs
     if let some g ← tryWPFVarZeta goal target info then
@@ -389,14 +374,9 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
     let f := info.prog.getAppFn
     if f.isConst || f.isFVar then
       VCGen.burnOne
-      return ← applySpec scope goal target pre α preIsTop info
+      return ← applySpec scope goal target info
     return .noStrategyForProgram info.prog
 
-  -- Phase 5 (last resort): introduce a bare pure precondition so the residual VC
-  -- has the form `⊤ ⊑ φ`.
-  if !preIsTop && α.isProp then
-    return .goals scope [← introPre (ofProp := false) goal]
-
   return .noProgramOrLatticeFoundInTarget rhs
 
 end VCGen