SortInsertion Sort

Sorting can be done in expected O(N log N) time by various algorithms (quicksort, mergesort, heapsort, etc.). But for smallish inputs, a simple quadratic-time algorithm such as insertion sort can actually be faster. It's certainly easier to implement -- and to verify.

The Insertion-Sort Program

Insertion sort on lists instead of arrays:

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

Specification of Correctness

When is a list sorted?

The empty list is sorted.
- Any single-element list is sorted.
- For any two adjacent elements, they must be in the proper order.

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

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

Proof of Correctness

In a series of exercises, you will prove the correctness of insertion sort.

Exercise: 2 stars, standard (sort_sorted)

Theorem sort_sorted: ∀ l, sorted (sort l).
Proof.
(* FILL IN HERE *) Admitted.
☐

Exercise: 3 stars, standard (sort_perm)

Theorem sort_perm: ∀ l, Permutation l (sort l).
Proof.
(* FILL IN HERE *) Admitted.
☐

Exercise: 1 star, standard (insertion_sort_correct)

Theorem insertion_sort_correct:
is_a_sorting_algorithm sort.
Proof.
(* FILL IN HERE *) Admitted.
☐