Basic library files and modules management

Summary

This tutorial is about how to get the most out of library files, that is Coq files containing definitions, lemmas, notations, ... Coq Library files are modules, which may themselves contain (non-file) inner modules. In order to reuse the content of a file, one has to Require it first. We will first see how these library files are identified by Coq and how to Require them in practice. Coq Modules provide, among other things, namespace facilities as well as some form of locality. We will see how to identify the constants (definitions, lemmas, ...) contained in a module with a (more or less) qualified name such as Bool.andb_true_l. In order to use an unqualified name, such as andb_true_l, one has to Import this module. It turns out this can lead to shadowing other existing constants. We will detail when and how it may happen. Next, we will be interested with other content types in modules, that is, hints, coercions, notations, ... and how they are typically not available when the module is not Imported. We will see how to restrict what is visible outside a module, either from the user side with selective imports, or from the module writer side with locality attributes. We will finally clarify the difference between Importing and Exporting a module. The second and third part of this tutorial are (almost) independent. These topics are often skipped from lectures or courses about Coq because they are mostly technical and somewhat boring. However, any Coq user needs to learn (usually the hard way) this content before writing their own libraries.

Table of content

• 1. Library files, modules and identifiers
  • 1.1 The Require command and fully qualified names
  • 1.2. Basic modules and the Import command
  • 1.3. Name clashes and disambiguation
  • 1.4. Other content types in modules
  • 1.5. Guidelines about the order of Require and Import commands
• 2. Fine control over module features
  • 2.1. On the user's side: selective import
  • 2.2. On the writer's side: locality attributes in modules
• 3. The Export command

Prerequisites

Needed:

• The user should already have some basic Coq experience: writing definitions, lemmas, proofs...
• Some parts deal with more advanced Coq content (user-defined tactics, notations, coercions...); having some basic knowledge about it is better to appreciate what Coq can offer, but is not really needed.

Installation: This tutorial should work for Coq V8.17 or later.

1. Library files, modules and identifiers

1.1 The Require command and fully qualified names

Coq's basic compilation unit is the library file. Each compiled file can be Required in order to make its logical and computational content available in the current file. If not stated otherwise (with the -no-init command-line flag), Coq's initial state is populated by a dozen library files called the Prelude (the interested reader can consult its source code). We can see these files with the Print Libraries command:

As we can see, these files share a common logical prefix made of:

• Coq: the library prefix used by the standard library
• Init: the subdirectory of the root directory of Coq's standard library where these library files are located

This means that the Init directory contains the (compiled) files Notations.vo, Ltac.vo, Logic.vo, ... and we can already use their content, for instance the commutativity of the disjunction:

Let's require another small library file.

The previous command told Coq to load all logical and computational content in the file Bool.vo contained in the directory Bool of the root directory of Coq's standard library (the interested reader can browse its current source code). Now let's see how our list of libraries has evolved:

As we can see, we have not one but two more library files. The Coq.Classes.DecidableClass is itself required in Coq.Bool.Bool. Now there are two very important message here: 1. When we Require a file, we Require recursively any file it has Required (and any file Required in the Required files, and so on). 2. There is **no way** to "unrequire" anything. Once a file has been required, its content will remain in the global environment of the user in every file where it was (transitively) required, possibly cluttering up Search output. As a consequence, one should be careful of what one Requires. Now that we have required Coq.Bool.Bool, we have many more lemmas about boolean operations.

Some of them are qualified with the Bool. prefix, these come from Coq.Bool.Bool. Others have short names, these come from one of the Coq.Init files. Using the About command gives us their locations.

Now let's take a look at Bool.andb_true_l

We see that it expands to Coq.Bool.Bool.andb_true_l. This is the internal name Coq uses to distinguish it from any other constant. We call it an absolutely qualified identifier or fully qualified identifier. This is a technical but important notion, so we should take some time to describe this identifier. There are several parts separated by dots.

• The first part is Coq: it is the logical name of the library. Other mechanisms (for instance a _CoqProject file, or -R and -Q options for coqc, locations which are known by coqc, such as the output of coqc -where, ...) associate a logical name to a physical directory in the user's system which is the root directory of this library.
• The second and third part correspond to the path of the file (relative to the root of the library) containing the identifier in the given library, in our case, on a Unix family system, it corresponds to Bool/Bool.vo.

Now, at this point, Coq.Bool.Bool is the last required library file called Bool containing a constant named andb_true_l, so Coq accepts (and prints) as a shorter partially qualified the identifier Bool.andb_true_l. Another valid partially qualified identifier for the same constant is Bool.Bool.andb_true_l. All these identifiers refer to the same constant:

However, at this point Coq does not accept the unqualified andb_true_l as a valid identifier:

Coq does not allow us to use this short name automatically because it risks to silently shadow another constant with the same short name. The Locate command shows all constants associated to an unqualified identifier and how to refer to it in the shortest way possible.

If we want to use such a short name, we need to Import the Bool module (yes, we said module here and not library file, more about this later).

Now we can refer to the constants in Bool with their short names.

Coq will also display short names in its messages:

In passing, we have Imported Bool with a small unqualified name because there was no confusion:

But we can refer to the Bool with a more qualified name too:

In fact, most users prefer short names to fully qualified names so, in practice, one usually Requires and Imports a file at the same time. This is done, for instance, with the syntax: From Coq Require Import Bool.Bool. In passing, there are many more possibilities to Require (with or with Import) a library file. The fully qualified name of this file is Coq.Bool.Bool, and one can factor any prefix in the From part of the command, so the following command achieves the same goal: From Coq.Bool Require Import Bool. or, with an empty From part: Require Import Coq.Bool.Bool. In fact, the From part is mostly a convenience to require multiple parts from a common library or sublibrary. For instance, if one uses the mathcomp library, the single line: From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. loads and imports 6 files from the mathcomp library. If there is no confusion, it is even possible to omit the directory (or directories) part. In our case there is only one file Bool.vo in all Coq's standard library, so we could also have used From Coq Require Import Bool. What to choose is then mostly a matter of taste (and clearly depends on the number of files in the library).

1.2. Basic modules and the Import command

