Struct ProofState 

pub struct ProofState { /* private fields */ }

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.

Implementations

impl ProofState

pub fn start(premises: Vec<ProofExpr>, goal: ProofExpr) -> Self

Begin proving goal from premises, naming the hypotheses hp0, hp1, ….

pub fn start_with_names( premises: Vec<ProofExpr>, names: &[Option<String>], goal: ProofExpr, ) -> Self

Begin proving goal from premises, using the given names for the hypotheses where present (parallel to premises), falling back to the positional hp{i} otherwise. Lets a surface Given (h): … name a premise so a Proof: script can say cases h instead of cases hp0.

pub fn focus(&self) -> Option<&Goal>

The focused goal, or None if the proof is complete.

pub fn open_goals(&self) -> usize

Number of still-open goals.

pub fn focused_target(&self) -> Option<&ProofExpr>

The focused goal’s target, if any goal is open — the tactic-script and IDE surface for inspecting where a proof stands.

pub fn scope_simp_set(&self) -> SimpSet

A crate::simp::SimpSet compiled from every in-scope hypothesis that orients as a rewrite rule — the default rule set for the script-level simp (a premise or cited lemma of rule shape is automatically a rule).

pub fn intro(&mut self, name: &str) -> Result<&mut Self, TacticError>

intro name: for a goal P → Q, assume P as hypothesis name and reduce to Q; for ∀x. φ(x), introduce the bound variable under name and reduce to φ(name). Mirrors Lean’s intro.

pub fn assumption(&mut self) -> Result<&mut Self, TacticError>

assumption: close the goal with any hypothesis whose proposition is exactly the target, emitting THAT hypothesis’s proof (a direct reference, or a ConjunctionElim projection for a conjunct extracted by cases).

pub fn exact(&mut self, name: &str) -> Result<&mut Self, TacticError>

exact name: close the goal with the specifically-named hypothesis, which must prove the target.

pub fn split(&mut self) -> Result<&mut Self, TacticError>

constructor / split: for a goal A ∧ B, reduce to the two subgoals A and B.

pub fn left(&mut self) -> Result<&mut Self, TacticError>

left: prove A ∨ B by proving A.

pub fn right(&mut self) -> Result<&mut Self, TacticError>

right: prove A ∨ B by proving B.

pub fn exists(&mut self, witness: ProofTerm) -> Result<&mut Self, TacticError>

exists w: prove ∃x. φ(x) by exhibiting the witness w and reducing to φ(w).

pub fn apply(&mut self, rule: &ProofExpr) -> Result<&mut Self, TacticError>

apply rule: rule is P → Goal (a hypothesis or premise). Reduce the goal to its antecedent P by modus ponens.

pub fn cases(&mut self, name: &str) -> Result<&mut Self, TacticError>

cases h / destruct h: eliminate a hypothesis by its shape.

• A ∧ B: add h_1 : A and h_2 : B to the goal, each backed by the ConjunctionElim projection of h — so using a conjunct emits the projection, never a dangling reference.
• A ∨ B: split into two goals, one assuming A, one assuming B (DisjunctionCases).
• ∃x. φ: introduce a fresh witness c and the hypothesis φ(c) (ExistentialElim); the goal must not mention c, which holds since it is fresh.

pub fn induction(&mut self) -> Result<&mut Self, TacticError>

induction: on a goal ∀n. P(n) over Nat, split into the base case P(Zero) and the step case P(Succ k) with the induction hypothesis ih : P(k) in scope. Certified as a Fix/Match over the kernel’s Nat recursor; the IH resolves to the recursive call. (Nat only for now — List/general inductives need the dependent InductionScheme.)

pub fn induction_over( &mut self, ind_type: &str, ctors: Vec<CtorSpec>, ) -> Result<&mut Self, TacticError>

induction_over: generic structural induction over ANY inductive ind_type, one subgoal per constructor. On a goal ∀x. P(x), each constructor C a₀…aₙ yields the subgoal P(C a₀ … aₙ); every recursive argument aᵢ (one of the inductive type) contributes an induction hypothesis P(aᵢ), placed FIRST so auto/assumption discharge the recursive obligation against the IH rather than a base fact. Generalizes induction (fixed to the nullary-base + unary-step Nat shape) to constructors with several — or zero — recursive positions (Nil/Cons, Leaf/Node, an N-way enum). Assembled as the dependent InductionScheme eliminator (fix rec. λx. match x { … }), which the kernel re-checks for coverage, case types, and termination.

