chore: various fixes

Author: sgraf812

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

@@ -88,6 +88,9 @@ public structure VCGen.IntroRules where
   /-- The backward rule for `Lean.Order.ofProp_le`. Introduces an embedded pure
   precondition `⌜p⌝` on any complete lattice. -/
   ofPropPreIntro : BackwardRule
+  /-- The backward rule for `Lean.Order.true_le`. Replaces a `True` precondition
+  with `⊤` on the `Prop` lattice. -/
+  truePreIntro : BackwardRule
 
 public structure VCGen.Context where
   /-- Pre-built backward rules for the introduction steps of `solve`. -/

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

@@ -116,11 +116,13 @@ public def mkContext (lemmas : Syntax) (goal : MVarId) (ignoreStarArg := false)
   let topStateArgIntro ← mkBackwardRuleFromDecl ``Lean.Order.top_le_of_forall_top_le
   let propPreIntro ← mkBackwardRuleFromDecl ``Lean.Order.prop_le
   let ofPropPreIntro ← mkBackwardRuleFromDecl ``Lean.Order.ofProp_le
+  let truePreIntro ← mkBackwardRuleFromDecl ``Lean.Order.true_le
   let elimPreRule ← mkBackwardRuleFromDecl ``Lean.Order.top_le_prop
   let andIntroRule ← mkBackwardRuleFromDecl ``And.intro
   let specThmsNew ← SymM.run <| migrateSpecTheoremsDatabase specThms simpThms
   let ctx : VCGen.Context := {
-    introRules := { tripleIntro, stateArgIntro, topStateArgIntro, propPreIntro, ofPropPreIntro },
+    introRules := { tripleIntro, stateArgIntro, topStateArgIntro, propPreIntro, ofPropPreIntro,
+                    truePreIntro },
     elimPreRule,
     andIntroRule,
   }

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

@@ -122,46 +122,48 @@ 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 most recently lifted pure precondition,
-cached in `Scope.lastLiftedPre?`. This is one defeq check against one hypothesis, not an
-assumption search.
+/-- Strategy 10: close `pre ⊑ φ` on the `Prop` lattice against the most recently lifted pure
+precondition, cached in `Scope.lastLiftedPre?`. Runs after lattice decomposition, so `φ` is an
+opaque proposition rather than a lattice connective. 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 (scope : VCGen.Scope) (goal : MVarId) (α pre rhs : Expr) :
     VCGenM (Option (List MVarId)) :=
   goal.withContext do
+    unless α.isProp do return none
     if rhs.hasExprMVar then 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
-          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
+    unless ← isDefEqS rhs hyp.type do return none
     trace[Elab.Tactic.Do.vcgen] "Solved by lifted hypothesis {hyp.userName}"
