refactor: discharge handoff VCs against the lifted hypothesis

The solver gains a targeted assumption step: after reflexivity, it tries to close `pre ⊑ rhs` against the newest pure hypothesis in the local context, which is typically the precondition lifted just before the previous spec application. This is one defeq check against one hypothesis, not an assumption search. With it, the lift trigger returns to its simple form: lift a pure precondition whenever the spec rule has a post or epost VC, since those premises never see the goal's precondition. Chains of specs with concrete pre/postconditions close under plain mvcgen' at their previous cost, loop invariants need not restate pure facts, and goals whose RHS contains metavariables are skipped so the check cannot assign post abstractions.

Also renames repeatAndRfl to solveTrivialConjuncts.

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

Author: sgraf812

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

@@ -26,7 +26,7 @@ The `mvcgen'` tactic, split across the modules above.
 - `VCGen.RuleConstruction` — SymM rule constructors from spec/simp/split info.
 - `VCGen.Context` — `VCGenM`, its `Context`/`State`, the bundle of pre-built rules.
 - `VCGen.EPost` — exception-postcondition decomposition helpers.
-- `VCGen.Util` — generic VCGenM helpers (`introsHygienic`, `simpGoalTelescope`, `repeatAndRfl`).
+- `VCGen.Util` — generic VCGenM helpers (`introsHygienic`, `simpGoalTelescope`, `solveTrivialConjuncts`).
 - `VCGen.RuleCache` — VCGenM cache wrappers around the SymM rule constructors.
 - `VCGen.Entails` — entailment-shaped goal decomposition (Triple unfolding, state/precondition intro, EPost and lattice steps).
 - `VCGen.Solve` — the main `solve` step / `SolveResult`.

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

@@ -100,7 +100,7 @@ public structure VCGen.Context where
   /-- User-customizable simp methods used to pre-simplify hypotheses. -/
   hypSimpMethods : Option Sym.Simp.Methods := none
   /-- The `trivial` config option: when `true` (default), `Driver.emitVC` runs
-  `repeatAndRfl` to collapse trivial `And.intro` chains; when `false`, the goal is
+  `solveTrivialConjuncts` to collapse trivial `And.intro` chains; when `false`, the goal is
   emitted as-is. -/
   trivial : Bool := true
   /-- The `jp` config option: when `true`, `tryLetIntro` recognises `__do_jp` lets

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

@@ -93,11 +93,11 @@ public def emitVC (goal : Grind.Goal) : VCGenM Unit := do
       goal := { goal with mvarId }
   goal ← processHypotheses goal
   if goal.inconsistent then return
-  -- `trivial`: when false, skip `repeatAndRfl` (which collapses And-chains via rfl);
+  -- `trivial`: when false, skip `solveTrivialConjuncts` (which collapses And-chains via rfl);
   -- emit the goal as-is.
   let mvarId ←
     if (← read).trivial then
-      let some mvarId ← repeatAndRfl goal.mvarId | return
+      let some mvarId ← solveTrivialConjuncts goal.mvarId | return
       pure mvarId
     else
       pure goal.mvarId

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

@@ -378,13 +378,11 @@ private def mkSpecBackwardProof
   let mut postAbstract := postSpec.consumeMData
   let mut epostAbstract := epostSpec.consumeMData
   let mut specApplied := specProof
-  let progMVars ← getMVars prog
-  let mut premiseHasProg := false
+  let mut hasContinuationVC := false
 
   /- abstract concrete `post` if it is not already abstract -/
   unless postAbstract.isMVar do
-    unless premiseHasProg do
-      premiseHasProg := (← getMVars postSpec).any progMVars.contains
+    hasContinuationVC := true
     /- `α → Pred`: type of `post` -/
     let postTy ← Sym.inferType postSpec
     /- mvar `postAbstract` for new abstract `post` -/
@@ -423,8 +421,7 @@ private def mkSpecBackwardProof
         This proof DOES NOT have a `?epostImpl` premise -/
       specApplied ← mkAppM ``WPMonad.wp_econs_bot_le #[prog, postAbstract, epostAbstract, specApplied]
     else
-      unless premiseHasProg do
-        premiseHasProg := (← getMVars epostSpec).any progMVars.contains
+      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
@@ -453,7 +450,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, premiseHasProg)
+  return (← abstractMVars specApplied, hasContinuationVC)
 
 /--
 Try to build a backward rule from a single spec theorem in `⊑` form.
@@ -469,7 +466,7 @@ Given a spec `pre ⊑ wp prog post epost` where the lattice type is
 public def tryMkBackwardRuleFromSpec (specThm : SpecTheorem) (info : WPInfo)
     (stateArgNames : Array Name := #[]) : OptionT SymM (BackwardRule × Bool) := do
   -- Instantiate the spec theorem, creating metavars for all universally quantified params
-  let (xs, _bs, specProof, specType) ← specThm.instantiate
+  let (_xs, _bs, specProof, specType) ← specThm.instantiate
   let_expr PartialOrder.rel Pred' _cl' pre rhs := specType
     | throwError "target not a partial order ⊑ application {specType}"
   guard <| ← isDefEqGuarded info.Pred Pred'
@@ -484,20 +481,12 @@ 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, postVCHasProg) ← mkSpecBackwardProof pre prog postSpec epostSpec specProof info.EPred ss ssTypes stateArgNames
+  let (res, hasContinuationVC) ← mkSpecBackwardProof pre prog postSpec epostSpec specProof info.EPred ss ssTypes stateArgNames
   let rule ← mkBackwardRuleFromExpr res.expr res.paramNames.toList
