Skip to content

GitLab

Commit 51aee842 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

change definition of intertype and update proofs accordingly

parent 26fbc9c0
Hide whitespace changes
Inline Side-by-side
language.tex
View file @ 51aee842
......@@ -644,7 +644,7 @@ We start by defining the algorithm for each single occurrence, that is for the d
\constr{\varpi.r}{\Gamma,e,t} & = & \bpr{\env {\Gamma,e,t} (\varpi)}\label{cinque}\\[\sk]
\constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\label{sei}\\[\sk]
\constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\label{sette}\\[.8mm]
\env {\Gamma,e,t} (\varpi) & = & \constr \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}\label{otto}
\env {\Gamma,e,t} (\varpi) & = & \tsrep {\constr \varpi {\Gamma,e,t} \tsand \tyof {\occ e \varpi} \Gamma}\label{otto}
\end{eqnarray}\vspace{-5mm}\\
All the functions above are defined if and only if the initial path
$\varpi$ is valid for $e$ (i.e., $\occ e{\varpi}$ is defined) and $e$
......
proofs.tex
View file @ 51aee842
......@@ -947,7 +947,7 @@
\constr{\varpi.r}{\Gamma,e,t} & = & \bpr{\env {\Gamma,e,t} (\varpi)}\\
\constr{\varpi.f}{\Gamma,e,t} & = & \pair{\env {\Gamma,e,t} (\varpi)}\Any\\
\constr{\varpi.s}{\Gamma,e,t} & = & \pair\Any{\env {\Gamma,e,t} (\varpi)}\\
\env {\Gamma,e,t} (\varpi) & = & \constr \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}
\env {\Gamma,e,t} (\varpi) & = & \tsrep {\constr \varpi {\Gamma,e,t} \tsand \tyof {\occ e \varpi} \Gamma}
\end{eqnarray}
\begin{align*}
......@@ -1053,11 +1053,11 @@
Now, let's prove the second property.
We perform a (nested) induction on $\varpi$.
Recall that $\env {\Gamma,e,t} (\varpi) = \constr \varpi {\Gamma,e,t} \land \tsrep {\tyof {\occ e \varpi} \Gamma}$.
We can easily derive $\pvdash \Gamma e t \varpi : \tsrep {\tyof {\occ e \varpi} \Gamma}$ by using the outer induction hypothesis
(by definition of $\tsrep {\_}$ we have $\forall \ts.\ \ts \leq \tsrep \ts$).
Recall that $\env {\Gamma,e,t} (\varpi) = \tsrep {\constr \varpi {\Gamma,e,t} \tsand \tyof {\occ e \varpi} \Gamma}$.
For any $t'$ such that $\tyof {\occ e \varpi} \Gamma \leq t'$, we can easily derive $\pvdash \Gamma e t \varpi : t'$ by using the outer induction hypothesis
(the first property that we have proved above) and the rule \Rule{PTypeof}.
We also have to derive $\pvdash \Gamma e t \varpi : \constr \varpi {\Gamma,e,t}$ (then it will be easy to conclude using the rule \Rule{PInter}).
Now we have to derive $\pvdash \Gamma e t \varpi : \constr \varpi {\Gamma,e,t}$ (then it will be easy to conclude using the rule \Rule{PInter}).
\begin{description}
\item[$\varpi=\epsilon$] We use the rule \Rule{PEps}.
\item[$\varpi=\varpi'.1$]
......@@ -1174,6 +1174,7 @@
\begin{lemma}
\begin{align*}
&\forall t,\ts.\ \tsrep{t\tsand\ts} \leq t \land \tsrep{\ts}\\
&\forall t,\ts.\ t\tsand\ts \not\simeq \Empty \Rightarrow \tsrep{t\tsand\ts} \simeq t \land \tsrep{\ts}\\
&\forall \ts_1,\ts_2.\ \tsrep{\apply {\ts_1}{\ts_2}} \leq \apply {\tsrep {\ts_1}}{\tsrep {\ts_2}}
\end{align*}
\end{lemma}
......@@ -1226,7 +1227,7 @@
we have $\tyof e {\Gamma'} \leq \tyof e {\Gamma'\setminus \{e\}} \leq \tyof e {\Gamma}$ by induction hypothesis.
Thus, let's suppose that $e\not\in\dom\Gamma$ and $e\not\in\dom{\Gamma'}$.
From now we know that the last rule in $\tyof e {\Gamma}$ and $\tyof e {\Gamma'}$ is the same.
From now we know that the last rule in the derivation of $\tyof e {\Gamma}$ and $\tyof e {\Gamma'}$ (if any) is the same.
\begin{description}
\item[$e=c$] The last rule is \Rule{Const\Aa}. It does not depend on $\Gamma$ so this case is trivial.
......@@ -1274,8 +1275,19 @@
Now, let's prove the second property.
We perform a (nested) induction on $\varpi$.
We know that $\tsrep{\tyof {\occ e \varpi} {\Gamma'}} \leq \tsrep{\tyof {\occ e \varpi} {\Gamma}}$
by the outer induction hypothesis (for $\varpi=\epsilon$ we use the proof of the first property above).
Recall that we have $\forall t,\ts.\ t\tsand\ts \not\simeq \Empty \Rightarrow \tsrep{t\tsand\ts} \simeq t \land \tsrep{\ts}$.
Thus, in order to prove
$\tsrep {\constr {\varpi} {\Gamma',e,t} \tsand \tyof {\occ e \varpi} {\Gamma'}} \leq \tsrep {\constr {\varpi} {\Gamma,e,t} \tsand \tyof {\occ e \varpi} {\Gamma}}$,
we can prove the following:
\begin{align*}
&\constr {\varpi} {\Gamma',e,t} \leq \constr {\varpi} {\Gamma,e,t}\\
&\tyof {\occ e \varpi} {\Gamma'} \leq \tyof {\occ e \varpi} {\Gamma}\\
&\tsrep{\tyof {\occ e \varpi} {\Gamma'}} \leq \tsrep{\tyof {\occ e \varpi} {\Gamma}}
\end{align*}
The two last inequalities can be proved
with the outer induction hypothesis (for $\varpi=\epsilon$ we use the proof of the first property above).
Thus we just have to prove that $\constr {\varpi} {\Gamma',e,t} \leq \constr {\varpi} {\Gamma,e,t}$.
The only case that is interesting is the case $\varpi=\varpi'.1$.
......@@ -1354,9 +1366,9 @@
\item[\Rule{Inter}] By using the induction hypothesis we get $\tsrep{\tyof e \Gamma} \leq t_1$ and $\tsrep{\tyof e \Gamma} \leq t_2$.
Thus, we have $\tsrep{\tyof e \Gamma} \leq t_1 \land t_2$.
\item[\Rule{Subs}] Trivial using the induction hypothesis.
\item[\Rule{Const}] We know that the derivation of $\tyof e \Gamma$ ends with the rule \Rule{Const\Aa}.
\item[\Rule{Const}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Const\Aa}.
Thus this case is trivial.
\item[\Rule{App}] We know that the derivation of $\tyof e \Gamma$ ends with the rule \Rule{App\Aa}.
\item[\Rule{App}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{App\Aa}.
Let $\ts_1 = \tyof {e_1} \Gamma$ and $\ts_2 = \tyof {e_2} \Gamma$.
With the induction hypothesis we have $\tsrep {\ts_1} \leq \arrow {t_1} {t_2}$ and $\tsrep {\ts_2} \leq t_1$, with $t_2=t$.
According to the descriptive definition of $\apply{}{}$, we have
......@@ -1364,14 +1376,14 @@
As we also have $\tsrep{\apply {\ts_1} {\ts_2}} \leq \apply{\tsrep {\ts_1}}{\tsrep {\ts_2}}$,
we can conclude that $\tyof e \Gamma \leq t_2=t$.
\item[\Rule{Abs+}] We know that the derivation of $\tyof e \Gamma$ ends with the rule \Rule{Abs\Aa}.
\item[\Rule{Abs+}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Abs\Aa}.
This case is straightforward using the induction hypothesis.
\item[\Rule{Abs-}] This case is impossible (the derivation is positive).
\item[\Rule{Case}] We know that the derivation of $\tyof e \Gamma$ ends with the rule \Rule{Case\Aa}.
\item[\Rule{Case}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Case\Aa}.
By using the induction hypothesis and the monotonicity lemma, we get $\tsrep{\ts_1}\leq t$ and $\tsrep{\ts_2}\leq t$.
So we have $\tsrep{\ts_1\tsor\ts_2}=\tsrep{\ts1}\vee\tsrep{\ts2}\leq t$.
\item[\Rule{Proj}] Quite similar to the case \Rule{App}.
\item[\Rule{Pair}] We know that the derivation of $\tyof e \Gamma$ ends with the rule \Rule{Pair\Aa}.
\item[\Rule{Pair}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Pair\Aa}.
We just use the induction hypothesis and the fact that $\tsrep{\ts_1\tstimes\ts_2}=\pair {\tsrep{\ts1}} {\tsrep{\ts2}}$.
\end{description}
......@@ -1391,10 +1403,15 @@
\begin{description}
\item[\Rule{PSubs}] Trivial using the induction hypothesis.
\item[\Rule{PInter}] By using the induction hypothesis we get
$\env {\Gamma_1'',e,t} (\varpi) \leq t_1$ and $\env {\Gamma_2'',e,t} (\varpi) \leq t_2$
with $\RefineStep {e,t}^{n_1} (\Gamma_2) \leqA \Gamma_1''$ and
$\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''$. By taking $n'=\max (n_1,n_2)$,
\item[\Rule{PInter}] By using the induction hypothesis we get:
\begin{align*}
&\env {\Gamma_1'',e,t} (\varpi) \leq t_1\\
&\env {\Gamma_2'',e,t} (\varpi) \leq t_2\\
&\RefineStep {e,t}^{n_1} (\Gamma_2) \leqA \Gamma_1''\\
&\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''
\end{align*}
By taking $n'=\max (n_1,n_2)$,
we have $\RefineStep {e,t}^{n'} (\Gamma_2) \leqA \Gamma''$ with $\Gamma'' \leqA \Gamma_1''$ and $\Gamma'' \leqA \Gamma_2''$.
Thus, by using the monotonicity lemma, we can obtain $\env {\Gamma'',e,t} (\varpi) \leq t_1 \land t_2 = t'$.
\item[\Rule{PTypeof}] By using the outer induction hypothesis we get
......@@ -1403,10 +1420,14 @@
(by definition), thus we can conclude directly.
\item[\Rule{PEps}] Trivial.
\item[\Rule{PAppR}] By using the induction hypothesis we get
$\env {\Gamma_1'',e,t} (\varpi.0) \leq \arrow {t_1} {t_2}$ and $\env {\Gamma_2'',e,t} (\varpi) \leq t_2'$
with $\RefineStep {e,t}^{n_1} (\Gamma_2) \leqA \Gamma_1''$, $\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''$
and $t_2\land t_2' \simeq \Empty$.
\item[\Rule{PAppR}] By using the induction hypothesis we get:
\begin{align*}
&\env {\Gamma_1'',e,t} (\varpi.0) \leq \arrow {t_1} {t_2}\\
&\env {\Gamma_2'',e,t} (\varpi) \leq t_2'\\
& t_2\land t_2' \simeq \Empty\\
&\RefineStep {e,t}^{n_1} (\Gamma_2) \leqA \Gamma_1''\\
&\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''
\end{align*}
By taking $n'=\max (n_1,n_2) + 1$,
we have $\RefineStep {e,t}^{n'} (\Gamma_2) \leqA \Gamma''$ with $\Gamma'' \leqA \RefineStep {e,t} (\Gamma_1'')$
......@@ -1434,15 +1455,20 @@
It concludes this case.
\item[\Rule{PAppL}] By using the induction hypothesis we get
$\env {\Gamma_1'',e,t} (\varpi.1) \leq t_1$ and $\env {\Gamma_2'',e,t} (\varpi) \leq t_2$
with $\RefineStep {e,t}^{n_1} (\Gamma_2) \leqA \Gamma_1''$ and
$\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''$. By taking $n'=\max (n_1,n_2)$,
\item[\Rule{PAppL}] By using the induction hypothesis we get:
\begin{align*}
&\env {\Gamma_1'',e,t} (\varpi.1) \leq t_1\\
&\env {\Gamma_2'',e,t} (\varpi) \leq t_2\\
&\RefineStep {e,t}^{n_1} (\Gamma_2) \leqA \Gamma_1''\\
&\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''
\end{align*}
By taking $n'=\max (n_1,n_2)$,
we have $\RefineStep {e,t}^{n'} (\Gamma_2) \leqA \Gamma''$ with $\Gamma'' \leqA \Gamma_1''$ and $\Gamma'' \leqA \Gamma_2''$.
Thus, by using the monotonicity lemma, we can obtain $\env {\Gamma'',e,t} (\varpi.0) \leq \neg (\arrow {t_1} {\neg t_2}) = t'$.
\item[\Rule{PPairL}] Trivial using the induction hypothesis and the descriptive definition of $\bpi_1$.
\item[\Rule{PPairR}] Trivial using the induction hypothesis and the descriptive definition of $\bpi_2$.
\item[\Rule{PPairL}] Quite straightforward using the induction hypothesis and the descriptive definition of $\bpi_1$.
\item[\Rule{PPairR}] Quite straightforward using the induction hypothesis and the descriptive definition of $\bpi_2$.
\item[\Rule{PFst}] Trivial using the induction hypothesis.
\item[\Rule{PSnd}] Trivial using the induction hypothesis.
\end{description}
......@@ -1498,8 +1524,53 @@
the rule \Rule{Abs-} could possibly be used after a rule \Rule{Env} applied on $e$.
However, this case can easily be eliminated by changing the premise of this \Rule{Abs-} with another one
that does not use the rule \Rule{Env} on $e$ (the type of the premise does not matter for the rule \Rule{Abs-},
even $\Any$ suffices).
even $\Any$ suffices). Thus let's assume $e\not\in\dom\Gamma$.
Now we analyze the last rule of the derivation (only the cases that are not similar are shown):
\begin{description}
\item[\Rule{Abs-}] We know that the derivation of $\tyof e \Gamma$ (if any) ends with the rule \Rule{Abs\Aa}.
Moreover, by using the induction hypothesis on the premise, we know that $\tyof e \Gamma \neq \varnothing$.
Thus we have $\tyof e \Gamma \leq \neg (\arrow {t_1} {t_2}) = t$ (because every type $\neg (\arrow {s'} {t'})$
such that $\neg (\arrow {s'} {t'}) \land \bigwedge_{i\in I} \arrow {s_i} {t_i} \neq \Empty$ is in $\tsint{\tsfun{\arrow {s_i} {t_i}}}$).
\end{description}
\
Now let's prove the second property. We have a rank-0 negated derivation of $\Gamma \evdash e t \Gamma'$.
TODO
\begin{description}
\item[\Rule{Base}] Any value of $n_o$ will give $\Refine {e,t} \Gamma \leqA \Gamma$, even $n_o = 0$.
\item[\Rule{Path}] We have $\Gamma' = \Gamma_1,(\occ e \varpi:t')$.
We proceed the same way as in the previous proof, but this time the induction hypothesis is weaker
(we don't have $\tsrep {\tyof e \Gamma} \leq t$ but only $\tyof e \Gamma \leq t$).
Thus, we can't prove that $\env {\Gamma'',e,t} (\varpi) \leq t'$ with $\RefineStep {e,t}^{n'} (\Gamma_2) \leqA \Gamma''$
for a certain $n'$. Instead, we will prove that
$\env {\Gamma'',e,t} (\varpi) \tsand \tyof {\occ e \varpi} {\Gamma''} \leq t'$.
It suffices to conclude in the same way as in the previous proof.
\begin{description}
\item[\Rule{PSubs}] Trivial using the induction hypothesis.
\item[\Rule{PInter}] Quite similar to the previous proof (the induction hypothesis is weaker, but it works the same way).
\item[\Rule{PTypeof}] By using the outer induction hypothesis we get $\tyof {\occ e \varpi} {\Gamma_2} \leq t'$ so it is trivial.
\item[\Rule{PEps}] Trivial.
\item[\Rule{PAppR}] TODO
\item[\Rule{PAppL}] %By using the induction hypothesis we get:
%\begin{align*}
% &\env {\Gamma_1'',e,t} (\varpi.1) \tsand \tyof {\occ e {\varpi.1}} {\Gamma_1''} \leq t_1\\
% &\env {\Gamma_2'',e,t} (\varpi) \tsand \tyof {\occ e {\varpi}} {\Gamma_2''} \leq t_2\\
% &\RefineStep {e,t}^{n_1} (\Gamma_2) \leqA \Gamma_1''\\
% &\RefineStep {e,t}^{n_2} (\Gamma_2) \leqA \Gamma_2''
%\end{align*}
%
TODO
\item[\Rule{PPairL}] TODO%Quite straightforward using the induction hypothesis and the descriptive definition of $\bpi_1$.
\item[\Rule{PPairR}] TODO%Quite straightforward using the induction hypothesis and the descriptive definition of $\bpi_2$.
\item[\Rule{PFst}] TODO%Trivial using the induction hypothesis.
\item[\Rule{PSnd}] TODO%Trivial using the induction hypothesis.
\end{description}
\end{description}
\end{proof}
\ No newline at end of file
\ No newline at end of file
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