Chapter 5  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.

5.1  Modules and module types

Access path.

It is denoted by p, it 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.

It 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 module or a module type abbreviation.

Structure expression.

It is denoted by S and can be:

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,

is written ModA(X==p) and consists of a module variable X and a module path p.

Module type abbreviation,

is written ModType(Y:=S), where Y is an identifier and S is any structure expression .

5.2  Typing Modules

In order to introduce the typing system we first slightly extend the syntactic class of terms and environments given in section 4.1. 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:

The rules for forming structures are the following:

WF-STR
 WF(E;E′)[]
E[] ⊢  WF( Struct E′  End)
WF-FUN
E; Mod(X:S)[] ⊢  WF(
S
)
E[] ⊢  WF( Functor(X:SS′)

Evaluation of structures to weak head normal form:

WEVAL-APP
    E[] ⊢ S —→ Functor(X:S1S2     E[] ⊢ S1 —→ S1
    E[] ⊢ p : S3     E[] ⊢ S3 <: 
S1
E[] ⊢ S p —→ S2{p/X,t1/p1.c1,…,tn/pn.cn}

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 form Mod(X:S1) by the corresponding delta-reduced term ti in p.

WEVAL-WITH-MOD
    E[] ⊢ S —→ Struct e1;…;ei; Mod(X:S1);ei+2;… ;en  End     E;e1;…;ei[] ⊢ S1 —→ S1
    E[] ⊢ p : S2     E;e1;…;ei[] ⊢ S2 <: 
S1
    E[] ⊢ S  with x := p —→
Struct e1;…;ei; ModA(X==p);ei+2{p/X} ;…;en{p/X End
WEVAL-WITH-MOD-REC
    E[] ⊢ S —→ Struct e1;…;ei; Mod(X1:S1);ei+2;… ;en  End
    E;e1;…;ei[] ⊢ S1  with p := p1 —→ S2
    E[] ⊢ S  with X1.p := p1 —→
Struct e1;…;ei; Mod(X:S2);ei+2{p1/X1.p} ;…;en{p1/X1.p End
WEVAL-WITH-DEF
    E[] ⊢ S —→ Struct e1;…;ei;Assum()(c:T1);ei+2;… ;en  End
    E;e1;…;ei[] ⊢ Def()(c:=t:T) <: Assum()(c:T1)
    E[] ⊢ S  with c := t:T —→
Struct e1;…;ei;Def()(c:=t:T);ei+2;… ;en  End
WEVAL-WITH-DEF-REC
    E[] ⊢ S —→ Struct e1;…;ei; Mod(X1:S1);ei+2;… ;en  End
    E;e1;…;ei[] ⊢ S1  with p := p1 —→ S2
    E[] ⊢ S  with X1.p := t:T —→
Struct e1;…;ei; Mod(X:S2);ei+2;… ;en  End
WEVAL-PATH-MOD
    E[] ⊢ p —→ Struct e1;…;ei; Mod(X:S [:=S1]);ei+2;… ;en  End
    E;e1;…;ei[] ⊢ S —→ S
E[] ⊢ p.X —→ S
     WF(E)[]       Mod(X:S [:=S1])∈ E
    E[] ⊢ S —→ S
E[] ⊢ X —→ S
WEVAL-PATH-ALIAS
    E[] ⊢ p —→ Struct e1;…;ei; ModA(X==p1);ei+2;… ;en  End
    E;e1;…;ei[] ⊢ p1 —→ S
E[] ⊢ p.X —→ S
       WF(E)[]        ModA(X==p1)∈ E
      E[] ⊢ p1 —→ S
E[] ⊢ X —→ S
WEVAL-PATH-TYPE
    E[] ⊢ p —→ Struct e1;…;ei; ModType(Y:=S);ei+2;… ;en  End
    E;e1;…;ei[] ⊢ S —→ S
E[] ⊢ p.Y —→ S
WEVAL-PATH-TYPE
     WF(E)[]        ModType(Y:=S)∈ E
    E[] ⊢ S —→ S
E[] ⊢ Y —→ S

Rules for typing module:

MT-EVAL
E[] ⊢ p —→ S
E[] ⊢ p : 
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:

The notation Indp()[ΓP](

ΓC:=ΓI  )

denotes an inductive definition that is definitionally equal to the inductive definition in the module denoted by the path p. All rules which have IndP](ΓC := ΓI) as premises are also valid for Indp()[ΓP](

ΓC:=ΓI  )

. We give the formation rule for Indp()[ΓP](

ΓC:=ΓI  )

below as well as the equality rules on inductive types and constructors.
The module subtyping rules:

MSUB-STR
      E;e1;…;en[] ⊢ eσ(i) <: ei for  i=1..m 
      σ : {1… m} → {1… n}  injective
E[] ⊢  Struct e1;…;en  End <:  Struct e1;…;em  End
MSUB-FUN
E[] ⊢ 
S1
 <: 
S1
          E; Mod(X:S1′)[] ⊢ 
S2
 <: 
S2
E[] ⊢  Functor(X:S1S2 <:  Functor(X:S1′) S2

Structure element subtyping rules:

ASSUM-ASSUM
E[] ⊢ T1βδιζη T2
E[] ⊢ Assum()(c:T1) <: Assum()(c:T2)
DEF-ASSUM
E[] ⊢ T1βδιζη T2
E[] ⊢ Def()(c:=t:T1) <: Assum()(c:T2)
ASSUM-DEF
E[] ⊢ T1βδιζη T2        E[] ⊢ c =βδιζη t2
E[] ⊢ Assum()(c:T1) <: Def()(c:=t2:T2)
DEF-DEF
E[] ⊢ T1βδιζη T2        E[] ⊢ t1 =βδιζη t2
E[] ⊢ Def()(c:=t1:T1) <: Def()(c:=t2:T2)
IND-IND
E[] ⊢ ΓP =βδιζη ΓP′        EP] ⊢ ΓC =βδιζη ΓC′        EPC] ⊢ ΓI =βδιζη ΓI
E[] ⊢ IndP](ΓC := ΓI) <: IndP′](ΓC′ := ΓI′)
INDP-IND
E[] ⊢ ΓP =βδιζη ΓP′        EP] ⊢ ΓC =βδιζη ΓC′        EPC] ⊢ ΓI =βδιζη ΓI
E[] ⊢ Indp()[ΓP](
ΓC:=ΓI  )
 <: IndP′](ΓC′ := ΓI′)
