Nathaniel pushed to branch bosn at Stefan / Typer

Commits: e25ebfb7 by nbos at 2018-08-30T19:00:52Z Review of completeness of translation proof

- - - - - d374fc40 by nbos at 2018-09-01T09:22:40Z Rephrase parts of completeness of translation proof; finish soundness of translation proof; finish example

- - - - -

1 changed file:

- doc/formal/typer_theory.tex

Changes:

===================================== doc/formal/typer_theory.tex ===================================== @@ -737,7 +737,7 @@ Before proving the correctness of the equality, we show the following lemmas: \end{lemma}

\subsection{Completeness of translation} -By structural induction on typing derivation, as per theorem \ref{thm:correctness-translation} ($\Rightarrow$), each valid derivation of \CC\ translates to a valid derivation in the Typer system. For most typing rules, the proof consists in assuming the translated premises by the induction hypothesis and then showing that the translation of the conclusion from them by one of Typer's typing rules. +By structural induction on typing derivation of \CC, as per theorem \ref{thm:correctness-translation} ($\Rightarrow$), each valid derivation translates to a valid derivation in the Typer system. For most typing rules, by assuming the rule in \CC, we derive the necessary premises in Typer to show that the corresponding Typer rule also applies.

\underline{\textbf{CC-Wf-E:}} \begin{mathpar} @@ -761,13 +761,13 @@ The translation is immediately true under Typer by rule \textsc{Wf-E}. {\Ga , x:T \CCdash} \tag{CC-Wf-S} \end{mathpar} -By the induction hypothesis we can assume +By the induction hypothesis we assume $$\rew{\Ga} ~ \rew{T}:\rew{s}$$

-and from lemma \ref{lem:S-equiv} we can infer +From lemma \ref{lem:S-equiv} we infer $$\rew{s} \in \S$$

-We have yet to show that +To apply the Typer rule \textsc{Wf-S}, we have to show that $$x \notin \dv{\rew{\Ga}}$$

\begin{lemma} @@ -786,7 +786,7 @@ $$x \notin \dv{\rew{\Ga}}$$ Follows directly from lemma \ref{lem:DV-equiv}. \end{proof} \end{lemma} -We can now infer the translation of the conclusion by rule +We reach the translation of the conclusion by rule \begin{mathpar} \infer {\rew{\Ga} ~ \rew{T}:\rew{s} \ \rew{s} \in \S \ x \notin \dv{\rew{\Ga}}} @@ -801,10 +801,10 @@ We can now infer the translation of the conclusion by rule {\Ga \CCdash s_1:s_2} \tag{CC-Sort} \end{mathpar} -By the induction hypothesis we can assume +By the induction hypothesis we assume $$\rew{\Ga} ~$$

-and from lemma \ref{lem:A-equiv} we can infer +From lemma \ref{lem:A-equiv} we infer $$(\rew{s_1}:\rew{s_2}) \in \A$$

We reach the translation of the conclusion by rule @@ -822,7 +822,7 @@ We reach the translation of the conclusion by rule {\Ga \CCdash x:T} \tag{CC-Var} \end{mathpar} -By the induction hypothesis we can assume +By the induction hypothesis we assume $$\rew{\Ga} ~$$

\begin{lemma} @@ -834,7 +834,7 @@ $$\rew{\Ga} ~$$ \end{proof} \end{lemma}

