.. _themodulesystem:

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 :math:`p` and can be
either a module variable :math:`X` or, if :math:`p′` is an access path
and :math:`id` an identifier, then :math:`p′.id` is an access path.


**Structure element.** A structure element is denoted by :math:`e` and
is either a definition of a :term:`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 :math:`S` and can be:

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

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


**Module alias.** A module alias is written :math:`\ModA{X}{p}`
and consists of a module variable :math:`X` and a module path
:math:`p`.

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

.. extracted from Gallina extensions chapter

Using modules
-------------

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


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

   .. insertprodn module_binder module_expr_inl

   .. prodn::
      module_binder ::= ( {? {| Import | Export } {? @import_categories } } {+ @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 :token:`ident`.  See the examples :ref:`here<module_examples>`.

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

   Specifying :n:`{* @module_binder }` starts a functor with
   parameters given by the :n:`@module_binder`\s.  (A *functor* is a function
   from modules to modules.)

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

   .. todo: would like to find a better term than "interactive", not very descriptive

   :n:`:= {+<+ @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 :cmd:`End`
   instead of in a single :cmd:`Module` command.
   Interactively defining the :n:`@module_expr_inl`\s in a series of
   :cmd:`Include` commands is equivalent to giving them all in a single
   non-interactive :cmd:`Module` command.

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

   .. todo: What is an Inline directive?  sb command but still unclear.  Maybe referring to the
      "inline" in functor_app_annot?  or assumption_token Inline assum_list?

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

   Defines a module type named :n:`@ident`.  See the example :ref:`here<example_def_simple_module_type>`.

   Specifying :n:`{* @module_binder }` starts a functor type with
   parameters given by the :n:`@module_binder`\s.

   :n:`:= {+<+ @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 :cmd:`End`
   instead of in a single :cmd:`Module Type` command.
   Interactively defining the :n:`@module_type_inl`\s in a series of
   :cmd:`Include` commands is equivalent to giving them all in a single
   non-interactive :cmd:`Module Type` command.

.. _terminating_module:

**Terminating an interactive module or module type definition**

Interactive modules are terminated with the :cmd:`End` command, which
is also used to terminate :ref:`Sections<section-mechanism>`.
:n:`End @ident` closes the interactive module or module type :token:`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 (:term:`constants <constant>`, inductive types, submodules etc.)
are now available through the dot notation.

.. exn:: Signature components for field @ident do not match.
    :undocumented:

.. exn:: The field @ident is missing in @qualid.
   :undocumented:

.. |br| raw:: html

    <br>

.. note::

  #. Interactive modules and module types can be nested.
  #. Interactive modules and module types can't be defined inside of :ref:`sections<section-mechanism>`.
     Sections can be defined inside of interactive modules and module types.
  #. Hints and notations (the :ref:`Hint <creating_hints>` and :cmd:`Notation`
     commands) can also appear inside interactive
     modules and module types. Note that with module definitions like:

     :n:`Module @ident__1 : @module_type := @ident__2.`

     or

     :n:`Module @ident__1 : @module_type.` |br|
     :n:`Include @ident__2.` |br|
     :n:`End @ident__1.`

     hints and the like valid for :n:`@ident__1` are the ones defined in :n:`@module_type`
     rather then those defined in :n:`@ident__2` (or the module body).
  #. Within an interactive module type definition, the :cmd:`Parameter` command declares a
     :term:`constant` instead of definining a new axiom (which it does when not in a module type definition).
  #. Assumptions such as :cmd:`Axiom` that include the :n:`Inline` clause will be automatically
     expanded when the functor is applied, except when the function application is prefixed by ``!``.

