Chapter 14 Utilities

The distribution provides utilities to simplify some tedious works beside proof development, tactics writing or documentation.

14.1 Building a toplevel extended with user tactics

The native-code version of Coq cannot dynamically load user tactics using Objective Caml code. It is possible to build a toplevel of Coq, with Objective Caml code statically linked, with the tool coqmktop.

For example, one can build a native-code Coq toplevel extended with a tactic which source is in tactic.ml with the command

     % coqmktop -opt -o mytop.out tactic.cmx

where tactic.ml has been compiled with the native-code compiler ocamlopt. This command generates an executable called mytop.out. To use this executable to compile your Coq files, use coqc -image mytop.out.

A basic example is the native-code version of Coq (coqtop.opt), which can be generated by coqmktop -opt -o coqopt.opt.

Application: how to use the Objective Caml debugger with Coq.

One useful application of coqmktop is to build a Coq toplevel in order to debug your tactics with the Objective Caml debugger. You need to have configured and compiled Coq for debugging (see the file INSTALL included in the distribution). Then, you must compile the Caml modules of your tactic with the option -g (with the bytecode compiler) and build a stand-alone bytecode toplevel with the following command:

% coqmktop -g -o coq-debug <your .cmo files>

To launch the Objective Caml debugger with the image you need to execute it in an environment which correctly sets the COQLIB variable. Moreover, you have to indicate the directories in which ocamldebug should search for Caml modules.

A possible solution is to use a wrapper around ocamldebug which detects the executables containing the word coq. In this case, the debugger is called with the required additional arguments. In other cases, the debugger is simply called without additional arguments. Such a wrapper can be found in the dev/ subdirectory of the sources.

14.2 Modules dependencies

In order to compute modules dependencies (so to use make), Coq comes with an appropriate tool, coqdep.

coqdep computes inter-module dependencies for Coq and Objective Caml programs, and prints the dependencies on the standard output in a format readable by make. When a directory is given as argument, it is recursively looked at.

Dependencies of Coq modules are computed by looking at Require commands (Require, Require Export, Require Import, Require Implementation), but also at the command Declare ML Module.

Dependencies of Objective Caml modules are computed by looking at open commands and the dot notation module.value. However, this is done approximatively and you are advised to use ocamldep instead for the Objective Caml modules dependencies.

See the man page of coqdep for more details and options.

14.3 Creating a `Makefile` for Coq modules

When a proof development becomes large and is split into several files, it becomes crucial to use a tool like make to compile Coq modules.

The writing of a generic and complete Makefile may be a tedious work and that’s why Coq provides a tool to automate its creation, coq_makefile. Given the files to compile, the command coq_makefile prints a Makefile on the standard output. So one has just to run the command:

% coq_makefile file₁.v … file_n.v > Makefile

The resulted Makefile has a target depend which computes the dependencies and puts them in a separate file .depend, which is included by the Makefile. Therefore, you should create such a file before the first invocation of make. You can for instance use the command

% touch .depend

Then, to initialize or update the modules dependencies, type in:

% make depend

There is a target all to compile all the files file₁ … file_n, and a generic target to produce a .vo file from the corresponding .v file (so you can do make file.vo to compile the file file.v).

coq_makefile can also handle the case of ML files and subdirectories. For more options type

% coq_makefile --help

Warning: To compile a project containing Objective Caml files you must keep the sources of Coq somewhere and have an environment variable named COQTOP that points to that directory.

14.4 Documenting Coq files with coqdoc

coqdoc is a documentation tool for the proof assistant Coq, similar to javadoc or ocamldoc. The task of coqdoc is

to produce a nice L^AT_EX and/or HTML document from the Coq sources, readable for a human and not only for the proof assistant;
to help the user navigating in his own (or third-party) sources.

14.4.1 Principles

Documentation is inserted into Coq files as special comments. Thus your files will compile as usual, whether you use coqdoc or not. coqdoc presupposes that the given Coq files are well-formed (at least lexically). Documentation starts with (**, followed by a space, and ends with the pending *). The documentation format is inspired by Todd A. Coram’s Almost Free Text (AFT) tool: it is mainly ASCII text with some syntax-light controls, described below. coqdoc is robust: it shouldn’t fail, whatever the input is. But remember: “garbage in, garbage out”.

