SelectionSelection Sort

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.
(* select x l is (y, l'), where y is the smallest element
   of x :: l, and l' is all the remaining elements of x :: l. *)

Fixpoint select (x: nat) (l: list nat) : nat × list nat :=
  match l with
  | [](x, [])
  | h :: t
    if x <=? h
    then let (j, l') := select x t
         in (j, h :: l')
    else let (j, l') := select h t
         in (j, x :: l')
  end.
Selection sort should repeatedly extract the smallest element and make a list of the results. But the following attempted definition fails:
Fail Fixpoint selsort (l : list nat) : list nat :=
  match l with
  | [][]
  | x :: rlet (y, r') := select x r
            in y :: selsort r'
  end.
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.
Fixpoint selsort (l : list nat) (n : nat) : list nat :=
  match l, n with
  | _, O[] (* ran out of fuel *)
  | [], _[]
  | x :: r, S n'let (y, r') := select x r
                  in y :: selsort r' n'
end.
If fuel runs out, we get the wrong output.
Example out_of_fuel: selsort [3;1;4;1;5] 3 [1;1;3;4;5].
Proof.
  simpl. intro. discriminate.
Qed.
Extra fuel isn't a problem though.
Example extra_fuel: selsort [3;1;4;1;5] 10 = [1;1;3;4;5].
Proof.
  simpl. reflexivity.
Qed.
The exact amount of fuel needed is the length of the input list. So that's how we define selection_sort:
Definition selection_sort (l : list nat) : list nat :=
  selsort l (length l).

Example sort_pi :
  selection_sort [3;1;4;1;5;9;2;6;5;3;5] = [1;1;2;3;3;4;5;5;5;6;9].
Proof.
  unfold selection_sort.
  simpl. reflexivity.
Qed.

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.
Inductive sorted: list nat Prop :=
 | sorted_nil: sorted []
 | sorted_1: i, sorted [i]
 | sorted_cons: i j l, i j sorted (j :: l) sorted (i :: j :: l).

Hint Constructors sorted : core.

Definition is_a_sorting_algorithm (f: list nat list nat) := al,
    Permutation al (f al) sorted (f al).
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.
Example pairs_example : (a c x : nat) (b d l : list nat),
    (a, b) = (let (c, d) := select x l in (c, d))
    (a, b) = select x l.
Proof.
  intros. destruct (select x l) as [c' d'] eqn:E. auto.
Qed.

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.
Lemma select_perm: x l y r,
    select x l = (y, r) Permutation (x :: l) (y :: r).
Proof.
  (* FILL IN HERE *) Admitted.

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.
Lemma select_rest_length : x l y r,
    select x l = (y, r) length l = length r.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 3 stars, standard (selsort_perm)

Prove that if you provide sufficient fuel, selsort produces a permutation. Proceed by induction on n.
Lemma selsort_perm: n l,
    length l = n Permutation l (selsort l n).
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 1 star, standard (selection_sort_perm)

Prove that selection_sort produces a permutation.
Lemma selection_sort_perm: l,
    Permutation l (selection_sort l).
Proof.
  (* FILL IN HERE *) Admitted.

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.
Lemma select_fst_leq: al bl x y,
    select x al = (y, bl)
    y x.
Proof.
  (* FILL IN HERE *) Admitted.
To represent the concept of comparing a number to a list, we introduce a new notation:
Definition le_all x xs := Forall (fun yx y) xs.
Hint Unfold le_all : core.
Infix "<=*" := le_all (at level 70, no associativity).

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.
Lemma le_all__le_one : lst y n,
    y <=* lst In n lst y n.
Proof. (* FILL IN HERE *) Admitted.

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.
Lemma select_smallest: al bl x y,
    select x al = (y, bl)
    y <=* bl.
Proof.
  (* FILL IN HERE *) Admitted.

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.
Lemma select_in : al bl x y,
    select x al = (y, bl)
    In y (x :: al).
Proof.
  (* FILL IN HERE *) Admitted.

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.
Lemma cons_of_small_maintains_sort: bl y n,
    n = length bl
    y <=* bl
    sorted (selsort bl n)
    sorted (y :: selsort bl n).
Proof.
  (* FILL IN HERE *) Admitted.

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.
Lemma selsort_sorted : n al,
    length al = n sorted (selsort al n).
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 1 star, standard (selection_sort_sorted)

Prove that selection_sort produces a sorted list.
Lemma selection_sort_sorted : al,
    sorted (selection_sort al).
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 1 star, standard (selection_sort_is_correct)

Finish the proof of correctness!
Theorem selection_sort_is_correct :
  is_a_sorting_algorithm selection_sort.
Proof.
  (* FILL IN HERE *) Admitted.

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.
Require Import Recdef. (* needed for measure feature *)
Now we can add a measure annotation on the definition of selsort to tell Coq that each recursive call decreases the length of l:
Function selsort' l {measure length l} :=
  match l with
  | [][]
  | x :: rlet (y, r') := select x r
            in y :: selsort' r'
end.
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.
Proof.
  intros l x r HL y r' Hsel.
  apply select_rest_length in Hsel. inv Hsel. simpl. lia.
Defined.
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.
Example selsort'_example : selsort' [3;1;4;1;5;9;2;6;5] = [1;1;2;3;4;5;5;6;9].
Proof. reflexivity. Qed.
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.
Lemma selsort'_perm : n l,
    length l = n Permutation l (selsort' l).
Proof.
  (* FILL IN HERE *) Admitted.

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.
Lemma cons_of_small_maintains_sort': bl y,
    y <=* bl
    sorted (selsort' bl)
    sorted (y :: selsort' bl).
Proof. (* FILL IN HERE *) Admitted.

Exercise: 1 star, standard (selsort'_sorted)

Hint: Follow the same strategy as selsort_sorted. In our solution, there were only three small changes.
Lemma selsort'_sorted : n al,
    length al = n sorted (selsort' al).
Proof. (* FILL IN HERE *) Admitted.

Exercise: 1 star, standard (selsort'_is_correct)

Finish the proof of correctness!
Theorem selsort'_is_correct :
  is_a_sorting_algorithm selsort'.
Proof. (* FILL IN HERE *) Admitted.

Selection Sort with Multisets (Optional)

This section relies on Multiset.
From VFA Require Import 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)

Lemma select_contents : al bl x y,
  select x al = (y, bl)
  union (singleton x) (contents al) = union (singleton y) (contents bl).
Proof. (* FILL IN HERE *) Admitted.

Exercise: 3 stars, standard, optional (selection_sort_contents)

Lemma selection_sort_contents : n l,
  length l = n
  contents l = contents (selection_sort l).
Proof. (* FILL IN HERE *) Admitted.

Exercise: 2 stars, standard, optional (sorted_iff_sorted)

Lemma sorted_iff_sorted : l, sorted l Sort.sorted l.
Proof. (* FILL IN HERE *) Admitted.

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

Theorem selection_sort_correct' :
  is_a_sorting_algorithm' selection_sort.
Proof. (* FILL IN HERE *) Admitted.
(* 2023-08-23 11:34 *)