Introduction
Introduction
This document is the Reference Manual of version V6.2 of the Coq proof assistant. A companion volume, the Coq Tutorial, is provided
for the beginners. It is advised to read the Tutorial first.
The system Coq is designed to write formal specifications,
programs and to verify that programs are correct with respect to their
specification. It provides a specification language named Gallina. Terms of
Gallina can represent programs as well as properties of these
programs and proofs of these properties. Using the so-called
Curry-Howard isomorphism, programs, properties and proofs are
formalized the same
language called Calculus of Inductive Constructions, that is
a l-calculus with a rich type system.
All logical judgments in Coq are typing judgments. The very heart of the Coq
system is the type-checking algorithm that checks the correctness of
proofs, in other words that checks that a program complies to its
specification. Coq also provides an interactive proof assistant to
build proofs using specific programs called tactics.
All services of the Coq proof assistant are accessible by
interpretation of a command language called the vernacular.
Coq has an interactive mode in which commands are interpreted as the
user types them in from the keyboard and a compiled mode where
commands are processed from a file. Other modes of interaction with
Coq are possible, through an emacs shell window, or through a
customized interface with the Centaur environment (CTCoq). These
facilities are not documented here.
-
The interactive mode may be used as a debugging mode in which
the user can develop his theories and proofs step by step,
backtracking if needed and so on. The interactive mode is run with
the coqtop command from the operating system (which we shall
assume to be some variety of UNIX in the rest of this document).
- The compiled mode acts as a proof checker taking a file
containing a whole development in order to ensure its correctness.
Moreover, Coq's compiler provides an output file containing a
compact representation of its input. The compiled mode is run with
the coqc command from the operating system. Its use is
documented in chapter 11.
Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.x.0.html at 8/10/98