Mergesort in Idris

SortedList.idr

module SortedList

-- Based on http://mazzo.li/posts/AgdaSort.html

import Decidable.Decidable
import Decidable.Order
import Uninhabited

%default total

class Poset t po => TotalOrder t (po : t -> t -> Type) where
  total totalOrder : (x : t) -> (y : t) -> Either (po x y) (po y x)

zero_lte : (m : Nat) -> NatLTE Z m
zero_lte Z = nEqn
zero_lte (S m) = nLTESm (zero_lte m)

lte_lift : (n : Nat) -> (m : Nat) -> NatLTE n m -> NatLTE (S n) (S m)
lte_lift n n nEqn = nEqn
lte_lift n (S m) (nLTESm r) = nLTESm (lte_lift n m r)

instance TotalOrder Nat NatLTE where
  totalOrder Z m = Left (zero_lte m)
  totalOrder n Z = Right (zero_lte n)
  totalOrder (S n) (S m) with (totalOrder n m)
    | Left nm  = Left  (lte_lift n m nm)
    | Right mn = Right (lte_lift m n mn)

class (Poset t po, Decidable [t,t] po) => DecidablePoset t (po : t -> t -> Type)

data BoundedPoset : Type -> Type where
  Bottom : BoundedPoset t
  Top    : BoundedPoset t
  X      : t -> BoundedPoset t

data BPO : (po : t -> t -> Type) -> BoundedPoset t -> BoundedPoset t -> Type where
  BottomLe : {r : BoundedPoset t} -> BPO po Bottom r
  TopGe    : {l : BoundedPoset t} -> BPO po l Top
  XLe      : {l : t} -> {r : t} -> (le : po l r) -> BPO po (X l) (X r)

using (t : Type, po : t -> t -> Type)
  instance Uninhabited (BPO po Top Bottom) where
    uninhabited BottomLe impossible
    uninhabited TopGe impossible
    uninhabited (XLe _) impossible

  xNotLeBottom : {a : t} -> BPO po (X a) Bottom -> _|_
  xNotLeBottom BottomLe impossible
  xNotLeBottom TopGe impossible
  xNotLeBottom (XLe _) impossible

  topNotLeX : {b : t} -> BPO po Top (X b) -> _|_
  topNotLeX BottomLe impossible
  topNotLeX TopGe impossible
  topNotLeX (XLe _) impossible

  orderPres : {a : t} -> {b : t} -> BPO po (X a) (X b) -> po a b
  orderPres (XLe ab) = ab

  instance Preorder t po => Preorder (BoundedPoset t) (BPO po) where
    reflexive Bottom = BottomLe
    reflexive Top    = TopGe
    reflexive (X x)  = XLe (reflexive x)

    transitive Bottom b c _ _ = BottomLe
    transitive a b Top    _ _ = TopGe
    transitive (X a) (X b) (X c) (XLe ab) (XLe bc) = XLe (transitive a b c ab bc)

  instance Poset t po => Poset (BoundedPoset t) (BPO po) where
    antisymmetric Bottom Bottom BottomLe BottomLe = refl
    antisymmetric Top Top TopGe TopGe = refl
    antisymmetric (X a) (X b) (XLe ab) (XLe ba) = cong (antisymmetric a b ab ba)

  instance TotalOrder t po => TotalOrder (BoundedPoset t) (BPO po) where
    totalOrder Bottom _ = Left BottomLe
    totalOrder _ Bottom = Right BottomLe
    totalOrder Top _ = Right TopGe
    totalOrder _ Top = Left TopGe
    totalOrder (X x) (X y) = either (Left . XLe) (Right . XLe) (totalOrder x y)

  instance Decidable [t,t] po => Decidable [BoundedPoset t,BoundedPoset t] (BPO po) where
    decide Bottom b = Yes BottomLe
    decide a Top    = Yes TopGe
    decide (X a) (X b) with (decide {ts=[t,t]} {p=po} a b)
      | Yes ab = Yes (XLe ab)
      | No ab  = No (ab . orderPres)
    decide (X a) Bottom = No xNotLeBottom
    decide Top (X b) = No topNotLeX
    decide Top Bottom = No uninhabited

data OList : {t : Type} -> {po : t -> t -> Type} -> BoundedPoset t -> BoundedPoset t -> Type where
  nil  : {l : BoundedPoset t} -> {u : BoundedPoset t} -> BPO po l u -> OList {t} {po} l u
  cons : (x : t) -> OList {t} {po} (X x) u -> BPO po l (X x) -> OList {t} {po} l u

