last-append.hs

-- Given:

append a []     = a : []          -- 1.1
append a (x:xs) = x : append a xs -- 1.2

last []       = Nothing -- 2.1
last (x : []) = Just x  -- 2.2
last (x : xs) = last xs -- 2.3

-- Prove:

last (append a l) == Just a

-- Basic case, l is empty:

last (append a []) = -- 1.1
= last (a : [])    = -- 2.2
= Just  a 

-- l is non-empty i.e. (x : xs)

-- Assume it works for the sub-case, i.e.
last (append a xs) == Just a -- (assumption)
-- We need to prove last (append a (x : xs)) = Just a

last (append a (x:xs))     = -- 1.2
= last (x : (append a xs)) = -- 2.3
= last (append a xs)       = -- (assumption)
= Just a

-- By induction we have proven it for all lists.