Simplification

At the core of ImandraX is a powerful symbolic simplifier and partial evaluator. The simplifier transforms formulas into simpler forms by applying rewrite rules, forward-chaining rules, and built-in decision procedures. It is the most consequential stage of the waterfall — most proofs succeed primarily through simplification.

How simplification works

The simplifier operates on a compact directed graph representation of formulas. This memoized representation gives ImandraX remarkable efficiency — it can evaluate recursive functions on large inputs almost instantly by sharing common subexpressions.

For example, a naive Fibonacci function that would take standard OCaml over 10 minutes for fib 200 can be evaluated by ImandraX's simplifier in milliseconds, because the digraph representation automatically memoizes previously computed values.

Rewrite rules

A rewrite rule has the form:

hypotheses imply left-hand-side equals right-hand-side

During simplification, when the simplifier encounters a term matching the left-hand-side, it replaces it with the instantiated right-hand-side (provided the hypotheses are satisfied).

Install a theorem as a rewrite rule with [@@rw]:

lemma rev_len xs =
  List.length (List.rev xs) = List.length xs
[@@by auto] [@@rw]

Now wherever the simplifier sees List.length (List.rev <expr>), it rewrites it to List.length <expr>.

Designing good rewrite rules

The right-hand-side should be simpler or more canonical than the left-hand-side. Rules that make terms more complex can cause the simplifier to loop.

(* GOOD: simplifies by removing rev *)
lemma rev_len xs =
  List.length (List.rev xs) = List.length xs
[@@by auto] [@@rw]
 
(* BAD: would make terms more complex *)
(* lemma bad_rule xs =
     List.length xs = List.length (List.rev xs) *)

Conditional rewrite rules

Rewrite rules can have hypotheses. The rule only fires when its hypotheses are satisfied:

lemma insert_invariant a xs =
  is_sorted xs ==> is_sorted (insert a xs)
[@@by auto] [@@rw]

This rule rewrites is_sorted (insert a xs) to true, but only when is_sorted xs is known.

Variable coverage

The left-hand-side of a rewrite rule must contain all the theorem's top-level variables. If some variables only appear in hypotheses, use the [@trigger rw] annotation:

lemma mem_subset x y z =
  List.mem x y && (subset y z [@trigger rw]) ==> List.mem x z
[@@by auto] [@@rw]

Permutative rewrite rules

Some useful rewrite rules are permutative — they don't simplify terms but reorder them into a canonical form. A classic example is commutativity:

lemma add_commutes x y =
  x + y = y + x
[@@by auto] [@@rw] [@@perm]

Without [@@perm], this rule would loop forever: a + b → b + a → a + b → .... The [@@perm] (or [@@permutative]) annotation restricts the rule to fire only when the result is lexicographically smaller than the original, ensuring termination while still canonicalizing terms.

Forward-chaining rules

Forward-chaining rules derive new facts from existing hypotheses. While rewrite rules transform terms, forward-chaining rules add new knowledge to the proof context.

Install with [@@fc] and mark trigger terms with [@trigger]:

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

When the simplifier encounters List.length <expr> in any context, it adds the fact List.length <expr> >= 0 to the hypotheses.

Forward chaining with multiple triggers

theorem odds_len x =
  x <> [] && List.tl x <> []
  ==>
  (List.length (odds x) [@trigger]) < List.length x
[@@by induct ~on_fun:[%id odds] ()] [@@fc]

This forward-chaining rule fires whenever List.length (odds x) appears, adding the bound as a hypothesis (provided the guards are met).

Using simplification tactics

`simplify ()`

Apply the full simplifier with all enabled rules:

[@@by simplify ()]

`[%simp rule1, rule2, ...]`

Simplify using specific additional rules:

lemma foo g h x y =
  k (List.length (List.rev (x @ y))) = List.length (y @ x)
[@@by [%simp rev_len, len_append]]

`[%simp_only rule1, rule2, ...]`

Simplify using only the listed rules (no automatic rules):

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

`[%norm ...]` / `normalize`

Normalize a specific term:

[@@by normalize ~rules:[[%id rev_len]] [%t List.length (List.rev (x @ y))]
    @> [%simp_only k]
    @> [%simp_only len_append]]

Controlling the simplifier

Disabling rules

Prevent specific rules or function definitions from being used during simplification with the [@@disable] attribute:

[@@by auto] [@@disable some_rule, some_function]

Global disable

Use [@@@disable] (three @) at the file level to disable rules globally:

[@@@disable some_rule]

Example: The simplifier in action

Here's how simplification works in a real proof. Consider proving that k (List.length (List.rev (x @ y))) = List.length (y @ x) where k x = x + 1 - 1:

let k x = x + 1 - 1
 
lemma k_eq x = k x = x [@@rw]
 
lemma rev_len x =
  List.length (List.rev x) = List.length x
[@@by auto] [@@rw]
 
lemma len_append x y =
  List.length (x @ y) = List.length x + List.length y
[@@by auto] [@@rw]
 
lemma add_commutes x y =
  x + y = y + x
[@@by auto] [@@rw] [@@perm]
 
lemma foo g h x y =
  k (List.length (List.rev (x @ y))) = (List.length (y @ x))
[@@by [%simp rev_len, len_append]]

The simplifier:

Applies rev_len to rewrite List.length (List.rev (x @ y)) → List.length (x @ y)
Applies len_append on both sides
Applies k_eq to simplify k
Uses add_commutes to canonicalize the arithmetic
The goal reduces to true