SelectionSelection Sort, With Specification and Proof of Correctness
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.
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.
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. (* WORK IN CLASS *) Admitted.
Lemma select_perm': ∀x l y r,
(y, r) = select x l → Permutation (x :: l) (y :: r).
Proof. (* WORK IN CLASS *) Admitted.
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.