\documentclass[11pt]{article}+
−
+
−
\begin{document}+
−
+
−
\noindent+
−
A lemma which might be true, but can also be false, is as follows:+
−
+
−
\begin{center}+
−
\begin{tabular}{lll}+
−
If   & (1) & $v_1 \succ_{der\;c\;r} v_2$,\\+
−
     & (2) & $\vdash v_1 : der\;c\;r$, and\\ +
−
     & (3) & $\vdash v_2 : der\;c\;r$ holds,\\+
−
then &     & $inj\;r\;c\;v_1 \succ_r inj\;r\;c\;v_2$ also holds.  +
−
\end{tabular}+
−
\end{center}+
−
+
−
\noindent It essentially states that if one value $v_1$ is +
−
bigger than $v_2$ then this ordering is preserved under +
−
injections. This is proved by induction (on the definition of +
−
$der$\ldots this is very similar to an induction on $r$).+
−
\bigskip+
−
+
−
\noindent+
−
The case that is still unproved is the sequence case where we +
−
assume $r = r_1\cdot r_2$ and also $r_1$ being nullable.+
−
The derivative $der\;c\;r$ is then+
−
+
−
\begin{center}+
−
$der\;c\;r = ((der\;c\;r_1) \cdot r_2) + (der\;c\;r_2)$+
−
\end{center}+
−
+
−
\noindent +
−
or without the parentheses+
−
+
−
\begin{center}+
−
$der\;c\;r = (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$+
−
\end{center}+
−
+
−
\noindent +
−
In this case the assumptions are+
−
+
−
\begin{center}+
−
\begin{tabular}{ll}+
−
(a) & $v_1 \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} v_2$\\+
−
(b) & $\vdash v_1 : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\+
−
(c) & $\vdash v_2 : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\+
−
(d) & $nullable(r_1)$+
−
\end{tabular}+
−
\end{center}+
−
+
−
\noindent +
−
The induction hypotheses are+
−
+
−
\begin{center}+
−
\begin{tabular}{ll}+
−
(IH1) & $\forall v_1 v_2.\;v_1 \succ_{der\;c\;r_1} v_2+
−
\;\wedge\; \vdash v_1 : der\;c\;r_1 \;\wedge\; +
−
\vdash v_2 : der\;c\;r_1\qquad$\\+
−
      & $\hfill\longrightarrow+
−
         inj\;r_1\;c\;v_1 \succ{r_1} \;inj\;r_1\;c\;v_2$\smallskip\\+
−
(IH2) & $\forall v_1 v_2.\;v_1 \succ_{der\;c\;r_2} v_2+
−
\;\wedge\; \vdash v_2 : der\;c\;r_2 \;\wedge\; +
−
\vdash v_2 : der\;c\;r_2\qquad$\\+
−
      & $\hfill\longrightarrow+
−
         inj\;r_2\;c\;v_1 \succ{r_2} \;inj\;r_2\;c\;v_2$\\+
−
\end{tabular}+
−
\end{center}+
−
+
−
\noindent +
−
The goal is+
−
+
−
\[+
−
(goal)\qquad+
−
inj\; (r_1 \cdot r_2)\;c\;v_1 \succ_{r_1 \cdot r_2} +
−
inj\; (r_1 \cdot r_2)\;c\;v_2+
−
\]+
−
+
−
\noindent +
−
If we analyse how (a) could have arisen (that is make a case+
−
distinction), then we will find four cases:+
−
+
−
\begin{center}+
−
\begin{tabular}{ll}+
−
LL & $v_1 = Left(w_1)$, $v_2 = Left(w_2)$\\+
−
LR & $v_1 = Left(w_1)$, $v_2 = Right(w_2)$\\+
−
RL & $v_1 = Right(w_1)$, $v_2 = Left(w_2)$\\+
−
RR & $v_1 = Right(w_1)$, $v_2 = Right(w_2)$\\+
−
\end{tabular}+
−
\end{center}+
−
+
−
+
−
\noindent +
−
We have to establish our goal in all four cases. +
−
+
−
+
−
\subsubsection*{Case LR}+
−
+
−
The corresponding rule (instantiated) is:+
−
+
−
\begin{center}+
−
\begin{tabular}{c}+
−
$len\,|w_1| \geq len\,|w_2|$\\+
−
\hline+
−
$Left(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Right(w_2)$+
−
\end{tabular}+
−
\end{center}+
−
+
−
\noindent +
−
This means we can also assume in this case+
−
+
−
\[+
−
(e)\quad len\,|w_1| \geq len\,|w_2|+
−
\] +
−
+
−
\noindent +
−
which is the premise of the rule above.+
−
Instantiating $v_1$ and $v_2$ in the assumptions (b) and (c)+
−
gives us+
−
+
−
\begin{center}+
−
\begin{tabular}{ll}+
−
(b*) & $\vdash Left(w_1) : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\+
−
(c*) & $\vdash Right(w_2) : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\+
−
\end{tabular}+
−
\end{center}+
−
+
−
\noindent Since these are assumptions, we can further analyse+
−
how they could have arisen according to the rules of $\vdash+
−
\_ : \_\,$. This gives us two new assumptions+
−
+
−
\begin{center}+
−
\begin{tabular}{ll}+
−
(b**) & $\vdash w_1 : (der\;c\;r_1) \cdot r_2$\\+
−
(c**) & $\vdash w_2 : der\;c\;r_2$\\+
−
\end{tabular}+
−
\end{center}+
−
+
−
\noindent +
−
Looking at (b**) we can further analyse how this+
−
judgement could have arisen. This tells us that $w_1$+
−
must have been a sequence, say $u_1\cdot u_2$, with+
−
+
−
\begin{center}+
−
\begin{tabular}{ll}+
−
(b***) & $\vdash u_1 : der\;c\;r_1$\\+
−
       & $\vdash u_2 : r_2$\\+
−
\end{tabular}+
−
\end{center}+
−
+
−
\noindent +
−
Instantiating the goal means we need to prove+
−
+
−
\[+
−
inj\; (r_1 \cdot r_2)\;c\;(Left(u_1\cdot u_2)) \succ_{r_1 \cdot r_2} +
−
inj\; (r_1 \cdot r_2)\;c\;(Right(w_2))+
−
\]+
−
+
−
\noindent +
−
We can simplify this according to the rules of $inj$:+
−
+
−
\[+
−
(inj\; r_1\;c\;u_1)\cdot u_2 \succ_{r_1 \cdot r_2} +
−
(mkeps\;r_1) \cdot (inj\; r_2\;c\;w_2)+
−
\]+
−
+
−
\noindent+
−
This is what we need to prove.+
−
+
−
+
−
\subsubsection*{Case RL}+
−
+
−
The corresponding rule (instantiated) is:+
−
+
−
\begin{center}+
−
\begin{tabular}{c}+
−
$len\,|w_1| > len\,|w_2|$\\+
−
\hline+
−
$Right(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Left(w_2)$+
−
\end{tabular}+
−
\end{center}+
−
+
−
+
−
\end{document}  +
−