osa1 feed

Proving sorting algorithms correct

September 8, 2014 - Tagged as: coq, en.

I've been working on proving some sorting algorithms correct in Coq. After 600 lines of Coq proofs, I managed to prove correctness of insertion sort, selection sort, and a weird sorting algorithm called pancake sort. This post is a literate Coq file which you can download and execute in a Coq IDE, step by step. To keep the post shorter and easier to read and make it more like an exercise, I hided most of the proofs in HTML version.
Goals of this post are:
  • Provide some guidance for starters who are interested in proving algorithms correct.
  • Demonstrate how to prove properties of functions with accumulators and functions that work on list indexes, instead of elements of the list.
  • Demonstrate how to use "timeout" arguments to convince Coq that a function is really terminating on all inputs.
A note before starting: I deliberately ignored advanced proof automation tools and go with more primitive way of proving. This is for two reasons: 1) I don't like magic, and since I don't understand underlying mechanics of advanced proofs tactics like crush, it's magic to me 2) They're sometimes so powerful, they get in your way to understand what's really happening in the proof.
If you're reading this post as an exercise and filling the proofs yourself, that should not be a problem for you. Otherwise you may find my proofs more verbose than what's necessary.
Let's start with standard stuff: imports. These are for some list helpers, list syntax, Peano definitions + functions etc. Just standard stuff. Only exception is the Permutation library, which I'll soon explain why it's necessary.

Require Import List.
Import ListNotations.
Open Scope list_scope.
Require Import Arith.
Require Import Omega.
Require Import Permutation.

Our goal is to define some sorting algorithms and then prove them correct, but for that we first need to define what we mean by for a sorting algorithm to be "correct". For some functions definition of correctness may be tricky to give, but in the context of sorting I think it's obvious:
  • Result should be a permutation of it's parameter.
  • Result should be in sorted order.
Definition of a "permutation" is defined in the Permutation library we've just included, and it comes with lots of very useful lemmas. I suggest you to go to Permutation library's documentation(you can go to the docs by clicking Permutation link in the imports part above) and just skim through the definition and lemmas, and convince yourself that the definition is really enough to show that two lists are really a permutation.
For being sorted, we need to define what does that mean.

Inductive sorted : list natProp :=
| Sorted_nil : sorted []
| Sorted_singleton : e, sorted [e]
| Sorted_cons : e h t, sorted (h :: t) → e hsorted (e :: h :: t).

Again, convince yourself that sorted l really encodes what we intuitively know about being sorted. Main property that should hold for any l that is sorted l is that for any consecutive elements a and b in the list, a b should hold, which our third constructor shows.
Using Permutation and sorted, we can define what does being correct for a sorting algorithm mean:

Inductive Sorting_correct (algo : list natlist nat) :=
| sorting_correct_intro :
    ( l, sorted (algo l) Permutation l (algo l)) → Sorting_correct algo.

Note that in both definition of sorted and Sorting_correct, we used list of nats instead of any lists of ordered elements. This is really just to make definitions and proofs simpler. Generalization may be done as an exercise.
Now with those definitions, we can prove our first and easiest-to-prove algorithm.

Insertion sort

We define insertion sort as a right fold:

Fixpoint insert (i : nat) (l : list nat) :=
  match l with
  | [][i]
  | h :: tif leb i h then i :: h :: t else h :: insert i t
  end.

Definition insertion_sort := fold_right insert [].

Now if we could show that insert h t on list h :: t returns a permutation, we could easily show that insertion sort returns a permutation, because all it does is to call insert on list elements, using fold_right.
***** Exercise: 1 star.
Lemma insert_perm : h t, Permutation (insert h t) (h :: t).

***** Exercise: 2 stars. Use insert_perm and transitivity, symmetry and reflexivity of Permutation.
To show that it returns sorted, we use a similar approach. We first show that if sorted l, then sorted (insert e l). Empty and singleton lists are sorted by definition. Using these facts, we can easily prove that insertion sort really return sorted.
***** Exercise: 2 star. You need to use some lemmas about leb that are already included. Use SearchAbout leb.
Lemma insert_sorted_preserve : e l,
  sorted lsorted (insert e l).

***** Exercise: 2 star. Use insert_sorted_preserve.
With permutation and sorted properties proved, we can show that our insertion sort implementation is correct:

Theorem insertion_sort_correct : Sorting_correct insertion_sort.
Proof.
  constructor. split. apply insertion_sort_sorted. apply Permutation_insertion_sort.
Qed.

Selection sort

