The Coq Proof Assistant Changes from Coq V5.10 to Coq V6.1

Version 6.1^{∗}

Projet Coq

INRIA-Rocquencourt^{†} — CNRS - ENS Lyon ^{‡}

∗This research was partly supported by ESPRIT Basic Research Action “Types” and by the GDR “Programmation” co-financed by MRE-PRC and CNRS.

†B.P. 105, 78153 Le Chesnay CEDEX, France. ‡LIP URA 1398 du CNRS, 46 Allée d’Italie, 69364 Lyon CEDEX 07, France.

V6.1, 1st Printing December 13th, 1996

\begin{matrix}c \\ ◯ \end{matrix}INRIA 1996

1 Overview

The main novelties of Coq V6.1 are :

• Port to Objective Caml

• Syntax and printing

– A new mechanism Cases of function definition by pattern-matching which superseds the Case construction.

– A new mode for automatic synthesis of implicit arguments

– Automatic coercion between types

– A new printer of proofs in natural language

• Tactics – A new decision tactic for Presburger Arithmetic

– A new tactic for simplification of expression in rings (not yet documented)

– An extended automatic proof search (tactic EAuto) Moreover, the following already existing things have changed:

• Change in the structure of sorts : the sort Typeset is now identified with the sort Type.

• The theories has been reorganised keeping only general purpose libraries for being reused in developments.

• Rewrite et Dependent Rewrite fails when rewriting will not progress.

• The constructors of an inductive definition cannot have an already use name.

• Inversion tactics now applies to goal of type Type.

• Intuition now do Intros.

Source of incompatibilities

You may have to change your tactic scripts because of Rewrite and Dependent Rewrite: they now fail where before they left the goal unchanged. Note also that Intuition performs Intros before halting. Inductive Definition may fail to typecheck when the names of constructors were already defined.

2 Objective Caml

The port of Coq to Objective Caml makes the system faster. In fact, corresponding to the two flavours of Objective Caml (byte-code or native code), there are two flavours of Coq:

• The coqtop command runs only byte-code but may dynamically load new packages written in Objective Caml.

• The -opt option to coqtop command runs fast native code but cannot link dynamically new packages.

A new command coqmktop allows to statically build native code images of the kernel of Coq + additional packages.

See the reference manual, chapter The Coq commands.

Extraction towards Objective Caml is also provided (see the additional manual on extraction).

3 Reorganisation of the library

A standard library. The theories directory has been reorganised, keeping only general purpose libraries. The bigger developments like ALGEBRA or PROGRAMS have been moved in the contributions library.

The developments in the theory directory are compiled during the installation procedure. The compiled files will be moved to a standard library known by the coqtop command, such that any Require command to one of these development can be done without specifying any additional path.

Users’ contributions. The contributions to the Coq library are no longer distributed with the system, but as another tar file. The Makefile files in the contrib directory have been rewritten in order to allow the compiling of any contribution independently of its position with respect to the Coq files (binaries or libraries), only assuming that the Coq commands are in your path and that the Coq library has been properly installed. (For this, the tool do Makefile has been rewritten and uses a description file to generate automatically generic Makefile. See the Reference Manual, chapter Utilities, for more details).

4 Sorts

The sort Typeset has disappeared. The sort Type is now both the type of Prop and of Set. Furthermore there is an implicit coercion between Prop and Type and Set and Type such that any object of type Prop or Set has also type Type.

The extraction mechanism is not compatible with this universe hierarchy. It is supposed to work only on terms which are explicitely typed in the Calculus of Constructions without universes and with Inductive Definitions at the Set level and only a small elimination. In other cases, extraction may generate a dummy answer and sometimes failed. To avoid failure when developing proof, an error while extracting the computational contents of a proof will not stop the proof but only give a warning.

5 Syntax and printing

5.1 Function definition by cases

Case analysis à la ML is now possible (see the reference Manual, chapter The macro Cases). Most of the definitions which was using the construction case ... of ... end can be written in a more readable and sometimes more concise way by using Cases.

The command Recursive Definition is not anymore available and should be replaced by a combination of Fixpoint and Cases. In some cases, recursive calls accepted by Recursive Definition are not well-formed with respect to a single Fixpoint definition and several fixpoints are necessary to encode the definition.

5.2 Implicit syntax

A new mode determines automatically implicit arguments (see the reference manual, chapter Syntax extensions). This mode may be sometimes unconvenient or weaker, then the command Syntactic Definition is still available.

Some automatic coercion between types may be forced (see the reference manual, chapter Syntax extensions).

5.3 Natural

Natural is a new package contributed by Yann Coscoy. It prints proofs in natural language. See the corresponding separate documentations Natural.dvi.

5.4 Inductive Definitions

An inductive definition is not accepted when the names of a constructor override an existing name.

6 Tactics

6.1 Tactic bahaviour changes

Rewrite and Dependent Rewrite now fails when they leave the goal unchanged. Intuition now performs Intros before halting.

6.2 EAuto

A new tatic EAuto is available. It uses the Hint list of the Auto tactic but performs an extended proof search in the style of the Prolog tactic. It accepts to apply lemmas generating existential variables like a transitivity property or the introduction of an existential quantifier. Such lemmas are now accepted as hints but are only used with the EAuto tactic and not the Auto tactic.

6.3 Omega

Omega is a decision tactic for Presburger Arithmetic contributed by Pierre Crégut. It is documented in the separate files Omega.v.*.

6.4 Simplification on rings

A new tactics of simplification of expressions in commutative rings will be soon documented.