[Git][monnier/typer][bosn] 2 commits: Populate soundness proof with typing rules; rephrase some sentences to be… - Typer

17 Aoû 2018


      Nathaniel pushed to branch bosn at Stefan / Typer
Commits:
1ee31754 by nbos at 2018-08-16T18:02:55Z
Populate soundness proof with typing rules; rephrase some sentences to be impersonal; add substitution in definition of translation
- - - - -
5bfe76e4 by nbos at 2018-08-17T21:55:44Z
Add &#39;pack&#39; as an example
- - - - -
1 changed file:
- doc/formal/typer_theory.tex
Changes:
=====================================
doc/formal/typer_theory.tex
=====================================
@@ -423,6 +423,9 @@ Our definition of \CC\ is based on the original Calculus of Constructions (CC) \
                           \rew{M}|||\rew{N} &\text{if $(M:\tau:\Prop)$ and $(T:\tau':\Type_i)$} \ 
                           \rew{M}|\rew{N}  &\text{otherwise}
                         \end{cases}\
+        \rew{U{N/x}} &= \rew{U}{\rew{N}/x}\
+        % FIXME: Is substitution relevent here? Is it part of the syntax or
+        % meta-syntax?
       \end{align*}
     \end{minipage}
   }
@@ -545,7 +548,7 @@ Before proving the correctness of the equality, we will need the following lemma
   $$x \notin \fv{M^*}$$
\begin{proof}\ \
-    By structural induction, for every term of the codomain of the extraction function (see figure \ref{fig:*}), we either show that $M^*$ cannot be equal to it, or that $x$ cannot be free in it, thus showing that $x \notin \fv{M^*}$. First, we show how some terms cannot be $M^*$:
+    By structural induction on extracted terms (see figure \ref{fig:*}), either $M^*$ cannot be equal to it, or $x$ cannot be free within it, thus showing that $x \notin \fv{M^*}$. First, some terms that cannot be $M^*$:
%% 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*).  
@@ -555,7 +558,7 @@ Before proving the correctness of the equality, we will need the following lemma
     \underline{\textbf{Case}} $M^* = ((x:t)\explicit V)^*$ or $((x:t)\erasable V)^*$:\
     $M$ cannot be a product type since it inhabits the type $\Type\ \z$ which is our smallest universe so we cannot have a type two levels down.
-    Now for the cases where we can prove that $x$ is not free in the extraction of $M$:
+    Now for the cases where $x$ is not free in the extraction of $M$:
\underline{\textbf{Case}} $M^* = (s)^*$ with $s \in \S$:\
     %% FIXME: More specifically, the sorts `s` are (closed) constants.
@@ -590,7 +593,7 @@ Before proving the correctness of the equality, we will need the following lemma
 \end{lemma}
\subsection{Completeness of translation}
-We 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.
+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.
\underline{\textbf{CC-Wf-E:}}
 \begin{mathpar}
@@ -733,34 +736,6 @@ from which we can conclude
   \tag{E-Prod}
 \end{mathpar}
-\underline{\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}
-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}$:
-
-\textbf{Predicative subcase:}\
-\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}
-\textbf{Impredicative subcase:}\
-\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}
-
 \underline{\textbf{CC-Lam:}}\
 \begin{mathpar}
   \infer
@@ -782,6 +757,7 @@ The predicative product type translates to an explicit product type $(x:\rew{T})
   {\rew{\Ga} ~ \la(x:\rew{T}) \explicit \rew{M} : (x:\rew{T}) \explicit \rew{U}}
   \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 $\rew{\Prop} = \Type\ \z$. We can appeal to lemma \ref{lem:E-Lam-FV} which states that if we have
 \begin{mathpar}
@@ -798,93 +774,189 @@ and we have the sufficient premises to apply rule \textsc{E-Lam} and we obtain t
   \tag{E-Lam}
 \end{mathpar}
+\underline{\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}
+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}$:
+
+\textbf{Predicative subcase:}\
+\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}
+\textbf{Impredicative subcase:}\
+\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}
+
 \subsection{Soundness of translation}
-By structural induction on typing derivation, we show that, as per theorem \ref{thm:correctness-translation}, each valid derivation in the Typer system translates to a valid derivation of \CC\ ($\Leftarrow$). 
+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.
\underline{\textbf{Wf-E:}}\
 \begin{mathpar}
   \infer
   {\ }
-  {\emptyctx ~}
-  \textsc{ (Wf-E)}
+  {\rew{\cdot} ~}
+  \tag{Wf-E}
+\end{mathpar}
+
+The original judgment is immediately true in \CC\ by rule \textsc{CC-Wf-E}
+
+\begin{mathpar}
+  \infer
+  {\ }
+  {\emptyctx \CCdash}
+  \tag{CC-Wf-E}
 \end{mathpar}
\underline{\textbf{Wf-S:}}\
 \begin{mathpar}
   \infer
-  {\Ga ~ T:s \ s \in \S \ x \notin \dv{\Ga}}
-  {\Ga , x:T ~}
-  \textsc{ (Wf-S)}
+  {\rew{\Ga} ~ \rew{T}:\rew{s} \ \rew{s} \in \S \ x \notin \dv{\rew{\Ga}}}
+  {\rew{\Ga} , x:\rew{T} ~}
+  \tag{WF-S}
+\end{mathpar}
+\begin{mathpar}
+  \infer
+  {\Ga \CCdash T:s \ s \in \S_{CC} \ x \notin \dv{\Ga}}
+  {\Ga , x:T \CCdash}
+  \tag{CC-Wf-S}
 \end{mathpar}
