Getting Started
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 new book by Y. Bertot and P. Castéran on practical uses of the Coq system.

Coq can be used from a standard teletype-like shell window but preferably through the graphical user interface CoqIde1.

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

In the following, we assume that Coq  is called from a standard teletype-like shell window. All examples preceded by the prompting sequence Coq < represent user input, terminated by a period.

The following lines usually show Coq's answer as it appears on the users screen. 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.

The sequence of such examples is a valid Coq  session, unless otherwise specified. This version of the tutorial has been prepared on a PC workstation running Linux. The standard invocation of Coq delivers a message such as:

unix:~> coqtop
Welcome to Coq x.x

Coq < 

The first line gives a banner stating the precise version of Coq  used. You should always return this banner when you report an anomaly on our bug-tracking system:

1 Alternative graphical interfaces exist: Proof General and Pcoq.