Verification Tactics

ImandraX introduces a unified language for tactics and tacticals, based on the by annotation. This approach allows users to structure proofs through a combination of smaller tactics and more sophisticated tacticals, enabling modular, reusable proof strategies. Additionally, ImandraX includes a rich library of built-in tactics and tacticals, encompassing a broad spectrum of proof methods and strategies, from highly automated (auto, unroll, etc.) to surgical ([%expand ...] and exact).

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"]
           @> [%skip]
           @> skip
           @> [%skip "hello again from subgoal 2"]
           @> auto);
          (expr_simplify
           @> [%replace x]
           @> [%replace y]
           @> [%expand (g 7 7)]
           @> simp)
          ]
       ]

auto

auto apply Imandra’s inductive waterfall proof strategy, which combines simplification (including automatic subgoaling, conditional rewriting and forward-chaining using previously proved lemmas, decision procedures for datatypes and arithmetic, etc.), and may decide to do induction. This is the most common way to prove a theorem in Imandra.

Rule Classes

Theorems may be installed as rules, which instructs Imandra to apply them in certain ways during subsequent proof attempts. The development of an appropriate collection of rules can be used to “teach” Imandra how to reason in a new domain.

• [@@rw] or [@@rewrite]: install theorem as a rewrite rule
• [@@permutative]: restrict rewrite rule as permutative
• [@@fc]: install theorem as a forward chaining rule
• [@@elim] or [@@elimination]: install theorem as an elimination rule
• [@@gen] or [@@generalization]: install theorem as a generalization rule

induct

induct is auto with some parameters exposed for controlling it.

• ~smt:<smt_solver> - use the given SMT solver for the induction, for example, “~smt:”z3”. Pass ~smt:"None" to use the best available solver.
• ~on_fun:<func_name> - perform functional induction using an induction scheme derived from <func_name>
• ~on_vars:<args> - perform structural induction on the arguments <args> if given, else on a heuristically chosen collection of variables. The types of the induction variables must be algebraic datatypes / variant types. An additive approach (linear in the total number of constructors) is taken for combining the schemes of individual variables into a composite induction scheme.
• ~max_induct:<n> - set the maximum induction depth to <n>.

Other Common Tactics

intros

intros takes a goal with implications and conjunctions H |- (A && B) ==> C and returns the new goal H, A, B |- C. This is typically the first tactic in a chain when the goal has premises that need to be introduced as hypotheses.

lemma foo x y = x > 0 && y > 0 ==> x + y > 0 [@@by intros @> auto]

simp / simplify

Apply simplification to the goal. There are several variants:

• simp - Quick and simple simplifier, always returns 1 goal
• simplify () - Full waterfall simplifier with all active rules
• [%simp rule1, rule2] - Simplify using specific rewrite rules
• [%simp_only rule1, rule2] - Simplify using ONLY the given rules (strict mode)

lemma rev_rev x = List.rev (List.rev x) = x [@@by auto] [@@rw]

(* Using specific rules *)
lemma foo x y = List.length (List.rev (x @ y)) = List.length x + List.length y
  [@@by [%simp rev_len, len_append]]

unroll

unroll n performs bounded model checking via SMT, unrolling recursive definitions up to n steps. This is useful for goals that can be discharged by finite exploration.

(* Unroll with default SMT solver *)
verify (fun x -> x < 10 ==> f x >= 0) [@@by unroll 100]

(* Unroll with specific solver *)
[@@by unroll ~smt:"z3" 50]

Arithmetic Decision Procedures

• arith - Decision procedure for linear (real and integer) arithmetic
• nonlin () - SMT solver with non-linear arithmetic enabled

lemma linear_example x y = x + y >= x [@@by intros @> arith]

lemma quadratic_example x = x * x >= 0 [@@by nonlin ()]

cases

[%cases t1, t2, ..., tk] performs case analysis on boolean conditions, generating k+1 subgoals: one for each case (with the case as hypothesis) and one for when all cases are false.

lemma abs_nonneg x = abs x >= 0
  [@@by [%cases x >= 0] @>| [auto; auto]]

expand

[%expand "f"] unfolds the definition of function f. Use [%expand (f x y)] to expand a specific application.

let square x = x * x

lemma square_pos x = x <> 0 ==> square x > 0
  [@@by intros @> [%expand "square"] @> nonlin ()]

use

[%use lemma_name args] instantiates a previously proven theorem and adds it as a hypothesis to the current goal.

lemma pow_pos_helper b n = b > 0 ==> pow b n > 0 [@@by auto]

lemma foo x = x > 0 ==> pow x 5 + 1 > 1
  [@@by intros @> [%use pow_pos_helper x 5] @> auto]

Combinators

Tactics support monadic operations, enabling clean and modular chaining of reasoning steps. Operators like @>, <|>, and @>>| allow for intuitive composition and conditional application of tactics.

• @>: t @> t' expects t to produce exactly one sub-goal, and uses t' to prove this subgoal.
• <|>: t1 <|> t2 is the or tactical which applies t1 and uses its result if it succeeds, and otherwise applies t2 if t1 had failed
• @>>|: t1 @>>| t2 applies t1 and then applies t2 to all t1-generated subgoals.
• @>|: t @>| [t1; t2; ...; tn] expects t to produce n subgoals, and , and uses t_i to solve the i-th goal.

