Sorting can be done in expected O(N log N) time by various algorithms (quicksort, mergesort, heapsort, etc.). But for smallish inputs, a simple quadratic-time algorithm such as insertion sort can actually be faster. It's certainly easier to implement -- and to verify. If you don't recall insertion sort or haven't seen it in awhile, see Wikipedia or read any standard textbook; for example:

• Sections 2.0 and 2.1 of Algorithms, Fourth Edition, by Sedgewick and Wayne, Addison Wesley 2011; or
• Section 2.1 of Introduction to Algorithms, 3rd Edition, by Cormen, Leiserson, and Rivest, MIT Press 2009.

The Insertion-Sort Program

Insertion sort is usually presented as an imperative program operating on arrays. But it works just as well as a functional program operating on linked lists.

We won't analyze or prove anything about the efficiency of sort. Instead, we will verify its correctness: that it produces the correct output for a given input.

Specification of Correctness

A sorting algorithm must rearrange the elements into a list that is totally ordered. There are many ways we might express that idea formally in Coq. One is with an inductively-defined relatio that says:

• The empty list is sorted.
  • Any single-element list is sorted.
  • For any two adjacent elements, they must be in the proper order.

This definition might not be the most obvious. Another definition, perhaps more familiar, might be: for any two elements of the list (regardless of whether they are adjacent), they should be in the proper order. Let's try formalizing that. We can think in terms of indices into a list lst, and say: for any valid indices i and j, if i < j then index lst i ≤ index lst j, where index lst n means the element of lst at index n. Unfortunately, formalizing this idea becomes messy, because any Coq implementing index must be total: it must return some result even if the index is out of range for the list. The Coq standard library contains two such functions:

These two functions ensure totality in different ways:

• nth takes an additional argument of type A --a default value-- to be returned if the index is out of range, whereas
• nth_error returns Some v if the index is in range and None
  • -an error-- otherwise.

If we use nth, we must ensure that indices are in range:

The choice of default value, here 0, is unimportant, because it will never be returned for the i and j we pass. If we use nth_error, we must add additional antecedents:

Here, the validity of i and j are implicit in the fact that we get Some results back from each call to nth_error. All three definitions of sortedness we have given are reasonable. In practice, sorted' is easier to work with than sorted'' because it doesn't need to mention the length function. And sorted is easier than either. Using sorted, we specify what it means to be a correct sorting algorthm:

Function f is a correct sorting algorithm if f al is sorted and is a permutation of its input.

Proof of Correctness

In the following exercises, you will prove the correctness of insertion sort.

Exercise: 3 stars, standard (insert_sorted)

Exercise: 2 stars, standard (sort_sorted)

Using insert_sorted, prove that insertion sort makes a list sorted.

Exercise: 3 stars, standard (insert_perm)

The following lemma will be useful soon as a helper. Take advantage of helpful theorems from the Permutation library.

Exercise: 3 stars, standard (sort_perm)

Prove that sort is a permutation, using insert_perm.

Exercise: 1 star, standard (insertion_sort_correct)

Finish the proof of correctness!

Validating the Specification (Advanced)

You can prove that a program satisfies a specification, but how can you prove you have the right specification? Actually, you cannot. The specification is an informal requirement in your mind. As Alan Perlis quipped, "One can't proceed from the informal to the formal by formal means." But one way to build confidence in a specification is to state it in two different ways, then prove they are equivalent.

Exercise: 4 stars, advanced (sorted_sorted')

Hint: Instead of doing induction on the list al, do induction on the sortedness of al. This proof is a bit tricky, so you may have to think about how to approach it, and try out one or two different ideas.

Exercise: 3 stars, advanced (sorted'_sorted)

Here, you can't do induction on the sortedness of the list, because sorted' is not an inductive predicate. But the proof is not hard.

Proving Correctness from the Alternative Spec (Optional)

Depending on how you write the specification of a program, it can be harder or easier to prove correctness. We saw that predicates sorted and sorted' are equivalent. It is significantly harder, though, to prove correctness of insertion sort directly from sorted'. Give it a try! The best proof we know of makes essential use of the auxiliary lemma nth_default_insert, so you may want to prove that first. And some other auxiliary lemmas may be needed too. But maybe you will find a simpler appraoch! DO NOT USE sorted_sorted', sorted'_sorted, insert_sorted, or sort_sorted in these proofs. That would defeat the purpose!

Exercise: 5 stars, standard, optional (insert_sorted')

If you complete the proofs above, you will note that the proof of insert_sorted is relatively easy compared to the proof of insert_sorted', even though sorted al ↔ sorted' al. So, suppose someone asked you to prove sort_sorted'. Instead of proving it directly, it would be much easier to design predicate sorted, then prove sort_sorted and sorted_sorted'. The moral of the story is therefore: Different formulations of the functional specification can lead to great differences in the difficulty of the correctness proofs.