week6/camil/BewijsMapFlatten.icl

   1 Zij gegeven:
   2
   3 (++) :: [a] [a] -> [a]
   4 (++) []     xs = xs                (1)
   5 (++) [y:ys] xs = [y : ys ++ xs]    (2)
   6
   7 map :: (a -> b) [a] -> [b]
   8 map f []       = []                (3)
   9 map f [x:xs]   = [f x : map f xs]  (4)
  10
  11 flatten :: [[a]] -> [a]
  12 flatten []     = []                (5)
  13 flatten [x:xs] = x ++ (flatten xs) (6)
  14
  15 1.
  16 Te bewijzen:
  17         voor iedere functie f, eindige lijst as en bs:
  18
  19                 map f (as ++ bs) = (map f as) ++ (map f bs)
  20
  21 Bewijs:
  22 Met inductie over as.
  23
  24 Inductiebasis:
  25 Stel as = []. Dan hebben we:
  26
  27     map f (as ++ bs)                        // aanname as = []
  28     = map f ([] ++ bs)                      // definitie van ++, regel 1
  29     = map f bs                              // definitie van ++, regel 1
  30     = [] ++ (map f bs)                      // definitie van map, regel 3
  31     = (map f []) ++ (map f bs)              // aanname as = []
  32     = (map f as) ++ (map f bs).
  33
  34 Inductiestap:
  35 Stel map f (as ++ bs) = (map f as) ++ (map f bs) voor zekere as en elke bs (inductiehypothese). Dan hebben we:
  36
  37     map f ([a:as] ++ bs)                    // definitie van ++, regel 2
  38     = map f [a:as ++ bs]                    // definitie van map, regel 4
  39     = [f a : map f (as ++ bs)]              // inductiehypothese: map f (as ++ bs) = (map f as) ++ (map f bs)
  40     = [f a : (map f as) ++ (map f bs)]      // lijst herschrijven
  41     = [f a : map f as] ++ (map f bs)        // definitie van map, regel 4
  42     = (map f [a:as]) ++ (map f bs).
  43
  44 Uit het principe van volledige inductie volgt nu dat voor iedere functie f, eindige lijst as en bs:
  45
  46     map f (as ++ bs) = (map f as) ++ (map f bs)     (9.4.1)
  47
  48 2.
  49 Te bewijzen:
  50         voor iedere functie f, voor iedere eindige lijst xs:
  51
  52                 flatten (map (map f) xs) = map f (flatten xs)
  53
  54 Bewijs:
  55 Met inductie over xs.
  56
  57 Inductiebasis:
  58 Stel xs = []. Dan hebben we:
  59
  60     flatten (map (map f) xs)                    // aanname xs = []
  61     = flatten (map (map f) [])                  // definitie van map, regel 3
  62     = flatten []                                // definitie van flatten, regel 5
  63     = []                                        // definitie van map, regel 3
  64     = map f []                                  // definitie van flatten, regel 5
  65     = map f (flatten [])                        // aanname xs = []
  66     = map f (flatten xs).
  67
  68 Inductiestap:
  69 Stel flatten (map (map f) xs) = map f (flatten xs) voor een zekere eindige lijst xs (inductiehypothese). Dan hebben we:
  70
  71     flatten (map (map f) [x:xs])                // definitie van map, regel 4
  72     = flatten [map f x : map (map f) xs]        // definitie van flatten, regel 6
  73     = (map f x) ++ flatten (map (map f) xs)     // inductiehypothese: flatten (map (map f) xs) = map f (flatten xs)
  74     = (map f x) ++ (map f (flatten xs))         // 9.4.1
  75     = map f (x ++ (flatten xs))                 // definitie van flatten, regel 6
  76     = map f (flatten [x:xs]).
  77
  78 Uit het principe van volledige inductie volgt nu dat voor iedere functie f en eindige lijst xs geldt:
  79
  80     flatten (map (map f) xs) = map f (flatten xs)