Gabriel's suggestions

axioms.tex

@@ -68,27 +68,16 @@ \subsection{Reduction}
 \frac{\ell\equiv\ell'}{\Gamma\vdash\U_\ell\Leftrightarrow\U_\ell'}$$
 $$\frac{\Gamma\vdash\alpha\Leftrightarrow\alpha'\quad \Gamma,x:\alpha\vdash e\Leftrightarrow e'}{\Gamma\vdash\lambda x:\alpha.\;e\Leftrightarrow \lambda x:\alpha'.\;e'}\qquad
 \frac{\Gamma\vdash\alpha\Leftrightarrow\alpha'\quad \Gamma,x:\alpha\vdash e\Leftrightarrow e'}{\Gamma\vdash\forall x:\alpha.\;e\Leftrightarrow \forall x:\alpha'.\;e'}$$
-$$\frac{}{\Gamma\vdash \lambda x:\alpha.\;e\;x\Leftrightarrow e}\qquad
+$$\frac{\Gamma\vdash e:\forall x:\alpha.\;\beta\quad\Gamma,x:\alpha\vdash e\;x\leftrightarrow e'\;x}{\Gamma\vdash e\Leftrightarrow e'}\qquad
 \frac{\Gamma\vdash p:\P\quad \Gamma\vdash h:p\quad \Gamma\vdash h':p'\quad \Gamma \vdash p\Leftrightarrow p'}{\Gamma \vdash h\Leftrightarrow h'}$$
 $$\frac{\Gamma\vdash e_1\Leftrightarrow e'_1\quad \Gamma\vdash e_2\Leftrightarrow e'_2}{\Gamma\vdash e_1\;e_2\Leftrightarrow e'_1\;e'_2}\qquad
-\frac{e\downarrow k\quad e'\downarrow k'\quad \Gamma\vdash k\Leftrightarrow k'}{\Gamma\vdash e\Leftrightarrow e'}$$
+\frac{e\rightsquigarrow k\quad \Gamma\vdash k\Leftrightarrow e'}{\Gamma\vdash e\Leftrightarrow e'}$$
 
