[Git][monnier/typer][bosn] Rewrite a valid proof of lem:E-Lam-FV; start proof of soundness of translation;… - Typer

30 Aoû 2018


      Nathaniel pushed to branch bosn at Stefan / Typer
Commits:
89aecbb1 by nbos at 2018-08-30T09:05:45Z
Rewrite a valid proof of lem:E-Lam-FV; start proof of soundness of translation; expand on guarded by destructors predicate D
- - - - -
1 changed file:
- doc/formal/typer_theory.tex
Changes:
=====================================
doc/formal/typer_theory.tex
=====================================
@@ -25,8 +25,8 @@ The gist of the theory behind Typer is Coquand and Huet's Calculus of Constructi
 \begin{itemize}
   \renewcommand{\labelitemi}{$-$}
   \setlength\itemsep{-3pt}
-\item An infinite hierarchy of predicative type universes inspired by Luo's Extended Calculus of Constructions (ECC) \cite{luo} without cumulativity;
-\item A parallel hierarchy of impredicative universes
+\item An infinite hierarchy of type universes inspired by Luo's Extended Calculus of Constructions (ECC) \cite{luo} without cumulativity;
+\item Product rules that allow for both predicative and impredicative arguments and abstractions in every universe;
 \item Universe polymorphism allowing the parametrization of type universes;
 \item Erasure of propositional arguments with decidable type checking from Barras and Bernardo's variant of Miquel's Implicit Calculus of Constructions (ICC) \cite{bruno}\cite{miquel};
 \item Inductive definitions as presented by Gim'enez in \cite{gimenez}.
@@ -99,7 +99,7 @@ After elaboration, implicit terms behave exactly like explicit terms so we will
   \caption{Extraction function $M \mapsto M^*$}
   \label{fig:*}
 \end{figure}
-We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure \ref{fig:*}. It erases domains of abstraction, erasable abstractions and erasable applications and turns erasable products into a propositional form. The typing rules for Typer are shown in figure \ref{fig:Typing-rules}. They are the standard rules of a Church-style lambda calculus, duplicated for both kinds of terms.
+We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure \ref{fig:*}. It erases domains of abstraction, erasable abstractions and erasable applications and turns erasable products into a propositional form. The typing rules shown in figure \ref{fig:Typing-rules} are the rules from Barras and Bernardo's ICC \cite{bruno}.
\begin{figure}[h]
   \ \ \ \  \fbox{
@@ -158,7 +158,7 @@ We define an extractions function $M \mapsto M^*$ (as in \cite{bruno}) in figure
       \
     \end{mathpar}
   }
