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.
-
Command
Module ImportExport? ident module_binder* of_module_type? := module_expr_inl+<+?
¶ - |[ no inline ]
Defines a module named
ident
. See the examples here.The
Import
andExport
flags specify whether the module should be automatically imported or exported.Specifying
module_binder*
starts a functor with parameters given by themodule_binder
s. (A functor is a function from modules to modules.)of_module_type
specifies the module type.<: module_type_inl+
starts a module that satisfies eachmodule_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 withEnd
instead of in a singleModule
command. Interactively defining themodule_expr_inl
s in a series ofInclude
commands is equivalent to giving them all in a single non-interactiveModule
command.The ! prefix indicates that any assumption command (such as
Axiom
) with anInline
clause in the type of the functor arguments will be ignored.
-
Command
Module Type ident module_binder* <: module_type_inl* := module_type_inl+<+?
¶ Defines a module type named
ident
. See the example here.Specifying
module_binder*
starts a functor type with parameters given by themodule_binder
s.:= 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 withEnd
instead of in a singleModule Type
command. Interactively defining themodule_type_inl
s in a series ofInclude
commands is equivalent to giving them all in a single non-interactiveModule 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.
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.
Note
Interactive modules and module types can be nested.
Interactive modules and module types can't be defined inside of sections. Sections can be defined inside of interactive modules and module types.
Hints and notations (the Hint and
Notation
commands) can also appear inside interactive modules and module types. Note that with module definitions like:Module ident1 : module_type := ident2.
or
Module ident1 : module_type.
Include ident2.
End ident1.
hints and the like valid for
ident1
are the ones defined inmodule_type
rather then those defined inident2
(or the module body).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).Assumptions such as
Axiom
that include theInline
clause will be automatically expanded when the functor is applied, except when the function application is prefixed by!
.
-
Command
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 instantiatemodule_type_inl
with the current interactive module.Including multiple modules is a single
Include
is equivalent to including each module in a separateInclude
command.
-
Command
Include Type module_type_inl+<+
¶ Deprecated since version 8.3: Use
Include
instead.
-
Command
Declare Module ImportExport? ident module_binder* : module_type_inl
¶ Declares a module
ident
of typemodule_type_inl
.If
module_binder
s are specified, declares a functor with parameters given by the list ofmodule_binder
s.
-
Command
Import filtered_import+
¶ If
qualid
denotes a valid basic module (i.e. its module type is a signature), makes its components available by their short names.Example
- Module Mod.
- Interactive Module Mod started
- Definition T:=nat.
- T is defined
- Check T.
- T : Set
- End Mod.
- Module Mod is defined
- Check Mod.T.
- Mod.T : Set
- Fail Check T.
- The command has indeed failed with message: The reference T was not found in the current environment.
- Import Mod.
- Check T.
- T : Set
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 theImport
command. Such declarations are only accessible through their fully qualified name.Example
- Module A.
- Interactive Module A started
- Module B.
- Interactive Module B started
- Local Definition T := nat.
- T is defined
- End B.
- Module B is defined
- End A.
- Module A is defined
- Import A.
- Check B.T.
- Toplevel input, characters 6-9: > Check B.T. > ^^^ Error: The reference B.T was not found in the current environment.
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
.Example
- Module A.
- Interactive Module A started
- Module B.
- Interactive Module B started
- Inductive T := C.
- T is defined T_rect is defined T_ind is defined T_rec is defined T_sind is defined
- Definition U := nat.
- U is defined
- End B.
- Module B is defined
- Definition Z := Prop.
- Z is defined
- End A.
- Module A is defined
- Import A(B.T(..), Z).
- Check B.T.
- B.T : Prop
- Check B.C.
- B.C : B.T
- Check Z.
- Z : Type
- Fail Check B.U.
- The command has indeed failed with message: The reference B.U was not found in the current environment.
- Check A.B.U.
- A.B.U : Set
-
Command
Export filtered_import+
¶ Similar to
Import
, except that when the module containing this command is imported, thequalid+
are imported as well.The selective import syntax also works with Export.
-
Flag
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
andPrint Module Type
.
Examples¶
Example: Defining a simple module interactively
- Module M.
- Interactive Module M started
- Definition T := nat.
- T is defined
- Definition x := 0.
- x is defined
- Definition y : bool.
- 1 subgoal ============================ bool
- exact true.
- No more subgoals.
- Defined.
- End M.
- Module M is defined
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:
- Print M.x.
- M.x = 0 : nat
Example: Defining a simple module type interactively
- Module Type SIG.
- Interactive Module Type SIG started
- Parameter T : Set.
- T is declared
- Parameter x : T.
- x is declared
- End SIG.
- Module Type SIG is defined
Example: 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
.
- Module N : SIG with Definition T := nat := M.
- Module N is defined
- Print N.T.
- N.T = nat : Set
- Print N.x.
- *** [ N.x : N.T ]
- Fail Print N.y.
- The command has indeed failed with message: N.y not a defined object.
- Module M.
- Interactive Module M started
- Definition T := nat.
- T is defined
- Definition x := 0.
- x is defined
- Definition y : bool.
- 1 subgoal ============================ bool
- exact true.
- No more subgoals.
- Defined.
- End M.
- Module M is defined
- Module Type SIG.
- Interactive Module Type SIG started
- Parameter T : Set.
- T is declared
- Parameter x : T.
- x is declared
- End SIG.
- Module Type SIG is defined
The definition of N
using the module type expression SIG
with
Definition T := nat
is equivalent to the following one:
- Module Type SIG'.
- Interactive Module Type SIG' started
- Definition T : Set := nat.
- T is defined
- Parameter x : T.
- x is declared
- End SIG'.
- Module Type SIG' is defined
- Module N : SIG' := M.
- Module N is defined
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
- Module P <: SIG := M.
- Module P is defined
- Print P.y.
- P.y = true : bool
Example: Creating a functor (a module with parameters)
- Module Two (X Y: SIG).
- Interactive Module Two started
- Definition T := (X.T * Y.T)%type.
- T is defined
- Definition x := (X.x, Y.x).
- x is defined
- End Two.
- Module Two is defined
and apply it to our modules and do some computations:
- Module Q := Two M N.
- Module Q is defined
- Eval compute in (fst Q.x + snd Q.x).
- = N.x : nat
Example: A module type with two sub-modules, sharing some fields
- Module Type SIG2.
- Interactive Module Type SIG2 started
- Declare Module M1 : SIG.
- Module M1 is declared
- Module M2 <: SIG.
- Interactive Module M2 started
- Definition T := M1.T.
- T is defined
- Parameter x : T.
- x is declared
- End M2.
- Module M2 is defined
- End SIG2.
- Module Type SIG2 is defined
- Module Mod <: SIG2.
- Interactive Module Mod started
- Module M1.
- Interactive Module M1 started
- Definition T := nat.
- T is defined
- Definition x := 1.
- x is defined
- End M1.
- Module M1 is defined
- Module M2 := M.
- Module M2 is defined
- End Mod.
- Module Mod is defined
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 the global 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 \(S_1\) is a subtype of a structure \(S_2\).
\(\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
- \[\frac{% \WF{E;E′}{}% }{% \WFT{E}{ \Struct~E′ ~\End}% }\]
- WF-FUN
- \[\frac{% \WFT{E; \ModS{X}{S}}{ \ovl{S′} }% }{% \WFT{E}{ \Functor(X:S)~S′}% }\]
Evaluation of structures to weak head normal form:
- WEVAL-APP
- \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S}{\Functor(X:S_1 )~S_2}~~~~~\WEV{E}{S_1}{\ovl{S_1}} \\% \hspace{3em}% \WTM{E}{p}{S_3}~~~~~ \WS{E}{S_3}{\ovl{S_1}}% \hspace{3em}% \end{array}% }{% \WEV{E}{S~p}{S_2 \{p/X,t_1 /p_1 .c_1 ,…,t_n /p_n.c_n \}}% }\end{split}\]
In the last rule, \(\{t_1 /p_1 .c_1 ,…,t_n /p_n .c_n \}\) is the resulting substitution from the inlining mechanism. We substitute in \(S\) the inlined fields \(p_i .c_i\) from \(\ModS{X}{S_1 }\) by the corresponding delta- reduced term \(t_i\) in \(p\).
- WEVAL-WITH-MOD
- \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% E[] ⊢ S \lra \Struct~e_1 ;…;e_i ; \ModS{X}{S_1 };e_{i+2} ;… ;e_n ~\End \\% \hspace{3em}% E;e_1 ;…;e_i [] ⊢ S_1 \lra \ovl{S_1} ~~~~~~% \hspace{3em}% E[] ⊢ p : S_2 \\% \hspace{3em}% E;e_1 ;…;e_i [] ⊢ S_2 <: \ovl{S_1}% \hspace{3em}% \end{array}% }{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S~\with~x := p}{}\\% \hspace{3em}% \Struct~e_1 ;…;e_i ; \ModA{X}{p};e_{i+2} \{p/X\} ;…;e_n \{p/X\} ~\End% \hspace{3em}% \end{array}% }\end{split}\]
- WEVAL-WITH-MOD-REC
- \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1}{S_1 };e_{i+2} ;… ;e_n ~\End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}}% \hspace{3em}% \end{array}% }{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S~\with~X_1.p := p_1}{} \\% \hspace{3em}% \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% \hspace{3em}% \end{array}% }\end{split}\]
- WEVAL-WITH-DEF
- \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S}{\Struct~e_1 ;…;e_i ;\Assum{}{c}{T_1};e_{i+2} ;… ;e_n ~\End} \\% \hspace{3em}% \WS{E;e_1 ;…;e_i }{Def()(c:=t:T)}{\Assum{}{c}{T_1}}% \hspace{3em}% \end{array}% }{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S~\with~c := t:T}{} \\% \hspace{3em}% \Struct~e_1 ;…;e_i ;Def()(c:=t:T);e_{i+2} ;… ;e_n ~\End% \hspace{3em}% \end{array}% }\end{split}\]
- WEVAL-WITH-DEF-REC
- \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1 }{S_1 };e_{i+2} ;… ;e_n ~\End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}}% \hspace{3em}% \end{array}% }{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S~\with~X_1.p := t:T}{} \\% \hspace{3em}% \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2} };e_{i+2} ;… ;e_n ~\End% \hspace{3em}% \end{array}% }\end{split}\]
- WEVAL-PATH-MOD1
- \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{p}{\Struct~e_1 ;…;e_i ; \Mod{X}{S}{S_1};e_{i+2} ;… ;e_n End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}}% \hspace{3em}% \end{array}% }{% E[] ⊢ p.X \lra \ovl{S}% }\end{split}\]
- WEVAL-PATH-MOD2
- \[\frac{% \WF{E}{}% \hspace{3em}% \Mod{X}{S}{S_1}∈ E% \hspace{3em}% \WEV{E}{S}{\ovl{S}}% }{% \WEV{E}{X}{\ovl{S}}% }\]
- WEVAL-PATH-ALIAS1
- \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModA{X}{p_1};e_{i+2} ;… ;e_n End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{p_1}{\ovl{S}}% \hspace{3em}% \end{array}% }{% \WEV{E}{p.X}{\ovl{S}}% }\end{split}\]
- WEVAL-PATH-ALIAS2
- \[\frac{% \WF{E}{}% \hspace{3em}% \ModA{X}{p_1 }∈ E% \hspace{3em}% \WEV{E}{p_1}{\ovl{S}}% }{% \WEV{E}{X}{\ovl{S}}% }\]
- WEVAL-PATH-TYPE1
- \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModType{Y}{S};e_{i+2} ;… ;e_n End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}}% \hspace{3em}% \end{array}% }{% \WEV{E}{p.Y}{\ovl{S}}% }\end{split}\]
- WEVAL-PATH-TYPE2
- \[\frac{% \WF{E}{}% \hspace{3em}% \ModType{Y}{S}∈ E% \hspace{3em}% \WEV{E}{S}{\ovl{S}}% }{% \WEV{E}{Y}{\ovl{S}}% }\]
Rules for typing module:
- MT-EVAL
- \[\frac{% \WEV{E}{p}{\ovl{S}}% }{% E[] ⊢ p : \ovl{S}% }\]
- MT-STR
- \[\frac{% 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{split}\frac{% \begin{array}{c}% \hspace{3em}% \WS{E;e_1 ;…;e_n }{e_{σ(i)}}{e'_i ~\for~ i=1..m} \\% \hspace{3em}% σ : \{1… m\} → \{1… n\} ~\injective% \hspace{3em}% \end{array}% }{% \WS{E}{\Struct~e_1 ;…;e_n ~\End}{~\Struct~e'_1 ;…;e'_m ~\End}% }\end{split}\]
- MSUB-FUN
- \[\frac{% \WS{E}{\ovl{S_1'}}{\ovl{S_1}}% \hspace{3em}% \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
- \[\frac{% E[] ⊢ T_1 ≤_{βδιζη} T_2% }{% \WS{E}{\Assum{}{c}{T_1 }}{\Assum{}{c}{T_2 }}% }\]
- DEF-ASSUM
- \[\frac{% E[] ⊢ T_1 ≤_{βδιζη} T_2% }{% \WS{E}{\Def{}{c}{t}{T_1 }}{\Assum{}{c}{T_2 }}% }\]
- ASSUM-DEF
- \[\frac{% E[] ⊢ T_1 ≤_{βδιζη} T_2% \hspace{3em}% E[] ⊢ c =_{βδιζη} t_2% }{% \WS{E}{\Assum{}{c}{T_1 }}{\Def{}{c}{t_2 }{T_2 }}% }\]
- DEF-DEF
- \[\frac{% E[] ⊢ T_1 ≤_{βδιζη} T_2% \hspace{3em}% E[] ⊢ t_1 =_{βδιζη} t_2% }{% \WS{E}{\Def{}{c}{t_1 }{T_1 }}{\Def{}{c}{t_2 }{T_2 }}% }\]
- IND-IND
- \[\frac{% E[] ⊢ Γ_P =_{βδιζη} Γ_P'% \hspace{3em}% E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C'% \hspace{3em}% E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I'% }{% \WS{E}{\ind{Γ_P}{Γ_C}{Γ_I}}{\ind{Γ_P'}{Γ_C'}{Γ_I'}}% }\]
- INDP-IND
- \[\frac{% E[] ⊢ Γ_P =_{βδιζη} Γ_P'% \hspace{3em}% E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C'% \hspace{3em}% E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I'% }{% \WS{E}{\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{\ind{Γ_P'}{Γ_C'}{Γ_I'}}% }\]
- INDP-INDP
- \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% E[] ⊢ Γ_P =_{βδιζη} Γ_P'% \hspace{3em}% E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' \\% \hspace{3em}% E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I'% \hspace{3em}% E[] ⊢ p =_{βδιζη} p'% \hspace{3em}% \end{array}% }{% \WS{E}{\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{\Indp{}{Γ_P'}{Γ_C'}{Γ_I'}{p'}}% }\end{split}\]
- MOD-MOD
- \[\frac{% \WS{E}{S_1}{S_2}% }{% \WS{E}{\ModS{X}{S_1 }}{\ModS{X}{S_2 }}% }\]
- ALIAS-MOD
- \[\frac{% E[] ⊢ p : S_1% \hspace{3em}% \WS{E}{S_1}{S_2}% }{% \WS{E}{\ModA{X}{p}}{\ModS{X}{S_2 }}% }\]
- MOD-ALIAS
- \[\frac{% E[] ⊢ p : S_2% \hspace{3em}% \WS{E}{S_1}{S_2}% \hspace{3em}% E[] ⊢ X =_{βδιζη} p% }{% \WS{E}{\ModS{X}{S_1 }}{\ModA{X}{p}}% }\]
- ALIAS-ALIAS
- \[\frac{% E[] ⊢ p_1 =_{βδιζη} p_2% }{% \WS{E}{\ModA{X}{p_1 }}{\ModA{X}{p_2 }}% }\]
- MODTYPE-MODTYPE
- \[\frac{% \WS{E}{S_1}{S_2}% \hspace{3em}% \WS{E}{S_2}{S_1}% }{% \WS{E}{\ModType{Y}{S_1 }}{\ModType{Y}{S_2 }}% }\]
New environment formation rules
- WF-MOD1
- \[\frac{% \WF{E}{}% \hspace{3em}% \WFT{E}{S}% }{% WF(E; \ModS{X}{S})[]% }\]
- WF-MOD2
- \[\frac{% \WS{E}{S_2}{S_1}% \hspace{3em}% \WF{E}{}% \hspace{3em}% \WFT{E}{S_1}% \hspace{3em}% \WFT{E}{S_2}% }{% \WF{E; \Mod{X}{S_1}{S_2}}{}% }\]
- WF-ALIAS
- \[\frac{% \WF{E}{}% \hspace{3em}% E[] ⊢ p : S% }{% \WF{E, \ModA{X}{p}}{}% }\]
- WF-MODTYPE
- \[\frac{% \WF{E}{}% \hspace{3em}% \WFT{E}{S}% }{% \WF{E, \ModType{Y}{S}}{}% }\]
- WF-IND
- \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WF{E;\ind{Γ_P}{Γ_C}{Γ_I}}{} \\% \hspace{3em}% E[] ⊢ p:~\Struct~e_1 ;…;e_n ;\ind{Γ_P'}{Γ_C'}{Γ_I'};… ~\End : \\% \hspace{3em}% E[] ⊢ \ind{Γ_P'}{Γ_C'}{Γ_I'} <: \ind{Γ_P}{Γ_C}{Γ_I}% \hspace{3em}% \end{array}% }{% \WF{E; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p} }{}% }\end{split}\]
Component access rules
- ACC-TYPE1
- \[\frac{% E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Assum{}{c}{T};… ~\End% }{% E[Γ] ⊢ p.c : T% }\]
- ACC-TYPE2
- \[\frac{% 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
- \[\frac{% 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 \([p_1 :P_1 ;…;p_r :P_r ]\), \(Γ_I\) is \([I_1 :A_1 ;…;I_k :A_k ]\), and \(Γ_C\) is \([c_1 :C_1 ;…;c_n :C_n ]\).
- ACC-IND1
- \[\frac{% 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
- \[\frac{% 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
- \[\frac{% E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~\End% }{% E[] ⊢ p.I_i \triangleright_δ p'.I_i% }\]
- ACC-INDP2
- \[\frac{% 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 identifiers). 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 By 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 By command line options).
Qualified identifiers¶
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 Top-level 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.
Example
- Check 0.
- 0 : nat
- Definition nat := bool.
- nat is defined
- Check 0.
- 0 : Datatypes.nat
- Check Datatypes.nat.
- Datatypes.nat : Set
- Locate nat.
- Constant Top.nat Inductive Coq.Init.Datatypes.nat (shorter name to refer to it in current context is Datatypes.nat)
See also
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 with 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 with 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 By command line options for a more general view over the Coq command line options.
Controlling the scope of commands with locality attributes¶
Many commands have effects that apply only within a specific scope,
typically the section or the module in which the command was
called. Locality attributes can alter the scope of
the effect. Below, we give the semantics of each locality attribute
while noting a few exceptional commands for which local
and
global
attributes are interpreted differently.
-
Attribute
local
¶ The
local
attribute limits the effect of the command to the current scope (section or module).The
Local
prefix is an alternative syntax for thelocal
attribute (seelegacy_attr
).Note
Warning
Exception: when
local
is applied toDefinition
,Theorem
or their variants, its semantics are different: it makes the defined objects available only through their fully-qualified names rather than their unqualified names after anImport
.
-
Attribute
export
¶ The
export
attribute makes the effect of the command persist when the section is closed and applies the effect when the module containing the command is imported.Commands supporting this attribute include
Set
,Unset
and the Hint commands, although the latter don't support it within sections.
-
Attribute
global
¶ The
global
attribute makes the effect of the command persist even when the current section or module is closed. Loading the file containing the command (possibly transitively) applies the effect of the command.The
Global
prefix is an alternative syntax for theglobal
attribute (seelegacy_attr
).