Struct GoalState 

pub struct GoalState { /* private fields */ }

A proof under construction: the statement, the metavariables standing for its unproved parts, and the goals still open.

Implementations

impl GoalState

pub fn new(ctx: &Context, statement: &Term) -> Result<GoalState, TacticError>

A proof of statement in ctx, one goal open. statement must be a type.

pub fn goals(&self) -> Vec<Goal>

The open goals, the focused one first.

pub fn read(&self, term: &Term) -> Term

term as the focused goal reads it: a global named like one of its hypotheses is that hypothesis.

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

The finished proof: the statement’s proof term with every goal’s solution in place, closed and checked by the kernel against the statement.

pub fn step(&mut self, step: &TacticStep) -> Result<(), TacticError>

Run one step; a step that does not apply leaves the state as it found it, a multi-name intro included.

pub fn run(&mut self, script: &[TacticStep]) -> Result<(), ScriptError>

Run a script, step by step; the first step that does not apply stops it, the state left as that step found it.

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

intro x: a goal Π(y : A). B becomes B[y := x] with the hypothesis x : A.

pub fn exact(&mut self, term: &Term) -> Result<(), TacticError>

exact e: close the goal with e, whose holes and implicit arguments unification fills.

pub fn apply(&mut self, term: &Term) -> Result<(), TacticError>

apply f: unify f’s conclusion with the goal; each premise of f unification does not determine becomes a goal, in order.

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

assumption: close the goal with a hypothesis whose type it is.

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

exfalso: prove the goal from False, by False’s elimination with no case.

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

constructor: apply the first constructor of the goal’s family that applies.

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

left: apply the first of the two constructors of the goal’s family.

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

right: apply the second of the two constructors of the goal’s family.

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

exists w: the goal’s family has one constructor, applied to the family’s parameters and the witness w; its remaining premises are the goals (Ex A P leaves P w).

pub fn have(&mut self, name: &str, fact: &Term) -> Result<(), TacticError>

have h : A: prove A first, then the goal with the hypothesis h : A.

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

rfl: close an equation whose two sides convert.

pub fn change(&mut self, target: &Term) -> Result<(), TacticError>

change T: replace the goal by a target it converts with.

pub fn rewrite( &mut self, eq_proof: &Term, reverse: bool, ) -> Result<(), TacticError>

rw [h] (reverse: rw [← h]): with h : Eq A l r, replace every occurrence of l (of r) in the goal by r (by l), occurrences under binders included, and close the goal by transport along h.

pub fn induction( &mut self, var: &str, names: &[&[&str]], ) -> Result<(), TacticError>

induction x with | c₁ a… | c₂ b… …: x : I p̄ ī, a hypothesis whose indices are distinct hypotheses, is eliminated by I_rec. The motive abstracts x, its indices and every hypothesis that depends on them (reintroduced in each case under its own name); each constructor’s case is a goal whose fields and induction hypotheses are named by names[i], in order, the rest named fresh.

pub fn cases(&mut self, var: &str, names: &[&[&str]]) -> Result<(), TacticError>

cases x with | c₁ a… | …: x : I p̄ ī is eliminated by an indexed match, which owes a case only for the constructors ī allows (type_checker::constructors_the_indices_allow): cases h with h : Eq Nat (Succ a) Zero closes the goal with no case at all, as Lean’s noConfusion does. With indices that are hypotheses of their own, the motive abstracts them, x, and every hypothesis depending on them, as GoalState::induction does, without induction hypotheses. An index that is not a hypothesis, at a family a constructor can still produce it in, needs equations between indices and is refused.

pub fn subst(&mut self, h: &str) -> Result<(), TacticError>

subst h: h : Eq A a b where b (or else a) is a hypothesis that the other side and A do not mention; it is replaced by the other side everywhere and leaves the context with h.

pub fn injection(&mut self, h: &str, names: &[&str]) -> Result<(), TacticError>

injection h as e₁ …: h : Eq T (C ā) (C b̄) gives eᵢ : Eq Tᵢ aᵢ bᵢ for each field of C whose type no earlier field decides; h : Eq T (C ā) (D b̄) with C ≠ D closes the goal. Each fact is proved by transport along h into a predicate that matches on the value, the construction Lean’s noConfusion packages.

pub fn calc(&mut self, steps: &[(Term, Term)]) -> Result<(), TacticError>

calc [R₁ := p₁, R₂ := p₂, …]: a chain of equations Eq A l r, a step’s left side _ read as the previous step’s right side, joined by transitivity into a proof that the first left side equals the last right side, which closes the goal. A step proved by _ is left as a goal.

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

cc: close an equation the hypotheses entail by congruence: their equations, read in either direction and chained, and the rule that equal functions applied to equal arguments are equal. The proof is built from the hypotheses by symmetry, transitivity and congruence, each a match on an equation’s proof, so nothing is trusted: qed checks the chain.

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

decide: a goal P with a Decidable P instance the kernel evaluates to isTrue. The proof is of_decide_eq_true P inst (refl Bool true), which the kernel accepts by computing decide P inst to true: a proved bridge and conversion, nothing assumed.

pub fn simp(&mut self, lemmas: &[Term]) -> Result<(), TacticError>

simp [l₁ …]: rewrite the goal by each lemma (Π x̄. Eq A l r: a hypothesis, a constant or a term), left to right, wherever an instance of l stands outside every binder of the goal, until none applies, then close the goal by rfl when its sides agree. With no lemma it rewrites by the context’s @[simp] theorems. Each rewrite is a rewrite along the lemma at the matched instance, so the proof is the chain of their transports with each lemma cited by name, and nothing is trusted. A run that rewrites nothing is refused, as is one still rewriting after SIMP_STEPS rewrites; either leaves the goal as it found it.

pub fn refine(&mut self, term: &Term) -> Result<(), TacticError>

refine e: e with holes (_), elaborated against the goal; every hole unification leaves open becomes a goal, in the order the holes appear, with the binders around it as hypotheses.

Trait Implementations

impl Clone for GoalState

fn clone(&self) -> GoalState

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for GoalState

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.