fix: lift pure preconditions only when a premise verifies program parts without them

The goal's precondition reaches exactly one premise of a constructed spec rule: the precondition VC. The solver now lifts a pure goal precondition only when some other premise mentions parts of the program, that is, when program verification continues somewhere the precondition cannot reach. This covers the loop specifications (their step and exit premises mention the loop body) and specs with hypotheses about program arguments, while chains of specs whose program occurs only in the precondition VC keep their reflexivity handoff. The PurePrecond benchmark closes under plain mvcgen' again at its previous cost.

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

Author: sgraf812

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

@@ -143,10 +143,10 @@ public structure VCGen.Scope where
 public structure VCGen.State where
   /--
   A cache mapping registered SpecThms to their backward rule to apply, paired with whether
-  the rule has a post or epost VC (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 excess state arguments that the weakest precondition target is
-  applied to.
+  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
+  excess state arguments that the weakest precondition target is applied to.
   -/
   specBackwardRuleCache : Std.HashMap (Name × Expr × Nat) (BackwardRule × Bool) := {}
   /--

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

@@ -378,11 +378,13 @@ private def mkSpecBackwardProof
   let mut postAbstract := postSpec.consumeMData
   let mut epostAbstract := epostSpec.consumeMData
   let mut specApplied := specProof
-  let mut hasContinuationVC := false
+  let progMVars ← getMVars prog
+  let mut premiseHasProg := false
 
   /- abstract concrete `post` if it is not already abstract -/
   unless postAbstract.isMVar do
-    hasContinuationVC := true
+    unless premiseHasProg do
+      premiseHasProg := (← getMVars postSpec).any progMVars.contains
     /- `α → Pred`: type of `post` -/
     let postTy ← Sym.inferType postSpec
     /- mvar `postAbstract` for new abstract `post` -/
@@ -421,7 +423,8 @@ 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
+      unless premiseHasProg do
+        premiseHasProg := (← getMVars epostSpec).any progMVars.contains
       /- 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 +453,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)
+  return (← abstractMVars specApplied, premiseHasProg)
 
 /--
 Try to build a backward rule from a single spec theorem in `⊑` form.
@@ -466,7 +469,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'
@@ -481,12 +484,20 @@ 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 (res, postVCHasProg) ← 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, so its fact stays
-  -- available there.
-  return (rule, hasContinuationVC)
+  -- 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)
 
 /-! ## Equality spec rules
 

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

@@ -224,17 +224,17 @@ private def tryWPHeadReduce (goal : MVarId) (target : Expr) (info : WPInfo) :
 /-- 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 post or epost VC, a pure goal precondition is lifted into the local
-context first. Those VCs never see the goal's precondition, so the lift is what keeps the
-fact available in them. -/
+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
   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, hasContinuationVC) ←
+  let some (rule, needsPureLift) ←
     try
       mkBackwardRuleFromSpecCached thm info |>.run
     catch ex =>
@@ -244,7 +244,7 @@ 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 hasContinuationVC && !preIsTop then
+  if needsPureLift && !preIsTop then
     if let some g ← liftPurePre? goal pre then
       return .goals scope [g]
     if α.isProp then

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

@@ -244,8 +244,6 @@ instance : PartialOrder Prop where
   rel_trans := fun h1 h2 x => h2 (h1 x)
   rel_antisymm := fun h1 h2 => propext ⟨h1, h2⟩
 
-/-- `⊑` on the `Prop` lattice is implication. Tagged `@[grind =]` so `grind` can decompose
-entailments at `Prop` in partially decomposed verification conditions. -/
 @[grind =, simp] theorem le_prop_eq_imp (p q : Prop) : (p ⊑ q) = (p → q) := rfl
 
 /-- Supremum for Prop: true iff some element of the set is true -/

tests/bench/mvcgen/sym/vcgen_pure_precond.lean

@@ -16,7 +16,7 @@ set_option maxHeartbeats 10000000
 
 example : Goal 10 := by
   simp only [Goal, loop, step]
-  mvcgen' with finish
+  mvcgen'
 
-#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen' with finish) `(tactic| fail)
+#eval runBenchUsingTactic ``Goal [``loop, ``step] `(tactic| mvcgen') `(tactic| fail)
   [100, 400, 700]