.. cmd:: Include @module_type_inl {* <+ @module_expr_inl }

   Includes the content of module(s) in the current
   interactive module. Here :n:`@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 :n:`@module_type_inl` with the current
   interactive module.

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

.. cmd:: Include Type {+<+ @module_type_inl }

   .. deprecated:: 8.3

      Use :cmd:`Include` instead.

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

   Declares a module :token:`ident` of type :token:`module_type_inl`.

   If :n:`@module_binder`\s are specified, declares a functor with parameters given by the list of
   :token:`module_binder`\s.

.. cmd:: Import {? @import_categories } {+ @filtered_import }

   .. insertprodn import_categories filtered_import

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

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

   .. example::

      .. coqtop:: reset in

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

      .. coqtop:: 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 :ref:`Notations`).

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

   .. example::

      .. coqtop:: in

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

      .. coqtop:: 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 :term:`constants <constant>`, 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 :term:`constant` in the same module whose
   name is the inductive type's name suffixed by one of ``_sind``,
   ``_ind``, ``_rec`` or ``_rect``.

   .. example::

      .. coqtop:: reset in

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

      .. coqtop:: all

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

   .. warn:: Cannot import local constant, it will be ignored.

      This warning is printed when a name in the list of names to
      import was declared as a local constant, and the name is not imported.

   Putting a list of :n:`@import_categories` after ``Import`` will
   restrict activation of features according to those categories.
   Currently supported categories are:

   - ``coercions`` corresponding to :cmd:`Coercion`.

   - ``hints`` corresponding to the `Hint` commands (e.g. :cmd:`Hint
     Resolve` or :cmd:`Hint Rewrite`) and :ref:`typeclass
     <typeclasses>` instances.

   - ``canonicals`` corresponding to :cmd:`Canonical Structure`.

   - ``notations`` corresponding to :cmd:`Notation` (including
     :cmd:`Reserved Notation`), scope controls (:cmd:`Delimit Scope`,
     :cmd:`Bind Scope`, :cmd:`Open Scope`) and :ref:`Abbreviations`.

   - ``ltac.notations`` corresponding to :cmd:`Tactic Notation`.

   - ``ltac2.notations`` corresponding to :cmd:`Ltac2 Notation`
     (including Ltac2 abbreviations).

   Plugins may define their own categories.

.. cmd:: Export {? @import_categories } {+ @filtered_import }

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

   The selective import syntax also works with Export.

   .. exn:: @qualid is not a module.
      :undocumented:

   .. warn:: Trying to mask the absolute name @qualid!
      :undocumented:

.. cmd:: Print Module @qualid

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

.. cmd:: Print Module Type @qualid

   Prints the module type corresponding to :n:`@qualid`.

.. flag:: Short Module Printing

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

.. _module_examples:

Examples
~~~~~~~~

.. example:: Defining a simple module interactively

    .. coqtop:: in

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

    .. coqtop:: all

       Definition y : bool.
       exact true.

    .. coqtop:: in

       Defined.
       End M.

Inside a module one can define :term:`constants <constant>`, 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:

.. coqtop:: all

   Print M.x.

.. _example_def_simple_module_type:

.. example:: Defining a simple module type interactively

   .. coqtop:: in

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

.. _example_filter_module:

.. example:: Creating a new module that omits some items from an existing module

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

   .. coqtop:: all

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

   .. reset to remove N (undo in last coqtop block doesn't seem to do that), invisibly redefine M, SIG
   .. coqtop:: 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 :g:`N` using the module type expression :g:`SIG` with
:g:`Definition T := nat` is equivalent to the following one:

.. coqtop:: in

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

   Module N : SIG' := M.

.. exn:: No field named @ident in @qualid.

   Raised when the final :n:`@ident` in the left-hand side :n:`@qualid` of
   a :n:`@with_declaration` is applied to a module type :n:`@qualid` that
   has no field named this :n:`@ident`.

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

.. coqtop:: in

   Module P <: SIG := M.

.. coqtop:: all

   Print P.y.

.. example:: Creating a functor (a module with parameters)

   .. coqtop:: 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:

   .. coqtop:: in


      Module Q := Two M N.

   .. coqtop:: all

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

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

   .. coqtop:: in

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

   .. coqtop:: 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 :ref:`The-terms`. The
environments, apart from definitions of :term:`constants <constant>` and inductive types now also
hold any other structure elements. Terms, apart from variables, :term:`constants <constant>` and
complex terms, also include access paths.

We also need additional typing judgments:


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

The rules for forming structures are the following:

.. inference:: WF-STR

   \WF{E;E′}{}
   ------------------------
   \WFT{E}{ \Struct~E′ ~\End}

.. inference:: WF-FUN

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


Evaluation of structures to weak head normal form:

.. inference:: 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}{\subst{S_2}{X}{p}}


.. inference:: 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};\subst{e_{i+2}}{X}{p} ;…;\subst{e_n}{X}{p} ~\End
   \end{array}

.. inference:: 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}};\subst{e_{i+2}}{X_1.p}{p_1} ;…;\subst{e_n}{X_1.p}{p_1} ~\End
   \end{array}

.. inference:: WEVAL-WITH-DEF

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

.. inference:: 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}

.. inference:: 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}

.. inference:: WEVAL-PATH-MOD2

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

.. inference:: 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}}

.. inference:: WEVAL-PATH-ALIAS2

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

.. inference:: 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}}

.. inference:: WEVAL-PATH-TYPE2

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


Rules for typing module:

.. inference:: MT-EVAL

   \WEV{E}{p}{\ovl{S}}
   --------------------------
   E[] ⊢ p : \ovl{S}

.. inference:: 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 :math:`S/p` has the following
meaning:


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

    + :math:`(c:=t:T)/p = (c:=t:T)`
    + :math:`(c:U)/p = (c:=p.c:U)`
    + :math:`\ModS{X}{S}/p = \ModA{X}{p.X}`
    + :math:`\ModA{X}{p′}/p = \ModA{X}{p′}`
    + :math:`\ind{r}{Γ_I}{Γ_C}/p = \Indp{r}{Γ_I}{Γ_C}{p}`
    + :math:`\Indpstr{r}{Γ_I}{Γ_C}{p'}{p} = \Indp{r}{Γ_I}{Γ_C}{p'}`

+ if :math:`S \lra \Functor(X:S′)~S″` then :math:`S/p=S`


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

The module subtyping rules:

.. inference:: 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}

.. inference:: 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:

.. inference:: ASSUM-ASSUM

   E[] ⊢ T_1 ≤_{βδιζη} T_2
   --------------------------
   \WS{E}{(c:T_1)}{(c:T_2)}

.. inference:: DEF-ASSUM

   E[] ⊢ T_1 ≤_{βδιζη} T_2
   --------------------------
   \WS{E}{(c:=t:T_1)}{(c:T_2)}

.. inference:: ASSUM-DEF

   E[] ⊢ T_1 ≤_{βδιζη} T_2
   E[] ⊢ c =_{βδιζη} t_2
   --------------------------
   \WS{E}{(c:T_1)}{(c:=t_2:T_2)}

.. inference:: DEF-DEF

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

.. inference:: IND-IND

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

.. inference:: INDP-IND

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

.. inference:: INDP-INDP

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

.. inference:: MOD-MOD

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

.. inference:: ALIAS-MOD

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

.. inference:: MOD-ALIAS

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

.. inference:: ALIAS-ALIAS

   E[] ⊢ p_1 =_{βδιζη} p_2
   --------------------------
   \WS{E}{\ModA{X}{p_1 }}{\ModA{X}{p_2 }}

.. inference:: 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


.. inference:: WF-MOD1

   \WF{E}{}
   \WFT{E}{S}
   --------------------------
   \WF{E; \ModS{X}{S}}{}

.. inference:: WF-MOD2

   \WS{E}{S_2}{S_1}
   \WF{E}{}
   \WFT{E}{S_1}
   \WFT{E}{S_2}
   --------------------------
   \WF{E; \ModImp{X}{S_1}{S_2}}{}

.. inference:: WF-ALIAS

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

.. inference:: WF-MODTYPE

   \WF{E}{}
   \WFT{E}{S}
   --------------------------
   \WF{E; \ModType{Y}{S}}{}

.. inference:: WF-IND

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


Component access rules


.. inference:: ACC-TYPE1

   E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;(c:T);… ~\End
   --------------------------
   E[Γ] ⊢ p.c : T

.. inference:: ACC-TYPE2

   E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;(c:=t:T);… ~\End
   --------------------------
   E[Γ] ⊢ p.c : T

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

.. inference:: ACC-DELTA

    E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;(c:=t:U);… ~\End
    --------------------------
    E[Γ] ⊢ p.c \triangleright_δ t

In the rules below we assume
:math:`Γ_P` is :math:`[p_1{:}P_1 ; …; p_r {:}P_r ]`,
:math:`Γ_I` is :math:`[I_1{:}∀ Γ_P, A_1 ; …; I_k{:}∀ Γ_P, A_k ]`,
and :math:`Γ_C` is :math:`[c_1{:}∀ Γ_P, C_1 ; …; c_n{:}∀ Γ_P, C_n ]`.


.. inference:: ACC-IND1

   E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{r}{Γ_I}{Γ_C};… ~\End
   --------------------------
   E[Γ] ⊢ p.I_j : ∀ Γ_P, A_j

.. inference:: ACC-IND2

   E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{r}{Γ_I}{Γ_C};… ~\End
   --------------------------
   E[Γ] ⊢ p.c_m : ∀ Γ_P, C_m

.. inference:: ACC-INDP1

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

.. inference:: ACC-INDP2

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

.. extracted from Gallina extensions chapter

Libraries and qualified names
---------------------------------

.. _names-of-libraries:

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
:ref:`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 :ref:`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 :ref:`command-line-options`).

.. _qualified-names:

Qualified identifiers
~~~~~~~~~~~~~~~~~~~~~

.. insertprodn qualid field_ident

.. prodn::
   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 :cmd:`Require`, :cmd:`Import` and :cmd:`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 :attr:`local` attribute are only accessible with
