Tactic Catalogue

Tactics are the verbs of Verum's proof DSL. A tactic transforms a proof state — zero or more open goals, each with a context of hypotheses — into a new proof state. A proof by T succeeds when T drives the proof state to zero goals.

This page is the reference to every built-in tactic. For the DSL syntax, see Proof DSL.

Grammar:

tactic_expr  = tactic_name , [ '(' , [ argument_list ] , ')' ]
             | tactic_expr , ';' , tactic_expr
             | '(' , tactic_expr , ')'
             | 'try' , '{' , tactic_expr , '}' , [ 'else' , '{' , tactic_expr , '}' ]
             | 'repeat' , [ '(' , integer_lit , ')' ] , '{' , tactic_expr , '}'
             | 'first' , '{' , tactic_expr , { ';' , tactic_expr } , '}'
             | 'all_goals' , '{' , tactic_expr , '}'
             | 'focus' , '(' , integer_lit , ')' , '{' , tactic_expr , '}' ;

tactic_name  = 'auto' | 'simp' | 'ring' | 'field' | 'omega' | 'blast' | 'smt'
             | 'trivial' | 'assumption' | 'contradiction' | 'induction' | 'cases'
             | 'rewrite' | 'unfold' | 'apply' | 'exact' | 'intro' | 'intros'
             | 'cubical' | 'category_simp' | 'category_law' | 'descent_check'
             | identifier ;

Trivial tactics

`trivial`

Solves goals that are definitionally true: true, 0 <= 0, forall x: Unit. x == (), and simple reflexive equalities.

theorem t_zero() ensures 0 == 0 { proof by trivial }

`assumption`

Closes a goal if it is exactly one of the current hypotheses.

theorem h(p: Bool) requires p ensures p { proof by assumption }

`contradiction`

Closes any goal if the hypotheses include a logical contradiction (e.g. h: False, or a > b together with a <= b).

theorem ex_falso(p: Bool, h: p, nh: !p) ensures forall x: Int. x == x
{
    proof by contradiction
}

Introduction tactics

`intro`

Introduces one variable or hypothesis from the goal:

forall x: T. P(x) → P(x) with x: T in context.
P -> Q → goal becomes Q with h: P in context.

// Goal: forall n: Int. n == n
proof {
    intro n;
    // Now: n: Int, goal: n == n
    exact Eq.refl(n)
}

`intros`

Repeats intro until the goal is no longer a forall or an implication. A common opening move.

`exact(term)`

Provides the exact proof term — used when the caller has a witness.

theorem refl<T>(x: T) -> Path<T>(x, x)
{
    proof by exact(path_refl(x))
}

`apply(lemma)`

Applies a lemma or hypothesis. Matches the goal against the lemma's conclusion; remaining premises become new subgoals.

// Goal: 0 <= n * n
proof {
    apply square_nonneg;    // square_nonneg: forall n. 0 <= n * n
}

Simplification tactics

`simp`

Rewrite-based simplifier. Applies a curated lemma set — simp lemmas — plus user-marked rewrites (@simp) until a fixed point is reached.

proof by simp

simp is the first thing to try for algebraic identities, trivial containers, and standard-library lemmas.

Parameterised form: simp(on = [lemma1, lemma2]) restricts to a lemma set; simp(off = [lemma3]) excludes specific lemmas from the default set.

`unfold(name)`

Expands a definition one step. Useful when simp refuses because of opacity:

proof {
    unfold is_sorted;          // expand the predicate
    simp;
    omega
}

`rewrite(eq)`

Rewrites the goal left-to-right by the given equality. Right-to-left is rewrite(eq, ltr = false).

proof {
    rewrite add_comm(a, b);    // replaces `a + b` with `b + a`
    simp
}

Arithmetic tactics

`omega`

Decision procedure for Presburger arithmetic — linear integer arithmetic with +, −, ·-by-constant, <, ≤, =, ≠, and quantifiers.

Solves:

ensures 2 * (a + b) == 2 * a + 2 * b
ensures forall i in 0..n. 0 <= i < n

Does not solve non-linear goals (a * b == b * a may fail, a * a >= 0 fails). Use ring for those.

`ring`

Decides equalities in commutative rings — polynomial identities in Int, Float, Rational, and user-defined rings.

proof by ring          // for (a + b)² = a² + 2ab + b²

`field`

Like ring but over fields — allows division by nonzero. Requires hypotheses that denominators are nonzero.

theorem div_dist(a: Float, b: Float, c: Float, h: c != 0.0)
    ensures (a + b) / c == a/c + b/c
{
    proof by field
}

Structural tactics

`induction(target)`

Structural induction over a target: a list, a nat, a variant type. Generates one subgoal per constructor.

theorem sum_nonneg(xs: List<Int>)
    requires forall x in xs. x >= 0
    ensures  xs.sum() >= 0
{
    proof by induction xs
}

Equivalent explicit form:

proof {
    induction xs;
    // Generates:
    //  goal 1: when xs = Nil
    //  goal 2: when xs = Cons(h, t), with IH: t.sum() >= 0
    all_goals { simp; omega }
}

`cases(target)`

Case-splits on a target without recursion — one subgoal per constructor, no induction hypothesis.

