This sorting algorithm works by choosing (and deleting) the smallest element, then doing it again, and so on. It takes O(N^2) time. You should never* use a selection sort. If you want a simple quadratic-time sorting algorithm (for small input sizes) you should use insertion sort. Insertion sort is simpler to implement, runs faster, and is simpler to prove correct. We use selection sort here only to illustrate the proof techniques. *Well, hardly ever. If the cost of "moving" an element is much larger than the cost of comparing two keys, then selection sort is better than insertion sort. But this consideration does not apply in our setting, where the elements are represented as pointers into the heap, and only the pointers need to be moved. What you should really never use is bubble sort. Bubble sort would be the wrong way to go. Everybody knows that! https://www.youtube.com/watch?v=k4RRi_ntQc8

The Selection-Sort Program

Find (and delete) the smallest element in a list.

Now, selection-sort works by repeatedly extracting the smallest element, and making a list of the results. But the following attempted definition fails:

Error: Recursive call to selsort has principal argument equal to r' instead of r. That is, the recursion is not structural, since the list r' is not a structural sublist of i::r. One way to fix the problem is to use Coq's Function feature, and prove that length r' < length (i::r). Later in this chapter, we'll show that approach. Instead, here we solve this problem is by providing "fuel", an additional argument that has no use in the algorithm except to bound the amount of recursion. The n argument, below, is the fuel.

What happens if we run out of fuel before we reach the end of the list? Then WE GET THE WRONG ANSWER.

What happens if we have have too much fuel? No problem.

The selection_sort algorithm provides just enough fuel.

Now we repeat (from Sort) the specification of a correct sorting algorithm: it rearranges the elements into a list that is totally ordered.

Proof of Correctness of Selection sort

Here's what we want to prove.

For the exercises below, you may uncomment the next line and use the techniques and definitions from the Multiset chapter to prove the results. If you do that, make sure to leave the theorem statements unchanged. Note that there is no need to use multisets: they are completely optional.

We'll start by working on part 1, permutations. First, let's prove that select gives us back a permutation of its input.

Exercise: 2 stars, standard (select_perm)

Hints: After destructing select x l, you should be able to quickly finish with the lemma above. If you're using multisets, contents_perm could be helpful.

Exercise: 3 stars, standard (selection_sort_perm)

Hints: Induct on n. The lemma just proved above will be helpful; but, the let expression might get in the way of immediately applying it. You can assert an instantiated form of the lemma, including the let, for a particular x and l, then use rewriting to make use of the lemma. The standard library theorem Permutation_length could also be helpful. If you're using multisets, same_contents_iff_perm could be helpful.

Exercise: 3 stars, standard (select_smallest)

Hints: You do not need induction. Helpful lemmas include select_perm and Forall_perm.

Hint: Induct on al, but leave x universally quantified in the inductive hypothesis.

Exercise: 3 stars, standard (selection_sort_sorted)

Hint: You do not need induction. Helpful lemmas include selsort_perm and Forall_perm.

Hints: Induct on the length of al, leaving al universally quantified in the inductive hypothesis. Useful lemmas include selection_sort_sorted_aux and select_perm. You might also find use for select_smallest or Permutation_length.

Now we wrap it all up.

Recursive Functions That are Not Structurally Recursive

Fixpoint in Coq allows for recursive functions where some parameter is structurally recursive: in every call, the argument passed at that parameter position is an immediate substructure of the corresponding formal parameter. For recursive functions where that is not the case -- but for which you can still prove that they terminate -- you can use a more advanced feature of Coq, called Function.

When you use Function with measure, it's your obligation to prove that the measure actually decreases.

The proof must end with Defined instead of Qed, otherwise you can't compute with the function in Coq.

You won't want to unfold selsort' (or anything defined with Function) in proofs. Instead, rewrite with selsort'_equation, which was automatically defined by the Function command.

Exercise: 3 stars, standard (selsort'_perm)

Hint: Follow the same strategy as selsort_perm.