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