SelectionSelection Sort, With Specification and Proof of Correctness

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


Require Export Coq.Lists.List.
From VFA Require Import Perm.
Find (and delete) the smallest element in a list.
Fixpoint select (x: nat) (l: list nat) : nat * list nat :=
match l with
| nil ⇒ (x, nil)
| 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.
Now, selection-sort works by repeatedly extracting the smallest element, and making a list of the results. But the following attempted definition fails:
Fail Fixpoint selsort l :=
match l with
| i::r ⇒ let (j,r') := select i r
        in j :: selsort r'
| nil ⇒ nil
end.
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.
Fixpoint selsort l n {struct n} :=
match l, n with
| x::r, S n' ⇒ let (y,r') := select x r
              in y :: selsort r' n'
| nil, _ ⇒ nil
| _::_, O ⇒ nil (* Oops!  Ran out of fuel! *)
end.
What happens if we run out of fuel before we reach the end of the list? Then WE GET THE WRONG ANSWER.
Example out_of_gas: selsort [3;1;4;1;5] 3 ≠ [1;1;3;4;5].
Proof.
simpl.
intro.
discriminate.
Qed.
What happens if we have have too much fuel? No problem.
Example too_much_gas: selsort [3;1;4;1;5] 10 = [1;1;3;4;5].
Proof.
simpl.
reflexivity.
Qed.
The selection_sort algorithm provides just enough fuel.
Definition selection_sort l := 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.
Now we repeat (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 nil
 | sorted_1: ∀i, sorted (i::nil)
 | sorted_cons: ∀i j l, i ≤ j → sorted (j::l) → sorted (i::j::l).
Definition is_a_sorting_algorithm (f: list nat → list nat) :=
  ∀al, Permutation al (f al) ∧ sorted (f al).

Proof of Correctness of Selection sort

Here's what we want to prove.
Definition selection_sort_correct : Prop :=
    is_a_sorting_algorithm selection_sort.
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.
(* Require Import Multiset. *)
We'll start by working on part 1, permutations.
First, let's prove that select gives us back a permutation of its input.
Local Hint Constructors Permutation.
Lemma select_perm': ∀x l y r,
  (y, r) = select x l → Permutation (x :: l) (y :: r).
Proof. (* WORKED IN CLASS *)
  intros x l. generalize dependent x.
  induction l as [ | h t]; intros x y r Hsel; simpl in Hsel.
  - inversion Hsel. subst. auto.
  - bdestruct (x <=? h).
    + destruct (select x t) as (j, l') eqn:Hd. inversion Hsel. subst. eauto.
    + destruct (select h t) as (j, l') eqn:Hd. inversion Hsel. subst. eauto.
Qed.

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

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.
Lemma selsort_perm:
  ∀n,
  ∀l, length l = n → Permutation l (selsort l n).
Proof. (* FILL IN HERE *) Admitted.
Theorem selection_sort_perm:
  ∀l, Permutation l (selection_sort l).
Proof. (* FILL IN HERE *) Admitted.
☐

Exercise: 3 stars, standard (select_smallest)

Hints: You do not need induction. Helpful lemmas include select_perm and Forall_perm.
Lemma select_smallest_aux:
  ∀x al y bl,
    Forall (fun z ⇒ y ≤ z) bl →
    select x al = (y,bl) →
    y ≤ x.
Proof. (* FILL IN HERE *) Admitted.
Hint: Induct on al, but leave x universally quantified in the inductive hypothesis.
Theorem select_smallest:
  ∀x al y bl, select x al = (y,bl) →
     Forall (fun z ⇒ y ≤ z) bl.
Proof. (* FILL IN HERE *) Admitted.
☐

Exercise: 3 stars, standard (selection_sort_sorted)

Hint: You do not need induction. Helpful lemmas include selsort_perm and Forall_perm.
Lemma selection_sort_sorted_aux:
  ∀y bl,
   sorted (selsort bl (length bl)) →
   Forall (fun z : nat ⇒ y ≤ z) bl →
   sorted (y :: selsort bl (length bl)).
Proof.
 (* FILL IN HERE *) Admitted.
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.
Theorem selection_sort_sorted: ∀al, sorted (selection_sort al).
Proof. (* FILL IN HERE *) Admitted.
☐
Now we wrap it all up.
Theorem selection_sort_is_correct: selection_sort_correct.
Proof.
split. apply selection_sort_perm. apply selection_sort_sorted.
Qed.

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.
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'
| nil ⇒ nil
end.
When you use Function with measure, it's your obligation to prove that the measure actually decreases.
Proof.
intros.
pose proof (select_perm x r).
rewrite teq0 in H.
apply Permutation_length in H.
simpl in *.
omega.
Defined.
The proof must end with Defined instead of Qed, otherwise you can't compute with the function in Coq.
Compute selsort' [3;1;4;1;5;9;2;6;5].
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.
Check selsort'_equation.

Exercise: 3 stars, standard (selsort'_perm)

Hint: Follow the same strategy as selsort_perm.
Lemma selsort'_perm:
  ∀n,
  ∀l, length l = n → Permutation l (selsort' l).
Proof.
(* FILL IN HERE *) Admitted.
☐
(* Thu May 2 14:47:51 EDT 2019 *)