Module 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.

Functions

all_goals

t1 <;> t2-style: apply t to EVERY goal currently open (not just the focused one). Each goal is focused in turn; the subgoals t produces for it become the new open set, in original goal order.

assumption

assumption as a tactic value.

auto

auto (the backward chainer) as a tactic value.

cases

cases name (∧/∨/∃ elimination) as a tactic value.

crush

crush as a tactic value.

decide

decide as a tactic value.

exact

exact name as a tactic value.

exists

exists witness (∃I) as a tactic value.

first

first [t1, t2, …]: try each tactic on a speculative copy and commit the first that succeeds; fail only if none apply.

induction

induction (structural induction over Nat) as a tactic value.

induction_over

induction_over (generic structural induction over ind_type) as a tactic value.

intro

intro name as a tactic value.

left

left (∨I) as a tactic value.

omega

omega as a tactic value.

repeat

repeat t: apply t as long as it keeps applying (committing each success), then stop. Always succeeds. Bounded to avoid a non-progressing tactic looping forever.

rewrite

rewrite name (Leibniz substitution by an equality) as a tactic value.

right

right (∨I) as a tactic value.

seq

t1; t2; …: run each tactic in turn; fail (without committing the rest) at the first that does not apply.

simp

simp as a tactic value, its rule set drawn from everything in scope (premises, intro’d hypotheses, cited lemmas) — the script-level default.

split

split (∧I) as a tactic value.

then_all

t1 <;> t2: run t1 on the focused goal, then t2 on every goal it produces.

try_

try t: run t if it applies, otherwise leave the state unchanged. Always succeeds.