Tutorial: Verifying Insertion Sort

In this tutorial, we'll verify that insertion sort is correct — meaning it produces sorted output that contains exactly the same elements as the input. This is a gentle introduction to induction, rewrite rules, and ImandraX's automatic proof capabilities.

The algorithm

Insertion sort works by maintaining a sorted prefix and inserting each new element into its correct position:

let rec insert (x : int) xs =
  match xs with
  | [] -> [x]
  | a :: bs ->
    if x <= a then x :: xs
    else a :: (insert x bs)
 
let rec insert_sort xs =
  match xs with
  | [] -> []
  | x :: xs -> insert x (insert_sort xs)

Both functions are structurally recursive (recursing on a sublist), so ImandraX proves termination automatically.

Part 1: Insertion sort produces sorted output

First, let's define what "sorted" means:

let rec is_sorted (x : int list) =
  match x with
  | [] -> true
  | [_] -> true
  | x :: x' :: xs -> x <= x' && is_sorted (x' :: xs)

The key lemma

To prove the main theorem, we need a helper lemma: inserting into a sorted list preserves sortedness.

theorem insert_invariant a x =
  is_sorted x ==> is_sorted (insert a x)
[@@by auto] [@@rw]

Notice two things:

1. [@@by auto] — ImandraX proves this automatically using the waterfall (with induction on x)
2. [@@rw] — This installs the theorem as a rewrite rule. Whenever the simplifier sees is_sorted (insert a x) and knows is_sorted x, it rewrites it to true

The main theorem

With the rewrite rule in place, the main theorem follows:

theorem insert_sort_sorts x =
  is_sorted (insert_sort x)
[@@by auto]

ImandraX inducts on x:

• Base case (x = []): insert_sort [] = [], and is_sorted [] is true ✓
• Inductive step (x = a :: xs): By the IH, is_sorted (insert_sort xs). Then insert_sort (a :: xs) = insert a (insert_sort xs). By insert_invariant, since insert_sort xs is sorted, so is insert a (insert_sort xs) ✓

Part 2: Insertion sort preserves elements

Sorting isn't just about ordering — we also need to verify that no elements are added or removed. We prove this by showing that the number of occurrences of each element is preserved.

let rec num_occurs x y =
  match y with
  | [] -> 0
  | hd :: tl when hd = x ->
    1 + num_occurs x tl
  | _ :: tl ->
    num_occurs x tl

Helper lemmas

We need two lemmas about how insert affects element counts:

(* Inserting x adds exactly one occurrence of x *)
theorem lemma_1 x a =
  num_occurs a (insert a x) = num_occurs a x + 1
[@@by auto] [@@rw]
 
(* Inserting x doesn't change the count of any other element *)
theorem lemma_2 x a b =
  a <> b ==> num_occurs b (insert a x) = num_occurs b x
[@@by auto] [@@rw]

Both are installed as rewrite rules so the simplifier can use them automatically.

The main theorem

theorem insert_sort_elements a (x : int list) =
  num_occurs a x = num_occurs a (insert_sort x)
[@@by auto]

With the rewrite rules from lemma_1 and lemma_2 in place, ImandraX proves this automatically.

The complete verified program

Here's the entire file in one piece:

(* Correctness of insertion sort in ImandraX *)
 
let rec insert (x : int) xs =
  match xs with
  | [] -> [x]
  | a :: bs ->
    if x <= a then x :: xs
    else a :: (insert x bs)
 
let rec insert_sort xs =
  match xs with
  | [] -> []
  | x :: xs -> insert x (insert_sort xs)
 
let rec is_sorted (x : int list) =
  match x with
  | [] -> true
  | [_] -> true
  | x :: x' :: xs -> x <= x' && is_sorted (x' :: xs)
 
theorem insert_invariant a x =
  is_sorted x ==> is_sorted (insert a x)
[@@by auto] [@@rw]
 
theorem insert_sort_sorts x =
  is_sorted (insert_sort x)
[@@by auto]
 
let rec num_occurs x y =
  match y with
  | [] -> 0
  | hd :: tl when hd = x -> 1 + num_occurs x tl
  | _ :: tl -> num_occurs x tl
 
theorem lemma_1 x a =
  num_occurs a (insert a x) = num_occurs a x + 1
[@@by auto] [@@rw]
 
theorem lemma_2 x a b =
  a <> b ==> num_occurs b (insert a x) = num_occurs b x
[@@by auto] [@@rw]
 
theorem insert_sort_elements a (x : int list) =
  num_occurs a x = num_occurs a (insert_sort x)
[@@by auto]

What you've learned

• Rewrite rules ([@@rw]) are the key to modular proofs — prove small lemmas and let the simplifier compose them
• Induction is applied automatically when [@@by auto] encounters recursive functions
• Two-part correctness: sorting algorithms need both a sortedness proof and an element preservation proof
• Lemma-driven development: break complex proofs into lemmas, prove each independently, and let the waterfall compose them

Next steps

The Merge Sort tutorial extends these ideas with custom termination measures and manual tactic proofs.