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 :: r ⇒ let (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 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.
Definition is_a_sorting_algorithm (f: list nat → list 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 l → Permutation (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 :: r ⇒ let (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.