match x {
    Maybe.Some(v) => ...,
    Maybe.None    => ...,
}
// Proof side: `cases x` splits into two goals.

`blast`

Heavy structural search — tries intros, cases, simp, assumption, and a bounded set of lemma applications. Best when auto is not strong enough but the goal is still propositional or simply quantified.

Automation

`auto`

The workhorse. Composes intros, simp, assumption, omega, and a bounded search over in-scope lemmas. The default when no tactic is specified by an @verify(formal) function.

Parameterised form:

auto(depth = 8, lemmas = [my_lemma, other])

Settings:

depth: bound on the search depth. Default 4.
lemmas: lemmas in addition to the default in-scope set.
timeout: milliseconds. Default 500.

`smt`

Hands the goal to the SMT backend — the SMT backend, or a portfolio, selected by the router. See verification/smt-routing.

proof by smt

Parameterised form:

smt(backend = "z3",      // force backend
    logic   = "QF_LIA",  // force SMT-LIB logic
    timeout = 10000)     // milliseconds

Useful when you know the goal fits a specific theory; otherwise let the router pick.

Cubical type theory

`cubical`

Solves equalities by cubical reasoning: transport, hcomp, and coherence laws in cubical type theory. Required for proofs involving Path<T>(a, b) paths.

See verification/cubical-hott.

theorem loop_equiv<T>(p: Path<T>(a, b))
    ensures transport(p, transport(p.inv(), x)) == x
{
    proof by cubical
}

Category theory

`category_simp`

Simplifies commutative diagrams and categorical identities. Knows id ; f = f, f ; (g ; h) = (f ; g) ; h, functor laws, monad laws, adjunction laws.

theorem unit_law<F: Monad>(m: F<T>)
    ensures m.bind(F.pure) == m
{
    proof by category_simp
}

`category_law(name)`

Applies a specific categorical law by name (e.g., associativity, yoneda, kan_extension).

`descent_check`

Verifies that a construction over a category of covers coheres — used in sheaf-theoretic and scheme-theoretic verification contexts.

Combinators

`;` (sequencing)

Runs tactics in order. Common idiom:

proof {
    intros;
    simp;
    omega
}

`try { t } else { t2 }`

If t fails (leaves goals unchanged or errors), run t2 instead.

proof by try { auto } else { smt }

`try { t }`

Short for try { t } else { trivial } — never fails, even if t did nothing.

`repeat { t }` and `repeat(n) { t }`

Apply t until it stops making progress. With a bound n, at most n times.

proof by repeat { simp; rewrite some_rule }

`first { t1 ; t2 ; t3 }`

Try each t_i in order; the first one that succeeds wins. If all fail, first fails.

proof by first {
    omega ;         // cheap, often works
    ring ;
    smt             // heavy last resort
}

`all_goals { t }`

Apply t to every remaining subgoal. After an induction that spawns several cases, use all_goals to close them uniformly:

proof {
    induction xs;
    all_goals { simp; omega }
}

`focus(i) { t }`

Apply t only to the i-th subgoal (1-based). Useful when different subgoals need different approaches.

proof {
    induction xs;
    focus(1) { simp };          // base case
    focus(2) { apply IH; ring } // step case
}

User-defined tactics

tactic name(params) { body } declares a tactic that composes the above. Parameters and body use the tactic grammar:

tactic arith_full(x: Int) {
    try { simp };
    try { unfold definition_of_foo };
    first { omega ; ring ; smt }
}

theorem use_it(a: Int, b: Int)
    ensures 2 * (a + b) == 2 * a + 2 * b
{
    proof by arith_full(a + b)
}

Cheat-sheet: when to reach for which

Goal kind	First try	Fallback
Trivial equality	`trivial`	—
`H ⊢ H`	`assumption`	—
Linear integer arithmetic	`omega`	`smt`
Polynomial identity	`ring`	`field`, `smt`
List, nat, ADT structural	`induction`	`blast`, `auto`
One-shot case split	`cases`	`blast`
Rewrite by a known lemma	`rewrite`	`simp(on = [...])`
Expand a named definition	`unfold`	`simp`
Unknown — general SMT theory	`smt`	`auto(depth = 12)`
Cubical path / HoTT	`cubical`	—
Category / functor / monad law	`category_simp`	`category_law`
"I have a witness"	`exact`	`apply`
"Eliminate universals and implications"	`intros`	`auto`
Don't know — just let the engine try	`auto`	`smt`, `blast`

Trivial tactics​

trivial​

assumption​

contradiction​

Introduction tactics​

intro​

intros​

exact(term)​

apply(lemma)​

Simplification tactics​

simp​

unfold(name)​

rewrite(eq)​

Arithmetic tactics​

omega​

ring​

field​

Structural tactics​

induction(target)​

cases(target)​

blast​

Automation​

auto​

smt​

Cubical type theory​

cubical​

Category theory​

category_simp​

category_law(name)​

descent_check​

Combinators​

; (sequencing)​

try { t } else { t2 }​

try { t }​

repeat { t } and repeat(n) { t }​

first { t1 ; t2 ; t3 }​

all_goals { t }​

focus(i) { t }​

User-defined tactics​

Cheat-sheet: when to reach for which​

See also​