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

Instance CmdMonadLaws : Monad_with_Laws NCmdMonad.Cmd.

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'))
                         y :: (inner_merge ys')

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

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

intros. apply (merge_pairs_length).

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

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.

Theorem merge_sort_corr : sort_corr merge_sort.

This page has been generated by coqdoc