From 34b4a8162a94d30974432f5a4f40369c82c08b59 Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Wed, 18 Mar 2015 10:27:23 +0100 Subject: [PATCH] Added comments --- week6/camil/9.4.1 | 18 +++++++++++++++--- week6/camil/9.4.2 | 19 ++++++++++++++++--- 2 files changed, 31 insertions(+), 6 deletions(-) diff --git a/week6/camil/9.4.1 b/week6/camil/9.4.1 index 0f279ca..d9b2608 100644 --- a/week6/camil/9.4.1 +++ b/week6/camil/9.4.1 @@ -2,10 +2,22 @@ Induction base: Suppose as = []. Then we have: - map f (as ++ bs) = map f ([] ++ bs) = map f bs = [] ++ (map f bs) = (map f []) ++ (map f bs) = (map f as) ++ (map f bs). + + 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. Then we have: - map f ([a:as] ++ bs) = map f [a:as ++ bs] = [f a : map f (as ++ bs)] = [f a : (map f as) ++ (map f bs)] = [f a : map f as] ++ (map f bs) = (map f [a:as]) ++ (map f bs). + 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 index c23b58e..bc95352 100644 --- a/week6/camil/9.4.2 +++ b/week6/camil/9.4.2 @@ -2,10 +2,23 @@ Induction base: Suppose xs = []. Then we have: - flatten (map (map f) xs) = flatten (map (map f) []) = flatten [] = [] = map f [] = map f (flatten []) = map f (flatten xs). + + 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. Then we have: - flatten (map (map f) [x:xs]) = flatten [map f x : map (map f) xs] = (map f x) ++ flatten (map (map f) xs) = (map f x) ++ (map f (flatten xs)) =(9.4.1) map f (x ++ (flatten xs)) = map f (flatten [x:xs]). + 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 -- 2.20.1