SortInsertion Sort
- Sections 2.0 and 2.1 of Algorithms, Fourth Edition, by
Sedgewick and Wayne, Addison Wesley 2011; or
- Section 2.1 of Introduction to Algorithms, 3rd Edition, by Cormen, Leiserson, and Rivest, MIT Press 2009.
The Insertion-Sort Program
(* insert i l inserts i into its sorted place in list l.
Precondition: l is sorted. *)
Fixpoint insert (i : nat) (l : list nat) :=
match l with
| [] ⇒ [i]
| h :: t ⇒ if i <=? h then i :: h :: t else h :: insert i t
end.
Fixpoint sort (l : list nat) : list nat :=
match l with
| [] ⇒ []
| h :: t ⇒ insert h (sort t)
end.
Example sort_pi :
sort [3;1;4;1;5;9;2;6;5;3;5]
= [1;1;2;3;3;4;5;5;5;6;9].
Proof. simpl. reflexivity. Qed.
We won't analyze or prove anything about the efficiency of
sort. Instead, we will verify its correctness: that it produces
the correct output for a given input.
Specification of Correctness
- The empty list is sorted.
- Any single-element list is sorted.
- For any two adjacent elements, they must be in the proper order.
- Any single-element list is sorted.
Inductive sorted : list nat → Prop :=
| sorted_nil :
sorted []
| sorted_1 : ∀ x,
sorted [x]
| sorted_cons : ∀ x y l,
x ≤ y → sorted (y :: l) → sorted (x :: y :: l).
This definition might not be the most obvious. Another definition,
perhaps more familiar, might be: for any two elements of the list
(regardless of whether they are adjacent), they should be in the
proper order. Let's try formalizing that.
We can think in terms of indices into a list lst, and say: for
any valid indices i and j, if i < j then index lst i ≤
index lst j, where index lst n means the element of lst at
index n. Unfortunately, formalizing this idea becomes messy,
because any Coq implementing index must be total: it must return
some result even if the index is out of range for the list.
The Coq standard library contains two such functions:
Check nth : ∀ A : Type, nat → list A → A → A.
Check nth_error : ∀ A : Type, list A → nat → option A.
These two functions ensure totality in different ways:
If we use nth, we must ensure that indices are in range:
- nth takes an additional argument of type A --a default
value-- to be returned if the index is out of range, whereas
- nth_error returns Some v if the index is in range and None
- -an error-- otherwise.
The choice of default value, here 0, is unimportant, because it
will never be returned for the i and j we pass.
If we use nth_error, we must add additional antecedents:
Definition sorted' (al : list nat) := ∀ i j iv jv,
i < j →
nth_error al i = Some iv →
nth_error al j = Some jv →
iv ≤ jv.
Here, the validity of i and j are implicit in the fact
that we get Some results back from each call to nth_error.
All three definitions of sortedness are reasonable. In practice,
sorted' is easier to work with than sorted'' because it
doesn't need to mention the length function. And sorted is
easiest, because it doesn't need to mention indices.
Using sorted, we specify what it means to be a correct sorting
algorthm:
Definition is_a_sorting_algorithm (f: list nat → list nat) := ∀ al,
Permutation al (f al) ∧ sorted (f al).
Function f is a correct sorting algorithm if f al is
sorted and is a permutation of its input.
Proof of Correctness
Exercise: 3 stars, standard (insert_sorted)
(* Prove that insertion maintains sortedness. Make use of tactic
bdestruct, defined in Perm. *)
Lemma insert_sorted:
∀ a l, sorted l → sorted (insert a l).
Proof.
intros a l S. induction S; simpl.
(* FILL IN HERE *) Admitted.
☐
Exercise: 2 stars, standard (sort_sorted)
Exercise: 3 stars, standard (insert_perm)
Validating the Specification (Advanced)
Exercise: 4 stars, advanced (sorted_sorted')
Hint: Instead of doing induction on the list al, do induction on
the sortedness of al. This proof is a bit tricky, so you may
have to think about how to approach it, and try out one or two
different ideas.
Proof.
(* FILL IN HERE *) Admitted.
☐
(* FILL IN HERE *) Admitted.
☐
Here, you can't do induction on the sortedness of the list,
because sorted' is not an inductive predicate. But the proof
is not hard.
(* FILL IN HERE *) Admitted.
☐
☐
Proving Correctness from the Alternative Spec (Optional)
Exercise: 5 stars, standard, optional (insert_sorted')
Lemma nth_error_insert : ∀ l a i iv,
nth_error (insert a l) i = Some iv →
a = iv ∨ ∃ i', nth_error l i' = Some iv.
Proof.
(* FILL IN HERE *) Admitted.
Lemma insert_sorted':
∀ a l, sorted' l → sorted' (insert a l).
Proof.
(* FILL IN HERE *) Admitted.
☐
Theorem sort_sorted': ∀ l, sorted' (sort l).
Proof.
induction l.
- unfold sorted'. intros. destruct i; inv H0.
- simpl. apply insert_sorted'. auto.
Qed.
If you complete the proofs above, you will note that the proof of
insert_sorted is relatively easy compared to the proof of
insert_sorted', even though sorted al ↔ sorted' al. So,
suppose someone asked you to prove sort_sorted'. Instead of
proving it directly, it would be much easier to design predicate
sorted, then prove sort_sorted and sorted_sorted'.
The moral of the story is therefore: Different formulations of
the functional specification can lead to great differences in the
difficulty of the correctness proofs.
(* 2021-05-04 07:54 *)