INDP-INDP
E[] ⊢ ΓP =βδιζη ΓP′      EP] ⊢ ΓC =βδιζη ΓC′      EPC] ⊢ ΓI =βδιζη ΓI′      E[] ⊢ p =βδιζη p
E[] ⊢ Indp()[ΓP](
ΓC:=ΓI  )
 <: Indp()[ΓP′](
ΓC′:=ΓI′  )
MOD-MOD
E[] ⊢ S1 <: S2
E[] ⊢  Mod(X:S1) <:  Mod(X:S2)
ALIAS-MOD
E[] ⊢ p : S1        E[] ⊢ S1 <: S2
E[] ⊢  ModA(X==p) <:  Mod(X:S2)
MOD-ALIAS
E[] ⊢ p : S2         E[] ⊢ S1 <: S2        E[] ⊢ X =βδιζη p
E[] ⊢  Mod(X:S1) <:  ModA(X==p)
ALIAS-ALIAS
E[] ⊢ p1 =βδιζη p2
E[] ⊢  ModA(X==p1) <:  ModA(X==p2)
MODTYPE-MODTYPE
E[] ⊢ S1 <: S2        E[] ⊢ S2 <: S1
E[] ⊢  ModType(Y:=S1) <:  ModType(Y:=S2)

New environment formation rules

WF-MOD
 WF(E)[]        E[] ⊢  WF(S)
 WF(E; Mod(X:S))[]
WF-MOD
  E[] ⊢ S2 <: S1
   WF(E)[]     E[] ⊢  WF(S1)     E[] ⊢  WF(S2)
 WF(E; Mod(X:S1 [:=S2]))[]
WF-ALIAS
 WF(E)[]           E[] ⊢ p : S
 WF(E, ModA(X==p))[]
WF-MODTYPE
 WF(E)[]           E[] ⊢  WF(S)
 WF(E, ModType(Y:=S))[]
WF-IND
       WF(E;IndP](ΓC := ΓI))[]
      E[] ⊢ p: Struct e1;…;en;IndP′](ΓC′ := ΓI′);…  End : 
E[] ⊢ IndP′](ΓC′ := ΓI′) <: IndP](ΓC := ΓI)
 WF(E;Indp()[ΓP](
ΓC:=ΓI  )
)[]

Component access rules

ACC-TYPE
E[Γ] ⊢ p :  Struct e1;…;ei;Assum()(c:T);…  End
E[Γ] ⊢ p.c : T

E[Γ] ⊢ p :  Struct e1;…;ei;Def()(c:=t:T);…  End
E[Γ] ⊢ p.c : T
ACC-DELTA
Notice that the following rule extends the delta rule defined in section 4.3
E[Γ] ⊢ p :  Struct e1;…;ei;Def()(c:=t:U);…  End
E[Γ] ⊢ p.cδ 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-IND
E[Γ] ⊢ p :  Struct e1;…;ei;IndP](ΓC := ΓI);…  End
E[Γ] ⊢ p.Ij : (p1:P1)…(pr:Pr)Aj
E[Γ] ⊢ p :  Struct e1;…;ei;IndP](ΓC := ΓI);…  End
E[Γ] ⊢ p.cm : (p1:P1)…(pr:Pr)CmIj(Ij p1pr)j=1… k
ACC-INDP
E[] ⊢ p :  Struct e1;…;ei;Indp()[ΓP](
ΓC:=ΓI  )
;…  End
E[] ⊢ p.Iiδ p′.Ii
E[] ⊢ p :  Struct e1;…;ei;Indp()[ΓP](
ΓC:=ΓI  )
;…  End
E[] ⊢ p.ciδ p′.ci

1
Opaque definitions are processed as assumptions.