module l19 where

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

Lecture 19: Merge Sort (IV)

As a final trick with our Merge Sort algorithm, we will show that the output
of the sort function is a _sorted_ list. To do this we must first define what
it is to be a sorted list. For clarity we shall lose the size indicies, though
it's straight forward to combine the two proofs and show the output to be
sorted, and of the right size:

-}

open import Data.List
open import Data.Nat hiding (_≤_ ; _<_)
open import Data.Product

{-

The first change is that we will now want proofs of the ordering between the
numbers we are sorting. So let's bring back the inductive definition of _≤_
you've used before, and the proof that it is transitive:

-}

data _≤_ :     Set where
z≤n :  {n}                  zero   n
s≤s :  {m n} (m≤n : m  n)  suc m  suc n

trans≤ :  {m n o}  m  n  n  o  m  o
trans≤ z≤n q = z≤n
trans≤ (s≤s m≤n) (s≤s n≤o) = s≤s (trans≤ m≤n n≤o)

{-

We will also want _<_ and a proof that if m < n the m ≤ n:

-}

_<_ :     Set
m < n = suc m  n

<implies≤ :  {m n}  m < n  m  n
<implies≤ {zero} (s≤s m≤n) = z≤n
<implies≤ {suc m} (s≤s m≤n) = s≤s (<implies≤ m≤n)

{-

Now we adapt our order type to talk about the numbers we are sorting,
Order m n is _either_ a proof that m ≤ n or the n < m:

-}

data Order :     Set where
le : {m n : }  m  n  Order m n
gt : {m n : }  n < m  Order m n

{-

And our function order must now produce the proof object so, in the recursive
case we must inspect the recursive call:

-}

order : (m n : )  Order m n
order zero n = le z≤n
order (suc m) zero = gt (s≤s z≤n)
order (suc m) (suc n) with order m n
... | le p = le (s≤s p)
... | gt q = gt (s≤s q)

{-

Before we continue we must explain what an order list is, and to do so we must
index our lists by their lower bound, a natural number which is ≤ all the
elements in the list. (For simplicity we have fixed the element type of OList
to ℕ)

-}

data OListℕ :   Set where
{- The empty list is ordered and can have _any_ lower bound -}
[] : {b : }  OListℕ b
{- To add an element, we must produce a proof that it is not smaller than the
lower bound. Note that the head element the serves as the lower bound for
the rest of the list: -}
_-_∷_ : {b : }  (n : )  b  n  OListℕ n  OListℕ b

{-

We can throw away the proofs, to recover a normal list:

-}

fog : {b : }  OListℕ b  List
fog [] = []
fog (n - _  ns) = n  fog ns

{-

The type of the merge function now expresses the fact that it takes two
sorted lists and produces a sorted list as a result, note that the result of
the order function provides the proofs that we need to show that the reult
list is in fact sorted:

-}

mutual
merge : {b : }  OListℕ b  OListℕ b  OListℕ b
merge [] ns = ns
merge (m - p  ms) [] = m - p  ms
merge (m - p  ms) (n - q  ns) with order m n
... | le p' = m - p  merge ms (n - p'  ns)
... | gt q' = n - q  merge' m (<implies≤ q') ms ns

merge' : {b : } (m : )  b  m  OListℕ m  OListℕ b  OListℕ b
merge' m p ms [] = m - p  ms
merge' m p ms (n - q  ns) with order m n
... | le p' = m - p  merge ms (n - p'  ns)
... | gt q' = n - q  merge' m (<implies≤ q') ms ns

{-

Recall that the trees we build are not sorted in this algortihm, so the code
for this part remains unchanged:

-}

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

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)

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

{-

But now when we merge a tree, or sort a list the result is an ordered list.
(Note that we are able to use 0 as the default lower bound only because ℕ has
0 as its least element - we could not do this, for instance, if we were
sorting integers)

-}

mergeT : DealT   OListℕ 0
mergeT empT = []
mergeT (leafT n) =  n - z≤n  []
mergeT (nodeT p l r) = merge (mergeT l) (mergeT r)

sort : List   OListℕ 0
sort ns = mergeT (deal ns)

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

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