Skip to content

Latest commit

 

History

History
1013 lines (727 loc) · 31.7 KB

modules.rst

File metadata and controls

1013 lines (727 loc) · 31.7 KB
Raw

The Module System

The module system extends the Calculus of Inductive Constructions providing a convenient way to structure large developments as well as a means of massive abstraction.

Modules and module types

Access path. An access path is denoted by p and can be either a module variable X or, if p′ is an access path and id an identifier, then p′.id is an access path.

Structure element. A structure element is denoted by e and is either a definition of a constant, an assumption, a definition of an inductive, a definition of a module, an alias of a module or a module type abbreviation.

Structure expression. A structure expression is denoted by S and can be:

  • an access path p
  • a plain structure $\Struct~e ; … ; e~\End$
  • a functor $\Functor(X:S)~S′$, where X is a module variable, S and S′ are structure expressions
  • an application S p, where S is a structure expression and p an access path
  • a refined structure $S~\with~p := p$′ or $S~\with~p := t:T$ where S is a structure expression, p and p′ are access paths, t is a term and T is the type of t.

Module definition. A module definition is written $\Mod{X}{S}{S'}$ and consists of a module variable X, a module type S which can be any structure expression and optionally a module implementation S′ which can be any structure expression except a refined structure.

Module alias. A module alias is written $\ModA{X}{p}$ and consists of a module variable X and a module path p.

Module type abbreviation. A module type abbreviation is written $\ModType{Y}{S}$, where Y is an identifier and S is any structure expression .

Using modules

The module system provides a way of packaging related elements together, as well as a means of massive abstraction.

Module {? {| Import | Export } } @ident {* @module_binder } {? @of_module_type } {? := {+<+ @module_expr_inl } }

module_binder ::= ( {? {| Import | Export } } {+ @ident } : @module_type_inl ) module_type_inl ::= ! @module_type | @module_type {? @functor_app_annot } functor_app_annot ::= [ inline at level @natural ] | [ no inline ] module_type ::= @qualid | ( @module_type ) | @module_type @module_expr_atom | @module_type with @with_declaration with_declaration ::= Definition @qualid {? @univ_decl } := @term | Module @qualid := @qualid module_expr_atom ::= @qualid | ( {+ @module_expr_atom } ) of_module_type ::= : @module_type_inl | {* <: @module_type_inl } module_expr_inl ::= ! {+ @module_expr_atom } | {+ @module_expr_atom } {? @functor_app_annot }

Defines a module named ident. See the examples here<module_examples>.

The Import and Export flags specify whether the module should be automatically imported or exported.

Specifying {* @module_binder } starts a functor with parameters given by the @module_binders. (A functor is a function from modules to modules.)

@of_module_type specifies the module type. {+ <: @module_type_inl } starts a module that satisfies each @module_type_inl.

:= {+<+ @module_expr_inl } specifies the body of a module or functor definition. If it's not specified, then the module is defined interactively, meaning that the module is defined as a series of commands terminated with End instead of in a single Module command. Interactively defining the @module_expr_inls in a series of Include commands is equivalent to giving them all in a single non-interactive Module command.

The ! prefix indicates that any assumption command (such as Axiom) with an Inline clause in the type of the functor arguments will be ignored.

Module Type @ident {* @module_binder } {* <: @module_type_inl } {? := {+<+ @module_type_inl } }

Defines a module type named @ident. See the example here<example_def_simple_module_type>.

Specifying {* @module_binder } starts a functor type with parameters given by the @module_binders.

:= {+<+ @module_type_inl } specifies the body of a module or functor type definition. If it's not specified, then the module type is defined interactively, meaning that the module type is defined as a series of commands terminated with End instead of in a single Module Type command. Interactively defining the @module_type_inls in a series of Include commands is equivalent to giving them all in a single non-interactive Module Type command.

Terminating an interactive module or module type definition

Interactive modules are terminated with the End command, which is also used to terminate Sections<section-mechanism>. End @ident closes the interactive module or module type ident. If the module type was given, the command verifies that the content of the module matches the module type. If the module is not a functor, its components (constants, inductive types, submodules etc.) are now available through the dot notation.

No such label @ident.

Signature components for label @ident do not match.

The field @ident is missing in @qualid.

Note

  1. Interactive modules and module types can be nested.
  2. Interactive modules and module types can't be defined inside of sections<section-mechanism>. Sections can be defined inside of interactive modules and module types.

  3. Hints and notations (the Hint <creating_hints> and Notation commands) can also appear inside interactive modules and module types. Note that with module definitions like:

    Module @ident__1 : @module_type := @ident__2.

    or

    Module @ident__1 : @module_type. Include @ident__2. End @ident__1.

    hints and the like valid for @ident__1 are the ones defined in @module_type rather then those defined in @ident__2 (or the module body).

  4. Within an interactive module type definition, the Parameter command declares a constant instead of definining a new axiom (which it does when not in a module type definition).
  5. Assumptions such as Axiom that include the Inline clause will be automatically expanded when the functor is applied, except when the function application is prefixed by !.

Include @module_type_inl {* <+ @module_expr_inl }

Includes the content of module(s) in the current interactive module. Here @module_type_inl can be a module expression or a module type expression. If it is a high-order module or module type expression then the system tries to instantiate @module_type_inl with the current interactive module.

Including multiple modules is a single Include is equivalent to including each module in a separate Include command.

Include Type {+<+ @module_type_inl }

8.3

Use Include instead.

Declare Module {? {| Import | Export } } @ident {* @module_binder } : @module_type_inl

Declares a module ident of type module_type_inl.

If @module_binders are specified, declares a functor with parameters given by the list of module_binders.

Import {+ @filtered_import }

filtered_import ::= @qualid {? ( {+, @qualid {? ( .. ) } } ) }

If qualid denotes a valid basic module (i.e. its module type is a signature), makes its components available by their short names.

reset in

Module Mod. Definition T:=nat. Check T. End Mod. Check Mod.T.

all

Fail Check T. Import Mod. Check T.

Some features defined in modules are activated only when a module is imported. This is for instance the case of notations (see Notations).

Declarations made with the local attribute are never imported by the Import command. Such declarations are only accessible through their fully qualified name.

in

Module A. Module B. Local Definition T := nat. End B. End A. Import A.

all fail

Check B.T.

Appending a module name with a parenthesized list of names will make only those names available with short names, not other names defined in the module nor will it activate other features.

The names to import may be constants, inductive types and constructors, and notation aliases (for instance, Ltac definitions cannot be selectively imported). If they are from an inner module to the one being imported, they must be prefixed by the inner path.

The name of an inductive type may also be followed by (..) to import it, its constructors and its eliminators if they exist. For this purpose "eliminator" means a constant in the same module whose name is the inductive type's name suffixed by one of _sind, _ind, _rec or _rect.

reset in

Module A. Module B. Inductive T := C. Definition U := nat. End B. Definition Z := Prop. End A. Import A(B.T(..), Z).

all

Check B.T. Check B.C. Check Z. Fail Check B.U. Check A.B.U.

Export {+ @filtered_import }

Similar to Import, except that when the module containing this command is imported, the {+ @qualid } are imported as well.

The selective import syntax also works with Export.

@qualid is not a module.

Trying to mask the absolute name @qualid!

Print Module @qualid

Prints the module type and (optionally) the body of the module @qualid.

Print Module Type @qualid

Prints the module type corresponding to @qualid.

Short Module Printing

This flag (off by default) disables the printing of the types of fields, leaving only their names, for the commands Print Module and Print Module Type.

Examples

Defining a simple module interactively

in

Module M. Definition T := nat. Definition x := 0.

all

Definition y : bool. exact true.

in

Defined. End M.

Inside a module one can define constants, prove theorems and do anything else that can be done in the toplevel. Components of a closed module can be accessed using the dot notation:

all

Print M.x.

Defining a simple module type interactively

in

Module Type SIG. Parameter T : Set. Parameter x : T. End SIG.

Creating a new module that omits some items from an existing module

Since SIG, the type of the new module N, doesn't define y or give the body of x, which are not included in N.

all

Module N : SIG with Definition T := nat := M. Print N.T. Print N.x. Fail Print N.y.

none reset

Module M. Definition T := nat. Definition x := 0. Definition y : bool. exact true. Defined. End M.

Module Type SIG. Parameter T : Set. Parameter x : T. End SIG.

The definition of N using the module type expression SIG with Definition T := nat is equivalent to the following one:

in

Module Type SIG'. Definition T : Set := nat. Parameter x : T. End SIG'.

Module N : SIG' := M.

If we just want to be sure that our implementation satisfies a given module type without restricting the interface, we can use a transparent constraint

in

Module P <: SIG := M.

all

Print P.y.

Creating a functor (a module with parameters)

in

Module Two (X Y: SIG). Definition T := (X.T * Y.T)%type. Definition x := (X.x, Y.x). End Two.

and apply it to our modules and do some computations:

in

Module Q := Two M N.

all

Eval compute in (fst Q.x + snd Q.x).

A module type with two sub-modules, sharing some fields

in

Module Type SIG2.

Declare Module M1 : SIG. Module M2 <: SIG. Definition T := M1.T. Parameter x : T. End M2.

End SIG2.

in

Module Mod <: SIG2.
Module M1.

Definition T := nat. Definition x := 1.

End M1.

Module M2 := M. End Mod.

Notice that M is a correct body for the component M2 since its T component is nat as specified for M1.T.

Typing Modules

In order to introduce the typing system we first slightly extend the syntactic class of terms and environments given in section The-terms. The environments, apart from definitions of constants and inductive types now also hold any other structure elements. Terms, apart from variables, constants and complex terms, include also access paths.

We also need additional typing judgments:

  • $\WFT{E}{S}$, denoting that a structure S is well-formed,
  • $\WTM{E}{p}{S}$, denoting that the module pointed by p has type S in environment E.
  • $\WEV{E}{S}{\ovl{S}}$, denoting that a structure S is evaluated to a structure S in weak head normal form.
  • $\WS{E}{S_1}{S_2}$ , denoting that a structure S1 is a subtype of a structure S2.
  • $\WS{E}{e_1}{e_2}$ , denoting that a structure element e_1 is more precise than a structure element e_2.

The rules for forming structures are the following:

WF-STR

WF{E;E′}{}

WFT{E}{ Struct~E′ ~End}

WF-FUN

WFT{E; ModS{X}{S}}{ ovl{S′} } --------------------------WFT{E}{ Functor(X:S)~S′}

Evaluation of structures to weak head normal form:

WEVAL-APP

begin{array}{c} WEV{E}{S}{Functor(X:S_1 )~S_2}~~~~~WEV{E}{S_1}{ovl{S_1}} \ WTM{E}{p}{S_3}~~~~~ WS{E}{S_3}{ovl{S_1}} end{array} --------------------------WEV{E}{S~p}{S_2 {p/X,t_1 /p_1 .c_1 ,…,t_n /p_n.c_n }}

In the last rule, {t1/p1.c1, …, tn/pn.cn} is the resulting substitution from the inlining mechanism. We substitute in S the inlined fields pi.ci from $\ModS{X}{S_1 }$ by the corresponding delta-reduced term ti in p.

WEVAL-WITH-MOD

begin{array}{c} E[] ⊢ S lra Struct~e_1 ;…;e_i ; ModS{X}{S_1 };e_{i+2} ;… ;e_n ~End \ E;e_1 ;…;e_i [] ⊢ S_1 lra ovl{S_1} ~~~~~~ E[] ⊢ p : S_2 \ E;e_1 ;…;e_i [] ⊢ S_2 <: ovl{S_1} end{array} ----------------------------------begin{array}{c} WEV{E}{S~with~x := p}{}\ Struct~e_1 ;…;e_i ; ModA{X}{p};e_{i+2} {p/X} ;…;e_n {p/X} ~End end{array}

WEVAL-WITH-MOD-REC

begin{array}{c} WEV{E}{S}{Struct~e_1 ;…;e_i ; ModS{X_1}{S_1 };e_{i+2} ;… ;e_n ~End} \ WEV{E;e_1 ;…;e_i }{S_1~with~p := p_1}{ovl{S_2}} end{array} --------------------------begin{array}{c} WEV{E}{S~with~X_1.p := p_1}{} \ Struct~e_1 ;…;e_i ; ModS{X}{ovl{S_2}};e_{i+2} {p_1 /X_1.p} ;…;e_n {p_1 /X_1.p} ~End end{array}

WEVAL-WITH-DEF

begin{array}{c} WEV{E}{S}{Struct~e_1 ;…;e_i ;Assum{}{c}{T_1};e_{i+2} ;… ;e_n ~End} \ WS{E;e_1 ;…;e_i }{Def()(c:=t:T)}{Assum{}{c}{T_1}} end{array} --------------------------begin{array}{c} WEV{E}{S~with~c := t:T}{} \ Struct~e_1 ;…;e_i ;Def()(c:=t:T);e_{i+2} ;… ;e_n ~End end{array}

WEVAL-WITH-DEF-REC

begin{array}{c} WEV{E}{S}{Struct~e_1 ;…;e_i ; ModS{X_1 }{S_1 };e_{i+2} ;… ;e_n ~End} \ WEV{E;e_1 ;…;e_i }{S_1~with~p := p_1}{ovl{S_2}} end{array} --------------------------begin{array}{c} WEV{E}{S~with~X_1.p := t:T}{} \ Struct~e_1 ;…;e_i ; ModS{X}{ovl{S_2} };e_{i+2} ;… ;e_n ~End end{array}

WEVAL-PATH-MOD1

begin{array}{c} WEV{E}{p}{Struct~e_1 ;…;e_i ; Mod{X}{S}{S_1};e_{i+2} ;… ;e_n End} \ WEV{E;e_1 ;…;e_i }{S}{ovl{S}} end{array} --------------------------E[] ⊢ p.X lra ovl{S}

WEVAL-PATH-MOD2

WF{E}{} Mod{X}{S}{S_1}∈ E WEV{E}{S}{ovl{S}} --------------------------WEV{E}{X}{ovl{S}}

WEVAL-PATH-ALIAS1

begin{array}{c} WEV{E}{p}{~Struct~e_1 ;…;e_i ; ModA{X}{p_1};e_{i+2} ;… ;e_n End} \ WEV{E;e_1 ;…;e_i }{p_1}{ovl{S}} end{array} --------------------------WEV{E}{p.X}{ovl{S}}

WEVAL-PATH-ALIAS2

WF{E}{} ModA{X}{p_1 }∈ E WEV{E}{p_1}{ovl{S}} --------------------------WEV{E}{X}{ovl{S}}

WEVAL-PATH-TYPE1

begin{array}{c} WEV{E}{p}{~Struct~e_1 ;…;e_i ; ModType{Y}{S};e_{i+2} ;… ;e_n End} \ WEV{E;e_1 ;…;e_i }{S}{ovl{S}} end{array} --------------------------WEV{E}{p.Y}{ovl{S}}

WEVAL-PATH-TYPE2

WF{E}{} ModType{Y}{S}∈ E WEV{E}{S}{ovl{S}} --------------------------WEV{E}{Y}{ovl{S}}

Rules for typing module:

MT-EVAL

WEV{E}{p}{ovl{S}}

E[] ⊢ p : ovl{S}

MT-STR

E[] ⊢ p : S

E[] ⊢ p : S/p

The last rule, called strengthening is used to make all module fields manifestly equal to themselves. The notation S/p has the following meaning:

  • if $S\lra~\Struct~e_1 ;…;e_n ~\End$ then $S/p=~\Struct~e_1 /p;…;e_n /p ~\End$ where e/p is defined as follows (note that opaque definitions are processed as assumptions):

    • $\Def{}{c}{t}{T}/p = \Def{}{c}{t}{T}$
    • $\Assum{}{c}{U}/p = \Def{}{c}{p.c}{U}$
    • $\ModS{X}{S}/p = \ModA{X}{p.X}$
    • $\ModA{X}{p′}/p = \ModA{X}{p′}$
    • $\Ind{}{Γ_P}{Γ_C}{Γ_I}/p = \Indp{}{Γ_P}{Γ_C}{Γ_I}{p}$
    • $\Indpstr{}{Γ_P}{Γ_C}{Γ_I}{p'}{p} = \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'}$
  • if $S \lra \Functor(X:S′)~S″$ then S/p = S

The notation $\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}$ denotes an inductive definition that is definitionally equal to the inductive definition in the module denoted by the path p. All rules which have $\Ind{}{Γ_P}{Γ_C}{Γ_I}$ as premises are also valid for $\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}$. We give the formation rule for $\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}$ below as well as the equality rules on inductive types and constructors.