Next, we move to selection sort. This one is significantly harder and most stuff we define in this section will be used in the next section.
Before implementing the algorithm, we need some auxiliary functions. find_min_idx is both used in selection sort and pancake sort. As you can imagine from the name, it returns index of one of the smallest elements in a list.
Note that it's very very hard to reason about this definition. The reason is that we're using index of a list, instead of head/tail of it. Simple induction-based proofs that we do before simply don't work on this definition.

Fixpoint find_min_idx_aux (l : list nat) (min min_idx cur_idx : nat) : nat :=
  match l with
  | []min_idx
  | h :: tif leb h min then find_min_idx_aux t h cur_idx (S cur_idx)
                           else find_min_idx_aux t min min_idx (S cur_idx)
  end.

Definition find_min_idx (l : list nat) : nat :=
  match l with
  | [] ⇒ 0
  | h :: tfind_min_idx_aux t h 0 1
  end.

An invariant of find_min_idx:
***** Exercise: 1 star.
Lemma find_min_idx_len_inv : l m mi ci r,
  find_min_idx_aux l m mi ci = r
  mi < ci
  r < ci + length l.

Make sure you understand what it's saying. We need this lemma to eliminate some impossible cases in proofs.
We also need a "membership" predicate. This is used to express the idea of "for all elements in the list ...", which is expressed in Coq like e, member e l ....

Inductive member {A} : Alist AProp :=
| Member_head : e l, member e (e :: l)
| Member_tail : e h t, member e tmember e (h :: t).

Again, convince yourself that this really expresses that idea. Here's a property of member:
***** Exercise: 1 star.
Lemma member_preserved_by_perm : A (l : list A) l' e,
  Permutation l l'
  member e l
  member e l'.

Now using member, we can express correctness of find_min_idx and prove it. Note that this is a very hard exercise. I couldn't solve it for a week, and even after that period I couldn't solve it without help from Coq IRC channel. Feel free to cheat by looking the source of this post.

***** Exercise: 5 stars. find_min_idx really returns index of smallest element.
Lemma find_min_idx_correct : n l,
  find_min_idx l = n
  ( e, member e lnth n l 0 e).

Now, in selection sort, we run several operations on argument. One of them is find_min_idx which we already defined. Another one of them is replace operation, which replaces nth element in a list with given element. Here's a definition and some properties:

Fixpoint replace {A} (l : list A) (idx : nat) (e : A) : list A :=
  match l with
  | [][]
  | h :: t
      match idx with
      | 0 ⇒ e :: t
      | S idx'h :: replace t idx' e
      end
  end.

***** Exercise: 1 star. First part of correctness proof of replace.
Lemma replace_nth : l i e l',
  i < length l
  replace l i e = l'
  nth i l' 0 = e.

***** Exercise: 1 star. Second part of correctness proof of replace. replace preserves length of the list.
Lemma replace_len : A l i (e : A),
  i < length l
  length l = length (replace l i e).

Using replace, we can define selection_sort. Note that our naive implementation doesn't convince Coq that it terminates on all input. An easy workaround is to add a step parameter. Observing that selection sort algorithm terminates in length l steps, where l is the input, we can define this:

Fixpoint selection_sort_aux (l : list nat) (step : nat) : list nat :=
  match step with
  | 0 ⇒ l
  | S step'
      match l with
      | [][]
      | h :: t
          match find_min_idx_aux t h 0 1 with
          | 0 ⇒ h :: selection_sort_aux t step'
          | S minnth min t 0 :: selection_sort_aux (replace t min h) step'
          end
      end
  end.

Definition selection_sort (l : list nat) : list nat := selection_sort_aux l (length l).

We have all we need to prove permutation property. It's still not easy though. I'm putting an extra lemma here as a tip.

***** Exercise: 2 stars.
Lemma replace_perm_head : n h t,
  n < length t
  Permutation (h :: t) (nth n t 0 :: replace t n h).

***** Exercise: 3 stars. Use replace_perm_head.
Proving sorted property is again, not easy. I'm putting some lemmas as pointers. Lemmas are very easy to prove, leaving only the master theorem as a challange.
***** Exercise: 1 star.
Lemma member_replace : A l i (x y : A),
  member x (replace l i y) →
  x = y member x l.

***** Exercise: 2 stars. Use member_replace and find_min_idx_correct.
Lemma swap_min_replace : h t min_idx,
  find_min_idx (h :: t) = S min_idx
  ( e, member e (replace t min_idx h) → nth min_idx t 0 e).

