Msort.agda

{-# OPTIONS --universe-polymorphism #-}

module Msort where

open import Level
open import Data.Nat
open import Data.Sum 
open import Data.Unit
open import Data.Empty
open import Data.List renaming (_∷_ to _::_)
open import Relation.Binary renaming (DecTotalOrder to DTO ; IsTotalOrder to ITO ; IsDecTotalOrder to IDTO)
open import Relation.Binary.Core
open import Relation.Nullary.Core
open import Induction.WellFounded as WF
open import Induction.Nat

_<l_ : ∀ {a}{A : Set a} -> Rel (List (List A)) zero
xs <l ys = length xs <′ length ys

-- _<l_ is Well-founded (See Induction.WellFounded)
<l-well-founded : {A : Set} -> Well-founded (_<l_ {A = A})
<l-well-founded xs = f xs (<-well-founded(length xs))
    where
      f : ∀ xs -> Acc _<′_ (length xs) -> Acc _<l_ xs
      f xs (acc rs) = acc (\ys h -> f ys (rs (length ys) h))

-- if_then_else_ for Dec
IF_then_else_ : ∀ {l a}{P : Set l}{A : Set a} -> Dec P -> A -> A -> A
IF yes p then t else _ = t
IF no np then _ else f = f

≡-rect : ∀ {a l}{A : Set a}{x : A}{P : A -> Set l} -> P x -> ∀ {y : A} -> x ≡ y -> P y
≡-rect Px refl = Px

orprop : ∀{a}{A B : Set a} -> A ⊎ B -> (A -> ⊥) -> B
orprop (inj₁ A) nA = ⊥-elim (nA A)
orprop (inj₂ B) nA = B

merge : (D : DTO zero zero zero) ->  List (DTO.Carrier D) -> List (DTO.Carrier D) -> List (DTO.Carrier D)
merge _ [] ys = ys
merge _ xs [] = xs
merge D (x :: xs) (y :: ys) = IF (DTO._≤?_ D x y) then (x :: merge D xs (y :: ys)) else (y :: merge D (x :: xs) ys)

msort' : (D : DTO zero zero zero) -> List (List (DTO.Carrier D)) -> List (List (DTO.Carrier D))
msort' _ [] = []
msort' _ (xs :: []) = xs :: []
msort' D (xs :: ys :: zss) = merge D xs ys :: msort' D zss

msort'_ind : (D : DTO zero zero zero) -> (P : List (List (DTO.Carrier D)) -> List (List (DTO.Carrier D)) -> Set) -> P [] [] -> (∀ {x : List (DTO.Carrier D)} -> P (x :: []) (x :: [])) -> 
    (∀ (x y : List (DTO.Carrier D))(zs : List (List (DTO.Carrier D))) -> P zs zs -> P (x :: y :: zs) (x :: y :: zs)) -> ∀ (l : List (List (DTO.Carrier D))) -> P l l
msort'_ind D P Pnn Poo Pi [] = Pnn
msort'_ind D P Pnn Poo Pi (x :: []) = Poo
msort'_ind D P Pnn Poo Pi (x :: y :: zs) = Pi x y zs (msort'_ind D P Pnn Poo Pi zs)

≤′-step2 : {n m : ℕ} -> n ≤′ m -> suc n ≤′ suc m
≤′-step2 ≤′-refl = ≤′-refl
≤′-step2 (≤′-step p) = ≤′-step (≤′-step2 p)