Reference for All Tactics

1. quote_term
   • Signature: 'a -> 'a term
   • Doc: quote_term (1 + 2) is a quotation that will not evaluate to anything but the term “1 + 2”. It can then be provided as-is to a tactic.
2. combine_proofs
   • Signature: proof list -> proof -> proof
   • Doc: Given a proof p of box A1, ..., box An |- box B and hyps, proofs of |- box A_i respectively, return a proof of |- box B
3. skip
   • Signature: t
   • Doc: skip is a no-op from a reasoning perspective (goal will be unchanged). This can be useful when needing to put a place-holder tactic in, e.g., a list of tactics for subgoals when using @>|, e.g., ... @|> [...; skip; ...].

See the variant skip_msg which is like skip but also prints a message.

Note the notation [%skip "skip message"] can be used, with [%skip] emitting no message.

1. skip_msg
   • Signature: string -> t
   • Doc: skip_msg "msg" is like skip (a reasoning no-op) but also prints the string “msg”. This can be useful for tactic debugging.

Note the notation [%skip "skip message"] can be used, with [%skip] emitting no message.

1. ground_eval
   • Signature: ?max_cache:int -> unit -> t
2. qs
   • Signature: t
   • Doc: A very fast, incomplete SMT solver for simple QF_UFDT/LIA/LRA goals.
3. cc
   • Signature: t
4. simp
   • Signature: t
   • Doc: Quick and simple simplifier. This always returns 1 goal.
5. simp_all
   • Signature: t
   • Doc: Quick and simple simplifier on hypotheses and conclusion. This always returns 1 goal.
6. ctx_simplify
   • Signature: t
   • Doc: Contextual simplifcation
7. expr_simplify
   • Signature: t
   • Doc: Moral equivalent of Z3’s Expr.simplify applied to each hypothesis and conclusion in the goal.
8. or_left
   • Signature: t
   • Doc: Takes G ?- a || b, returns G ?- a
9. or_right
   • Signature: t
   • Doc: Takes G ?- a || b, returns G ?- b
10. split_and
    • Signature: t
    • Doc: Takes G ?- a && b, returns G ?- a and G ?- b
11. exact
    • Signature: t
    • Doc: Takes G, t ?- t, ..., succeeds with no further goal. Otherwise fails.
12. trivial
    • Signature: t
    • Doc: Succeeds if a goal is trivially true due to having false in the hypotheses, true in the conclusion, or the exact same term in the hypotheses and conclusion (subsuming the exact tactic).
13. intros
    • Signature: t
    • Doc: intros takes a goal H |- (A && B) ==> C and returns the new goal H, A, B |- C.
14. unintros
    • Signature: int list -> t
    • Doc: unintros [1;3;4] takes a goal H0; H1; ...; H7 |- C and turns it into H0; H2; H5; H6; H7 |- (H1 && H3 && H4) ==> C. In that sense it’s the inverse of intros.
15. swap
    • Signature: int -> t
    • Doc: swap i takes a goal H0; ...; Hk |- C0; ...; Ck and swaps a literal (either a hypothesis or a conclusion term) over the sequent line (|-), negating it in the process.

If i>=0, then hypothesis i (Hi) is negated and made a conclusion. If i<0, then conclusion abs(i+1) (C(abs(i+1))) is negated and made a hypothesis.

1. drop
   • Signature: int -> t
   • Doc: drop i drops a hypothesis or conclusion, using the same literal addressing scheme as swap.
2. expand
   • Signature: ?index:int -> ?all:bool -> string -> t
   • Doc: expand "foo" expands the first occurrence of foo. expand ~index:3 "foo" expands the index 3 (i.e., fourth) occurrence of foo. expand ~all:true "foo" expands all current instances of foo. Instances introduced through this expansion process will not be recursively expanded.

Note the notation [%expand "foo"] can also be used, with either function names or terms which will be automatically quoted (see expand_term).

1. expand_term
   • Signature: ?index:int -> ?all:bool -> 'a term -> t
   • Doc: expand_term (quote_term (foo x)) expands the first occurrence of foo x. expand_term ~index:3 (quote_term (foo x)) expands the index 3 (i.e., fourth) occurrence of foo x. expand_term ~all:true (quote_term (foo x)) expands all current instances of foo. Instances introduced through this expansion process will not be recursively expanded.

Note the notation [%expand (foo x)] handles term quoting automatically.

1. replace
   • Signature: 'a term -> t
   • Doc: replace (quote_term x) uses an equality hypothesis x=t to replace x by t.
2. normalize
   • Signature: ?rules:identifier list -> ?strict:bool -> ?basis:identifier list -> ?inline:bool -> 'a term -> t
   • Doc: normalize (quote_term t) normalizes a given term under hypotheses of the current goal, replacing the term with its normalized version if it appears in the goal, and adding the hypotheses t = normalized_t if the target term does not appear already in the goal.

