\documentclass[draft]{article} \input linear \def\bad#1{{\em [XXX: #1]}} \def\cn{{:}} \def\dv{{\div}} \def\sr{{\star}} \def\vv{\mathrel{\vdash\!\!\!\vdash}} \def\isem{{\mathrel;\mkern-9.5mu\mathrel-}} \def\ssem{{\mathrel,\mkern-7mu\mathrel\star}} \def\rnil{{\sans nil}} \def\rtype{{\sans type}} \def\rkind{{\sans kind}} \def\whr{\mathrel{\mathop{\longrightarrow}\limits^{whr}}} \begin{document} %\title{LFIN \break %\small ({\bf LF} with {\bf I}rrelevance and {\bf N}otational definitions)} \title{LF with Irrelevance and Notational Definitions} \author{Jason Reed} \maketitle \tableofcontents % \section{Language} \begin{center}\begin{tabular}{lll} Kinds&$K$&$::=\rtype\celse \Pi x \cn A . K \celse \Pi x \dv A . K$\\ Types&$A$&$::=a\cdot S \celse \Pi x \cn A . B \celse \Pi x \dv A . B$\\ Objects&$M$&$::= H \cdot S \celse \lambda x \cn A . M \celse \lambda x \dv A . M \celse M \cdot S$\\ Spines&$S$&$::= \rnil \celse (M ; S) \celse (M\ \isem S)$\\ Heads&$H$&$::= c \celse x \celse d$\\ \\ Signatures&$\Sigma$&$::= \cdot \celse \Sigma, a : K\celse \Sigma, c : A \celse \Sigma, d : A = M$\\ Contexts&$\Gamma$&$::= \cdot \celse \Gamma, x : A \celse \Gamma, x \div A$\\ Erased Contexts&$\Gamma^\square$&$::= \cdot \celse \Gamma^\square, x$\\ \end{tabular}\end{center} % \section{Proof Typing} Functions: \begin{center}\begin{tabular}{llp{1.8in}} Proof Promotion&$\Gamma \mapsto \Gamma^\oplus$& Promote proof variables in $\Gamma$ to term variables\\ \end{tabular}\end{center} Judgments: \begin{center}\begin{tabular}{llp{1.8in}} Proof Object Typing&$\Gamma \prov M \div A$& In $\Gamma$, $M$ has irrelevant type $A$.\\ \end{tabular}\end{center} % \subsection{Proof Promotion} \begin{eqnarray*} \cdot^\oplus &:=& \cdot\\ (\Gamma, x : A)^\oplus &:=& \Gamma^\oplus, x : A\\ (\Gamma, x \div A)^\oplus &:=& \Gamma^\oplus, x : A \end{eqnarray*} % \subsection{Proof Object Typing} $$\begin{prooftree} \Gamma^\oplus \prov M : A \qquad \Gamma \prov A : \rtype \using \ir pot. \justifies \Gamma \prov M \div A \end{prooftree}$$ % \section{Typing} Judgments: \begin{center}\begin{tabular}{llp{1.8in}} Spine Typing&$\Gamma \prov S : A > a$& In $\Gamma$, $S$ gives base type $a$ for a head of type $A$.\\ Type Spine Kinding&$\Gamma \prov S : K \gg \rtype$& In $\Gamma$, $S$ gives a type for a head of kind $K$.\\ Object Typing&$\Gamma \prov M : A$& In $\Gamma$, $M$ has type $A$.\\ Type Validity&$\Gamma \prov A : \rtype$& In $\Gamma$, $A$ is a valid type.\\ Kind Validity&$\Gamma \prov K : \rkind$& In $\Gamma$, $K$ is a valid kind.\\ \end{tabular}\end{center} % \subsection{Spine Typing} $$\begin{prooftree} \using \ir st_nil. \justifies \Gamma \prov \rnil : A > A \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov M : A \qquad \Gamma \prov S : [M/x] B > C \using \ir st_cons. \justifies \Gamma \prov (M ; S) : \Pi x \cn A . B > C \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov M \div A \qquad \Gamma \prov S : [M/x] B > C \using \ir st_icons. \justifies \Gamma \prov (M\ \isem S) : \Pi x {\div} A . B > C \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov S : A > B \qquad \Gamma \prov B = B' : \rtype \using \ir st_conv. \justifies \Gamma \prov S : A > B' \end{prooftree}$$ % \subsection{Type Spine Kinding} $$\begin{prooftree} \using \ir tsk_nil. \justifies \Gamma \prov \rnil : \rtype \gg \rtype \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov M : A \qquad \Gamma \prov S : [M/x] K \gg \rtype \using \ir tsk_cons. \justifies \Gamma \prov (M ; S) : \Pi x \cn A . K \gg \rtype \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov M \div A \qquad \Gamma \prov S : [M/x] K \gg \rtype \using \ir tsk_icons. \justifies \Gamma \prov (M\ \isem S) : \Pi x {\div} A . K \gg \rtype \end{prooftree}$$ % \subsection{Object Typing} $$\begin{prooftree} c : A \in \Sigma \qquad \Gamma \prov S : A > B \using \ir ot_const. \justifies \Gamma \prov c \cdot S : B \end{prooftree}$$ $$\begin{prooftree} x : A \in \Gamma \qquad \Gamma \prov S : A > B \using \ir ot_var. \justifies \Gamma \prov x \cdot S : B \end{prooftree}$$ $$\begin{prooftree} d : A = M \in \Sigma \qquad \Gamma \prov S : A > B \using \ir ot_def. \justifies \Gamma \prov d \cdot S : B \end{prooftree}$$ $$\begin{prooftree} \Gamma, x\star A \prov M : B \qquad \Gamma \prov A : \rtype \using \ir ot_lam. \justifies \Gamma \prov \lambda x\sr A . M : \Pi x \sr A . B \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov M : A \qquad \Gamma \prov S : A > B \using \ir ot_app. \justifies \Gamma \prov M \cdot S : B \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov M : A \qquad \Gamma \prov A = B : \rtype \using \ir ot_conv. \justifies \Gamma \prov M : B \end{prooftree}$$ % \subsection{Type Validity} $$\begin{prooftree} a : K \in \Sigma \qquad \qquad \Gamma \prov S : K \gg \rtype \using \ir tv_const. \justifies \Gamma \prov a \cdot S : \rtype \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov A : \rtype \qquad \Gamma, x \star A \prov B : \rtype \using \ir tv_pi. \justifies \Gamma \prov \Pi x \sr A . B : \rtype \end{prooftree}$$ % \subsection{Kind Validity} $$\begin{prooftree} \using \ir kv_type. \justifies \Gamma \prov \rtype : \rkind \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov A : \rtype \qquad \Gamma, x \star A \prov K : \rkind \using \ir kv_pi. \justifies \Gamma \prov \Pi x \sr A . K : \rkind \end{prooftree}$$ % \section{Equality} Judgments: \begin{center}\begin{tabular}{p{1.0in}lp{1.8in}} Proof Equality&$\Gamma \prov M_1 = M_2 \div A$& In $\Gamma$, $M_1=M_2$ at irrelevant type $A$.\\ Object Equality&$\Gamma \prov M_1 = M_2 : A$& In $\Gamma$, $M_1=M_2$ at type $A$.\\ Type Equality&$\Gamma \prov A_1 = A_2 : \rtype$& In $\Gamma$, $A_1$ and $A_2$ are equal types.\\ Kind Equality&$\Gamma \prov K_1 = K_2 : \rkind$& In $\Gamma$, $K_1$ and $K_2$ are equal kinds.\\ Spine Equality&$\Gamma \prov S_1 = S_2 : A>B$& In $\Gamma$, $S_1=S_2$ at type $A>B$.\\ Type Spine\hfil\break Equality&$\Gamma \prov S_1 = S_2 : K \gg \rtype$& In $\Gamma$, $S_1=S_2$ at kind $\rtype$. \end{tabular}\end{center} % \subsection{Proof Equality} $$\begin{prooftree} \Gamma^\oplus \prov M = M : A \qquad \Gamma^\oplus \prov N = N : A \qquad \Gamma \prov A : \rtype \using \ir pe. \justifies \Gamma\prov M = N \div A \end{prooftree}$$ % \subsection{Object Equality} \subsubsection{Simultaneous Congruence} $$\begin{prooftree} c : A \in \Sigma \qquad \Gamma \prov S_1 = S_2 : A > B \using \ir oe_const. \justifies \Gamma \prov c \cdot S_1 = c \cdot S_2 : B \end{prooftree}$$ $$\begin{prooftree} x : A \in \Gamma \qquad \Gamma \prov S_1 = S_2 : A > B \using \ir oe_var. \justifies \Gamma \prov x \cdot S_1 = x \cdot S_2 : B \end{prooftree}$$ $$\begin{prooftree} d : A = M \in \Sigma \qquad \Gamma \prov M \cdot S_1 = M \cdot S_2 : B \using \ir oe_def. \justifies \Gamma \prov d \cdot S_1 = d \cdot S_2 : B \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov A_1' = A_1 : \rtype \qquad \Gamma \prov A_1'' = A_1 : \rtype \qquad \Gamma, x \star A_1 \prov M = N : A_2 \using \ir oe_lam. \justifies \Gamma \prov \lambda x \sr A_1' . M = \lambda x \sr A_1'' . N : \Pi x \sr A_1 . A_2 \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov M_1 = M_2 : A \qquad \Gamma \prov S_1 = S_2 : A > B \using \ir oe_app. \justifies \Gamma \prov M_1 \cdot S_1 = M_2 \cdot S_2 : B \end{prooftree}$$ \subsubsection{Extensionality} $$\begin{prooftree} \Gamma \prov A_1 : \rtype \qquad {\{\Gamma \prov M_1, M_2 : \Pi x \cn A_1 . A_2\} \atop \Gamma, x : A_1 \prov M_1 \cdot (x \cdot \rnil; \rnil) = M_2 \cdot (x \cdot \rnil; \rnil) : A_2} \using \ir oe_ext. \justifies \Gamma \prov M_1 = M_2 : \Pi x \cn A_1 . A_2 \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov A_1 : \rtype \qquad {\{\Gamma \prov M_1, M_2 : \Pi x \dv A_1 . A_2\} \atop \Gamma, x \div A_1 \prov M_1 \cdot (x \cdot \rnil\ \isem \rnil) = M_2 \cdot (x \cdot \rnil\ \isem \rnil) : A_2} \using \ir oe_iext. \justifies \Gamma \prov M_1 = M_2 : \Pi x \dv A_1 . A_2 \end{prooftree}$$ \subsubsection{Parallel Reduction} $$\begin{prooftree} \Gamma \prov M = N : B \using \ir oe_red_nil. \justifies \Gamma \prov M \cdot \rnil = N : B \end{prooftree}$$ $$\begin{prooftree} \Gamma\prov H \cdot \rnil : B \qquad \Gamma \prov S_1 = S_2 : B > C \using \ir oe_red_nil2. \justifies \Gamma \prov (H \cdot \rnil) \cdot S_1 = H \cdot S_2 : C \end{prooftree}$$ $$\begin{prooftree} $\Gamma, x : B \prov M_1 = M_2 : A \djust \Gamma \prov N_1 = N_2 : B$ \qquad \Gamma, x : B \prov S = S' : A > C \using \ir oe_red_cons.\justifies \Gamma \prov (\lambda x \cn B . M_1) \cdot (N_1 ; S) = [N_2/x]M_2 \cdot S' : [N_1/x]C \end{prooftree}$$ $$\begin{prooftree} $\Gamma, x \div B \prov M_1 = M_2 : A \djust \Gamma \prov N_1 = N_2 \div B$ \qquad \Gamma, x \div B \prov S = S' : A > C \using \ir oe_red_icons.\justifies \Gamma \prov (\lambda x \dv B . M_1) \cdot (N_1\ \isem S) = [N_2/x]M_2 \cdot S' : [N_1/x]C \end{prooftree}$$ \subsubsection{Type Conversion} $$\begin{prooftree} \Gamma \prov M = N : A \qquad \Gamma \prov A = B : \rtype \using \ir oe_conv. \justifies \Gamma \prov M = N : B \end{prooftree}$$ % \subsection{Type Equality} \subsubsection{Simultaneous Congruence} $$\begin{prooftree} a : K \in \Sigma \qquad \Gamma \prov S_1 = S_2 : K \gg \rtype \using \ir te_const. \justifies \Gamma \prov a \cdot S_1 = a \cdot S_2 : \rtype \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov A' = A : \rtype \qquad \Gamma, x \star A \prov B = B' : \rtype \using \ir te_pi. \justifies \Gamma \prov \Pi x \sr A . B = \Pi x \sr A' . B' : \rtype \end{prooftree}$$ % \subsection{Kind Equality} \subsubsection{Simultaneous Congruence} $$\begin{prooftree} \using \ir ke_type. \justifies \Gamma \prov \rtype = \rtype : \rkind \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov A' = A : \rtype \qquad \Gamma, x \star A \prov K = K' : \rkind \using \ir ke_pi. \justifies \Gamma \prov \Pi x \sr A . K = \Pi x \sr A' . K' : \rkind \end{prooftree}$$ % \subsection{Spine Equality} \subsubsection{Simultaneous Congruence} $$\begin{prooftree} \using \ir se_nil. \justifies \Gamma \prov \rnil = \rnil : A > A \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov M_1 = M_2 : A \qquad \Gamma \prov S_1 = S_2 : [M_1/x]B > C \using \ir se_cons. \justifies \Gamma \prov (M_1 ; S_1) = (M_2 ; S_2) : \Pi x \cn A . B > C \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov M_1 = M_2 \div A \qquad \Gamma \prov S_1 = S_2 : [M_1/x]B > C \using \ir se_icons. \justifies \Gamma \prov (M_1\ \isem S_1) = (M_2\ \isem S_2) : \Pi x \dv A . B > C \end{prooftree}$$ % \subsection{Type Spine Equality} \subsubsection{Simultaneous Congruence} $$\begin{prooftree} \using \ir tse_nil. \justifies \Gamma \prov \rnil = \rnil : \rtype \gg \rtype \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov M_1 = M_2 : A \qquad \Gamma \prov S_1 = S_2 : [M_1/x]K \gg \rtype \using \ir tse_cons. \justifies \Gamma \prov (M_1 ; S_1) = (M_2 ; S_2) : \Pi x \cn A . K \gg \rtype \end{prooftree}$$ $$\begin{prooftree} \Gamma \prov M_1 = M_2 \div A \qquad \Gamma \prov S_1 = S_2 : [M_1/x]K \gg \rtype \using \ir tse_icons. \justifies \Gamma \prov (M_1\ \isem S_1) = (M_2\ \isem S_2) : \Pi x \dv A . K \gg \rtype \end{prooftree}$$ %%% \begin{lemma}[Functionality] \begin{enumerate} \end{enumerate} \end{lemma} \begin{proof} \cqed \end{proof} \begin{lemma} ($\eta$-conversion) \label{eta} \begin{enumerate} \item If $\Gamma \prov M : \Pi x \cn A . B$, then $\Gamma \prov M = \lambda x \cn A . M \cdot (x \cdot \rnil ; \rnil) : \Pi x \cn A . B$ \item If $\Gamma \prov M : \Pi x \dv A . B$, then $\Gamma \prov M = \lambda x \dv A . M \cdot (x \cdot \rnil\ \isem \rnil) : \Pi x \dv A . B$ \end{enumerate} \end{lemma} \begin{proof}\ \begin{enumerate} \item {\small $$\begin{prooftree} $\[\using \ir oe_red_nil. \justifies x \cdot \rnil = (x \cdot \rnil) \cdot \rnil$$\justifies (x\cdot \rnil ; \rnil) = (x\cdot \rnil ; \rnil)$ \using \ir oe_red_cons. \justifies \Gamma, x : A \prov M \cdot (x \cdot \rnil ; \rnil) = (\lambda y \cn A . M \cdot (y \cdot \rnil ; \rnil)) \cdot (x \cdot \rnil ; \rnil) : B \] \using \ir oe_ext.\justifies \Gamma \prov M = \lambda y \cn A . M \cdot (y \cdot \rnil ; \rnil) : \Pi y \cn A . B \end{prooftree}$$} \item Similar. \end{enumerate} \cqed \end{proof} %%% \begin{lemma} (Spine Splicing) \label{splice} \begin{enumerate} \item If $\Gamma \prov S : A > B$, $\Gamma \prov M : \Pi x \cn C . A$ and $\Gamma \prov N : C$, then $\Gamma\prov M \cdot (N; S) = (M \cdot (N; \rnil)) \cdot S : B$ \item If $\Gamma \prov S : A > B$, $\Gamma \prov M : \Pi x \dv C . A$ and $\Gamma \prov N \div C$, then $\Gamma\prov M \cdot (N\ \isem S) = (M \cdot (N\ \isem \rnil)) \cdot S : B$ \end{enumerate} \end{lemma} \begin{proof} \begin{enumerate} \item By Lemma~\ref{eta} and $\ir oe_app.$, we know $$\Gamma \prov M \cdot (N; S) = (\lambda x \cn A . M \cdot (x \cdot \rnil ; \rnil)) \cdot (N ; S) : B$$ By $\ir oe_red_cons.$, (using $\ir oe_red_nil.$ to see that $N \cdot \rnil = N$) we have $$\Gamma \prov M \cdot (N; S) = (M \cdot (N; \rnil)) \cdot S : B$$ as required. \item Similar. \end{enumerate} \cqed \end{proof} \begin{lemma} (Validity) \begin{enumerate} \item If $\Gamma\prov M \star A$, then $\Gamma \prov A : \rtype$. \item If $\Gamma\prov S : A > B$ and $\Gamma \prov A : \rtype$, then $\Gamma \prov B : \rtype$. \item If $\Gamma, x \star A\prov B : \rtype$ and $\Gamma \prov M \star A$, then $\Gamma \prov [M/x]B : \rtype$. \item If $\Gamma\prov M_1 = M_2 \star A$, then $\Gamma \prov M_1 \star A$ and $\Gamma \prov M_2 \star A$. \item If $\Gamma\prov S_1 = S_2 : A > B$, then $\Gamma \prov S_1 : A > B$ and $\Gamma \prov S_2 : A > B$. \item If $\Gamma\prov A_1 = A_2 : \rtype$, then $\Gamma \prov A_1 : \rtype$ and $\Gamma \prov A_2 : \rtype$. \end{enumerate} \end{lemma} \begin{proof} By induction on the appropriate rules. \cqed \end{proof} \begin{lemma} (Unicity) \begin{enumerate} \item If $\Gamma\prov M \star A$ and $\Gamma\prov M \star A'$, then $\Gamma \prov A = A' : \rtype$. \item If $\Gamma\prov S : A > B$, and $\Gamma \prov S : A' > B'$, and also $\Gamma \prov A = A' : \rtype$, then $\Gamma \prov B = B' : \rtype$. \end{enumerate} \end{lemma} \begin{proof} By simultaneous induction on the structure of the relevant typing deductions. \cqed \end{proof} %\begin{lemma} %If $\Gamma \prov S : A > B$, then $B$ is of the form $a \cdot S'$. %\end{lemma} %\begin{proof} %By induction on the spine typing and type equality rules. %\cqed %\end{proof} %\begin{lemma} (Extensionality) %%If $\Gamma \prov M : \Pi x_1 : A_1 . \Pi x_2 : A_2 . \cdots \Pi x_n : A_n . B$, then %%$M$ is of the form $\lambda x_1 : A_1 . \lambda x_2 . A_2 . \cdots \lambda x_n : A_n . M'$, %%and $\Gamma, x_1 : A_1, x_2 : A_2, \ldots, x_n : A_n \prov M' : B$. %If $\Gamma \prov M : \Pi x \sr A . B$, then %$M$ is of the form $\lambda x \sr A . M'$, %and $\Gamma, x \star A \prov M' : B$. %\end{lemma} %\begin{proof} %By induction on the object typing and type equality rules. %\cqed %\end{proof} % \section{Strictness} \def\rpat{{\ \sans pat}} Functions: \begin{center}\begin{tabular}{llp{1.8in}} Erasure&$\Gamma \mapsto \Gamma^\square$& Remove types and irrelevant variables from $\Gamma$\\ \end{tabular}\end{center} Judgments: \begin{center}\begin{tabular}{llp{1.8in}} Pattern Spine&$\Delta^\square \prov S \rpat$& In $\Delta$, $S$ is a pattern spine.\\ Local Strict Occurrences&$\Gamma;\Delta \vv_x M$& $x$ occurs locally strict in $M$\\ &$\Gamma;\Delta \vv_x A$& $x$ occurs locally strict in $A$\\ &$\Gamma;\Delta \vv_x S$& $x$ occurs locally strict in $S$\\ Strict Occurrences&$\Gamma \vv_x M$& $x$ occurs strict in $M$\\ Strictness&$\Gamma \vv M$& $M$ is strict\\ \end{tabular}\end{center} % \subsection{Erasure} \begin{eqnarray*} \cdot^\square &:=& \cdot\\ (\Gamma, x : A)^\square &:=& \Gamma^\square, x^: \\ (\Gamma, x \div A)^\square &:=& \Gamma^\square, x^\div \end{eqnarray*} \subsection{Pattern Spines} $$\begin{prooftree} \using \ir pat_nil. \justifies \Delta^\square \prov \rnil \rpat \end{prooftree}$$ $$\begin{prooftree} \Delta^\square \prov S \rpat \qquad x^\star \not\in \Delta^\square \using \ir pat_cons. \justifies \Delta^\square, x^: \prov (x; S) \rpat \end{prooftree}$$ $$\begin{prooftree} \Delta^\square \prov S \rpat \using \ir pat_icons. \justifies \Delta^\square \prov (M\ \isem S) \rpat \end{prooftree}$$ %%% \begin{lemma} Suppose $\Gamma \prov N_1, N_2 \div A$. \begin{enumerate} \item If $\Gamma, z \div A \prov M \star B$, then $\Gamma \prov [N_1/z]M = [N_2/z]M \star [N_1/z]B$. \item If $\Gamma, z \div A \prov S : A > B$, then $\Gamma \prov [N_1/z]S = [N_2/z]S : [N_1/z]A > [N_1/z]B$. \item If $\Gamma, z \div A \prov B \star \rtype$, then $\Gamma \prov [N_1/z]B = [N_2/z]B \star \rtype$. \end{enumerate} \label{irrel.subst} \end{lemma} \begin{proof} Simultaneous induction on the object and spine typing and type validity rules. \cqed \end{proof} %%% \begin{lemma}\label{nil.replace}\ \begin{enumerate} \item If $\Gamma \prov M : A$, then $\Gamma \prov [x\cdot \rnil / x]M = M : A$. \item If $\Gamma \prov S : A > B$, then $\Gamma \prov [x\cdot \rnil / x]S = S : A > B$. \item If $\Gamma \prov A : \rtype$, then $\Gamma \prov [x\cdot \rnil / x]A = A : \rtype$. \end{enumerate} \end{lemma} \begin{proof} Simultaneous induction on the object and spine typing and type validity rules. The critical case is $\ir ot_var.$, where we use $\ir oe_red_nil2.$. \cqed \end{proof} %%% \begin{lemma}\label{pi.nil.replace} If $\Gamma \prov \Pi y \sr B . B' : \rtype$ and $x \not \in \Gamma$, then $\Gamma \prov \Pi x \sr B. [x\cdot \rnil / y] B' = \Pi y \sr B . B' : \rtype$. \end{lemma} \begin{proof} By $\alpha$-conversion, we know $\Gamma \prov \Pi x \sr B . [x/y]B' : \rtype$, and inversion on the type validity rules gives $\Gamma, x \star B \prov [x/y]B' : \rtype$. By Lemma~\ref{nil.replace} and the fact that $x\not\in\Gamma$ and consequently $x$ does not appear free in $B'$, we know $\Gamma, x \star B \prov [x\cdot \rnil / y]B' : \rtype$, hence $\Gamma \prov \Pi x \sr B . [x\cdot \rnil / y]B' : \rtype$, as required. \cqed \end{proof} %%% \begin{lemma} If \begin{enumerate} \item $\Delta^\square \prov S \rpat$, \item $\Gamma \prov M_1, M_2 : A_2$, \item $\Delta \prov S : A_1 > C$, \item $\Gamma, \Delta \prov A_1 = A_2 : \rtype$ \item $\Gamma, \Delta \prov M_1 \cdot S = M_2 \cdot S : C$, and \label{big.assume} \item The variable names in $\Gamma$ and $\Delta$ are disjoint. \end{enumerate} then $\Gamma \prov M_1 = M_2 : A_2$. \end{lemma} \begin{proof} By induction on $\D :: \Delta^\square \prov S \rpat$. \begin{itemize} \item[Case:] $$\D = \begin{prooftree} \using \ir pat_nil. \justifies \Delta^\square \prov \rnil \rpat \end{prooftree}$$ In this case, $S = \rnil$. By inversion on the spine typing rules, $A_1$ is identical to $C$, so we have $\Gamma, \Delta \prov C = A_2 : \rtype$. We know that $\Gamma, \Delta \prov M_1 \cdot \rnil = M_2 \cdot \rnil : C$, so by $\ir oe_red_nil.$ we can conclude $\Gamma, \Delta \prov M_1 = M_2 : C$. By $\ir oe_conv.$, we know $\Gamma, \Delta \prov M_1 = M_2 : A_2$. But no variable from $\Delta$ appears free in $M_1$ or $M_2$, so $\Gamma \prov M_1 = M_2 : A_2$. \item[Case:] $$\D = \begin{prooftree} $\D' \djust (\Delta')^\square \prov S' \rpat$ $\djust x^\star \not\in (\Delta')^\square$ \using \ir pat_cons. \justifies (\Delta')^\square, x^: \prov (x \cdot \rnil; S') \rpat \end{prooftree}$$ In this case, $S = (x \cdot \rnil; S')$ and $x : B \in \Delta$ for some $B : \rtype$. So we know $\Delta \prov (x \cdot \rnil ; S') : A_1 > C$. Assumption~(\ref{big.assume}) in this case is $$\Gamma, \Delta \prov M_1 \cdot (x \cdot \rnil; S') = M_2 \cdot (x \cdot \rnil; S') : C$$ By Lemma~\ref{splice} we can infer $$\Gamma, \Delta \prov (M_1 \cdot (x \cdot \rnil; \rnil)) \cdot S' = (M_2 \cdot (x \cdot \rnil;\rnil)) \cdot S' : C$$ Now by inversion on the spine typing rules, $A_1$ must be of the form $\Pi y \cn B . B'$, such that $\Delta' \prov S' : [x\cdot\rnil/y]B' > C$. Notice that we can also now show that $$\Gamma, x : B \prov M_1 \cdot (x \cdot \rnil; \rnil), M_2 \cdot (x \cdot \rnil; \rnil) : [x\cdot\rnil/y]B'$$ and $\Gamma, \Delta \prov B' = B' : \rtype$, and also $\Gamma, x : B$ is disjoint from $\Delta'$. By the induction hypothesis, we get $$\Gamma, x : B \prov (M_1 \cdot (x \cdot \rnil; \rnil)) = (M_2 \cdot (x \cdot \rnil;\rnil)) : [x\cdot\rnil/y]B'$$ Using $\ir oe_ext.$, and Lemma~\ref{pi.nil.replace}, we conclude $$\Gamma, \Delta \prov M_1 = M_2 : \Pi y \cn B . B'$$ and so $$\Gamma \prov M_1 = M_2 : A_2$$ by type conversion and the observation that no variables in $\Delta$ appear free in $M_1$ or $M_2$ by their typing. \item[Case:] $$\D = \begin{prooftree} $\D' \djust \Delta^\square \prov S' \rpat$ \using \ir pat_icons. \justifies \Delta^\square \prov (M'\ \isem S') \rpat \end{prooftree}$$ In this case, $S = (M' \ \isem S')$. By inversion on the spine typing rules, $\Delta \prov M' \div B$ for some $B \div \rtype$ and $A_1$ is of the form $\Pi y \dv B . B'$, such that $\Delta \prov S' : [M'/y]B' > C$. So we know $\Delta \prov (M' \ \isem S') : \Pi y \dv B . B' > C$. Assumption~(\ref{big.assume}) in this case is $$\Gamma, \Delta \prov M_1 \cdot (M' \ \isem S') = M_2 \cdot (M' \ \isem S') : C$$ By Lemma~\ref{splice} we can infer $$\Gamma, \Delta \prov (M_1 \cdot (M' \ \isem \rnil)) \cdot S' = (M_2 \cdot (M' \ \isem\rnil)) \cdot S' : C$$ Now create a fresh variable $\bar x : A$ for each $x : A\in \Delta$. Put $\bar\Delta = \{\bar x : A \st x : A \in \Delta\}$. We have (by the triviality of equality at irrelevant type) that $$\Delta,\bar \Delta \prov M' = [\bar\Delta / \Delta]M' \div B$$ and so $$\Gamma, \bar\Delta, \Delta \prov (M_1 \cdot ([\bar\Delta/\Delta]M' \ \isem \rnil)) \cdot S' = (M_2 \cdot ([\bar\Delta/\Delta]M' \ \isem\rnil)) \cdot S' : C$$ by using Lemma~\ref{irrel.subst}. Notice that we do not substitute for any occurrences of $M'$ in $S'$. We can also now show that $$\Gamma, \bar \Delta \prov M_1 \cdot ([\bar\Delta/\Delta]M' \ \isem \rnil), M_2 \cdot ([\bar\Delta/\Delta]M' \ \isem \rnil) : [[\bar\Delta/\Delta]M'/y]B'$$ and $\Gamma, \bar\Delta, \Delta \prov [M'/y]B' = [[\bar\Delta/\Delta]M'/y]B' \div \rtype$, and also $\Gamma, \bar\Delta$ is disjoint from $\Delta$, since the variables in $\bar\Delta$ were chosen to be fresh. By the induction hypothesis, we get $$\Gamma, \bar \Delta \prov (M_1 \cdot ([\bar\Delta/\Delta]M' \ \isem \rnil)) = (M_2 \cdot ([\bar\Delta/\Delta]M' \ \isem\rnil)) : [[\bar\Delta/\Delta]M'/y]B'$$ Using Lemma~\ref{irrel.subst} again, we can see that $$\Gamma, \bar \Delta, w \div [\bar\Delta/\Delta]B \prov (M_1 \cdot (w \cdot \rnil \ \isem \rnil)) = (M_2 \cdot (w\cdot \rnil\ \isem\rnil)) : [w\cdot \rnil/y]B'$$ By, $\ir oe_ext.$ $$\Gamma, \bar \Delta \prov M_1 = M_2 : \Pi w \dv [\bar\Delta/\Delta]B . [w\cdot \rnil/y]B'$$ Lemma~\ref{pi.nil.replace} provides the simplification $$\Gamma, \bar \Delta \prov M_1 = M_2 : \Pi w \dv [\bar\Delta/\Delta]B . [w/y]B'$$ and $\alpha$-conversion gives $$\Gamma, \bar \Delta \prov M_1 = M_2 : \Pi y \dv [\bar\Delta/\Delta]B . B'$$ But we can kind convert to $$\Gamma, \bar \Delta, \Delta \prov M_1 = M_2 : \Pi y \dv B . B'$$ and so $$\Gamma \prov M_1 = M_2 : A_2$$ by strengthening, using the observation that no variables in $\Delta,\bar \Delta$ can appear free in $M_1$ or $M_2$ by their typing. \end{itemize} \cqed \end{proof} \subsection{Local Strict Occurrences} $$\begin{prooftree} \Delta \prov S \rpat \qquad \Delta \prov S : B > C \using \ir ls_pat. \justifies \Gamma;\Delta \vv_x x \cdot S \end{prooftree}$$ $$\begin{prooftree} \Gamma ; \Delta \vv_x M \using \ir ls_hd. \justifies \Gamma ; \Delta \vv_x (M ; S) \end{prooftree} \qquad%%%%%%%%%%%%%% \begin{prooftree} \Gamma ; \Delta \vv_x S \using \ir ls_sp. \justifies \Gamma ; \Delta \vv_x (M ; S) \end{prooftree}$$ $$\begin{prooftree} \Gamma ; \Delta \vv_x S \using \ir ls_isp. \justifies \Gamma ; \Delta \vv_x (M\ \isem S) \end{prooftree}$$ $$\begin{prooftree} y : A \in \Delta \qquad \Gamma ; \Delta \vv_x S \using \ir ls_var. \justifies \Gamma ; \Delta \vv_x y \cdot S \end{prooftree}$$ $$\begin{prooftree} \Gamma ; \Delta \vv_x S \using \ir ls_a. \justifies \Gamma ; \Delta \vv_x a \cdot S \end{prooftree} \qquad%%%%%%%%%%%%%% \begin{prooftree} \Gamma ; \Delta \vv_x S \using \ir ls_c. \justifies \Gamma ; \Delta \vv_x c \cdot S \end{prooftree}$$ $$\begin{prooftree} d = M : A \in \Sigma \qquad \cdot \vv M \qquad \Gamma ; \Delta \vv_x S \using \ir ls_d. \justifies \Gamma ; \Delta \vv_x d \cdot S \end{prooftree}$$ $$\begin{prooftree} M \whr M' \qquad \Gamma; \Delta\vv_x M' \using \ir ls_red. \justifies \Gamma ; \Delta \vv_x M \end{prooftree}$$ $$\begin{prooftree} \Gamma; \Delta \vv_x A \using \ir ls_ld. \justifies \Gamma; \Delta \vv_x \lambda y : A . M \end{prooftree} \qquad%%%%%%%%%%%%%% \begin{prooftree} \Gamma; \Delta, y \star A \vv_x M \using \ir ls_lb. \justifies \Gamma; \Delta \vv_x \lambda y \star A . M \end{prooftree}$$ $$\begin{prooftree} \Gamma; \Delta \vv_x A_1 \using \ir ls_pd. \justifies \Gamma; \Delta \vv_x \Pi y : A_1 . A_2 \end{prooftree} \qquad%%%%%%%%%%%%%% \begin{prooftree} \Gamma; \Delta, y \star A_1 \vv_x A_2 \using \ir ls_pb. \justifies \Gamma; \Delta \vv_x \Pi y \star A_1 . A_2 \end{prooftree}$$ % \subsection{Strict Occurrences} $$\begin{prooftree} M \whr M' \qquad \Gamma \vv_x M' \using \ir rs_red. \justifies \Gamma \vv_x M \end{prooftree}$$ $$\begin{prooftree} d = M : A \in \Sigma \qquad \cdot \vv M \qquad \Gamma ; \cdot \vv_x S \using \ir rs_d. \justifies \Gamma \vv_x d \cdot S \end{prooftree}$$ $$\begin{prooftree} \Gamma ; \cdot \vv_x S \using \ir rs_c. \justifies \Gamma \vv_x c \cdot S \end{prooftree}$$ $$\begin{prooftree} \Gamma, y \star A \vv_x M \using \ir rs_lam. \justifies \Gamma \vv_x \lambda y \star A . M \end{prooftree}$$ % \subsection{Strictness} $$\begin{prooftree} M \whr M' \qquad \Gamma \vv M' \using \ir gs_red. \justifies \Gamma \vv M \end{prooftree}$$ $$\begin{prooftree} d = M : A \in \Sigma \qquad \cdot \vv M \qquad \Gamma \vv M \cdot S \using \ir gs_d. \justifies \Gamma \vv d \cdot S \end{prooftree}$$ $$\begin{prooftree} \using \ir gs_c. \justifies \Gamma \vv c \cdot S \end{prooftree}$$ $$\begin{prooftree} \Gamma, x : A \vv_x M \qquad \Gamma, x : A \vv M \using \ir gs_lam. \justifies \Gamma \vv \lambda x : A . M \end{prooftree}$$ $$\begin{prooftree} \Gamma, x \div A \vv M \using \ir gs_ilam. \justifies \Gamma \vv \lambda x \div A . M \end{prooftree}$$ \begin{lemma}(Completeness)\label{completeness} Let $\sigma_1, \sigma_2$ be such that $\Gamma'; \Delta' \prov \sigma_1, \sigma_2 : \Gamma; \Delta$. \begin{enumerate} \item If \begin{enumerate} \item $x : A\in \Gamma$ \item $\Gamma; \Delta \vv_x M$ \item $\Gamma, \Delta \prov M : B$ \item $\Gamma', \Delta' \prov M[\sigma_1] = M[\sigma_2] : B[\sigma_1]$ \end{enumerate} then $\Gamma'\prov \sigma_1(x) = \sigma_2(x) : A[\sigma_1]$. \item If \begin{enumerate} \item $x : A\in \Gamma$ \item $\Gamma; \Delta \vv_x B$ \item $\Gamma, \Delta \prov B : \rtype$ \item $\Gamma', \Delta' \prov B[\sigma_1] = B[\sigma_2] : \rtype$ \end{enumerate} then $\Gamma'\prov \sigma_1(x) = \sigma_2(x) : A[\sigma_1]$. \item If \begin{enumerate} \item $x : A\in \Gamma$ \item $\Gamma; \Delta \vv_x S$ \item $\Gamma, \Delta \prov S : B > C$ \item $\Gamma', \Delta' \prov S[\sigma_1] = S[\sigma_2] : B[\sigma_1] > C[\sigma_1]$ \end{enumerate} then $\Gamma'\prov \sigma_1(x) = \sigma_2(x) : A[\sigma_1]$. \item If \begin{enumerate} \item $x : A\in \Gamma$ \item $\Gamma \vv_x M$ \item $\Gamma, \Delta\prov M : B$ \item $\Gamma', \Delta' \prov S : B[\sigma_1] > C[\sigma_1]$, \item $\Gamma' \prov M[\sigma_1] \cdot S = M[\sigma_2] \cdot S : C[\sigma_1]$ \end{enumerate} then $\Gamma'\prov \sigma_1(x) = \sigma_2(x) : A[\sigma_1]$. \item If \label{completeness.final} \begin{enumerate} \item $\Gamma \vv M$ \item $\Gamma \prov M : B$ \item $\Gamma \prov S_1, S_2 : B[\sigma_1] > C[\sigma_1]$ \item $\Gamma' \prov M[\sigma_1] \cdot S_1 = M[\sigma_2] \cdot S_2 : C[\sigma_1]$ \end{enumerate} then $\Gamma'\prov S_1 = S_2 : B[\sigma_1] > C[\sigma_1]$. \end{enumerate} \end{lemma} \begin{proof} Simultaneous induction over the rules defining the $\vv$ judgments. \cqed \end{proof} \begin{theorem}(Injectivity) If $d : A = M$ is strict, i.e. $\cdot \vv M$, then $d$ is injective. (as in \cite{strictness}) \end{theorem} \begin{proof} Follows immediately from Lemma~\ref{completeness}~(\ref{completeness.final}), with $\sigma_1,\sigma_2$ both the identity substitution. \cqed \end{proof} \bibliographystyle{alpha} \bibliography{id} \end{document} $$\begin{prooftree} \Delta^\square \prov S \rpat \using \ir pat_iic. \justifies \Delta^\square, x \div \square \prov (x\ \isem S) \rpat \end{prooftree} \qquad \begin{prooftree} \Delta^\square, x \div \square \prov S \rpat \using \ir pat_iic2. \justifies \Delta^\square, x \div \square \prov (x\ \isem S) \rpat \end{prooftree}$$ $$\begin{prooftree} \Delta^\square \prov S \rpat \using \ir pat_c. \justifies \Delta^\square, x : \square \prov (x; S) \rpat \end{prooftree}$$ $$\begin{prooftree} \Delta^\square \prov S \rpat \using \ir pat_ic. \justifies \Delta^\square, x : \square \prov (x\ \isem S) \rpat \end{prooftree} \qquad \begin{prooftree} \Delta^\square, x : \square \prov S \rpat \using \ir pat_ic2. \justifies \Delta^\square, x : \square \prov (x\ \isem S) \rpat \end{prooftree}$$ $$\Gamma, x \div A', x'\div A' \prov [x/z][x'/x]M_1' = [x/z][x'/x]M_2' : [x/z]B'$$ and, knowing that there are no free occurrences of $x$ in $[x'/x]M_1'$ or $[x'/x]M_2'$, we can infer $$\Gamma, x'\div A' \prov \lambda x\dv A' . [x/z][x'/x]M_1' = \lambda x \dv A' . [x/z][x'/x]M_2'$$ $$\qquad : \Pi x \dv A' . [x/z][x'/x]B'$$ and then $\alpha$-convert to $$\Gamma, x'\div A' \prov \lambda z\dv A' . [x'/x]M_1' = \lambda z \dv A' . [x'/x]M_2' : \Pi z \dv A' . [x'/x]B'$$ and finally conclude $$\Gamma, x\div A' \prov \lambda z\dv A' . M_1' = \lambda z \dv A' . M_2' : \Pi z \dv A' . B'$$ or in other words $$\Gamma \prov M_1 = M_2 : A$$