# Agda Exercise: Proving that Mergesort Returns Ordered Lists

Continuing with my Adga programming practice. This time I am implementing the example in another section of Why Dependent Types Matter by Altenkirch, McBride, and McKinna in Agda: proving that mergesort returns an ordered list.

``````
> module Main where

> open import Prelude
> open import Data.Nat hiding (_≤_)
> open import Data.List
``````

### Order

To begin with, a term of type `m ≤ n` is a proof that a natural number `m` is at most `n`:

``````
> data _≤_ : Nat -> Nat -> Set where
>  le0 : {n : Nat} -> zero ≤ n
>  le1 : {m n : Nat} -> m ≤ n -> (1 + m) ≤ (1 + n)
``````

An auxiliary function `weaken`, which I will need later, weakens a proof of `(1+m) ≤ n` to a proof of `m ≤ n`:

``````
> weaken : {y x : Nat} -> (1 + y) ≤ x -> y ≤ x
> weaken (le1 le0) = le0
> weaken (le1 (le1 p)) = le1 (weaken (le1 p))
``````

Given two natural numbers `m` and `n`, the function `order`, to be defined later, determines their order by returning a proof. The proof has to be wrapped in a datatype `Order`:

``````
> data Order : Nat -> Nat -> Set where
>   leq : {m n : Nat} -> m ≤ n -> Order m n
>   gt : {m n : Nat} -> (1 + n) ≤ m -> Order m n
``````

Agda does not provide a generic `case` expression, so I have to define my own for `Order`:

``````
> caseord : {m n : Nat} {a : Set} -> Order m n
>             -> ((m ≤ n) -> a) -> (((1 + n) ≤ m) -> a) -> a
> caseord (leq p) f g = f p
> caseord (gt p) f g = g p
``````

The function `order` can thus be defined by:

``````
> order : (m : Nat) -> (n : Nat) -> Order m n
> order zero n = leq le0
> order (suc m) zero = gt (le1 le0)
> order (suc m) (suc n) =
>   caseord (order m n) (leq ∘ le1) (gt ∘ le1)
``````

### Ordered List

There are many ways one can express the property that a list is sorted. The choice depends on what one needs for the proof. To prove that `merge` sorts the list, Altenkirch, McBride, and McKinna suggests the following “external bound” representation of sortedness:

``````
> data OList : Nat -> Set where
>   Nil : {b : Nat} -> OList b
>   Cons : {b : Nat} -> (x : Nat) -> (b ≤ x) -> OList x -> OList b
``````

The datatype `OList b` represents a sorted list of natural numbers whose elements are all greater than or equal to the bound `b`. The bound, however, is supplied externally and need not be precise. Every sorted list of natural numbers has type `OList 0`, for instance. The `Cons` constructor demands that the newly added element `x` is bounded by the externally supplied bound `b`, and that the tail can be bounded by `x`.

### Merging Sorted Lists

With `OList`, `merge` can be verified very easily:

``````
> merge : {b : Nat} -> OList b -> OList b -> OList b
> merge Nil ys = ys
> merge xs Nil = xs
> merge (Cons x blex xs) (Cons y bley ys) =
>   caseord (order x y)
>     (\\ xley -> Cons x blex (merge {x} xs (Cons y xley ys)))
>     (\\ pylex -> Cons y bley (merge {y} (Cons x (weaken pylex) xs) ys))
``````

Note, for example, that `Cons y bley ys : OList b` is updated to `Cons y xley ys : OList x` simply by using a different proof.

### Mergesort

The rest are just some routine code: dealing elements to a tree, and perform successive merging by a fold on the tree. Mergesort is defined by `mergeT ∘ dealT`. The code below is similar to that in my previous blog entry, but without the size constraint.

``````
> data Parity : Set where
>   Even : Parity
>   Odd : Parity

> data Tree (a : Set) : Set where
>   Nul : Tree a
>   Tip : a -> Tree a
>   Bin : Parity -> Tree a -> Tree a -> Tree a

> foldT : {a b : Set}
>           -> (Parity -> b -> b -> b)
>           -> (a -> b)
>           -> b
>           -> Tree a -> b
> foldT f g e Nul = e
> foldT f g e (Tip x) = g x
> foldT f g e (Bin p t u) = f p (foldT f g e t) (foldT f g e u)

> insert : {a : Set} -> a -> Tree a -> Tree a
> insert x Nul = Tip x
> insert x (Tip y) = Bin Even (Tip x) (Tip y)
> insert x (Bin Even t u) =
>    Bin Odd (insert x t) u
> insert x (Bin Odd t u) =
>    Bin Even t (insert x u)

> dealT : List Nat -> Tree Nat
> dealT = foldr insert Nul

> mergeT : Tree Nat -> OList 0
> mergeT = foldT (\p xs ys -> merge xs ys)
>                (\x -> Cons x le0 Nil)
>                Nil

> msort : List Nat -> OList 0
> msort = mergeT ∘ dealT
``````

### 2 thoughts on “Agda Exercise: Proving that Mergesort Returns Ordered Lists”

1. newsh (sorry for the late response),

I think OList is a sorted list. Consider xs : OList 0. If xs is Nil, it is sorted. If xs equals, say, Cons 3 0≤3 ys, the tail ys must have type OList 3. Thus ys is lower-bounded by 3, not 0.

2. I think this only proves that the resulting list has a lower bound. You can construct arbitrary (unordered) lists of type (OList 0). The only restriction is that all elements are >= 0 (which is true by the definition of >=).