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

Fixpoint sort (l : list nat) : list nat :=
match l with
| [] ⇒ []
| h :: tinsert 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 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).
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.