1 \documentclass[11pt]{article} |
1 \documentclass[11pt]{article} |
2 \usepackage[left]{lineno} |
2 \usepackage[left]{lineno} |
|
3 \usepackage{amsmath} |
3 |
4 |
4 \begin{document} |
5 \begin{document} |
5 \linenumbers |
6 %%\linenumbers |
6 |
7 |
7 \noindent |
8 \noindent |
8 A lemma which might be true, but can also be false, is as follows: |
9 We already proved that |
|
10 |
|
11 \[ |
|
12 \text{If}\;nullable(r)\;\text{then}\;POSIX\;(mkeps\; r)\;r |
|
13 \] |
|
14 |
|
15 \noindent |
|
16 holds. This is essentially the ``base case'' for the |
|
17 correctness proof of the algorithm. For the ``induction |
|
18 case'' we need the following main theorem, which we are |
|
19 currently after: |
|
20 |
|
21 \begin{center} |
|
22 \begin{tabular}{lll} |
|
23 If & (*) & $POSIX\;v\;(der\;c\;r)$ and $\vdash v : der\;c\;r$\\ |
|
24 then & & $POSIX\;(inj\;r\;c\;v)\;r$ |
|
25 \end{tabular} |
|
26 \end{center} |
|
27 |
|
28 \noindent |
|
29 That means a POSIX value $v$ is still $POSIX$ after injection. |
|
30 I am not sure whether this theorem is actually true in this |
|
31 full generality. Maybe it requires some restrictions. |
|
32 |
|
33 If we unfold the $POSIX$ definition in the then-part, we |
|
34 arrive at |
|
35 |
|
36 \[ |
|
37 \forall v'.\; |
|
38 \text{if}\;\vdash v' : r\; \text{and} \;|inj\;r\;c\;v| = |v'|\; |
|
39 \text{then}\; |inj\;r\;c\;v| \succ_r v' |
|
40 \] |
|
41 |
|
42 \noindent |
|
43 which is what we need to prove assuming the if-part (*) in the |
|
44 theorem above. Since this is a universally quantified formula, |
|
45 we just need to fix a $v'$. We can then prove the implication |
|
46 by assuming |
|
47 |
|
48 \[ |
|
49 \text{(a)}\;\;\vdash v' : r\;\; \text{and} \;\; |
|
50 \text{(b)}\;\;inj\;r\;c\;v = |v'| |
|
51 \] |
|
52 |
|
53 \noindent |
|
54 and our goal is |
|
55 |
|
56 \[ |
|
57 (goal)\;\;inj\;r\;c\;v \succ_r v' |
|
58 \] |
|
59 |
|
60 \noindent |
|
61 There are already two lemmas proved that can transform |
|
62 the assumptions (a) and (b) into |
|
63 |
|
64 \[ |
|
65 \text{(a*)}\;\;\vdash proj\;r\;c\;v' : der\;c\;r\;\; \text{and} \;\; |
|
66 \text{(b*)}\;\;c\,\#\,|v| = |v'| |
|
67 \] |
|
68 |
|
69 \noindent |
|
70 Another lemma shows that |
|
71 |
|
72 \[ |
|
73 |v'| = c\,\#\,|proj\;r\;c\;v| |
|
74 \] |
|
75 |
|
76 \noindent |
|
77 Using (b*) we can therefore infer |
|
78 |
|
79 \[ |
|
80 \text{(b**)}\;\;|v| = |proj\;r\;c\;v| |
|
81 \] |
|
82 |
|
83 \noindent |
|
84 The main idea of the proof is now a simple instantiation |
|
85 of the assumption $POSIX\;v\;(der\;c\;r)$. If we unfold |
|
86 the $POSIX$ definition, we get |
|
87 |
|
88 \[ |
|
89 \forall v'.\; |
|
90 \text{if}\;\vdash v' : der\;c\;r\; \text{and} \;|v| = |v'|\; |
|
91 \text{then}\; v \succ_{der\;c\;r}\; v' |
|
92 \] |
|
93 |
|
94 \noindent |
|
95 We can instantiate this $v'$ with $proj\;r\;c\;v'$ and can use |
|
96 (a*) and (b**) in order to infer |
|
97 |
|
98 \[ |
|
99 v \succ_{der\;c\;r}\; proj\;r\;c\;v' |
|
100 \] |
|
101 |
|
102 \noindent |
|
103 The point of the side-lemma below is that we can ``add'' an |
|
104 $inj$ to both sides to obtain |
|
105 |
|
106 \[ |
|
107 inj\;r\;c\;v \succ_r\; inj\;r\;c\;(proj\;r\;c\;v') |
|
108 \] |
|
109 |
|
110 \noindent Finally there is already a lemma proved that shows |
|
111 that an injection and projection is the identity, meaning |
|
112 |
|
113 \[ |
|
114 inj\;r\;c\;(proj\;r\;c\;v') = v' |
|
115 \] |
|
116 |
|
117 \noindent |
|
118 With this we have shown our goal (pending a proof of the side-lemma |
|
119 next). |
|
120 |
|
121 |
|
122 \subsection*{Side-Lemma} |
|
123 |
|
124 A side-lemma needed for the theorem above which might be true, but can also be false, is as follows: |
9 |
125 |
10 \begin{center} |
126 \begin{center} |
11 \begin{tabular}{lll} |
127 \begin{tabular}{lll} |
12 If & (1) & $v_1 \succ_{der\;c\;r} v_2$,\\ |
128 If & (1) & $v_1 \succ_{der\;c\;r} v_2$,\\ |
13 & (2) & $\vdash v_1 : der\;c\;r$, and\\ |
129 & (2) & $\vdash v_1 : der\;c\;r$, and\\ |