Nathaniel pushed to branch bosn at Stefan / Typer

Commits: 769d8856 by nbos at 2018-08-10T02:28:06Z Fix and streamline lem:S-equiv and lem:A-equiv; split first part of lem:R-equiv into lem:Re-equiv

- - - - -

1 changed file:

- doc/formal/typer_theory.tex

Changes:

===================================== doc/formal/typer_theory.tex ===================================== @@ -433,14 +433,15 @@ Before proceeding with the proofs, we will show the following lemmas: \label{lem:S-equiv} $s \in \S_{CC} \iff \rew{s} \in \S$ \begin{proof} - For \Prop, we know that $\rew{\Prop} = \Type\ \z$ with $\Type\ \z \in \S$. For \Type$_i$, we know that for all $i$ we have $\rew{\Type_i} = \Type\ (\s^i\ \z)$ with $\Type\ (\s^i\ \z) \in \S ~ \forall i > 0$. + In the forward direction, for $\Prop \in S_{CC}$, we know that $$\rew{\Prop} = \Type\ \z\ \in \S$$ + And for $\Type_i \in \S_{CC}$, we know that $$\rew{\Type_i} = \Type\ (\s^i\ \z) \in \S \quad \forall i > 0$$ %% FIXME: Being injective is not sufficient. %% 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' - Because the translation on sorts is defined on $S_{CC}$, it follows that if $\rew{s} \in S$, then $s \in S_{CC}$. + 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}

@@ -448,35 +449,42 @@ Before proceeding with the proofs, we will show the following lemmas: \label{lem:A-equiv} $(s_1:s_2) \in \A_{CC} \iff (\rew{s_1}:\rew{s_2}) \in \A$ \begin{proof} - For $(\Prop:\Type_1)$, we know that $$(\rew{\Prop}:\rew{\Type_1}) = (\Type\ \z:\Type\ (\s\ \z)) \in A$$ For $(\Type_i:\Type_{i+1})$, we know that + 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$$ + 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*} - Because the translation on sorts is defined on $S_{CC} = {\Prop; \Type_i}\ \forall i > 0$, the axioms of the form $(\rew{s_1}:\rew{s_2}) \in \A$ are $(\rew{\Prop}:\rew{\Type_1})$ for which we have $$(\Prop:\Type_1) \in \A_{CC}$$ and $(\rew{\Type_i}:\rew{\Type_{i+1}}) \forall i > 0$ for which we have $$(\Type_i:\Type_{i+1}) \in A_{CC} \quad \forall i > 0$$ + 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. \end{proof} \end{lemma}

\begin{lemma} \label{lem:R-equiv} - Each rule $(\Type_i,\Prop,\Prop) \in \R_{CC}$ has a distinct and equivalent rule $(\rew{\Type_i},\rew{Prop},\rew{Prop}) \in R_e$ and each other rule $(s_1,s_2,s_3) \in \R_{CC}$ has a distinct and equivalent rule $(\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$; i.e. \begin{align*} - (\Type_i,\Prop,\Prop) \in \R_{CC} &\iff (\rew{\Type_i},\rew{Prop},\rew{Prop}) \in R_e\ (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$} \end{align*} \begin{proof} - For $(\Type_i,\Prop,\Prop) \in \R_{CC}$, we have + 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\ \l,\Type\ - \z, \Type\ \z) & \in \R_e \quad &\forall\ \l \in \mathbb{L} \backslash {\z} + (\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$ + For $(\Prop, \Prop, \Prop)$, we have \todo \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 + \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.

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