relaxLowerBound : Preorder t po => (l1 : BoundedPoset t) -> (l2 : BoundedPoset t) -> (u : BoundedPoset t) ->
                  BPO po l1 l2 -> OList {po=po} l2 u -> OList {po=po} l1 u
relaxLowerBound l1 l2 u l1l2 (nil l2u) = nil (transitive l1 l2 u l1l2 l2u)
relaxLowerBound l1 l2 u l1l2 (cons x xs l2x) = cons x xs (transitive l1 l2 (X x) l1l2 l2x)

relaxUpperBound : Preorder t po => (l : BoundedPoset t) -> (u1 : BoundedPoset t) -> (u2 : BoundedPoset t) ->
                  BPO po u1 u2 -> OList {po=po} l u1 -> OList {po=po} l u2
relaxUpperBound l u1 u2 u1u2 (nil lu1) = nil (transitive l u1 u2 lu1 u1u2)
relaxUpperBound l u1 u2 u1u2 (cons x xs lx) = cons x (relaxUpperBound (X x) u1 u2 u1u2 xs) lx

toList : OList {t} {po} l u -> List t
toList (nil _) = []
toList (cons x xs _) = x :: toList xs

insert : TotalOrder t po => {l : BoundedPoset t} -> {u : BoundedPoset t} ->
         (x : t) -> OList {po=po} l u -> BPO po l (X x) -> BPO po (X x) u -> OList {po=po} l u
insert x (nil _) lx xu = cons x (nil xu) lx
insert x (cons y ys ly) lx xu with (totalOrder x y)
  | Left xy  = cons x (cons y ys (XLe xy)) lx
  | Right yx = cons y (insert x ys (XLe yx) xu) ly

insertionSort : (TotalOrder t po, Foldable f) => f t -> OList {po=po} Bottom Top
insertionSort = foldr (\x => \l => insert x l BottomLe TopGe) (nil BottomLe)

data Inspect : (x : a) -> Type where
  it : {x : a} -> (y : a) -> (x = y) -> Inspect x

inspect : (x : a) -> Inspect x
inspect x = it x refl

min'' : TotalOrder t po => (a : t) -> (b : t) -> (m : t ** (po m a, po m b))
min'' a b with (totalOrder a b)
  | Left ab  = (a ** (reflexive a, ab))
  | Right ba = (b ** (ba, reflexive b))

min' : TotalOrder t po => t -> t -> t
min' a b = getWitness (min'' a b)

min'_le1 : TotalOrder t po => (a : t) -> (b : t) -> po (min' {t=t} {po=po} a b) a
min'_le1 a b = fst (getProof (min'' a b))

min'_le2 : TotalOrder t po => (a : t) -> (b : t) -> po (min' {t=t} {po=po} a b) b
min'_le2 a b = snd (getProof (min'' a b))

-- Universal property of min'
min'_up : TotalOrder t po => (c : t) -> (a : t) -> (b : t) -> po c a -> po c b -> po c (min' a b)
min'_up c a b ca cb with (inspect (totalOrder a b))
  | it (Left ab)  p = ?min'_up1
  | it (Right ba) p = ?min'_up2

min'_monotonic : TotalOrder t po => {a1 : t} -> {a2 : t} -> {b1 : t} -> {b2 : t} ->
                 po a1 a2 -> po b1 b2 -> po (min' a1 b1) (min' a2 b2)
min'_monotonic {a1} {a2} {b1} {b2} a1a2 b1b2 =
  min'_up (min' a1 b1) a2 b2
          (transitive (min' a1 b1) a1 a2 (min'_le1 a1 b1) a1a2)
          (transitive (min' a1 b1) b1 b2 (min'_le2 a1 b1) b1b2)

max'' : TotalOrder t po => (a : t) -> (b : t) -> (M : t ** (po a M, po b M))
max'' a b with (totalOrder a b)
  | Left ab  = (b ** (ab, reflexive b))
  | Right ba = (a ** (reflexive a, ba))

max' : TotalOrder t po => t -> t -> t
max' a b = getWitness (max'' a b)

max'_ge1 : TotalOrder t po => (a : t) -> (b : t) -> po a (max' {t=t} {po=po} a b)
max'_ge1 a b = fst (getProof (max'' a b))

