Mergesort

This exercise is taken from Conor McBride's tutorial on Epigram

Sorting

First, specify sorting lists of natural numbers through a predicate :
sort : list nat -> list nat -> Prop.

Merging

Define a function merge: list nat -> list nat -> list nat such that the following lemma holds :
Lemma merge_and_sort : forall l l', sorted l -> sorted l' ->
                                    sort (l++l') (merge l l').
Prove this property.

Balanced binary trees

Consider the type of binary trees whose nodes are labeled in type N and leaves in type L:
Inductive tree(N L:Type):Type :=
  Leaf : L -> tree N L
| Node : N -> tree N L -> tree N L -> tree N L.
We now consider trees whose nodes contain boolean values and leaves an optional value of type L, i.e trees of type tree bool (option L).
Complete the following definition:
(* A (bool,option L) tree is balanced if every node labeled with true has 
   the same number of leaves labeled with L in both subtrees, and every
   node labeled with false has one more leave labeled with L in its left son
   than its right son *)

Inductive  balanced(L:Type): tree bool (option L) -> nat -> Prop :=

Insertion in a balanced tree

Define a function :
insert (L:Type): L ->  tree bool (option L)) ->  tree bool (option L)
such that the insertion of l:L into a balanced tree ressults in a balanced tree

Building a balanced tree from a list

Define a function
share (L:Type) : L -> tree bool (option L)
such that share _ ls returns a balanced tree contianing all the elements of ls

mergesort itself

We now have all material for building a sorting function
mergesort : list nat -> list nat
  1. let l be a list of natural numbers
  2. build a balanced tree whose leaves are labled with the elements of l
  3. flatten this tree, using merge> to combine the leaves of the left and right subtrees
Prove the theorem:
Theorem mergesort_ok : forall l, sort l (mergesort l).

Solution

Follow this link
Going home