MP3.agda

--
-- Mini project 3 by Morten Fangel Jensen (mfan) & Christian Harrington (cnha)
--

module MiniProject where

open import Prelude
open Nats
open LessThan 

module NatUtils where
  open Sum
  open Decidable
  open Eq

  -- Warm-up 1
  min : (n m : Nat) -> Either (n <= m) (m <= n)
  min zero zero = left zero<=
  min zero (suc m) = left zero<=
  min (suc n) zero = right zero<=
  min (suc n) (suc m) with min n m
  min (suc n) (suc m) | left x = left (suc<= x)
  min (suc n) (suc m) | right x = right (suc<= x)

  -- Warm-up 2.1
  <=refl : ∀ n -> n <= n
  <=refl zero = zero<=
  <=refl (suc n) = suc<= (<=refl n)

  -- Warm-up 2.2
  <=trans : ∀ {a b c} → a <= b → b <= c → a <= c
  <=trans zero<= Hac = zero<=
  <=trans (suc<= Hab') (suc<= Hac') = suc<= (<=trans Hab' Hac')

  <=suc : ∀ {n m} → suc n <= suc m → n <= m
  <=suc (suc<= x) = x

  -- Warm-up 3
  _<=?_ : ∀ n m → Dec (n <= m)
  zero <=? zero = yes zero<=
  zero <=? suc m = yes zero<=
  suc n <=? zero = no (λ ())
  suc n <=? suc m with n <=? m 
  suc n <=? suc m | yes x = yes (suc<= x)
  suc n <=? suc m | no x = no (λ nope → x (<=suc nope))

