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

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

    Reply
  2. Shin Post author

    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.

    Reply

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>