Tactic Reference

Complete reference for ImandraX's tactic language. For an introductory guide with worked examples, see Tactics.

Tactical combinators

Tactics are composed using combinators that build complex proof strategies from simple ones.

@> — Sequence

Chain two tactics. The first must produce exactly one subgoal, which the second tactic then solves.

[@@by intros @> auto]

@>| — Branch to subgoals

Apply a list of tactics to subgoals by position. The first tactic must produce exactly n subgoals, and the list must contain exactly n tactics.

[@@by induction ()
   @>| [auto;                     (* base case *)
        simplify () @> arith]]    (* step case *)

@>>| — Map to all subgoals

Apply the same tactic to every subgoal produced by the first tactic, regardless of how many there are.

[@@by induction () @>>| auto]

<|> — Alternative

Try the first tactic; if it fails, try the second.

[@@by simplify () <|> auto]

try_

Apply a tactic; if it fails, do nothing (equivalent to t <|> skip).

repeat

Apply a tactic repeatedly to the goal and its subgoals, up to a maximum depth (default 20).

Signature: ?depth:int -> t -> t

par

Split a goal into subgoals using the first tactic, then solve each subgoal in parallel using the second tactic.

Signature: t -> t term -> t

Automation tactics

auto

ImandraX's flagship automated proof tactic. Runs the full inductive waterfall: conditional rewriting with back-chaining, forward-chaining, symbolic execution, speculative expansion of recursive functions, destructor elimination, generalization, and automated induction. Takes into account all active rule classes ([@@rw], [@@fc], [@@elim], [@@gen]).

Once bounded verification confirms no counterexamples exist, most true goals succeed with just [@@by auto].

theorem sort_sorts xs = is_sorted (insert_sort xs)
[@@by auto]

induct

Parameterized version of auto — runs the full inductive waterfall with explicit control over induction scheme and variables. Unlike induction (), this runs the complete waterfall, so chaining with auto is redundant.

Signature: ?on_fun:identifier -> ?on_vars:string list -> ?otf:bool -> ?max_induct:int -> ?do_not:string list -> unit -> t

(* Function induction *)
[@@by induct ~on_fun:[%id my_function] ()]
 
(* Structural induction on specific variables *)
[@@by induct ~on_vars:["x"; "y"] ()]

induction

Apply induction to produce subgoals (base cases and inductive steps), then stop. Does not invoke the full waterfall — combine with other tactics to handle subgoals.

Signature: ?id:identifier -> ?vars:string list -> unit -> t

[@@by induction () @>>| auto]
[@@by induction ~id:[%id my_function] () @>>| auto]

Simplification tactics

simp

Quick, simple simplifier. Always returns exactly 1 goal.

[@@by simp]

simp_all

Quick simplifier applied to both hypotheses and conclusions. Always returns 1 goal.

simplify

Full waterfall simplifier with all active rules. Applies conditional rewriting, forward-chaining, and speculative expansion of recursive functions.

Signature: ?backchain_limit:int -> ?rules:identifier list -> ?strict:bool -> ?basis:identifier list -> unit -> t

[@@by simplify ()]

PPX notation:

• [%simp rule1, rule2] — simplify with specific additional rules
• [%simp_only rule1, rule2] — simplify with only the listed rules (strict mode)

[@@by [%simp rev_len, len_append]]
[@@by [%simp_only rev_len] @> [%simp_only len_append, k]]

ctx_simplify

Contextual simplification.

esimp / expr_simplify

Expression-level simplification applied to each hypothesis and conclusion.

[@@by esimp @> auto]

Propositional tactics

intros

Move antecedents of implications into the hypothesis set. Transforms H |- (A && B) ==> C into H, A, B |- C.

[@@by intros @> auto]

trivial

Close goals that are trivially true: false in hypotheses, true in conclusion, or an exact match between a hypothesis and the conclusion. Subsumes exact.

exact

Close a goal when it exactly matches a hypothesis.

[@@by intros @> exact]

tauto

Propositional tautology checker. Implemented as lift_ifs @>>| exact — if-normalization is a complete decision procedure for propositional tautologies.

lift_ifs

Lift if-then-else expressions to top-level case splits. Performs limited feasibility checking to eliminate infeasible branches.

[@@by lift_ifs @> auto]

flatten

Disjunctive flattening.

[@@by intros @> flatten @> auto]

or_left

Transform G |- a || b into G |- a.

or_right

Transform G |- a || b into G |- b.

split_and

Transform G |- a && b into two subgoals: G |- a and G |- b.

Decision procedures

arith

Decision procedure for linear (real and integer) arithmetic.

[@@by arith]

nonlin

Reasoning with nonlinear arithmetic enabled.

Signature: unit -> t

[@@by nonlin ()]

cc

Congruence closure reasoning.

[@@by cc]

qs

Fast, incomplete decision procedure for simple QF_UFDT/LIA/LRA goals.

[@@by qs]

smolsmt

Small, simple solver for QF_UF goals.

unroll

Bounded model checking. Incrementally unfolds recursive definitions and checks satisfiability modulo ground decision procedures.

Signature: int -> t

[@@by unroll 100]

ground_eval

Ground evaluation — evaluate concrete terms.

Signature: ?max_cache:int -> unit -> t

