isSorted.idr

module Main

-- Definition of what it means for List to be sorted
data Sorted : (v : List Nat) -> Type
    where
        -- empty list is always sorted
        EmptySorted : Sorted []
        -- list of one element is always sorted
        OneSorted : (a : Nat) -> Sorted [a]
        -- list of two or more element is sorted iff both are true
        -- * first is less or equal than second
        -- * tail is sorted
        RecSorted : (a : Nat) -> (b : Nat) -> (rem : List Nat)
            -> LTE a b -> Sorted (b :: rem) -> Sorted (a :: b :: rem)

-- Proof that list is not sorted if first element is greater than second
total
notSortedE1E2 : (a : Nat) -> (b : Nat) -> (rem : List Nat)
    -> Not (LTE a b) -> Sorted (a :: b :: rem) -> Void
notSortedE1E2 _ _ _ _ EmptySorted impossible
notSortedE1E2 _ _ _ _ (OneSorted _) impossible
notSortedE1E2 a b rem notLTE (RecSorted a b rem lte _) = notLTE lte

-- Proof that list is not sorted if tail is not sorted
total
notSortedBRem : (a : Nat) -> (b : Nat) -> (rem : List Nat)
    -> Not (Sorted (b :: rem)) -> Sorted (a :: b :: rem) -> Void
notSortedBRem _ _ _ _ EmptySorted impossible
notSortedBRem _ _ _ _ (OneSorted _) impossible
notSortedBRem a b rem notSorted (RecSorted _ _ _ _ sorted) = notSorted sorted

total
isSorted : (v : List Nat) -> Dec (Sorted v)
isSorted [] = Yes EmptySorted
isSorted [a] = Yes $ OneSorted a
isSorted (a :: b :: rem) with (isLTE a b, isSorted (b :: rem))
    -- if first is less or equal then second and tail is sorted, then it is sorted
    isSorted (a :: b :: rem) | (Yes prfLTE, Yes prfSortedBRem) = Yes $ RecSorted a b rem prfLTE prfSortedBRem
    -- otherwise it is not sorted
    isSorted (a :: b :: rem) | (_, No contra) = No $ notSortedBRem a b rem contra
    isSorted (a :: b :: rem) | (No contra, _) = No $ notSortedE1E2 a b rem contra

-- Non-dependent-types shortcut
total
isSortedBool : (v : List Nat) -> Bool
isSortedBool v = case isSorted v of
    Yes _ => True
    No _ => False

main : IO ()
main = putStrLn $ show $ isSortedBool [2, 3, 5]