{-
Computer Aided Formal Reasoning (G53CFR, G54CFR)
Peter Morris
Lecture 18: Merge Sort (III)
In the last lecture, we showed that our Merge Sort implementation was
terminating. Now we will try to show that sorting preserves the size of the
input list. We do this by adapting the implementation to use Vectors, rather
than plain Lists. By doing so we can also ensure that the Tree we build
is balanced, and therefore our algorithm has the right time complexity.
-}
module l18 where
open import Algebra
open import Data.Vec
open import Data.Nat
open import Data.Nat.Properties
private
module ℕ = CommutativeSemiring commutativeSemiring
open import Data.Product
open import Relation.Binary.PropositionalEquality
import Algebra.RingSolver.AlmostCommutativeRing as ACR
import Algebra.RingSolver.Simple as Solver
open Solver (ACR.fromCommutativeSemiring commutativeSemiring)
zeroLem : (n : ℕ) → n ≡ n + 0
zeroLem = solve 1 (\n → n := n :+ con 0) refl
sucLem₁ : (m n : ℕ) → (1 + (m + n)) ≡ (m + (1 + n))
sucLem₁ = solve 2 (\m n → con 1 :+ (m :+ n) := m :+ (con 1 :+ n)) refl
sucLem₂ : (m n : ℕ) → (m + (1 + n)) ≡ (1 + (m + n))
sucLem₂ m n = sym (sucLem₁ m n)
{-
Ordering things doesn't talk about size, so this code stays the same:
-}
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
{-
However, merge, does talk about size, here we must ensure that if we merge
two vectors, then the result as as many elements as both lists added together:
-}
mutual
merge : {m n : ℕ} → Vec ℕ m → Vec ℕ n → Vec ℕ (m + n)
merge [] ns = ns
{-
In the first base case (above), everything works, in the second (below)
though, we have to fixe up the types since ms has type Vec ℕ lm and the in
hole we need something of type Vec ℕ (lm + 0), so we use subst to coerce
between these types
-}
merge {suc lm} {zero} (m ∷ ms) [] = m ∷ subst (Vec ℕ) (zeroLem lm) ms
merge {suc lm} {suc ln} (m ∷ ms) (n ∷ ns) with order m n
... | le = m ∷ merge ms (n ∷ ns)
{-
Again, in the 2nd recursive case, we must appeal to subst to fix up the types
when the definition of + does not provide the equality we need
-}
... | gt = n ∷ subst (Vec ℕ) (sucLem₁ lm ln) (merge' m ms ns)
{-
merge' incorporates the same tweaks as merge:
-}
merge' : {m n : ℕ} → ℕ → Vec ℕ m → Vec ℕ n → Vec ℕ (1 + (m + n))
merge' {lm} {zero} m ms [] = m ∷ subst (Vec ℕ) (zeroLem lm) ms
merge' {lm} {suc ln} m ms (n ∷ ns) with order m n
... | le = m ∷ merge ms (n ∷ ns)
... | gt = n ∷ subst (Vec ℕ) (sucLem₁ lm ln) (merge' m ms ns)
{-
We now must adapt our DealT type to take account of size, first of all we'll
need to embed our Parity type in the the Natural Numbers:
-}
data Parity : Set where p0 p1 : Parity
pℕ : Parity → ℕ
pℕ p0 = 0
pℕ p1 = 1
{-
Now we can index our trees by their size, empT and leafT have obvious sizes:
-}
data DealT (X : Set) : ℕ → Set where
empT : DealT X 0
leafT : X → DealT X 1
{-
But what about nodeT? We want the two sub trees to have approximately the same
size. We use the parity bit (and it's embedding in the natural numbers) to
describe the difference in size between those two trees:
-}
nodeT : {n : ℕ} (p : Parity) → DealT X (pℕ p + n) → DealT X n
→ DealT X (((pℕ p + n) + n))
{-
Inserting into a DealT increases its size by 1, note that if we insert into
an unbalanced tree (to obtain a balanced one, we must again use subst to fix
up the types DealT ℕ (1 + (1 + n) + n) and DealT ℕ (0 + (1 + n) + (1 + n))
-}
insert : {X : Set}{n : ℕ} → X → DealT X n → DealT X (1 + n)
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} x (nodeT {n} p1 l r) = subst (\n → DealT X n) (cong suc (sucLem₂ n n)) (nodeT p0 l (insert x r))
{-
The rest of the code however, does through with out a hitch when we adapt the
types to use Vectors:
-}
deal : {n : ℕ} → Vec ℕ n → DealT ℕ n
deal [] = empT
deal (n ∷ ns) = insert n (deal ns)
mergeT : {n : ℕ} → DealT ℕ n → Vec ℕ n
mergeT empT = []
mergeT (leafT n) = [ n ]
mergeT (nodeT p l r) = merge (mergeT l) (mergeT r)
sort : {n : ℕ} → Vec ℕ n → Vec ℕ n
sort ns = mergeT (deal ns)
ex1 : Vec ℕ 6
ex1 = 5 ∷ 2 ∷ 0 ∷ 1 ∷ 4 ∷ 3 ∷ []
ex2 : Vec ℕ 6
ex2 = 100 ∷ 1 ∷ 10 ∷ 1 ∷ 100 ∷ 10 ∷ []