# CS 6115 Problem Set 5

In lecture we modeled commands of type t as functions that take a heap and return an optional pair of a heap and a t. So this is really a combination of the state and option monad:

Definition Cmd(t:Type) := heap -> option(heap*t).

Definition ret t (x:t) : Cmd t := fun h => Some (h,x).

Definition bind t u (c : Cmd t) (f : t -> Cmd u) : Cmd u :=
fun h1 =>
match c h1 with
| None => None
| Some (h2,v) => f v h2
end.
0. Prove that this monad satisfies the monad laws:

Class Monad (M:Type -> Type) :=
{
ret : forall {A:Type}, A -> M A ;
bind : forall {A B:Type}, M A -> (A -> M B) -> M B
}.

Class Monad_with_Laws (M: Type -> Type) {MonadM : Monad M} :=
{
m_left_id : forall {A B:Type} (x:A) (f:A -> M B), bind (ret x) f = f x ;
m_right_id : forall {A B:Type} (c:M A), bind c ret = c ;
m_assoc : forall {A B C} (c:M A) (f:A->M B) (g:B -> M C),
bind (bind c f) g = bind c (fun x => bind (f x) g)
}.

## Algorithmic correctness

In lecture we defined a merge sort function merge_sort:

Fixpoint merge (xs:list nat) : list nat -> list nat :=
match xs with
| nil => fun ys => ys
| (x::xs') =>
(fix inner_merge (ys:list nat) : list nat :=
match ys with
| nil => x::xs'
| y::ys' => if nat_lte x y then
x :: (merge xs' (y::ys'))
else
y :: (inner_merge ys')
end)
end.

Fixpoint merge_pairs (xs:list (list nat)) : list (list nat) :=
match xs with
| h1::h2::t => (merge h1 h2) :: (merge_pairs t)
| xs' => xs'
end.

Merges a bunch of sorted lists into one sorted list.
Function merge_iter (xs: list (list nat)) { measure length xs } : list nat :=
match xs with
| nil => nil
| h::nil => h
| h1::h2::xs' => merge_iter (merge_pairs (h1::h2::xs'))
end.

intros. apply (merge_pairs_length).
Defined.

Turns a list into a list of singleton lists of the elements.
Definition make_lists (xs:list nat) : list (list nat) :=
List.map (fun x => x::nil) xs.

Returns input list sorted into ascending order.
Definition merge_sort (xs:list nat) :=
merge_iter (make_lists xs).

But does it work?

Definition list_all {A:Type} (P:A->Prop) (xs:list A) : Prop :=
fold_right (fun h t => P h /\ t) True xs.

Fixpoint sorted (xs:list nat) : Prop :=
match xs with
| [] => True
| h::t => sorted t /\ list_all (le h) t
end.

Definition count := count_occ nat_eq.

1. Show that
• a. sorted xs -> sorted ys -> sorted (merge xs ys)
• b. length xs + length ys = length (merge xs ys)
• c. (x is in xs or ys) iff (x is in merge xs ys)
• d. The number of occurrences of x in merge xs ys = the total number of occurrences in xs and ys.
Lemma merge_preserves_sorted : forall xs ys,
sorted xs -> sorted ys -> sorted (merge xs ys).

Lemma merge_preserves_length : forall xs ys,
(length xs + length ys) = length (merge xs ys).

Lemma merge_preserves_In : forall xs ys x,
In x xs \/ In x ys <-> In x (merge xs ys).

Lemma merge_preserves_count : forall (xs ys : list nat) x,
count xs x + count ys x = count (merge xs ys) x.

2. Show that
• a. list_all sorted xs -> list_all sorted (merge_pairs xs)
• b. (sum of lengths of lists in xs) = (sum of lengths of lists in merge_pairs xs)
• c. (the occurrences of x in the lists in xs) = (the occurrences of x in the lists in merge_pairs xs)
3. Show that
• a. list_all sorted xs -> sorted (merge_iter xs)
• b. (sum of lengths of lists in xs) = length of merge_iter xs
• c. (the occurrences of x in the lists in xs) = the occurrences of x in merge_iter xs
4. Show that
• a. make_lists xs is sorted
• b. length xs = (sum of the lengths of the lists in make_lists xs)
• c. count xs x = (occurrences of x in the lists in make_lists xs)
5. Define correctness for sorting and show that merge_sort is correct.

Definition sort_corr (algorithm: list nat -> list nat) : Prop.