-  \caption{Typer's Typing Rules}
+  \caption{Typer's Typing Rules from ICC}
   \label{fig:Typing-rules}
 \end{figure}
@@ -226,9 +226,9 @@ The typing rules for inductive definitions and case analysis are presented in fi
         %% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l
         %% Eq_refl : ((x : ?t) ≡> Eq x x);
         %% Eq_cast : (x : ?t) ≡> (y : ?t)
-        %% ≡> (p : Eq x y)
-        %% ≡> (f : ?t -> ?t')
-        %% ≡> f x -> f y;
+        %% .                  ≡> (p : Eq x y)
+        %% .                  ≡> (f : ?t -> ?t')
+        %% .                  ≡> f x -> f y;
         %% 
         %% At run-time `Eq_cast` will be a no-op (i.e. `Eq_cast x` will reduce
         %% to `x`), but there is no corresponding normalization rule applied
@@ -279,16 +279,18 @@ Recursion is specified through the use of a recursive operator \Letrec \todo
   A \emph{recursive position} in the term $(\vec{x}:\vec{M}) (X \vec{N})$ where $X$ is restricted to strictly positive occurrences, is a number $i \in |\vec{M}|$ such that $X$ appears in term $M_i$. We abbreviate this property as $RP{i,C}$ where $C \equiv (\vec{x}:\vec{M}) (X \vec{N})$.
 \end{definition}
 \begin{definition}
-  The \emph{guarded by destructors} condition is written as the predicate $\D_\V{f,k,x,M}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which represent the recursive components of $x$ in $M$. Below, we write $\D_\V{M}$ for brevity, but $f$, $k$ and $x$ remain bound to their presence in full predicate $\D_\V{f,k,x,M}$. We also write $\D_\V{\vec{M}}$ instead of $\bigwedge_i \D_\V{M_i}$. The condition $\D_\V{M} = \D_\V{f,k,x,M}$ is determined by structural induction on term $M$:
+  The \emph{guarded by destructors} condition is written as the predicate $\D_\V{f,k,x,M}$ where $k$ is a positive integer, $M$ is a term, $f$ and $x$ are identifiers, and $\V$ is a set of identifiers which represent the recursive components of $x$ in $M$. Below, we write $\D_\V{M}$ for brevity instead of the full $\D_\V{f,k,x,M}$. We also write $\D_\V{\vec{M}}$ instead of $\bigwedge_i \D_\V{M_i}$. By structural induction on term $M$, we describe when $\D_\V{M} = \D_\V{f,k,x,M}$ is true by assigning conjunctions of necessary conditions to each form of $M$:
   \begin{align*}
-    \D_\V{M} && = && \text{True} && \text{if } f \notin \fv{M}\
-    \D_\V{\la (z:P)\to Q} && = && \D_\V{P} \land \D_\V{Q} \
-    \D_\V{(z:P)\to Q} && = && \D_\V{P} \land \D_\V{Q} \
-    \D_\V{\Letrec ?} && = && \ ? \
-    \D_\V{\Ind(X:A)<\vec{C}>} && = && \D_\V{A} \land \D_\V{\vec{C}} \
-    \D_\V{f \vec{P}} && = && (|\vec{P}| > k) \land (P_{k+1} \equiv (z\vec{Q}) \land \D_\V{\vec{P}} \
-    \D_\V{\Case\ N:S \text{ of } <\vec{G}>} \todo\ 
-    \D_\V{N \vec{P}} \todo\
+    \D_\V{M} & = \text{True} & \text{if } f \notin \fv{M}\
+    \D_\V{\la (z:P)\to Q} & = \D_\V{P} \land \D_\V{Q} \
+    \D_\V{(z:P)\to Q} & = \D_\V{P} \land \D_\V{Q} \
+    \D_\V{\Letrec ?} & = \ ? \
+    \D_\V{\Ind(X:A)<\vec{C}>} & = \D_\V{A} \land \D_\V{\vec{C}} \
+    \D_\V{f \vec{P}} & = (|\vec{P}| > k) \land (P_{k+1} \equiv (z\ \vec{Q})) \land \D_\V{\vec{P}} & \text{with $z \in \V$}\
+    \D_\V{N \vec{P}} & = \D_\V{N} \land \D_\V{\vec{P}} &\text{if $N \neq f$}\
+    \D_\V{\Case\ (z\ \vec{P}):S \text{ of } <\vec{G}>} & = \D_\V{Q} \land \D_\V{S} \land \D_\V{\vec{P}} &\text{with $z \in \V \cup {x}$}\
+               & \quad \land S \equiv I\vec{R} & \text{with }I =\Ind (X:A)<\vec{C}> \
+    & \quad \land \text{if } 
   \end{align*}
 \end{definition}
@@ -388,7 +390,7 @@ In this section we will show that the erasable terms of Typer allows for a repre
Our definition of \CC\ is based on the original Calculus of Constructions (CC) \cite{CC}, to which we add an infinite hierarchy of predicative universes above an impredicative \Prop. Thus we have: $$\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_{\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\ might therefore behave differently than other definitions of \CC\ (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}, where 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\ might therefore behave differently than other definitions of \CC\ (for example \cite{miquel}).
\subsection{Translation}
 \begin{figure}[h]
@@ -412,7 +414,7 @@ Our definition of \CC\ is based on the original Calculus of Constructions (CC) \
                                  \end{cases}\
         \rew{M \ap N} &=
                         \begin{cases}
-                          \rew{M}|||\rew{N} &\text{if $(M:\tau:\Prop)$ and $(T:\tau':\Type_i)$} \ 
+                          \rew{M}|||\rew{N} &\text{if $(M:\tau:\Prop)$ and $(N:\tau':\Type_i)$} \ 
                           \rew{M}|\rew{N}  &\text{otherwise}
                         \end{cases}\
         \rew{U{N/x}} &= \rew{U}{\rew{N}/x}\
@@ -434,7 +436,7 @@ The translator operator \rew{_} is defined on contexts and terms of \CC. We exp
   \end{align*}
 \end{theorem}
-Before proving the correctness of the equality, we need the following lemmas:
+Before proving the correctness of the equality, we show the following lemmas:
 \begin{lemma}
   \label{lem:S-equiv}
   $s \in \S_{CC} \iff \rew{s} \in \S$
@@ -517,6 +519,222 @@ Before proving the correctness of the equality, we need the following lemmas:
   \end{proof}
 \end{lemma}
+\begin{lemma}
+  \label{lem:E-Lam-FV}
+  If we have
+  \begin{mathpar}
+    % Induction on derivations in CCω is used because induction on
+    % derivations of translated terms in Typer can lead to a case
+    % (e.g. X-App) where it is possible to insert a term absent in CCω
+    % (e.g. an explicit abstraction of a higher sort over a body of sort
+    % Type z) in the derivation tree, thus allowing variable 'y' to appear
+    % free in the term
+
+    % So instead of using this lemma (in completeness, case:E-Lam) with the
+    % translated premises, we can use it with the initial (CCω) ones
+    {\Ga, y:V \CCdash P:W \ \Ga, y:V \CCdash  W : \Prop \ \Ga \CCdash V : \Type_i}
+  \end{mathpar}
+  then the following always holds
+  $$y \notin \fv{\rew{P}^*}$$
+
+  \begin{proof}
+    By induction on the typing derivation $\Ga, y:V \CCdash P:W$, either a typing rule is not applicable to this derivation or we show that it satisfies $y \notin \fv{\rew{P}^*}$.
+
+    \textbf{CC-Sort:}\
+    \begin{mathpar}
+      \infer
+      {\Ga \CCdash \ (s_1:s_2) \in \A_{CC}}
+      {\Ga \CCdash s_1:s_2}
+      \tag{CC-Sort}
+    \end{mathpar}
+    All axioms of $\A_{CC}$ are constructed with sorts $s_1, s_2 \in \S_{CC}$. There are no sorts in $\S_{CC}$ smaller than $\Prop$. Since here $s_2$ is $W$ and by assuption $W : \Prop$, then no axiom $(s_1:s_2) \in \A_{CC}$ will match $(P:W)$ and this typing rule cannot apply.
+    
+    \textbf{CC-Var:}\
+    \begin{mathpar}
+      \infer
+      {\Ga \CCdash \ (x:T) \in \Ga} 
+      {\Ga \CCdash x:T}
+      \tag{CC-Var}
+    \end{mathpar}
+    Considering that typing judgments are introduced in contexts exclusively by means of rule \textsc{CC-Wf-S}, we can assume
+    \begin{mathpar}
+      {\Ga \CCdash T:s \ s \in \S_{CC} \ x \notin \dv{\Ga}}
+    \end{mathpar}
+    which all holds by the assignment $s = \Prop$. Thus, $P$ (here $x$) is a variable. The translation and extraction for the variable leaves it untouched
+    $$\rew{P}^* = P^* = P$$
+    Because $y : V : \Type_i$ and $P : W : \Prop$, we have that $y \neq P$ because they are variables that inhabit different universes so it follows that $y \notin \fv{P}$.
+    
+    \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}}
+      {\Ga \CCdash (x:T) \explicit U : \s_3}
+      \tag{CC-Prod}
+    \end{mathpar}
+    Similarly to case \textsc{CC-Sort}, we cannot apply this rule because here $s_3 = W$ and by assumption $W : \Prop$ and \Prop\ is the smallest universe in $\S_{CC}$. So no rule $(s_1,s_2,s_3) \in \R_{CC}$ can match in this case.
+    
+    \textbf{CC-Lam:}\
+    \begin{mathpar}
+      \infer
+      {\Ga, x:T \CCdash M:U \ \Ga \CCdash (x:T) \explicit U : s}
+      {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U}
+      \tag{CC-Lam}
+    \end{mathpar}
+    Sort $s$ here is $\Prop$ because $(x:T) \explicit U$ is $W$ and by assumption $W : \Prop$. The construction of $(x:T) \explicit U$ reveals that $U : \Prop$ because every rule $(s_1,s_2,s_3) \in \R_{CC}$ that has $s_3 = \Prop$ also has $s_2 = \Prop$:
+    \begin{mathpar}
+      \infer
+      {\Ga \CCdash T:s_1 \ \Ga, x:T \CCdash U:\Prop \ (s_1,\Prop,\Prop) \in \R_{CC}}
+      {\Ga \CCdash (x:T) \explicit U : \Prop}
+      \tag{CC-Prod}
+    \end{mathpar}
+    The translation for the lambda abstraction $\la(x:T) \explicit M$ has a predicative and impredicative case. In both cases, however, the extraction erases the type annotation $\rew{T}$. Therefore $\fv{\rew{P}^*} = \fv{\rew{M}^*}$ and $y \notin \fv{\rew{M}^*}$ holds by the induction hypothesis because $M : U : \Prop$.
+    
+    \textbf{CC-App:}\
+    \begin{mathpar}
+      \infer
+      {\Ga \CCdash M : (x:T) \explicit U \ \Ga \CCdash N:T}
+      {\Ga \CCdash M|N : U{N/x}}
+      \tag{CC-App}
+    \end{mathpar}
+    Here $P = M|N$ and $W = U{N/x}$. $y \notin \fv{\rew{P}^*}$ will hold if we can show that $y \notin \fv{\rew{M}^*}$ and---unless $N$ is an impredicative argument---$y \notin \fv{\rew{N}^*}$. By assumption $U{N/x} : \Prop$
+    %% Does this step really hold?
+    and therefore also $U : \Prop$. It follows that $(x:T)\explicit U : \Prop$ by the typing rule \textsc{CC-Prod}. Thus, by induction hypothesis, we have $y \notin \fv{\rew{M}^*}$ because $M : (x:T)\explicit U : \Prop$. If $N : T : \Prop$, then we can also apply the induction hypothesis. Otherwise, the extraction on the translation erases the impredicative argument completely.
+
+  \end{proof}
+
+  %% **PURGATORY** ATTEMPTED PROOF ON TYPER DERIVATIONS
+  %\textbf{Sort:}\
+  % \begin{mathpar}
+  %   \infer
+  %   {\rew{\Ga, y:V} ~ \ (\rew{s_1}:\rew{s_2}) \in \A}
+  %   {\rew{\Ga, y:V} ~ \rew{s_1}:\rew{s_2}}
+  %   \tag{Sort}
+  % \end{mathpar}
+  % \textsc{Sort} is not applicable to this derivation because $\rew{W}$ is set to have sort $\Type\ \z$ but there is no sort $\rew{s_2}$ that has sort $\Type\ \z$ because it is itself the smallest sort.
+  
+  % \textbf{Var:}\
+  % \begin{mathpar}
+  %   \infer
+  %   {\rew{\Ga, y:V} ~ \ (x:\rew{T}) \in \rew{\Ga, y:V}} 
+  %   {\rew{\Ga, y:V} ~ x:\rew{T}}
+  %   \tag{Var}
+  % \end{mathpar}
+  % It is not possible that $x = y$ because that would imply that their types satisfy $\rew{T} = \rew{V}$ (i.e. $\rew{W} = \rew{V}$) and, further, that their unverses satisfy $\Type\ (\s\ \l) = \Type\ \z$ which is false. Then, $x \neq y$ and we have that  $$y \notin \fv{x^*} ~~ \equiv ~~ y \notin \fv{x}$$ because $x$ and $y$ are different variables.
+  
+  % \textbf{X-Prod & E-Prod:}\
+  % Both \textsc{X-Prod} and \textsc{E-Prod} do not apply because both would set $\rew{W}$ to be a sort:
+  % $${\rew{\Ga, y:V} ~ (x:\rew{T}) \explicit \rew{U} : \rew{s_3}}$$
+  % $$\rew{\Ga, y:V} ~ (x:\rew{T}) \erasable \rew{U} : \rew{\Prop}$$
+  
+  % but $\rew{W} : \Type\ \z$ and there is no sort that has sort $\Type\ \z$, because it is the smallest sort.
+  
+  % \textbf{X-Lam:}\
+  % \begin{mathpar}
+  %   \infer
+  %   {\rew{\Ga, y:V, x:T} ~ \rew{M}:\rew{U} \ \rew{\Ga, y:V} ~ (x:\rew{T}) \explicit \rew{U} : s}
+  %   {\rew{\Ga, y:V} ~ \la(x:\rew{T}) \explicit \rew{M} : (x:\rew{T}) \explicit \rew{U}}
+  %   \tag{X-Lam}
+  % \end{mathpar}
+
+  % We know that $s = \Type\ \z$ because here $\rew{W} = (x:\rew{T})\explicit \rew{U}$ and by assumption $\rew{W} : \Type\ \z$. By the construction of the explicit product $(x:\rew{T}) \explicit \rew{U}$, we have
+  % \begin{mathpar}
+  %   \infer
+  %   {\rew{\Ga, y:V} ~ \rew{T}:s_1 \ \rew{\Ga, y:V, x:T} ~ \rew{U}:s_2 \ (s_1,s_2,\Type\ \z) \in \R}
+  %   {\rew{\Ga, y:V} ~ (x:\rew{T}) \explicit \rew{U} : \Type\ \z}
+  %   \tag{X-Prod}
+  % \end{mathpar}
+  % The only rule in $\R$ that matches $(s_1,s_2,\Type\ \z)$ is $(\Type\ \z, \Type\ \z, \Type\ \z)$ where, in particular, $s_2 = \Type\ \z$ and therefore $\rew{U} : \Type\ \z$. The extraction $\rew{P}^*$ here is:
+  % $$(\la(x:\rew{T}) \explicit \rew{M})^* = \la (x) \explicit \rew{M}^*$$
+  % Therefore,
+  % $$\fv{(\la(x:\rew{T}) \explicit \rew{M})^*} = \fv{\rew{M}^*}$$
+  % And we have
+  % \begin{mathpar}
+  %   {\rew{\Ga, y:V, x:T} ~ \rew{M}:\rew{U} \ \rew{\Ga, y:V} ~ \rew{U} : \Type\ \z}
+  % \end{mathpar}
+  % so by the induction hypothesis, we can assume
+  % $$y \notin \fv{\rew{M}^*}$$
+
+  % \textbf{E-Lam:}\
+  % \begin{mathpar}
+  %   \infer
+  %   {\rew{\Ga, y:V, x:T} ~ \rew{M}:\rew{U} \ \rew{\Ga, y:V} ~ (x:\rew{T}) \erasable \rew{U} : s \ x \notin \fv{\rew{M}^*}}
+  %   {\rew{\Ga, y:V} ~ \la(x:\rew{T}) \erasable \rew{M} : (x:\rew{T}) \erasable \rew{U}}
+  %   \tag{E-Lam}
+  % \end{mathpar}
+  
+  % Similarly, here we know that $s = \Type\ \z$ because $\rew{W} : \Type\ \z$. By the construction of the erasable product $(x:\rew{T}) \erasable \rew{U}$, we have
+  % \begin{mathpar}
+  %   \infer
+  %   {\rew{\Ga, y:V} ~ \rew{T}:s_1 \ \rew{\Ga, y:V, x:T} ~ \rew{U}:\Type\ \z \ (s_1,\Type\ \z,\Type\ \z) \in \R_e}
+  %   {\rew{\Ga, y:V} ~ (x:\rew{T}) \erasable \rew{U} : \Type\ \z}
+  %   \tag{E-Prod}
+  % \end{mathpar}
+  % The extraction is
+  % $$(\la(x:\rew{T}) \erasable \rew{M})^* = \la (x) \erasable \rew{M}^*$$
+  % Therefore,
+  % $$\fv{(\la(x:\rew{T}) \erasable \rew{M})^*} = \fv{\rew{M}^*}$$
+  % And we have
+  % \begin{mathpar}
+  %   {\rew{\Ga, y:V, x:T} ~ \rew{M}:\rew{U} \ \rew{\Ga, y:V} ~ \rew{U} : \Type\ \z}
+  % \end{mathpar}
+  % so by the induction hypothesis, we can assume
+  % $$y \notin \fv{\rew{M}^*}$$
+  
+  % \textbf{X-App:}\
+  % \begin{mathpar}
+  %   \infer
+  %   {\rew{\Ga, y:V} ~ \rew{M} : (x:T) \explicit \rew{U} \ \rew{\Ga, y:V} ~ \rew{N}:T}
+  %   {\rew{\Ga, y:V} ~ \rew{M}|\rew{N} : \rew{U}{\rew{N}/x}}
+  %   \tag{X-App}
+  % \end{mathpar}
+  % We know that $\rew{U}{\rew{N}/x} : \Type\ \z$ because here $\rew{W} = \rew{U}{\rew{N}/x}$ and by assumption $\rew{W} : \Type\ \z$.
+  %     %% FIXME: Does the next sentence really hold?
+  % Because $\rew{U}{\rew{N}/x} : \Type\ \z$, we also have $\rew{U} : \Type\ \z$. By the construction of the explicit product, we have
+  % \begin{mathpar}
+  %   \infer
+  %   {\rew{\Ga, y:V} ~ T:s_1 \ \rew{\Ga, y:V}, x:T ~ \rew{U}:\Type\ \z \ (s_1,\Type\ \z,s_3) \in \R}
+  %   {\rew{\Ga, y:V} ~ (x:T) \explicit \rew{U} : s_3}
+  %   \tag{X-Prod}
+  % \end{mathpar}
+  % The only rule in $\R$ that matches $(s_1,\Type\ \z,s_3)$ is $(\Type\ \z, \Type\ \z, \Type\ \z)$ where, in particular, $\rew{U} : \Type\ \z$.
+  
+  % Because $\rew{M}|\rew{N}$ is a translated term $\rew{P} = \rew{M|N}$ whose translation is not an erasable application, by the definition of the translation (figure \ref{fig:[]}):
+  % \begin{align*}
+  %   \rew{M \ap N} &=
+  %   \begin{cases}
+  %     \rew{M}|||\rew{N} &\text{if $(M:\tau:\Prop)$ and $(N:\tau':\Type_i)$} \ 
+  %     \rew{M}|\rew{N}  &\text{otherwise}
+  %   \end{cases}
+  % \end{align*}
+  % we infer that either $M$ has a type of a sort other than $\Prop$ or $N$ has a type of sort \Prop. We know that
+  % \begin{align*}
+  %   sssss      
+  % \end{align*}
+
+
+  % The extraction $\rew{P}^*$ here is:
+  % $$(\la(x:\rew{T}) \explicit \rew{M})^* = \la (x) \explicit \rew{M}^*$$
+  % Therefore,
+  % $$\fv{(\la(x:\rew{T}) \explicit \rew{M})^*} = \fv{\rew{M}^*}$$
+  % And we have
+  % \begin{mathpar}
+  %   {\rew{\Ga, y:V, x:T} ~ \rew{M}:\rew{U} \ \rew{\Ga, y:V} ~ \rew{U} : \Type\ \z}
+  % \end{mathpar}
+  % so by the induction hypothesis, we can assume
+  % $$y \notin \fv{\rew{M}^*}$$
+
+
+  % \textbf{E-App:}\
+  % \begin{mathpar}
+  %   \infer
+  %   {\rew{\Ga, y:V} ~ \rew{M} : (x:\rew{T}) \erasable \rew{U} \ \rew{\Ga, y:V} ~ \rew{N}:\rew{T}}
+  %   {\rew{\Ga, y:V} ~ \rew{M}|||\rew{N} : \rew{U}{\rew{N}/x}}
+  %   \tag{E-App}
+  % \end{mathpar}
+  
+  % \end{proof}
+  
+\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.
@@ -608,6 +826,7 @@ By the induction hypothesis we can assume
 $$\rew{\Ga} ~$$
\begin{lemma}
+  \label{lem:in-ctx-equiv}
   The following holds:
   $$(x:T) \in \Ga \iff (x:\rew{T}) \in \rew{\Ga}$$
   \begin{proof}
@@ -685,70 +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$. To apply the corresponding Typer rule \textsc{E-Lam}, we must first show that $x \notin \fv{\rew{M}^*}$.
-
-\begin{lemma}
-  \label{lem:E-Lam-FV}
-  If we have
-  \begin{mathpar}
-    %% 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{\rew{M}^*}$$
-
-  \begin{proof}\ \
-    By structural induction on $\rew{M}^*$:
-    
-    \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} $\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$ .
-
-    %% 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*(\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} $\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}
-
-By lemma \ref{lem:E-Lam-FV} above, we can infer
-$$x \notin \fv{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} = \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:
 \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}^*}}
@@ -807,13 +963,22 @@ 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}:\rew{s} \ \rew{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
+\begin{mathpar}
+  {\Ga \CCdash T:s'}
+\end{mathpar}
+by the induction hypothesis, since $s = \rew{s'}$. Finally,
+\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}:
 \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}
@@ -825,6 +990,11 @@ The original judgment is immediately true in \CC\ by rule \textsc{CC-Wf-E}
   {\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
+\begin{mathpar}
+  {\Ga \CCdash}
+\end{mathpar}
+by the induction hypothesis. Therefore we have the rule:
 \begin{mathpar}
   \infer
   {\Ga \CCdash \ (s_1:s_2) \in \A_{CC}}
@@ -839,6 +1009,11 @@ The original judgment is immediately true in \CC\ by rule \textsc{CC-Wf-E}
   {\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
+\begin{mathpar}
+  \Ga \CCdash
+\end{mathpar}
+by the induction hypothesis. We get:
 \begin{mathpar}
   \infer
   {\Ga \CCdash \ (x:T) \in \Ga} 
@@ -847,17 +1022,18 @@ The original judgment is immediately true in \CC\ by rule \textsc{CC-Wf-E}
 \end{mathpar}
\underline{\textbf{X-Prod:}}\
-Where $s_1 \neq \Type_1$ or $s_2 \neq \Prop$:
+Where $s_1 \neq \Type_i$ or $s_2 \neq \Prop$:
 \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}
-  {\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
 \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}
@@ -870,7 +1046,7 @@ Where $s_1 \neq \Type_1$ or $s_2 \neq \Prop$:
 \end{mathpar}
 \begin{mathpar}
   \infer
-  {\Ga \CCdash T:\Type_1 \ \Ga, x:T \CCdash U:\Prop \ (\Type_i,\Prop,\Prop) \in \R_{CC}}
+  {\Ga \CCdash T:\Type_i \ \Ga, x:T \CCdash U:\Prop \ (\Type_i,\Prop,\Prop) \in \R_{CC}}
   {\Ga \CCdash (x:T) \explicit U : \Prop}
   \tag{CC-Prod}
 \end{mathpar}
@@ -973,6 +1149,8 @@ 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:
View it on GitLab: https://gitlab.com/monnier/typer/commit/89aecbb1547ea6467c0f8e84d2f288bbaa29...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/commit/89aecbb1547ea6467c0f8e84d2f288bbaa29...
You're receiving this email because of your account on gitlab.com.



    