Why doesn't Coq have a theorem Type like HOL Light?

Miscellaneous
4

I’ll take this opportunity to compare some aspects of Coq and HOL, for future reference. There will inevitably be some overlap with answers in related threads.

  • Coq is based on dependent types and is inspired by Martin-Löf’s type theories from the 1970s. HOL builds on Church’s extensions to the lambda-calculus, in the form of simple types, from the 1930s. A basic distinction between Coq’s and HOL’s foundations is that the former allows types to be directly parameterized on terms, while the latter does not. The paradigmatic example is a type representing a vector space over real numbers, which in Coq may directly depend on a natural number for the dimension; in HOL the encoding must be less direct.

  • The propositions-as-types principle was important to Coq’s designers, and means that proofs (most directly, terms of types that live in Prop) are in principle built and processed in the same way as other terms, such as terms representing programs. In contrast, HOL proofs are essentially lists of Gentzen-style sequents and are exposed only indirectly at the metalanguage level, i.e., not as transparent objects in their own right.

  • Coq proofs (proof objects) are usually built and stored in full and are reasonably tractable to view thanks to support for purely computational reasoning steps. In contrast, HOL proofs are typically huge, do not contain implicit computation, and are almost never built in full or inspected by users.

  • Coq’s logic is constructive (intuitionistic) and its functions are computable by default. HOL’s classical logic conflates booleans and propositions and permits functions that aren’t computable or even fully specified. The SSReflect proof language and MathComp library for Coq can be viewed as reinstating boolean-based reasoning of the kind done by HOL users for dependent type theory.

  • Classical choice (of inhabitants in types) is included in HOL in the form of Hilbert’s epsilon operator, and key to this is that all HOL types are inhabited. In contrast, non-inhabited types such as False are central to Coq, and there is no classical choice without adding axioms.

  • HOL has a relatively straightforward interpretation (semantics) in terms of ZFC set theory, while Coq’s metatheory is much more involved, as can be seen in this thread.

For references on the implementation architecture of Coq, see this post and other replies in that thread.

3 Likes