Problems 3                             

Proof by Induction

Assume the following definitions.

sumlist1 [] = 0  sumlist1.0

sumlist1 x:xs = x + sumlist1 xs   sumlist1.1

sumlist2 xs = foldr + 0 xs          sumlist2.0

double1 [] = []  double1.0

double1 x:xs =(2* x) : double1 xs         double1.1

double2 xs = map (2*) xs         double2.0

rev1 [] = []       rev1.0

rev1 x:xs = rev1 xs ++ [x]         rev1.1

rev2 ([],ys) = ys            rev2.0

rev2 (x:xs,ys) = rev2(xs, x:ys)   rev2.1

rev2 (xs,[]) ++ [x] = rev2 (xs,[x])  rev2.2

True && x = x &&.0

False && x = False      &&.1

foldr f a [] =a    foldr.0

foldr f a x:xs = f x (foldr f a xs)  foldr.1

map f [] = []     map.0

map f x:xs = (f x) : map f xs       map.1

 

Now prove the following by case or by induction

  1. For all Booleans, && is associative.
  2. For all Booleans, && is commutative.
  3. For all finite xs. sumlist1 xs = sumlist2 xs.
  4. For all finite xs. double1 xs = double2 xs.
  5. For all finite xs. rev1 xs = rev2 (xs,[]) .