# SelectionSelection Sort, With Specification and Proof of Correctness

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

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

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.

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.

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.

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.

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.

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.

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

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

Definition selection_sort_correct : Prop :=

is_a_sorting_algorithm selection_sort.

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.

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)

Lemma select_perm: ∀x l,

let (y,r) := select x l in Permutation (x::l) (y::r).

Proof. (* FILL IN HERE *) Admitted.

☐
let (y,r) := select x l in Permutation (x::l) (y::r).

Proof. (* FILL IN HERE *) Admitted.

#### Exercise: 3 stars, standard (selection_sort_perm)

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.

☐
∀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)

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.

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

☐
∀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)

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.

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

☐
Proof. (* FILL IN HERE *) Admitted.

Theorem selection_sort_is_correct: selection_sort_correct.

Proof.

split. apply selection_sort_perm. apply selection_sort_sorted.

Qed.

Proof.

split. apply selection_sort_perm. apply selection_sort_sorted.

Qed.

# Recursive Functions That are Not Structurally Recursive

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.

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.

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.

Lemma selsort'_perm:

∀n,

∀l, length l = n → Permutation l (selsort' l).

Proof.

(* FILL IN HERE *) Admitted.

☐
∀n,

∀l, length l = n → Permutation l (selsort' l).

Proof.

(* FILL IN HERE *) Admitted.

(* Thu May 2 14:47:51 EDT 2019 *)