-  -- The goal's precondition reaches exactly one premise: the precondition VC. Every other
-  -- premise that mentions parts of the program verifies program fragments without it. When
-  -- such a premise exists, the caller lifts a pure goal precondition into the local context
-  -- first, so its fact stays available everywhere.
-  let progMVars ← getMVars prog
-  let mut hypHasProg := false
-  for x in xs do
-    if x.isMVar && !hypHasProg then
-      let xTy ← Meta.inferType x
-      if ← Meta.isProp xTy then
-        hypHasProg := (← getMVars xTy).any progMVars.contains
-  return (rule, hypHasProg || postVCHasProg)
+  -- 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)
 
 /-! ## Equality spec rules
 

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

@@ -122,6 +122,39 @@ 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.
+
+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)) :=
+  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 proof? ← match_expr rhs with
+      | CompleteLattice.ofProp _l _inst φ => do
+        if ← isDefEqS φ hyp.type then
+          pure (some (← mkAppM ``Lean.Order.le_ofProp #[pre, φ, hyp.toExpr]))
+        else
+          pure none
+      | _ => do
+        if α.isProp then
+          if ← isDefEqS rhs hyp.type then
+            pure (some (← mkAppM ``Lean.Order.le_prop #[pre, rhs, hyp.toExpr]))
+          else
+            pure none
+        else
+          pure none
+    let some proof := proof? | return none
+    trace[Elab.Tactic.Do.vcgen] "Solved by lifted hypothesis {hyp.userName}"
+    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
@@ -281,20 +314,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. **State-argument introduction**: If the lattice carrier is a function type
+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
    `σ₁ → ... → σₙ → Base`, introduce all excess state arguments.
-6. **EPost projection reduction**: reduce an `EPost.Cons.head` RHS to the projected component.
-7. **Lattice decomposition**: decompose `⊓`, `⇨`, `⌜p⌝` and `⊤` RHS connectives.
-8. **WP decomposition**: when the RHS is `wp e post epost s₁ ... sₙ`, in order:
+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.
-9. **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 9, and inside steps 7/8
-right before a `⊓` or match split duplicates 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.
+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.
 -/
 public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := goal.withContext do
   if ← outOfFuel then return .stop
@@ -318,6 +354,7 @@ 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
 
   -- Phase 2: introduce excess state arguments and reduce EPost projections, so that the RHS
   -- exposes either a lattice connective or a `wp` application.

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

@@ -20,7 +20,7 @@ open Lean Meta Sym Lean.Order
 /-!
 Generic `VCGenM` helpers: checked backward-rule application, telescope-aware `simp` driver,
 hygienic binder introduction, hypothesis-internalization for grind, and the trivial-conjunct
-collapser `repeatAndRfl`. None of these know anything about the entailment shapes `solve`
+collapser `solveTrivialConjuncts`. None of these know anything about the entailment shapes `solve`
 decomposes.
 -/
 
@@ -132,7 +132,7 @@ exactly the conjuncts that could not be solved.
 This procedure may assign metavariables in `e₁`/`e₂`, for example for `e = ?m` it will assign
 `?m := e`.
 -/
-public partial def repeatAndRfl (goal : MVarId) : VCGenM (Option MVarId) :=
+public partial def solveTrivialConjuncts (goal : MVarId) : VCGenM (Option MVarId) :=
     goal.withContext do
   let ctx ← read
   let ty ← instantiateMVars (← goal.getType)
@@ -141,8 +141,8 @@ public partial def repeatAndRfl (goal : MVarId) : VCGenM (Option MVarId) :=
     return none
   else if ty.isAppOf ``And then
     let .goals [g₁, g₂] ← ctx.andIntroRule.applyChecked goal
-      | throwError "repeatAndRfl: failed to apply {.ofConstName ``And.intro} to{indentExpr ty}"
-    match ← repeatAndRfl g₁, ← repeatAndRfl g₂ with
+      | throwError "solveTrivialConjuncts: failed to apply {.ofConstName ``And.intro} to{indentExpr ty}"
+    match ← solveTrivialConjuncts g₁, ← solveTrivialConjuncts g₂ with
     | none,    none    => return none
     | some g,  none    => return some g
     | none,    some g  => return some g

src/Std/Internal/Do/Order/Basic.lean

@@ -267,6 +267,9 @@ theorem prop_le (x y : Prop) : (x → (⊤ : Prop) ⊑ y) → x ⊑ y :=
 theorem top_le_prop (x : Prop) : x → (⊤ : Prop) ⊑ x :=
   fun hx _ => hx
 
+theorem le_prop (x y : Prop) : y → x ⊑ y :=
+  fun hy _ => hy
+
 theorem of_top_le_prop {x : Prop} : (⊤ : Prop) ⊑ x → x :=
   fun h => h (le_top True trivial)