Nathaniel pushed to branch bosn at Stefan / Typer

Commits: ce6c1ca9 by nbos at 2018-08-03T19:45:52Z Define translation operator; stage the proof to be bidirectional; replace correspondance between PTS's with lemmas of injective maps between sorts and axioms of CCw and Typer

- - - - - 69c04c10 by nbos at 2018-08-03T20:12:04Z Prove lemma 3.3 + 3.4

- - - - - 1599bd1c by nbos at 2018-08-03T20:25:50Z Prove lemma 3.5

- - - - -

1 changed file:

- doc/formal/typer_theory.tex

Changes:

===================================== doc/formal/typer_theory.tex ===================================== @@ -43,10 +43,10 @@ We here formalize the Typer language and prove some of its properties. The gist \end{figure}

\subsection{Universes and Universe Polymorphism} -Each type universe $\Type\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \mathsf{z} ~~|~~ \mathsf{s}\ \l ~~|~~ \l_1 \cup \l_2 ~~|~~ l$$ +Each type universe $\Type\ \l$ is indexed by a \emph{type level} defined by the syntax: $$\l ::= \z ~~|~~ \s\ \l ~~|~~ \l_1 \cup \l_2 ~~|~~ l$$ %% FIXME: We'll need somewhere to clarify that those `l`s have to be present %% in the Γ environment with type TypeLevel. -All type levels $\l$ inhabit the type \TypeLevel\ which itself belongs to the sort \SortL. The two first constructs correspond to the constant zero and to the successor function, respectively. We define a set $\mathbb{L}$ which is closed under those two constructs and thus contains a type level $\l \in \mathbb{L}$ for every conventional natural number $n \in \mathbb{N}$. The operator $\cup$ returns the maximum of two type levels. The construct $l$ stands for a \emph{level variable} which will occur in universe polymorphic definitions. +All type levels $\l$ inhabit the type \TypeLevel\ which itself belongs to the sort \SortL. The two first constructs correspond to the constant zero and to the successor function, respectively. Sometimes we write $\s^i$ to abbreviate the application of the successor $i$ times. We define a set $\mathbb{L}$ which is closed under those two constructs. The operator $\cup$ returns the maximum of two type levels. The construct $l$ stands for a \emph{level variable} which will occur in universe polymorphic definitions.

We have that \Sortw\ is the unique sort of all the types of universe polymorphic functions. We can now describe the explicit subset of Typer as a Pure Type System \cite{barendregt}:

@@ -79,7 +79,7 @@ Because of the impredicativity of the erasable part of Typer, we need to define \subsection{ICC in Typer} Typer manipulates three separate kinds of terms to simplify both the writing and execution of programs. \emph{Explicit} terms are the usual expression that are written by the user and then executed. \emph{Implicit} terms are also used during execution, but Typer is able to infer them during elaboration such that they do not need to be written by the user. \emph{Erasable} terms are neither written by the user nor executed; they are inferred during elaboration, participate in type checking and are then erased before execution.

-The notation we adopt in this document is meant to both allow for the distinction between the three kinds of terms and to evoke actual Typer source code. Thus, the traditional explicit lambda term $\la(x:A).b$ will here be written $\la(x:A)\explicit b$ and similarly the product type $\Pi(x:A).B$ will be written $(x:A)\explicit B$. The type of arrow used will convey the kind of term being defined. Thus, compound terms of our calculus will all take one of the following forms: +\textbf{Notation:} The notation we adopt in this document is meant to both allow for the distinction between the three kinds of terms and to evoke actual Typer source code. The traditional explicit lambda term $\la(x:A).b$ will here be written $\la(x:A)\explicit b$ and similarly the product type $\Pi(x:A).B$ will be written $(x:A)\explicit B$. The type of arrow used will convey the kind of term being defined. Thus, compound terms of our calculus will all take one of the following forms:

