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