Tactics
ImandraX has a unified tactic language that gives you fine-grained control over proof search. Tactics transform proof goals (things to be proved) into simpler subgoals, eventually closing the proof.
For a quick-reference table of all tactics, see the Tactic Reference. For the pattern language used to pick subterms from proof goals, see Subterm Selection.
Using tactics
Attach tactics to any verification goal with [@@by ...]:
theorem my_theorem x y =
some_property x y
[@@by auto]
(* Works with verify too *)
verify (fun x y -> some_property x y) [@@by auto]When no [@@by ...] clause is specified, ImandraX uses a default tactic of unrolling up to a low bound.
Tactical combinators
Tactics are composed using combinators — operators that build complex proof strategies from simple ones.
@> — Sequence
Apply the first tactic, then the second to the resulting single subgoal. The first tactic must produce exactly one subgoal.
[@@by [%use my_lemma x] @> auto]<|> — Alternative
Try the first tactic; if it fails, try the second:
[@@by simplify () <|> auto]@>>| — Map to all subgoals
Apply the same tactic to every subgoal generated by the previous step:
[@@by induction () @>>| auto]@>| — Apply different tactics to different subgoals
Apply a specific tactic to each subgoal by position. The number of tactics in the list must match the number of subgoals exactly.
[@@by induction ()
@>| [
(* base case *) auto;
(* step case *) simplify () @> arith
]]try_ — Try or skip
Apply a tactic; if it fails, do nothing. Equivalent to t <|> skip.
repeat — Repeat a tactic
Apply a tactic to the goal and recursively to all resulting subgoals, until the tactic does nothing.
repeat ?depth:int -> t -> t
| Parameter | Default | Description |
|---|---|---|
~depth:n | 20 | Maximum recursion depth to prevent infinite loops |
par — Parallel subgoal solving
Split a goal into subgoals using the first tactic, then solve each subgoal in parallel using the second.
par : t -> t term -> t
Comprehensive example
This example demonstrates several tactics and combinators working together:
lemma test_8 x y =
x=7 && y=6+1 ==> g x y = 1
[@@by intros
@> [%cases (x=y), (x>7)]
@>| [(expr_simplify
@> [%replace y]
@> esimp
@> [%expand "g"]
@> [%replace x]
@> esimp);
([%skip "hello from subgoal 2"]
@> auto);
(expr_simplify
@> [%replace x]
@> [%replace y]
@> [%expand (g 7 7)]
@> simp)
]
]Automation tactics
auto — The inductive waterfall
ImandraX's flagship automated proof tactic. Runs the full inductive waterfall: conditional rewriting with back-chaining, speculative expansion of recursive functions and symbolic execution, forward-chaining for simplification contexts, subgoaling, congruence closure, tautology detection, destructor elimination, generalization, and automated induction.
Takes into account all active rule classes ([@@rw], [@@fc], [@@elim], [@@gen]).
Takes no parameters.
theorem sort_sorts xs = is_sorted (insert_sort xs)
[@@by auto]The verification workflow
Start by exploring goals with bounded verification (unrolling) to find and eliminate counterexamples — this is extremely fast. Once no counterexamples exist up to a large bound, use [@@by auto] to prove the goal. Most true goals succeed with just [@@by auto]. When they don't, use other tactics to guide specific steps, then let the waterfall handle the rest.
induction — Apply induction
Synthesize an induction scheme for the goal and apply it, producing subgoals (base cases and inductive steps). Does not invoke the full waterfall — combine with other tactics to handle the subgoals.
induction : ?id:identifier -> ?vars:string list -> unit -> t
| Parameter | Description |
|---|---|
~id:[%id f] | Use function f's recursion scheme as the induction scheme |
~vars:["x"; "y"] | Induction on the specified variables |
If neither ~id nor ~vars is given, ImandraX uses heuristic scheme selection.
(* Heuristic induction, then auto on each subgoal *)
[@@by induction () @>>| auto]
(* Use a specific function's induction scheme *)
[@@by induction ~id:[%id my_function] () @>>| auto]
(* Induction on specific variables *)
[@@by induction ~vars:["xs"] () @>>| auto]
(* Different tactics for different subgoals *)
[@@by induction ()
@>| [auto; (* base case *)
simplify () @> arith]] (* step case *)induct — Parameterized waterfall
A parameterized version of auto — runs the full inductive waterfall with explicit control over the induction scheme, variables, and other parameters. Unlike induction (), this runs the complete waterfall, so chaining with auto is redundant.
induct : ?on_fun:identifier -> ?on_vars:string list ->
?otf:bool -> ?max_induct:int ->
?do_not:string list -> unit -> t
| Parameter | Description |
|---|---|
~on_fun:[%id f] | Use function f's recursion scheme for function induction |
~on_vars:["x"; "y"] | Structural induction on specified variables (must be algebraic datatypes) |
~otf:true | Enable on-the-fly induction |
~max_induct:n | Maximum induction depth |
~do_not:["elim"; "gen"] | List of waterfall steps to skip: "elim" (destructor elimination) or "gen" (generalization) |
(* Function induction *)
[@@by induct ~on_fun:[%id some_function] ()]
(* Structural induction on specific variables *)
[@@by induct ~on_vars:["x"; "y"] ()]
(* Skip destructor elimination and generalization *)
[@@by induct ~do_not:["elim"; "gen"] ()]Simplification tactics
simp — Quick simplifier
Quick, simple simplifier. Always returns exactly 1 goal. Takes no parameters.
[@@by simp]simp_all — Quick simplifier on all
Quick simplifier applied to both hypotheses and conclusions. Always returns 1 goal. Takes no parameters.
simplify — Full waterfall simplifier
Apply the full waterfall simplifier with all active rules. Applies conditional rewriting, forward-chaining, and speculative expansion of recursive functions to leverage inductive hypotheses.
simplify : ?backchain_limit:int -> ?rules:identifier list ->
?strict:bool -> ?basis:identifier list -> unit -> t
| Parameter | Description |
|---|---|
~backchain_limit:n | Controls the recursive depth of back-chaining on hypotheses during relief of rewrite rule guards |
~rules:[[%id r1]; [%id r2]] | Restrict to only these rewrite rules during simplification |
~strict:true | When used with ~rules, further restricts to only definitional rules (function definitions) and the explicit rules list |
~basis:[[%id f1]; [%id f2]] | Restrict which function definitions can be expanded. Basis members are not expanded unless explicitly given via rules with strict:true |
[@@by simplify ()]
(* Limit back-chaining depth *)
[@@by simplify ~backchain_limit:3 ()]
(* Restrict to specific rules *)
[@@by simplify ~rules:[[%id rev_len]; [%id len_append]] ()]PPX notation shortcuts:
| Notation | Equivalent to |
|---|---|
[%simp rule1, rule2] | simplify ~rules:[[%id rule1]; [%id rule2]] () |
[%simp_only rule1, rule2] | simplify ~rules:[[%id rule1]; [%id rule2]] ~strict:true () |
(* Simplify with specific additional rules *)
[@@by [%simp rev_len, len_append]]
(* Simplify with ONLY the listed rules (strict mode) *)
[@@by [%simp_only rev_len] @> [%simp_only len_append, k]]ctx_simplify — Contextual simplification
Contextual simplification. Takes no parameters.
esimp / expr_simplify — Expression simplification
Expression-level simplification applied to each hypothesis and conclusion in the goal. Takes no parameters.
[@@by esimp @> auto]normalize — Normalize a term
Normalize a specific term under the hypotheses of the current goal. Applies all active rewrite rules, forward-chaining rules, and expands enabled non-recursive function definitions. Includes speculative expansion of recursive functions to leverage inductive hypotheses, in the same manner as the waterfall simplifier.
If the target term appears in the goal, it's replaced with the normalized form. Otherwise, a hypothesis t = normalized_t is added.
normalize : ?rules:identifier list -> ?strict:bool ->
?basis:identifier list -> ?inline:bool ->
'a term -> t
| Parameter | Description |
|---|---|
~rules:[...] | Restrict which rewrite rules are applied (same as simplify) |
~strict:true | With ~rules, restrict to definitions plus the explicit rules |
~basis:[...] | Restrict which function definitions can be expanded |
~inline:true | Control inlining behavior |
PPX notation: [%normalize t] or [%norm t]
[@@by [%norm square_sum xs] @> arith]Propositional tactics
intros — Introduce hypotheses
Move antecedents of implications into the hypothesis set. Transforms H |- (A && B) ==> C into H, A, B |- C. Takes no parameters.
[@@by intros @> simplify ()]unintros — Move hypotheses back
Inverse of intros. Move specified hypotheses back into the conclusion as an implication.
unintros : int list -> t
unintros [1;3;4] transforms H0, H1, H2, H3, H4, H5, H6, H7 |- C into H0, H2, H5, H6, H7 |- (H1 && H3 && H4) ==> C.
trivial — Close trivial goals
Close goals that are trivially true: false in hypotheses, true in conclusion, or an exact match between a hypothesis and the conclusion. Subsumes exact. Takes no parameters.
[@@by simplify () @> trivial]exact — Close by exact match
Close a goal when it exactly matches a hypothesis. Takes no parameters.
[@@by intros @> exact]tauto — Propositional tautology checker
Complete propositional tautology checker. Implemented as lift_ifs @>>| exact — if-normalization followed by exact matching is a complete decision procedure for propositional tautologies. Fails if the goal is not a tautology. Takes no parameters.
lift_ifs — Lift conditionals
Lift if-then-else expressions to top-level case splits. Performs limited feasibility checking to eliminate subgoals with infeasible branches under the current context. Takes no parameters.
[@@by lift_ifs @> auto]flatten — Disjunctive flattening
Flatten disjunctive structure in the goal. Takes no parameters.
[@@by intros @> flatten @> auto]or_left — Select left disjunct
Transform G |- a || b into G |- a. Takes no parameters.
or_right — Select right disjunct
Transform G |- a || b into G |- b. Takes no parameters.
split_and — Split conjunction
Transform G |- a && b into two subgoals: G |- a and G |- b. Takes no parameters.
Decision procedures
arith — Linear arithmetic
Decision procedure for linear (real and integer) arithmetic. Takes no parameters.
[@@by arith]nonlin — Nonlinear arithmetic
Reasoning with nonlinear arithmetic enabled.
nonlin : unit -> t
[@@by nonlin ()]cc — Congruence closure
Congruence closure reasoning. Takes no parameters.
[@@by cc]qs — Quick solver
Fast, incomplete decision procedure for simple QF_UFDT/LIA/LRA goals. Takes no parameters.
[@@by qs]smolsmt — Small solver
Small, simple solver for QF_UF goals. Takes no parameters.
unroll — Bounded model checking
Bounded model checking via incremental recursive function unrolling.
unroll : ?query_timeout:int -> ?no_asm_query_timeout:int -> int -> t
| Parameter | Description |
|---|---|
n (required) | Number of unrolling rounds |
~query_timeout:ms | Timeout per satisfiability query (milliseconds) |
~no_asm_query_timeout:ms | Timeout for queries without assumptions |
[@@by unroll 100]
[@@by unroll ~query_timeout:5000 50]ground_eval — Ground evaluation
Evaluate concrete (ground) terms. Useful when all variables have been instantiated.
ground_eval : ?max_cache:int -> unit -> t
| Parameter | Description |
|---|---|
~max_cache:n | Maximum cache size for memoization |
Term manipulation tactics
use — Apply a lemma
Instantiate a theorem and add it as a hypothesis to the current goal. The term is the theorem applied to its arguments.
use : bool term -> t
PPX notation: [%use lemma_name arg1 arg2]
(* Add a specific lemma instance as a hypothesis *)
[@@by [%use my_lemma x y] @> auto]
(* Chain multiple lemma applications *)
[@@by [%use lemma1 x]
@> [%use lemma2 y]
@> auto]cases — Case split
Case-split on boolean expressions. Produces k+1 subgoals: one for each case (with the case added as a hypothesis), plus one "negative" subgoal where all cases are false. All terms must be boolean-valued.
cases : bool term list -> t
PPX notation: [%cases expr1, expr2, ...]
(* Split on one condition *)
[@@by [%cases x > 0]
@>| [auto; (* case: x > 0 *)
auto]] (* case: not (x > 0) *)
(* Split on multiple conditions (produces 3 subgoals) *)
[@@by [%cases (x > 0), (y > 0)]
@>| [auto; auto; auto]]subgoal — Introduce a subgoal
Apply the cut rule: assume a term and add its correctness as a subgoal. Produces two subgoals: one where the term has been assumed, and one where it must be proved. The term must be boolean-valued.
subgoal : bool term -> t
PPX notation: [%subgoal expr]
[@@by [%subgoal some_fact x y]
@>| [
(* prove the subgoal *) auto;
(* use it to prove the main goal *) auto
]]expand — Expand a definition
Unfold a function definition. By default, expands the first occurrence.
expand : ?index:int -> ?all:bool -> string -> t
| Parameter | Description |
|---|---|
~index:n | Expand the n-th occurrence (0-indexed) instead of the first |
~all:true | Expand all current occurrences |
Instances introduced through expansion are not recursively expanded.
PPX notation: [%expand "name"] for function names, [%expand (f x)] for specific applications (term is automatically quoted).
[@@by [%expand "square"] @> nonlin ()]
(* Expand a specific application *)
[@@by [%expand (g 7 7)] @> simp]
(* Expand all occurrences *)
[@@by expand ~all:true "foo" @> auto]
(* Expand the third occurrence *)
[@@by expand ~index:2 "foo" @> auto]replace — Substitute
Use an equality hypothesis x = t to replace x by t throughout the goal.
replace : 'a term -> t
PPX notation: [%replace x]
[@@by intros @> [%replace x] @> auto]generalize — Generalize a term
Replace a term with a fresh Skolem variable of the appropriate type throughout the goal. The name must not conflict with existing terms in the goal and must follow IML identifier rules.
generalize : 'a term -> string -> t
[@@by generalize (quote_term (f x)) "z" @> auto]swap — Swap across sequent line
Move a literal (hypothesis or conclusion) across the sequent line (|-), negating it.
swap : int -> t
| Index | Behavior |
|---|---|
i >= 0 | Hypothesis i is negated and moved to the conclusions |
i < 0 | Conclusion abs(i+1) is negated and moved to the hypotheses |
[@@by swap (-1) @> auto]drop — Remove a literal
Remove a hypothesis or conclusion. Uses the same index addressing scheme as swap.
drop : int -> t
name — Name a hypothesis
Give a name to an unnamed hypothesis (useful for subterm selection with named hypotheses).
name : int -> string -> t
rename — Rename a hypothesis
Rename a named hypothesis.
rename : string -> string -> t
Utility tactics
skip — No-op
A no-op — the goal remains unchanged. Useful as a placeholder in tactic lists.
PPX notation: [%skip] or [%skip "message"] (the message variant prints to the tactic trace, useful for debugging).
quickcheck — Random testing
Try random instances on the goal, possibly refuting it. If no counterexample is found, returns the same goal unchanged.
quickcheck : ?seed:int -> ?num:int -> unit -> t
| Parameter | Description |
|---|---|
~seed:n | Random seed for reproducibility |
~num:n | Number of random instances to try |
[@@by quickcheck ~num:1000 ()]enumerate — Enumerate finite types
Enumerate all values of finite-type variables, turning the goal into a finite number of ground instances.
enumerate : string list -> t
The argument is a list of variable names whose types are finite (e.g., variant types with no recursive constructors).
[@@by enumerate ["color"; "direction"] @> auto]Rule classes
When a theorem is proved, you can install it as a rule that directs how it's used by auto and simplify in future proofs.
[@@rw] — Rewrite rule
The theorem is used as a left-to-right rewrite rule during simplification:
theorem append_nil xs = xs @ [] = xs
[@@by auto] [@@rw]
(* Now `xs @ []` is automatically rewritten to `xs` *)[@@fc] — Forward-chaining rule
The theorem is used to derive new facts from existing hypotheses. The [@trigger] annotation marks which term pattern activates the rule:
theorem length_non_neg xs =
(List.length xs [@trigger]) >= 0
[@@by auto] [@@fc][@@elim] — Elimination rule
The theorem is used for destructor elimination in the waterfall:
lemma hd_tl_elim x =
x <> [] ==> List.hd x :: List.tl x = x
[@@by auto] [@@elim][@@gen] — Generalization rule
The theorem constrains generalizations during the waterfall's generalization step:
lemma square_gen n =
(n * n [@trigger]) >= 0
[@@by auto] [@@gen][@@perm] / [@@permutative] — Permutative rewrite rule
A rewrite rule that only fires when the result is lexicographically smaller than the input, preventing infinite rewriting loops:
lemma add_commutes x y =
x + y = y + x
[@@by auto] [@@rw] [@@perm]A complete example
Here's a proof from the majority voting algorithm example, showing tactics in action:
lemma majority_key e c i xs =
i >= 0
&& (i + List.length xs)
< 2 * ((if c = (Some e) then i else 0) + num_occurs e xs)
==>
majority_aux c i xs = Some e
[@@by auto]
lemma majority_is_correct c xs =
is_majority c xs
==>
majority xs = Some c
[@@by [%use majority_key c (Some c) 0 xs] @> auto]
lemma majority_unique c d xs =
is_majority c xs && is_majority d xs
==>
c = d
[@@by [%use majority_is_correct c xs]
@> [%use majority_is_correct d xs]
@> auto]The last proof works by using two instances of the correctness lemma — once for c and once for d — then letting auto derive that they must be equal.