intro and coq comparison

Wtypes.tex

@@ -1,4 +1,4 @@
-\section{Reduction of inductive types to $\W$-types}
+\section{Reduction of inductive types to $\W$-types}\label{sec:wtype}
 
 Given the complicated structure involved in simply stating the axioms of inductive types, one may wonder if there is an easier way. In fact there is; we can replace the whole structure of inductive types with a few simple inductive type constructors.
 

abstract.tex

@@ -1,8 +1,8 @@
 \section*{Abstract}
 % \addcontentsline{toc}{chapter}{abstract}
 
-This thesis is a presentation of dependent type theory with inductive types, a hierarchy of universes, with an impredicative universe of propositions, proof irrelevance, and subsingleton elimination, along with axioms for propositional extensionality, quotient types, and the axiom of choice. This theory is notable for being the axiomatic framework of the Lean theorem prover. The axiom system is given here in complete detail, including ``optional'' features of the type system such as $\mathsf{let}$ binders and definitions. We provide a reduction of the theory to a finitely axiomatized fragment utilizing a fixed set of inductive types (the $\W$ -type plus a few others), to ease the study of this framework.
+This thesis is a presentation of dependent type theory with inductive types, a hierarchy of universes, with an impredicative universe of propositions, proof irrelevance, and subsingleton elimination, along with axioms for propositional extensionality, quotient types, and the axiom of choice. This theory is notable for being the axiomatic framework of the Lean theorem prover. The axiom system is given here in complete detail, including ``optional'' features of the type system such as $\mathsf{let}$ binders and definitions. We provide a reduction of the theory to a finitely axiomatized fragment utilizing a fixed set of inductive types (the $\W$-type plus a few others), to ease the study of this framework.
 
-The metatheory of this theory (which we will call Lean) is studied. In particular, we prove unique typing of the definitional equality, and use this to construct the expected set-theoretic model, from which we derive consistency of Lean relative to ZFC with $n$ inaccessible cardinals for all $n<\omega$ (a relatively weak large cardinal assumption). As Lean supports models of ZFC with $n$ inaccessible cardinals, this is optimal.
+The metatheory of this theory (which we will call Lean) is studied. In particular, we prove unique typing of the definitional equality, and use this to construct the expected set-theoretic model, from which we derive consistency of Lean relative to $\mathsf{ZFC}+\{\mbox{there are }n\mbox{ inaccessible cardinals}\mid n<\omega\}$ (a relatively weak large cardinal assumption). As Lean supports models of ZFC with $n$ inaccessible cardinals, this is optimal.
 
 We also show a number of negative results, where the theory is less nice than we would like. In particular, type checking is undecidable, and the type checking as implemented by the Lean theorem prover is a decidable non-transitive underapproximation of the typing judgment. Non-transitivity also leads to lack of subject reduction, and the reduction relation does not satisfy the Church-Rosser property, so reduction to a normal form does not produce a decision procedure for definitional equality. However, a modified reduction relation allows us to restore the Church-Rosser property at the expense of guaranteed termination, so that unique typing is shown to hold.

axioms.tex

@@ -1,4 +1,4 @@
-\section{The axioms}
+\section{The axioms}\label{sec:axioms}
 
 \subsection{Typing}
 
@@ -244,3 +244,36 @@ \subsubsection{Axiom of choice}
 From the axiom of choice, the law of excluded middle is derived (it is not stated as a separate axiom).
 
 \subsection{Differences from \textsf{Coq}}\label{sec:notcoq}
