Induction

Induction is the fundamental technique for proving properties of recursively defined structures — natural numbers, lists, trees, and any recursive datatype. When a property holds for base cases and can be shown to carry over from smaller to larger structures, it holds universally.

Induction in ImandraX

A standard inductive proof requires:

  1. Base case(s): Show the property holds for the smallest elements (e.g., empty list, leaf node, zero)
  2. Inductive step(s): Assuming the property holds for smaller elements (the inductive hypothesis), show it holds for the next larger element

ImandraX automates this process. When you write [@@by auto], ImandraX:

  1. Analyzes the recursive functions in your goal
  2. Synthesizes an appropriate induction scheme from their recursion patterns
  3. Applies the scheme, generating base and step subgoals
  4. Attempts to prove each subgoal (usually via simplification)

Functional induction

Functional induction derives induction schemes from recursive function definitions. The key insight: the termination proof for a recursive function already contains the information needed to construct a valid induction principle.

For example, given:

let rec length = function
  | [] -> 0
  | _ :: xs -> 1 + length xs

The termination proof says: "length terminates because xs is structurally smaller than _ :: xs." This generates an induction scheme:

  • Base case: xs = []
  • Inductive step: xs = a :: xs', with hypothesis that the property holds for xs'

When you prove a theorem involving length, ImandraX uses this scheme:

theorem length_append xs ys =
  length (xs @ ys) = length xs + length ys
[@@by auto]

Automatic scheme selection

When a goal involves multiple recursive functions, ImandraX heuristically selects the best induction scheme. You can override this:

(* Induct using the scheme from a specific function *)
[@@by induction ~id:[%id my_function] ()]

Custom induction schemes

For complex proofs, you can define a function purely to induce a custom induction scheme. ImandraX examines only the recursion pattern, not what the function computes:

(* This function exists only to define an induction scheme *)
let rec compiler_induct s e =
  let ih s x y =
    compiler_induct s x
    && compiler_induct
      { stack = (eval_expr x) :: s.stack }
      y
  in
  match e with
  | Plus (x, y) | Times (x, y) | Sub (x, y) | Div (x, y) ->
    ih s x y
  | _ -> true
[@@adm e]
 
(* Use the custom scheme with the full waterfall *)
theorem compiler_correct s e =
  run s (compile e) = { stack = (eval_expr e) :: s.stack }
[@@by induct ~on_fun:[%id compiler_induct] ()]

Structural induction

Structural induction derives induction schemes directly from algebraic datatype definitions, rather than from function recursion patterns. This is useful when the goal doesn't involve a recursive function with the right shape.

type 'a tree = Leaf of 'a | Node of 'a tree * 'a tree
 
(* Structural induction on the tree type gives:
   Base case: t = Leaf a
   Inductive step: t = Node (l, r), with hypotheses for l and r *)
 
theorem size_positive t =
  size t >= 1
[@@by auto]

Additive vs multiplicative structural induction

When inducting over multiple variables simultaneously, there are two schemes:

Additive (default) generates cases that mirror pattern matching:

For variables xs : 'a list and ys : 'a list:

  • Base: xs = []
  • Base: xs = a :: xs', ys = []
  • Step: xs = a :: xs', ys = b :: ys', with IH for (xs', ys')

Multiplicative generates all combinations:

  • Base: xs = [], ys = []
  • Step: xs = a :: xs', ys = [], with IH for xs'
  • Step: xs = [], ys = b :: ys', with IH for ys'
  • Step: xs = a :: xs', ys = b :: ys', with IH for (xs', ys')

Multiplicative induction is more thorough but generates more subgoals:

[@@by induction ~vars:["xs"; "ys"] ()]

Examples from the repos

List append associativity

theorem append_assoc xs ys zs =
  (xs @ ys) @ zs = xs @ (ys @ zs)
[@@by auto]

ImandraX inducts on xs:

  • Base: ([] @ ys) @ zs = [] @ (ys @ zs) — both sides simplify to ys @ zs
  • Step: Assuming (xs' @ ys) @ zs = xs' @ (ys @ zs), show ((a :: xs') @ ys) @ zs = (a :: xs') @ (ys @ zs) — both sides simplify to a :: ((xs' @ ys) @ zs), and the IH closes the goal

Tree flattening

A classic induction benchmark — proving that a tail-recursive mc_flatten equals a naive flatten:

type 'a tree = Node of 'a tree * 'a tree | Leaf of 'a
 
let rec flatten = function
  | Leaf a -> [a]
  | Node (a, b) -> flatten a @ flatten b
 
let rec mc_flatten x ans =
  match x with
  | Leaf a -> a :: ans
  | Node (a, b) -> mc_flatten a (mc_flatten b ans)
 
theorem mc_flat_elim x ans =
  mc_flatten x ans = flatten x @ ans
[@@by auto]

Pigeon Hole Principle

ImandraX proves the pigeon hole principle for arbitrary n:

let rec sum_holes = function
  | [] -> 0
  | x :: xs -> x + sum_holes xs
 
let rec max_1_per_hole = function
  | [] -> true
  | x :: xs -> (x = 0 || x = 1) && max_1_per_hole xs
 
lemma key l n =
  0 < List.length l && List.length l < sum_holes l
  ==> not (max_1_per_hole l)
[@@by auto]
 
theorem php l n =
  0 < n && List.length l = n && sum_holes l = n + 1
  ==>
  not (max_1_per_hole l)
[@@by [%use key l n] @> auto]

Note how the key insight is in the key lemma: a generalization that makes the induction go through. The main theorem then follows by instantiating the lemma.

Previous← Unrolling
NextThe Waterfall →