If you don't recall selection sort or haven't seen it in a while, see Wikipedia or read any standard textbook; some suggestions can be found in Sort. The specification for sorting algorithms we developed in Sort can also be used to verify selection sort. The selection-sort program itself is interesting, because writing it in Coq will cause us to explore a new technique for convincing Coq that a function terminates. A couple of notes on efficiency:

• Selection sort, like insertion sort, runs in quadratic time. But selection sort typically makes many more comparisons than insertion sort, so insertion sort is usually preferable for sorting small inputs. Selection sort can beat insertion sort if the cost of swapping elements is vastly higher than the cost of comparing them, but that doesn't apply to functional lists.
• What you should really never use is bubble sort. "Bubble sort would be the wrong way to go." Everybody should know that! See this video for a definitive statement: https://www.youtube.com/watch?v=k4RRi_ntQc8&t=34

The Selection-Sort Program

Selection sort on lists is more challenging to code in Coq than insertion sort was. First, we write a helper function to select the smallest element.

Selection sort should repeatedly extract the smallest element and make a list of the results. But the following attempted definition fails:

Coq rejects selsort because it doesn't satisfy Coq's requirements for termination. The problem is that the recursive call in selsort is not structurally decreasing: the argument r' at the call site is not known to be a smaller part of the original input l. Indeed, select might not return such a list. For example, select 1 [0; 2] is (0, [1; 2]), but [1; 2] is not a part of [0; 2]. There are several ways to fix this problem. One programming pattern is to provide fuel: an extra argument that has no use in the algorithm except to bound the amount of recursion. The n argument, below, is the fuel. When it reaches 0, the recursion terminates.

If fuel runs out, we get the wrong output.

Extra fuel isn't a problem though.

The exact amount of fuel needed is the length of the input list. So that's how we define selection_sort:

Proof of Correctness

We begin by repeating from Sort the specification of a correct sorting algorithm: it rearranges the elements into a list that is totally ordered.

In the following exercises, you will prove that selection sort is a correct sorting algorithm. You might wish to keep track of the lemmas you have proved, so that you can spot places to use them later. Depending on the path you have followed through Software Foundations it might have been a while since you have worked with pairs. Here's a brief reminder of how destruct can be used to break a pair apart into its components. A similar technique will be needed in many of the following proofs.

Exercise: 2 stars, standard (select_perm)

Prove that select returns a permutation of its input. Proceed by induction on l. The inv tactic defined at the end of Perm will be helpful. The eauto tactic] will be helpful at finding instantiations for perm_trans.

Exercise: 1 star, standard (select_rest_length)

Prove that select returns a list that has the correct length. You can do this without induction if you make use of select_perm.

Exercise: 3 stars, standard (selsort_perm)

Prove that if you provide sufficient fuel, selsort produces a permutation. Proceed by induction on n.

Exercise: 1 star, standard (selection_sort_perm)

Prove that selection_sort produces a permutation.

Exercise: 2 stars, standard (select_fst_leq)

Prove that the first component of select x _ is no bigger than x. Proceed by induction on al.

To represent the concept of comparing a number to a list, we introduce a new notation:

Exercise: 1 star, standard (le_all__le_one)

Prove that if y is no more than any of the elements of lst, and if n is in lst, then y is no more than n. Hint: a library theorem about Forall and In will make this easy.

Exercise: 2 stars, standard (select_smallest)

Prove that the first component of select _ _ is no bigger than any of the elements in the second component. Proceed by induction on al.

Exercise: 2 stars, standard (select_in)

Prove that the element returned by select must be one of the elements in its input. Proceed by induction on al.

Exercise: 3 stars, standard (cons_of_small_maintains_sort)

Prove that adding an element to the beginning of a selection-sorted list maintains sortedness, as long as the element is small enough and enough fuel is provided. No induction is needed.

Exercise: 2 stars, standard (selsort_sorted)

Prove that selsort produces a sorted list when given sufficient fuel. Proceed by induction on n. This proof will make use of a few previous lemmas.

Exercise: 1 star, standard (selection_sort_sorted)

Prove that selection_sort produces a sorted list.

Exercise: 1 star, standard (selection_sort_is_correct)

Finish the proof of correctness!

Recursive Functions That are Not Structurally Recursive

We used fuel above to create a structurally recursive version of selsort that Coq would accept as terminating. The amount of fuel decreased at each call, until it reached zero. Since the fuel argument was structurally decreasing, Coq accepted the definition. But it complicated the implementation of selsort and the proofs about it. Coq provides a command Function that implements a similar idea as fuel, but without requiring the function definition to be structurally recursive. Instead, the function is annotated with a measure that is decreasing at each recursive call. To activate such annotations, we need to load a library.

Now we can add a measure annotation on the definition of selsort to tell Coq that each recursive call decreases the length of l:

The measure annotation takes two parameters, a measure function and an argument name. Above, the function is length and the argument is l. The function must return a nat when applied to the argument. Coq then challenges us to prove that length applied to l is actually decreasing at every recursive call.

The proof must end with Defined instead of Qed. That ensures the function's body can be used in computation. For example, the following unit test succeeds, but try changing Defined to Qed and see how it gets stuck.

The definition of selsort' is completed by the Function command using a helper function that it generates, selsort'_terminate. Neither of them is going to be useful to unfold in proofs:

Instead, anywhere you want to unfold or simplify selsort', you should now rewrite with selsort'_equation, which was automatically defined by the Function command:

Exercise: 1 star, standard (selsort'_perm)

Hint: Follow the same strategy as selsort_perm. In our solution, there was only a one-line change.

Exercise: 1 star, standard (cons_of_small_maintains_sort')

Hint: Follow the same strategy as cons_of_small_maintains_sort'. In our solution, there was only a one-line change.

Exercise: 1 star, standard (selsort'_sorted)

Hint: Follow the same strategy as selsort_sorted. In our solution, there were only three small changes.

Exercise: 1 star, standard (selsort'_is_correct)

Finish the proof of correctness!

Selection Sort with Multisets (Optional)

This section relies on Multiset.

Let's prove the correctness of selection_sort using multisets instead of permutations. These exercises and their proofs were contributed by William Ma.

Exercise: 3 stars, standard, optional (select_contents)

Exercise: 3 stars, standard, optional (selection_sort_contents)

Exercise: 2 stars, standard, optional (sorted_iff_sorted)

Exercise: 1 star, standard, optional (selection_sort_correct')