Commit 6f0828e8 authored by Gaspard Ferey's avatar Gaspard Ferey

Removed useless lemmas. Added rules for relations.

parent 4d32871d
......@@ -27,108 +27,110 @@
\label{fig:sttsyntax}
\end{figure}
\begin{definition}
Let \(\mathcal{X}\) be a countable set of variables.
\end{definition}
\begin{definition}
We denote \(\mathcal{T}_{\mathcal{X}}\) the free algebra over the terms with variables in \(\mathcal{X}\).
\end{definition}
Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\begin{definition}
We define \(\mathfrak{R}_{\mathcal{X}}\) the set of pairs of terms:
\[\mathfrak{R}_{\mathcal{X}} \defn \{(t,u) \mid t,u \in \mathcal{T}_{\mathcal{X}}\} \]
\end{definition}
\begin{definition}
We denote \(Dom(\Gamma)\) the domain of \(\Gamma\) defines as:
\begin{align*}
Dom(\emptyset) &\defn \emptyset \\
Dom(\Gamma , \mathcal{R}) &\defn Dom(\Gamma) \\
Dom(\Gamma , x : A) &\defn Dom(\Gamma) \cup \{x\}
\end{align*}
\end{definition}
%\begin{definition}
% Let \(\mathcal{X}\) be a countable set of variables.
%\end{definition}
%
%\begin{definition}
% We denote \(\mathcal{T}_{\mathcal{X}}\) the free algebra over the terms with variables in \(\mathcal{X}\).
%\end{definition}
%
%Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
%
%\begin{definition}
% We define \(\mathfrak{R}_{\mathcal{X}}\) the set of pairs of terms:
% \[\mathfrak{R}_{\mathcal{X}} \defn \{(t,u) \mid t,u \in \mathcal{T}_{\mathcal{X}}\} \]
%\end{definition}
%
%\begin{definition}
% We denote \(Dom(\Gamma)\) the domain of \(\Gamma\) defines as:
% \begin{align*}
% Dom(\emptyset) &\defn \emptyset \\
% Dom(\Gamma , \mathcal{R}) &\defn Dom(\Gamma) \\
% Dom(\Gamma , x : A) &\defn Dom(\Gamma) \cup \{x\}
% \end{align*}
%\end{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}
\begin{rules}{typing}{Typing rules}
\inferrule*{ }
\begin{rules}{Typing rules}{Typing rules}
\inferrule*[right=empty]{ }
{\wf{[]}}
\and
\inferrule*{
\wf{\Gamma}
\\
{\Gamma \vdash A : \ttype}
\and \inferrule*[right=var-decl]
{
\Gamma \vdash A : s \\
x \notin \Gamma
}
{\wf{\Gamma, x:A}}
\and
\inferrule*{
\wf{\Gamma}
\\
{\mathcal{R} \in \mathfrak{R}_{Dom(\Gamma)}}
\\
{\Gamma \vdash \wf{\mathcal{R}}}
}
\and \inferrule*[right=rule-decl]
{\Gamma \vdash \wf{\mathcal{R}}}
{\wf{\Gamma, \mathcal{R}}}
\and
\inferrule*[right=Rel]{
\Gamma \vdash A : s
\\
\Gamma \vdash t : A
\\
\and \inferrule*[right=Rel]
{
\Gamma \vdash A : s \\
\Gamma \vdash t : A \\
\Gamma \vdash u : A
}
{\Gamma \vdash \wf{\mathcal{R} = (t,u)}}
\and
\inferrule*{
\wf{\Gamma}
\\
\and \inferrule*[right=axiom]
{
\wf{\Gamma} \\
x : A \in \Gamma
}
{\Gamma \vdash x : A}
\and
\inferrule*{
}
\and \inferrule*[right=sort]
{\wf{\Gamma}}
{\Gamma \vdash \ttype : \tkind}
\and
\inferrule*{
\Gamma \vdash A : \ttype
\\
\and \inferrule*[right=product]
{
\Gamma \vdash A : \ttype \\
\Gamma, x : A \vdash B : s
}
{\Gamma \vdash \tpi{x}{A}{B} : s}
\and
\inferrule*[right=lambda]{
\Gamma \vdash A : \ttype
\\
\Gamma, x : A \vdash B : s
\\
\and \inferrule*[right=lambda]
{
\Gamma \vdash A : \ttype \\
\Gamma, x : A \vdash B : s \\
\Gamma, x : A \vdash t : B
}
{\Gamma \vdash \tabs{x}{A}{t} : \tpi{x}{A}{B}}
\and
\inferrule*[right=app]{
\Gamma \vdash t : \tpi{x}{A}{B}
\\
\and \inferrule*[right=app]
{
\Gamma \vdash t : \tpi{x}{A}{B} \\
\Gamma \vdash u : A
}
{\Gamma \vdash t~u : \subst{B}{x}{u}}
\and
\inferrule*[right=conv]{
\Gamma \vdash t : A
\\
\Gamma \vdash B : s
\\
\and \inferrule*[right=conv]
{
\Gamma \vdash t : A \\
\Gamma \vdash B : s \\
A \convbg B
}
{\Gamma \vdash t: B}
\end{rules}
\begin{lemma}
Whenever $\Gamma \vdash t : A$ is derivable, $\wf{\Gamma}$ is also derivable.
\end{lemma}
\begin{proof}
By induction on the derivation of $\Gamma \vdash t : A$.\\
\textsc{axiom} and \textsc{sort} are base cases yielding the result from their first premise.\\
We conclude in the other cases: \textsc{product}, \textsc{lambda}, \textsc{app} and \textsc{conv}, by induction on the first premise.
\end{proof}
\begin{lemma}
There is no context \(\Gamma\) and term \(A\) such that \(\Gamma \vdash \tkind : A\) is derivable.
\end{lemma}
......@@ -218,4 +220,60 @@ The subjection conversion property is a generalization of a subject reduction in
\begin{proof}
\todo{PROOF}
\end{proof}
\begin{rules}{Relation rules}{Relation rules}
\inferrule*{
}
{\Gamma \vdash A \equiv A}
\and \inferrule*
{\Gamma \vdash B \equiv A}
{\Gamma \vdash A \equiv B}
\and \inferrule*
{\Gamma \vdash A \equiv B \\
\Gamma \vdash B \equiv C
}
{\Gamma \vdash A \equiv C}
\and \inferrule*[right=beta]{
}
{\Gamma \vdash (\tabs{x}{A}{t})~u \equiv \subst{t}{x}{u} }
\and \inferrule*[right=gamma]
{ (t,u) \in \Gamma }
{\Gamma \vdash t \equiv u }
\and \inferrule*
{\Gamma \vdash A \equiv A' \\
\Gamma \vdash t \equiv t'
}
{\Gamma \vdash \tabs{x}{A}{t} \equiv \tabs{x}{A'}{t'} }
\and \inferrule*
{\Gamma \vdash A \equiv A' \\
\Gamma \vdash t \equiv t'
}
{\Gamma \vdash \tpi{x}{A}{t} \equiv \tpi{x}{A'}{t'} }
\and \inferrule*
{\Gamma \vdash t \equiv t' \\
\Gamma \vdash u \equiv u'
}
{\Gamma \vdash t~u \equiv t'~u' }
\and \inferrule*
{\Gamma \vdash A \equiv B}
{A \convbg B}
\end{rules}
\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