week6/camil/BewijsMapFlatten.icl

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