(** * Selection: Selection 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: forall i, sorted [i]
| sorted_cons: forall 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) := forall 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: forall 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.