The Coq Proof Assistant

Coq is a Proof Assistant for a Logical Framework known as the Calculus of Inductive Constructions. It allows the interactive construction of formal proofs, and also the manipulation of functional programs consistently with their specifications. It runs as a computer program on many architectures.

It is available with a variety of user interfaces. The present document does not attempt to present a comprehensive view of all the possibilities of Coq, but rather to present in the most elementary manner a tutorial on the basic specification language, called Gallina, in which formal axiomatisations may be developed, and on the main proof tools. For more advanced information, the reader could refer to the Coq Reference Manual or the Coq’Art, a book by Y. Bertot and P. Castéran on practical uses of the Coq system.

Instructions on installation procedures, as well as more comprehensive documentation, may be found in the standard distribution of Coq, which may be obtained from Coq web site https://coq.inria.fr/¹. Coq is distributed together with a graphical user interface called CoqIDE. Alternative interfaces exist such as Proof General².

In the following examples, lines preceded by the prompt Coq < represent user input, terminated by a period. The following lines usually show Coq’s answer. When used from a graphical user interface such as CoqIDE, the prompt is not displayed: user input is given in one window and Coq’s answers are displayed in a different window.

1

You can report any bug you find while using Coq at https://coq.inria.fr/bugs. Make sure to always provide a way to reproduce it and to specify the exact version you used. You can get this information by running coqc -v

2

See https://proofgeneral.github.io/.