# CS 6115 Problem Set 5

## Monads

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)

}.

Instance CmdMonad: Monad NCmdMonad.Cmd.

Admitted.

Instance CmdMonadLaws : Monad_with_Laws NCmdMonad.Cmd.

Admitted.

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.

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.

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

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

Admitted.

Lemma merge_preserves_length : forall xs ys,

(length xs + length ys) = length (merge xs ys).

Admitted.

Lemma merge_preserves_In : forall xs ys x,

In x xs \/ In x ys <-> In x (merge xs ys).

Admitted.

Lemma merge_preserves_count : forall (xs ys : list nat) x,

count xs x + count ys x = count (merge xs ys) x.

Admitted.

sorted xs -> sorted ys -> sorted (merge xs ys).

Admitted.

Lemma merge_preserves_length : forall xs ys,

(length xs + length ys) = length (merge xs ys).

Admitted.

Lemma merge_preserves_In : forall xs ys x,

In x xs \/ In x ys <-> In x (merge xs ys).

Admitted.

Lemma merge_preserves_count : forall (xs ys : list nat) x,

count xs x + count ys x = count (merge xs ys) x.

Admitted.

2. Show that
3. Show that
4. Show that
5. Define correctness for sorting and show that merge_sort is correct.

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

- 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

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

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

Admitted.

Theorem merge_sort_corr : sort_corr merge_sort.

Admitted.

This page has been generated by coqdoc