diff options
Diffstat (limited to 'week6/mart')
| -rw-r--r-- | week6/mart/BewijsMapFlatten.icl | 97 |
1 files changed, 97 insertions, 0 deletions
diff --git a/week6/mart/BewijsMapFlatten.icl b/week6/mart/BewijsMapFlatten.icl new file mode 100644 index 0000000..59fa5bc --- /dev/null +++ b/week6/mart/BewijsMapFlatten.icl @@ -0,0 +1,97 @@ +Zij gegeven:
+
+(++) :: [a] [a] -> [a]
+(++) [] xs = xs (1)
+(++) [y:ys] xs = [y : ys ++ xs] (2)
+
+map :: (a -> b) [a] -> [b]
+map f [] = [] (3)
+map f [x:xs] = [f x : map f xs] (4)
+
+flatten :: [[a]] -> [a]
+flatten [] = [] (5)
+flatten [x:xs] = x ++ (flatten xs) (6)
+
+1.
+Te bewijzen:
+ voor iedere functie f, eindige lijst as en bs:
+
+ map f (as ++ bs) = (map f as) ++ (map f bs)
+
+Bewijs:
+ met inductie naar de lengte van as.
+
+ Basis:
+ aanname: as = [].
+
+ map f ([] ++ bs) = (map f []) ++ (map f bs) basis
+ ********
+ => map f (bs) = (map f []) ++ (map f bs) (1)
+ ********
+ => map f (bs) = [] ++ (map f bs) (3)
+ ****************
+ => map f bs = map f bs (1)
+
+ Inductiestap:
+ aanname: stelling geldt voor zekere as, ofwel:
+ map f (as ++ bs) = (map f as) ++ (map f bs) (IH)
+
+ Te bewijzen: stelling geldt ook voor as, ofwel:
+ map f ([a:as] ++ bs) = (map f [a:as]) ++ (map f bs)
+
+ map f ([a:as] ++ bs) = (map f [a:as]) ++ (map f bs) basis
+ ************
+ => map f [a:as ++ bs] = (map f [a:as]) ++ (map f bs) (2)
+ ******************
+ => [f a : map f (as ++ bs)] = (map f [a:as]) ++ (map f bs) (4)
+ ************
+ => [f a : map f (as ++ bs)] = [f a : map f as] ++ (map f bs) (4)
+ ****************************
+ => [f a : map f (as ++ bs)] = [f a : (map f as) ++ (map f bs)] (4)
+ **************** ************************
+ => map f (as ++ bs) = (map f as) ++ (map f bs) (IH)
+
+ Dus: basis + inductiestap => stelling bewezen.
+
+2.
+Te bewijzen:
+ voor iedere functie f, voor iedere eindige lijst xs:
+
+ flatten (map (map f) xs) = map f (flatten xs)
+
+Bewijs:
+ met inductio van de lengte van xs
+
+ Basis:
+ aanname: xs = [].
+
+ flatten (map (map f) []) = map f (flatten []) basis
+ **************
+ = flatten [] = map f (flatten []) (3)
+ **********
+ = flatten [] = map f [] (5)
+ **********
+ = [] = map f [] (5)
+ *****
+ = [] = [] (3)
+
+ Inductiestap:
+ aanname: stelling geldt voor zekere xs, ofwel:
+ flatten (map (map f) xs) = map f (flatten xs)
+
+ Te bewijzen: stelling geldt ook voor xs, ofwel:
+ flatten (map (map f) [x:xs]) = map f (flatten [x:xs])
+
+ flatten (map (map f) [x:xs]) = map f (flatten [x:xs]) basis
+ ******************
+ => flatten [map f x: map (map f) xs] = map f (flatten [x:xs]) (4)
+ *********************************
+ => (map f x) ++ (flatten (map (map f) xs)) = map f (flatten [x:xs]) (6)
+ **************
+ => (map f x) ++ (flatten (map (map f) xs)) = map f (x ++ (flatten xs)) (6)
+ *************************
+ => (map f x) ++ (flatten (map (map f) xs)) = (map f x) ++ (map f (flatten xs)) (9.4.1)
+ ************************ ****************
+ => flatten (map (map f) xs) = map f (flatten xs) (IH)
+
+ Dus: basis + inductiestap => stelling bewezen.
|