Entailment-shaped goal decomposition for pre ⊑ rhs targets: unfolding Triple, introducing excess state arguments and pure preconditions, reducing exception-postcondition projections, and decomposing lattice connectives.

def Lean.Elab.Tactic.VCGen.unfoldTriple (goal : MVarId) : VCGenM MVarId

Unfold ⦃P⦄ x ⦃Q; E⦄ into the underlying entailment P ⊑ wp x Q E.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.VCGen.introPre (rule : Meta.Sym.BackwardRule) (goal : MVarId) : VCGenM (MVarId × FVarId)

Apply precondition-intro rule rule to goal, then introduce the freed hypothesis, leaving ⊤ as the residual precondition. Returns the new goal and the introduced hypothesis.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.VCGen.headReduceFstRhs? (goal : MVarId) (target α inst pre rhs : Expr) : VCGenM (Option MVarId)

Reduce a Prod.fst projection of a concrete tuple on the RHS of pre ⊑ rhs to the component it selects. An exception postcondition is a tuple with one component per exception layer, so the head layer of pre ⊑ epost.fst is a Prod.fst projection. reduceHead? performs the reduction, so a .snd chain below the projection and excess state arguments reduce in the same pass. Returns none if the RHS head is not Prod.fst or does not reduce; a ⊥/⊤ tuple falls through to the Prod.fst lattice split in splitLatticeOp?.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.VCGen.splitLatticeOp? (goal : MVarId) (rhs : Expr) : VCGenM (Option (List MVarId))

Decompose a supported lattice connective (⊓, ⇨, ⌜p⌝, ⊤, iInf, a ⊥/⊤ tuple projection) or a registered frame operator on the RHS of pre ⊑ rhs by saturating it with the built-in and @[frameproc] rewrites, closing it with a terminal, and point-framing any excess state arguments. Returns none if the head is neither a built-in connective nor a frame operator, or its rule does not apply.

An embedded proposition ⌜p⌝ is decomposed only when the precondition is ⊤: its ⊤-fixed terminal top_le_ofProp fails to apply otherwise, since turning pre ⊑ ⌜p⌝ into the subgoal p drops pre.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.VCGen.splitForallLe? (goal : MVarId) (rhs : Expr) : VCGenM (Option (List MVarId))

Decompose a ∀/→ on the RHS of pre ⊑ (∀ x, q x) via le_forall.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.VCGen.reduceTopAppliedPre? (goal : MVarId) (target pre : Expr) : Meta.Sym.SymM (Option MVarId)

Reduce a precondition that is the bare top applied to the state arguments introduced by le_of_forall_le, (⊤ : σ₁ → … → σₙ → Prop) s₁ … sₙ, to the bare (⊤ : Prop), rewriting goal's target pre ⊑ rhs to ⊤ ⊑ rhs. The equation pre = ⊤ is built on demand by folding Lean.Order.top_apply over the excess arguments and applied with replaceTargetEq.

The proof term is built directly with mkApp/mkConst and instances extracted from pre, avoiding mkAppM/instance synthesis (both expensive and unable to unify max-of-universe-variable instance levels in the abstract-monad setting). Returns none if pre is not the bare top applied to ≥ 1 argument, or its lattice instances are not in the expected instCompleteLatticePi shape (the caller then falls through).

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.VCGen.elimTopPre (goal : MVarId) : VCGenM MVarId

Reduce a Prop-lattice goal (⊤ : Prop) ⊑ φ to the bare proposition φ via top_le_prop, returning any other goal unchanged. The match on Sort 0 keeps it to the Prop base lattice, where the reduction is sound; entailments at an abstract lattice carrier pass through.

Equations

• One or more equations did not get rendered due to their size.