From e038bd97c96eef24418d63dd236116073205ad56 Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Wed, 18 Mar 2015 13:05:33 +0100 Subject: [PATCH] Put w6 in format --- week6/camil/9.4.1 | 23 --------- week6/camil/9.4.2 | 24 ---------- week6/camil/BewijsMapFlatten.icl | 80 ++++++++++++++++++++++++++++++++ 3 files changed, 80 insertions(+), 47 deletions(-) delete mode 100644 week6/camil/9.4.1 delete mode 100644 week6/camil/9.4.2 create mode 100644 week6/camil/BewijsMapFlatten.icl diff --git a/week6/camil/9.4.1 b/week6/camil/9.4.1 deleted file mode 100644 index d9b2608..0000000 --- a/week6/camil/9.4.1 +++ /dev/null @@ -1,23 +0,0 @@ -9.4.1 - proof by induction over as - -Induction base: - Suppose as = []. Then we have: - - map f (as ++ bs) // assumption as = [] - = map f ([] ++ bs) // definition of ++, rule 1 - = map f bs // definition of ++, rule 1 - = [] ++ (map f bs) // definition of map, rule 3 - = (map f []) ++ (map f bs) // assumption as = [] - = (map f as) ++ (map f bs). - -Induction step: - Suppose map f (as ++ bs) = (map f as) ++ (map f bs) for certain as and any bs (induction hypothesis). Then we have: - - map f ([a:as] ++ bs) // definition of ++, rule 2 - = map f [a:as ++ bs] // definition of map, rule 4 - = [f a : map f (as ++ bs)] // induction hypothesis: assumption map f (as ++ bs) = (map f as) ++ (map f bs) - = [f a : (map f as) ++ (map f bs)] // rewriting list - = [f a : map f as] ++ (map f bs) // definition of map, rule 4 - = (map f [a:as]) ++ (map f bs). - -By the principle of induction we have now proven that map f (as ++ bs) = (map f as) ++ (map f bs) for any finite lists as, bs. \ No newline at end of file diff --git a/week6/camil/9.4.2 b/week6/camil/9.4.2 deleted file mode 100644 index bc95352..0000000 --- a/week6/camil/9.4.2 +++ /dev/null @@ -1,24 +0,0 @@ -9.4.2 - proof by induction over xs - -Induction base: - Suppose xs = []. Then we have: - - flatten (map (map f) xs) // assumption xs = [] - = flatten (map (map f) []) // definition of map, rule 3 - = flatten [] // definition of flatten, rule 5 - = [] // definition of map, rule 3 - = map f [] // definition of flatten, rule 5 - = map f (flatten []) // assumption xs = [] - = map f (flatten xs). - -Induction step: - Suppose flatten (map (map f) xs) = map f (flatten xs) for certain xs of finite length (induction hypothesis). Then we have: - - flatten (map (map f) [x:xs]) // definition of map, rule 4 - = flatten [map f x : map (map f) xs] // definition of flatten, rule 6 - = (map f x) ++ flatten (map (map f) xs) // induction hypothesis: assumption flatten (map (map f) xs) = map f (flatten xs) - = (map f x) ++ (map f (flatten xs)) // by 9.4.1 - = map f (x ++ (flatten xs)) // definition of flatten, rule 6 - = map f (flatten [x:xs]). - -By the principle of induction we have now proven that flatten (map (map f) xs) = map f (flatten xs) for any list of finite length xs. \ No newline at end of file diff --git a/week6/camil/BewijsMapFlatten.icl b/week6/camil/BewijsMapFlatten.icl new file mode 100644 index 0000000..44cf7c1 --- /dev/null +++ b/week6/camil/BewijsMapFlatten.icl @@ -0,0 +1,80 @@ +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 over as. + +Inductiebasis: +Stel as = []. Dan hebben we: + + map f (as ++ bs) // aanname as = [] + = map f ([] ++ bs) // definitie van ++, regel 1 + = map f bs // definitie van ++, regel 1 + = [] ++ (map f bs) // definitie van map, regel 3 + = (map f []) ++ (map f bs) // aanname as = [] + = (map f as) ++ (map f bs). + +Inductiestap: +Stel map f (as ++ bs) = (map f as) ++ (map f bs) voor zekere as en elke bs (inductiehypothese). Dan hebben we: + + map f ([a:as] ++ bs) // definitie van ++, regel 2 + = map f [a:as ++ bs] // definitie van map, regel 4 + = [f a : map f (as ++ bs)] // inductiehypothese: map f (as ++ bs) = (map f as) ++ (map f bs) + = [f a : (map f as) ++ (map f bs)] // lijst herschrijven + = [f a : map f as] ++ (map f bs) // definitie van map, regel 4 + = (map f [a:as]) ++ (map f bs). + +Uit het principe van volledige inductie volgt nu dat voor iedere functie f, eindige lijst as en bs: + + map f (as ++ bs) = (map f as) ++ (map f bs) (9.4.1) + +2. +Te bewijzen: + voor iedere functie f, voor iedere eindige lijst xs: + + flatten (map (map f) xs) = map f (flatten xs) + +Bewijs: +Met inductie over xs. + +Inductiebasis: +Stel xs = []. Dan hebben we: + + flatten (map (map f) xs) // aanname xs = [] + = flatten (map (map f) []) // definitie van map, regel 3 + = flatten [] // definitie van flatten, regel 5 + = [] // definitie van map, regel 3 + = map f [] // definitie van flatten, regel 5 + = map f (flatten []) // aanname xs = [] + = map f (flatten xs). + +Inductiestap: +Stel flatten (map (map f) xs) = map f (flatten xs) voor een zekere eindige lijst xs (inductiehypothese). Dan hebben we: + + flatten (map (map f) [x:xs]) // definitie van map, regel 4 + = flatten [map f x : map (map f) xs] // definitie van flatten, regel 6 + = (map f x) ++ flatten (map (map f) xs) // inductiehypothese: flatten (map (map f) xs) = map f (flatten xs) + = (map f x) ++ (map f (flatten xs)) // 9.4.1 + = map f (x ++ (flatten xs)) // definitie van flatten, regel 6 + = map f (flatten [x:xs]). + +Uit het principe van volledige inductie volgt nu dat voor iedere functie f en eindige lijst xs geldt: + + flatten (map (map f) xs) = map f (flatten xs) \ No newline at end of file -- 2.20.1