Coq is a proof assistant based on the Calculus of Inductive Constructions.
Coq is notable for being based on tactics. Instead of writing a term in type theory itself, the user uses a tactic, which builds a term in stages. The behaviour of tactics may range from simple term-building steps (i.e. intro
to introduce a -abstraction) to fully automated proof construction (e.g. decision procedures such as lia
or tauto
).
Coq supports three kinds of universes:
Prop
, an impredicative universe of propositionsSet
, a predicative universe of small typesType
, a predicative universe of large typesHistorically, Set
used to also be impredicative. This was changed in version 8.0 due to the incompatibility of impredicativity with various axioms of mainstream mathematics and classical logic. This is explained in detail in a GitHub wiki post by Pierre-Marie Pédrot.
There are at least two introductory books based on Coq: