Tutorial

The Coq Proof AssistantA TutorialFebruary 11, 20091Version 8.2Gérard Huet, Gilles Kahn and Christine Paulin-MohringTypiCal Project (formerly LogiCal)1This research was partly supported by IST working group “Types”V8.2, February 11, 2009c INRIA 1999-2004 (COQ versions 7.x)c 2004-2009 (COQ v 8.x)Getting startedCOQ is a Proof Assistant for a Logical Framework known as the Calculus of Induc-tive Constructions. It allows the interactive construction of formal proofs, and alsothe manipulation of functional programs consistently with their specifications. Itruns as a computer program on many architectures. It is available with a variety ofuser interfaces. The present document does not attempt to present a comprehensiveview of all the possibilities of COQ, but rather to present in the most elementarymanner a tutorial on the basic specification language, called Gallina, in which for-mal axiomatisations may be developed, and on the main proof tools. For moreadvanced information, the reader could refer to the COQ Reference Manual or theCoq’Art, a new book by Y. Bertot and P. Castéran on practical uses of the COQsystem.Coq can be used from a standard teletype-like shell window but preferably1through the graphical user interface CoqIde .Instructions on installation procedures, as well as more comprehensive docu-mentation, may be found in the standard distribution of COQ, which may be ob-tained from COQ web sitehttp://coq.inria.fr.In the following, we assume ...