add proof splitting and type injectivity sections

Author: digama0

main.tex

@@ -22,6 +22,7 @@
 \renewcommand{\P}{\mathbb{P}}
 \newcommand{\ctx}{\;\mathsf{ctx}}
 \newcommand{\scott}[1]{\llbracket #1\rrbracket}
+\newcommand{\ttag}[1]{\llparenthesis #1\rrparenthesis}
 \newcommand{\elet}[2]{\mathsf{let}\;#1\mathrel{\mathsf{in}}#2}
 \newcommand{\rec}{\mathsf{rec}}
 \newcommand{\ok}{\ \mathsf{ok}}
@@ -46,6 +47,7 @@
 \newcommand{\nonempty}{\mathsf{nonempty}}
 \newcommand{\refl}{\mathsf{refl}}
 \newcommand{\lvl}{\operatorname{lvl}}
+\newcommand{\sort}{\operatorname{sort}}
 \newcommand{\rank}{\operatorname{rank}}
 \DeclareMathOperator{\imax}{imax}
 \let\lGamma\Gamma \renewcommand{\Gamma}{\mathrm{\lGamma}}

normalization.tex

@@ -1,9 +1,21 @@
 \section{Strong normalization}
 \subsection{Evaluation in the empty context}
 In \autoref{sec:church_rosser}, we set up a reduction relation $\rightsquigarrow_\kappa$ which is plainly useless for a normalization algorithm, because of the following rule:
-$$(K)\ \frac{P\mbox{ is SS inductive}}{\Gamma\vdash \rec_P(C,e,p,h)\rightsquigarrow_\kappa e\;\inv[p,h]\;v}$$
-Recall that $v$ is a sequence of lambdas $v_i=\lambda x::\xi_i.\;\rec_P(C,e,\pi_i[\inv[p,h],x],u_i\;x)$. That is, we reduce any $\rec_P$ term, regardless of its arguments, to a longer expression that contains another $\rec_P$ term (assuming that the inductive type has a recursive argument). So this is guaranteed not to terminate, but it was sufficiently powerful to act as a semi-decision procedure for definitional equality where existing methods fail (by giving up early, they recover decidability at the cost of completeness).
+$$(K^+)\ \frac{P\mbox{ is SS inductive}\quad\Gamma\vdash \intro\;\inv[p,h]:\alpha}{\Gamma\vdash \rec_P\;C\;e\;p\;h\rightsquigarrow_\kappa e\;\inv[p,h]\;v}$$
+Recall that $v$ is a sequence of lambdas $v_i=\lambda x::\xi_i.\;\rec_P(C,e,\pi_i[\inv[p,h],x],u_i\;x)$. That is, we reduce any $\rec_P$ term, regardless of its arguments, to a longer expression that contains another $\rec_P$ term (assuming that the inductive type has a recursive argument). If the embedded $\rec_P$ term in $v$ is also susceptible to the $K^+$ reduction (which is quite often the case), then this will not terminate, but it was sufficiently powerful to act as a semi-decision procedure for definitional equality where existing methods fail (by giving up early, they recover decidability at the cost of completeness).
 
-But our examples thus far of undecidability of definitional equality all work in an inconsistent context. Is this necessary? What if the context is known to be inhabited by some terms? In this case we may as well substitute the terms in to reduce the problem to evaluation in the empty context.
+Let us scale back the $K^+$ rule, then, to the original $K$ rule, which is the same as $K^+$ except that it only applies if no $\inv_i$ terms are produced on the RHS. We will also reinstate the standard $\iota$ rule for subsingleton inductives as well. We will call the resulting reduction relation $\rightsquigarrow_\sigma$.
 
-That is, we wish to determine if $\vdash e\equiv e'$, hopefully by a method similar to the reduction $\rightsquigarrow_\kappa$, but without the self-destructive unfolding K rule.
+$$\boxed{\Gamma\vdash e\rightsquigarrow_\sigma e'}\qquad
+\frac{\Gamma\vdash e_1 \rightsquigarrow_\sigma e_1'}{\Gamma\vdash e_1\;e_2\rightsquigarrow_\sigma e_1'\;e_2}\qquad
+\frac{\Gamma\vdash e_2 \rightsquigarrow_\sigma e_2'}{\Gamma\vdash e_1\;e_2\rightsquigarrow_\sigma e_1\;e_2'}$$
+$$\frac{\Gamma\vdash \alpha \rightsquigarrow_\sigma\alpha'}{\Gamma\vdash \lambda x:\alpha.\;e\rightsquigarrow_\sigma \lambda x:\alpha'.\;e}\qquad
+\frac{\Gamma,x:\alpha\vdash e \rightsquigarrow_\sigma e'}{\Gamma\vdash \lambda x:\alpha.\;e\rightsquigarrow_\sigma \lambda x:\alpha.\;e'}\qquad\dots$$
+$$(\beta)\ \frac{}{\Gamma\vdash (\lambda x:\alpha.\;e)\;e'\rightsquigarrow_\sigma e[e'/x]}\qquad
+(\delta)\ \frac{\mathsf{def}\;c:\alpha:=e}{\Gamma\vdash c\rightsquigarrow_\sigma e}\qquad
+(\zeta)\ \frac{}{\Gamma\vdash \elet{x:\alpha:=e'}{e}\rightsquigarrow_\sigma e[e'/x]}$$
+$$(\iota)\ \frac{P\mbox{ is inductive with ctor }c}{\Gamma\vdash \rec_P\;C\;e\;p\;(c\;b)\rightsquigarrow_\sigma e_c\;b\;v}\qquad
+(\iota_q)\ \frac{}{\Gamma\vdash \lift\;R\;f\;h\;(\mk_R\;a)\rightsquigarrow_\sigma f\;a}$$
+$$(K)\ \frac{P\mbox{ is SS inductive}\quad\inv_i\notin\inv[p]\quad\Gamma\vdash \intro\;\inv[p]:\alpha}{\Gamma\vdash \rec_P\;C\;e\;p\;h\rightsquigarrow_\sigma e\;\inv[p]\;v}$$
+
+We have indicated that $\inv$ consists only of $p_i$ terms and not $\inv_i\;h$ by the notation $\inv_i\notin\inv[p]$.