Commit fdb4d4f0 authored by Gaspard Ferey's avatar Gaspard Ferey

Petit lemme intermédiaire.

parent 50bcc3d0
......@@ -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\).
......
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