Commit 96cbc902 authored by Gaspard Ferey's avatar Gaspard Ferey

Fixed lemma 2.

parent ccb3ba8f
......@@ -137,25 +137,19 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\end{proof}
\begin{lemma}
For any well-formed context\, $\Gamma$, term $t$, term $A$ such that $\Gamma \vdash t : A$, there exists $t'$ such that $t \convbg t'$ and $\tkind$ is not a subterm of $t'$.
Let $t$ be a term. If $t$ is typable in a well-formed context then $\tkind$ is not a subterm of $t$. The contrapositive states that if $\tkind$ is a subterm of $t$ then $t$ isn't typable in any well-formed context.
\end{lemma}
\begin{proof}
By induction on the derivation of $\Gamma \vdash t : A$.
By induction on the height of the derivation of $\Gamma \vdash t : A$.
If $\tkind$ is already not a subterm of $t$ we are done. \\
Otherwise $t$ is neither a variable nor $\ttype$ so only three rules can be applied:
If $t$ is a variable or $\ttype$ then we are done.
Otherwise:
\begin{itemize}
\item \textsc{conv} :
The induction hypothesis on the first premise gives us a suitable $t'$ such that $t \convbg t'$.
\item \textsc{app} : $t = u~v$ and $\tkind$ can be a subterm of $u$ or $u$.
The induction hypothesis on the first and second premises gives us $u'$ and $v'$ containing no subterm $\tkind$ and such that $u \convbg u'$ and $v \convbg v'$. It follows from Definition~\ref{def:convbg} that $t = u~v \convbg u'~v' = t'$ with $\tkind$ not a subterm of $t'$.
\item \textsc{lambda} : $t = \tabs{x}{A}{u}$ and $\tkind$ can be a subterm of $A$ and $u$.
The induction hypothesis on the first premise gives us a $\tkind$-free $A'$ such that $A' \convbg A$. Two solutions to conclude for $u$ :
\begin{itemize}
\item Consider that the induction on the height of the derivation is "forall context $\Gamma$".
\item Prove that adding a variable to the context doesn't enrich $\conv$.\\
i.e. $\conv_{\beta\Gamma} \ = \ \conv_{\beta\Gamma, x : A}$.
\end{itemize}
By induction hypothesis on the first premise, $\tkind$ is not a subterm of $t$.
\item \textsc{app} : $t = u~v$ and by induction hypothesis on the first and second premises, $\tkind$ is neither a subterm of $u$ nor a subterm of $v$ so it can't be a subterm of $t$ either.
\item \textsc{lambda} : $t = \tabs{x}{A}{u}$ and by induction hypothesis
on the first and third premises, $\tkind$ is neither a subterm of $A$ nor a subterm of $u$ so it can't be a subterm of $t$ either.
\end{itemize}
\end{proof}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment