# SelectionSelection Sort

From VFA Require Import Perm.

Hint Constructors Permutation.

From Coq Require Export Lists.List. (* for exercise involving List.length *)

# The Selection-Sort Program

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

Coq rejects selsort because it doesn't satisfy Coq's
requirements for termination. The problem is that the recursive
call in selsort is not
There are severals ways to fix this problem. One programming
pattern is to provide

*structurally decreasing*: the argument r' at the call site is not known to be a smaller part of the original input l. Indeed, select might not return such a list. For example, select 1 [0; 2] is (0, [1; 2], but [1; 2] is not a part of [0; 2].*fuel*: an extra argument that has no use in the algorithm except to bound the amount of recursion. The n argument, below, is the fuel. When it reaches 0, the recursion terminates.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.

Extra fuel isn't a problem though.

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

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 the following exercises, you will prove that selection sort
is a correct sorting algorithm. You might wish to keep track
of the lemmas you have proved, so that you can spot places to
use them later.
Depending on the path you have followed through

*Software Foundations*it might have been awhile since you have worked with pairs. Here's a brief reminder of how destruct can be used to break a pair apart into its components. A similar technique will be needed in many of the following proofs.
Example pairs_example : ∀ (a c x : nat) (b d l : list nat),

(a, b) = (let (c, d) := select x l in (c, d)) →

(a, b) = select x l.

Proof.

intros. destruct (select x l) eqn:E. auto.

Qed.

(a, b) = (let (c, d) := select x l in (c, d)) →

(a, b) = select x l.

Proof.

intros. destruct (select x l) eqn:E. auto.

Qed.

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

☐

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

Lemma selsort_perm: ∀ n l,

length l = n → Permutation l (selsort l n).

Proof.

(* FILL IN HERE *) Admitted.

☐

Lemma selection_sort_perm: ∀ l,

Permutation l (selection_sort l).

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 2 stars, standard (select_rest_length)

Lemma select_rest_length : ∀ x l y r,

select x l = (y, r) → length l = length r.

Proof.

(* FILL IN HERE *) Admitted.

☐

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

Lemma select_fst_leq: ∀ al bl x y,

select x al = (y, bl) →

y ≤ x.

Proof.

(* FILL IN HERE *) Admitted.

☐

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

Definition le_all x xs := Forall (fun y ⇒ x ≤ y) xs.

Infix "<=*" := le_all (at level 70, no associativity).

Proceed by induction on al.

Lemma select_smallest: ∀ al bl x y,

select x al = (y, bl) →

y <=* bl.

Proof.

(* FILL IN HERE *) Admitted.

☐

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

Lemma select_in : ∀ al bl x y,

select x al = (y, bl) →

In y (x :: al).

Proof.

(* FILL IN HERE *) Admitted.

☐

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

Lemma cons_of_small_maintains_sort: ∀ bl y n,

n = length bl →

y <=* bl →

sorted (selsort bl n) →

sorted (y :: selsort bl n).

Proof.

(* FILL IN HERE *) Admitted.

☐

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

Lemma selsort_sorted : ∀ n al,

length al = n → sorted (selsort al n).

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 1 star, standard (selection_sort_sorted)

Lemma selection_sort_sorted : ∀ al,

sorted (selection_sort al).

Proof.

(* FILL IN HERE *) Admitted.

☐

Theorem selection_sort_is_correct :

is_a_sorting_algorithm selection_sort.

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 5 stars, advanced, optional (selection_sort_is_correct_multiset)

(* From VFA Require Import Multiset. *)

☐

# Recursive Functions That are Not Structurally Recursive

*measure*that is decreasing at each recursive call. To activate this experimental command, we need to load a library.

Now we can add a measure annotation on the definition of
selsort to tell Coq that each recursive call decreases the
length of l:

Function selsort' l {measure length l} :=

match l with

| [] ⇒ []

| x :: r ⇒ let (y, r') := select x r

in y :: selsort' r'

end.

The measure annotation takes two parameters, a measure
function and an argument name. Above, the function is length
and the argument is l. The function must return a nat when
applied to the argument. Coq then challenges us to prove that
length applied to l is actually decreasing at every recursive
call.

Proof.

intros.

assert (Hperm: Permutation (x :: r) (y :: r')).

{ apply select_perm. auto. }

apply Permutation_length in Hperm.

inv Hperm. simpl. omega.

Defined.assert (Hperm: Permutation (x :: r) (y :: r')).

{ apply select_perm. auto. }

apply Permutation_length in Hperm.

inv Hperm. simpl. omega.

The proof must end with Defined instead of Qed. That
ensures the function's body can be used in computation. For
example, the following unit test succeeds, but try changing
Defined to Qed and see how it gets stuck.

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:

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

#### Exercise: 2 stars, standard (selsort'_perm)

Lemma selsort'_perm : ∀ n l,

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

Proof.

(* FILL IN HERE *) Admitted.

☐

#### Exercise: 5 stars, advanced, optional (selsort'_correct)

(* Mon May 11 15:03:15 EDT 2020 *)