-We reach the translation of the conclusion by rule +With lemma \ref{lem:in-ctx-equiv}, we reach the translation of the conclusion by rule \begin{mathpar} \infer {\rew{\Ga} ~ \ (x:\rew{T}) \in \rew{\Ga}} @@ -852,13 +852,13 @@ 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:}\ -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 +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 can assume \begin{mathpar} {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{s_2}} \end{mathpar} -and from lemma \ref{lem:R-equiv} we can infer +From lemma \ref{lem:R-equiv} we infer $$(\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$$ -from which we can conclude +with which we produce the translation of the conclusion by rule \begin{mathpar} \infer {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{s_2} \ (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R} @@ -867,13 +867,13 @@ from which we can conclude \end{mathpar}

\textbf{Impredicative subcase:}\ -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 +The impredicative subcase will concern applications of \textsc{CC-Prod} for which the rule is $(\Type_i,\Prop,\Prop) \in \R_{CC}$. We can assume \begin{mathpar} {\rew{\Ga} ~ \rew{T}:\rew{\Type_i} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{\Prop}} \end{mathpar} -and from lemma \ref{lem:Re-equiv} we can infer +From lemma \ref{lem:Re-equiv} we infer $$(\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e$$ -from which we can conclude +with which we produce the translation of the conclusion by rule \begin{mathpar} \infer {\rew{\Ga} ~ \rew{T}:\rew{\Type_i} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{\Prop} \ (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e} @@ -888,11 +888,11 @@ from which we can conclude {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U} \tag{CC-Lam} \end{mathpar} -By the induction hypothesis we can assume +By the induction hypothesis we assume \begin{mathpar} {\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U} \ \rew{\Ga} ~ \rew{(x:T) \explicit U} : \rew{s}} \end{mathpar} -We have two subcases to consider for the translation \rew{(x:T) \explicit U}: +To apply a lambda rule of Typer, we have to consider the two cases for the translation \rew{(x:T) \explicit U}:

\textbf{Predicative subcase:}\ The predicative product type translates to an explicit product type $(x:\rew{T}) \explicit \rew{U}$ and we apply the explicit \textsc{X-Lam} typing rule to derive the typing of the explicit lambda abstraction. @@ -904,7 +904,7 @@ The predicative product type translates to an explicit product type $(x:\rew{T}) \end{mathpar}

\textbf{Impredicative subcase:}\ -The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ which necessarily has sort $\rew{\Prop} = \Type\ \z$. We call upon lemma \ref{lem:E-Lam-FV} to infer that $x \notin \fv{\rew{M}^*}$ and we have the sufficient premises to apply rule \textsc{E-Lam} and we obtain the translation of the conclusion: +The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ which necessarily has sort $\rew{\Prop}$ with $T : \Type_i$ and $U : \Prop$ by the definition of translation. We call upon lemma \ref{lem:E-Lam-FV} to infer that $x \notin \fv{\rew{M}^*}$ and we have the sufficient premises to apply rule \textsc{E-Lam}. We obtain the translation of the conclusion \begin{mathpar} \infer {\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U} \ \rew{\Ga} ~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop} \ x \notin \fv{\rew{M}^*}} @@ -919,11 +919,11 @@ The impredicative product type translates to an erasable product type $(x:\rew{T {\Ga \CCdash M|N : U{N/x}} \tag{CC-App} \end{mathpar} -By the induction hypothesis we can assume +By the induction hypothesis we assume \begin{mathpar} {\rew{\Ga} ~ \rew{M} : \rew{(x:T) \explicit U} \ \rew{\Ga} ~ \rew{N}:\rew{T}} \end{mathpar} -And we again have two subcases to consider for the translation $\rew{(x:T) \explicit U}$: +Again, there are two subcases to consider for the translation $\rew{(x:T) \explicit U}$:

\textbf{Predicative subcase:}\ \begin{mathpar} @@ -939,9 +939,10 @@ And we again have two subcases to consider for the translation $\rew{(x:T) \expl {\rew{\Ga} ~ \rew{M}|||\rew{N} : \rew{U}{\rew{N}/x}} \tag{E-App} \end{mathpar} +\qed

\subsection{Soundness of translation} -By structural induction on typing derivation, as per theorem \ref{thm:correctness-translation} ($\Leftarrow$), each valid derivation of translated terms in the Typer system translates to a valid derivation of \CC. We consider each of Typer's typing rules, the terms of which are adapted to be translated terms of \CC's. We implicitly distribute the translation down to the atoms of terms. +By structural induction on typing derivations of Typer, as per theorem \ref{thm:correctness-translation} ($\Leftarrow$), each valid derivation of translated terms has a corresponding valid derivation in \CC. We consider each of Typer's typing rules, the terms of which are limited to be translated terms of \CC. We implicitly distribute translation in contexts.

\underline{\textbf{Wf-E:}}\ \begin{mathpar} @@ -963,22 +964,24 @@ The original judgment is immediately true in \CC\ by rule \textsc{CC-Wf-E} \underline{\textbf{Wf-S:}}\ \begin{mathpar} \infer - {\rew{\Ga} ~ \rew{T}:s \ s \in \S \ x \notin \dv{\rew{\Ga}}} + {\rew{\Ga} ~ \rew{T}:s' \ s' \in \S \ x \notin \dv{\rew{\Ga}}} {\rew{\Ga} , x:\rew{T} ~} \tag{WF-S} \end{mathpar} -By lemma \ref{lem:S-equiv}, we can infer from $s \in \S$ that $s' \in \S_{CC}$ for some $s'$ such that $s = \rew{s'}$. We can assume +It is not immediately obvious that sort $s'$ is a translated sort. Sorts in $\S$ that are not translations of sorts in $\S_{CC}$ include \SortL\ and \Sortw. However, because we assume the construction of translated term $\rew{T}$, it cannot correspond to \TypeLevel\ (inhabitant of \SortL) or universe-polymorphic types (inhabitants of \Sortw) so $s'$ can only really be of form $\Type\ \l$. Because each sort of the latter form has a corresponding sort in $\S_{CC}$ (lemma \ref{lem:S-equiv}), we can set $s' = \rew{s}$ with $s \in \S_{CC}$. + +Thus, by the induction hypothesis we have \begin{mathpar} - {\Ga \CCdash T:s'} + {\Ga \CCdash T:s \ s \in \S_{CC}} \end{mathpar} -by the induction hypothesis, since $s = \rew{s'}$. Finally, +By lemma \ref{lem:not-DV-equiv} we infer \begin{mathpar} x \notin \dv{\Ga} \end{mathpar} -is shown by means of lemma \ref{lem:not-DV-equiv}. Thus, we can reconstruct the inference step \textsc{CC-Wf-S}: +We therefore have the corresponding rule \begin{mathpar} \infer - {\Ga \CCdash T:s' \ s' \in \S_{CC} \ x \notin \dv{\Ga}} + {\Ga \CCdash T:s \ s \in \S_{CC} \ x \notin \dv{\Ga}} {\Ga , x:T \CCdash} \tag{CC-Wf-S} \end{mathpar} @@ -990,11 +993,11 @@ is shown by means of lemma \ref{lem:not-DV-equiv}. Thus, we can reconstruct the {\rew{\Ga} ~ \rew{s_1}:\rew{s_2}} \tag{Sort} \end{mathpar} -By lemma \ref{lem:A-equiv}, we can infer from $(\rew{s_1}:\rew{s_2}) \in \A$ that $(s_1:s_2) \in \A_{CC}$. We can assume +By lemma \ref{lem:A-equiv}, we infer from $(\rew{s_1}:\rew{s_2}) \in \A$ that $(s_1:s_2) \in \A_{CC}$. We can assume \begin{mathpar} {\Ga \CCdash} \end{mathpar} -by the induction hypothesis. Therefore we have the rule: +by the induction hypothesis. Therefore we have the rule \begin{mathpar} \infer {\Ga \CCdash \ (s_1:s_2) \in \A_{CC}} @@ -1009,11 +1012,11 @@ by the induction hypothesis. Therefore we have the rule: {\rew{\Ga} ~ x:\rew{T}} \tag{Var} \end{mathpar} -By lemma \ref{lem:in-ctx-equiv}, we can infer from $(x:\rew{T}) \in \rew{\Ga}$ that $(x:T) \in \Ga$ and we have +By lemma \ref{lem:in-ctx-equiv}, we infer from $(x:\rew{T}) \in \rew{\Ga}$ that $(x:T) \in \Ga$. By the induction hypothesis we have \begin{mathpar} \Ga \CCdash \end{mathpar} -by the induction hypothesis. We get: +We therefore have the corresponding rule \begin{mathpar} \infer {\Ga \CCdash \ (x:T) \in \Ga} @@ -1022,28 +1025,49 @@ by the induction hypothesis. We get: \end{mathpar}

\underline{\textbf{X-Prod:}}\ -Where $s_1 \neq \Type_i$ or $s_2 \neq \Prop$: +This case considers the typing derivation of term $\rew{(x:T)\explicit U}$. If \textsc{X-Prod} constructed it, then $\rew{(x:T)\explicit U} = (x:\rew{T})\explicit \rew{U}$. \begin{mathpar} \infer - {\rew{\Ga} ~ \rew{T}:s_1 \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:s_2 \ (s_1,s_2,\rew{s_3'}) \in \R} - {\rew{\Ga} ~ (x:\rew{T}) \explicit \rew{U} : \rew{s_3'}} + {\rew{\Ga} ~ \rew{T}:s_1' \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:s_2' \ (s_1',s_2',\rew{s_3}) \in \R} + {\rew{\Ga} ~ (x:\rew{T}) \explicit \rew{U} : \rew{s_3}} \tag{X-Prod} \end{mathpar} -By lemma \ref{lem:R-equiv}, we can infer from $(s_1,s_2,\rew{s_3'}) \in \R$ that $(s_1',s_2',s_3') \in \R_{CC}$ for some $s_1'$ and $s_2'$ such that $s_1 = \rew{s_1'}$ and $s_2 = \rew{s_2'}$. We can assume +\SortL\ is not part of the co-domain of the translation function $\rew{_}$, so $\rew{s_3}$ only matches with sorts of form $\Type\ \l\ $(where $\l \in \mathbb{L}$). The only rule scheme matching this condition is $(\Type\ \l_1, \Type\ \l_2, \Type\ (\l_1 \cup \l_2)) \in R$. Because every sort of form $\Type\ \l$ occupies the co-domain of the translation function, we can set $s_1' = \rew{s_1}$ and $s_2' = \rew{s_2}$. Thus, we have +\begin{mathpar} + {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{s_2} \ (\rew{s_1},\rew{s_2},\rew{s_3}) \in R_{CC}} +\end{mathpar} + +By induction hypothesis we assume +\begin{mathpar} + {\Ga \CCdash T:s_1 \ \Ga, x:T \CCdash U:s_2} +\end{mathpar} +By lemma \ref{lem:R-equiv} we infer +$$(s_1,s_2,s_3) \in \R_{CC}$$ +We can therefore apply the rule \begin{mathpar} \infer - {\Ga \CCdash T:s_1' \ \Ga, x:T \CCdash U:s_2' \ (s_1',s_2',s_3') \in \R_{CC}} - {\Ga \CCdash (x:T) \explicit U : s_3'} + {\Ga \CCdash T:s_1 \ \Ga, x:T \CCdash U:s_2 \ (s_1,s_2,s_3) \in \R_{CC}} + {\Ga \CCdash (x:T) \explicit U : s_3} \tag{CC-Prod} \end{mathpar}

\underline{\textbf{E-Prod:}}\ +This case considers the typing derivation of term $\rew{(x:T)\explicit U}$. If \textsc{E-Prod} constructed it, then $\rew{(x:T)\explicit U} = (x:\rew{T})\erasable \rew{U}$ so by the definition of translation, $U : \Prop$ and $T : \Type_i$. \begin{mathpar} \infer {\rew{\Ga} ~ \rew{T}:\rew{\Type_i} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{\Prop} \ (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e} {\rew{\Ga} ~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop}} \tag{E-Prod} \end{mathpar} +By the induction hypothesis we assume +\begin{mathpar} + {\Ga \CCdash T:\Type_i \ \Ga, x:T \CCdash U:\Prop} +\end{mathpar} +By lemma \ref{lem:Re-equiv} we have +\begin{mathpar} + {(\Type_i,\Prop,\Prop) \in \R_e} +\end{mathpar} +We can therefore apply the rule \begin{mathpar} \infer {\Ga \CCdash T:\Type_i \ \Ga, x:T \CCdash U:\Prop \ (\Type_i,\Prop,\Prop) \in \R_{CC}} @@ -1052,12 +1076,18 @@ By lemma \ref{lem:R-equiv}, we can infer from $(s_1,s_2,\rew{s_3'}) \in \R$ that \end{mathpar}

\underline{\textbf{X-Lam:}}\ +This case considers the typing derivation of term $\rew{\la(x:T)\explicit M}$. If \textsc{X-Lam} constructed it, then $\rew{\la(x:T)\explicit M} = \la(x:\rew{T})\explicit \rew{M}$ and accordingly has the product type $\rew{(x:T)\explicit U} = (x:\rew{T})\explicit \rew{U}$. \begin{mathpar} \infer {\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U} \ \rew{\Ga} ~ (x:\rew{T}) \explicit \rew{U} : \rew{s}} {\rew{\Ga} ~ \la(x:\rew{T}) \explicit \rew{M} : (x:\rew{T}) \explicit \rew{U}} \tag{X-Lam} \end{mathpar} +By the induction hypothesis we assume +\begin{mathpar} + {\Ga, x:T \CCdash M:U \ \Ga \CCdash (x:T) \explicit U : s} +\end{mathpar} +We can therefore apply the rule \begin{mathpar} \infer {\Ga, x:T \CCdash M:U \ \Ga \CCdash (x:T) \explicit U : s} @@ -1066,12 +1096,18 @@ By lemma \ref{lem:R-equiv}, we can infer from $(s_1,s_2,\rew{s_3'}) \in \R$ that \end{mathpar}

\underline{\textbf{E-Lam:}}\ +This case considers the typing derivation of term $\rew{\la(x:T)\explicit M}$. If \textsc{E-Lam} constructed it, then $\rew{\la(x:T)\explicit M} = \la(x:\rew{T})\erasable \rew{M}$ and accordingly has the product type $\rew{(x:T)\explicit U} = (x:\rew{T})\erasable \rew{U}$. In this case, by the definition of translation, we necessarily have $U:\Prop$ and $T:\Type_i$. \begin{mathpar} \infer {\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U} \ \rew{\Ga} ~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop} \ x \notin \fv{\rew{M}^*}} {\rew{\Ga} ~ \la(x:\rew{T}) \erasable \rew{M} : (x:\rew{T}) \erasable \rew{U}} \tag{E-Lam} \end{mathpar} +By the induction hypothesis we assume +\begin{mathpar} + {\Ga, x:T \CCdash M:U \ \Ga \CCdash (x:T) \explicit U : s} +\end{mathpar} +We can therefore apply the rule \begin{mathpar} \infer {\Ga, x:T \CCdash M:U \ \Ga \CCdash (x:T) \explicit U : \Prop} @@ -1080,12 +1116,18 @@ By lemma \ref{lem:R-equiv}, we can infer from $(s_1,s_2,\rew{s_3'}) \in \R$ that \end{mathpar}

\underline{\textbf{X-App:}}\ +This case considers the typing derivation of term $\rew{M|N}$. If \textsc{X-App} constructed it, then $\rew{M|N} = \rew{M}|\rew{N}$ and $\rew{M}$ has type $\rew{(x:T)\explicit U} = (x:\rew{T})\explicit \rew{U}$. \begin{mathpar} \infer {\rew{\Ga} ~ \rew{M} : (x:\rew{T}) \explicit \rew{U} \ \rew{\Ga} ~ \rew{N}:\rew{T}} {\rew{\Ga} ~ \rew{M}|\rew{N} : \rew{U}{\rew{N}/x}} \tag{X-App} \end{mathpar} +By the induction hypothesis we assume +\begin{mathpar} + {\Ga \CCdash M : (x:T) \explicit U \ \Ga \CCdash N:T} +\end{mathpar} +We can therefore apply the rule \begin{mathpar} \infer {\Ga \CCdash M : (x:T) \explicit U \ \Ga \CCdash N:T} @@ -1094,12 +1136,18 @@ By lemma \ref{lem:R-equiv}, we can infer from $(s_1,s_2,\rew{s_3'}) \in \R$ that \end{mathpar}

\underline{\textbf{E-App:}}\ +This case considers the typing derivation of term $\rew{M|N}$. If \textsc{E-App} constructed it, then $\rew{M|N} = \rew{M}|||\rew{N}$ and $\rew{M}$ has type $\rew{(x:T)\explicit U} = (x:\rew{T})\erasable \rew{U}$. \begin{mathpar} \infer {\rew{\Ga} ~ \rew{M} : (x:\rew{T}) \erasable \rew{U} \ \rew{\Ga} ~ \rew{N}:\rew{T}} {\rew{\Ga} ~ \rew{M}|||\rew{N} : \rew{U}{\rew{N}/x}} \tag{E-App} \end{mathpar} +By the induction hypothesis we assume +\begin{mathpar} + {\Ga \CCdash M : (x:T) \explicit U \ \Ga \CCdash N:T} +\end{mathpar} +We can therefore apply the rule \begin{mathpar} \infer {\Ga \CCdash M : (x:T) \explicit U \ \Ga \CCdash N:T} @@ -1107,7 +1155,7 @@ By lemma \ref{lem:R-equiv}, we can infer from $(s_1,s_2,\rew{s_3'}) \in \R$ that \tag{CC-App} \end{mathpar}

-Rules \textsc{Ind}, \textsc{Constr}, and \textsc{Case} cannot construct the judgment $\rew{\Ga} ~ \rew{e} : \rew{\tau}$ because inductive types are not part of the domain of the translation operator. +Rules \textsc{Ind}, \textsc{Constr}, and \textsc{Case} cannot construct the judgment $\rew{\Ga} ~ \rew{e} : \rew{\tau}$ because inductive types are not part of the domain of the translation operator. \qed

\subsection{Example} Consider the impredicative encoding of the \texttt{pack} existential type constructor in \CC: @@ -1132,7 +1180,7 @@ The translation of \texttt{pack} to Typer will assign abstractions to be either &\quad\leadsto\quad \rew{\Ga} ~ (x : \tau) \explicit \Type\ \z : \Type\ (\s\ \z) \end{align*}

-However, $b$ has both an erasable and an explicit component: +On the other hand, $b$ has both an erasable and an explicit component:

\begin{align*} \Ga &\CCdash t : \Prop \ @@ -1149,11 +1197,7 @@ However, $b$ has both an erasable and an explicit component: &\quad\leadsto\quad \rew{\Ga} ~ (y : \tau)\erasable (z : f|y)\explicit t : \Type\ \z\ \end{align*}

-In the above Typer expression, $y$ is an \emph{erasable} term applied \emph{explicitly} to the term $f$. This is not contradictory to the rule \textsc{E-Lam} because the type of - -Thus, the application of $b$ to the witness and the proof will translate \todo - -RESULT: +If we proceed acordingly on the rest of the term, we get \begin{align*} \mathtt{pack}\ : \quad &(\tau : \Type\ (\s\ \z)) \erasable (f : (x : \tau) \explicit \Type\ \z) \erasable (w : \tau) \erasable (p : f| w) \explicit\ @@ -1162,6 +1206,15 @@ RESULT: &\la (t : \Type\ \z) \erasable \la (b : (y : \tau) \erasable (z : f|y) \explicit t) \explicit b|||w|p \end{align*}

+Finally, we can apply the extraction function and erase all but the explicit program +\begin{align*} + \mathtt{pack}\ : \quad + &\forall (\tau : \Type\ (\s\ \z)).\forall(f : (x : \tau) \explicit \Type\ \z).\forall(w : \tau).(p : f| w) \explicit\ + &\forall(t : \Type\ \z).(b : \forall(y : \tau).(z : f|y) \explicit t) \explicit t {w/y} {p/z}\[10pt] + :=\ &\la (p) \explicit \la (b) \explicit b|p +\end{align*} + +

\newpage \bibliographystyle{alpha}

View it on GitLab: https://gitlab.com/monnier/typer/compare/89aecbb1547ea6467c0f8e84d2f288bbaa2...