their fully qualified name (see :ref:`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.

.. example::

    .. coqtop:: all

       Check 0.

       Definition nat := bool.

       Check 0.

       Check Datatypes.nat.

       Locate nat.

.. seealso:: Commands :cmd:`Locate`.

.. _libraries-and-filesystem:

Libraries and filesystem
~~~~~~~~~~~~~~~~~~~~~~~~

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
either the command line option ``-Q`` `path` ``Lib`` or the command
line option ``-R`` `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 automatically associate a logical path to files in
the repository tree 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
<http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html>`_)
with the same physical-to-logical translation and with an empty logical prefix.

.. todo: Needs a more better explanation of COQPATH and XDG* with example(s)
   and suggest best practices for their use

The choice between ``-Q`` and ``-R`` impacts how ambiguous names are
resolved in :cmd:`Require` (see :ref:`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 :cmd:`Declare ML Module` in
:ref:`compiled-files` to understand the need of the OCaml loadpath.

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

.. _controlling-locality-of-commands:

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 :term:`attributes <attribute>` can alter the scope of
the effect. Below, we give the semantics of each locality attribute
while noting a few exceptional commands for which :attr:`local` and
:attr:`global` attributes are interpreted differently.

.. attr:: local

   This :term:`attribute` limits the effect of the command to the
   current scope (section or module).

   The ``Local`` prefix is an alternative syntax for the :attr:`local`
   attribute (see :n:`@legacy_attr`).

   .. note::

      - For some commands, this is the only locality supported within
        sections (e.g., for :cmd:`Notation`, :cmd:`Ltac` and
        :ref:`Hint <creating_hints>` commands).

      - For some commands, this is the default locality within
        sections even though other locality attributes are supported
        as well (e.g., for the :cmd:`Arguments` command).

   .. warning::

      **Exception:** when :attr:`local` is applied to
      :cmd:`Definition`, :cmd:`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 an :cmd:`Import`.

.. attr:: export

   This :term:`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 :cmd:`Set`, :cmd:`Unset`
   and the :ref:`Hint <creating_hints>` commands, although the latter
   don't support it within sections.

.. attr:: global

   This :term:`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 the
   :attr:`global` attribute (see :n:`@legacy_attr`).

   .. warning::

      **Exception:** for a few commands (like :cmd:`Notation` and
      :cmd:`Ltac`), this attribute behaves like :attr:`export`.

   .. warning::

      We strongly discourage using the :attr:`global` locality
      attribute because the transitive nature of file loading gives
      the user little control. We recommend using the :attr:`export`
      locality attribute where it is supported.