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

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.

*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

end.

What happens if we run out of fuel before we reach the end
of the list? Then WE GET THE WRONG ANSWER.

What happens if we have have too much fuel? No problem.

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.

Specification of correctness of a sorting algorithm:
it rearranges the elements into a list that is totally ordered.

Inductive sorted: list nat -> Prop :=

| sorted_nil: sorted nil

| sorted_1: forall i, sorted (i::nil)

| sorted_cons: forall i j l, i <= j -> sorted (j::l) -> sorted (i::j::l).

Definition is_a_sorting_algorithm (f: list nat -> list nat) :=

forall al, Permutation al (f al) /\ sorted (f al).

NOTE: If you wish, you may Require Import Multiset and use the multiset
method, along with the theorem contents_perm. If you do,
you'll still leave the statement of this theorem unchanged.

intros x l; revert x.

induction l; intros; simpl in *.

Admitted.

NOTE: If you wish, you may Require Import Multiset and use the multiset
method, along with the theorem same_contents_iff_perm.

Lemma select_smallest_aux:

forall x al y bl,

Forall (fun z => y <= z) bl ->

select x al = (y,bl) ->

y <= x.

Proof.

Admitted.

Theorem select_smallest:

forall x al y bl, select x al = (y,bl) ->

Forall (fun z => y <= z) bl.

Proof.

intros x al; revert x; induction al; intros; simpl in *.

admit.

bdestruct (x <=? a).

*

destruct (select x al) eqn:?H.

Admitted.

forall x al y bl,

Forall (fun z => y <= z) bl ->

select x al = (y,bl) ->

y <= x.

Proof.

Admitted.

Theorem select_smallest:

forall x al y bl, select x al = (y,bl) ->

Forall (fun z => y <= z) bl.

Proof.

intros x al; revert x; induction al; intros; simpl in *.

admit.

bdestruct (x <=? a).

*

destruct (select x al) eqn:?H.

Admitted.

Lemma selection_sort_sorted_aux:

forall y bl,

sorted (selsort bl (length bl)) ->

Forall (fun z : nat => y <= z) bl ->

sorted (y :: selsort bl (length bl)).

Proof.

Admitted.

Theorem selection_sort_sorted: forall al, sorted (selection_sort al).

Proof.

intros.

unfold selection_sort.

Admitted.

forall y bl,

sorted (selsort bl (length bl)) ->

Forall (fun z : nat => y <= z) bl ->

sorted (y :: selsort bl (length bl)).

Proof.

Admitted.

Theorem selection_sort_sorted: forall al, sorted (selection_sort al).

Proof.

intros.

unfold selection_sort.

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

Require Import Recdef.

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,
before you can use the function.

Proof.

intros.

pose proof (select_perm x r).

rewrite teq0 in H.

apply Permutation_length in H.

simpl in *; omega.

Defined.

NOTE: If you wish, you may Require Import Multiset
and use the multiset method, along with the
theorem same_contents_iff_perm.
Important! Don't unfold selsort', or in general, never
unfold anything defined with Function. Instead, use the
recursion equation selsort'_equation that is automatically
defined by the Function command.

Admitted.

☐