Mercurial > 12ws.info2

comparison exercises/src/Exercise_10.hs @ 26:ce9610f08925

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge
author Markus Kaiser <markus.kaiser@in.tum.de>
date Wed, 09 Jan 2013 19:45:47 +0100
parents 34fea195e238 ea3fba2381bc
children
comparison
equal deleted inserted replaced
24:34fea195e238 26:ce9610f08925
8 8
9 {---------------------------------------------------------------------} 9 {---------------------------------------------------------------------}
10 {- Aufgabe G10.1 -} 10 {- Aufgabe G10.1 -}
11 11
12 {- 12 {-
13 13 \alpha ist wie in den Folien definiert:
14 Abstraktionsfunktion alpha: 14 alpha [] = {}
15 15 alpha (y:ys) = {y} union (alpha ys)
16 \alpha [] = {} -- alpha_empty
17 \alpha (x:xs) = {x} \union \alpha xs -- alpha_cons
18 16
19 Simulationseigenschaften: 17 Simulationseigenschaften:
20 18
21 1. \alpha empty = {} -- sim_empty 19 R_empty: \alpha empty = {}
22 2. \alpha (insert x xs) = {x} \union \alpha xs -- sim_insert 20 : a empty = {}
23 3. isin x xs = x \in \alpha xs -- sim_isin 21 empty = []
24 4. size xs = |\alpha xs| -- sim_size 22
25 23 a empty
26 Implementierung 1 - Listen mit Duplikaten: 24 == a [] -- by def of empty
27 25 == {} -- by def of alpha
28 empty = [] -- imp_empty 26
29 insert x xs = x : xs -- imp_insert 27
30 isin x xs = elem x xs -- imp_isin 28 R_insert: \alpha (insert x xs) = {x} \union \alpha xs
31 size xs = length (nub xs) -- imp_size 29 : a (insert x xs) = {x} union a xs
32 30 insert x xs = (x : xs)
33 elem _ [] = False -- elem_empty 31
34 elem x (y:ys) = x == y || elem x ys -- elem_cons 32 a (insert x xs)
35 33 == a (x : xs) -- by def of insert
36 nub [] = [] -- nub_empty 34 == {x} union (a xs) -- by def of alpha
37 nub (x:xs) | x `elem` xs = nub xs -- nub_cons_elem 35
38 | otherwise = x : nub xs -- nub_cons_notelem 36 R_isin: isin x xs = x \in \alpha xs
39 37 : isin x xs = x \in a xs
40 Korrektheitsbeweise: 38 isin x xs = elem x xs
41 39
42 1. \alpha empty 40 isin x xs
43 = 41 == elem x xs -- by implementation
44 2. \alpha (insert x xs) 42 == x \in (a xs) -- by L_elem
45 = 43
46 3. isin x xs 44 R_size: size xs = |\alpha xs|
47 = 45 : size xs = | a xs|
48 4. size xs 46 size xs = length (nub xs)
49 = 47
48 size xs
49 == length (nub xs) -- by implementation
50 == |a xs| -- by L_length
51
50 52
51 Hilfslemmata: 53 Hilfslemmata:
52 54
53 elem x xs = x \in \alpha xs -- lemma_elem 55 Funktionen:
54 56
55 Proof by structural induction on xs 57 elem x [] = False -- elem_Empty
56 58 elem x (y:ys) = x == y || elem x ys -- elem_Cons
57 Base case: lemma_elem([]) 59
58 To show: 60 nub [] = [] -- nub_Empty
59 61 nub (y:ys) = -- nub_Cons
60 Induction step: lemma_elem(ys) => lemma_elem(y : ys) 62 if y `elem` ys then nub ys
61 IH: 63 else {- not elem -} y : (nub ys)
62 To show: 64
63 65 ---
64 length (nub xs) = |\alpha xs| -- lemma_length 66
65 67 L_elem(xs): elem x xs = x \in a xs
66 Proof by structural induction on xs 68 Proof by structural induction on xs
67 69
68 Base case: lemma_length([]) 70 Base case: L_elem([])
69 To show: 71 To show: elem x [] = x \in a []
70 72 elem x []
71 Induction step: lemma_length(ys) => lemma_length(y : ys) 73 == False -- by elem_Empty
72 IH: 74
73 To show: 75 x \in a []
74 76 == x \in {} -- by alpha
75 Proof by cases: 77 == False -- by {}
76 Case: 78
77 79 Induction step: L_elem(ys) => L_elem(y : ys)
78 Case: 80 IH: elem x ys = x \in (a ys)
81 To show: elem x (y:ys) = x \in a (y:ys)
82 elem x (y:ys)
83 == x == y || elem x ys -- by elem_Cons
84 == x == y || x \in (a ys) -- by IH
85
86 x \in a (y:ys)
87 == x \in ({y} union (a ys)) -- alpha_Cons
88 == x \in {y} || x \in (a ys) -- by union
89 == x == y || x \in (a ys) -- by basic property
90
91 qed
92
93 ---
94
95
96 L_length(xs): length (nub xs) = |a xs|
97 Proof by structural induction on xs
98
99 Base case: L_length([])
100 To show: length (nub []) = |a []|
101 length (nub [])
102 == length [] -- by nub_Empty
103 == 0 -- by def of length
104
105 |a []|
106 == |{}| -- by alpha
107 == 0 -- by def of ||
108
109 Induction step: L_length(ys) => L_length(y : ys)
110 IH: length (nub ys) = |a ys|
111 To show: length (nub (y:ys)) = |a (y:ys)|
112 Proof by cases
113 case: y `elem` ys
114 length (nub (y:ys))
115 == length (nub ys) -- by nub_Cons
116 == |a ys| -- IH
117
118 |a (y:ys)|
119 == |{y} union a ys| -- alpha_Cons
120 == |(a ys)| -- by basic property
121
122 case: not (y `elem` ys)
123 length (nub (y:ys))
124 == length (y : (nub ys)) -- by nub_Cons
125 == 1 + length [] + length (nub ys) -- by length_Cons
126 == 1 + length (nub ys) -- by length_Empty
127 == 1 + |a ys| -- IH
128
129 |a (y:ys)|
130 == |{y} union a ys| -- alpha_Cons
131 == |{y}| + |a ys| -- by def of union, case
132 == 1 + |a ys| -- by def of ||
133
134 qed
79 135
80 -} 136 -}
81 137
82 138
83 139
92 {- Aufgabe G10.3 -} 148 {- Aufgabe G10.3 -}
93 149
94 {- siehe Queue.hs und SuperQueue.hs -} 150 {- siehe Queue.hs und SuperQueue.hs -}
95 151
96 {- 152 {-
153 Simulationseigenschaften zu beweisen:
154
155 \alpha empty = []
156 isEmpty q = \alpha q == []
157 \alpha (enqueue x q) = \alpha q ++ [x]
158 ~ isEmpty q ==> \alpha (dequeue q) = (head (\alpha q), tail (\alpha q))
159 q == q' = \alpha q == \alpha q'
160
97 Definition von \alpha: 161 Definition von \alpha:
98 162
99 \alpha (Queue front kcab) = undefined 163 \alpha (Queue front kcab) = front ++ reverse kcab
100 164
101 165 Beweis fuer "empty":
102 Simulationseigenschaften: (5) 166
103 167 \alpha empty
104 168 = \alpha (Queue [] []) -- by def of empty
105 169 = [] ++ reverse [] -- by def of \alpha
106 Beweise: 170 = [] -- by def of reverse, ++
171
172 Beweis fuer "isEmpty":
173
174 Hilfssatz: q == Queue [] [] = \alpha q == []
175
176 isEmpty q
177 = q == Queue [] [] -- by def of isEmpty
178 = \alpha q == [] -- by lemma
179
180 Beweis fuer "enqueue":
181
182 Sei q = Queue front kcab -- by exhaustivity of constructor
183
184 \alpha (enqueue x q)
185 = \alpha (enqueue x (Queue front kcab))
186 -- by def of q
187 = \alpha (Queue (front (x : kcab))) -- by def of enqueue
188 = front ++ reverse (x : kcab) -- by def of \alpha
189 = front ++ (reverse kcab ++ [x]) -- by def of reverse
190 = (front ++ reverse kcab) ++ [x] -- by commutativity of ++
191 = \alpha (Queue front kcab) ++ [x] -- by def of \alpha
192 = \alpha q ++ [x] -- by def of q
193
194 Hilfslemma L:
195
196 Zu beweisen: \alpha (Queue [] kcab) = \alpha (Queue (reverse kcab) [])
197
198 \alpha (Queue [] kcab)
199 = [] ++ reverse kcab -- by def of \alpha
200 = reverse kcab -- by def of ++
201
202 \alpha (Queue (reverse kcab) [])
203 = reverse kcab ++ [] -- by def of \alpha
204 = reverse kcab -- by def of ++
205
206 Beweis fuer "dequeue":
207
208 Annahme: ~ isEmpty q
209
210 Sei q = Queue front kcab
211
212 Fallunterscheidung auf front und kcab:
213
214 Fall front = [], kcab = []:
215 ~ isEmpty (Queue front kcab)
216 = ~ isEmpty (Queue [] [])
217 = False
218 Nichts mehr zu beweisen, weil die Annahme nicht erfuellt ist.
219
220 Fall front /= []:
221 \alpha (dequeue q)
222 = \alpha (dequeue (Queue front kcab))
223 -- def of q
224 = \alpha (head front, Queue (tail front) kcab)
225 -- def of dequeue (2nd equation)
226 = (head front, \alpha (Queue (tail front) kcab))
227 -- \alpha is an homomorphism
228
229 Es bleibt zu beweisen, dass
230
231 head front = head (\alpha q)
232 \alpha (Queue (tail front) kcab) = tail (\alpha q)
233
234 head (\alpha q)
235 = head (\alpha (Queue front kcab)) -- def of q
236 = head (front ++ reverse kcab) -- def of \alpha
237 = head front -- basic prop of head, front /= []
238
239 \alpha (Queue (tail front) kcab)
240 = tail front ++ reverse kcab -- def of \alpha
241
242 tail (\alpha q)
243 = tail (\alpha (Queue front kcab)) -- def of q
244 = tail (front ++ reverse kcab) -- def of \alpha
245 = tail front ++ reverse kcab -- basic prop of tail, front /= []
246
247 Fall front = [], kcab /= []:
248 \alpha (dequeue q)
249 = \alpha (dequeue (Queue front kcab)) -- def of q
250 = \alpha (dequeue (Queue [] kcab)) -- assumption front = []
251 = \alpha (dequeue (Queue (reverse kcab) []))
252 -- def of dequeue (1st equation)
253 = (head (\alpha (Queue (reverse kcab) [])),
254 tail (\alpha (Queue (reverse kcab) [])))
255 -- by reduction to already proved
256 -- case, reverse kcab /= []
257 = (head (\alpha (Queue [] kcab)), tail (\alpha (Queue [] kcab)))
258 -- by lemma L (twice)
259 = (head (\alpha q), tail (\alpha q)) -- by def of q (twice)
260
261 Beweis fuer ==:
262
263 Zu beweisen: q == q' = \alpha q == \alpha q'
264
265 Seien q = Queue (front kcab)
266 q' = Queue (front' kcab')
267
268 q == q'
269 = Queue (front kcab) == Queue (front' kcab')
270 -- by def of q, q'
271 = toList (Queue (front kcab)) == toList (Queue (front' kcab'))
272 -- by def of ==
273 = front ++ reverse kcab == front' ++ reverse kcab'
274 -- by def of toList
275
276 \alpha q == \alpha q'
277 = \alpha (Queue (front kcab)) == \alpha (Queue (front' kcab'))
278 -- by def of ==
279 = front ++ reverse kcab == front' ++ reverse kcab'
280 -- by def of \alpha
281
107 -} 282 -}
108 283
109 284
110 285
111 {---------------------------------------------------------------------} 286 {---------------------------------------------------------------------}