The Coq Proof Assistant

3.1  Opening library modules

When you start Coq without further requirements in the command line, you get a bare system with few libraries loaded. As we saw, a standard prelude module provides the standard logic connectives, and a few arithmetic notions. If you want to load and open other modules from the library, you have to use the Require command, as we saw for classical logic above. For instance, if you want more arithmetic constructions, you should request:

Such a command looks for a (compiled) module file Arith.vo in the libraries registered by Coq. Libraries inherit the structure of the file system of the operating system and are registered with the command Add LoadPath. Physical directories are mapped to logical directories. Especially the standard library of Coq is pre-registered as a library of name Coq. Modules have absolute unique names denoting their place in Coq libraries. An absolute name is a sequence of single identifiers separated by dots. E.g. the module Arith has full name Coq.Arith.Arith and because it resides in eponym subdirectory Arith of the standard library, it can be as well required by the command

This may be useful to avoid ambiguities if somewhere, in another branch of the libraries known by Coq, another module is also called Arith. Notice that by default, when a library is registered, all its contents, and all the contents of its subdirectories recursively are visible and accessible by a short (relative) name as Arith. Notice also that modules or definitions not explicitly registered in a library are put in a default library called Top.

The loading of a compiled file is quick, because the corresponding development is not type-checked again.

3.2  Creating your own modules

You may create your own module files, by writing Coq commands in a file, say my_module.v. Such a module may be simply loaded in the current context, with command Load my_module. It may also be compiled, in “batch” mode, using the UNIX command coqc. Compiling the module my_module.v creates a file my_module.vo that can be reloaded with command Require Import my_module.

If a required module depends on other modules then the latters are automatically required beforehand. However their contents is not automatically visible. If you want a module M required in a module N to be automatically visible when N is required, you should use Require Export M in your module N.

3.3  Managing the context

It is often difficult to remember the names of all lemmas and definitions available in the current context, especially if large libraries have been loaded. A convenient Search command is available to lookup all known facts concerning a given predicate. For instance, if you want to know all the known lemmas about both the successor and the less or equal relation, just ask:

Another command SearchHead displays only lemmas where the searched predicate appears at the head position in the conclusion.

The Search commands also allows finding the theorems containing a given pattern, where _ can be used in place of an arbitrary term. As shown in this example, Coq provides usual infix notations for arithmetic operators.

3.4  Now you are on your own

This tutorial is necessarily incomplete. If you wish to pursue serious proving in Coq, you should now get your hands on Coq’s Reference Manual, which contains a complete description of all the tactics we saw, plus many more. You also should look in the library of developed theories which is distributed with Coq, in order to acquaint yourself with various proof techniques.