SelectionSelection 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.

From VFA Require Import Perm.
Hint Constructors Permutation.
From Coq Require Export Lists.List. (* for exercise involving List.length *)

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
in their original order. *)

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.
The problem is that the recursive call in selsort is not structurally decreasing.
One solution is to use fuel:

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

The specification, repeated from Sort:

Inductive sorted: list natProp :=
| sorted_nil: sorted []
| sorted_1: i, sorted [i]
| sorted_cons: i j l, ijsorted (j :: l) → sorted (i :: j :: l).

Hint Constructors sorted.

Definition is_a_sorting_algorithm (f: list natlist nat) := al,
Permutation al (f al) ∧ sorted (f al).
In a series of exercises, you will prove the correctness of selection sort.

Exercise: 3 stars, standard (select_perm)

Lemma select_perm: x l y r,
(y, r) = select x lPermutation (x :: l) (y :: r).
Proof.
(* FILL IN HERE *) Admitted.
...skipping many exercises...

Exercise: 1 star, standard (selection_sort_is_correct)

Theorem selection_sort_is_correct :
is_a_sorting_algorithm selection_sort.
Proof.
(* FILL IN HERE *) Admitted.

Recursive Functions That are Not Structurally Recursive

An experimental Function command in Coq enables defining recursive functions that are not structurally recursive, but instead have a decreasing measure.

Require Import Recdef. (* needed for measure feature *)

Function selsort' l {measure length l} :=
match l with
| [] ⇒ []
| x :: rlet (y, r') := select x r
in y :: selsort' r'
end.
Annotation measure length l means the length of l must decrease at each call. Which we must prove.

Proof.
intros.
assert (Hperm: Permutation (x :: r) (y :: r')).
{ apply select_perm. auto. }
apply Permutation_length in Hperm.
inv Hperm. simpl. omega.
Defined.
Defined makes the function usable in computation.

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:

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

Check selsort'_equation.