blob: 59fa5bc4dcf26993e9a5f4eef4e87b109f7b33a4 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
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.
|
