diff --git a/LaTeX/lfmt.tex b/LaTeX/lfmt.tex index 0f952a83f36d6d0da316fe9d86e13bb3c31f239a..c4348fe71e4f92710724ca67e29762c94859e204 100644 --- a/LaTeX/lfmt.tex +++ b/LaTeX/lfmt.tex @@ -51,7 +51,7 @@ Note: $$\mathcal{T}_{\mathcal{\emptyset}}$$ is the set of closed terms. \end{align*} \end{definition} -\begin{definition} +\begin{definition}\label{def:convbg} We define $$\convbg$$ as the reflexive, symmetric, transitive closure of $$\beta$$ and $$\bigcup_{\mathcal{R} \in \Gamma} \mathcal{R}$$ and closed by context. \end{definition} @@ -102,7 +102,7 @@ Note: $$\mathcal{T}_{\mathcal{\emptyset}}$$ is the set of closed terms. } {\Gamma \vdash \tpi{x}{A}{B} : s} \and - \inferrule*{ + \inferrule*[Right=lambda]{ \Gamma \vdash A : \ttype \\ \Gamma, x : A \vdash B : s @@ -111,7 +111,7 @@ Note: $$\mathcal{T}_{\mathcal{\emptyset}}$$ is the set of closed terms. } {\Gamma \vdash \tabs{x}{A}{t} : \tpi{x}{A}{B}} \and - \inferrule*{ + \inferrule*[Right=app]{ \Gamma \vdash t : \tpi{x}{A}{B} \\ \Gamma \vdash u : A @@ -136,6 +136,29 @@ Note: $$\mathcal{T}_{\mathcal{\emptyset}}$$ is the set of closed terms. By induction on the derivation of $$\Gamma \vdash \tkind : A$$. The only rule that can be applied is \textsc{conv}. We conclude this case by applying the induction hypothesis on the first premise. \end{proof} +\begin{lemma} + For any context $\Gamma$ and terms $t$ and $A$ such that $\Gamma \vdash t : A$, there exists $t'$ such that $t \convbg t'$ and $\tkind$ is not a subterm of $t'$. +\end{lemma} +\begin{proof} + By induction on 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: + \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 Proove that adding a variable to the context doesn't enrich $\conv$.\\ + i.e. $\conv_{\beta\Gamma} \ = \ \conv_{\beta\Gamma, x : A}$. + \end{itemize} + \end{itemize} +\end{proof} + \begin{lemma} For any context $$\Gamma$$, if $$\tkind \convbg t$$ then $$t = \tkind$$.