\begin{code}
{-# OPTIONS_GHC -Wall #-}
module Jan19 where
import Data.List (partition)
\end{code}
Learning objectives:
\begin{itemize}
\item sorting (quicksort, insertion)
\item ‘conceptual clarity’
\item proofs by induction
\end{itemize}
Recall ‘quicksort pattern’:
\begin{enumerate}
\item pick a pivot
\item partition rest of elements in < and >=
\item recursively sort
\item put lists back together
\end{enumerate}
\begin{code}
qs :: Ord a => [a] -> [a]
qs [] = []
qs (x : xs) = (qs l) ++ (x : qs r)
where (l, r) = partition (< x) xs
\end{code}
Lists in Haskell are \emph{linked lists}.
And now 'insertion sort':
\begin{enumerate}
\item for every element in the source list,
\item insert it 'in the right place' in the sorted output list
\end{enumerate}
\begin{code}
insert :: Ord a => a -> [a] -> [a]
insert x [] = [x]
insert x l@(y : ys) | x < y = x : l
| otherwise = y : insert x ys
insertionsort :: Ord a => [a] -> [a]
insertionsort = foldr insert []
\end{code}
(where we eta-contracted ‘insertionsort’)
\newpage
Induction!
\begin{code}
sum’ :: [Integer] -> Integer
sum’ [] = 0 — sum.1
sum’ (x : xs) = x + sum’ xs — sum.2
— the better definion: sum’ = foldr (+) 0
\end{code}
Induction Principle for lists: to prove predicate P holds for all lists
\begin{enumerate}
\item prove P []
\item forall x, xs. prove that P xs implies P (x : xs)
\item conclude forall l . P l
\end{enumerate}
\begin{code}
map’ :: (a -> b) -> [a] -> [b]
map’ _ [] = [] — map.1
map’ f (x : xs) = f x : map’ f xs — map.2
doubleAll :: [Integer] -> [Integer]
doubleAll = map’ (2 *)
\end{code}
Prove the following: forall l. sum (doubleAll l) = 2 * sum l
\begin{verbatim}
Base case: l = []
lhs: sum (doubleAll []) = — definition
sum (map’ (2 *) []) = — map.1
sum [] = — sum.1
0 = — 0 = 2 * 0
2 * 0 = — sum.1
2 * sum []
rhs:
Inductive case. Assume true for l = xs
lhs:
sum (doubleAll (x : xs)) = — definition
sum (map (2 *) (x : xs)) = — map.2
sum ((2 *) x : map (2 *) xs) = — applying (2 *) x
sum (2 * x : map (2 *) xs) = — sum.2
(2 * x) + sum (map (2 *) xs) = — ih
(2 * x) + 2 * sum xs = — distribute *
2 * (x + sum xs) = — sum.2
2 * (sum (x : xs))
\end{verbatim}
(We’ll format these more nicely later)