\underline{\textbf{Sort:}}\
 \begin{mathpar}
   \infer
-  {\Ga ~ \ (s_1:s_2) \in \A}
-  {\Ga ~ s_1:s_2}
-  \textsc{ (Sort)}
+  {\rew{\Ga} ~ \ (\rew{s_1}:\rew{s_2}) \in \A}
+  {\rew{\Ga} ~ \rew{s_1}:\rew{s_2}}
+  \tag{Sort}
+\end{mathpar}
+\begin{mathpar}
+  \infer
+  {\Ga \CCdash \ (s_1:s_2) \in \A_{CC}}
+  {\Ga \CCdash s_1:s_2}
+  \tag{CC-Sort}
 \end{mathpar}
\underline{\textbf{Var:}}\
 \begin{mathpar}
   \infer
-  {\Ga ~ \ (x:T) \in \Ga} 
-  {\Ga ~ x:T}
-  \textsc{ (Var)}
+  {\rew{\Ga} ~ \ (x:\rew{T}) \in \rew{\Ga}} 
+  {\rew{\Ga} ~ x:\rew{T}}
+  \tag{Var}
+\end{mathpar}
+\begin{mathpar}
+  \infer
+  {\Ga \CCdash \ (x:T) \in \Ga} 
+  {\Ga \CCdash x:T}
+  \tag{CC-Var}
 \end{mathpar}
\underline{\textbf{X-Prod:}}\
+Where $s_1 \neq \Type_1$ or $s_2 \neq \Prop$:
 \begin{mathpar}
   \infer
-  {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2,s_3) \in \R}
-  {\Ga ~ (x:T) \explicit U : s_3}
-  \textsc{ (X-Prod)}
+  {\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}}
+  \tag{X-Prod}
 \end{mathpar}
-
-\underline{\textbf{X-Lam:}}\
 \begin{mathpar}
   \infer
-  {\Ga, x:T ~ M:U \ \Ga ~ (x:T) \explicit U : s}
-  {\Ga ~ \la(x:T) \explicit M : (x:T) \explicit U}
-  \textsc{ (X-Lam)}
+  {\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{X-App:}}\
+\underline{\textbf{E-Prod:}}\
 \begin{mathpar}
   \infer
-  {\Ga ~ M : (x:T) \explicit U \ \Ga ~ N:T}
-  {\Ga ~ M|N : U{N/x}}
-  \textsc{ (X-App)}
+  {\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}
+\begin{mathpar}
+  \infer
+  {\Ga \CCdash T:\Type_1 \ \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}
-\underline{\textbf{E-Prod:}}\
+\underline{\textbf{X-Lam:}}\
 \begin{mathpar}
   \infer
-  {\Ga ~ T:s_1 \ \Ga, x:T ~ U:s_2 \ (s_1,s_2,s_3) \in \R_e}
-  {\Ga ~ (x:T) \erasable U : s_3}
-  \textsc{ (E-Prod)}
+  {\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}
+\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}
\underline{\textbf{E-Lam:}}\
 \begin{mathpar}
   \infer
-  {\Ga, x:T ~ M:U \ \Ga ~ (x:T) \erasable U : s \ x \notin \fv{M^*}}
-  {\Ga ~ \la(x:T) \erasable M : (x:T) \erasable U}
-  \textsc{ (E-Lam)}
+  {\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}
+\begin{mathpar}
+  \infer
+  {\Ga, x:T \CCdash M:U \ \Ga \CCdash (x:T) \explicit U : \Prop}
+  {\Ga \CCdash \la(x:T) \explicit M : (x:T) \explicit U}
+  \tag{CC-Lam}
 \end{mathpar}
-\underline{\textbf{E-App:}}\
+\underline{\textbf{X-App:}}\
+\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}
 \begin{mathpar}
   \infer
-  {\Ga ~ M : (x:T) \erasable U \ \Ga ~ N:T}
-  {\Ga ~ M|||N : U{N/x}}
-  \textsc{ (E-App)}
+  {\Ga \CCdash M : (x:T) \explicit U \ \Ga \CCdash N:T}
+  {\Ga \CCdash M|N : U{N/x}}
+  \tag{CC-App}
 \end{mathpar}
+\underline{\textbf{E-App:}}\
+\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}
+\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}
-Rules \textsc{Ind}, \textsc{Constr}, and \textsc{Case} cannot infer the type $\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.
\subsection{Example}
+\begin{align*}
+  \mathtt{pack =}\ &\la (\tau : \Type_1) \explicit \la (f : (x : \tau) \explicit \Prop) \explicit \la (w : \tau) \explicit \la (p : f|w) \explicit\ &\la (t : \Prop) \explicit \la (b : (y : \tau) \explicit f|y \explicit t) \explicit (b|w)|p\[10pt]
+  \mathtt{pack :}\ & (\tau : \Type_1) \explicit (f : (x : \tau) \explicit \Prop) \explicit (w : \tau) \explicit (p : f| w) \explicit\ &(t : \Prop) \explicit (b : (y : \tau) \explicit (z : f|y) \explicit t) \explicit t {w/y} {p/z}
+\end{align*}
+
\newpage
 \bibliographystyle{alpha}
View it on GitLab: https://gitlab.com/monnier/typer/compare/74dcbd9d022f3db4ea2c04d57cbda409d56...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/compare/74dcbd9d022f3db4ea2c04d57cbda409d56...
You're receiving this email because of your account on gitlab.com.



    