Commit 6d990ebd authored by François Thiré's avatar François Thiré

clarify last commit

parent b28e6140
......@@ -110,7 +110,7 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\Gamma, x : A \vdash t : B
}
{\Gamma \vdash \tabs{x}{A}{t} : \tpi{x}{A}{B}}
\and
\and
\inferrule*[right=app]{
\Gamma \vdash t : \tpi{x}{A}{B}
\\
......@@ -137,7 +137,7 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\end{proof}
\begin{lemma}
For any well-formed 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'$.
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'$.
\end{lemma}
\begin{proof}
By induction on the derivation of $\Gamma \vdash t : A$.
......@@ -162,81 +162,67 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\begin{definition}[subject conversion]
A well-formed context $\Gamma$ satisfies the \emph{subject conversion} property
when for all terms $t_1, t_2, T_1, T_2$ such that
$t_1 \convbg t_2$, $\Gamma \vdash t_1 : T_1$ and $\Gamma \vdash t_2 : T_2$,
then $T_1 \convbg T_2$.
when for all terms $t_1, t_2, A, B$ such that
$t_1 \convbg t_2$, $\Gamma \vdash t_1 : A$ and $\Gamma \vdash t_2 : B$,
then $A \convbg B$.
\end{definition}
Remark: when $A$ (resp. $B$) is typable with a sort, $\Gamma \vdash A :s$ (resp. $\Gamma \vdash B :s$), then it follows from $A \convbg B$ that $\Gamma \vdash t_2 : A$ (resp. $\Gamma \vdash t_1 : B$).
The subjection conversion property is a generalization of a subject reduction in a context where the \emph{computation} is not oriented but it is also weaker as we will see below:
\begin{definition}[subject reduction]
A well-formed context $\Gamma$ satisfies the \emph{subject reduction} property
when for all terms $t_1, t_2, A$ such that
$t_1 \hookrightarrow t_2$, $\Gamma \vdash t_1 : A$ then $\Gamma \vdash t_2 : A$.
\end{definition}
Remark: when $T_1$ (resp. $T_2$) is typable with a sort, $\Gamma \vdash T_1 :s$ (resp. $\Gamma \vdash T_2 :s$), then it follows from $T_1 \convbg T_2$ that $\Gamma \vdash t_2 : T_1$ (resp. $\Gamma \vdash t_2 : T_1$).
\begin{definition}[typability preservation]
A well-formed context $\Gamma$ satisfies the \emph{typability preservation} property
when for all terms $t_1, t_2, A$ such that
$t_1 \hookrightarrow t_2$, $\Gamma \vdash t_1 : A$ then $\exists B, \Gamma \vdash t_2 : B$.
\end{definition}
\begin{lemma}
When the relation system is oriented (a rewriting system) then
\emph{subject conversion} and \emph{typability preservation} together
imply the \emph{subject reduction} property.
\end{lemma}
\begin{proof}
$\Gamma$ verify the \emph{subject reduction} property when
$$
\forall t_1, t_2, T, \quad
\left\{
\begin{aligned}
& t_1 \longrightarrow^{\Gamma} t_2 \\
& \Gamma \vdash t_1 : T
\end{aligned}
\right.
\quad \Longrightarrow \quad
\Gamma \vdash t_2 : T
$$
$\Gamma$ verify the \emph{typability preservation} property when
$$
\forall t_1, t_2, T_1, \quad
\left\{
\begin{aligned}
& t_1 \longrightarrow^{\Gamma} t_2 \\
& \Gamma \vdash t_1 : T_1
\end{aligned}
\right.
\quad \Longrightarrow \quad
\exists T_2, \ \Gamma \vdash t_2 : T_2
$$
$\Gamma$ verify the \emph{subject conversion} property when
$$
\forall t_1, t_2, T_1, T_2 \quad
\left\{
\begin{aligned}
& t_1 \convbg t_2 \\
& \Gamma \vdash t_1 : T_1 \\
& \Gamma \vdash t_2 : T_2
\end{aligned}
\right.
\quad \Longrightarrow \quad
T_1 \convbg T_2
$$
\end{proof}
\begin{lemma}[False]
For any well-formed context \(\Gamma\), and term $t$ such that \(\tkind \convbg t\) then \(t = \tkind\).
\end{lemma}
\begin{proof}
By induction on the length of \(\Gamma\).
The idea, is to be able to use the \textsc{conv} rule to deduce this property.
We want to prove that \(\Gamma \vdash t_2 : A\) from the fact that \(t_1 \hookrightarrow t_2\) and \(\Gamma \vdash t_1 : A\).
We use the \emph{typability preservation} property to get a type \(B\) to \(t_2\). Then, from the \emph{subject conversion} property, we know that \(\Gamma \vdash A \convbg B\).
The only thing we need now to apply the \textsc{conv} rule is to show that \(\Gamma \vdash A : s\) for some sort \(s\). However, this is not possible in general, for example when \(A = \tkind\). We have two cases to prove:
\begin{itemize}
\item base case: \(\Gamma\) is \(\empty\) and the \(\beta\) rule cannot be applied
\item inductive case:
\begin{itemize}
\item \(\Gamma = \Gamma, x : A\), then the congruence relation is the same
\item \(\Gamma = \Gamma, (t,u)\), TODO
\end{itemize}
\item If \(A = kind\), then using Lemma TODO, we can show that \(B = kind\), hence subject reduction is satisfied
\item If \(A \neq kind\), because \(A\) is inhabited, we can use Lemma TODO to conclude that \(\Gamma \vdash A :s\). Hence we can apply the \textsc{conv}, this closes the proof.
\end{itemize}
we can prove that there is no \(u\) such that \(\Gamma \vdash \wf{(\tkind,u)}\) or the symmetrical case are derivable.
\end{proof}
\begin{lemma}
For any context \(\Gamma\), if \(\ttype \convbg t\) then \(t = \ttype\).
\end{lemma}
\begin{proof}
Same proof as the precedent lemma.
\end{proof}
% \begin{lemma}[False]
% For any well-formed context \(\Gamma\), and term $t$ such that \(\tkind \convbg t\) then \(t = \tkind\).
% \end{lemma}
% \begin{proof}
% By induction on the length of \(\Gamma\).
% \begin{itemize}
% \item base case: \(\Gamma\) is \(\empty\) and the \(\beta\) rule cannot be applied
% \item inductive case:
% \begin{itemize}
% \item \(\Gamma = \Gamma, x : A\), then the congruence relation is the same
% \item \(\Gamma = \Gamma, (t,u)\), TODO
% \end{itemize}
% \end{itemize}
% we can prove that there is no \(u\) such that \(\Gamma \vdash \wf{(\tkind,u)}\) or the symmetrical case are derivable.
% \end{proof}
% \begin{lemma}
% For any context \(\Gamma\), if \(\ttype \convbg t\) then \(t = \ttype\).
% \end{lemma}
% \begin{proof}
% Same proof as the precedent lemma.
% \end{proof}
\end{document}
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