From 96cbc9021502352503d1ed7f72a247fc3641cf49 Mon Sep 17 00:00:00 2001
From: Gaspard Ferey
Date: Tue, 24 Apr 2018 13:38:10 +0200
Subject: [PATCH] Fixed lemma 2.
---
LaTeX/lfmt.tex | 22 ++++++++--------------
1 file changed, 8 insertions(+), 14 deletions(-)
diff --git a/LaTeX/lfmt.tex b/LaTeX/lfmt.tex
index 2593e84..1babb62 100644
--- a/LaTeX/lfmt.tex
+++ b/LaTeX/lfmt.tex
@@ -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}
--
2.24.1