The module subtyping rules:

MSUB-STR

begin{array}{c} WS{E;e_1 ;…;e_n }{e{σ(i)}}{e'_i ~for~ i=1..m} \ σ : {1… m} → {1… n} ~injective end{array} --------------------------WS{E}{Struct~e_1 ;…;e_n ~End}{~Struct~e'_1 ;…;e'_m ~End}

MSUB-FUN

WS{E}{ovl{S_1'}}{ovl{S_1}} WS{E; ModS{X}{S_1'}}{ovl{S_2}}{ovl{S_2'}} --------------------------E[] ⊢ Functor(X:S_1 ) S_2 <: Functor(X:S_1') S_2'

Structure element subtyping rules:

ASSUM-ASSUM

E[] ⊢ T_1 ≤_{βδιζη} T_2

WS{E}{Assum{}{c}{T_1 }}{Assum{}{c}{T_2 }}

DEF-ASSUM

E[] ⊢ T_1 ≤_{βδιζη} T_2

WS{E}{Def{}{c}{t}{T_1 }}{Assum{}{c}{T_2 }}

ASSUM-DEF

E[] ⊢ T_1 ≤_{βδιζη} T_2 E[] ⊢ c =_{βδιζη} t_2 --------------------------WS{E}{Assum{}{c}{T_1 }}{Def{}{c}{t_2 }{T_2 }}

DEF-DEF

E[] ⊢ T_1 ≤_{βδιζη} T_2 E[] ⊢ t_1 =_{βδιζη} t_2 --------------------------WS{E}{Def{}{c}{t_1 }{T_1 }}{Def{}{c}{t_2 }{T_2 }}

IND-IND

E[] ⊢ Γ_P =_{βδιζη} Γ_P' E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' --------------------------WS{E}{ind{Γ_P}{Γ_C}{Γ_I}}{ind{Γ_P'}{Γ_C'}{Γ_I'}}

INDP-IND

E[] ⊢ Γ_P =_{βδιζη} Γ_P' E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' --------------------------WS{E}{Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{ind{Γ_P'}{Γ_C'}{Γ_I'}}

INDP-INDP

begin{array}{c} E[] ⊢ Γ_P =_{βδιζη} Γ_P' E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' \ E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' E[] ⊢ p =_{βδιζη} p' end{array} --------------------------WS{E}{Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{Indp{}{Γ_P'}{Γ_C'}{Γ_I'}{p'}}

MOD-MOD

WS{E}{S_1}{S_2}

WS{E}{ModS{X}{S_1 }}{ModS{X}{S_2 }}

ALIAS-MOD

E[] ⊢ p : S_1 WS{E}{S_1}{S_2} --------------------------WS{E}{ModA{X}{p}}{ModS{X}{S_2 }}

MOD-ALIAS

E[] ⊢ p : S_2 WS{E}{S_1}{S_2} E[] ⊢ X =_{βδιζη} p --------------------------WS{E}{ModS{X}{S_1 }}{ModA{X}{p}}

ALIAS-ALIAS

E[] ⊢ p_1 =_{βδιζη} p_2

WS{E}{ModA{X}{p_1 }}{ModA{X}{p_2 }}

MODTYPE-MODTYPE

WS{E}{S_1}{S_2} WS{E}{S_2}{S_1} --------------------------WS{E}{ModType{Y}{S_1 }}{ModType{Y}{S_2 }}

New environment formation rules

WF-MOD1

WF{E}{} WFT{E}{S} --------------------------WF(E; ModS{X}{S})[]

WF-MOD2

WS{E}{S_2}{S_1} WF{E}{} WFT{E}{S_1} WFT{E}{S_2} --------------------------WF{E; Mod{X}{S_1}{S_2}}{}

WF-ALIAS

WF{E}{} E[] ⊢ p : S --------------------------WF{E, ModA{X}{p}}{}

WF-MODTYPE

WF{E}{} WFT{E}{S} --------------------------WF{E, ModType{Y}{S}}{}

WF-IND

begin{array}{c} WF{E;ind{Γ_P}{Γ_C}{Γ_I}}{} \ E[] ⊢ p:~Struct~e_1 ;…;e_n ;ind{Γ_P'}{Γ_C'}{Γ_I'};… ~End : \ E[] ⊢ ind{Γ_P'}{Γ_C'}{Γ_I'} <: ind{Γ_P}{Γ_C}{Γ_I} end{array} --------------------------WF{E; Indp{}{Γ_P}{Γ_C}{Γ_I}{p} }{}

Component access rules

ACC-TYPE1

E[Γ] ⊢ p :~Struct~e_1 ;…;e_i ;Assum{}{c}{T};… ~End --------------------------E[Γ] ⊢ p.c : T

ACC-TYPE2

E[Γ] ⊢ p :~Struct~e_1 ;…;e_i ;Def{}{c}{t}{T};… ~End --------------------------E[Γ] ⊢ p.c : T

Notice that the following rule extends the delta rule defined in section Conversion-rules

ACC-DELTA

E[Γ] ⊢ p :~Struct~e_1 ;…;e_i ;Def{}{c}{t}{U};… ~End --------------------------E[Γ] ⊢ p.c triangleright_δ t

In the rules below we assume ΓP is [p1 : P1; …; pr : Pr], ΓI is [I1 : A1; …; Ik : Ak], and ΓC is [c1 : C1; …; cn : Cn].

ACC-IND1

E[Γ] ⊢ p :~Struct~e_1 ;…;e_i ;ind{Γ_P}{Γ_C}{Γ_I};… ~End --------------------------E[Γ] ⊢ p.I_j : (p_1 :P_1 )…(p_r :P_r )A_j

ACC-IND2

E[Γ] ⊢ p :~Struct~e_1 ;…;e_i ;ind{Γ_P}{Γ_C}{Γ_I};… ~End --------------------------E[Γ] ⊢ p.c_m : (p_1 :P_1 )…(p_r :P_r )C_m I_j (I_j~p_1 …p_r )_{j=1… k}

ACC-INDP1

E[] ⊢ p :~Struct~e_1 ;…;e_i ; Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~End --------------------------E[] ⊢ p.I_i triangleright_δ p'.I_i

ACC-INDP2

E[] ⊢ p :~Struct~e_1 ;…;e_i ; Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~End --------------------------E[] ⊢ p.c_i triangleright_δ p'.c_i

Libraries and qualified names

Names of libraries

The theories developed in Coq are stored in library files which are hierarchically classified into libraries and sublibraries. To express this hierarchy, library names are represented by qualified identifiers qualid, i.e. as list of identifiers separated by dots (see qualified-names). For instance, the library file Mult of the standard Coq library Arith is named Coq.Arith.Mult. The identifier that starts the name of a library is called a library root. All library files of the standard library of Coq have the reserved root Coq but library filenames based on other roots can be obtained by using Coq commands (coqc, coqtop, coqdep, …) options -Q or -R (see command-line-options). Also, when an interactive Coq session starts, a library of root Top is started, unless option -top or -notop is set (see command-line-options).

Qualified identifiers

qualid ::= @ident {* @field_ident } field_ident ::= .@ident

Library files are modules which possibly contain submodules which eventually contain constructions (axioms, parameters, definitions, lemmas, theorems, remarks or facts). The absolute name, or full name, of a construction in some library file is a qualified identifier starting with the logical name of the library file, followed by the sequence of submodules names encapsulating the construction and ended by the proper name of the construction. Typically, the absolute name Coq.Init.Logic.eq denotes Leibniz’ equality defined in the module Logic in the sublibrary Init of the standard library of Coq.

The proper name that ends the name of a construction is the short name (or sometimes base name) of the construction (for instance, the short name of Coq.Init.Logic.eq is eq). Any partial suffix of the absolute name is a partially qualified name (e.g. Logic.eq is a partially qualified name for Coq.Init.Logic.eq). Especially, the short name of a construction is its shortest partially qualified name.

Coq does not accept two constructions (definition, theorem, …) with the same absolute name but different constructions can have the same short name (or even same partially qualified names as soon as the full names are different).

Notice that the notion of absolute, partially qualified and short names also applies to library filenames.

Visibility

Coq maintains a table called the name table which maps partially qualified names of constructions to absolute names. This table is updated by the commands Require, Import and Export and also each time a new declaration is added to the context. An absolute name is called visible from a given short or partially qualified name when this latter name is enough to denote it. This means that the short or partially qualified name is mapped to the absolute name in Coq name table. Definitions with the local attribute are only accessible with their fully qualified name (see gallina-definitions).

It may happen that a visible name is hidden by the short name or a qualified name of another construction. In this case, the name that has been hidden must be referred to using one more level of qualification. To ensure that a construction always remains accessible, absolute names can never be hidden.

all

Check 0.

Definition nat := bool.

Check 0.

Check Datatypes.nat.

Locate nat.

Commands Locate.

Libraries and filesystem

Note

The questions described here have been subject to redesign in Coq 8.5. Former versions of Coq use the same terminology to describe slightly different things.

Compiled files (.vo and .vio) store sub-libraries. In order to refer to them inside Coq, a translation from file-system names to Coq names is needed. In this translation, names in the file system are called physical paths while Coq names are contrastingly called logical names.

A logical prefix Lib can be associated with a physical path using the command line option -Q path Lib. All subfolders of path are recursively associated to the logical path Lib extended with the corresponding suffix coming from the physical path. For instance, the folder path/fOO/Bar maps to Lib.fOO.Bar. Subdirectories corresponding to invalid Coq identifiers are skipped, and, by convention, subdirectories named CVS or _darcs are skipped too.

Thanks to this mechanism, .vo files are made available through the logical name of the folder they are in, extended with their own basename. For example, the name associated to the file path/fOO/Bar/File.vo is Lib.fOO.Bar.File. The same caveat applies for invalid identifiers. When compiling a source file, the .vo file stores its logical name, so that an error is issued if it is loaded with the wrong loadpath afterwards.

Some folders have a special status and are automatically put in the path. Coq commands associate automatically a logical path to files in the repository trees rooted at the directory from where the command is launched, coqlib/user-contrib/, the directories listed in the $COQPATH, ${XDG_DATA_HOME}/coq/ and ${XDG_DATA_DIRS}/coq/ environment variables (see XDG base directory specification) with the same physical-to-logical translation and with an empty logical prefix.

The command line option -R is a variant of -Q which has the strictly same behavior regarding loadpaths, but which also makes the corresponding .vo files available through their short names in a way similar to the Import command. For instance, -R path Lib associates to the file /path/fOO/Bar/File.vo the logical name Lib.fOO.Bar.File, but allows this file to be accessed through the short names fOO.Bar.File,Bar.File and File. If several files with identical base name are present in different subdirectories of a recursive loadpath, which of these files is found first may be system-dependent and explicit qualification is recommended. The From argument of the Require command can be used to bypass the implicit shortening by providing an absolute root to the required file (see compiled-files).

There also exists another independent loadpath mechanism attached to OCaml object files (.cmo or .cmxs) rather than Coq object files as described above. The OCaml loadpath is managed using the option -I path (in the OCaml world, there is neither a notion of logical name prefix nor a way to access files in subdirectories of path). See the command Declare ML Module in compiled-files to understand the need of the OCaml loadpath.

See command-line-options for a more general view over the Coq command line options.