CSci 555: Functional Programming
Spring Semester 1997

Assignment #5
Due Wednesday, 9 April

Prove the following properties using the definitions given at the end. You may use earlier properties in proofs of later ones.

1. Prove for all finite lists xs and ys that
   sumlist (xs ++ ys) = sumlist xs + sumlist ys

2. Prove for all finite lists xs and ys that
   sumlist (xs ++ ys) = sumlist (ys ++ xs)

3. Prove for all finite lists xs that
   length (double xs) = length xs

4. Prove for all natural numbers n that
   fac n = fac2 n

5. Prove for all finite lists xs and ys and all predicates p of the proper type that
   filter p (xs ++ ys) = filter p xs ++ filter p ys

6. Prove for all finite lists xs and all functions f and g of conforming types that
   map (f . g) xs = (map f . map g) xs

    (++) :: [a] -> [a] -> [a]
    [] ++ ys     = ys                        -- append.1
    (x:xs) ++ ys = x:(xs ++ ys)              -- append.2

    length :: [a] -> Int
    length []      = 0                       -- length.1
    length (_:xs)  = 1 + length xs           -- length.2

    map :: (a -> b) -> [a] -> [b]
    map f []     = []                        -- map.1
    map f (x:xs) = f x : map f xs            -- map.2


    filter :: (a -> Bool) -> [a] -> [a]
    filter p []     = []                     -- filter.1
    filter p (x:xs)
        | p x       = x : filter p xs        -- filter.2
	| otherwise = filter p xs            -- filter.3

    (.) :: (b -> c) -> (a -> b) -> (a -> c)
    (f . g) x = f (g x)                      -- composition

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

    double :: [Int] -> [Int]
    double []      = []                      -- double.1
    double (x:xs)  = (2*x):double xs         -- double.2

    fac :: Int -> Int
    fac 0         = 1                        -- fac.1
    fac n | n > 0 = n * fac (n-1)            -- fac.2

    fac2 :: Int -> Int
    fac2 n | n >= 0 = facAux n 1             -- fac2.1
        where 
            facAux 0 p = p                   -- fac2.2
            facAux n p = facAux (n-1) (n*p)  -- fac2.3

UP to CSCI 555 assignments document?