+As mentioned in the introduction, Coq is a theorem prover also based on the Calculus of Constructions with inductive types (CIC), and it is quite old and well studied \cite{barrassets, barrastypedec, coqincoq, coquandcoc, lee2011, ecc, notsosimple}. So a natural question is to what degree Lean and CIC are similar, and whether proofs that apply to one system generalize, straightforwardly or otherwise, to the other. See \cite{lee2011} for a concise description of the proof theory of CIC. The following is a summary of differences with Lean's axiomatization, and their effects on the theorems here:
+
+\begin{enumerate}
+\item Coq has universe cumulativity. That is, the definitional equality relation is replaced by a cumulativity relation $\preceq$ that is roughly the same, except that $\Gamma\vdash\U_i\preceq \U_j$ when $i\le j$. This breaks the unique typing theorem \autoref{thm:unique}, and it is not clear whether there is an adequate replacement in conjunction with all the other axioms of Lean. Luo \cite{ecc} shows that a large subset of CIC including cumulative universes retains good type theoretic properties, including strong normalization, from which an analogue of unique typing can be derived.
+\item Gallina, the underlying core syntax of Coq, uses primitives $\mathsf{fix}$ and $\mathsf{match}$ to implement inductive types, rather than $\mathsf{rec}$ as is done here, and this is difference usually reflected in theoretical presentations as well. The difference is that while $\mathsf{rec}$ performs structural recursion over an inductive type, $\mathsf{fix}$ performs unbounded recursion, while $\mathsf{match}$ does (primitive) pattern matching over inductive types. In order to prevent infinite recursion and inconsistency as a result, the body of a $\mathsf{fix}$ must be typechecked with a modified typing judgment to ensure that all recursive calls are to elements generated by a $\mathsf{match}$ on the input.
+
+While in theory these approaches are equivalent, the $\mathsf{fix}$/$\mathsf{match}$ approach is more expressive, and the equivalence is sensitive to the exact rules available in both systems. Lean addresses this mismatch by allowing definitions using (effectively) $\mathsf{fix}$ and $\mathsf{match}$ at the user level, and compiling these away to recursors in the kernel language.
+
+\item Definitions in Lean are universe polymorphic, in the sense that they may contain free universe variables that are implicitly universally quantified at the point of definition, and applications of the constants include substitutions for all the universe variables involved in the definition. Coq definitions live in ``indefinite universes'' -- that is, each constant lives in a concrete universe but the level of this universe is held variable globally over the whole database, and using constants together generates level inequalities as side conditions that are maintained as a partial order. Coq reports an error if this order becomes inconsistent, i.e. there is no assignment of natural numbers to these variables that respects all the side conditions.
+
+There are Lean terms that cannot be checked in Coq with this approach, because Lean can reuse the same constant at two different levels while Coq has to resolve both instances of the constant to the same level. But this does not affect the set of provable theorems, since ``universe polymorphism is a luxury''; for a concrete theorem at a fixed universe level we may make duplicates of Coq constants as necessary to represent different instantiations of Lean constants.
+
+\item Coq inductive types allow ``non-uniform parameters''. These are parameters that vary subject to the restriction that they appear as is in each constructor's target type. These can be encoded using regular inductive types.
+
+\item Coq also supports mutual inductives, nested inductive types, and coinductive types. These can all be encoded using regular inductives, although some definitional equalities may fail to hold in the encodings.
+
+\item On the other hand, Lean supports definitional proof irrelevance, while Coq merely has an axiom that asserts this as a propositional equality. This is a major departure for the theory, and the reason why the counterexamples in \autoref{sec:undecidable} don't work in Coq.
+
+\item Lean supports quotient types with a definitional reduction rule, but Coq doesn't. The Coq ecosystem has compensated for this by using \emph{setoids} in place of types in many places, which are types with a designated equivalence relation that plays the role of equality. Although we have not investigated this, it should be possible to eliminate quotients from Lean entirely by using setoids instead. (There are good ergonomic reasons to have quotient types though, lest we end up in ``setoid hell''.)
+
+\item Lean offers (and de facto uses) three axioms, for propositional extensionality, quotient types and the axiom of choice. Coq has a comparatively large list of common axioms:
+\begin{itemize}
+  \item Proof irrelevance and axiom K are propositional versions of Lean's definitional proof irrelevance. They hold in Lean ``with no axioms''.
+  \item Propositional extensionality is the same in Coq and Lean.
+  \item Functional extensionality is proven in Lean as a consequence of propositional extensionality and quotient types.
+  \item Coq has many variations on the law of excluded middle -- $P\lor\neg P$, $P=\mathsf{true}\lor P=\mathsf{false}$, and $P+\neg P$ (using a sum type). The first is excluded middle, the second is propositional degeneracy, which follows from excluded middle and propositional extensionality, and the third follows from excluded middle and the axiom of choice. In Lean all of these are proven using the axiom of choice.
+  \item The axiom of choice can be stated as $(\forall x,\exists y,R(x,y))\to(\exists f,\forall x,R(x,f(x)))$ or\\
+  $\exists f,\forall x,(\exists y,R(x,y))\to R(x,f(x))$. These assert the existence of choice functions over limited domains, which is of course implied by a global choice function as with Lean's $\mathsf{choice}:\nonempty\;\alpha\to\alpha$.
+  \item Indefinite description, $(\exists x, P(x))\to\Sigma x, P(x)$, is equivalent to Lean's $\mathsf{choice}$.
+  \item Hilbert's epsilon, $\epsilon:(\alpha\to\mathsf{Prop})\to \alpha$ such that $(\exists x,P(x))\to P(\epsilon(P))$, is also equivalent to $\mathsf{choice}$.
+\end{itemize}
+So all of Coq's axioms taken together are implied by Lean's axioms, and the converse is true except for definitional proof irrelevance and a computation rule for quotient types. (One can build set-quotients in Coq as well as Lean, but they lack the computation rule.)
+\end{enumerate}