Commit 2478298a authored by Mickael Laurent's avatar Mickael Laurent
Browse files

fix in the proofs

parent 55aa2e99
......@@ -206,9 +206,21 @@
In this section, the substitutions on expressions that we introduce are up to alpha-renaming and perform only one pass.
For instance, if our substitution is $\rho=\subst {(\lambda^t x. x) y} {y}$, we have $((\lambda^t x. x)((\lambda^t z. z) y))\rho = (\lambda^t x. x) y$.
The environements also operate up to alpha-renaming.
The environments also operate up to alpha-renaming.
Finally, the only environments that we consider are well-formed environments (see definition below). We can easily
check that every derivation only contains well-formed environments, provided that the initial judgement also use a well-formed environment.
It is a consequence of the fact that rule \Rule{Case} require $e$ to be typeable and that it only refines subexpressions of $e$.
\subsubsection{Environments --- definitions}
\begin{definition}[Well-formed environment]
We say that an environment $\Gamma$ is well-formed iff
$\forall e\in\dom\Gamma \text{ s.t. $e$ is not a variable}.\ \exists t.\ \Gamma\setminus\{e\} \vdash e:t$.
In other words, an environment can refine the type of an expression, but only if this expression is already typeable
without this entry in the environment (possibly with a strictly weaker type).
\end{definition}
\begin{definition}[Bottom environment]
Let $\Gamma$ an environment.\\
......@@ -318,7 +330,7 @@
\item[\Rule{PSubs}] Trivial (we use the induction hypothesis).
\item[\Rule{PEps}] This case is impossible.
\item[\Rule{PAppL}] We have $v \not\in \valsemantic{\neg (\arrow {t_1} {\neg t_2})}$. Thus, we have $v \in \valsemantic{\arrow {t_1} {\neg t_2}}$
and in consequence we can derive $\Gamma \vdash v:\arrow {t_1} {\neg t_2}$.
and in consequence we can derive $\Gamma \vdash v:\arrow {t_1} {\neg t_2}$ (because $e$ is well-typed in $\Gamma$).
Recall that $\occ e {\varpi.1}$ is necessarily a value (by hypothesis).
By using the induction hypothesis on $\pvdash \Gamma e t \varpi.1:t_1$, we can suppose $\occ e {\varpi.1} \in \valsemantic{t_1}$ (otherwise, we can conclude directly).
......@@ -335,7 +347,7 @@
Recall that $\occ e {\varpi.0}$ is necessarily a value (by hypothesis).
By using the induction hypothesis on $\pvdash \Gamma e t \varpi.0:\arrow {t_1} {t_2}$, we can suppose $\occ e {\varpi.0} \in \valsemantic{\arrow {t_1} {t_2}}$ (otherwise, we can conclude directly).
Thus, we can derive $\Gamma \vdash \occ e {\varpi.0}: \arrow {t_1} {t_2}$.
Thus, we can derive $\Gamma \vdash \occ e {\varpi.0}: \arrow {t_1} {t_2}$ (because $e$ is well-typed in $\Gamma$).
From $\Gamma \vdash v:t_1$ and $\Gamma \vdash \occ e {\varpi.0}: \arrow {t_1} {t_2}$, we can derive $\Gamma \vdash \occ e {\varpi}: t_2$
using the rule \Rule{App}.
......@@ -969,6 +981,7 @@
well-typed in $\Gamma$.
We will reuse the definitions and notations introduced in the previous proofs.
In particular, we only consider well-formed environments, as in the proofs of the declarative type system.
\subsubsection{Soundness}
......@@ -1323,10 +1336,12 @@
If $e=x$ is a variable, then the derivation only uses \Rule{Env}, \Rule{Inter} and \Rule{Subs}.
We can easily conclude just be using \Rule{Var\Aa}. Thus, let's suppose $e$ is not a variable.
If $e\in\dom\Gamma$, we can have the rule \Rule{Env} in our derivation, but there can only be
\Rule{Inter} and \Rule{Subs} after it (not \Rule{Abs-} as we have a positive derivation).
Thus, we can build a positive derivation of $\Gamma \vdash e:t'$ that does not use the rule \Rule{Env} on $e$
and such that $t'\land \Gamma(e) \leq t$. Thus we have a positive derivation for $\Gamma\setminus\{e\} \vdash e:t'$.
If $e\in\dom\Gamma$, we can have the rule \Rule{Env} applied to $e$ in our derivation, but in this case
there can only be \Rule{Inter} and \Rule{Subs} after it (not \Rule{Abs-} as we have a positive derivation).
Thus, our derivation contains a derivation of $\Gamma \vdash e:t'$ that does not use the rule \Rule{Env} on $e$
and such that $t'\land \Gamma(e) \leq t$ (actually, it is possible for our derivation to typecheck $e$ only using the rule \Rule{Env}:
in this case we can take $t'=\Any$ and use the fact that $\Gamma$ is well-formed).
Hence, we can build a positive derivation for $\Gamma\setminus\{e\} \vdash e:t'$.
By using the induction hypothesis we deduce that $\tsrep{\tyof e {\Gamma\setminus\{e\}}} \leq t'$.
Thus, by looking at the rule \Rule{Env\Aa},
we deduce $\tsrep{\tyof e \Gamma} \leq \Gamma(e) \land \tsrep{\tyof e {\Gamma\setminus\{e\}}} \leq t$.
......@@ -1469,3 +1484,22 @@
&\forall \Gamma, \Gamma', e, t.\ \Gamma \evdash e t \Gamma' \text{ has a rank-0 negated derivation } \Rightarrow \Refine {e,t} \Gamma \leqA \Gamma' \text{ (for $n_o$ large enough)}
\end{align*}
\end{theorem}
\begin{proof}
This proof is quite similar to that of the completeness for positive derivations.
In consequence, we will only detail cases that are quite different from those of the previous proof.
Let's begin with the first property. We have a rank-0 negated derivation of $\Gamma \vdash e:t$.
We want to show $\tyof e \Gamma \leq t$ (note that this is weaker than showing $\tsrep {\tyof e \Gamma} \leq t$).
As in the previous proof, we can suppose that $\Gamma \neq \bot$ and that $e$ is not a variable.
The case $e\in\dom\Gamma$ is also very similar, but there is an additional case to consider:
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).
TODO
\end{proof}
\ 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