max'_ge2 : TotalOrder t po => (a : t) -> (b : t) -> po b (max' {t=t} {po=po} a b)
max'_ge2 a b = snd (getProof (max'' a b))

max'_up : TotalOrder t po => (c : t) -> (a : t) -> (b : t) -> po a c -> po b c -> po (max' a b) c
max'_up c a b ac bc with (inspect (totalOrder a b))
  | it (Left ab)  p = ?max'_up1
  | it (Right ba) p = ?max'_up2

max'_monotonic : TotalOrder t po => {a1 : t} -> {a2 : t} -> {b1 : t} -> {b2 : t} ->
                 po a1 a2 -> po b1 b2 -> po (max' a1 b1) (max' a2 b2)
max'_monotonic {a1} {a2} {b1} {b2} a1a2 b1b2 =
  max'_up (max' a2 b2) a1 b1
          (transitive a1 a2 (max' a2 b2) a1a2 (max'_ge1 a2 b2))
          (transitive b1 b2 (max' a2 b2) b1b2 (max'_ge2 a2 b2))

min'_le_max' : TotalOrder t po => (a : t) -> (b : t) -> po (min' a b) (max' a b)
min'_le_max' a b = transitive (min' a b) a (max' a b) (min'_le1 a b) (max'_ge1 a b)

%assert_total
merge : TotalOrder t po => OList {po=po} l1 u1 -> OList {po=po} l2 u2 -> OList {po=po} (min' l1 l2) (max' u1 u2)
merge {po=po} {l1=l1} {u1=u1} {l2=l2} {u2=u2} (nil l1u1) xs =
  relaxUpperBound (min' {po=(BPO po)} l1 l2) u2 (max' {po=(BPO po)} u1 u2) (max'_ge2 {po=(BPO po)} u1 u2) $
  relaxLowerBound (min' {po=(BPO po)} l1 l2) l2 u2 (min'_le2 {po=(BPO po)} l1 l2) xs
merge {po=po} {l1=l1} {u1=u1} {l2=l2} {u2=u2} xs (nil l2u2) =
  relaxUpperBound (min' {po=(BPO po)} l1 l2) u1 (max' {po=(BPO po)} u1 u2) (max'_ge1 {po=(BPO po)} u1 u2) $
  relaxLowerBound (min' {po=(BPO po)} l1 l2) l1 u1 (min'_le1 {po=(BPO po)} l1 l2) xs
merge {po=po} {l1=l1} {u1=u1} {l2=l2} {u2=u2} (cons x xs l1x) (cons y ys l2y) with (totalOrder x y)
  | Left xy  = cons x (relaxLowerBound (X x) (min' (X x) (X y)) (max' u1 u2) x_le_minxy recur) lower_bound
    where lower_bound = transitive (min' l1 l2) l1 (X x) (min'_le1 l1 l2) l1x
          recur = merge xs (cons y ys (reflexive (X y)))
          x_le_minxy = min'_up (X x) (X x) (X y) (reflexive (X x)) (XLe xy)
  | Right yx = cons y (relaxLowerBound (X y) (min' (X x) (X y)) (max' u1 u2) y_le_minxy recur) lower_bound
    where lower_bound = transitive (min' l1 l2) l2 (X y) (min'_le2 l1 l2) l2y
          recur = merge (cons x xs (reflexive (X x))) ys
          y_le_minxy = min'_up (X y) (X x) (X y) (XLe yx) (reflexive (X y))

split : Foldable f => f a -> (List a, List a)
split = foldr (\e => \p => (snd p, e :: fst p)) ([], [])

%assert_total
mergeSort : TotalOrder t po => List t -> OList {po=po} Bottom Top
mergeSort z with (split z)
  | ([],[])  = nil BottomLe
  | ([],[a]) = cons a (nil TopGe) BottomLe
  | (ls,rs)  = merge (mergeSort ls) (mergeSort rs)

---------- Proofs ----------

SortedList.min'_up2 = proof
  intros
  rewrite sym p
  compute
  trivial

SortedList.min'_up1 = proof
  intros
  rewrite sym p
  compute
  trivial

SortedList.max'_up1 = proof
  intros
  rewrite sym p
  compute
  trivial

SortedList.max'_up2 = proof
  intros
  rewrite sym p
  compute
  trivial