Nathaniel pushed to branch bosn at Stefan / Typer

Commits: e9edd7ec by nbos at 2018-08-10T03:40:34Z Put theorems and lemmas on the same counter

- - - - - 9b526a75 by nbos at 2018-08-14T04:21:58Z Reduce margin; avoid undefined use of ∪ with CCω sorts; make eq:corresctness-translation a theorem; finish proof of lem:R-equiv; start proof of lem:Re-equiv

- - - - - 37d2e51b by nbos at 2018-08-14T06:02:11Z Fix references to lemmas lem:S- lem:A- lem:R- and lem:Re-equiv in proof

- - - - - 998d77aa by nbos at 2018-08-14T06:22:00Z Complete proof of lem:Re-equiv

- - - - -

2 changed files:

- doc/formal/commands.tex - doc/formal/typer_theory.tex

Changes:

===================================== doc/formal/commands.tex ===================================== @@ -1,7 +1,8 @@ \renewcommand{\rmdefault}{ptm} + %% Theorems \newtheorem{theorem}{Theorem}[section] -\newtheorem{lemma}{Lemma}[section] +\newtheorem{lemma}[theorem]{Lemma}

\theoremstyle{definition} \newtheorem{definition}{Definition}[section]

===================================== doc/formal/typer_theory.tex ===================================== @@ -1,5 +1,5 @@ \documentclass[10pt]{article} -% \usepackage[a4paper,margin=1in,footskip=0.25in]{geometry} +\usepackage[a4paper,margin=35mm,footskip=10mm]{geometry}

\usepackage{amsmath,amsthm,amssymb,mathtools,stmaryrd} \usepackage{mathpartir,mdframed,empheq} @@ -333,7 +333,7 @@ In this section we will prove that the erasable terms of Typer allow for a repre \R_{CC} = { &(\Prop, \Prop, \Prop) \ &(\Prop, \Type_i, \Type_i) &\forall i > 0 \ &(\Type_i, \Prop, \Prop); &\forall i > 0 \ - &(\Type_i,\Type_j,(\Type_i\cup\Type_j)); &\forall i > 0 \ + &(\Type_i,\Type_j,\Type_{\max (i,j)}); &\forall i > 0 \ \end{empheq} \vspace{-5mm} \caption{\CC's Pure Type System} @@ -387,12 +387,13 @@ In this section we will prove that the erasable terms of Typer allow for a repre

Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, but with an added infinite hierarchy of universes above an impredicative \Prop. They are arranged in the series: $$\Prop : \Type_1 : \Type_2 : \Type_3 : \Type_4 : ...$$

-\CC's PTS definition is shown in figure \ref{fig:CC-pts}. The typing rules for \CC\ are shown in figure \ref{fig:CC-rules}. The structure of the PTS is derived from Luo's own extension of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop, \Prop, \Prop)$, $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, (\Type_i\cup\Type_j))$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). Our definition of \CC\ will therefore behave differently than other definitions of \CC\ (see for example \cite{miquel}). +\CC's PTS definition is shown in figure \ref{fig:CC-pts}. The typing rules for \CC\ are shown in figure \ref{fig:CC-rules}. The structure of the PTS is derived from Luo's own extension of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\Prop, \Prop, \Prop)$, $(\Prop,\Type_i,\Type_i)$ and $(\Type_i, \Type_j, \Type_{\max (i,j)})$. This is because we do not have access to ECC's cumulativity and \emph{lift} operator, which would usually permit us to derive the sort of a type constructed from the abstraction of a variable in one universe over a term in another universe (i.e. dependent types and polymorphic functions). Our definition of \CC\ will therefore behave differently than other definitions of \CC\ (see for example \cite{miquel}).

