summaryrefslogtreecommitdiff
path: root/fp1/week6/mart/BewijsMapFlatten.icl
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.