summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--week6/camil/9.4.123
-rw-r--r--week6/camil/9.4.224
-rw-r--r--week6/camil/BewijsMapFlatten.icl80
3 files changed, 80 insertions, 47 deletions
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