The following theorem is obviously true, but how is it proved (most cleanly and
simply) in Haskell?
Theorem: (nondecreasing xs) => nondecreasing (insert x xs), where:
nondecreasing :: (Ord a) => [a] -> Bool
nondecreasing [] = True
nondecreasing xxs@(x : xs) = and [a <= b | (a, b) <- zip xxs xs]
insert :: (Ord a) => a -> [a] -> [a]
insert x xs = takeWhile (<= x) xs ++ [x] ++ dropWhile (<=
x) xs
Thanks.
_________________________________________________________________
Hotmail® is up to 70% faster. Now good news travels really fast.
http://windowslive.com/online/hotmail?ocid=TXT_TAGLM_WL_HM_70faster_032009
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
