Generic VCGenM helpers: checked backward-rule application, telescope-aware simp driver, hygienic binder introduction, hypothesis-internalization for grind, and the emission-time cleanup cleanupVC. None of these know anything about the entailment shapes solve decomposes.

def Lean.MVarId.replaceTargetDefEqFast (goal : MVarId) (targetNew : Expr) : MetaM MVarId

Change goal's Prop-typed target to the definitionally-equal targetNew, assigning goal a fresh synthetic-opaque goal for targetNew, so the kernel checks the two types against each other. Unlike MVarId.replaceTargetDefEq it skips the instantiateMVars/Expr.equal round-trip, so it neither detects a no-op change nor supports a non-Prop target; the caller must pass a genuinely different targetNew definitionally equal to the current target.

Equations

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

def Lean.Meta.Sym.BackwardRule.shareCommon (rule : BackwardRule) : SymM BackwardRule

Internalize a backward rule's pattern into the current SymM share table. See Pattern.shareCommon. Designed for dot notation: rule.shareCommon.

Equations

• rule.shareCommon = do let __do_lift ← rule.pattern.shareCommon pure { expr := rule.expr, pattern := __do_lift, resultPos := rule.resultPos }

def Lean.Elab.Tactic.VCGen.Lean.Meta.Sym.BackwardRule.applyChecked (rule : Meta.Sym.BackwardRule) (goal : MVarId) (ruleDesc? : Option MessageData := none) : VCGenM Meta.Sym.ApplyResult

VCGenM wrapper around BackwardRule.apply. Behaves identically to rule.apply goal unless the application fails and Context.debug is on. In that case it retries on a fresh metavariable whose type is the unfoldReducible-normalized goal type. If the retry succeeds, an earlier step forgot a normalization; we throw a hard error pointing at the rule and the missing reduction.

ruleDesc? describes the rule for debug output. When none, the description is reconstructed from rule.expr.getAppFn — works for the common case of a constant rule. Pass a custom message for dynamically-built rules.

Designed for dot notation: rule.applyChecked goal. Requires open Lean.Elab.Tactic.VCGen in scope so that the dot lookup resolves.

Equations

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

def Lean.Elab.Tactic.VCGen.processHypotheses (goal : Meta.Grind.Goal) : VCGenM Meta.Grind.Goal

Grind.processHypotheses if Context.internalize is true, otherwise a no-op.

Equations

• Lean.Elab.Tactic.VCGen.processHypotheses goal = do let __do_lift ← read if __do_lift.internalize = true then liftM (Lean.Meta.Grind.processHypotheses goal) else pure goal

def Lean.Elab.Tactic.VCGen.isProgramName (n : Name) : Bool

Whether n is a program variable's own name: no macro scopes and no implementation-detail __ prefix. Such a name stays accessible in a verification condition.

Equations

• Lean.Elab.Tactic.VCGen.isProgramName n = (!n.hasMacroScopes && !n.isImplementationDetail)

def Lean.Elab.Tactic.VCGen.numBindersToIntro : Expr → Nat

The leading binders of type, stopping at a binder over a product: ∀ (n : Nat) (p : α × β) counts one, because solve splits p into one binder per component first.

Equations

• Lean.Elab.Tactic.VCGen.numBindersToIntro (Lean.Expr.forallE binderName d b binderInfo) = if d.isAppOf `Prod = true then 0 else Lean.Elab.Tactic.VCGen.numBindersToIntro b + 1
• Lean.Elab.Tactic.VCGen.numBindersToIntro (Lean.Expr.letE declName type value b nondep) = Lean.Elab.Tactic.VCGen.numBindersToIntro b + 1
• Lean.Elab.Tactic.VCGen.numBindersToIntro x✝ = 0

def Lean.Elab.Tactic.VCGen.introsHygienicN (goal : MVarId) (n : Nat) : VCGenM MVarId

Introduce the first n binders of goal, named by mkFreshBinderNameForTactic, which tactic.hygienic makes inaccessible: ∀ acc, acc % 2 = 0 introduces acc✝.

Equations

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

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

introsHygienicN for every non-Prod binder the goal leads with.

Equations

• Lean.Elab.Tactic.VCGen.introsHygienic goal = do let __do_lift ← liftM goal.getType Lean.Elab.Tactic.VCGen.introsHygienicN goal (Lean.Elab.Tactic.VCGen.numBindersToIntro __do_lift)

def Lean.Elab.Tactic.VCGen.simpGoalTelescope (goal : MVarId) : VCGenM Meta.Sym.SimpGoalResult

Simplify the goal's target with the configured hypothesis simp methods (a no-op without Context.hypSimpMethods), threading the persistent simp cache through VCGenM's state. .noProgress is forwarded to the caller.

Equations

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

partial def Lean.Elab.Tactic.VCGen.introsExcessArgs (goal : MVarId) : VCGenM (Option MVarId)

Introduce the excess state arguments of an entailment goal pre ⊑ rhs whose lattice type is a function type σ₁ → … → σₙ → α: repeatedly apply stateArgIntro (a backward rule for Lean.Order.le_of_forall_le) and introduce the new state binder, until the lattice type is no longer a function type. Returns none when the carrier is not a function type (nothing to introduce); throws when the carrier is a function type that le_of_forall_le cannot peel, such as a dependent function lattice (a : α) → β a → ….

partial def Lean.Elab.Tactic.VCGen.cleanupVC (goal : MVarId) : VCGenM (Option MVarId)

Solves conjunctions whose leaves are True or e₁ = e₂, and returns a residual goal containing exactly the conjuncts that could not be solved. The goal is head-reduced first, so a conjunction that a match on a constructor or a projection of a tuple leaves behind a redex is still recognized. This procedure may assign metavariables in e₁/e₂, for example for e = ?m it will assign ?m := e.