[Git][monnier/typer][bosn] 2 commits: Add a few theorem-style environments; clean some unused commands - Typer

31 Jul 2018


      Nathaniel pushed to branch bosn at Stefan / Typer
Commits:
da1e981a by nbos at 2018-07-31T12:36:38Z
Add a few theorem-style environments; clean some unused commands
- - - - -
42ee60bb by nbos at 2018-07-31T12:39:09Z
Begin Lemma 3.1; clean translation format; add theorem-style environments where appropriate
- - - - -
2 changed files:
- doc/formal/commands.tex
- doc/formal/typer_theory.tex
Changes:
=====================================
doc/formal/commands.tex
=====================================
@@ -1,4 +1,14 @@
 \renewcommand{\rmdefault}{ptm}
+%% Theorems
+\newtheorem{theorem}{Theorem}[section]
+\newtheorem{lemma}{Lemma}[section]
+
+\theoremstyle{definition}
+\newtheorem{definition}{Definition}[section]
+
+\theoremstyle{definition}
+\newtheorem{remark}{Remark}[section]
+
%% Defined/Free variables
 \newcommand{\Dom}[1]{\textsf{Dom}(#1)}
@@ -52,11 +62,13 @@
 \newcommand{\implicit}{\hspace{\ProdSpace}\Rightarrow\hspace{\ProdSpace}}
 \newcommand{\erasable}{\hspace{\ProdSpace}\Rrightarrow\hspace{\ProdSpace}}
-% \infer options
-\mprset {sep=6mm}
-
 % Misc
+\newcommand{\SmallTitle}[1]{\vspace{3mm}\begin{center}
+    \bf \underline{#1}
+  \end{center}}
+
 \renewcommand{\tag}[1]{\textsc{(#1)}}
+\newcommand{\rew}[1]{\ensuremath{\llbracket #1 \rrbracket}}
\newcommand{\emptyctx}{%
   \mathchoice{\raisebox{1pt}{$\displaystyle\cdot$}}
@@ -68,16 +80,9 @@
 \newcommand{\app}{\raisebox{1.7pt}{\scalebox{0.8}{$||$}}}
 \newcommand{\appp}{\raisebox{1.7pt}{\scalebox{0.8}{$|||$}}}
-\renewcommand{\u}{$\scriptstyle\cup\ $}
-\newcommand{\CC}{\text{CC$\omega$}}
-
-\newcommand{\SmallTitle}[1]{\vspace{3mm}\begin{center}
-    \bf \underline{#1}
-  \end{center}}
-
 \renewcommand{:}{\hspace{-3pt}:\hspace{-3pt}}
 \newcommand{\nottype}{/\hspace{-7pt}:}
-\newcommand{\rew}[1]{\ensuremath{\llbracket #1 \rrbracket}}
+\newcommand{\CC}{\text{CC$\omega$}}
 \newcommand{\CCdash}{\vdash_{\hspace{-2pt}_{CC}}}
 \newcommand{\Tdash}{\vdash_{\hspace{-2pt}_{T}}}
\ No newline at end of file
=====================================
doc/formal/typer_theory.tex
=====================================
@@ -151,7 +151,7 @@ The typing rules for explicit and erasable terms are shown in Figure X. They are
 \end{figure}
-There are two differences between explicit and erasable typing rules:
+There are two notable differences between explicit and erasable typing rules:
 \begin{enumerate}
 \item In the erasable product rule \textsc{E-Prod}, the set of rules is the impredicative $\R_e$ instead of $\R$
 \item In the erasable abstraction rule \textsc{E-Lam}, erasable abstraction are conditional on the bound variable not being free in the expression after erasure ($x \notin \fv{M^*}$). This ensures that the variable is only used in ``erasable'' ways inside the expression such that we are not left with incoherent terms.
@@ -162,14 +162,16 @@ There are two differences between explicit and erasable typing rules:
 \subsection{Inductive Definitions}
 \textbf{Notation:} We use a vector notation to refer to an arbitrary countable number of instances of some kind of term, i.e. $(X \vec{N})$ refers to the identifier $X$ followed by $N_1$, $N_2$, ...,  $N_n$ for $n = |\vec{N}|$ where $|\vec{N}|$ is the size of the term vector $\vec{N}$. Similarly, $(\vec{x}:\vec{M})X$ refers to the term $(x_1:M_1)(x_2:M_2)...(x_n:M_n)X$ for $n = |\vec{x}| = |\vec{M}|$. We also write $i \in |\vec{N}|$ to refer to an $i$ member of the set ${1,2,3,...,n}$ for $n = |\vec{N}|$.
-\textbf{Definition:} We say that $X$ is restricted to a \emph{strictly positive occurrence} in a term $P$ if $P \equiv (\vec{x}:\vec{M})(X \vec{N})$ where $X$ is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$.
-
-\textbf{Definition:} We say that $C$ is a \emph{form of constructor} w.r.t. $X$ if it can be constructed with the following syntax:
+\begin{definition}
+We say that $X$ is restricted to a \emph{strictly positive occurrence} in a term $P$ if $P \equiv (\vec{x}:\vec{M})(X \vec{N})$ where $X$ is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$.
+\end{definition}
+\begin{definition}
+We say that $C$ is a \emph{form of constructor} w.r.t. $X$ if it can be constructed with the following syntax:
$$C ::= (X \vec{N}) ~~|~~ P\to C ~~|~~  (\vec{x}:\vec{M})C$$
Where $X$ is restricted to strictly positive occurrences in the term $P$ and is not free in $N_i$ $\forall i \in |\vec{N}|$ nor in $M_j$ $\forall j \in |\vec{M}|$.
-
+\end{definition}
 We extend our abstract syntax with four terms introduced in \cite{gimenez} to express typing rules of inductive definitions. They are:
 \begin{itemize}
   \renewcommand{\labelitemi}{$-$}
@@ -263,9 +265,11 @@ Recursion is specified through the use of a recursive operator \Letrec \todo
   \textsc{ (Let)}
 \end{mathpar}
-\textbf{Definition:} 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})$.
-
-\textbf{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$:
+\begin{definition}
+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$:
 \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} \
@@ -276,6 +280,7 @@ Recursion is specified through the use of a recursive operator \Letrec \todo
   \D_\V{\Case\ N:S \text{ of } <\vec{G}>} \todo\ 
   \D_\V{N \vec{P}} \todo\
 \end{align*}
+\end{definition}
\subsection{Conversion Rules}
 Typer admits $\beta$ and $\iota$ conversion rules under the congruence written $\cong$. [Expand \todo]
@@ -372,7 +377,9 @@ 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 set up a correspondance between \CC's and Typer's PTS structures such to allow for the translation of set theoric judgements found in typing rules. We first define the translation between universes $\rew{\ } : \S_{CC} \to \S$:
+
+
+We set up a correspondance between \CC's and Typer's PTS structures to allow for the translation of set theoric judgements found in typing rules. We first define the translation between universes $\rew{\ } : \S_{CC} \to \S$:
 \begin{align*}
   \rew{\Prop} ~~~ &= ~~~ \Type\ \mathsf{z} \
   \rew{\Type_1} ~~~ &= ~~~ \Type\ \mathsf{(s\ z)} \
@@ -401,7 +408,7 @@ Thus, the translation of set theoric propositions is the following:
   \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{s_1},\rew{\Prop},\rew{\Prop}) \in \R_e  &\text{if $s_1 \neq \Prop$}\[-4pt]
+    (\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}
@@ -421,11 +428,13 @@ The translation on terms is the one which maintains the provability of translate
We 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 premises by the induction hypothesis and show that the translation of the conclusion can be reached from those premises by one of Typer's typing rules.
-\textbf{Case \textsc{CC-Wf-E}:}
+
+\underline{\textbf{Case 1:}}
 \begin{mathpar}
   \infer
   {\ }
   {\emptyctx \CCdash}
+  \tag{CC-Wf-E}
 \end{mathpar}
 The translation is immediately true under Typer by rule \textsc{Wf-E}.
 \begin{mathpar}
@@ -439,17 +448,16 @@ The translation is immediately true under Typer by rule \textsc{Wf-E}.
   \tag{Wf-E}
 \end{mathpar}
-\textbf{Case \textsc{CC-Wf-S}:}
+\underline{\textbf{Case 2:}}
 \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}
 By the induction hypothesis we can assume
 \begin{mathpar}
-  \infer
   {\rew{\Ga} ~ \rew{T}:\rew{s} \ \rew{s} \in \S \ x \notin \dv{\rew{\Ga}}}
-  {\ }
 \end{mathpar}
 which allows us to infer the translation of the conclusion by rule
 \begin{mathpar}
@@ -459,17 +467,16 @@ which allows us to infer the translation of the conclusion by rule
   \tag{WF-S}
 \end{mathpar}
-\textbf{Case \textsc{CC-Sort}:}\
+\underline{\textbf{Case 3:}\}
 \begin{mathpar}
   \infer
   {\Ga \CCdash \ (s_1:s_2) \in \A_{CC}}
   {\Ga \CCdash s_1:s_2}
+  \tag{CC-Sort}
 \end{mathpar}
 By the induction hypothesis we can assume
 \begin{mathpar}
-  \infer
   {\rew{\Ga} ~ \ (\rew{s_1}:\rew{s_2}) \in \A}
-  {\ }
 \end{mathpar}
 and reach the translation of the conclusion by rule
 \begin{mathpar}
@@ -479,17 +486,16 @@ and reach the translation of the conclusion by rule
   \tag{Sort}
 \end{mathpar}
-\textbf{Case \textsc{CC-Var}:}\
+\underline{\textbf{Case 4:}\}
 \begin{mathpar}
   \infer
   {\Ga \CCdash \ (x:T) \in \Ga} 
   {\Ga \CCdash x:T}
+  \tag{CC-Var}
 \end{mathpar}
 By the induction hypothesis we can assume
 \begin{mathpar}
-  \infer
   {\rew{\Ga} ~ \ (x:\rew{T}) \in \rew{\Ga}} 
-  {\ }
 \end{mathpar}
 and reach the translation of the conclusion by rule
 \begin{mathpar}
@@ -499,20 +505,19 @@ and reach the translation of the conclusion by rule
   \tag{Var}
 \end{mathpar}
-\textbf{Case \textsc{CC-Prod}:}\
+\underline{\textbf{Case 5:}\}
 \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}
 By the induction hypothesis, there are two subcases to consider---a predicative and an impredicative one:
-\underline{Predicative:}\
+\textbf{Predicative subcase:}\
 We have the assumptions
 \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}
-  {\ }
 \end{mathpar}
 from which we can conclude
 \begin{mathpar}
@@ -522,51 +527,50 @@ from which we can conclude
   \tag{X-Prod}
 \end{mathpar}
-\underline{Impredicative:}\
+\textbf{Impredicative subcase:}\
 We have the assumptions
 \begin{mathpar}
-  \infer
-  {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{\Prop} \ (\rew{s_1},\rew{\Prop},\rew{\Prop}) \in \R_e}
-  {\ }
+  {\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}
 \end{mathpar}
 from which we can conlcude 
 \begin{mathpar}
   \infer
-  {\rew{\Ga} ~ \rew{T}:\rew{s_1} \ \rew{\Ga}, x:\rew{T} ~ \rew{U}:\rew{\Prop} \ (\rew{s_1},\rew{\Prop},\rew{\Prop}) \in \R_e}
+  {\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}
-Thus we have that
-\begin{align}
+
+\begin{remark} The only way to construct a product type in \CC\ is through the application of typing rule \textsc{CC-Prod}, so all translations of product types will follow this rule:
+\begin{align*}
   \rew{(x:T)\explicit U} \leadsto
   \begin{cases}
-    (x:\rew{T})\erasable \rew{U} & \text{if $(U:\Prop)$ and $\neg(T:\Prop)$} \
+    (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{align*}
+\end{remark}
-\textbf{Case \textsc{CC-App}:}\
+\underline{\textbf{Case 6:}\}
 \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}
-  \infer
   {\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 (3)):
+And we again have two subcases to consider for the translation $\rew{(x:T) \explicit U}$ (see Remark 3.1):
-\underline{Predicative:}\
+\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}
-\underline{Impredicative:}\
+\textbf{Impredicative subcase:}\
 \begin{mathpar}
   \infer
   {\rew{\Ga} ~ \rew{M} : (x:\rew{T}) \erasable \rew{U} \ \rew{\Ga} ~ \rew{N}:\rew{T}}
@@ -574,21 +578,20 @@ And we again have two subcases to consider for the translation $\rew{(x:T) \expl
   \tag{E-App}
 \end{mathpar}
-\textbf{Case \textsc{CC-Lam}:}\
+\underline{\textbf{Case 7:}\}
 \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}
 By the induction hypothesis we can assume
 \begin{mathpar}
-  \infer
   {\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U} \ \rew{\Ga} ~ \rew{(x:T) \explicit U} : \rew{s}}
-  {\ }
 \end{mathpar}
-And by (3), we have two subcases to consider for the translation \rew{(x:T) \explicit U}:
+And by Remark 3.1, we have two subcases to consider for the translation \rew{(x:T) \explicit U}:
-\underline{Predicative:}\
+\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.
 \begin{mathpar}
   \infer
@@ -596,20 +599,37 @@ 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}
-\underline{Impredicative:}\
-The impredicative product type translates to an erasable product type $(x:\rew{T}) \erasable \rew{U}$ and we apply the erasable \textsc{E-Lam} typing rule to derive the typing of the erasable lambda abstraction. However, an additional premise is required \todo
+\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,
 \begin{mathpar}
   \infer
-  {\rew{\Ga}, x:\rew{T} ~ \rew{M}:\rew{U} \ \rew{\Ga} ~ (x:\rew{T}) \erasable \rew{U} : \rew{s} \ x \notin \fv{\rew{M}^*}}
+  {\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}
+but we have yet to show that the additional premise $x \notin \fv{\rew{M}^*}$ of rule \textsc{E-Lam} holds in all cases.
-\textbf{Lemma:} \todo
+\begin{lemma}
+  By our currently defined translation \rew{\ }, the following holds: \vspace{-5mm}
+\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*}
 \end{proof}
+
+
 \subsection{Example}
\newpage
View it on GitLab: https://gitlab.com/monnier/typer/compare/b2fdff75dab72f50d5ddf163dbcfcd00a22...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/compare/b2fdff75dab72f50d5ddf163dbcfcd00a22...
You're receiving this email because of your account on gitlab.com.



    