Formal Reasoning: Example

Suppose we are given the following function definitions:

addNats   :: Int -> Int
addNats 0  = 0                     -- addNats.1
addNats n  = n + addNats (n - 1)   -- addNats.2

natList   :: Int -> [Int]
natList 0  = []                    -- natList.1
natList n  = n : natList (n - 1)   -- natList.2

sumList        :: [Int] -> Int
sumList []      = 0                -- sumList.1
sumList (x:xs)  = x + sumList xs   -- sumList.2

Show by equational reasoning and induction that, for every natural number n, we have

addNats n = sumList (natList (n))

Do not forget to provide justifications for each proof step.

Gabriele Keller

Last modified: Tue Oct 30 09:29:45 EST 2001