\begin{center} \begin{tabular}[h]{rclll} @@ -378,56 +378,92 @@ Our definition of \CC\ is based on the original Calculus of Constructions (CC) \ \CC's PTS definition is shown in Figure X. The typing rules for \CC\ are shown in Figure X. The structure of the PTS is derived from Luo's own extention of CC (ECC) \cite{luo}, but the product rule of the form $(\Type_i, \Type_i, \Type_i)$ is replaced with $(\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, for example, Miquel's definition of \CC\ \cite{miquel}.

\subsection{Translation} -We introduce a translator operator \rew{\ } which is defined on all expressions of our syntax for \CC. We will consider a translation valid if for each context and each typing judgement of \CC, we have the following: -\begin{align} - \Ga \CCdash & ~~ \Rightarrow ~~ \rew{\Ga} ~ \ - \Ga \CCdash e:\tau & ~~ \Rightarrow ~~ \rew{\Ga} ~ \rew{e}:\rew{\tau} -\end{align} - -We will proceed by induction on typing derivation to show that each valid derivation of \CC\ translates to a valid derivation in the Typer system. For most typing rules, the proof is straightforward: we assume the translated type theoric premises by the induction hypothesis and and the translated set theoric premises by an injective map from \CC's to Typer's PTS; we then show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules. - -The correspondance between \CC's and Typer's PTS structures is first defined between the universe hierarchies $\rew{\ } : \S_{CC} \to \S$: +We introduce a translator operator \rew{\ } defined on contexts and terms of \CC: \begin{align*} - \rew{\Prop} ~~~ &= ~~~ \Type\ \mathsf{z} \ - \rew{\Type_1} ~~~ &= ~~~ \Type\ \mathsf{(s\ z)} \ - \rew{\Type_2} ~~~ &= ~~~ \Type\ \mathsf{(s\ (s\ z))} \ - \vdots~~~~~ ~~~ &= ~~~ ~~~~~~~\vdots + \rew{\cdot} &= \cdot & \rew{\Prop} &= \Type\ \z \ + \rew{\Ga,x:T} &= \rew{\Ga},x:\rew{T} & \rew{\Type_{i}} &= \Type\ (\s^{i}\ \z) \[-20pt] \end{align*} - -Then, axioms of $\A_{CC}$ translate to axioms of $\A$ by the translation of respective sorts, e.g. $\rew{(\Prop : \Type_1)} = (\rew{\Prop} : \rew{\Type_1}) = (\Type\ \mathsf{z} : \Type\ \mathsf{(s\ z)})$. We note that the mapping of axioms is injective because $\A$ has an axiom scheme structurally identical to $\A_{CC}$'s. - -Finally, rules in $\R_{CC}$ translate to rules either in $\R$ or $\R_e$, depending on whether they are predicative or impredicative. For example, consider the translation of the predicative rule \begin{align*} - \rew{(\Prop,\Type_1,\Type_1)} &= (\rew{\Prop},\rew{\Type_1},\rew{\Type_1}) \ - &= (\Type\ \z,\Type\ (\s\ \z),\Type\ (\s\ \z)) \in \R + \rew{\la(x:T)\explicit U} &= + \begin{cases} + \la(x : \rew{T}) \erasable \rew{U} &\text{if $(U:\tau)$, $(\tau : \Prop)$ and $(T:\Type_i)$}\ + \la(x : \rew{T}) \explicit \rew{U} &\text{otherwise} + \end{cases}\ + \rew{(x:T)\explicit U} &= + \begin{cases} + (x : \rew{T})\erasable \rew{U} &\text{if $(U: \Prop)$ and $(T:\Type_i)$}\ + (x : \rew{T})\explicit \rew{U} &\text{otherwise} + \end{cases}\ + \rew{M \ap N} &= + \begin{cases} + \rew{M}|||\rew{N} \todo \ + \rew{M}|\rew{N} \todo + \end{cases}\ \end{align*}

-and conversly, the translation of the impredicative rule -\begin{align*} - \rew{(\Type_1,\Prop,\Prop)} &= (\rew{\Type_1},\rew{\Prop},\rew{\Prop}) \ - &= (\Type\ (\s\ \z),\Type\ \z,\Type\ \z) \in \R_e. -\end{align*} -In general, if a product type of \CC\ has a domain of higher sort than its range, i.e. it is impredicative, then it can only be of form $(\Type_i,\Prop,\Prop)$ (see Figure 7). In all other cases, i.e. the predicative rules $(\Prop, \Type_i, \Type_i)$ and $(\Type_i, \Type_j, (\Type_i \cup \Type_j))$, the sort of the product type will be $s_3 = (s_1 \cup s_2)$.

-Thus, the translation of set theoric propositions is the following: -\begin{align*} - \rew{s \in \S_{CC}} &\leadsto\ \rew{s} \in \S \ - \rew{(s_1:s_2) \in \A_{CC}} &\leadsto\ (\rew{s_1}:\rew{s_2}) \in \A \ - \rew{(s_1,s_2,s_3) \in \R_{CC}} &\leadsto\ - \begin{cases} - (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e &\text{if $s_1 \neq \Prop$}\[-4pt] - & \text{and $s_2 = \Prop$}\ - (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R &\text{otherwise} - \end{cases} -\end{align*} +We will consider this translation valid if for each valid context and typing judgment of \CC, we get a valid contexts and typing judgments in Typer and vice versa: +\begin{align} + \Ga \CCdash & ~~ \iff ~~ \rew{\Ga} ~ \ + \Ga \CCdash e:\tau & ~~ \iff ~~ \rew{\Ga} ~ \rew{e}:\rew{\tau} +\end{align} + +We will proceed by 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. + +Before proceeding with the proof, we will show the following lemmas: + +\begin{lemma} + Each sort $s \in \S_{CC}$ of \CC\ has an distinct equivalent sort $\rew{s} \in \S$ in Typer; i.e. $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$. This translation is an injectie function, so we also have a unique $s$ for every $\rew{s}$ + \end{proof} +\end{lemma} + +\begin{lemma} + Every axiom $(s_1:s_2) \in \A_{CC}$ of \CC\ has a disctinct equivalent axiom $(\rew{s_1}:\rew{s_2}) \in \A$ in Typer; i.e. $(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))$ with $(\Type\ \z:\Type\ (\s\ \z)) \in A$. For $(\Type_i:\Type_{i+1})$, we know that for all $i$, we have + \begin{align*} + (\rew{\Type_i}:\rew{\Type_{i+1}}) &= (\Type\ (\s^i\ \z):\Type\ (\s^{i+1}\ \z))\ + &= (\Type\ (\s^i\ \z):\Type\ (\s\ (\s^i\ \z)) + \end{align*} +which corresponds to the axiom scheme $(\Type\ \l:\Type\ \s\ \l) ~ \forall \l\in\mathbb{L}$ considering that $(\s^i\ \z) \in \mathbb{L} ~ \forall i>0$ + \end{proof} +\end{lemma} +% Finally, rules in $\R_{CC}$ translate to rules either in $\R$ or $\R_e$, depending on whether they are predicative or impredicative. For example, consider the translation of the predicative rule +% \begin{align*} +% \rew{(\Prop,\Type_1,\Type_1)} &= (\rew{\Prop},\rew{\Type_1},\rew{\Type_1}) \ +% &= (\Type\ \z,\Type\ (\s\ \z),\Type\ (\s\ \z)) \in \R +% \end{align*} + +% and conversly, the translation of the impredicative rule +% \begin{align*} +% \rew{(\Type_1,\Prop,\Prop)} &= (\rew{\Type_1},\rew{\Prop},\rew{\Prop}) \ +% &= (\Type\ (\s\ \z),\Type\ \z,\Type\ \z) \in \R_e. +% \end{align*} +% In general, if a product type of \CC\ has a domain of higher sort than its codomain, i.e. it is impredicative, then it can only be of form $(\Type_i,\Prop,\Prop)$ (see Figure 7). In all other cases, i.e. the predicative rules $(\Prop, \Type_i, \Type_i)$ and $(\Type_i, \Type_j, (\Type_i \cup \Type_j))$, the sort of the product type will be $s_3 = (s_1 \cup s_2)$. + +% Thus, the translation of set theoric propositions is the following: +% \begin{align*} +% \rew{s \in \S_{CC}} &\leadsto\ \rew{s} \in \S \ +% \rew{(s_1:s_2) \in \A_{CC}} &\leadsto\ (\rew{s_1}:\rew{s_2}) \in \A \ +% \rew{(s_1,s_2,s_3) \in \R_{CC}} &\leadsto\ +% \begin{cases} +% (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e &\text{if $s_1 \neq \Prop$}\[-4pt] +% & \text{and $s_2 = \Prop$}\ +% (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R &\text{otherwise} +% \end{cases} +% \end{align*}

We define the translation on context recursively: \begin{align*} - \rew{\cdot} &\leadsto\ \cdot \ - \rew{\Ga, x:e} &\leadsto\ \rew{\Ga}, x:\rew{e} + \rew{\cdot} &= \cdot \ + \rew{\Ga, x:e} &= \rew{\Ga}, x:\rew{e} \end{align*}

-\underline{\textbf{Case 1:}} +We now proceed by case analysis on typing derivation steps to show that (1) and (2) hold: + +\underline{\textbf{CC-Wf-E:}} \begin{mathpar} \infer {\ } @@ -446,7 +482,7 @@ The translation is immediately true under Typer by rule \textsc{Wf-E}. \tag{Wf-E} \end{mathpar}

-\underline{\textbf{Case 2:}} +\underline{\textbf{CC-Wf-S:}} \begin{mathpar} \infer {\Ga \CCdash T:s \ s \in \S_{CC} \ x \notin \dv{\Ga}} @@ -457,16 +493,23 @@ By the induction hypothesis we can assume $$\rew{\Ga} ~ \rew{T}:\rew{s}$$

and we have that -$$\rew{s \in S_{CC}} \leadsto \rew{s} \in \S.$$ +$$s \in S_{CC} \iff \rew{s} \in \S.$$

We have yet to show that $$x \notin \dv{\rew{\Ga}}$$

+\begin{lemma} + We have the following equality: + $$\dv{\Ga} = \dv{\rew{\Ga}}$$ + \begin{proof} + By induction on the size of the context. The equality holds on the base case $\rew{\cdot} = \cdot$ since both the empty context and its translation have no declared varaibles. The equality holds on the recursive case $\rew{\Ga, x : T} = \rew{\Ga}, x : \rew{T}$ since the name of the declared variable is left unchanged. + \end{proof} +\end{lemma} \begin{lemma} The following holds: - $$x \notin \dv{\Ga} \Rightarrow x \notin \dv{\rew{\Ga}}$$ + $$x \notin \dv{\Ga} \iff x \notin \dv{\rew{\Ga}}$$ \begin{proof} - \todo + Follows directly from the previous lemma. \end{proof} \end{lemma} We can now infer the translation of the conclusion by rule @@ -477,7 +520,7 @@ We can now infer the translation of the conclusion by rule \tag{WF-S} \end{mathpar}

-\underline{\textbf{Case 3:}\} +\underline{\textbf{CC-Sort:}\} \begin{mathpar} \infer {\Ga \CCdash \ (s_1:s_2) \in \A_{CC}} @@ -488,7 +531,7 @@ By the induction hypothesis we can assume $$\rew{\Ga} ~$$

and we have that -$$\rew{(s_1:s_2) \in \A_{CC}} \leadsto (\rew{s_1}:\rew{s_2}) \in \A.$$ +$$(s_1:s_2) \in \A_{CC} \iff (\rew{s_1}:\rew{s_2}) \in \A.$$

We reach the translation of the conclusion by rule \begin{mathpar} @@ -498,7 +541,7 @@ We reach the translation of the conclusion by rule \tag{Sort} \end{mathpar}

-\underline{\textbf{Case 4:}\} +\underline{\textbf{CC-Var:}\} \begin{mathpar} \infer {\Ga \CCdash \ (x:T) \in \Ga} @@ -510,13 +553,13 @@ $$\rew{\Ga} ~$$

\begin{lemma} The following holds: - $$(x:T) \in \Ga \Rightarrow (x:\rew{T}) \in \rew{\Ga}$$ + $$(x:T) \in \Ga \iff (x:\rew{T}) \in \rew{\Ga}$$ \begin{proof} - If $\Ga = \cdot\ $, then the implication is true by the fact that the antecedant is false. Else, if $\Ga = \Delta, (x : T)$, then + By induction on the size of the context. The base case makes the proposition false on both sides. By lemma 3.3, the set of declared variables in a \CC\ context and in its translation are the same, so we must only show that they both have the appropriate types. It follows from the recursive definition of translation on contexts $\rew{\Ga, x : T} = \rew{\Ga}, x : \rew{T}$ that they do. \end{proof} \end{lemma}

-and reach the translation of the conclusion by rule +We reach the translation of the conclusion by rule \begin{mathpar} \infer {\rew{\Ga} ~ \ (x:\rew{T}) \in \rew{\Ga}} @@ -524,7 +567,7 @@ and reach the translation of the conclusion by rule \tag{Var} \end{mathpar}

-\underline{\textbf{Case 5:}\} +\underline{\textbf{CC-Prod:}\} \begin{mathpar} \infer {\Ga \CCdash T:s_1 \ \Ga, x:T \CCdash U:s_2 \ (s_1,s_2,s_3) \in \R_{CC}} @@ -539,7 +582,7 @@ We have the assumptions {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{s_2}} \end{mathpar} and we know that -$$\rew{(s_1,s_2,s_3) \in \R_{CC}} \leadsto (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$$ +$$(s_1,s_2,s_3) \in \R_{CC} \iff (\rew{s_1},\rew{s_2},\rew{s_3}) \in \R$$ from which we can conclude \begin{mathpar} \infer @@ -554,7 +597,7 @@ We have the assumptions {\rew{\Ga} ~ \rew{T}:\rew{\Type_i} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{\Prop}} \end{mathpar} and we know that -$$\rew{(\Type_i,\Prop,\Prop) \in \R_{CC}} \Rightarrow (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e$$ +$$(\Type_i,\Prop,\Prop) \in \R_{CC} \iff (\rew{\Type_i},\rew{\Prop},\rew{\Prop}) \in \R_e$$ from which we can conlcude \begin{mathpar} \infer @@ -563,17 +606,7 @@ from which we can conlcude \tag{E-Prod} \end{mathpar}

-\begin{remark} The only way to construct a product type in \CC\ is through the application of typing rule \textsc{CC-Prod}, so we know that all translations of product types will follow the rule: - \begin{align*} - \rew{(x:T)\explicit U} \leadsto - \begin{cases} - (x:\rew{T})\erasable \rew{U} & \text{if $(U:\Prop)$ and $(T:\Type_i)$} \ - (x:\rew{T})\explicit \rew{U} & \text{otherwise} - \end{cases} - \end{align*} -\end{remark} - -\underline{\textbf{Case 6:}\} +\underline{\textbf{CC-App:}\} \begin{mathpar} \infer {\Ga \CCdash M : (x:T) \explicit U \ \Ga \CCdash N:T} @@ -584,7 +617,7 @@ By the induction hypothesis we can 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}$ (see Remark 3.1): +And we again have two subcases to consider for the translation $\rew{(x:T) \explicit U}$:

\textbf{Predicative subcase:}\ \begin{mathpar} @@ -601,7 +634,7 @@ And we again have two subcases to consider for the translation $\rew{(x:T) \expl \tag{E-App} \end{mathpar}

-\underline{\textbf{Case 7:}\} +\underline{\textbf{CC-Lam:}\} \begin{mathpar} \infer {\Ga, x:T \CCdash M:U \ \Ga \CCdash (x:T) \explicit U : s} @@ -612,7 +645,7 @@ By the induction hypothesis we can assume \begin{mathpar} {\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U} \ \rew{\Ga} ~ \rew{(x:T) \explicit U} : \rew{s}} \end{mathpar} -And by Remark 3.1, we have two subcases to consider for the translation \rew{(x:T) \explicit U}: +We have two subcases to consider 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. @@ -623,7 +656,7 @@ The predicative product type translates to an explicit product type $(x:\rew{T}) \tag{X-Lam} \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 \Prop\ by Remark 3.1. We would expect to apply the erasable \textsc{E-Lam} typing rule to derive the typing of the erasable lambda abstraction, +The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ which necessarily has sort \Prop. We would expect to apply the erasable \textsc{E-Lam} typing rule to derive the typing of the erasable lambda abstraction, \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}^*}} @@ -633,22 +666,23 @@ The impredicative product type translates to an erasable product type $(x:\rew{T but we have yet to show that the additional premise $x \notin \fv{\rew{M}^*}$ of rule \textsc{E-Lam} holds in all cases.

\begin{lemma} - The following holds: \vspace{-5mm} + If + $$\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U}$$ + and + $$\rew{\Ga} ~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop}$$ + then the following always holds + $$x \notin \fv{\rew{M}^*}$$ \end{lemma} -\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}^*}} - \tag{L1} -\end{mathpar} + \begin{proof} - Because we have a well typed erasable product type which can only be constructed by means of rule \textsc{E-Prod}, we can assume under the induction hypothesis that $T:\Type_i$ and that $U:\Prop$. With those additional assumptions, we will show that $x \notin \fv{\rew{M}^*}$ by case analysis on $\rew{M}$. - \begin{align*} - s^* &= s & x^* &= x \[5pt] - (\la(x:T)\explicit U)^* &= \la(x)\explicit U^* & ((x:T)\explicit U)^* &= (x:T^*)\explicit U^* \ - (\la(x:T)\erasable U)^* &= U^* & ((x:T)\erasable U)^* &= \forall(x:T^*).U^* \[5pt] - (M \ap N)^* &= M^*\ap N^* & (M \appp N)^* &= M^* - \end{align*} + \todo + % Because we have a well typed erasable product type which can only be constructed by means of rule \textsc{E-Prod}, we can assume under the induction hypothesis that $T:\Type_i$ and that $U:\Prop$. With those additional assumptions, we will show that $x \notin \fv{\rew{M}^*}$ by case analysis on $\rew{M}$. + % \begin{align*} + % s^* &= s & x^* &= x \[5pt] + % (\la(x:T)\explicit U)^* &= \la(x)\explicit U^* & ((x:T)\explicit U)^* &= (x:T^*)\explicit U^* \ + % (\la(x:T)\erasable U)^* &= U^* & ((x:T)\erasable U)^* &= \forall(x:T^*).U^* \[5pt] + % (M \ap N)^* &= M^*\ap N^* & (M \appp N)^* &= M^* + % \end{align*} \end{proof}

View it on GitLab: https://gitlab.com/monnier/typer/compare/2eb3b21039b42625aefadf9dece27105959...