|
23
|
1 module Exercise_10 (module Join, module SafeMap) where |
|
|
2 |
|
|
3 {- Library DO NOT CHANGE -} |
|
|
4 import SafeMap (SafeMap, empty, update, lookup) |
|
|
5 import Join (Field, doJoin, doJoinFormat, parseFormat) |
|
|
6 {- End Library -} |
|
|
7 |
|
|
8 |
|
|
9 {---------------------------------------------------------------------} |
|
|
10 {- Aufgabe G10.1 -} |
|
|
11 |
|
|
12 {- |
|
25
|
13 \alpha ist wie in den Folien definiert: |
|
|
14 alpha [] = {} |
|
|
15 alpha (y:ys) = {y} union (alpha ys) |
|
23
|
16 |
|
|
17 Simulationseigenschaften: |
|
|
18 |
|
|
19 R_empty: \alpha empty = {} |
|
|
20 : a empty = {} |
|
25
|
21 empty = [] |
|
|
22 |
|
|
23 a empty |
|
|
24 == a [] -- by def of empty |
|
|
25 == {} -- by def of alpha |
|
23
|
26 |
|
|
27 |
|
|
28 R_insert: \alpha (insert x xs) = {x} \union \alpha xs |
|
|
29 : a (insert x xs) = {x} union a xs |
|
25
|
30 insert x xs = (x : xs) |
|
23
|
31 |
|
25
|
32 a (insert x xs) |
|
|
33 == a (x : xs) -- by def of insert |
|
|
34 == {x} union (a xs) -- by def of alpha |
|
23
|
35 |
|
|
36 R_isin: isin x xs = x \in \alpha xs |
|
25
|
37 : isin x xs = x \in a xs |
|
|
38 isin x xs = elem x xs |
|
23
|
39 |
|
25
|
40 isin x xs |
|
|
41 == elem x xs -- by implementation |
|
|
42 == x \in (a xs) -- by L_elem |
|
23
|
43 |
|
|
44 R_size: size xs = |\alpha xs| |
|
25
|
45 : size xs = | a xs| |
|
|
46 size xs = length (nub xs) |
|
23
|
47 |
|
25
|
48 size xs |
|
|
49 == length (nub xs) -- by implementation |
|
|
50 == |a xs| -- by L_length |
|
23
|
51 |
|
|
52 |
|
|
53 Hilfslemmata: |
|
|
54 |
|
25
|
55 Funktionen: |
|
|
56 |
|
|
57 elem x [] = False -- elem_Empty |
|
|
58 elem x (y:ys) = x == y || elem x ys -- elem_Cons |
|
|
59 |
|
|
60 nub [] = [] -- nub_Empty |
|
|
61 nub (y:ys) = -- nub_Cons |
|
|
62 if y `elem` ys then nub ys |
|
|
63 else {- not elem -} y : (nub ys) |
|
|
64 |
|
|
65 --- |
|
|
66 |
|
|
67 L_elem(xs): elem x xs = x \in a xs |
|
23
|
68 Proof by structural induction on xs |
|
|
69 |
|
|
70 Base case: L_elem([]) |
|
25
|
71 To show: elem x [] = x \in a [] |
|
|
72 elem x [] |
|
|
73 == False -- by elem_Empty |
|
|
74 |
|
|
75 x \in a [] |
|
|
76 == x \in {} -- by alpha |
|
|
77 == False -- by {} |
|
23
|
78 |
|
25
|
79 Induction step: L_elem(ys) => L_elem(y : ys) |
|
|
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 --- |
|
23
|
94 |
|
|
95 |
|
25
|
96 L_length(xs): length (nub xs) = |a xs| |
|
23
|
97 Proof by structural induction on xs |
|
|
98 |
|
25
|
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 || |
|
23
|
108 |
|
25
|
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 |
|
23
|
135 |
|
|
136 -} |
|
|
137 |
|
|
138 |
|
|
139 |
|
|
140 {---------------------------------------------------------------------} |
|
|
141 {- Aufgabe G10.2 -} |
|
|
142 |
|
|
143 {- siehe SetPairList.hs -} |
|
|
144 |
|
|
145 |
|
|
146 |
|
|
147 {---------------------------------------------------------------------} |
|
|
148 {- Aufgabe G10.3 -} |
|
|
149 |
|
|
150 {- siehe Queue.hs und SuperQueue.hs -} |
|
|
151 |
|
|
152 {- |
|
25
|
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 |
|
23
|
161 Definition von \alpha: |
|
|
162 |
|
25
|
163 \alpha (Queue front kcab) = front ++ reverse kcab |
|
|
164 |
|
|
165 Beweis fuer "empty": |
|
|
166 |
|
|
167 \alpha empty |
|
|
168 = \alpha (Queue [] []) -- by def of empty |
|
|
169 = [] ++ reverse [] -- by def of \alpha |
|
|
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 |
|
23
|
183 |
|
25
|
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. |
|
23
|
219 |
|
25
|
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 |
|
23
|
230 |
|
25
|
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 /= [] |
|
23
|
246 |
|
25
|
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) |
|
23
|
260 |
|
25
|
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 |
|
23
|
282 -} |
|
|
283 |
|
|
284 |
|
|
285 |
|
|
286 {---------------------------------------------------------------------} |
|
|
287 {- Aufgabe H10.1 -} |
|
|
288 |
|
|
289 {- siehe SafeMap.hs -} |
|
|
290 |
|
|
291 |
|
|
292 |
|
|
293 {---------------------------------------------------------------------} |
|
|
294 {- Aufgabe H10.2 -} |
|
|
295 |
|
|
296 {- siehe Join.hs -} |
|
|
297 |
|
|
298 |
|
|
299 |
|
|
300 {---------------------------------------------------------------------} |
|
|
301 {- Aufgabe H10.3 -} |
|
|
302 |
|
|
303 {- siehe Morsi.hs -} |
