Skip to main content

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 , [ type_args ] , [ '(' , [ argument_list ] , ')' ]
             | tactic_expr , ';' , tactic_expr
             | '(' , tactic_expr , ')'
             | 'try' , '{' , tactic_expr , '}' , [ 'else' , '{' , tactic_expr , '}' ]
             | 'repeat' , [ '(' , integer_lit , ')' ] , '{' , tactic_expr , '}'
             | 'first' , '{' , tactic_expr , { ';' , 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)
    given h: p
    given 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)
    given 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.

auto takes no parameters — tactic auto() { auto }. There is no depth, lemmas or timeout setting to pass, and no named-argument call form in the language at all: arg_list in grammar/verum.ebnf is a list of expressions, so auto(depth = 8) parses depth = 8 as an assignment and fails with unbound variable: depth.

The library's way of varying a tactic is a separate tactic, not an options bag — simp() beside simp_with(lemmas), intro() beside intro_as(name), destruct(var) beside destruct_as(...). To bring extra lemmas into a search, name them:

proof by { simp_with([my_lemma, other]); auto }

smt​

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

proof by smt

smt takes no parameters either — tactic smt() { smt }. Backend, logic and timeout are the router's decision, not a call argument; see verification/smt-routing for what steers it.

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​

caution
A tactic body is parsed but not checked

Name resolution and type checking do not enter a tactic body. The same two lines are refused inside fn and accepted inside tactic:

tactic probe(goal: Prop) {
    let x: Int = deliberately_unbound_probe(7);   // accepted, rc=0
    let best: Int = "not an int";                 // accepted, rc=0
}

fn probe() -> Int {
    let best: Int = "not an int";                 // error<E400>, rc=101
}

Only syntactic damage is caught — the parser does enter the body. So a clean verum check over a file containing a tactic says nothing about what the tactic's body refers to or whether its types line up. Read the bodies on this page as illustrations of the shape, and expect no compiler help while writing your own.

tactic name<generics>(params) { body } declares a tactic that composes built-in and user-defined tactics. Tactics are polymorphic, typed, and structured — they can take typed parameters with defaults, open type variables, and build their proof search with let, match, if, and fail in addition to the usual combinators.

Minimal form​

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)
}

Generic tactics​

Tactics can be parameterised by types — essential for writing once, applying across every model of a theory:

tactic category_law<C>() {
    repeat {
        first {
            rewrite(C.assoc);
            rewrite(C.id_left);
            rewrite(C.id_right);
        }
    };
    simp
}

tactic functor_law<F>() {
    repeat {
        first {
            rewrite(F.map_id);
            rewrite(F.map_compose);
        }
    };
    category_law<F>()
}

Type arguments are passed with angle brackets at call sites: category_law<C>(), functor_law<F.Source>().

Typed parameters​

Parameters accept both the classical kind forms (Expr, Type, Tactic, Hypothesis, Int, Prop) and any concrete type. An optional default value is supplied with = expr:

tactic oracle(goal: Prop, confidence: Float = 0.9) {
    let candidates: Giry<Prop> = @llm_oracle(goal);
    let best: Maybe<Prop> = sample_above(candidates, confidence);
    match best {
        Maybe.Some(proof_term) => {
            apply(proof_term);
            try { smt } else {
                fail("oracle candidate rejected by SMT backend")
            }
        },
        Maybe.None => fail("oracle confidence below threshold"),
    }
}
warning
@llm_oracle is not a meta-function the compiler knows

The name is declared nowhere in the compiler, so the call in the block above draws

warning<E0410>: unknown meta-function `@llm_oracle`

and the expression takes the type Unit, which will not unify with Giry<Prop> — so the example stops at the type check. The standard library calls it too, in core/math/tactics.vr, behind a @cfg(feature = "llm_oracle") gate that is off by default. Read the block as the intended shape of an oracle tactic; the parameter-kind table below is unaffected.

Parameter kindMeaning
ExprAny expression — bound as-is, substituted into the body
TypeA type expression
TacticA higher-order tactic (a tactic that takes tactics)
HypothesisA simple identifier referring to an in-scope hypothesis
IntAn integer literal
PropA first-class proposition
any typeArbitrary typed parameter — Float, List<T>, Maybe<U>, …

Structured tactic bodies​

Tactic bodies are not only sequences of combinators — they can thread local state and branch on values:

  • let name: T = expr; — local binding, analogous to Lean's monadic let x ← …. The bound value is available to the rest of the tactic sequence.
  • match scrutinee { P => tactic, … } — pattern-directed branching; each arm is a full tactic expression.
  • if cond { t1 } else { t2 } — conditional tactic execution.
  • fail("reason") — abort this proof branch with a diagnostic; feeds into enclosing try/first combinators for recovery.

Grammar​

tactic_decl =
    'tactic' , identifier , [ generics ] ,
    '(' , [ tactic_param_list ] , ')' ,
    [ where_clause ] , tactic_body ;

tactic_param  = identifier , ':' , tactic_param_type ,
                [ '=' , expression ] ;

tactic_param_type = 'Expr' | 'Type' | 'Tactic' | 'Hypothesis' | 'Int'
                  | 'Prop' | type_expr ;

tactic_body   = tactic_expr | '{' , { tactic_stmt } , '}' ;

tactic_stmt =
      'let'   , identifier , [ ':' , type_expr ] , '=' , expression , ';'
    | 'if'    , expression , '{' , tactic_expr , '}' ,
                [ 'else' , ( 'if' , expression , '{' , tactic_expr , '}'
                           | '{' , tactic_expr , '}' ) ]
    | 'match' , expression , '{' ,
                match_arm , { ( ',' | ';' ) , match_arm } , [ ',' | ';' ] , '}'
    | 'fail'  , '(' , expression , ')'
    | tactic_expr , [ ';' ] ;

Cheat-sheet: when to reach for which​

Goal kindFirst tryFallback
Trivial equalitytrivial—
H ⊢ Hassumption—
Linear integer arithmeticomegasmt
Polynomial identityringfield, smt
List, nat, ADT structuralinductionblast, auto
One-shot case splitcasesblast
Rewrite by a known lemmarewritesimp(on = [...])
Expand a named definitionunfoldsimp
Unknown — general SMT theorysmtauto(depth = 12)
Cubical path / HoTTcubical—
Category / functor / monad lawcategory_simpcategory_law
"I have a witness"exactapply
"Eliminate universals and implications"introsauto
Don't know — just let the engine tryautosmt, blast

See also​