1 \documentclass[11pt]{article} |
|
2 \usepackage[left]{lineno} |
|
3 \usepackage{amsmath} |
|
4 \usepackage{stmaryrd} |
|
5 |
|
6 \begin{document} |
|
7 %%%\linenumbers |
|
8 |
|
9 \noindent |
|
10 We already proved that |
|
11 |
|
12 \[ |
|
13 \text{If}\;nullable(r)\;\text{then}\;POSIX\;(mkeps\; r)\;r |
|
14 \] |
|
15 |
|
16 \noindent |
|
17 holds. This is essentially the ``base case'' for the |
|
18 correctness proof of the algorithm. For the ``induction |
|
19 case'' we need the following main theorem, which we are |
|
20 currently after: |
|
21 |
|
22 \begin{center} |
|
23 \begin{tabular}{lll} |
|
24 If & (*) & $POSIX\;v\;(der\;c\;r)$ and $\vdash v : der\;c\;r$\\ |
|
25 then & & $POSIX\;(inj\;r\;c\;v)\;r$ |
|
26 \end{tabular} |
|
27 \end{center} |
|
28 |
|
29 \noindent |
|
30 That means a POSIX value $v$ is still $POSIX$ after injection. |
|
31 I am not sure whether this theorem is actually true in this |
|
32 full generality. Maybe it requires some restrictions. |
|
33 |
|
34 If we unfold the $POSIX$ definition in the then-part, we |
|
35 arrive at |
|
36 |
|
37 \[ |
|
38 \forall v'.\; |
|
39 \text{if}\;\vdash v' : r\; \text{and} \;|inj\;r\;c\;v| = |v'|\; |
|
40 \text{then}\; |inj\;r\;c\;v| \succ_r v' |
|
41 \] |
|
42 |
|
43 \noindent |
|
44 which is what we need to prove assuming the if-part (*) in the |
|
45 theorem above. Since this is a universally quantified formula, |
|
46 we just need to fix a $v'$. We can then prove the implication |
|
47 by assuming |
|
48 |
|
49 \[ |
|
50 \text{(a)}\;\;\vdash v' : r\;\; \text{and} \;\; |
|
51 \text{(b)}\;\;inj\;r\;c\;v = |v'| |
|
52 \] |
|
53 |
|
54 \noindent |
|
55 and our goal is |
|
56 |
|
57 \[ |
|
58 (goal)\;\;inj\;r\;c\;v \succ_r v' |
|
59 \] |
|
60 |
|
61 \noindent |
|
62 There are already two lemmas proved that can transform |
|
63 the assumptions (a) and (b) into |
|
64 |
|
65 \[ |
|
66 \text{(a*)}\;\;\vdash proj\;r\;c\;v' : der\;c\;r\;\; \text{and} \;\; |
|
67 \text{(b*)}\;\;c\,\#\,|v| = |v'| |
|
68 \] |
|
69 |
|
70 \noindent |
|
71 Another lemma shows that |
|
72 |
|
73 \[ |
|
74 |v'| = c\,\#\,|proj\;r\;c\;v| |
|
75 \] |
|
76 |
|
77 \noindent |
|
78 Using (b*) we can therefore infer |
|
79 |
|
80 \[ |
|
81 \text{(b**)}\;\;|v| = |proj\;r\;c\;v| |
|
82 \] |
|
83 |
|
84 \noindent |
|
85 The main idea of the proof is now a simple instantiation |
|
86 of the assumption $POSIX\;v\;(der\;c\;r)$. If we unfold |
|
87 the $POSIX$ definition, we get |
|
88 |
|
89 \[ |
|
90 \forall v'.\; |
|
91 \text{if}\;\vdash v' : der\;c\;r\; \text{and} \;|v| = |v'|\; |
|
92 \text{then}\; v \succ_{der\;c\;r}\; v' |
|
93 \] |
|
94 |
|
95 \noindent |
|
96 We can instantiate this $v'$ with $proj\;r\;c\;v'$ and can use |
|
97 (a*) and (b**) in order to infer |
|
98 |
|
99 \[ |
|
100 v \succ_{der\;c\;r}\; proj\;r\;c\;v' |
|
101 \] |
|
102 |
|
103 \noindent |
|
104 The point of the side-lemma below is that we can ``add'' an |
|
105 $inj$ to both sides to obtain |
|
106 |
|
107 \[ |
|
108 inj\;r\;c\;v \succ_r\; inj\;r\;c\;(proj\;r\;c\;v') |
|
109 \] |
|
110 |
|
111 \noindent Finally there is already a lemma proved that shows |
|
112 that an injection and projection is the identity, meaning |
|
113 |
|
114 \[ |
|
115 inj\;r\;c\;(proj\;r\;c\;v') = v' |
|
116 \] |
|
117 |
|
118 \noindent |
|
119 With this we have shown our goal (pending a proof of the side-lemma |
|
120 next). |
|
121 |
|
122 |
|
123 \subsection*{Side-Lemma} |
|
124 |
|
125 A side-lemma needed for the theorem above which might be true, but can also be false, is as follows: |
|
126 |
|
127 \begin{center} |
|
128 \begin{tabular}{lll} |
|
129 If & (1) & $v_1 \succ_{der\;c\;r} v_2$,\\ |
|
130 & (2) & $\vdash v_1 : der\;c\;r$, and\\ |
|
131 & (3) & $\vdash v_2 : der\;c\;r$ holds,\\ |
|
132 then & & $inj\;r\;c\;v_1 \succ_r inj\;r\;c\;v_2$ also holds. |
|
133 \end{tabular} |
|
134 \end{center} |
|
135 |
|
136 \noindent It essentially states that if one value $v_1$ is |
|
137 bigger than $v_2$ then this ordering is preserved under |
|
138 injections. This is proved by induction (on the definition of |
|
139 $der$\ldots this is very similar to an induction on $r$). |
|
140 \bigskip |
|
141 |
|
142 \noindent |
|
143 The case that is still unproved is the sequence case where we |
|
144 assume $r = r_1\cdot r_2$ and also $r_1$ being nullable. |
|
145 The derivative $der\;c\;r$ is then |
|
146 |
|
147 \begin{center} |
|
148 $der\;c\;r = ((der\;c\;r_1) \cdot r_2) + (der\;c\;r_2)$ |
|
149 \end{center} |
|
150 |
|
151 \noindent |
|
152 or without the parentheses |
|
153 |
|
154 \begin{center} |
|
155 $der\;c\;r = (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$ |
|
156 \end{center} |
|
157 |
|
158 \noindent |
|
159 In this case the assumptions are |
|
160 |
|
161 \begin{center} |
|
162 \begin{tabular}{ll} |
|
163 (a) & $v_1 \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} v_2$\\ |
|
164 (b) & $\vdash v_1 : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\ |
|
165 (c) & $\vdash v_2 : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\ |
|
166 (d) & $nullable(r_1)$ |
|
167 \end{tabular} |
|
168 \end{center} |
|
169 |
|
170 \noindent |
|
171 The induction hypotheses are |
|
172 |
|
173 \begin{center} |
|
174 \begin{tabular}{ll} |
|
175 (IH1) & $\forall v_1 v_2.\;v_1 \succ_{der\;c\;r_1} v_2 |
|
176 \;\wedge\; \vdash v_1 : der\;c\;r_1 \;\wedge\; |
|
177 \vdash v_2 : der\;c\;r_1\qquad$\\ |
|
178 & $\hfill\longrightarrow |
|
179 inj\;r_1\;c\;v_1 \succ{r_1} \;inj\;r_1\;c\;v_2$\smallskip\\ |
|
180 (IH2) & $\forall v_1 v_2.\;v_1 \succ_{der\;c\;r_2} v_2 |
|
181 \;\wedge\; \vdash v_2 : der\;c\;r_2 \;\wedge\; |
|
182 \vdash v_2 : der\;c\;r_2\qquad$\\ |
|
183 & $\hfill\longrightarrow |
|
184 inj\;r_2\;c\;v_1 \succ{r_2} \;inj\;r_2\;c\;v_2$\\ |
|
185 \end{tabular} |
|
186 \end{center} |
|
187 |
|
188 \noindent |
|
189 The goal is |
|
190 |
|
191 \[ |
|
192 (goal)\qquad |
|
193 inj\; (r_1 \cdot r_2)\;c\;v_1 \succ_{r_1 \cdot r_2} |
|
194 inj\; (r_1 \cdot r_2)\;c\;v_2 |
|
195 \] |
|
196 |
|
197 \noindent |
|
198 If we analyse how (a) could have arisen (that is make a case |
|
199 distinction), then we will find four cases: |
|
200 |
|
201 \begin{center} |
|
202 \begin{tabular}{ll} |
|
203 LL & $v_1 = Left(w_1)$, $v_2 = Left(w_2)$\\ |
|
204 LR & $v_1 = Left(w_1)$, $v_2 = Right(w_2)$\\ |
|
205 RL & $v_1 = Right(w_1)$, $v_2 = Left(w_2)$\\ |
|
206 RR & $v_1 = Right(w_1)$, $v_2 = Right(w_2)$\\ |
|
207 \end{tabular} |
|
208 \end{center} |
|
209 |
|
210 |
|
211 \noindent |
|
212 We have to establish our goal in all four cases. |
|
213 |
|
214 |
|
215 \subsubsection*{Case LR} |
|
216 |
|
217 The corresponding rule (instantiated) is: |
|
218 |
|
219 \begin{center} |
|
220 \begin{tabular}{c} |
|
221 $len\,|w_1| \geq len\,|w_2|$\\ |
|
222 \hline |
|
223 $Left(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Right(w_2)$ |
|
224 \end{tabular} |
|
225 \end{center} |
|
226 |
|
227 \noindent |
|
228 This means we can also assume in this case |
|
229 |
|
230 \[ |
|
231 (e)\quad len\,|w_1| \geq len\,|w_2| |
|
232 \] |
|
233 |
|
234 \noindent |
|
235 which is the premise of the rule above. |
|
236 Instantiating $v_1$ and $v_2$ in the assumptions (b) and (c) |
|
237 gives us |
|
238 |
|
239 \begin{center} |
|
240 \begin{tabular}{ll} |
|
241 (b*) & $\vdash Left(w_1) : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\ |
|
242 (c*) & $\vdash Right(w_2) : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\ |
|
243 \end{tabular} |
|
244 \end{center} |
|
245 |
|
246 \noindent Since these are assumptions, we can further analyse |
|
247 how they could have arisen according to the rules of $\vdash |
|
248 \_ : \_\,$. This gives us two new assumptions |
|
249 |
|
250 \begin{center} |
|
251 \begin{tabular}{ll} |
|
252 (b**) & $\vdash w_1 : (der\;c\;r_1) \cdot r_2$\\ |
|
253 (c**) & $\vdash w_2 : der\;c\;r_2$\\ |
|
254 \end{tabular} |
|
255 \end{center} |
|
256 |
|
257 \noindent |
|
258 Looking at (b**) we can further analyse how this |
|
259 judgement could have arisen. This tells us that $w_1$ |
|
260 must have been a sequence, say $u_1\cdot u_2$, with |
|
261 |
|
262 \begin{center} |
|
263 \begin{tabular}{ll} |
|
264 (b***) & $\vdash u_1 : der\;c\;r_1$\\ |
|
265 & $\vdash u_2 : r_2$\\ |
|
266 \end{tabular} |
|
267 \end{center} |
|
268 |
|
269 \noindent |
|
270 Instantiating the goal means we need to prove |
|
271 |
|
272 \[ |
|
273 inj\; (r_1 \cdot r_2)\;c\;(Left(u_1\cdot u_2)) \succ_{r_1 \cdot r_2} |
|
274 inj\; (r_1 \cdot r_2)\;c\;(Right(w_2)) |
|
275 \] |
|
276 |
|
277 \noindent |
|
278 We can simplify this according to the rules of $inj$: |
|
279 |
|
280 \[ |
|
281 (inj\; r_1\;c\;u_1)\cdot u_2 \succ_{r_1 \cdot r_2} |
|
282 (mkeps\;r_1) \cdot (inj\; r_2\;c\;w_2) |
|
283 \] |
|
284 |
|
285 \noindent |
|
286 This is what we need to prove. There are only two rules that |
|
287 can be used to prove this judgement: |
|
288 |
|
289 \begin{center} |
|
290 \begin{tabular}{cc} |
|
291 \begin{tabular}{c} |
|
292 $v_1 = v_1'$\qquad $v_2 \succ_{r_2} v_2'$\\ |
|
293 \hline |
|
294 $v_1\cdot v_2 \succ_{r_1\cdot r_2} v_1'\cdot v_2'$ |
|
295 \end{tabular} & |
|
296 \begin{tabular}{c} |
|
297 $v_1 \succ_{r_1} v_1'$\\ |
|
298 \hline |
|
299 $v_1\cdot v_2 \succ_{r_1\cdot r_2} v_1'\cdot v_2'$ |
|
300 \end{tabular} |
|
301 \end{tabular} |
|
302 \end{center} |
|
303 |
|
304 \noindent |
|
305 Using the left rule would mean we need to show that |
|
306 |
|
307 \[ |
|
308 inj\; r_1\;c\;u_1 = mkeps\;r_1 |
|
309 \] |
|
310 |
|
311 \noindent |
|
312 but this can never be the case.\footnote{Actually Isabelle |
|
313 found this out after analysing its argument. ;o)} Lets assume |
|
314 it would be true, then also if we flat each side, it must hold |
|
315 that |
|
316 |
|
317 \[ |
|
318 |inj\; r_1\;c\;u_1| = |mkeps\;r_1| |
|
319 \] |
|
320 |
|
321 \noindent |
|
322 But this leads to a contradiction, because the right-hand side |
|
323 will be equal to the empty list, or empty string. This is |
|
324 because we assumed $nullable(r_1)$ and there is a lemma |
|
325 called \texttt{mkeps\_flat} which shows this. On the other |
|
326 side we know by assumption (b***) and lemma \texttt{v4} that |
|
327 the other side needs to be a string starting with $c$ (since |
|
328 we inject $c$ into $u_1$). The empty string can never be equal |
|
329 to something starting with $c$\ldots therefore there is a |
|
330 contradiction. |
|
331 |
|
332 That means we can only use the rule on the right-hand side to |
|
333 prove our goal. This implies we need to prove |
|
334 |
|
335 \[ |
|
336 inj\; r_1\;c\;u_1 \succ_{r_1} mkeps\;r_1 |
|
337 \] |
|
338 |
|
339 |
|
340 \subsubsection*{Case RL} |
|
341 |
|
342 The corresponding rule (instantiated) is: |
|
343 |
|
344 \begin{center} |
|
345 \begin{tabular}{c} |
|
346 $len\,|w_1| > len\,|w_2|$\\ |
|
347 \hline |
|
348 $Right(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Left(w_2)$ |
|
349 \end{tabular} |
|
350 \end{center} |
|
351 |
|
352 \subsection*{Test Proof} |
|
353 |
|
354 We want to prove that |
|
355 |
|
356 \[ |
|
357 nullable(r) \;\text{implies}\; POSIX (mkeps\; r)\; r |
|
358 \] |
|
359 |
|
360 \noindent |
|
361 We prove this by induction on $r$. There are 5 subcases, and |
|
362 only the $r_1 + r_2$-case is interesting. In this case we know the |
|
363 induction hypotheses are |
|
364 |
|
365 \begin{center} |
|
366 \begin{tabular}{ll} |
|
367 (IMP1) & $nullable(r_1) \;\text{implies}\; |
|
368 POSIX (mkeps\; r_1)\; r_1$ \\ |
|
369 (IMP2) & $nullable(r_2) \;\text{implies}\; |
|
370 POSIX (mkeps\; r_2)\; r_2$ |
|
371 \end{tabular} |
|
372 \end{center} |
|
373 |
|
374 \noindent and know that $nullable(r_1 + r_2)$ holds. From this |
|
375 we know that either $nullable(r_1)$ holds or $nullable(r_2)$. |
|
376 Let us consider the first case where we know $nullable(r_1)$. |
|
377 |
|
378 |
|
379 \subsection*{Problems in the paper proof} |
|
380 |
|
381 I cannot verify\ldots |
|
382 |
|
383 |
|
384 |
|
385 \newpage |
|
386 \section*{Isabelle Cheat-Sheet} |
|
387 |
|
388 \begin{itemize} |
|
389 \item The main notion in Isabelle is a \emph{theorem}. |
|
390 Definitions, inductive predicates and recursive |
|
391 functions all have underlying theorems. If a definition |
|
392 is called \texttt{foo}, then the theorem will be called |
|
393 \texttt{foo\_def}. Take a recursive function, say |
|
394 \texttt{bar}, it will have a theorem that is called |
|
395 \texttt{bar.simps} and will be added to the simplifier. |
|
396 That means the simplifier will automatically |
|
397 Inductive predicates called \texttt{baz} will be called |
|
398 \texttt{baz.intros}. For inductive predicates, there are |
|
399 also theorems \texttt{baz.induct} and |
|
400 \texttt{baz.cases}. |
|
401 |
|
402 \item A \emph{goal-state} consists of one or more subgoals. If |
|
403 there are \texttt{No more subgoals!} then the theorem is |
|
404 proved. Each subgoal is of the form |
|
405 |
|
406 \[ |
|
407 \llbracket \ldots{}premises\ldots \rrbracket \Longrightarrow |
|
408 conclusion |
|
409 \] |
|
410 |
|
411 \noindent |
|
412 where $premises$ and $conclusion$ are formulas of type |
|
413 \texttt{bool}. |
|
414 |
|
415 \item There are three low-level methods for applying one or |
|
416 more theorem to a subgoal, called \texttt{rule}, |
|
417 \texttt{drule} and \texttt{erule}. The first applies a |
|
418 theorem to a conclusion of a goal. For example |
|
419 |
|
420 \[\texttt{apply}(\texttt{rule}\;thm) |
|
421 \] |
|
422 |
|
423 If the conclusion is of the form $\_ \wedge \_$, |
|
424 $\_ \longrightarrow \_$ and $\forall\,x. \_$ the |
|
425 $thm$ is called |
|
426 |
|
427 \begin{center} |
|
428 \begin{tabular}{lcl} |
|
429 $\_ \wedge \_$ & $\Rightarrow$ & $conjI$\\ |
|
430 $\_ \longrightarrow \_$ & $\Rightarrow$ & $impI$\\ |
|
431 $\forall\,x.\_$ & $\Rightarrow$ & $allI$ |
|
432 \end{tabular} |
|
433 \end{center} |
|
434 |
|
435 Many of such rule are called intro-rules and end with |
|
436 an ``$I$'', or in case of inductive predicates $\_.intros$. |
|
437 |
|
438 |
|
439 \end{itemize} |
|
440 |
|
441 |
|
442 \end{document} |
|