A surpassing problem

surpassing.hs

module Surpassing where

import Control.Monad
import Data.List
import Data.Char
import Language.Haskell.Liquid.ProofCombinators 


{-@ type NonEmpty a = {v: [a] | 0 < len v} @-}
{-@ msc :: Ord a => NonEmpty a -> Int @-}
msc :: Ord a => [a] -> Int
msc xs = maximum[scount z zs | z:zs <- tails xs]
scount x xs = length(filter(x<)xs)

{- Tests -}

split :: [a] -> ([a], [a])
split xs = splitAt (((length xs) + 1) `div` 2) xs

msc xs
  = msc [1] 
  ==. msc [2]
  ==. msc ['A']
  ==. msc ['a']
  ==. msc ['b', 'a']
  ==. 0
  *** QED

ys = fst split xs
zs = snd split xs

msc xs
  = join(msc fst split xs)(msc snd split xs)
  ==. join(msc ys)(msc zs)
  ==. msc (ys ++ zs)
  *** QED


{- O(n lg n) -}

table [x] = [(x, 0)]
table xs = join (m - n) (table ys) (table zs)
            where m = length xs
                  n = m `div` 2
                  (ys, zs) = splitAt n xs

join 0 txs [] = txs
join n [] tys = tys
join n txs@((x, c): txs') tys@((y, d): tys')
              | x < y = (x, c + n): join n txs' tys
              | x >= y = (y, d): join (n - 1) txs tys'

mscP xs = maximum map (snd) (table xs)