Nathaniel pushed to branch bosn at Stefan / Typer

Commits: c52700fd by nbos at 2018-08-22T21:29:36Z Finish fix lem:FV-E-Lam

- - - - -

1 changed file:

- doc/formal/typer_theory.tex

Changes:

===================================== doc/formal/typer_theory.tex ===================================== @@ -433,7 +433,7 @@ Our definition of \CC\ is based on the original Calculus of Constructions (CC) \ \label{fig:[]} \end{figure}

-The translator operator \rew{\ } is defined on contexts and terms of \CC. We expose the translation on figure \ref{fig:[]}. We will consider this translation correct if it is both complete and sound as per the following definitions. \emph{Completeness} of the translation ($\Rightarrow$) is established if every translated expression of \CC\ inhabits its translated type in the Typer system. \emph{Soundness} of the translation ($\Leftarrow$) is established if every valid typing derivation of translated terms in the Typer system implies a valid typing derivation in \CC: +The translator operator \rew{_} is defined on contexts and terms of \CC. We expose the translation on figure \ref{fig:[]}. We will consider this translation correct if it is both complete and sound as per the following definitions. \emph{Completeness} of the translation ($\Rightarrow$) is established if every translated expression of \CC\ inhabits its translated type in the Typer system. \emph{Soundness} of the translation ($\Leftarrow$) is established if every valid typing derivation of translated terms in the Typer system implies a valid typing derivation in \CC: \begin{theorem} \label{thm:correctness-translation} \begin{align*} @@ -699,48 +699,57 @@ The impredicative product type translates to an erasable product type $(x:\rew{T \label{lem:E-Lam-FV} If we have \begin{mathpar} - %% TODO: Check if the condition `T:Type (s ℓ)` is really necessary - %% (If not, also fix on last case of completeness proof) - {\Ga, x:T ~ M:U \ \Ga, x:T ~ U : \Type\ \z \ \Ga ~ T : \Type\ (\s\ \l)} + %% FIXME: I am limiting the proof to translated terms because + %% 1) We don't need more than this + %% 2) The lemma doesn't seem to hold otherwise; e.g. + %% M := P|Q + %% M := λ(y:T)->V | x + %% + %% where V : U : Type0 so that (λ(y:T)->V | x) : U : Type0 + %% + %% Now, I don't know where y would appear in V while respecting V : U + %% and y : T, but we still have x ∈ FV(λ(y:T)->V | x) which is enough + %% as far as I know to disprove the lemma. This is not a counterexample + %% if we limit the lemma to translated terms [M] because the rule + %% (Type₁,Type₀,Type₁) ∉ Rcc, but instead (Type₁,Type₀,Type₀) ∈ R which + %% makes the abstraction erasable in Typer and thus, x is not free + {\rew{\Ga, x:T} ~ \rew{M}:\rew{U} \ \rew{\Ga, x:T} ~ \rew{U} : \Type\ \z \ \rew{\Ga} ~ \rew{T} : \Type\ (\s\ \l)} \end{mathpar} then the following always holds - $$x \notin \fv{M^*}$$ + $$x \notin \fv{\rew{M}^*}$$

\begin{proof}\ \ - By structural induction on extracted terms (figure \ref{fig:*}), either $M^*$ cannot be equal to it, or $x$ cannot be free within it, thus showing that $x \notin \fv{M^*}$. + By structural induction on $\rew{M}^*$:

- \textbf{Case} $M^* = y^*$:\ - The extraction is $y^* = y$. It cannot be that $y = x$ because $x : T : \Type (\s\ \l)$ and $y : U : \Type\ \z$ and equality is not defined between inhabitants of different types nor different universe. Therefore, $x \notin \fv{y}$ because $x \neq y$. + \textbf{Case} $\rew{M}^* = y^*$:\ + The extraction is $y^* = y$. It cannot be that $y = x$ because $x : \rew{T} : \Type (\s\ \l)$ and $y : \rew{U} : \Type\ \z$ and equality is not defined between inhabitants of different types nor of different universes. Therefore, $x \notin \fv{y}$ because $x \neq y$.

- \textbf{Case} $M^* = ((x:t)\explicit V)^*$ or $((x:t)\erasable V)^*$:\ - $M$ cannot be a product type since its type $U$ inhabits the smallest universe $\Type\ \z$ . + \textbf{Case} $\rew{M}^* = ((x:t)\explicit V)^*$ or $((x:t)\erasable V)^*$:\ + $\rew{M}$ cannot be a product type since its type $\rew{U}$ inhabits the smallest universe $\Type\ \z$ .

- %% FIXME: This shows a problem in our presentation. We use FV(M*) and we + %% FIX\rew{M}E: This shows a problem in our presentation. We use FV(\rew{M}*) and we %% define * but we don't define FV. Another option is to forget about * - %% and only define FV*(M), the set of non-erasable free variables. - \textbf{Case} $M^* = (s)^*$ with $s \in \S$:\ - The extraction is $s^* = s$. All $s \in S$ are closed constants and thus $x \notin \fv{s}$. + %% and only define FV*(\rew{M}), the set of non-erasable free variables. + \textbf{Case} $\rew{M}^* = \rew{s}^*$ with $\rew{s} \in \S$:\ + The extraction is $\rew{s}^* = \rew{s}$. All $\rew{s} \in S$ are closed constants and thus $x \notin \fv{\rew{s}}$.

- \textbf{Case} $M^* = (\la(y:t)\explicit V)^*$:\ - The extraction makes this $\la(y)\explicit V^*$. By the rules in $\R$, if $M$ has sort $\Type\ \z$, then it is an upper bound for the sort of $V$. Thus, $V : U' : \Type\ \z$ and we have $x \notin \fv{V^*}$ by the induction hypothesis. - - \textbf{Case} $M^* = (\la(y:t)\erasable V)^*$:\ - The extraction makes this $V^*$. By the rules in $\R_e$, if $M$ has sort $\Type\ \z$, then $V$ also has sort $\Type\ \z$. Thus, by the induction hypothesis, $x \notin \fv{V^*}$. - - %% FIXME: - \textbf{Case} $M^* = (P \ap Q)^*$:\ - The extraction is $(P \ap Q)^* = P^* \ap Q^*$. - %% FIXME: $P$ can be something else than an abstraction (e.g. it can be - %% a simple variable). What we can know is that P : T : Prop, because we - %% know that it returns something in Prop, so we can - %% apply the induction hypothesis to it. - $P$ can only expand to an abstraction such that $P^* \ap Q^* = (\la (x:t) \explicit V)^* | Q^*$. We have shown that $x$ is not free in the explicit abstraction. - %% FIXME: We can only use the induction hypothesis if Q : T : Prop! - By the induction hypothesis, $x$ is not free in $Q^*$. - - %% FIXME: Again, $P$ can be something else than an abstraction. - \textbf{Case} $M^* = (P \appp Q)^*$:\ - The extraction is $(P \appp Q)^* = P^*$. $P$ can only expand to an abstraction $(\la (\iota:t) \erasable V)^*$ and we have shown that $x$ is not free in the erasable abstraction. + \textbf{Case} $\rew{M}^* = (\la(y:t)\explicit V)^*$:\ + The extraction makes this $\la(y)\explicit V^*$. By the rules in $\R$, if $\rew{M}$ has sort $\Type\ \z$, then it is an upper bound for the sort of $V$. Thus, $V : U' : \Type\ \z$ and we have $x \notin \fv{V^*}$ by the induction hypothesis. + + \textbf{Case} $\rew{M}^* = (\la(y:t)\erasable V)^*$:\ + The extraction makes this $V^*$. By the rules in $\R_e$, if $\rew{M}$ has sort $\Type\ \z$, then $V$ also has sort $\Type\ \z$. Thus, by the induction hypothesis, $x \notin \fv{V^*}$. + + \textbf{Case} $\rew{M}^* = (P \ap Q)^*$:\ + The extraction is $(P \ap Q)^* = P^* \ap Q^*$. By the typing rule \textsc{X-App}, because $P \ap Q : \rew{U}$, then $$P : (y:t)\explicit \rew{U}{Q/y}$$ + %% FIXME: I'm not sure about this "reverse substitution" business + %% happening above. + %% FIXME: Also, are contexts necessary here? + for $t$ such that $Q:t$. Further, since $\rew{U} : \Type\ \z$ and because the only rules that match $(s_1,\Prop,s_3) \in R_{CC}$ have $s_3 = \Prop$ then by induction hypothesis on the completeness of the translation, we can infer $$(y:t)\explicit \rew{U}{Q/y} : \Type\ \z$$ +and thus assume $x \notin \fv{P^*}$ by induction hypothesis on this lemma---although only the cases of the variable, the lambda abstraction and the applications apply. Because the product type of $P$ is explicit, the sort of $Q$ is also upper bounded by $\Type\ \z$ because explicit product types occur by the application of \textsc{X-Prod} with a rule that has $s_3 = \max (s_1,s_2)$. Thus we have $x \notin \fv{Q^*}$ by the induction hypothesis. + + + \textbf{Case} $\rew{M}^* = (P \appp Q)^*$:\ + The extraction is $(P \appp Q)^* = P^*$. Similar to the previous case, because $P$ has the same sort as $\rew{M}$, we have $x \notin \fv{P^*}$ by induction hypothesis. \end{proof} \end{lemma}

View it on GitLab: https://gitlab.com/monnier/typer/commit/c52700fd91d2133021fd0e04a737fc5429b3...