The constructor arguments run the search as rigid eigen-CONSTANTS (so the backward chainer neither grounds nor unrolls them); assemble remaps each back to the bound Variable the certifier’s match arm binds.

pub fn rewrite(&mut self, name: &str) -> Result<&mut Self, TacticError>

rewrite h: h : lhs = rhs rewrites every occurrence of lhs to rhs in the goal, reducing it to goal[lhs := rhs]. Certified by Eq_rec (Leibniz): the node concludes the original goal (which contains lhs = to), its equality premise proves rhs = lhs (the symmetric of h, so from = rhs, to = lhs), and its source premise is the rewritten subgoal. Fails if lhs does not occur.

pub fn simp(&mut self, set: &SimpSet) -> Result<&mut Self, TacticError>

simp: normalize the focused goal by the rule set, left-to-right to a fixpoint, then close it if it became trivial (reflexivity or an exact hypothesis). Mirrors Lean’s simp.

Each rewrite is one certified Rewrite refinement — the instantiated rule equality (a UniversalInstTerm chain over the lemma, conditions discharged by ModusPonens) is the closed premise, the rewritten goal the open one — so qed re-checks every step in the kernel. Loop protection is a step budget plus a seen-goal set (commuting rules like a = b, b = a terminate instead of ping-ponging). Fails only if it neither rewrote nor closed anything.

pub fn decide(&mut self) -> Result<&mut Self, TacticError>

decide: close the focused goal by evaluation, if it is a closed decidable proposition that evaluates TRUE (ground arithmetic, comparisons, Bool equalities, and ∧/∨/→ over them). Mirrors Lean’s decide. A false or open goal is declined.

pub fn omega(&mut self) -> Result<&mut Self, TacticError>

omega: linear INTEGER arithmetic. When the in-scope ≤/< hypotheses are jointly unsatisfiable over ℤ — using discreteness (a < b ⟹ a+1 ≤ b), the fact rational solvers lack — refute them and discharge ANY goal by ex-falso. Proves x < y ∧ y < x+1 ⊢ Q, which linarith cannot (that system is rationally satisfiable). Mirrors the refutation half of Lean’s omega. Declines when the hypotheses have an integer model.

pub fn crush(&mut self) -> Result<&mut Self, TacticError>

crush: the grind-style closer. E-matches the in-scope ∀-equality lemmas at the goal’s ground terms, then discharges the goal by certified congruence closure. Proves goals plain auto cannot — e.g. ∀x. f(x)=g(x), a=b, P(g(b)) ⊢ P(f(a)) — and every step is kernel-checked.

pub fn auto(&mut self) -> Result<&mut Self, TacticError>

auto: discharge the focused goal with the backward chainer (the existing automation, hosted as one tactic). Its hypotheses and the premises are the available knowledge base.

pub fn assembled(&self) -> Option<DerivationTree>

Assemble the current proof tree, if every goal is closed (for inspection/debug).

pub fn run(&mut self, t: &Tactic) -> Result<&mut Self, TacticError>

Run a composed Tactic against this state, for fluent chaining with the primitive methods.

pub fn qed(&self) -> Result<VerifiedProof, TacticError>

Finish the proof: every goal must be closed. Assembles the recorded tactic steps into one derivation and runs it through the kernel trust door — the returned VerifiedProof is verified only if the kernel accepts the term.

impl ProofState

pub fn run_script(&mut self, src: &str) -> Result<&mut Self, ScriptError>

Parse and run a proof script against this state. The state is unchanged on a parse error; a tactic that fails mid-run leaves whatever it had committed.

pub fn run_script_with_env( &mut self, src: &str, env: &TacticEnv, ) -> Result<&mut Self, ScriptError>

Parse and run a proof script that may reference USER-DEFINED tactics from env (M).

Trait Implementations

impl Clone for ProofState

fn clone(&self) -> ProofState

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.