```{-
Computer Aided Formal Reasoning (G53CFR, G54CFR)
Peter Morris

Lecture 17: Merge Sort (II)

In Merge.agda, we wrote a naive sorting algorithm that we might write in
Haskell, but Agda didn't beleive that it was terminating. If we want to
verify this algorithm as 'correct' we must first prove it is terminating.

To do this, we observe that sorting proceeds in 2 phases. In the 1st
the input list is repeatedly 'dealt' in to two roughly even length lists until
the constituent lists are of length 1 (which we know, trivially, to be
sorted). We observed this 1st stage amounts to building a balance tree of
numbers.

The second stage amounts to repeatedly merging this tree back into a single
list. We shall now see that by exposing the tree built from the 1st stage, we
can  show that our algorithm terminates.

-}

module l17ii where

open import Data.List
open import Data.Nat
open import Data.Product

data Order : Set where le gt : Order

order : ℕ → ℕ → Order
order zero n = le
order (suc m) zero = gt
order (suc m) (suc n) = order m n

mutual
merge : List ℕ → List ℕ → List ℕ
merge [] ns = ns
merge (m ∷ ms) [] = m ∷ ms
merge (m ∷ ms) (n ∷ ns) with order m n
...                     | le = m ∷ merge ms (n ∷ ns)
...                     | gt = n ∷ merge' m ms ns

merge' : ℕ → List ℕ → List ℕ → List ℕ
merge' m ms [] = m ∷ ms
merge' m ms (n ∷ ns) with order m n
...                  | le = m ∷ merge ms (n ∷ ns)
...                  | gt = n ∷ merge' m ms ns

{-
We define another copy of the Booleans, which we will use to store information
on the balancing of the tree, p0 will denoted a tree with as many elements in
the left sub tree as the right. And p1 will denote a tree where there is one
more bit of payload in the left hand tree as in the right.

Trees are then empty, leaves, or nodes with parity information:
-}

data Parity : Set where p0 p1 : Parity

data DealT (X : Set) : Set where
empT : DealT X
leafT : X → DealT X
nodeT : Parity → DealT X → DealT X → DealT X

{-
We explain how to insert a new bit of payload into a tree, in the node case
we decide where to put the new data by looking at the parity bit. if it is p0
we insert in the left and return a tree with parity p1. If it is p1 we
insert on the right and return a p0 (balanced) tree:
-}

insert : {X : Set} → X → DealT X → DealT X
insert x empT = leafT x
insert x (leafT y) = nodeT p0 (leafT y) (leafT x)
insert x (nodeT p0 l r) = nodeT p1 (insert x l) r
insert x (nodeT p1 l r) = nodeT p0 l (insert x r)

{-
'Dealing' then amounts to repeated inserting into a balanced tree, note
that this operation differs from the previous deal in that it performs _all_
the dealing in one go.
-}

deal : List ℕ → DealT ℕ
deal [] = empT
deal (n ∷ ns) = insert n (deal ns)

{-
We now explain how to turn a tree into a sorted list by recursively merging
the sub trees:
-}

mergeT : DealT ℕ → List ℕ
mergeT empT = []
mergeT (leafT n) = [ n ]
mergeT (nodeT p l r) = merge (mergeT l) (mergeT r)

{-
Our sorting algorithm then proceeds by first building and then recursively
merging a tree.

Hopefully you can observe that this is equivalent to the naive implementation
but now Agda can see that it terminates:
-}

sort : List ℕ → List ℕ
sort ns = mergeT (deal ns)

ex1 : List ℕ
ex1 = 5 ∷ 2 ∷ 0 ∷ 1 ∷ 4 ∷ 3 ∷ []

ex2 : List ℕ
ex2 = 100 ∷ 1 ∷ 10 ∷ 1 ∷ 100 ∷ 10 ∷ []

```