***** Exercise: 1 star.
Lemma sorted_min_tail : h t,
  sorted t
  ( e, member e th e) →
  sorted (h :: t).

***** Exercise: 2 stars. Use member_preserved_by_perm.
Lemma min_preserved_by_perm : m l l',
  Permutation l l'
  ( e, member e lm e) →
  ( e, member e l'm e).

***** Exercise: 4 stars. Selection sort returns sorted.
***** Exercise: 1 star. Show that selection sort is correct.

Pancake sort

This is getting harder and harder. We'll define pancake sort in terms of rev_at which reverses a list at given index and map_rest which is like map, but applies the function to the rest of the list.

Fixpoint rev_at {A} idx (l : list A) : list A :=
  match idx with
  | 0 ⇒ rev l
  | S idx'
      match l with
      | [][]
      | h :: th :: rev_at idx' t
      end
  end.

Fixpoint map_rest_aux {A} (l : list A) (f : list Alist A) (timeout : nat) : list A :=
  match timeout with
  | 0 ⇒ l
  | S timeout'
      match f l with
      | [][]
      | h :: th :: map_rest_aux t f timeout'
      end
  end.

Definition map_rest {A} (l : list A) (f : list Alist A) : list A :=
  map_rest_aux l f (length l).

Two things to note: 1) rev_at returns the original list if idx is larger than length l - 1. 2) map_rest only works as expected if f preserves length of it's argument in it's return value.
There's a very useful property that we need to show before showing that pancake sort returns a permutation: if f l returns a permutation, than map_rest l f returns a permutation:
***** Exercise: 2 stars.
Lemma Permutation_map_rest :
   A (f : list Alist A),
  ( (l : list A), Permutation l (f l)) →
  ( (l : list A), Permutation l (map_rest l f)).

Using this definition we can define pancake sort:

Definition flip_pancakes (l : list nat) : list nat :=
  let min_idx := find_min_idx l in
  rev_at 0 (rev_at min_idx l).

Definition pancake_sort (l : list nat) : list nat := map_rest l flip_pancakes.

Showing permutation property is actually very easy. All we need is two simple lemmas:
***** Exercise: 2 stars. Use already included standard permutation lemmas.
Lemma Permutation_rev_at : A n (l : list A),
  Permutation l (rev_at n l).

***** Exercise: 2 stars. Use transitivity of permutation and Permutation_rev_at.
***** Exercise: 1 star. Use Permutation_flip_pancakes.
Now the hard part. I needed a lot of lemmas for showing sorted property. I'm listing lemmas I used in no particular order.
***** Exercise: 2 stars. Smallest element is still smallest in a permutation. I found this a bit tricky. You may need to use another lemma we defined.
Lemma min_permutation : e l,
  ( e', member e' le e') →
  ( l', Permutation l l'
    ( e', member e' l'e e')).

***** Exercise: 1 star. flip_pancakes preserves the length.
***** Exercise: 4 stars. We can use rev_at to move smallest element to the end of the list, and then to the beginning of the list. Very tricky. Feel free to cheat.
Lemma rev_at_n : n l h t,
  n < length l
  rev_at 0 (rev_at n l) = h :: t
  h = nth n l 0.


***** Exercise: 3 stars. flip_pancakes moves smallest element to the head of the list.
Lemma flip_pancakes_min : l h' t',
  flip_pancakes l = h' :: t'
  ( e', member e' t'h' e').

***** Exercise: 4 stars. You need a lot of lemmas we defined before, and it's a very long proof. Still not as hard as find_min_idx_correct.
Theorem pancake_sorted : l, sorted (pancake_sort l).

And finally, our master theorem:

Theorem pancake_sort_correct : Sorting_correct pancake_sort.
Proof.
  constructor. intro. split. apply pancake_sorted. apply Permutation_pancake_sort.
Qed.

Notes and lessons learned

Implementation of algorithms are not what you'd expect to have in an imperative language. Rather than mutable arrays with O(1) access, I used classic functional style, using persistent linked lists. While that doesn't affect runtime asymptotic complexities of sorting algorithms I used, it causes a lot of redundant allocations and worse iteration performance. Even the OCaml/Haskell extractions are not usable.
Still, proving on those purely functional definitions were very hard. The reason is that once you move away from basic "induction of subterm" style proofs, proving gets very hard very fast. Specifically, I found working on indexes and accumulators very hard.
As a next step, I'm hoping to define an imperative language in Coq, like IMP of Software Foundations but with mutable arrays, and prove same algorithms defined in that language correct.