From 6f604b19d3f5966e5c1d7c4fdf3703bd6ff0861c Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Thu, 16 Apr 2015 21:22:20 +0200 Subject: update to fp2 yay, public and licence --- fp1/week6/camil/BewijsMapFlatten.icl | 83 ++++++++++++++++++++++++++++++ fp1/week6/mart/BewijsMapFlatten.icl | 97 ++++++++++++++++++++++++++++++++++++ 2 files changed, 180 insertions(+) create mode 100644 fp1/week6/camil/BewijsMapFlatten.icl create mode 100644 fp1/week6/mart/BewijsMapFlatten.icl (limited to 'fp1/week6') diff --git a/fp1/week6/camil/BewijsMapFlatten.icl b/fp1/week6/camil/BewijsMapFlatten.icl new file mode 100644 index 0000000..7f2474e --- /dev/null +++ b/fp1/week6/camil/BewijsMapFlatten.icl @@ -0,0 +1,83 @@ +// Mart Lubbers, s4109503 +// Camil Staps, s4498062 + +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) diff --git a/fp1/week6/mart/BewijsMapFlatten.icl b/fp1/week6/mart/BewijsMapFlatten.icl new file mode 100644 index 0000000..59fa5bc --- /dev/null +++ b/fp1/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. -- cgit v1.2.3