Module tactic 

A tactic framework with a first-class goal state — the interactive proof interface (ROOT R5 of the Lean-competitive architecture).

A ProofState holds the open Goals; a tactic transforms the focused goal, replacing it with zero or more subgoals and recording the inference rule used. When no goals remain, ProofState::qed assembles the recorded steps into a single DerivationTree and runs it through the SAME trust door as every other proof (check_derivation): the certifier turns it into a kernel term and the kernel re-checks that term against the goal. So a tactic proof is exactly as trusted as an automated one — the tactics only build the derivation the kernel validates, they are never themselves trusted.

The backward chainer is hosted here as the ProofState::auto tactic, so the existing automation is one tactic among many rather than the whole story.

Modules

combinators

Tactic values and the combinators that compose them — the language layer over the primitive ProofState methods. The backtracking combinators (first, try_, repeat) speculate on a clone of the state and commit only on success, so a partial failure never corrupts the proof.

Structs

CtorSpec

One constructor of an inductive, as given to ProofState::induction_over: its name and, per positional argument, whether that argument is itself of the inductive type — a recursive position that carries an induction hypothesis. Nil is CtorSpec { constructor: "Nil", recursive: vec![] }; Cons (head then tail) is CtorSpec { constructor: "Cons", recursive: vec![false, true] }.

Goal

A single proof obligation: prove target under the local hyps.

Hyp

A local hypothesis: its name, its proposition prop, and proof — a derivation that proves prop in the current local context. For a hypothesis that is directly in scope (a premise, an intro-discharged antecedent, or a branch hypothesis bound by cases) the proof is a PremiseMatch leaf the certifier resolves against the bound/registered hypothesis. For a conjunct extracted by cases from A ∧ B, the proof is the ConjunctionElim PROJECTION of the parent — so using the conjunct emits the projection, not a dangling reference. This is what lets elimination compose with the rest.

ProofState

The interactive proof state: the partial derivation plus the queue of open goals (front = focused). Tactics consume the focused goal and push any subgoals they create back to the front, so the proof is built depth-first, first-subgoal first — the order a reader expects. Clone is cheap relative to a proof and is what lets the backtracking combinators (first/try/repeat) speculate.

Enums

TacticError

What went wrong applying a tactic.

Type Aliases

Tactic

A first-class tactic: a transformation of the proof state that either makes progress (Ok) or does not apply (Err). Tactics are values, so they compose with the combinators.