Commit 231eb3f9 authored by François Thiré's avatar François Thiré

Fix The Rel Rule

parent a195aa7d
......@@ -57,7 +57,7 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\begin{rules}{typing}{Typing rules}
\inferrule*{ }
{\wf{\emptyset}}
{\wf{[]}}
\and
\inferrule*{
\wf{\Gamma}
......@@ -76,7 +76,7 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
{\wf{\Gamma, \mathcal{R}}}
\and
\inferrule*[Right=Rel]{
\Gamma \vdash A : \ttype
\Gamma \vdash A : s
\\
\Gamma \vdash t : A
\\
......@@ -118,7 +118,7 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
}
{\Gamma \vdash t~u : \subst{B}{x}{u}}
\and
\inferrule*{
\inferrule*[Right=conv]{
\Gamma \vdash t : A
\\
\Gamma \vdash B : s
......@@ -129,12 +129,28 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\end{rules}
\begin{lemma}
There is no context \(\Gamma\) and term \(A\) such that \(\Gamma \vdash \tkind : A\) is derivable.
\end{lemma}
\begin{proof}
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\), if \(\tkind \convbg t\) then \(t = \tkind\).
\end{lemma}
\begin{proof}
By induction on the length of \(\Gamma\), we can prove that there is no \(u\) such that \(\Gamma \vdash \wf{(\tkind,u)}\) or the symmetrical case are derivable. From this, we can conclude the statement.
\todo{Peut-on le prouver sans induction ?}
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}
......
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