From 509520ebc8b75075575671dc96dc6ae3733f51a6 Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Tue, 17 Mar 2015 22:29:26 +0100 Subject: [PATCH] w6 camil --- week6/camil/9.4.1 | 11 +++++++++++ week6/camil/9.4.2 | 11 +++++++++++ 2 files changed, 22 insertions(+) create mode 100644 week6/camil/9.4.1 create mode 100644 week6/camil/9.4.2 diff --git a/week6/camil/9.4.1 b/week6/camil/9.4.1 new file mode 100644 index 0000000..0f279ca --- /dev/null +++ b/week6/camil/9.4.1 @@ -0,0 +1,11 @@ +9.4.1 - proof by induction over as + +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). + +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). + +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 new file mode 100644 index 0000000..c23b58e --- /dev/null +++ b/week6/camil/9.4.2 @@ -0,0 +1,11 @@ +9.4.2 - proof by induction over xs + +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). + +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]). + +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