CSci 555: Functional Programming
Fall Semester 2010

Assignment #4
Due Friday, 19 November

This is an individual assignment, which you must complete in accordance with the instructions given in the Professional Conduct and Assignments sections of the Syllabus .

Prove any six of the first seven properties given below using the definitions given at the end. You may use earlier properties in proofs of later ones. You also may, of course, use well-known properties of arithmetic, but please state the properties that you uses as justifications for steps.

Graduate students prove property 8 below.

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 predicates p and q of the proper types that
   filter p (filter q xs) = filter q (filter p xs)

7. Prove for all finite lists of lists xss and all functions f of the appropriate type that
   map f (concat xss) = concat (map (map f) xss)

8. Prove for all Nat values x and y, addNat x y = addNat y x.

    (++) :: [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

    concat :: [[a]] -> [a]
    concat []       = []                     -- concat.1
    concat (xs:xss) = xs ++ concat xss       -- concat.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

    data Nat = Zero | Succ Nat

    addNat :: Nat -> Nat -> Nat
    addNat Zero     y    = y
    addNat x        Zero = x
    addNat (Succ x) y    = addNat x (Succ y)

UP to CSCI 555 assignments document?