-In this judgment the transitivity rule is notably absent. Most of the congruence rules remain except for the $\beta$ rule, and these constitute all the ``easy'' cases of definitional equality. When the other rules fail to make progress, we use the ``weak head normal form'' reduction $e\downarrow k$ to apply the $\beta$ rule as well as the $\delta,\iota,\zeta$ rules which are discussed in their own section.
+In this judgment the transitivity rule is notably absent. Most of the congruence rules remain except for the $\beta$ rule, and these constitute all the ``easy'' cases of definitional equality. The $\eta$ rule is replaced with an extensionality principle. (This is justified because if $e\;x\equiv e'\;x$ then $\lambda x:\alpha.\;e\;x\equiv \lambda x:\alpha.\;e'\;x$, so $e\equiv e'$ by the $\eta$ rule.) When the other rules fail to make progress, we use the head reduction relation $e\rightsquigarrow^* k$ to apply the $\beta$ rule as well as the $\delta,\iota,\zeta$ rules which are discussed in their own section.
 %
-$$
-\begin{matrix}
-\boxed{e\downarrow k}\\[4mm]
-\displaystyle{
-\frac{e\rightsquigarrow e'\quad e'\downarrow k}{e\downarrow k}\qquad
-\frac{e\not\rightsquigarrow}{e\downarrow e}}
-\end{matrix}\qquad
-\begin{matrix}
-\boxed{e\rightsquigarrow e'}\\[4mm]
-\displaystyle{
+$$\boxed{e\rightsquigarrow e'}\qquad
 \frac{e_1\rightsquigarrow e'_1}{e_1\;e_2\rightsquigarrow e'_1\;e_2}\qquad
-\frac{}{(\lambda x:\alpha.\;e)\;e'\rightsquigarrow e[e'/x]}}
-\end{matrix}
-$$
+\frac{}{(\lambda x:\alpha.\;e)\;e'\rightsquigarrow e[e'/x]}$$
 
 We will add more rules to this list as we introduce new constructs, but this completes the description of the base dependent type theory foundation for Lean.
 
@@ -222,8 +211,8 @@ \subsubsection{The computation rule ($\iota$ reduction)}
 This rule only applies when all the variables in $b$ are actually on the LHS, which is the reason for the peculiar requirements on K-like eliminators. If $b_i$ appears in the parameters for its type, that means that $p_j[b]=b_i$ for some $j$, and so $b_i$ is on the LHS. 
 
 The foremost example of this is known in the literature as axiom K, which is the reason for the name ``K-like eliminator'', which is this principle applied to the equality type:
-$$\mathsf{rec}_{\mathsf{eq}a}\;C\;x\;a\;h\equiv x$$
-Here $\mathsf{rec}_{\mathsf{eq}a}\;C:a=b\to C\;a\to C\;b$ is the substitution principle of equality (suppressing the dependence of $C$ on the proof argument), and the computation rule says that ``casting'' $x:C\;a$ over an equality $h:a=a$ produces $x$ again.
+$$\mathsf{rec}_{a=}\;C\;x\;a\;h\equiv x$$
+Here $\mathsf{rec}_{a=}\;C:a=b\to C\;a\to C\;b$ is the substitution principle of equality (suppressing the dependence of $C$ on the proof argument), and the computation rule says that ``casting'' $x:C\;a$ over an equality $h:a=a$ produces $x$ again.
 %
 \subsection{Non-primitive axioms}
 

typesys.tex

@@ -73,7 +73,6 @@ \subsection{Regularity}
 \item If $\Gamma\vdash e:\alpha$, then $\Gamma\vdash\alpha\type$.
 \item\label{item:defeq_reg2} If $\Gamma\vdash e\equiv e'$, then there exists $\alpha,\alpha'$ such that $\Gamma\vdash e:\alpha$ and $\Gamma\vdash e':\alpha'$.
 \item If $\Gamma\vdash e:\alpha$ and $e\rightsquigarrow e'$, then $\Gamma\vdash e\equiv e'$.
-\item If $\Gamma\vdash e:\alpha$ and $e\downarrow k$, then $\Gamma\vdash e\equiv k$.
 \item\label{item:alg_defn} If $\Gamma\vdash e:\alpha$ and $\Gamma\vdash e':\alpha$, and $\Gamma\vdash e\Leftrightarrow e'$, then $\Gamma\vdash e\equiv e'$.
 \item If $\Gamma;t:F\vdash K\spec$, then $\Gamma\vdash F\type$ (and more precisely, $F=\forall x::\alpha.\;\U_\ell$ for some $\alpha,\ell$).
 \item If $\Gamma;t:F\vdash K\spec$ and $(c:\alpha)\in K$, then $\Gamma;t:F\vdash\alpha\ctor$.
@@ -349,11 +348,7 @@ \subsection{The Church-Rosser theorem}\label{sec:church_rosser}
 \item If $\lambda y:\beta^\bullet.\;e^\bullet\lll_\kappa\lambda x:\alpha.\;(\lambda y:\beta.\;e)\;h\gg_\kappa \lambda x:\alpha'.\;e'[h/y]$ by the lambda rule and beta rule, then $\lambda x:\alpha'.\;e'[h/y]\gg_\kappa \lambda x:\alpha^\circ.\;e^\circ[h/y]\equiv_p$\\$\lambda x:\beta^\bullet.\;e^\bullet[x/y]=\lambda y:\beta^\bullet.\;e^\bullet$. (Here we have used the $\lambda$ rule for $\equiv_p$ to equate $\alpha^\circ\equiv\beta^\bullet$, which are def.eq. because $\alpha$ and $\beta$ are.)
 \end{itemize}
 \item If $e^\bullet\lll_\kappa c\gg_\kappa e'$ by the delta rule, then $e'\gg_\kappa e^\circ\equiv_p e^\bullet$.
-\item If $e\ggg_\kappa e^\bullet$ by the zeta rule:
-\begin{itemize}
 \item If $e_1^\bullet[e_2^\bullet/x]\lll_\kappa\elet{x:\alpha:=e_1}{e_2}\gg_\kappa e_2'[e_1'/x]$ by the zeta rule, then $e_1'[e_2'/x]\gg_\kappa e_1^\circ[e_2^\circ/x]\equiv_p e_1^\bullet[e_2^\bullet/x]$.
-\item If $e_1^\bullet[e_2^\bullet/x]\lll_\kappa\elet{x:\alpha:=e_1}{e_2}\gg_\kappa \elet{x:\alpha':=e_1'}{e_2'}$ by the let compatibility rule, then $\elet{x:\alpha':=e_1'}{e_2'}\gg_\kappa e_1^\circ[e_2^\circ/x]\equiv_p e_1^\bullet[e_2^\bullet/x]$ by the zeta rule.
-\end{itemize}
 \item If $e\ggg_\kappa e^\bullet$ by the non-K inductive iota rule:
 \begin{itemize}
 \item If $e_c^\bullet\;b^\bullet\;v^\bullet\lll_\kappa \rec_P(C,e,p,c\;b)\gg_\kappa e_c'\;b'\;v'$ by the iota rule, then $e_c'\;b'\;v'\gg_\kappa e_c^\circ\;b^\circ\;v^\circ\equiv_p e_c^\bullet\;b^\bullet\;v^\bullet$.