R J wrote:
> 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
Since insert involves list concatenation at the outermost level, the
first step is to prove a lemma along the lines of
nondecreasing xs && nondecreasing ys && (last xs <= head ys)
=>
nondecreasing (xs ++ ys)
from which the wanted theorem follows immediately. The lemma itself is
proved readily by noting/proving
and (xs ++ ys)
= and xs && and ys
zip (xs ++ ys) (tail (xs ++ ys))
~= zip xs (tail xs) ++ [(last xs, head ys)] ++ zip ys (tail ys)
Regards,
apfelmus
--
http://apfelmus.nfshost.com
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
