CS 6115 Problem Set 5

Monads

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

Instance CmdMonad: Monad NCmdMonad.Cmd.
Admitted.

Instance CmdMonadLaws : Monad_with_Laws NCmdMonad.Cmd.
Admitted.

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

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

Theorem merge_sort_corr : sort_corr merge_sort.
Admitted.

This page has been generated by coqdoc