We will use modules here mostly because they will help us understand how to get what we want from library files (and reject, if possible, what we don't want). For now let us consider a very simple module:

Such a module, written down explicitly with End module_name at the end is called an interactive module. Our module Foo has 1 definition and 2 lemmas. It's printed out in the following way:

Notice that, surprisingly, the too lemmas are printed as Parameters, but they really are actual lemmas. We can access the content of the module with the dot syntax.

Foo.bar and Foo.baz are not Parameters or Axioms: the following Print Assumptions commands show that they are "closed under the global context", that is they do not rely on any axiom and are indeed proved.

But we cannot yet access them with short names:

The content of the module Foo can be used just like any other definitions and lemmas

This dot syntax is reminiscent of what we used for library files, and it is no accident. In fact, library files are modules. This is the most important fact to take home from this tutorial, and the main reason to study a part of Coq's module system. We can even print the content of library files, viewed as modules:

Import is actually a module command, so we can:

Now that Foo is Imported, we can access its content with short names:

To sum up without subtlety what we have learned so far:

• We Require library files to load their content.
• We Import modules to use short names for their content (among other things we will see shortly)
• Library files are modules.

1.3. Name clashes and disambiguation

When we Imported our Foo module before, there was no possible name clash since no constant in our context were named foo, bar or baz. In real life Coq, however, global contexts can be huge and there will be name clashes. So, what happens if we define and import the following module?

First, Coq emits no error or warning, so this is a legit operation. What is foo now?

Our OtherFoo.foo identifier has actually shadowed Foo.foo. To identify it, we now need to use a more qualified name.

The Locate command shows the list of identifiers whose unqualified name is the given argument:

The first item in the list is our OtherFoo.foo constant, it is available by its short name. Next is Foo.foo and Coq gives us the shortest partially qualified name to refer to it. What happens if we now Import Foo again?

We have changed again to which constant refers the short name foo! Our Foo.foo constant is now the first item in our list of foo constants. This changing short name resolution may look innocuous but it has a very important consequence: The order of the Import commands matters, changing it can break things. Notice that one can always use more qualified names, so that the resulting code is independent of the Import orders:

Now, for a real life example, let us consider the library files Coq.Arith.PeanoNat and Coq.ZArith.BinInt which contain the bulk of Coq's standard library content for, respectively Peano natural numbers and (binary) integers.

Most of the results and operations are actually contained in the interactive (inner) modules PeanoNat.Nat and BinInt.Z. These inner modules are not imported, yet.

Notice that the name add_0_r is used both for natural numbers and for integers, which seems right. At this point, add_0_r does not refer to anything.

We may choose to Import Nat if, for instance, our current development deals more with natural numbers than integers.

We could even Import both modules, but then beware that the order is important.

Another common choice is to Import neither of them and use the Nat. and Z. prefixes as namespaces. This is a bit more verbose, but it is also easier to read. What happens if module names themselves clash? We actually are already in that case:

We have one module named Nat in PeanoNat and another one in the form of a library file in the Init directory. The name of the module Coq.Init.Nat was shadowed when we Imported the module Coq.Arith.PeanoNat. As we have just seen, it suffices to qualify more the module which is shadowed if we want to explicitly refer to it. When two modules share the same name, there can be name clashes and shadowing if some of their constants have the same name. Let us illustrate it with nested modules. The situation would be similar if we required two library files with the same name in different libraries or directories (but we cannot illustrate this case conveniently in a single-file tutorial).

For now, there is no ambiguity, since we have not imported any module. Our 4 new constants are:

• NestedABC1.ABC.alice
• NestedABC1.ABC.bob
• NestedABC2.ABC.alice
• NestedABC2.ABC.charlie

Now we Import both outer modules:

What are ABC.alice, ABC.bob and ABC.charlie now?

As we see, ABC.alice from NestedABC1 has now been shadowed by ABC.alice in NestedABC2. Other than that, Coq is perfectly fine with ABC.bob, which means that the ABC prefix in these three identifiers can actually refer to different modules. Of course, we can still refer to the alice constant in the first module with a more qualified identifier:

What happens if we Import both ABC momdules? Anything more than what we already saw: the order of the Import commands will determine the meaning of the short name alice.

The previous command did not shadow the module name ABC itself, so it still refers to the previously Imported NestedABC2.ABC and we can Import it that way:

Where is the other alice?

To conclude this part, let us sum up what Coq allows and disallows regarding identifiers:

• it is possible to have two files with the same name as long as they are in different directories;
• it is possible to have two (non-file) modules with the same name as long as they are in different modules (which can be library files);
• it is possible to have two constants with the same name as long as they are in different modules (including library files)

1.4. Other content types in Modules

So far, our module Foo contained only definitions and lemmas. In practice there are many more content types in a module:

• parameters and axioms
• tactics
• notations, abbreviations, Ltac notations and Ltac2 notations
• hints and type class instances
• coercions
• canonical structures

It is not an issue if some (or all) these categories are obscure to you. We are only interested in what persists outside the module and in which case. We will only experiment with some of these categories.

We have not imported Bar yet. What do we have?

We see that parameters, axioms and lemmas are available, and axioms are treated as such after the end of the module. What about the other content?

As we can see, only the tactic `find_secret` and the abbreviation add_42 were available. Now let's Import Bar:

To sum things up:

• constants (i.e. parameters, definitions, lemmas, axioms, etc), tactics and abbreviations contained in a module are available even if we do not Import a module, with a qualified name;
• notations, Ltac notations, Ltac2 notations need the module to be imported to be available (note that notations are also associated to notation scopes we may have to Open or delimit with a key in order to use them)
• the same holds for coercions, hints, type class instances and canonical structures (we omit the experiments for brevity).

1.5 Guidelines about the order of Require and Import commands

We have seen that the order of Require and Import statements is important. Some constants could be shadowed by others, which can break definitions and proofs. In general, we should try to respect the following guidelines:

• All Require commands should (ultimately) be at the beginning of a file, it makes it easier to know on which theories the file is built. It is fine during development to experiment temporarily with Require commands in the middle of the file and in a final version, either move the require statement at the beginning of a file, or the whole experiment in a separate file.
• Usually, Require statements are actually Require Import statements: we want shorter names, notations, etc about theories we explicitly build on. Other constants which have been (implicitly) recursively Required need a longer name to be used, so it is easier not to use them by accident (or to finally decide that we need to explicitly Require Import other modules).
• We should Require Import only what is needed: it makes the global environment smaller, reduces the risks of shadowing and saves compilation time. In particular, breaking dependencies allows parallel compilation with multithreaded processors.
• In general, we should Require Import files from external libraries first, in a more or less specialization order (the most basic theories first). Then, we should Require Import other internal library files at the end. Doing so prevents an external project to break our file by shadowing internal constants we use in that file.
• We should try to Require Import files in the same order everytime to increase predictability of breakage due to shadowing.

2. Fine control over module features

2.1. On the user's side: selective import

Now is a good time to present a recent addition: selective import of modules. Recall that importing a module has basically two effects:

• make the short names of constants (lemmas, definitions, ...), abbreviations and tactics available
• enable the other content: notations, tactic notations, hints, coercions and canonical

Selective import lets us precisely choose what we want to import. To illustrate this, we create a hint database:

Our next example contains almost every categories of content:

Let us import our notations first:

Everything else has not been imported.

Let us now import our coercions and hints with one command:

Our notation is still there:

In fact, it is important to understand that there is no way to "un-import" anything in the same module or section. Once a module feature has been activated, it remains so until the end of the current section or module (or file), the only exception being shadowed content. We call the coercions and notations seen before import categories. The other import categories correspond to what we mentioned before, namely: hints, canonicals, ltac.notations and ltac2.notations. We can also select which constants and abbreviations are available by their short names:

There is also a way to tell Coq: Import everything except these categories. We just need to prepend them with a minus sign:

Notice that, when we import everything except some categories, it is not possible, at the time of writing, to choose which identifiers are imported to be available as short names: they all are. We can always change our mind and decide to import a category we did not:

To end this section, we turn to inductive types.

We have not imported anything yet. Our inductive types and their constructors are available with their qualified names:

So are our automatically generated induction principles (ending with _sind, _ind, _rec or _rect):

We can selectively Import all these constants and abbreviations. For an inductive type and its constructors, it suffices to give the type in the constants parenthesized list to be able to use its short name

However, its constructors and induction principles are not imported:

It is possible to Import them manually:

But there is a shortcut: using UnaryPos(..) imports at once the type, as well as its constructors and induction principles:

The following command enables all short names associated to the inductive type UnaryZ:

2.2. On the writer's side: locality attributes in modules

Let's now turn to a complementary tool to give control over what should remain local (if not hidden) and what should be exposed in a module (which can be a library file). Locality attributes change the visibility of content outside a section or a module. We're only interested in modules in this tutorial. Contrarily to selective import, which gives some amount of control on what is Imported to the user of a module, locality attributes lets the writer of a module control what should be imported or not. There are 3 locality attributes: #[local], #[export] and [#global]. The availability and effect of these attribute depends on each command (and even which Coq version we use) but, in short, when supported:

• the #[local] attribute makes some content unavailable for import
• the #[export] attribute makes some content available only if the module is Imported
• the #[global] attribute, in some cases, makes some content available outside the module even when not Imported.

We experiment with our useless module Baz:

The notation "x %" is also unavailable, but we cannot show it without stopping compilation, as it is not even parsed. You can try it by uncommenting: Compute 3 %. As we see, using the #[local] attribute in a module makes some content unavailable for import, which means, for constants, to make them only available with qualified names and for other categories (hints, coercions, etc), to disable them outside the module. This should be used without restraint on anything which should not be part of the user's interface, e.g. convenience ad-hoc tactics or unstable implementation details. The #[export] attribute is not as well supported as #[local]. In fact, in a module, since Coq 8.18, it is either not supported, or the default behavior (make a feature or short name available only when a module is Imported), except when used with the Set command which is used to change some Coq options. Prior to Coq 8.18, if one wants Hints to be available if (and only if) the module is Imported, they should have the #[export] attribute and in Coq 8.17, Coq will emit a fatal warning they do not have any attribute. The following example shows what to expect (in any recent Coq version) when a Hint is kept local and a Set command has no attribute:

The option "Universe Polymorphism" is not set outside the module.

Now, here is the same module with #[export] locality attributes:

As we saw, the #[export] locality attribute allowed us to Set our option whenever the module is Imported. For our hint, #[export] is the default attribute since Coq 8.18, but if you need to work with older versions, you should add it to your Hints, if you want them to be available after import. Now, for the #[global] setting. Again, it is often not supported and when it is, commands have the default behaviour (short names and features disabled except when the module is Imported), except when Setting options or with the Hint command (and typeclass instances): hints and settings with the #[global] attributes persist outside of the module, even if it is not Imported. Let us restore the state of the Universe Polymorphism option:

We didn't even import the module, and the setting is already there! This should really be used with caution as it imposes our choice to any user who Requires our library file. Our hints have also been silently added to our database, even without Import. Since hint databases have a tendency to make proofs very brittle this should also be used with caution.

Exercise: why could we use the same name in the two previous lemmas?

3. Exporting a module

Contrarily to Required library files, module imports are not transitive. Consider the following nested module:

This situation may seem contrived, but imagine rather a library file, say A.v which Requires and Imports another library file, say B.v. At this point, we are in a situation similar to being in yet another file C.v which has Required the file A.v (but not yet Imported it). We can access the content of A with qualified names.

If we Import A, we get short names for its content, including the module B itself.

But, even though B is Imported in A, we cannot use a short name for this_is_b:

This behaviour is actually very sane. Some programmers may have Imported modules in library files for convenience, this should not affect every users of their library. Still, there is a way (and sometimes good reason) to both Import a module (which could be a file) and mark it for importation whenever the current module (or file) is Imported: we use the Export command.

Since B' was Exported in A', Importing A' also Imports B':

As this gives less control to the final user, Exporting modules should not be done lightly. A common usage is to write a library split in small library files and a summary file Exporting all of them, so that requiring and importing it makes all the library content available at once. Another use case is when Importing a module (say about real numbers) would only really make sense when another one (say about integers) is also imported. Other than that, Export behaves much like Import: it allows us to use short names for constants, activates module features such as Hints, Notations, etc. One can also use selective import with Export, and locality attributes behave the same. Finally, it is possible to Require and Export a library file at the same time. For instance, the following command in Coq.Arith.Arith_base: From Coq Require Export Arith.PeanoNat. imports PeanoNat's content in Coq.Arith.Arith_base as well as in any file which Requires and Imports (or Exports) Coq.Arith.Arith_base.