Term manipulation tactics

use

Instantiate a theorem and add it as a hypothesis to the current goal.

Signature: bool term -> t

PPX notation: [%use lemma_name arg1 arg2]

[@@by [%use my_lemma x y] @> auto]

cases

Case-split on boolean expressions. Produces k+1 subgoals: one for each case (with the case as a hypothesis), plus one "negative" subgoal where all cases are false.

Signature: bool term list -> t

PPX notation: [%cases expr1, expr2, ...]

[@@by [%cases x > 0]
   @>| [auto;    (* case: x > 0 *)
        auto]]   (* case: not (x > 0) *)

subgoal

Introduce an intermediate claim (cut rule). Produces two subgoals: one where the claim must be proved, and one where it's available as a hypothesis.

Signature: bool term -> t

PPX notation: [%subgoal expr]

[@@by [%subgoal some_fact x y]
   @>| [auto;    (* prove the subgoal *)
        auto]]   (* use it to prove the main goal *)

expand

Unfold a function definition. Expands the first occurrence by default.

Signature: ?index:int -> ?all:bool -> string -> t

PPX notation: [%expand "name"] or [%expand (f x)]

[@@by [%expand "square"] @> nonlin ()]
[@@by [%expand (g 7 7)] @> simp]

Instances introduced by expansion are not recursively expanded.

replace

Use an equality hypothesis x = t to substitute x with t throughout the goal.

Signature: 'a term -> t

PPX notation: [%replace x]

[@@by intros @> [%replace x] @> auto]

normalize

Normalize a term under the current hypotheses. Applies all active rewrite rules, forward-chaining rules, and expands enabled non-recursive function definitions. If the term appears in the goal, it's replaced with the normalized form; otherwise a hypothesis t = normalized_t is added.

Signature: ?rules:identifier list -> ?strict:bool -> ?basis:identifier list -> ?inline:bool -> 'a term -> t

PPX notation: [%normalize t] or [%norm t]

[@@by [%norm square_sum xs] @> arith]

generalize

Replace a term with a fresh Skolem variable of the appropriate type throughout the goal.

Signature: 'a term -> string -> t

swap

Swap a literal across the sequent line (|-), negating it. Positive indices address hypotheses (moving them to conclusions); negative indices address conclusions (moving them to hypotheses).

Signature: int -> t

[@@by swap (-1) @> auto]

drop

Remove a hypothesis or conclusion. Uses the same index addressing scheme as swap.

Signature: int -> t

unintros

Inverse of intros — move specified hypotheses back into the conclusion as an implication.

Signature: int list -> t

name

Name an unnamed hypothesis.

Signature: int -> string -> t

rename

Rename a named hypothesis.

Signature: string -> string -> t

Utility tactics

skip

No-op — the goal remains unchanged. Useful as a placeholder in tactic lists.

PPX notation: [%skip] or [%skip "message"]

quickcheck

Try random instances to refute the goal. Returns the same goal if no counterexample is found.

Signature: ?seed:int -> ?num:int -> unit -> t

enumerate

Enumerate all values of finite-type variables.

Signature: string list -> t

Rule class annotations

When a theorem is proved, you can install it as a rule that directs how it's used in future proofs by auto and simplify.

theorem append_nil xs = xs @ [] = xs
[@@by auto] [@@rw]
 
theorem length_non_neg xs =
  (List.length xs [@trigger]) >= 0
[@@by auto] [@@fc]

Trigger annotations

Other annotations

Subterm selection

Some tactics that take a term argument (like use, cases, expand, normalize) support subterm selection — a pattern language for picking subterms from the current goal instead of spelling them out manually. This is especially useful when terms are complex or involve destructor expressions that can't easily be written directly.

Syntax

Subterm selections are written as [? combinators ] and can be used anywhere a term argument is expected:

theorem thm2 a b c =
  a * b + c = 0
[@@by [%use thm1 [? at (_ * _) in concl] ]]

Here, [? at (_ * _) in concl] selects the first subterm matching the pattern _ * _ in the conclusion — in this case, a * b.

Combinators

The selection language consists of two kinds of combinators: shape matching (what to pick) and focussing (where to look).

Focus expressions

The in combinator accepts these focus expressions:

If no in focus is specified, the default is in concl.

How combinators compose

Combinators describe a function composition — they are applied in reverse order (right to left). Each combinator maintains an internal iterator, and all are advanced in composition order until a subterm is found that all combinators agree on.

The algorithm is inspired by Gonthier and Tassi and Noschinski and Traut.

Examples

Given the goal:

theorem thm2 (a : int) (b : int) (c : int) (d : int) =
  ((a + b) * c) + d = g (x + 1)
[@@by [%use thm1 ...] @> ...]

Subterm selection with named hypotheses

When hypotheses are named, you can select subterms from a specific hypothesis:

theorem thm3 (x : int) (y : int) =
  f x > 0 [@name xgt0]
  && f y > 0 [@name ygt0]
  ==> g x y > 0
[@@by intros
   @> [%use helper [? at (f (_)) in xgt0]]
   @> auto]

Binding subterm selections

Subterm selections can be bound to variables and reused:

[@@by
  let trm = [? at ((a : int) + _) in (_ + (_ : int))] in
  [%use thm_int trm] @> auto]