From: Mart Lubbers <mart@martlubbers.net>
Date: Mon, 16 Mar 2015 12:00:37 +0000 (+0100)
Subject: week 6 done
X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=44595aeffa1932cbb41869d6ef87bc55f0521673;p=fp1415.git

week 6 done
---

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.