week6/mart/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 naar de lengte van as.
  23
  24         Basis:
  25         aanname: as = [].
  26
  27              map f ([] ++ bs) = (map f []) ++ (map f bs)                  basis
  28                    ********
  29           => map f (bs) = (map f []) ++ (map f bs)                        (1)
  30                            ********
  31           => map f (bs) = [] ++ (map f bs)                                (3)
  32                           ****************
  33           => map f bs = map f bs                                          (1)
  34
  35         Inductiestap:
  36         aanname: stelling geldt voor zekere as, ofwel:
  37                 map f (as ++ bs) = (map f as) ++ (map f bs) (IH)
  38
  39         Te bewijzen: stelling geldt ook voor as, ofwel:
  40                 map f ([a:as] ++ bs) = (map f [a:as]) ++ (map f bs)
  41
  42              map f ([a:as] ++ bs) = (map f [a:as]) ++ (map f bs)          basis
  43                  ************
  44           => map f [a:as ++ bs] = (map f [a:as]) ++ (map f bs)            (2)
  45             ******************
  46           => [f a : map f (as ++ bs)] = (map f [a:as]) ++ (map f bs)      (4)
  47                                         ************
  48           => [f a : map f (as ++ bs)] = [f a : map f as] ++ (map f bs)    (4)
  49                                         ****************************
  50           => [f a : map f (as ++ bs)] = [f a : (map f as) ++ (map f bs)]  (4)
  51                    ****************           ************************
  52           => map f (as ++ bs) = (map f as) ++ (map f bs)                  (IH)
  53
  54         Dus: basis + inductiestap => stelling bewezen.
  55
  56 2.
  57 Te bewijzen:
  58         voor iedere functie f, voor iedere eindige lijst xs:
  59
  60                 flatten (map (map f) xs) = map f (flatten xs)
  61
  62 Bewijs:
  63         met inductio van de lengte van xs
  64
  65         Basis:
  66         aanname: xs = [].
  67
  68             flatten (map (map f) []) = map f (flatten [])                                basis
  69                      **************
  70           = flatten [] = map f (flatten [])                                              (3)
  71                                 **********
  72           = flatten [] = map f []                                                        (5)
  73             **********
  74           = [] = map f []                                                                (5)
  75                  *****
  76           = [] = []                                                                      (3)
  77
  78         Inductiestap:
  79         aanname: stelling geldt voor zekere xs, ofwel:
  80                 flatten (map (map f) xs) = map f (flatten xs)
  81
  82         Te bewijzen: stelling geldt ook voor xs, ofwel:
  83                 flatten (map (map f) [x:xs]) = map f (flatten [x:xs])
  84
  85              flatten (map (map f) [x:xs]) = map f (flatten [x:xs])                       basis
  86                       ******************
  87           => flatten [map f x: map (map f) xs] = map f (flatten [x:xs])                  (4)
  88              *********************************
  89           => (map f x) ++ (flatten (map (map f) xs)) = map f (flatten [x:xs])            (6)
  90                                                             **************
  91           => (map f x) ++ (flatten (map (map f) xs)) = map f (x ++ (flatten xs))         (6)
  92                                                        *************************
  93           => (map f x) ++ (flatten (map (map f) xs)) = (map f x) ++ (map f (flatten xs)) (9.4.1)
  94                            ************************                  ****************
  95           => flatten (map (map f) xs) = map f (flatten xs)                               (IH)
  96
  97         Dus: basis + inductiestap => stelling  bewezen.