Tutorial: Verifying Merge Sort

This tutorial verifies merge sort — a more complex sorting algorithm than insertion sort. Along the way, you'll learn about custom termination measures, forward-chaining rules, and how to write proofs both automatically and manually using tactics.

The algorithm

Merge sort works by splitting a list into halves, recursively sorting each half, and merging the results:

let rec merge (l : int list) (m : int list) =
  match l, m with
  | [], _ -> m
  | _, [] -> l
  | a :: ls, b :: ms ->
    if a < b then a :: (merge ls m)
    else b :: (merge l ms)
[@@adm l, m]
[@@by auto]

Note the [@@adm l, m] annotation: merge termination requires a lexicographic argument — either l gets shorter, or l stays the same and m gets shorter. The [@@by auto] proves the termination obligation.

Splitting with `odds`

Instead of computing the midpoint, we split by taking alternate elements:

let rec odds l =
  match l with
  | [] -> []
  | [x] -> [x]
  | x :: _ :: rst -> x :: odds rst

We need a forward-chaining lemma establishing that odds produces shorter lists:

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

The [@trigger] annotation tells the forward-chaining system to activate this rule whenever it sees List.length (odds ...).

Merge sort itself

let rec merge_sort l =
  match l with
  | []  -> []
  | [_] -> l
  | _ :: ls -> merge (merge_sort (odds l)) (merge_sort (odds ls))
[@@measure Ordinal.of_int (List.length l)]

The [@@measure] annotation provides an explicit termination measure: the list length, expressed as an ordinal. ImandraX verifies that List.length (odds l) < List.length l using the forward-chaining rule above.

Part 1: Merge sort sorts

let rec is_sorted (x : int list) =
  match x with
  | [] -> true
  | [_] -> true
  | x :: x' :: xs -> x <= x' && is_sorted (x' :: xs)
 
(* Key lemma: merging sorted lists produces a sorted list *)
theorem merge_sorts x y =
  is_sorted x && is_sorted y ==> is_sorted (merge x y)
[@@by auto] [@@rw]
 
(* Main theorem *)
theorem merge_sort_sorts x =
  is_sorted (merge_sort x)
[@@by auto]

Part 2: Merge sort preserves elements

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 num_occur_merge a x y =
  num_occurs a (merge x y) = num_occurs a x + num_occurs a y
[@@by auto] [@@rw]

A manual proof (for learning)

The same theorem can be proved manually, to illustrate ImandraX's tactic language:

theorem num_occur_merge a x y =
  num_occurs a (merge x y) = num_occurs a x + num_occurs a y
[@@by induction ~id:[%id merge] ()
   @>| [
     lift_ifs @>>| ([%replace x] <|> [%replace y]) @> simplify ();
 
     [%normalize num_occurs a (merge x y)]
      @> [%replace num_occurs a (merge x (List.tl y))]
      @> lift_ifs
      @>| [swap (-1) @> [%normalize num_occurs a y] @> trivial;
           [%normalize num_occurs a y] @> arith];
 
     [%normalize num_occurs a (merge x y)]
      @> lift_ifs
      @>| [[%normalize num_occurs a x]
            @> [%replace num_occurs a (merge (List.tl x) y)]
            @> lift_ifs @> trivial;
           [%normalize num_occurs a x]
            @> [%replace num_occurs a (merge (List.tl x) y)]
            @> arith]
   ]]

This manual proof demonstrates:

induction ~id:[%id merge] () — induct using merge's recursion scheme
@>| — apply different tactics to different subgoals
lift_ifs — lift conditionals to case splits
[%normalize ...] — normalize a specific term
[%replace ...] — substitute using a hypothesis
arith — close goals with arithmetic reasoning

The elements theorem

theorem num_occurs_arith (x : int list) (a : int) =
  x <> [] && List.tl x <> []
  ==>
  num_occurs a (odds (List.tl x))
  = num_occurs a x - num_occurs a (odds x)
[@@by induct ~on_fun:[%id num_occurs] ()] [@@rw]
 
theorem merge_sort_elements a (x : int list) =
  num_occurs a x = num_occurs a (merge_sort x)
[@@by auto]

What you've learned

Lexicographic termination with [@@adm l, m]
Custom ordinal measures with [@@measure Ordinal.of_int ...]
Forward-chaining rules with [@@fc] and [@trigger]
Manual tactic proofs vs. automatic proofs — same theorem, both approaches
Tactic composition — @>| for subgoal-specific strategies

Next steps

The Compiler Verification tutorial shows how to verify a more complex system with custom induction schemes.