Normalization applies all active rewrite rules, forward chaining rules, expands all enabled non-recursive function definitions and includes the speculative expansion and simplification of recursive functions in order to take advantage of inductive hypotheses, in the same manner as the waterfall simplifier.

The rules and strict parameters behave the same as with the simplify tactic, restricting which rewrite rules and function definitions may be applied and/or expanded. The basis parameter acts as a restriction on which function definitions can be expanded (basis members are not expanded, unless they are explicitly given via rules with strict:true.

Note the notation [%normalize t] which normalizes term t with default arguments given to normalize.

1. generalize
   • Signature: 'a term -> string -> t
   • Doc: generalize (quote_term t) gen_name generalizes term t by replacing it with a fresh Skolem of the appropriate type throughout the goal. There are some restrictions on the name gen_name used for the new general term: no terms can already appear in the goal with the same name, and the term should follow the basic syntactic rules of IML/OCaml identifiers (begin with a lowercase alphabetical character or _, etc.).
2. cases
   • Signature: bool term list -> t
   • Doc: cases [(quote_term t1);...;(quote_term tk)] case-splits on the given cases, returning k+1 subgoals consisting of one for each case (with the case added as a hypothesis), and one additional subgoal for the ‘negative’ case in which all t1,…,tk are false. The terms must be boolean-valued.

Note the notation [%cases t1, t2, ..., tk] will handle term quoting automatically.

1. subgoal
   • Signature: bool term -> t
   • Doc: subgoal (quote_term t) assumes a term and adds the correctness of this assumption as a subgoal. This effectively applies the cut rule of sequent calculus to produce two subgoals: one in which the term has been assumed, and another in which the term must be proved under the current goal context. The term must be boolean-valued.

Note the notation [%subgoal t] will handle term quoting automatically.

1. lift_ifs
   • Signature: t
   • Doc: Lift if-then-else expressions to the top-level and split accordingly into subgoals. This does a limited amount of feasibility checking to eliminate obviously true subgoals (infeasible if branches under the current context) while lifting.
2. flatten
   • Signature: t
   • Doc: Disjunctive flattening.
3. smolsmt
   • Signature: t
   • Doc: A small and simple SMT solver for QF_UF goals.
4. unroll
   • Signature: ?smt:string -> ?query_timeout:int -> ?no_asm_query_timeout:int -> int -> t
   • Doc: unroll ~smt:"z3" 42 does 42 rounds of unrolling with SMT solver named “z3”. Pass ?smt:None to use the best available SMT solver.
5. arith
   • Signature: t
   • Doc: A decision procedure for linear (real and integer) arithmetic.
6. nonlin
   • Signature: ?smt:string -> unit -> t
   • Doc: An SMT solver with non-linear arithmetic enabled. Pass None to use the best available SMT solver.
7. auto
   • Signature: t
   • Doc: Auto tactic, Imandra’s flagship automated inductive waterfall proof procedure, taking into account all known active (rw,fc,elim,gen) rules, incorporating 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.
8. induction
   • Signature: ?id:identifier -> ?vars:string list -> unit -> t
   • Doc: Induction tactic: Synthesize an induction scheme for the goal and apply it. This does not invoke the induction waterfall (as in auto).
9. simplify
   • Signature: ?smt:string -> ?backchain_limit:int -> ?rules:identifier list -> ?strict:bool -> ?basis:identifier list -> unit -> t
   • Doc: Full simplifier (the waterfall simplifier). Pass ?smt:None to use the best available SMT solver. The parameter rules is an optional list of IDs of rewrite rules. If given, only these rewrite rules will be used during simplification. The parameter ~strict when true and given in conjunction with rules further restricts the simplifier to only use definitional rules (function definitions, both recursive and non-recursive) and rewrite rules which are explicitly present in the rules list. The parameter ~backchain_limit controls the recursive depth of back-chaining on hypotheses that is allowed during the relieving of rewrite rule guards (hypotheses).

Note the syntax [%simplify foo, bar, baz] which expands to simplify ~rules:[[%id foo]; [%id bar]; [%id baz]] ().

Note that [%simp ...] is an alias for [%simplify ...].

Note the syntax [%simplify_only ...] and its alias [%simp_only ...] which are like [%simp ...] with ~strict:true.

1. induct
   • Signature: ?smt:string -> ?on_fun:identifier -> ?on_vars:string list -> ?otf:bool -> ?max_induct:int -> ?do_not:string list -> unit -> t
   • Doc: Induction using the waterfall. Use like this: induct ~smt:"z3" ~on_vars:["x"; "y"] () for structural induction, or induct ~on_fun:[%id f] () for function induction with function f
2. use
   • Signature: bool term -> t
   • Doc: Use an existing theorem to add an additional hypothesis to the current goal. For example use (quote_term (add_is_commutative x y)) takes a goal A ?- B and returns a goal (x+y)=(y+x), A ?- B.

Note the notation [%use foo x y z] handles term quoting automatically.

1. enumerate
   • Signature: string list -> t
   • Doc: A tactic that enumerates all values of finite-type variables.
2. par_solve
   • Signature: (t term * goal) list -> proof list res
   • Doc: Primitive to solve subgoals in parallel