# [Haskell-cafe] Re: A non-inductive Haskell proof?

Heinrich Apfelmus apfelmus at quantentunnel.de
Mon Mar 16 09:07:53 EDT 2009

```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

```

More information about the Haskell-Cafe mailing list