Coq material inside documentation.

Coq material is quoted between the delimiters [ and ]. Square brackets may be nested, the inner ones being understood as being part of the quoted code (thus you can quote a term like [x:T]u by writing [[x:T]u]). Inside quotations, the code is pretty-printed in the same way as it is in code parts.

Pre-formatted vernacular is enclosed by [[ and ]]. The former must be followed by a newline and the latter must follow a newline.

Pretty-printing.

coqdoc uses different faces for identifiers and keywords. The pretty-printing of Coq tokens (identifiers or symbols) can be controlled using one of the following commands:

(** printing token %...L^AT_EX...% #...HTML...# *)

(** printing token $...L^AT_EX math...$ #...HTML...# *)

It gives the L^AT_EX and HTML texts to be produced for the given Coq token. One of the L^AT_EX or HTML text may be ommitted, causing the default pretty-printing to be used for this token.

The printing for one token can be removed with

(** remove printing token *)

Initially, the pretty-printing table contains the following mapping:

`->`	→	`<-`	←	`*`	×
`<=`	≤	`>=`	≥	`=>`	⇒
`<>`	≠	`<->`	↔	`\|-`	⊢
`\/`	∨	`/\`	∧	`~`	¬

Any of these can be overwritten or suppressed using the printing commands.

Important note: the recognition of tokens is done by a (ocaml)lex automaton and thus applies the longest-match rule. For instance, ->~ is recognized as a single token, where Coq sees two tokens. It is the responsability of the user to insert space between tokens or to give pretty-printing rules for the possible combinations, e.g.

(** printing ->~ %\ensuremath{\rightarrow\lnot}% *)

Sections.

Sections are introduced by 1 to 4 leading stars (i.e. at the beginning of the line) followed by a space. One star is a section, two stars a sub-section, etc. The section title is given on the remaining of the line. Example:

    (** * Well-founded relations
  
        In this section, we introduce...  *)

Lists.

List items are introduced by 1 to 4 leading dashes. Deepness of the list is indicated by the number of dashes. List ends with a blank line. Example:

    This module defines
        - the predecessor [pred]
        - the addition [plus]
        - order relations:
          -- less or equal [le]
          -- less [lt]

Rules.

More than 4 leading dashes produce an horizontal rule.

Escapings to L^AT_EX and HTML.

Pure L^AT_EX or HTML material can be inserted using the following escape sequences:

$...LaTeX stuff...$ inserts some L^AT_EX material in math mode. Simply discarded in HTML output.
%...LaTeX stuff...% inserts some L^AT_EX material. Simply discarded in HTML output.
#...HTML stuff...# inserts some HTML material. Simply discarded in L^AT_EX output.

Verbatim.

Verbatim material is introduced by a leading << and closed by >> at the beginning of a line. Example:

Here is the corresponding caml code:
<<
  let rec fact n = 
    if n <= 1 then 1 else n * fact (n-1)
>>

Hyperlinks.

Hyperlinks can be inserted into the HTML output, so that any identifier is linked to the place of its definition.

In order to get hyperlinks you need to first compile your Coq file using coqc --dump-glob file; this appends Coq names resolutions done during the compilation to file file. Take care of erasing this file, if any, when starting the whole compilation process.

Then invoke coqdoc --glob-from file to tell coqdoc to look for name resolutions into the file file.

Identifiers from the Coq standard library are linked to the Coq web site at http://coq.inria.fr/library/. This behavior can be changed using command line options --no-externals and --coqlib; see below.

Hiding / Showing parts of the source.

Some parts of the source can be hidden using command line options -g and -l (see below), or using such comments:

(* begin hide *)
some Coq material
(* end hide *)

Conversely, some parts of the source which would be hidden can be shown using such comments:

(* begin show *)
some Coq material
(* end show *)

The latter cannot be used around some inner parts of a proof, but can be used around a whole proof.

14.4.2 Usage

coqdoc is invoked on a shell command line as follows:

coqdoc <options and files>

Any command line argument which is not an option is considered to be a file (even if it starts with a -). Coq files are identified by the suffixes .v and .g and L^AT_EX files by the suffix .tex.

HTML output: This is the default output. One HTML file is created for each Coq file given on the command line, together with a file index.html (unless option -no-index is passed). The HTML pages use a style sheet named style.css. Such a file is distributed with coqdoc.
L^AT_EX output: A single L^AT_EX file is created, on standard output. It can be redirected to a file with option -o. The order of files on the command line is kept in the final document. L^AT_EX files given on the command line are copied ‘as is’ in the final document . DVI and PostScript can be produced directly with the options -dvi and -ps respectively.
T_EXmacs output: To translate the input files to T_EXmacs format, to be used by the T_EXmacs Coq interface (see http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/).

Command line options

Overall options

--html: Select a HTML output.
--latex: Select a L^AT_EX output.
--dvi: Select a DVI output.
--ps: Select a PostScript output.
--texmacs: Select a T_EXmacs output.
--stdout: Write output to stdout.
-o file, --output file: Redirect the output into the file ‘file’ (meaningless with -html).
-d dir, --directory dir: Output files into directory ‘dir’ instead of current directory (option -d does not change the filename specified with option -o, if any).
-s , --short: Do not insert titles for the files. The default behavior is to insert a title like “Library Foo” for each file.
-t string, --title string: Set the document title.
--body-only: Suppress the header and trailer of the final document. Thus, you can insert the resulting document into a larger one.
-p string, --preamble string: Insert some material in the L^AT_EX preamble, right before \begin{document} (meaningless with -html).
--vernac-file file, --tex-file file: Considers the file ‘file’ respectively as a .v (or .g) file or a .tex file.
--files-from file: Read file names to process in file ‘file’ as if they were given on the command line. Useful for program sources splitted in several directories.
-q, --quiet: Be quiet. Do not print anything except errors.
-h, --help: Give a short summary of the options and exit.
-v, --version: Print the version and exit.

Index options

Default behavior is to build an index, for the HTML output only, into index.html.

--no-index: Do not output the index.
--multi-index: Generate one page for each category and each letter in the index, together with a top page index.html.

Table of contents option

-toc, --table-of-contents: Insert a table of contents. For a L^AT_EX output, it inserts a \tableofcontents at the beginning of the document. For a HTML output, it builds a table of contents into toc.html.

Hyperlinks options

--glob-from file

Make references using Coq globalizations from file file. (Such globalizations are obtained with Coq option -dump-glob).

--no-externals

Do not insert links to the Coq standard library.

--coqlib url

Set base URL for the Coq standard library (default is http://coq.inria.fr/library/).

-R dir coqdir

Map physical directory dir to Coq logical directory coqdir (similarly to Coq option -R).

Note: option -R only has effect on the files following it on the command line, so you will probably need to put this option first.

Contents options

-g, --gallina

Do not print proofs.

-l, --light

Light mode. Suppress proofs (as with -g) and the following commands:

[Recursive] Tactic Definition
Hint / Hints
Require
Transparent / Opaque
Implicit Argument / Implicits
Section / Variable / Hypothesis / End

The behavior of options -g and -l can be locally overridden using the (* begin show *) … (* end show *) environment (see above).

Language options

Default behavior is to assume ASCII 7 bits input files.

-latin1, --latin1: Select ISO-8859-1 input files. It is equivalent to --inputenc latin1 --charset iso-8859-1.
-utf8, --utf8: Select UTF-8 (Unicode) input files. It is equivalent to --inputenc utf8 --charset utf-8. L^AT_EX UTF-8 support can be found at http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.
--inputenc string: Give a L^AT_EX input encoding, as an option to L^AT_EX package inputenc.
--charset string: Specify the HTML character set, to be inserted in the HTML header.

14.4.3 The coqdoc L^AT_EX style file

In case you choose to produce a document without the default L^AT_EX preamble (by using option --no-preamble), then you must insert into your own preamble the command

\usepackage{coqdoc}

Then you may alter the rendering of the document by redefining some macros:

coqdockw, coqdocid

The one-argument macros for typesetting keywords and identifiers. Defaults are sans-serif for keywords and italic for identifiers.

For example, if you would like a slanted font for keywords, you may insert

     \renewcommand{\coqdockw}[1]{\textsl{#1}}

anywhere between \usepackage{coqdoc} and \begin{document}.

coqdocmodule

One-argument macro for typesetting the title of a .v file. Default is

\newcommand{\coqdocmodule}[1]{\section*{Module #1}}

and you may redefine it using \renewcommand.

14.5 Exporting Coq theories to XML

This section describes the exportation of Coq theories to XML that has been contributed by Claudio Sacerdoti Coen. Currently, the main applications are the rendering and searching tool developed within the HELM¹ and MoWGLI² projects mainly at the University of Bologna and partly at INRIA-Sophia Antipolis.

14.5.1 Practical use of the XML exportation tool

The basic way to export the logical content of a file into XML format is to use coqc with option -xml. When the -xml flag is set, every definition or declaration is immediately exported to XML once concluded. The system environment variable COQ_XML_LIBRARY_ROOT must be previously set to a directory in which the logical structure of the exported objects is reflected.

For Makefile files generated by coq_makefile (see section 14.3), it is sufficient to compile the files using

make COQ_XML=-xml

(or, equivalently, setting the environment variable COQ_XML)

To export a development to XML, the suggested procedure is then:

add to your own contribution a valid Make file and use coq_makefile to generate the Makefile from the Make file.

Warning: Since logical names are used to structure the XML hierarchy, always add to the Make file at least one "-R" option to map physical file names to logical module paths.
set the COQ_XML_LIBRARY_ROOT environment variable to the directory where the XML file hierarchy must be physically rooted.
compile your contribution with "make COQ_XML=-xml"

Remark: In case the system variable COQ_XML_LIBRARY_ROOT is not set, the output is done on the standard output. Also, the files are compressed using gzip after creation. This is to save disk space since the XML format is very verbose.

14.5.2 Reflection of the logical structure into the file system

For each Coq logical object, several independent files associated to this object are created. The structure of the long name of the object is reflected in the directory structure of the file system. E.g. an object of long name ident₁.….ident_n.ident is exported to files in the subdirectory ident₁/…/ident_n of the directory bound to the environment variable COQ_XML_LIBRARY_ROOT.

14.5.3 What is exported?

The XML exportation tool exports the logical content of Coq theories. This covers global definitions (including lemmas, theorems, ...), global assumptions (parameters and axioms), local assumptions or definitions, and inductive definitions.

Vernacular files are exported to .theory.xml files. Comments are pre-processed with coqdoc (see section 14.4). Especially, they have to be enclosed within (** and *) to be exported.

For each inductive definition of name ident₁.….ident_n.ident, a file named ident.ind.xml is created in the subdirectory ident₁/…/ident_n of the xml library root directory. It contains the arities and constructors of the type. For mutual inductive definitions, the file is named after the name of the first inductive type of the block.

For each global definition of base name ident₁.….ident_n.ident, files named ident.con.body.xml and ident.con.xml are created in the subdirectory ident₁/…/ident_n. They respectively contain the body and the type of the definition.

For each global assumption of base name ident₁.ident₂.….ident_n.ident, a file named ident.con.xml is created in the subdirectory ident₁/…/ident_n. It contains the type of the global assumption.

For each local assumption or definition of base name ident located in sections ident′₁, …, ident′_p of the module ident₁.ident₂.….ident_n.ident, a file named ident.var.xml is created in the subdirectory ident₁/…/ident_n/ident′₁/…/ident′_p. It contains its type and, if a definition, its body.

In order to do proof-rendering (for example in natural language), some redundant typing information is required, i.e. the type of at least some of the subterms of the bodies and types of the CIC objects. These types are called inner types and are exported to files of suffix .types.xml by the exportation tool.

14.5.4 Inner types

The type of a subterm of a construction is called an inner type if it respects the following conditions.

Its sort is Prop³.
It is not a type cast nor an atomic term (variable, constructor or constant).
If it’s root is an abstraction, then the root’s parent node is not an abstraction, i.e. only the type of the outer abstraction of a block of nested abstractions is printed.

The rationale for the 3^rd condition is that the type of the inner abstractions could be easily computed starting from the type of the outer ones; moreover, the types of the inner abstractions requires a lot of disk/memory space: removing the 3^rd condition leads to XML file that are two times as big as the ones exported applying the 3^rd condition.

14.5.5 Interactive exportation commands

There are also commands to be used interactively in coqtop.

`Print XML` qualid

If the variable COQ_XML_LIBRARY_ROOT is set, this command creates files containing the logical content in XML format of qualid. If the variable is not set, the result is displayed on the standard output.

Variants:

Print XML File string qualid
This writes the logical content of qualid in XML format to files whose prefix is string.

`Show XML Proof`

If the variable COQ_XML_LIBRARY_ROOT is set, this command creates files containing the current proof in progress in XML format. It writes also an XML file made of inner types. If the variable is not set, the result is displayed on the standard output.

Variants:

Show XML File string Proof
This writes the logical content of qualid in XML format to files whose prefix is string.

14.5.6 Applications: rendering, searching and publishing

The HELM team at the University of Bologna has developed tools exploiting the XML exportation of Coq libraries. This covers rendering, searching and publishing tools.

All these tools require a running http server and, if possible, a MathML compliant browser. The procedure to install the suite of tools ultimately allowing rendering and searching can be found on the HELM web site http://helm.cs.unibo.it/library.html.

It may be easier though to upload your developments on the HELM http server and to re-use the infrastructure running on it. This requires publishing your development. To this aim, follow the instructions on http://mowgli.cs.unibo.it.

Notice that the HELM server already hosts a copy of the standard library of Coq and of the Coq user contributions.

14.5.7 Technical informations

CIC with Explicit Named Substitutions

The exported files are XML encoding of the lambda-terms used by the Coq system. The implementative details of the Coq system are hidden as much as possible, so that the XML DTD is a straightforward encoding of the Calculus of (Co)Inductive Constructions.

Nevertheless, there is a feature of the Coq system that can not be hidden in a completely satisfactory way: discharging (see Sect.2.4). In Coq it is possible to open a section, declare variables and use them in the rest of the section as if they were axiom declarations. Once the section is closed, every definition and theorem in the section is discharged by abstracting it over the section variables. Variable declarations as well as section declarations are entirely dropped. Since we are interested in an XML encoding of definitions and theorems as close as possible to those directly provided the user, we do not want to export discharged forms. Exporting non-discharged theorem and definitions together with theorems that rely on the discharged forms obliges the tools that work on the XML encoding to implement discharging to achieve logical consistency. Moreover, the rendering of the files can be misleading, since hyperlinks can be shown between occurrences of the discharge form of a definition and the non-discharged definition, that are different objects.

To overcome the previous limitations, Claudio Sacerdoti Coen developed in his PhD. thesis an extension of CIC, called Calculus of (Co)Inductive Constructions with Explicit Named Substitutions, that is a slight extension of CIC where discharging is not necessary. The DTD of the exported XML files describes constants, inductive types and variables of the Calculus of (Co)Inductive Constructions with Explicit Named Substitutions. The conversion to the new calculus is performed during the exportation phase.

The following example shows a very small Coq development together with its version in CIC with Explicit Named Substitutions.

# CIC version: #
Section S.
 Variable A : Prop.

 Definition impl := A -> A.

 Theorem t : impl.           (* uses the undischarged form of impl *)
  Proof.
   exact (fun (a:A) => a).
  Qed.

End S.

Theorem t' : (impl False).   (* uses the discharged form of impl *)
 Proof.
  exact (t False).           (* uses the discharged form of t *)
 Qed.

# Corresponding CIC with Explicit Named Substitutions version: #
Section S.
 Variable A : Prop.
 
 Definition impl(A) := A -> A. (* theorems and definitions are
                                  explicitly abstracted over the
                                  variables. The name is sufficient to
                                  completely describe the abstraction *)
 
 Theorem t(A) : impl.          (* impl where A is not instantiated *)
  Proof.
   exact (fun (a:A) => a).
  Qed.
 
End S.
 
Theorem t'() : impl{False/A}. (* impl where A is instantiated with False
                                 Notice that t' does not depend on A     *)
 Proof.
  exact t{False/A}.           (* t where A is instantiated with False *)
 Qed.

Further details on the typing and reduction rules of the calculus can be found in Claudio Sacerdoti Coen PhD. dissertation, where the consistency of the calculus is also proved.

The CIC with Explicit Named Substitutions XML DTD

A copy of the DTD can be found in the file “cic.dtd” in the contrib/xml source directory of Coq. The following is a very brief overview of the elements described in the DTD.

: <ConstantType> is the root element of the files that correspond to constant types.
: <ConstantBody> is the root element of the files that correspond to constant bodies. It is used only for closed definitions and theorems (i.e. when no metavariable occurs in the body or type of the constant)
: <CurrentProof> is the root element of the file that correspond to the body of a constant that depends on metavariables (e.g. unfinished proofs)
: <Variable> is the root element of the files that correspond to variables
: <InductiveTypes> is the root element of the files that correspond to blocks of mutually defined inductive definitions

The elements <LAMBDA>, <CAST>, <PROD>, <REL>, <SORT>, <APPLY>, <VAR>, <META>, <IMPLICIT>, <CONST>, <LETIN>, <MUTIND>, <MUTCONSTRUCT>, <MUTCASE>, <FIX> and <COFIX> are used to encode the constructors of CIC. The sort or type attribute of the element, if present, is respectively the sort or the type of the term, that is a sort because of the typing rules of CIC.

The element <instantiate> correspond to the application of an explicit named substitution to its first argument, that is a reference to a definition or declaration in the environment.

All the other elements are just syntactic sugar.

14.6 Embedded Coq phrases inside L^AT_EX documents

When writing a documentation about a proof development, one may want to insert Coq phrases inside a L^AT_EX document, possibly together with the corresponding answers of the system. We provide a mechanical way to process such Coq phrases embedded in L^AT_EX files: the coq-tex filter. This filter extracts Coq phrases embedded in LaTeX files, evaluates them, and insert the outcome of the evaluation after each phrase.

Starting with a file file.tex containing Coq phrases, the coq-tex filter produces a file named file.v.tex with the Coq outcome.

There are options to produce the Coq parts in smaller font, italic, between horizontal rules, etc. See the man page of coq-tex for more details.

Remark. This Reference Manual and the Tutorial have been completely produced with coq-tex.

14.7 Coq and GNU Emacs

14.7.1 The Coq Emacs mode

Coq comes with a Major mode for GNU Emacs, coq.el. This mode provides syntax highlighting (assuming your GNU Emacs library provides hilit19.el) and also a rudimentary indentation facility in the style of the Caml GNU Emacs mode.

Add the following lines to your .emacs file:

  (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist))
  (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t)

The Coq major mode is triggered by visiting a file with extension .v, or manually with the command M-x coq-mode. It gives you the correct syntax table for the Coq language, and also a rudimentary indentation facility:

pressing Tab at the beginning of a line indents the line like the line above;
extra Tabs increase the indentation level (by 2 spaces by default);
M-Tab decreases the indentation level.

An inferior mode to run Coq under Emacs, by Marco Maggesi, is also included in the distribution, in file coq-inferior.el. Instructions to use it are contained in this file.

14.7.2 Proof General

Proof General is a generic interface for proof assistants based on Emacs (or XEmacs). The main idea is that the Coq commands you are editing are sent to a Coq toplevel running behind Emacs and the answers of the system automatically inserted into other Emacs buffers. Thus you don’t need to copy-paste the Coq material from your files to the Coq toplevel or conversely from the Coq toplevel to some files.

Proof General is developped and distributed independently of the system Coq. It is freely available at proofgeneral.inf.ed.ac.uk.

14.8 Module specification

Given a Coq vernacular file, the gallina filter extracts its specification (inductive types declarations, definitions, type of lemmas and theorems), removing the proofs parts of the file. The Coq file file.v gives birth to the specification file file.g (where the suffix .g stands for Gallina).

See the man page of gallina for more details and options.

14.9 Man pages

There are man pages for the commands coqdep, gallina and coq-tex. Man pages are installed at installation time (see installation instructions in file INSTALL, step 6).

1: Hypertextual Electronic Library of Mathematics
2: Mathematics on the Web, Get it by Logic and Interfaces
3: or CProp which is the "sort"-like definition used in C-CoRN (see http://vacuumcleaner.cs.kun.nl/c-corn) to type computationally relevant predicative propositions.