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 :: tif i <=? h then i :: h :: t else h :: insert i t

Fixpoint sort (l : list nat) : list nat :=
  match l with
  | [] ⇒ []
  | h :: tinsert h (sort t)

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 natProp :=
| sorted_nil:
    sorted []
| sorted_1: x,
    sorted [x]
| sorted_cons: x y l,
    xysorted (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 natlist 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).
(* FILL IN HERE *) Admitted.

Exercise: 3 stars, standard (sort_perm)

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

Exercise: 1 star, standard (insertion_sort_correct)

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