\subsection{Translation} \begin{figure}[h] + \centering \fbox{ - \begin{minipage}{1.0\linewidth} + \begin{minipage}{0.85\linewidth} \begin{align*} \rew{\cdot} &= \cdot & \rew{\Prop} &= \Type\ \z \ \rew{\Ga,x:T} &= \rew{\Ga},x:\rew{T} & \rew{\Type_{i}} &= \Type\ (\s^{i}\ \z) \[-20pt] @@ -421,14 +422,15 @@ Our definition of \CC\ is based on the original Calculus of Constructions (CC) \ \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: -\begin{align} - \label{eq:iff-context} +\begin{theorem} + \label{thm:correctness-translation} +\begin{align*} \Ga \CCdash & ~~ \iff ~~ \rew{\Ga} ~ \ - \label{eq:iff-judgment} \Ga \CCdash e:\tau & ~~ \iff ~~ \rew{\Ga} ~ \rew{e}:\rew{\tau} -\end{align} +\end{align*} +\end{theorem}

-Before proceeding with the proofs, we will show the following lemmas: +Before proving the correctness of the equality, we will need the following lemmas: \begin{lemma} \label{lem:S-equiv} $s \in \S_{CC} \iff \rew{s} \in \S$ @@ -439,54 +441,87 @@ Before proceeding with the proofs, we will show the following lemmas: %% If we defined [Typeω] = Typeω, it would still be injective, and Typeω %% is in \S, yet Typeω is not in \S_CC so the reverse implication %% wouldn't hold. - %% FIXME: But [] is only defined on terms of S_{CC} so if there - %% exists a '[s]', then there necessarily exists a 's' + %% + %% %% FIXME: But [] is only defined on terms of S_{CC} so if there + %% %% exists a '[s]', then there necessarily exists a 's' Conversely, because the translation on sorts is defined on elements of $S_{CC}$, it follows that if $\rew{s} \in S$, then by necessity $s \in S_{CC}$. \end{proof} \end{lemma}

+% FIXME: For the following lemmas, I'm not sure whether to stop at the +% '(\s^i\ \z) \forall i' form or to show the switch to the '\Type\ \ell +% \forall \ell' form. The first is sufficient, but looks less like our +% presentation of the PTS but the second has the typelevel variable 'l' in +% the syntax for '\ell' and may lead to confusion even if we bind \ell to +% elements of \mathbb{L} + \begin{lemma} \label{lem:A-equiv} $(s_1:s_2) \in \A_{CC} \iff (\rew{s_1}:\rew{s_2}) \in \A$ \begin{proof} - In the forward direction, for $(\Prop:\Type_1) \in \A_{CC}$, we know that $$(\rew{\Prop}:\rew{\Type_1}) = (\Type\ \z:\Type\ (\s\ \z)) \in A$$ + In the forward direction, for $(\Prop:\Type_1) \in \A_{CC}$, we know that + \begin{align*} + (\rew{\Prop}:\rew{\Type_1}) &= (\Type\ \z:\Type\ (\s\ \z)) \in \A + \end{align*} + And for $(\Type_i:\Type_{i+1}) \in \A_{CC}$, we know that \begin{align*} (\rew{\Type_i}:\rew{\Type_{i+1}}) &= (\Type\ (\s^i\ \z):\Type\ (\s^{i+1}\ \z)) &&\forall\ i>0\ &= (\Type\ (\s^i\ \z):\Type\ (\s\ (\s^i\ \z)) &&\forall\ i>0\ &= (\Type\ \l:\Type\ (\s\ \l)) &\in \A \quad &\forall\ \l \in \mathbb{L} \backslash {\z} \end{align*} - Conversely, since the translation on sorts is defined on elements of $S_{CC}$, sorts $\rew{s}$ only match with sorts of the form $\Type\ (\s^i\ \z)\in \S\ \forall i \ge 0$ (lemma \ref{lem:S-equiv}) so it follows that rules $(\rew{s_1}:\rew{s_2}) \in \A$ only match with rules of the form $(\Type\ \l:\Type\ (\s\ \l)) \in \A ~~ \forall \l \in \mathbb{L}$, for each of which exists a rule $(s_1:s_2) \in A_{CC}$ by the equality just established in the forward direction. + Conversely, since the translation on sorts is defined on elements of $S_{CC}$, sorts $\rew{s}$ match with sorts of the form $\Type\ (\s^i\ \z)\in \S\ \forall i \ge 0$ (lemma \ref{lem:S-equiv}). It follows that axioms $(\rew{s_1}:\rew{s_2}) \in \A$ match with axioms of the form $(\Type\ \l:\Type\ (\s\ \l)) \in \A ~~ \forall \l \in \mathbb{L}$, for each of which there exists an axiom $(s_1:s_2) \in A_{CC}$ by the equality just established in the forward direction. \end{proof} \end{lemma}

\begin{lemma} - \label{lem:R-equiv} + \label{lem:R-equiv} $(s_1,s_2,s_3) \in \R_{CC} \iff (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R \text{ if } s_1 \neq \Type_i \text{ or } s_2 \neq \Prop$ +\begin{proof} + In the forward direction, first there is $(\Prop,\Prop,\Prop) \in \R_{CC}$ for which we have + $$(\rew{\Prop},\rew{\Prop},\rew{\Prop}) = (\Type\ \z,\Type\ \z,\Type\ \z) \in \R$$ + Second, there is $(\Prop, \Type_i, \Type_i) \in \R_{CC}\ \forall i > 0$ for which we have + $$(\rew{\Prop}, \rew{\Type_i}, \rew{\Type_i}) = (\Type\ \z, \Type\ (\s^i\ \z), \Type\ (\s^i\ \z)) \in \R \quad \forall i > 0$$ + And finally there is $(\Type_i, \Type_j, \Type_{\max (i,j)})$ for which we have \begin{align*} - (s_1,s_2,s_3) \in \R_{CC} &\iff (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R &\text{if $s_1 \neq \Type_i$} \[-5pt] - & &\text{or $s_2 \neq \Prop$} + (\rew{\Type_i}, \rew{\Type_j}, \rew{\Type_{\max (i,j)}}) &= + \begin{cases} + (\Type\ (\s^i\ \z),\Type\ (\s^j\ \z),\Type\ (\s^i\ \z)) & \text{if } i>j \ + (\Type\ (\s^i\ \z),\Type\ (\s^j\ \z),\Type\ (\s^j\ \z)) & \text{if } j>i + \end{cases} \quad \forall i,j > 0 \ + &= + \begin{cases} + (\Type\ \l_1, \Type\ \l_2, \Type\ \l_1) & \text{if } \l_1 \cup \l_2 = \l_1 \ + (\Type\ \l_1, \Type\ \l_2, \Type\ \l_2) & \text{if } \l_1 \cup \l_2 = \l_2 + \end{cases} \quad \forall \l_1,\l_2 \in \mathbb{L} \backslash {\z} \ + &= (\Type\ \l_1, \Type\ \l_2, \Type\ (\l_1 \cup \l_2)) \quad \in \R \quad \forall \l_1,\l_2 \in \mathbb{L} \backslash {\z} \end{align*} - \begin{proof} - For the impredicative rules, in the forward direction, for $(\Type_i,\Prop,\Prop) \in \R_{CC}$, we have - \begin{align*} - (\rew{\Type_i},\rew{Prop},\rew{Prop}) &= (\Type\ (\s^i\ \z),\Type\ \z, \Type\ \z) &&\forall\ i > 0\ - &= (\Type\ (\s\ \l),\Type\ \z, \Type\ \z) & \in \R_e \quad &\forall\ \l \in \mathbb{L} - \end{align*} - Conversly, we have already shown that $(\rew{\Type_i},\rew{Prop},\rew{Prop}) \in \R_e\ \forall i > 0$ + Conversely, since the translation on sorts is defined on elements of $S_{CC}$, sorts $\rew{s}$ match with sorts of the form $\Type\ (\s^i\ \z)\in \S\ \forall i \ge 0$ (lemma \ref{lem:S-equiv}). It follows that rules $(\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$ match with rules of the form $$(\Type\ \l_1, \Type\ \l_2, \Type\ (\l_1 \cup \l_2)) \in \R ~~ \forall \l_1,\l_2 \in \mathbb{L}$$ By the equalities established in the forward direction, each such rule has a single corresponding rule in $(s_1,s_2,s_3) \in \R_{CC}$, as long as $s_1 \neq \Type_i \text{ or } s_2 \neq \Prop$

- For $(\Prop, \Prop, \Prop)$, we have \todo - \end{proof} + % The condition $\text{ if } s_1 \neq \Type_i \text{ or } s_2 \neq \Prop$ ensures that the rule scheme + % \begin{align*} + % (\rew{\Type_i},\rew{\Prop},\rew{\Type_i}) = (\Type\ \l_1, \Type\ \z, \Type\ \l_1) &\in \R \ + % (\Type_i,\Prop,\Type_i) &\notin \R_{CC} + % \end{align*} + % is not considered. + +\end{proof} \end{lemma} \begin{lemma} \label{lem:Re-equiv} $$(\Type_i,\Prop,\Prop) \in \R_{CC} \iff (\rew{\Type_i},\rew{Prop},\rew{Prop}) \in \R_e \quad \forall i > 0$$ \begin{proof} - \todo + In the forward direction, for $(\Type_i,\Prop,\Prop) \in \R_{CC}$, we have + \begin{align*} + (\rew{\Type_i},\rew{Prop},\rew{Prop}) &= (\Type\ (\s^i\ \z),\Type\ \z, \Type\ \z) &&\forall\ i > 0\ + &= (\Type\ (\s\ \l),\Type\ \z, \Type\ \z) & \in \R_e \quad &\forall\ \l \in \mathbb{L} \backslash {\z} + \end{align*} + Conversely, $(\rew{\Type_i},\rew{Prop},\rew{Prop}) \in \R_e\ \forall i > 0$ matches with rules of the form $$(\Type\ (\s\ \l),\Type\ \z, \Type\ \z) \in \R_e \quad \forall\ \l \in \mathbb{L} \backslash {\z}$$ For each of which there is a rule $(\Type_i,\Prop,\Prop) \in \R_{CC}$ by the equality established in the forward direction. + \end{proof} \end{lemma}

\subsection{Completeness of translation} -We will proceed by structural induction on typing derivation to show that each valid derivation of \CC\ translates to a valid derivation in the Typer system ($\Rightarrow$). For most typing rules, the proof is straightforward: we assume the translated premises by the induction hypothesis and then show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules. +We will proceed by structural induction on typing derivation to show that, as per theorem \ref{thm:correctness-translation}, each valid derivation of \CC\ translates to a valid derivation in the Typer system ($\Rightarrow$). For most typing rules, the proof is straightforward: we assume the translated premises by the induction hypothesis and then show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules.

\underline{\textbf{CC-Wf-E:}} \begin{mathpar} @@ -513,8 +548,8 @@ The translation is immediately true under Typer by rule \textsc{Wf-E}. By the induction hypothesis we can assume $$\rew{\Ga} ~ \rew{T}:\rew{s}$$

-and we have that -$$s \in S_{CC} \iff \rew{s} \in \S.$$ +and from lemma \ref{lem:S-equiv} we can infer +$$\rew{s} \in \S$$

We have yet to show that $$x \notin \dv{\rew{\Ga}}$$ @@ -553,8 +588,8 @@ We can now infer the translation of the conclusion by rule By the induction hypothesis we can assume $$\rew{\Ga} ~$$

-and we have that -$$(s_1:s_2) \in \A_{CC} \iff (\rew{s_1}:\rew{s_2}) \in \A.$$ +and from lemma \ref{lem:A-equiv} we can infer +$$(\rew{s_1}:\rew{s_2}) \in \A$$

We reach the translation of the conclusion by rule \begin{mathpar} @@ -600,13 +635,12 @@ We reach the translation of the conclusion by rule By the induction hypothesis, there are two subcases to consider---a predicative and an impredicative one:

\textbf{Predicative subcase:}\ -We have the assumptions +The predicative subcase will concern applications of \textsc{CC-Prod} for which the rule is $(s_1,s_2,s_3) \in \R_{CC}$ where $s_1 \neq \Type_i$ or $s_2 \neq \Prop$. We have the assumptions \begin{mathpar} {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{s_2}} \end{mathpar} -and we know that -%% FIXME: This is only true if s1 != Type_i or s2 != Prop !!! -$$(s_1,s_2,s_3) \in \R_{CC} \iff (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$$ +and from lemma \ref{lem:R-equiv} we can infer +$$(\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$$ from which we can conclude \begin{mathpar} \infer @@ -616,12 +650,12 @@ from which we can conclude \end{mathpar}

\textbf{Impredicative subcase:}\ -We have the assumptions +The impredicative subcase will concern applications of \textsc{CC-Prod} for which the rule is $(\Type_i,\Prop,\Prop) \in \R_{CC}$. We have the assumptions \begin{mathpar} {\rew{\Ga} ~ \rew{T}:\rew{\Type_i} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{\Prop}} \end{mathpar} -and we know that -$$(\Type_i,\Prop,\Prop) \in \R_{CC} \iff (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e$$ +and from lemma \ref{lem:Re-equiv} we can infer +$$(\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e$$ from which we can conclude \begin{mathpar} \infer @@ -697,12 +731,14 @@ The impredicative product type translates to an erasable product type $(x:\rew{T

%% FIXME: This should be `y` (since it can be any variable, not only the %% variable `x` that we're trying to prove isn't ∈ FV(M*). - %% FIXME: It's not? The rule is about making an abstraction of 'x', so - %% why do we care for 'y'? I understand that we could have a case with - %% a variable that is not 'x' (and the same for the cases where [M]* is - %% a function) but they are trivial like the case for 's'. Should we still - %% mention them? - \underline{\textbf{Case}} $\rew{M}^* = x^* = x$:\ + %% + %% %% FIXME: It's not? The rule is about making an abstraction of 'x', so + %% %% why do we care for 'y'? I understand that we could have a case with + %% %% a variable that is not 'x' (and the same for the cases where [M]* is + %% %% a function) but they are trivial like the case for 's'. Should we still + %% %% mention them? + +\underline{\textbf{Case}} $\rew{M}^* = x^* = x$:\ This is impossible because we know that $x : \rew{T}$ and since $$(x:\rew{T})\erasable\rew{U} : \Prop$$ then, under the only possible construction of an erasable product type, we know that $\rew{T} : \rew{\Type_i}$ and $\rew{U} : \rew{\Prop}$. Because $\rew{T}$ and $\rew{U}$ inhabit different universes, their inhabitants $x : \rew{T}$ and $\rew{M} : \rew{U}$ cannot be equal.

\underline{\textbf{Case}} $\rew{M}^* = ((x:t)\explicit V)^*$ or $((x:t)\erasable V)^*$:\

View it on GitLab: https://gitlab.com/monnier/typer/compare/769d88566374e16553cec7f113f6a8ddfb3...