week6/camil/9.4.1

   1 9.4.1 - proof by induction over as
   2
   3 Induction base:
   4     Suppose as = []. Then we have:
   5
   6     map f (as ++ bs)                        // assumption as = []
   7     = map f ([] ++ bs)                      // definition of ++, rule 1
   8     = map f bs                              // definition of ++, rule 1
   9     = [] ++ (map f bs)                      // definition of map, rule 3
  10     = (map f []) ++ (map f bs)              // assumption as = []
  11     = (map f as) ++ (map f bs).
  12
  13 Induction step:
  14     Suppose map f (as ++ bs) = (map f as) ++ (map f bs) for certain as and any bs (induction hypothesis). Then we have:
  15
  16     map f ([a:as] ++ bs)                    // definition of ++, rule 2
  17     = map f [a:as ++ bs]                    // definition of map, rule 4
  18     = [f a : map f (as ++ bs)]              // induction hypothesis: assumption map f (as ++ bs) = (map f as) ++ (map f bs)
  19     = [f a : (map f as) ++ (map f bs)]      // rewriting list
  20     = [f a : map f as] ++ (map f bs)        // definition of map, rule 4
  21     = (map f [a:as]) ++ (map f bs).
  22
  23 By the principle of induction we have now proven that map f (as ++ bs) = (map f as) ++ (map f bs) for any finite lists as, bs.