Unary VCGen Internals

Implementation details for the unary VCGen planner and close passes.

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_pure_le_vcspec {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (x : α) (post : α → ENNReal) : post x ≤ wp (pure x) post

Cached raw-wp structural leaf for pure.

The equality theorem wp_pure remains the canonical rewrite rule. This lower-bound form lets raw wp goals use the cached @[vcspec] backward-rule path before falling back to @[wpStep].

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_map_le_vcspec {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} (f : α → β) (oa : OracleComp spec α) (post : β → ENNReal) : wp oa (post ∘ f) ≤ wp (f <$> oa) post

Cached raw-wp structural leaf for functorial map.

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_ite_le_vcspec {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (c : Prop) [Decidable c] (oa ob : OracleComp spec α) (post : α → ENNReal) : (if c then wp oa post else wp ob post) ≤ wp (if c then oa else ob) post

Cached raw-wp structural leaf for conditionals.

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_dite_le_vcspec {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (c : Prop) [Decidable c] (oa : c → OracleComp spec α) (ob : ¬c → OracleComp spec α) (post : α → ENNReal) : (if h : c then wp (oa h) post else wp (ob h) post) ≤ wp (dite c oa ob) post

Cached raw-wp structural leaf for dependent conditionals.

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_replicate_succ_le_vcspec {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (n : ℕ) (post : List α → ENNReal) : (wp oa fun (x : α) => wp (replicate n oa) fun (xs : List α) => post (x :: xs)) ≤ wp (replicate (n + 1) oa) post

Cached raw-wp structural leaf for replicate (n + 1).

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_list_mapM_cons_le_vcspec {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α β : Type} (x : α) (xs : List α) (f : α → OracleComp spec β) (post : List β → ENNReal) : (wp (f x) fun (y : β) => wp (List.mapM f xs) fun (ys : List β) => post (y :: ys)) ≤ wp (List.mapM f (x :: xs)) post

Cached raw-wp structural leaf for List.mapM on x :: xs.

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_list_foldlM_cons_le_vcspec {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α σ : Type} (x : α) (xs : List α) (f : σ → α → OracleComp spec σ) (init : σ) (post : σ → ENNReal) : (wp (f init x) fun (s : σ) => wp (List.foldlM f s xs) post) ≤ wp (List.foldlM f init (x :: xs)) post

Cached raw-wp structural leaf for List.foldlM on x :: xs.

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_query_le_vcspec {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (post : spec.Range t → ENNReal) : ∑' (u : spec.Range t), 1 / ↑(Fintype.card (spec.Range t)) * post u ≤ wp (query t) post

Cached raw-wp structural leaf for oracle queries.

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_HasQuery_query_le_vcspec {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] (t : spec.Domain) (post : spec.Range t → ENNReal) : ∑' (u : spec.Range t), 1 / ↑(Fintype.card (spec.Range t)) * post u ≤ wp (query t) post

Cached raw-wp structural leaf for HasQuery.query.

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_uniformSample_le_vcspec {α : Type} [SampleableType α] (post : α → ENNReal) : ∑' (u : α), Pr[= u | $ᵗ α] * post u ≤ wp ($ᵗ α) post

Cached raw-wp structural leaf for uniform sampling.

theorem OracleComp.ProgramLogic.TacticInternals.Unary.stdDoTriple_bind_wp {m : Type u → Type v} {Pred EPred α β : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {pre : Pred} (x : m α) (f : α → m β) (post : β → Pred) (epost : EPred) : Std.Do'.Triple pre x (fun (a : α) => Std.Do'.wp (f a) post epost) epost → Std.Do'.Triple pre (x >>= f) post epost

Generic Loom triple bind step with the intermediate postcondition fixed to the weakest precondition of the continuation. This is the Std.Do'.Triple counterpart of OracleComp.ProgramLogic.triple_bind_wp, and lets unary automation walk transformer-stack do blocks without guessing a user cut.

theorem OracleComp.ProgramLogic.TacticInternals.Unary.stdDoTriple_of_wp_le {m : Type u → Type v} {Pred EPred α : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {pre : Pred} (x : m α) (post : α → Pred) (epost : EPred) (hpre : Lean.Order.PartialOrder.rel pre (Std.Do'.wp x post epost)) : Std.Do'.Triple pre x post epost

Close a Loom triple from the corresponding WP entailment.

This is just Std.Do'.Triple.iff.mpr packaged as a theorem so tactic code can expose the weakest-precondition side condition and then run transformer-specific WP normalizers.

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_StateT_get_layer {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {σ : Type u} (post : σ → σ → Pred) (epost : EPred) : Std.Do'.wp MonadStateOf.get post epost = fun (s : σ) => Std.Do'.wp (pure (s, s)) (fun (p : σ × σ) => post p.1 p.2) epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_StateT_get_layer' {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {σ : Type u} (post : σ → σ → Pred) (epost : EPred) : Std.Do'.wp StateT.get post epost = fun (s : σ) => Std.Do'.wp (pure (s, s)) (fun (p : σ × σ) => post p.1 p.2) epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.stdDoTriple_StateT_get_of_rel {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {σ : Type u} (pre : σ → Pred) (post : σ → σ → Pred) (epost : EPred) (h : ∀ (s : σ), Lean.Order.PartialOrder.rel (pre s) (post s s)) : Std.Do'.Triple pre StateT.get post epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_StateT_set_layer {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {σ : Type u} (s' : σ) (post : PUnit.{u + 1} → σ → Pred) (epost : EPred) : Std.Do'.wp (set s') post epost = fun (x : σ) => Std.Do'.wp (pure (PUnit.unit, s')) (fun (p : PUnit.{u + 1} × σ) => post p.1 p.2) epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_StateT_run_get_layer {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {σ : Type u} (s : σ) (post : σ → σ → Pred) (epost : EPred) : Std.Do'.wp (MonadStateOf.get.run s) (fun (p : σ × σ) => post p.1 p.2) epost = Std.Do'.wp (pure (s, s)) (fun (p : σ × σ) => post p.1 p.2) epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_StateT_run_get_layer' {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {σ : Type u} (s : σ) (post : σ → σ → Pred) (epost : EPred) : Std.Do'.wp (StateT.get.run s) (fun (p : σ × σ) => post p.1 p.2) epost = Std.Do'.wp (pure (s, s)) (fun (p : σ × σ) => post p.1 p.2) epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_StateT_run_set_layer {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {σ : Type u} (s s' : σ) (post : PUnit.{u + 1} → σ → Pred) (epost : EPred) : Std.Do'.wp ((set s').run s) (fun (p : PUnit.{u + 1} × σ) => post p.1 p.2) epost = Std.Do'.wp (pure (PUnit.unit, s')) (fun (p : PUnit.{u + 1} × σ) => post p.1 p.2) epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_StateT_run_set_layer' {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {σ : Type u} (s s' : σ) (post : PUnit.{u + 1} → σ → Pred) (epost : EPred) : Std.Do'.wp ((StateT.set s').run s) (fun (p : PUnit.{u + 1} × σ) => post p.1 p.2) epost = Std.Do'.wp (pure (PUnit.unit, s')) (fun (p : PUnit.{u + 1} × σ) => post p.1 p.2) epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_StateT_map_layer {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {σ α β : Type u} (f : α → β) (x : StateT σ m α) (post : β → σ → Pred) (epost : EPred) : Std.Do'.wp (f <$> x) post epost = fun (s : σ) => Std.Do'.wp ((f <$> x).run s) (fun (p : β × σ) => post p.1 p.2) epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_ReaderT_read_layer {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {ρ : Type u} (post : ρ → ρ → Pred) (epost : EPred) : Std.Do'.wp MonadReaderOf.read post epost = fun (r : ρ) => Std.Do'.wp (pure r) (fun (a : ρ) => post a r) epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_ReaderT_read_layer' {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {ρ : Type u} (post : ρ → ρ → Pred) (epost : EPred) : Std.Do'.wp ReaderT.read post epost = fun (r : ρ) => Std.Do'.wp (pure r) (fun (a : ρ) => post a r) epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.stdDoTriple_ReaderT_read_of_rel {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {ρ : Type u} (pre : ρ → Pred) (post : ρ → ρ → Pred) (epost : EPred) (h : ∀ (r : ρ), Lean.Order.PartialOrder.rel (pre r) (post r r)) : Std.Do'.Triple pre MonadReaderOf.read post epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_ReaderT_run_read_layer {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {ρ : Type u} (r : ρ) (post : ρ → ρ → Pred) (epost : EPred) : Std.Do'.wp (MonadReaderOf.read.run r) (fun (a : ρ) => post a r) epost = Std.Do'.wp (pure r) (fun (a : ρ) => post a r) epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_ReaderT_run_read_layer' {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {ρ : Type u} (r : ρ) (post : ρ → ρ → Pred) (epost : EPred) : Std.Do'.wp (ReaderT.read.run r) (fun (a : ρ) => post a r) epost = Std.Do'.wp (pure r) (fun (a : ρ) => post a r) epost

theorem OracleComp.ProgramLogic.TacticInternals.Unary.mAlgOrdered_wp_OptionT_run_StateT_get {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {σ : Type} (s : σ) (post : σ → σ → ENNReal) (epost : EPost⟨ENNReal⟩) : MAlgOrdered.wp (StateT.get.run s).run (Std.Do'.EPost.cons.pushOption (fun (p : σ × σ) => post p.1 p.2) epost) = post s s

theorem OracleComp.ProgramLogic.TacticInternals.Unary.mAlgOrdered_wp_OptionT_run_StateT_set {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {σ : Type} (s s' : σ) (post : PUnit.{1} → σ → ENNReal) (epost : EPost⟨ENNReal⟩) : MAlgOrdered.wp ((StateT.set s').run s).run (Std.Do'.EPost.cons.pushOption (fun (p : PUnit.{1} × σ) => post p.1 p.2) epost) = post PUnit.unit s'

theorem OracleComp.ProgramLogic.TacticInternals.Unary.mAlgOrdered_wp_OptionT_run_lift {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {α : Type} (oa : OracleComp spec α) (post : α → ENNReal) (epost : EPost⟨ENNReal⟩) : MAlgOrdered.wp (OptionT.lift oa).run (Std.Do'.EPost.cons.pushOption post epost) = MAlgOrdered.wp oa post

theorem OracleComp.ProgramLogic.TacticInternals.Unary.mAlgOrdered_wp_OptionT_run_StateT_monadLift_lift {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {σ α : Type} (oa : OracleComp spec α) (s : σ) (post : α → σ → ENNReal) (epost : EPost⟨ENNReal⟩) : MAlgOrdered.wp ((MonadLift.monadLift (OptionT.lift oa)).run s).run (Std.Do'.EPost.cons.pushOption (fun (p : α × σ) => post p.1 p.2) epost) = MAlgOrdered.wp oa fun (a : α) => post a s

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_StateT_OptionT_monadLift_lift {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {σ α : Type} (oa : OracleComp spec α) (post : α → σ → ENNReal) (epost : EPost⟨ENNReal⟩) : Std.Do'.wp (MonadLift.monadLift (OptionT.lift oa)) post epost = fun (s : σ) => MAlgOrdered.wp oa fun (a : α) => post a s

theorem OracleComp.ProgramLogic.TacticInternals.Unary.mAlgOrdered_wp_OptionT_run_StateT_monadLift_lift_map {ι : Type u} {spec : OracleSpec ι} [spec.Fintype] [spec.Inhabited] {σ α β : Type} (oa : OracleComp spec α) (s : σ) (f : α × σ → β) (post : β → ENNReal) (nonePost : ENNReal) : (MAlgOrdered.wp ((MonadLift.monadLift (OptionT.lift oa)).run s).run fun (o : Option (α × σ)) => match Option.map f o with | some b => post b | none => nonePost) = MAlgOrdered.wp oa fun (a : α) => post (f (a, s))

theorem OracleComp.ProgramLogic.TacticInternals.Unary.wp_ReaderT_map_layer {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Std.Do'.Assertion Pred] [Std.Do'.Assertion EPred] [Std.Do'.WP m Pred EPred] {ρ α β : Type u} (f : α → β) (x : ReaderT ρ m α) (post : β → ρ → Pred) (epost : EPred) : Std.Do'.wp (f <$> x) post epost = fun (r : ρ) => Std.Do'.wp ((f <$> x).run r) (fun (b : β) => post b r) epost

vcspec_simp normalization set

Centralized registration of the transformer-wp peel lemmas, *.run projections, monadic-algebra rewrites, and the Loom.wp_eq_mAlgOrdered_wp bridges that the unary tactic uses to expose spec-applicable goal shapes. The single simp set is consumed by runVCSpecSimp. New normalization rewrites should be tagged here (or at definition) rather than inserted into a tactic-local simp only [...] list.

def OracleComp.ProgramLogic.TacticInternals.Unary.throwWpStepError : Lean.Elab.Tactic.TacticM Unit

def OracleComp.ProgramLogic.TacticInternals.Unary.runHoareStepRuleUsing (cut : Lean.TSyntax `term) : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.tryCloseSpecGoalImmediate : Lean.Elab.Tactic.TacticM Bool

Try to close the current goal using only immediate local information. This is intentionally cheap: it is used while speculating on triple_bind, so it must not launch expensive proof search on goals with unresolved cut metavariables.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryCloseSpecGoalSearch : Lean.Elab.Tactic.TacticM Bool

Try bounded local proof search on a closed goal. We only invoke solve_by_elim once the target has no unresolved expression metavariables; this avoids pathological search on speculative intermediate cuts introduced by triple_bind.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenStepWithTheorem (thm : Lean.TSyntax `term) (requireClosed : Bool := false) : Lean.Elab.Tactic.TacticM Bool

Apply an explicit unary theorem/assumption step and try to close any easy side goals. When requireClosed is true, the step only succeeds if no goals remain afterwards.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryCloseSpecGoal : Lean.Elab.Tactic.TacticM Bool

Try to close the current goal (typically a Triple subgoal) using direct hypotheses, canonical leaf rules, or bounded local consequence search.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryCloseSpecGoalFinal : Lean.Elab.Tactic.TacticM Bool

Finish-only closure step: includes the support-sensitive leaf rules that are too expensive for the default vcstep hot path.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenClosePass : Lean.Elab.Tactic.TacticM Bool

Run one bounded finish/closure pass across all current goals.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryMatchDecomp (comp : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Try to decompose a match expression in the computation by case-splitting on its discriminant(s). Only fires when the computation is a compiled matcher (detected via matchMatcherApp?). Delegates to split which handles the actual case analysis.

def OracleComp.ProgramLogic.TacticInternals.Unary.isConstantLambda (e : Lean.Expr) : Bool

Check if an expression is a lambda whose body does not use the bound variable (i.e. a constant function fun _ => c).

def OracleComp.ProgramLogic.TacticInternals.Unary.tryBindImmediate (comp : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Try the strongest automatic bind step: triple_bind plus immediate closure of the spec side-goal.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryLoopInvariantRuleAuto (comp : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Try only the automatic loop-invariant rules, without the structural fallback rules.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryLoopFallback (comp : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Try only the structural loop fallback rules (succ / cons) after invariant search.

def OracleComp.ProgramLogic.TacticInternals.Unary.runLoopInvExplicit (inv : Lean.TSyntax `term) : Lean.Elab.Tactic.TacticM Bool

Apply a loop invariant rule with an explicitly provided invariant.

def OracleComp.ProgramLogic.TacticInternals.Unary.findHoareCutHintCandidates : Lean.Elab.Tactic.TacticM (Array Lean.Name)

Find the local hypotheses that work as explicit bind cuts.

def OracleComp.ProgramLogic.TacticInternals.Unary.findUniqueHoareCutHint? : Lean.Elab.Tactic.TacticM (Option Lean.Name)

Find the unique local hypothesis that works as an explicit bind cut. Returns none if there are 0 or ≥ 2 viable candidates.

def OracleComp.ProgramLogic.TacticInternals.Unary.findLoopInvHintCandidates : Lean.Elab.Tactic.TacticM (Array Lean.Name)

Find the local hypotheses that work as explicit loop invariants.

def OracleComp.ProgramLogic.TacticInternals.Unary.findUniqueLoopInvHint? : Lean.Elab.Tactic.TacticM (Option Lean.Name)

Find the unique local hypothesis that works as an explicit loop invariant. Returns none if there are 0 or ≥ 2 viable candidates.

def OracleComp.ProgramLogic.TacticInternals.Unary.findRegisteredVCGenRuleCandidates : Lean.Elab.Tactic.TacticM (Array VCSpecEntry)

Find the registered unary @[vcspec] entries whose bounded application makes progress on the current goal. Prefers direct discrimination-tree hits on the goal's comp, falling back to kind-matched entries filtered by structural compatibility.

def OracleComp.ProgramLogic.TacticInternals.Unary.findRegisteredVCGenRule? : Lean.Elab.Tactic.TacticM (Option VCSpecEntry)

Find the first registered unary @[vcspec] entry whose bounded application makes progress.

def OracleComp.ProgramLogic.TacticInternals.Unary.throwVCGenStepError : Lean.Elab.Tactic.TacticM Unit

inductive OracleComp.ProgramLogic.TacticInternals.Unary.ProbEqAction : Type

Try to close or rewrite a Pr[ ...] = Pr[ ...] goal by swapping adjacent independent binds. Handles 0–2 layers of tsum peeling.

• swap : ProbEqAction
• congr : ProbEqAction
• congrNoSupport : ProbEqAction
• rewrite : ProbEqAction
• rewriteUnder (depth : ℕ) : ProbEqAction

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqSwap : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqCongrNoSupportWithNames (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqCongrNoSupport : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqCongrWithNames (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM Bool

Try to decompose a Pr[ ... | mx >>= f₁] = Pr[ ... | mx >>= f₂] goal by congruence, then auto-intro the bound variable and support hypothesis.

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqCongr : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqCongrChainWithNames (supportSensitive : Bool) (names : Array Lean.Name) : Lean.Elab.Tactic.TacticM Bool

partial def OracleComp.ProgramLogic.TacticInternals.Unary.mkProbSwapUnderProof (depth : ℕ) : Lean.Elab.Tactic.TacticM (Lean.TSyntax `term)

Build a theorem that swaps adjacent binds under depth shared prefixes.

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqRewrite : Lean.Elab.Tactic.TacticM Bool

Try to rewrite one top-level bind-swap without closing the goal.

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqRewriteUnder (depth : ℕ) : Lean.Elab.Tactic.TacticM Bool

Try to rewrite one bind-swap under depth shared prefixes on either side.

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqAction : ProbEqAction → Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.tryProbEqActions (steps : List ProbEqAction) : Lean.Elab.Tactic.TacticM Bool

Try a small backtracking-free sequence of probability-equality steps.

def OracleComp.ProgramLogic.TacticInternals.Unary.probEqActionPlans : List (List ProbEqAction)

def OracleComp.ProgramLogic.TacticInternals.Unary.tryProbEqPlans (plans : List (List ProbEqAction)) : Lean.Elab.Tactic.TacticM Bool

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbEqNormalize : Lean.Elab.Tactic.TacticM Bool

Explicit probability-equality normalization.

This runs the deeper planner-backed bind-rewrite/congruence search used by vcstep?, but only when the user asks for it. Plain vcstep keeps the smaller default plan set.

def OracleComp.ProgramLogic.TacticInternals.Unary.runProbOutputEqRelBridge : Lean.Elab.Tactic.TacticM Bool

Try to handle a Pr[ ...] = Pr[ ...] equality goal by swap, congr, or swap+congr. Also tries a fallback bridge from exact probOutput equalities into relational VCGen.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryProbEqGoal : Lean.Elab.Tactic.TacticM Bool

Try to handle a Pr[ ...] = Pr[ ...] equality goal by swap, congr, or swap+congr.

def OracleComp.ProgramLogic.TacticInternals.Unary.throwVCGenStepRwError (depth : ℕ) : Lean.Elab.Tactic.TacticM Unit

def OracleComp.ProgramLogic.TacticInternals.Unary.throwVCGenStepRwCongrError (supportSensitive : Bool) : Lean.Elab.Tactic.TacticM Unit

def OracleComp.ProgramLogic.TacticInternals.Unary.throwVCGenStepRwNormalizeError : Lean.Elab.Tactic.TacticM Unit

def OracleComp.ProgramLogic.TacticInternals.Unary.tryLowerProbGoal : Lean.Elab.Tactic.TacticM Bool

Try to lower a probability goal into a Triple, wp, or probability-equality goal.

def OracleComp.ProgramLogic.TacticInternals.Unary.tryRawWpStructuralStep : Lean.Elab.Tactic.TacticM Bool

Continue structural stepping on a raw wp goal after probability lowering or explicit wp-level work. This stays deliberately smaller than the Triple path.

def OracleComp.ProgramLogic.TacticInternals.Unary.trySupportCutBind (comp : Lean.Expr) : Lean.Elab.Tactic.TacticM Bool

Try to synthesize a support-based intermediate postcondition for a bind step. When the computation is oa >>= f and no explicit spec is available, tries applying triple_bind with an inferred cut and closing the spec subgoal via triple_support, which unifies the cut to fun x => 𝟙⟦x ∈ support oa⟧.

Goal classification and per-kind dispatch

Mirrors Loom.Tactic.VCGen.GoalKind and classifyGoalKind: the structural core picks one strategy per goal kind instead of falling through a procedural cascade. New monad transformers / combinators become a new UnaryGoalKind constructor plus a registered @[vcspec] rule, not another tryEvalTacticSyntax block.

Probability lowering is run opportunistically before classification, since Pr[…] may appear inside wp … goals that should ultimately dispatch via raw wp or Triple rules; only goals where lowering actually fires bypass the rest of the pipeline.

inductive OracleComp.ProgramLogic.TacticInternals.Unary.UnaryGoalKind : Type

High-level classification of a unary VCGen target.

Kept intentionally coarse: structural details (the bind continuation, ite condition, matcher app, …) live in the comp payload, not in the constructor, so per-kind handlers can share tryEvalTacticSyntax-style logic with the existing helpers.

• relational : UnaryGoalKind

  A relational RelTriple / RelWP goal; defer to the relational planner.

• tripleBind (comp : Lean.Expr) : UnaryGoalKind

  A unary Triple whose computation is a >>= application.

• tripleIte : UnaryGoalKind

  A unary Triple whose computation is ite c a b (non-dependent).

• tripleDite : UnaryGoalKind

  A unary Triple whose computation is dite c a b (dependent).

• tripleMatch (comp : Lean.Expr) : UnaryGoalKind

  A unary Triple whose computation is a compiled match matcher.

• tripleLoop (comp : Lean.Expr) : UnaryGoalKind

  A unary Triple whose computation is a replicate / List.mapM / List.foldlM head.

• tripleOther : UnaryGoalKind

  A unary Triple whose computation does not match the cases above; the dispatcher unfolds to raw wp and lets @[wpStep] rewrite.

• rawWp : UnaryGoalKind

  A raw wp / ≤ wp goal.

• unknown : UnaryGoalKind

  Unrecognized goal shape.

@[implicit_reducible]

instance OracleComp.ProgramLogic.TacticInternals.Unary.instInhabitedUnaryGoalKind : Inhabited UnaryGoalKind

def OracleComp.ProgramLogic.TacticInternals.Unary.instInhabitedUnaryGoalKind.default : UnaryGoalKind

def OracleComp.ProgramLogic.TacticInternals.Unary.classifyUnaryGoalKind (target : Lean.Expr) : Lean.MetaM UnaryGoalKind

Classify the current goal target as a UnaryGoalKind.

Probability lowering is intentionally not a kind here: it runs opportunistically in runVCGenStructuralCore before classification, so a wp … = ∑' u, Pr[…] * … goal still classifies as rawWp / tripleOther rather than getting stuck in a non-lowerable prob branch.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenStructuralCore : Lean.Elab.Tactic.TacticM Bool

Structural/default unary VCGen step, excluding explicit cut/invariant/theorem-driven fallbacks and the final close/search phase.

Implemented as a single goal-kind dispatch (mirroring Loom.Tactic.VCGen.solve): each kind picks one cluster of strategies, with the triple* kinds optionally chaining into runTripleFallback so that specialized dispatchers can defer cleanly. Probability lowering is run opportunistically before classification so that goals where lowering does not fire still flow through the structural dispatcher.

def OracleComp.ProgramLogic.TacticInternals.Unary.planVCGenStep? : Lean.Elab.Tactic.TacticM (Option PlannedStep)

Choose one unary VCGen step and remember how to replay it explicitly.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenPlannedStep? : Lean.Elab.Tactic.TacticM (Option PlannedStep)

Execute one planned unary VCGen step, returning the chosen step for replay/trace.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenStep : Lean.Elab.Tactic.TacticM Bool

One step of VCGen on a Triple goal. Returns true if any progress was made.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenPassPlanned : Lean.Elab.Tactic.TacticM (Array PlannedStep)

Run one VCGen pass across all current goals and record the chosen steps.

def OracleComp.ProgramLogic.TacticInternals.Unary.runVCGenPass : Lean.Elab.Tactic.TacticM Bool

Run one VCGen pass across all current goals.