-    goal.assign proof
+    goal.assign (← mkAppM ``Lean.Order.le_prop #[pre, rhs, hyp.toExpr])
     return some []
 
-/-- Strategy 6: lift an embedded pure precondition `⌜φ⌝` into the local context, leaving `⊤`
+/-- Close a bare `Prop` residual, such as the subgoal of the `⌜φ⌝` lattice rule, against the
+most recently lifted pure precondition. Runs when the target is not a lattice entailment,
+just before it would be classified as a VC. -/
+private def tryLiftedHypBare (scope : VCGen.Scope) (goal : MVarId) (target : Expr) :
+    VCGenM (Option (List MVarId)) :=
+  goal.withContext do
+    if target.hasExprMVar then return none
+    let some fvarId := scope.lastLiftedPre? | return none
+    let some hyp := (← getLCtx).find? fvarId | return none
+    unless ← isDefEqS target hyp.type do return none
+    trace[Elab.Tactic.Do.vcgen] "Solved by lifted hypothesis {hyp.userName}"
+    goal.assign hyp.toExpr
+    return some []
+
+/-- Strategy 5: 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 8: decompose a supported lattice connective on the RHS. -/
+/-- Strategy 9: decompose a supported lattice connective on the RHS. -/
 private def tryLattice (goal : MVarId) (target rhs : Expr) (preIsTop : Bool) :
     VCGenM (Option (List MVarId)) := do
   solveLatticeConnective? goal target rhs preIsTop
@@ -197,13 +199,13 @@ private def substOrHoistLet (goal : MVarId) (target : Expr) (info : WPInfo)
       | throwError "Failed to intro hoisted let"
     return goal
 
-/-- Strategy 7a: hoist or zeta-substitute a `let` from the program head. -/
+/-- Strategy 11a: hoist or zeta-substitute a `let` from the program head. -/
 private def tryWPLet (goal : MVarId) (target : Expr) (info : WPInfo) : VCGenM (Option MVarId) := do
   let .letE name type val body nondep := info.prog.getAppFn | return none
   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
+/-- Strategy 11b: 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
@@ -222,7 +224,7 @@ private def tryWPMatch (goal : MVarId) (target : Expr) (info : WPInfo) :
     | .closed => continue
   return some simpGoals.toList
 
-/-- Strategy 7c: zeta-unfold a local let-bound fvar used as the program head. -/
+/-- Strategy 11c: zeta-unfold a local let-bound fvar used as the program head. -/
 private def tryWPFVarZeta (goal : MVarId) (target : Expr) (info : WPInfo) :
     VCGenM (Option MVarId) := do
   let f := info.prog.getAppFn
@@ -232,7 +234,7 @@ private def tryWPFVarZeta (goal : MVarId) (target : Expr) (info : WPInfo) :
   let prog ← shareCommonInc (val.betaRev info.prog.getAppRevArgs)
   return some (← replaceProgDefEq goal target info prog)
 
-/-- Strategy 7d: reduce a projection head in the program. -/
+/-- Strategy 11d: reduce a projection head in the program. -/
 private def tryWPHeadReduce (goal : MVarId) (target : Expr) (info : WPInfo) :
     VCGenM (Option MVarId) := do
   let f := info.prog.getAppFn
@@ -242,7 +244,7 @@ private def tryWPHeadReduce (goal : MVarId) (target : Expr) (info : WPInfo) :
   let prog ← betaRevS f' info.prog.getAppRevArgs
   return some (← replaceProgDefEq goal target info prog)
 
-/-- Strategy 7e: look up a registered `@[spec]` theorem (triple or simp) for the program head
+/-- Strategy 11e: look up a registered `@[spec]` theorem (triple or simp) for the program head
 and apply its cached backward rule. -/
 private def applySpec (scope : VCGen.Scope) (goal : MVarId) (target : Expr) (info : WPInfo) :
     VCGenM SolveResult := do
@@ -293,23 +295,24 @@ 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` against the most recently lifted
-   precondition, cached in `Scope.lastLiftedPre?`.
-6. **Embedded pure precondition introduction**: lift a `⌜φ⌝` precondition into the local
+5. **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
+6. **State-argument introduction**: If the lattice carrier is a function type
    `σ₁ → ... → σₙ → Base`, introduce all excess state arguments.
-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.
+7. **Bare pure precondition introduction**: on the `Prop` lattice, replace a `True`
+   precondition by `⊤` and lift any other precondition into the local context.
+8. **EPost projection reduction**: reduce an `EPost.Cons.head` RHS to the projected component.
+9. **Lattice decomposition**: decompose `⊓`, `⇨`, `⌜p⌝` and `⊤` RHS connectives.
+10. **Lifted-hypothesis discharge**: close a residual `pre ⊑ φ` entailment against the most
+    recently lifted precondition, cached in `Scope.lastLiftedPre?`.
 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.
+Pure preconditions are lifted as soon as they arise (steps 5 and 7). The lifted hypothesis is
+cached in `Scope.lastLiftedPre?`. Step 10 closes residual entailments against it with a single
+defeq check, and bare `Prop` targets, such as the subgoal of the `⌜φ⌝` lattice rule, are
+checked against it before being classified as VCs.
 -/
 public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := goal.withContext do
   if ← outOfFuel then return .stop
@@ -329,11 +332,12 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
   if let some g ← tryTripleUnfold goal target then return .goals scope [g]
   if let some g ← tryBareWP goal target then return .goals scope [g]
 
-  let_expr PartialOrder.rel α inst pre rhs := target | return .noEntailment target
+  let some (α, inst, pre, rhs) := target.app4? ``PartialOrder.rel
+    | if let some gs ← tryLiftedHypBare scope goal target then return .goals scope gs
+      else return .noEntailment target
   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 scope goal α pre rhs then return .goals scope gs
 
   -- 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`
@@ -342,6 +346,10 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
     return .goals { scope with lastLiftedPre? := some h } [g]
   if α.isForall then return .goals scope [← introStateArgs preIsTop goal]
   if !preIsTop && α.isProp then
+    if pre.isTrue then
+      let .goals [g] ← (← read).introRules.truePreIntro.applyChecked goal
+        | throwError "Failed to apply {.ofConstName ``Lean.Order.true_le} to{indentExpr target}"
+      return .goals scope [g]
     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]
@@ -350,8 +358,10 @@ public def solve (scope : VCGen.Scope) (goal : MVarId) : VCGenM SolveResult := g
   -- (`tryWPMatch`, `tryLattice`) or apply a registered spec (`applySpec`).
   let scope ← scope.collectLocalSpecs goal
 
-  -- Phase 3: lattice connective decomposition.
+  -- Phase 3: lattice connective decomposition, then lifted-hypothesis discharge of the
+  -- residual entailments.
   if let some gs ← tryLattice goal target rhs preIsTop then return .goals scope gs
+  if let some gs ← tryLiftedHyp scope goal α pre rhs 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.

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

@@ -273,6 +273,9 @@ theorem le_prop (x y : Prop) : y → x ⊑ y :=
 theorem of_top_le_prop {x : Prop} : (⊤ : Prop) ⊑ x → x :=
   fun h => h (le_top True trivial)
 
+theorem true_le (x : Prop) : ((⊤ : Prop) ⊑ x) → (True : Prop) ⊑ x :=
+  fun h => le_prop True x (of_top_le_prop h)
+
 @[simp] theorem iInf_prop_eq_forall {ι : Type u} (f : ι → Prop) :
     (iInf f : Prop) = (∀ i, f i) := by
   apply propext