helper : (D : DTO zero zero zero)(x y z w : List (DTO.Carrier D))(zs : List (List (DTO.Carrier D))) -> msort' D (z :: w :: zs) <l ( z :: w :: zs) ->
    (merge D x y :: (msort' D (z :: w :: zs))) <l ( x :: y :: z :: w :: zs )
helper D x y z w zs Pzs = ≤′-step2 (≤′-step Pzs)

msort'len : (D : DTO zero zero zero) -> (x x' : List (DTO.Carrier D)) -> (xs : List (List (DTO.Carrier D))) -> msort' D (x :: x' :: xs) <l (x :: x' :: xs)
msort'len D x y zs = msort'_ind D (\l l' -> msort' D ( x :: y :: l' ) <l ( x :: y :: l )) ≤′-refl ≤′-refl (helper D x y) zs

checker : (D : DTO zero zero zero) -> List (List (DTO.Carrier D)) -> List (List (DTO.Carrier D))
checker D = wfRec (\_ -> List (List (DTO.Carrier D))) checker'
    where
      checker' : (xs : List (List (DTO.Carrier D))) -> ((ys : List (List (DTO.Carrier D))) -> ys <l xs -> List (List (DTO.Carrier D))) -> List (List (DTO.Carrier D))
      checker' [] _ = []
      checker' (x :: []) _ = x :: []
      checker' (x :: x' :: xs) f = f (msort' D (x :: x' :: xs)) (msort'len D x x' xs)
      open WF.All <l-well-founded public

msort : (D : DTO zero zero zero) -> List (DTO.Carrier D) -> List (DTO.Carrier D)
msort D xs = concat (checker D (Data.List.map [_] xs))

data Sorted (D : DTO zero zero zero) : List (DTO.Carrier D) -> Set where
    nil-sorted : Sorted D []
    one-sorted : (x : DTO.Carrier D) -> Sorted D [ x ]
    cons-sorted : (x y : DTO.Carrier D)(zs : List (DTO.Carrier D)) -> DTO._≤_ D x y -> Sorted D (y :: zs) -> Sorted D (x :: y :: zs)

Sorted_ind : (D : DTO zero zero zero) -> (P : List (DTO.Carrier D) -> Set) -> P [] -> ({x : DTO.Carrier D} -> P (x :: []))
    -> ({x y : DTO.Carrier D}{zs : List (DTO.Carrier D)} -> Sorted D (y :: zs) -> P (y :: zs) -> DTO._≤_ D x y -> P (x :: y :: zs)) -> (l : List (DTO.Carrier D)) -> Sorted D l -> P l
Sorted_ind _ _ Pn _ _ [] _ = Pn
Sorted_ind _ _ _ Po _ (x :: []) _ = Po
Sorted_ind D P Pn Po Pi (x :: y :: zs) (cons-sorted .x .y .zs x≤y Szs) = Pi Szs (Sorted_ind D P Pn Po Pi (y :: zs) Szs) x≤y

rest-sorted : {D : DTO zero zero zero} -> {x : DTO.Carrier D} -> (xs : List (DTO.Carrier D)) -> Sorted D (x :: xs) -> Sorted D xs
rest-sorted [] _ = nil-sorted
rest-sorted {x = x}(x' :: xs) (cons-sorted .x .x' .xs _ Sx'xs) = Sx'xs

DTO≰to≤ : (D : DTO zero zero zero) -> (x y : DTO.Carrier D) -> (DTO._≤_ D x y -> ⊥) -> DTO._≤_ D y x
DTO≰to≤ D x y x≰y = orprop (ITO.total (IDTO.isTotalOrder (DTO.isDecTotalOrder D)) x y) x≰y

IFprop1 : ∀{l l' a}{P : Set l}{A : Set a}(p : P)(X : A -> Set l'){t f : A} -> X (IF (yes p) then t else f) -> X t
IFprop1 p X Xa = Xa

IFprop2 : ∀{l l' a}{P : Set l}{A : Set a}(np : ¬ P)(X : A -> Set l'){t f : A} -> X (IF (no np) then t else f) -> X f
IFprop2 np X Xa = Xa

sortedMerge : (D : DTO zero zero zero) -> (xs ys : List (DTO.Carrier D)) -> Sorted D xs -> Sorted D ys -> Sorted D (merge D xs ys)
sortedMerge _ [] _ _ Sys = Sys
sortedMerge _ (x :: _) [] Sxs _ = Sxs
sortedMerge D (x :: []) (y :: []) _ _ with DTO._≤?_ D x y
...       | yes x≤y = cons-sorted x y [] x≤y (one-sorted y)
...       | no x≰y   = cons-sorted y x [] (DTO≰to≤ D x y x≰y) (one-sorted x)
sortedMerge D (x :: []) (y :: y' :: ys) _ (cons-sorted .y .y' .ys y≤y' Sy'ys) with DTO._≤?_ D x y | DTO._≤?_ D x y'
...       | yes x≤y | _ = cons-sorted x y (y' :: ys) x≤y (cons-sorted y y' ys y≤y' Sy'ys)
...       | no x≰y   | yes x≤y' = cons-sorted y x (y' :: ys) (DTO≰to≤ D x y x≰y) (cons-sorted x y' ys x≤y' Sy'ys)
...       | no x≰y   | no x≰y'   = cons-sorted y y' (merge D (x :: []) ys) y≤y' (IFprop2 x≰y' (Sorted D) {f = y' :: merge D (x :: []) ys} (sortedMerge D (x :: []) (y' :: ys) (one-sorted x) Sy'ys))
sortedMerge D (x :: x' :: xs) (y :: []) (cons-sorted .x .x' .xs x≤x' Sx'xs) _ with DTO._≤?_ D x y | DTO._≤?_ D x' y
...       | no x≰y   | _ = cons-sorted y x (x' :: xs) (DTO≰to≤ D x y x≰y) (cons-sorted x x' xs x≤x' Sx'xs)
...       | yes x≤y | yes x'≤y = cons-sorted x x' (merge D xs (y :: [])) x≤x' (IFprop2 x'≤y (Sorted D) (sortedMerge D (x' :: xs) (y :: []) Sx'xs (one-sorted y)))
...       | yes x≤y | no x'≰y   = cons-sorted x y (x' :: xs) x≤y (cons-sorted y x' xs (DTO≰to≤ D x' y x'≰y) Sx'xs)
sortedMerge D (x :: x' :: xs) (y :: y' :: ys) (cons-sorted .x .x' .xs x≤x' Sx'xs) (cons-sorted .y .y' .ys y≤y' Sy'ys) with DTO._≤?_ D x y | DTO._≤?_ D x' y | DTO._≤?_ D x y'
...       | yes x≤y | yes x'≤y | _ = cons-sorted x x' (merge D xs (y :: y' :: ys)) x≤x' (IFprop1 x'≤y (Sorted D) (sortedMerge D (x' :: xs) (y :: y' :: ys) Sx'xs (cons-sorted y y' ys y≤y' Sy'ys)))
...       | yes x≤y | no x'≰y   | _ = cons-sorted x y (merge D (x' :: xs) (y' :: ys)) x≤y (IFprop2 x'≰y (Sorted D) (sortedMerge D (x' :: xs) (y :: y' :: ys) Sx'xs (cons-sorted y y' ys y≤y' Sy'ys)))
...       | no x≰y   | _ | yes x≤y' = cons-sorted y x (merge D (x' :: xs) (y' :: ys)) (DTO≰to≤ D x y x≰y) (IFprop1 x≤y' (Sorted D) (sortedMerge D (x :: x' :: xs) (y' :: ys) (cons-sorted x x' xs x≤x' Sx'xs) Sy'ys))
...       | no x≰y   | _ | no x≰y'   = cons-sorted y y' (merge D (x :: x' :: xs) ys) y≤y' (IFprop2 x≰y' (Sorted D) (sortedMerge D (x :: x' :: xs) (y' :: ys) (cons-sorted x x' xs x≤x' Sx'xs) Sy'ys))

data Permutation (D : DTO zero zero zero) : List (DTO.Carrier D) -> List (DTO.Carrier D) -> Set where
    nil-perm : Permutation D [] []
    skip-perm : (x : DTO.Carrier D)(ys zs : List (DTO.Carrier D)) -> Permutation D ys zs -> Permutation D (x :: ys)(x :: zs)
    swap-perm : (x y : DTO.Carrier D)(zs : List (DTO.Carrier D)) -> Permutation D (x :: y :: zs) (y :: x :: zs)
    trans-perm : (xs ys zs : List (DTO.Carrier D)) -> Permutation D xs ys -> Permutation D ys zs -> Permutation D xs zs