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 http://coq.inria.fr/.

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

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:

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: http://logical.saclay.inria.fr/coq-bugs/index.cgi.

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 http://coq.inria.fr/.

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: http://logical.saclay.inria.fr/coq-bugs/index.cgi.

- 1 Alternative graphical interfaces exist: Proof General and Pcoq.