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

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.

What Sedgewick/Wayne and Cormen/Leiserson/Rivest don't acknowlege
is that the arrays-and-swaps model of sorting is not the only one
in the world. We are writing
As usual with functional lists, the output of sort may share
memory with the input. For example:

*functional programs*, where our sequences are (typically) represented as linked lists, and where we do*not*destructively splice elements into those lists.
The tail of this list, 12 :: 14 :: 18 :: [], is not disturbed or
rebuilt by the insert algorithm. The head 1 :: 3 :: 4 :: 7 :: ...
contains new nodes constructed by insert. The first three nodes
of the old list, 1 :: 3 :: 4 :: ..., will likely be
garbage-collected if no other data structure is still pointing at
them. Thus, in this typical case,
where X and Y are constants, independent of the length of the
tail. The value Y is the number of bytes in one list node: 2 to 4
words, depending on how the implementation handles
constructor-tags. We write (4-3) to indicate that four list nodes
are constructed, while three list nodes become eligible for
garbage collection.
We will not prove such things about the time and space cost, but
they are true anyway, and we should keep them in consideration.

- Time cost = 4X
- Space cost = (4-3)Y = Y

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

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

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.

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

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.

☐

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 less tricky than the previous.

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

☐

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 H

- simpl. apply insert_sorted'. auto.

Qed.

Proof.

induction l.

- unfold sorted'. intros. destruct i; inv H

_{0}.- 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*.
(* 2023-08-23 11:34 *)