module OList where
  open NatUtils 

  data OList : Nat -> Set where
    nil  : forall {b} -> OList b
    cons : forall {b} -> (x : Nat) -> (ok : b <= x) -> (xs : OList x) -> OList b

  -- Ordered Lists 1
  weakenOList : forall {b b'} -> b' <= b -> OList b -> OList b'
  weakenOList H nil = nil
  weakenOList H (cons x ok old) = cons x (<=trans H ok) old


module InsertionSort where
  open OList
  open Sum
  open Lists
  open Sigma
  open NatUtils

  -- Ordered Lists 2.1
  insertO : forall {b} -> (x : Nat) -> OList b -> Either (OList x) (OList b)
  insertO x nil = left (cons x (<=refl x) nil)
  insertO x (cons old_head ok old) with min x old_head 
  insertO x (cons old_head ok old) | left x<=old_head = left (cons x (<=refl x) (cons old_head x<=old_head old))
  insertO x (cons old_head ok old) | right old_head<=x with insertO x old 
  insertO x (cons old_head ok old) | right old_head<=x | left new_list = right (cons old_head ok (weakenOList old_head<=x new_list))
  insertO x (cons old_head ok old) | right old_head<=x | right new_list = right (cons old_head ok new_list)

  -- Ordered Lists 2.2
  insertionSort : List Nat -> Nat ** OList
  insertionSort [] = 0 , nil
  insertionSort (x :: xs) with insertionSort xs 
  insertionSort (x :: xs) | bound , sorted_xs with insertO x sorted_xs
  insertionSort (x :: xs) | bound , sorted_xs | left sorted_xs' = x , sorted_xs'
  insertionSort (x :: xs) | bound , sorted_xs | right sorted_xs' = bound , sorted_xs'

module OVec where
  open NatUtils
  open Sum
  open Sigma
  open Vecs
     
  -- Ordered Lists 3

  data OVec : Nat -> Nat -> Set where
    nil  : forall {b} -> OVec b zero
    cons : forall {b n} -> (x : Nat) -> (ok : b <= x) -> (xs : OVec x n) -> OVec b (suc n)

  weakenOVec : forall {b b' n} -> b' <= b -> OVec b n -> OVec b' n
  weakenOVec H nil = nil
  weakenOVec H (cons x ok xs) = cons x (<=trans H ok) xs

  insertO : forall {b n} -> (x : Nat) -> OVec b n -> Either (OVec x (suc n)) (OVec b (suc n))
  insertO x nil = left (cons x (<=refl x) nil)
  insertO x (cons old_head ok old) with min x old_head 
  insertO x (cons old_head ok old) | left x<=old_head = left (cons x (<=refl x) (cons old_head x<=old_head old))
  insertO x (cons old_head ok old) | right old_head<=x with insertO x old 
  insertO x (cons old_head ok old) | right old_head<=x | left new_list = right (cons old_head ok (weakenOVec old_head<=x new_list))
  insertO x (cons old_head ok old) | right old_head<=x | right new_list = right (cons old_head ok new_list)

  insertionSort : ∀ n → Vec Nat n -> Nat ** (λ b → OVec b n)
  insertionSort .0 [] = 0 , nil
  insertionSort .(suc n) (_::_ {n} x xs) with insertionSort n xs 
  insertionSort .(suc n) (_::_ {n} x xs) | bound , sorted_xs with insertO x sorted_xs 
  insertionSort .(suc n) (_::_ {n} x xs) | bound , sorted_xs | left sorted_xs' = x , sorted_xs'
  insertionSort .(suc n) (_::_ {n} x xs) | bound , sorted_xs | right sorted_xs' = bound , sorted_xs'


module TreeSort where
  open OList
  open Decidable
  open NatUtils
  open Eq
  open Sum
  open Lists
  open Sigma

  data Bound : Set where
    bot : Bound
    nat : Nat -> Bound
    top : Bound

  data _<=b_ : Bound -> Bound -> Set where
    bot<= : ∀ {b} -> bot <=b b
    natnat : ∀{n m} -> n <= m -> nat n <=b nat m
    <=top : ∀{b} -> b <=b top

  <=b-inj : ∀ n m → nat n <=b nat m → n <= m
  <=b-inj n m (natnat x) = x

  -- Bounded Binary Trees 1
  _<=b?_ : ∀ n m → Dec (n <=b m)
  bot <=b? m = yes bot<=
  nat x <=b? bot = no (λ ())
  nat x <=b? nat y with x <=? y
  nat x <=b? nat y | yes H = yes (natnat H)
  nat x <=b? nat y | no nope = no (λ H → nope (<=b-inj x y H))
  nat x <=b? top = yes <=top
  top <=b? bot = no (λ ())
  top <=b? nat x = no (λ ())
  top <=b? top = yes <=top

  <=b-trans : ∀ {b₁ b₂ b₃} → b₁ <=b b₂ → b₂ <=b b₃ → b₁ <=b b₃
  <=b-trans bot<= bot<= = bot<=
  <=b-trans bot<= (natnat x) = bot<=
  <=b-trans bot<= <=top = bot<=
  <=b-trans (natnat H₁) (natnat H₂) = natnat (<=trans H₁ H₂)
  <=b-trans (natnat _) <=top = <=top
  <=b-trans <=top <=top = <=top

  <=b-refl : ∀ b → b <=b b
  <=b-refl bot = bot<=
  <=b-refl (nat x) = natnat (<=refl x)
  <=b-refl top = <=top

  data NatTree : Bound -> Bound -> Set where
    E : ∀{b1 b2} -> b1 <=b b2 -> NatTree b1 b2
    T : ∀{b1 b2} -> (n : Nat) -> NatTree b1 (nat n) -> NatTree (nat n) b2 -> NatTree b1 b2

  data Member : forall b1 b2 -> Nat -> NatTree b1 b2 -> Set where
    isLeft  : ∀ b₁ b₂ x val t₁ t₂ → x <= val → Member b₁ (nat val) x t₁ → Member b₁ b₂ x (T val t₁ t₂)  
    isHere  : ∀ b₁ b₂ x t₁ t₂ → Member b₁ b₂ x (T x t₁ t₂)
    isRight : ∀ b₁ b₂ x val t₁ t₂ → val <= x → Member (nat val) b₂ x t₂ → Member b₁ b₂ x (T val t₁ t₂)

  -- Bounded Binary Trees 2
  insert : forall {b1 b2} -> (n : Nat) -> (b1 <=b nat n) -> (nat n <=b b2) -> NatTree b1 b2 -> NatTree b1 b2
  insert n H₁ H₂ (E _) = T n (E H₁) (E H₂)
  insert n H₁ H₂ (T val tree₁ tree₂) with min n val 
  insert n H₁ H₂ (T val tree₁ tree₂) | left n<=val with insert n H₁ (natnat n<=val) tree₁
  ... | res = T val res tree₂
  insert n H₁ H₂ (T val tree₁ tree₂) | right val<=n with insert n (natnat val<=n) H₂ tree₂
  ... | res = T val tree₁ res

  -- Bounded Binary Trees 3
  memberAfterInsert : forall {n b1 b2} ->
                      (ok1 : b1 <=b nat n) (ok2 : nat n <=b b2)
                      (t : NatTree b1 b2) ->
                      Member b1 b2 n (insert n ok1 ok2 t)
  memberAfterInsert {n} {b1} {b2} ok1 ok2 (E x) = isHere b1 b2 n (E ok1) (E ok2)
  memberAfterInsert {n} {b1} {b2} ok1 ok2 (T val t₁ t₂) with min n val
  memberAfterInsert {n} {b1} {b2} ok1 ok2 (T val t₁ t₂) | left n<=val with memberAfterInsert ok1 (natnat n<=val) t₁
  ... | member = isLeft b1 b2 n val (insert n ok1 (natnat n<=val) t₁) t₂ n<=val member 
  memberAfterInsert {n} {b1} {b2} ok1 ok2 (T val t₁ t₂) | right val<=n with memberAfterInsert (natnat val<=n) ok2 t₂
  ... | member  = isRight b1 b2 n val t₁ (insert n (natnat val<=n) ok2 t₂) val<=n member

  grow' : (l : List Nat) → (t : NatTree (nat 0) top) → NatTree (nat 0) top
  grow' [] t = t
  grow' (x :: xs) t with grow' xs t
  ... | res = insert x (natnat zero<=) <=top res

  grow : (l : List Nat) → NatTree (nat 0) top
  grow l = grow' l (E {nat 0} {top} <=top) 

  weakenTree : ∀ {b₁ b₁' b₂} → NatTree b₁ b₂ → b₁' <=b b₁ → NatTree b₁' b₂
  weakenTree (E x) H = E (<=b-trans H x)
  weakenTree (T n t₁ t₂) H = T n (weakenTree t₁ H) t₂

  -- Bounded Binary Trees 4
  mkTree : (l : List Nat) → NatTree bot top
  mkTree l = weakenTree (grow l) bot<=

  flatten : ∀ {b₁ b₂} → (t : NatTree b₁ b₂) → List Nat
  flatten (E x) = []
  flatten (T n t₁ t₂) = flatten t₁ ++ (n :: flatten t₂)

  sortViaTree : (l : List Nat) → List Nat
  sortViaTree l = flatten (grow l)

  -- Bounded Binary Trees 5 (BList def)
  data BList : Bound -> Bound -> Set where
    blnil : ∀ {b₁ b₂} → (ok : b₁ <=b b₂) → BList b₁ b₂
    blcons : ∀ {b₁ b₂} → (x : Nat) → (ok1 : b₁ <=b nat x) → (ok2 : nat x <=b b₂) → (xs : BList (nat x) b₂) → BList b₁ b₂

  bl-inj : ∀ b₁ b₂ → (l : BList b₁ b₂) → b₁ <=b b₂
  bl-inj b₁ b₂ (blnil ok) = ok
  bl-inj b₁ b₂ (blcons x ok1 ok2 l) = <=b-trans ok1 ok2

  weakenBList : ∀ {b₁ b₁' b₂} → b₁' <=b b₁ → BList b₁ b₂ → BList b₁' b₂
  weakenBList H (blnil ok) = blnil (<=b-trans H ok)
  weakenBList H (blcons x ok1 ok2 xs) = blcons x (<=b-trans H ok1) ok2 xs

  weakenUpList : ∀ {b₁ b₂ b₂'} → b₂ <=b b₂' → BList b₁ b₂ → BList b₁ b₂'
  weakenUpList H (blnil ok) = blnil (<=b-trans ok H)
  weakenUpList H (blcons x ok1 ok2 xs) = blcons x ok1 (<=b-trans ok2 H) (weakenUpList H xs) 

  -- Bounded Binary Trees 5 (BList-append)
  bl++ : ∀ {b₁ b₂ b₃} → BList b₁ b₂ → BList b₂ b₃ → BList b₁ b₃
  bl++ (blnil ok) b = weakenBList ok b
  bl++ (blcons x ok1 ok2 xs) (blnil ok) = blcons x ok1 (<=b-trans ok2 ok) (weakenUpList ok xs)
  bl++ (blcons x ok1 ok2 xs) (blcons y ok1' ok2' ys) = blcons x ok1 (<=b-trans ok2 (<=b-trans ok1' ok2')) (bl++ xs (blcons y ok1' ok2' ys)) 

  flatten' : ∀ {b₁ b₂} → (t : NatTree b₁ b₂) → BList b₁ b₂
  flatten' (E H) = blnil H
  flatten' (T x t₁ t₂) with flatten' t₁ 
  ... | t₁' with flatten' t₂ 
  flatten' (T x t₁ (E x₁)) | t₁' | t₂' = bl++ t₁' (blcons x (<=b-refl (nat x)) x₁ t₂')
  flatten' {b₁} {b₂} (T x t₁ (T n t₂ t₃)) | t₁' | t₂' = bl++ t₁' (blcons x (<=b-refl (nat x)) (bl-inj (nat x) b₂ t₂') t₂')

  BListToOList : ∀ {n b} → (bl : BList (nat n) b) → OList n
  BListToOList (blnil ok) = nil
  BListToOList {n} {b} (blcons x ok1 ok2 bl) = cons x (<=b-inj n x ok1) (BListToOList bl)

  -- Bounded Binary Trees 5 (sorting)
  SortViaTreesAndListsAndEverything : (l : List Nat) → OList zero
  SortViaTreesAndListsAndEverything l  = BListToOList (flatten' (grow l))


module MergeSort where
  open Vecs
  open OList
  open OVec
  open Sigma
  open Sum
  open NatUtils
  open Eq

  n+0 : ∀ n → n + 0 == n
  n+0 zero = refl
  n+0 (suc n) = cong suc (n+0 n)

  +-suc : ∀ a b → a + suc b == suc a + b
  +-suc zero b = refl
  +-suc (suc a) b = cong suc (+-suc a b)

  -- Merge Sort 1
  merge' : forall {b n m} -> OVec b n -> OVec b m -> OVec b (n + m)
  merge' nil nil = nil
  merge' nil l = l
  merge' {b} {n} {.0} l nil rewrite n+0 n = l
  merge' {b} {suc n} {suc m} (cons x okx xs) (cons y oky ys) with min x y
  merge' {b} {suc n} {suc m} (cons x okx xs) (cons y oky ys) | left x<=y = cons x okx (merge' xs (cons y x<=y ys))
  merge' {b} {suc n} {suc m} (cons x okx xs) (cons y oky ys) | right y<=x with OVec.cons x okx xs
  ... | res rewrite +-suc n m = cons y oky (merge' (cons x y<=x xs) ys)

  merge : ∀ {b₁ b₂ n m} → OVec b₁ n → OVec b₂ m → Nat ** (λ b₃ → OVec b₃ (n + m))
  merge {b₁} {b₂} l₁ l₂ with min b₁ b₂ 
  merge {b₁} {b₂} l₁ l₂ | left b₁<=b₂ = b₁ , merge' l₁ (weakenOVec b₁<=b₂ l₂)
  merge {b₁} {b₂} l₁ l₂ | right b₂<=b₁ = b₂ , merge' (weakenOVec b₂<=b₁ l₁) l₂


  data Fan : Nat -> Set where
    empty : Fan 0
    single : Nat -> Fan 1
    even : ∀{n} -> Fan n -> Fan n -> Fan (n + n)
    odd : ∀{n} -> Fan (suc n) -> Fan n -> Fan (suc (n + n))

  open Product 

  -- Merge Sort 2

  -- First a silly attempt that uses odd/even to cut a vector into
  -- size, to build the fan.

  take : forall {A m} n -> Vec A (n + m) -> Vec A n
  take zero xs = []
  take (suc n) (x :: xs) = x :: take n xs

  drop : forall {A m} n -> Vec A (n + m) -> Vec A m
  drop zero xs = xs
  drop (suc n) (x :: xs) = drop n xs

  splitEven : ∀ {n} → Vec Nat (n + n) → (Vec Nat n * Vec Nat n)
  splitEven {n} l = take n l , drop n l

  splitOdd : ∀ {n} → Vec Nat (suc (n + n)) → (Vec Nat (suc n) * Vec Nat n)
  splitOdd {n} l = take (suc n) l , drop (suc n) l

  data Even : Nat → Set where
    even : ∀ {n m} → n == m + m → Even n
    odd : ∀ {n m} → n == suc m + m → Even n

  helper₁ : ∀ {n m} → n == m + m → suc (suc n) == suc (m + suc m)
  helper₁ {n} {m} H rewrite +-suc m m = cong suc (cong suc H)

  helper₂ : ∀ {n m} → n == suc (m +  m) → n == m + suc m
  helper₂ {n} {m} H rewrite +-suc m m = H 

  isEven : (n : Nat) → Even n
  isEven zero = even {zero} {zero} refl
  isEven (suc zero) = odd {suc zero} {zero} refl
  isEven (suc (suc n)) with isEven n
  isEven (suc (suc n)) | even {.n} {m} H = even {suc (suc n)} {suc m} (helper₁ {n} {m} H)
  isEven (suc (suc n)) | odd {.n} {m} H = odd {suc (suc n)} {suc m} (cong (λ n → suc (suc n)) (helper₂ {n} {m} H))

  blower : ∀ {n} → Vec Nat n → Fan n
  blower [] = empty
  blower (x :: []) = single x
  blower {n} xs with isEven n
  blower {n} xs | even {.n} {m} H rewrite H with splitEven {m} xs
  blower xs | even H | fst , snd = even (blower fst) (blower snd)
  blower {n} xs | odd {.n} {m} H rewrite H with splitOdd {m} xs 
  blower xs | odd H | fst , snd = odd (blower fst) (blower snd) 

  mergeSort' : ∀ {n} → Fan n → Nat ** (λ b → OVec b n)
  mergeSort' empty = zero , nil
  mergeSort' (single x) = x , cons x (<=refl x) nil
  mergeSort' (even f₁ f₂) with mergeSort' f₁ | mergeSort' f₂
  mergeSort' (even f₁ f₂) | _ , l₁ | _ , l₂ = merge l₁ l₂ 
  mergeSort' (odd f₁ f₂) with mergeSort' f₁ | mergeSort' f₂ 
  mergeSort' (odd f₁ f₂) | _ , l₁ | _ , l₂ = merge l₁ l₂

  mergeSort : forall {n} -> Vec Nat n -> Nat ** (\ b -> OVec b n)
  mergeSort {n} l = mergeSort' {n} (blower l)

  -- And now a better approach that doesn't have to use cut on the
  -- vectors. This part has been done in collaboration with Thomas & Sune.

  +-suc-r : ∀ n m → n + suc m == suc (n + m)
  +-suc-r zero m = refl
  +-suc-r (suc n) m = cong suc (+-suc-r n m)

  addtofan : ∀ {n} → Nat → Fan n → Fan (suc n)
  addtofan x empty = single x
  addtofan x (single y) = even (single x) (single y)
  addtofan x (even f₁ f₂) = odd (addtofan x f₁) f₂
  addtofan x (odd {n} f₁ f₂) rewrite sym (+-suc-r n n) = even f₁ (addtofan x f₂)

  vec2fan : ∀ {n} → Vec Nat n → Fan n
  vec2fan [] = empty
  vec2fan (x :: xs) with vec2fan xs
  vec2fan (x :: xs) | empty = single x
  vec2fan (x :: xs) | single y = even (single x) (single y)
  vec2fan (x :: xs) | even f₁ f₂ = odd (addtofan x f₁) f₂ 
  vec2fan (x :: xs) | odd {n} f₁ f₂ rewrite sym (+-suc-r n n) = even f₁ (addtofan x f₂)
 
  mergeSort2 : ∀ {n} → Vec Nat n → Nat ** (λ b → OVec b n)
  mergeSort2 {n} l = mergeSort' {n} (vec2fan l)