Presentation of the formalization
General notice
Some generated links do not point to the right place because of
ambiguities: several files define the same name. A typical example is
term which is defined in both
Flanguage_v and
Llanguage_v. The
documentation does not assume these links to be correct, but still
uses the syntax to enhance these names.
The links of the form
<name>_v are unique and thus well-defined.
They point to an empty inductive at the beginning of the file named
<name>.v.
Quick pointers
A list of the files used in the formalization:
Excerpt from the manuscript
This formalization has been developed with Coq version 8.4pl2. It can
be found online at
http://phd.ia0.fr/. There is a
Makefile, so it suffices to run
make to compile the Coq files or
make html to also build the html version.
The formalization merges ideas from strong normalization proofs of
System F and step-indexed techniques. The strong normalization proof
techniques is initially inspired from
A formalization of strong
normalization for simply-typed lambda-calculus and system F but
adapted for soundness proofs and step-indices. The step-indexed
techniques are inspired from
An indexed model of recursive types for
foundational proof-carrying code but modified for strong reduction.
The main differences between the version of System Fcc presented in
this chapter and its formalization in Coq are the use of de Bruijn
indices and the parametrization of the type system. Using de Bruijn
indices makes it a lot easier and cleaner to deal with binders. The
parametrization is necessary to state the results and for the
induction to go well.
We will now give a small glimpse of the Coq code for the reader to
find its way through the files, definitions, and lemma. Files prefixed
with the capital letter
F refer to the indexed calculus: this letter
stands for fuel. Files prefixed with the capital letter
L refer to
the lambda calculus. Files without a prefix letter are more general,
like
typesystem_v which factorizes the type systems for both the
indexed calculus and the lambda calculus. We describe the files in
dependency order.
We first have a few independent files. The file
ext_v defines the
extensionality axioms we use. Propositional and functional
extensionality are the only axioms used. The other extensionality
rules are lemmas. The file
set_v defines a type for potentially
infinite sets as predicates in
Prop. The file
minmax_v defines the
tactic
minmax to deal with indices. The file
list_v defines useful
lemmas about lists, which we use for environments and mappings.
Finally, the file
mxx_v defines the parametrization of the type
system using a value of type
Mode, which is the pair of a boolean
and a version. The boolean tells whether we allow recursive types or
not. The soundness proof does not constrain this boolean while the
normalization proof requires the boolean to be false. The version is
defined by the inductive
Version and contains three possible values:
vP,
vF, and
vS. This manuscript corresponds to the
vP version,
which is the natural presentation. The
vF version contains
additional premises that are redundant by extraction but necessary for
the soundness induction. Finally, the
vS version removes some
premises from the
vF version which are required for extraction but
not for soundness. The proof of soundness is thus done in the
vS
version. We define two helpers to tell whether a premise is required
for extraction with
mE or for soundness with
mS. Finally, the
mR
helper tells which rules are about recursive types.
We can now define the indexed calculus in file
Flanguage_v. We
define the inductive
term for terms. All constructors of this
inductive are prefixed with a
nat representing the index of the
node. We then define a few functions to traverse terms, from which we
define lifting of index predicates to term, and the
lift and
subst
functions for de Bruijn lifting and substitution. We then define the
reduction relation in the inductive
red. We finally define errors in
Err and valid terms
V. What follows is a list of lemmas about
lifting, substitutions, lowering, and other functions over indices.
We prove the strong normalization of the pure indexed calculus in file
Fnormalization_v. This file is quite simple to follow: we define a
measure, prove that it strictly decreases with reduction in
red_measure, and finally prove that reduction is well founded in
wf_der.
We can now define a semantics for this indexed calculus in file
Fsemantics_v. We define the notion of interior in
Dec, the notion
of contraction in
Red, and the notion of expansion in
Exp. Using
expansion, we can define the set of sound terms
OK. We define
pretypes in
C and types in
CE. We define the closure of a set in
Cl, in order to define the arrow operator
EArr, product operator
EProd, and incoherent abstraction operator
EPi. We show that these
operators preserve types in
CE_EArr,
CE_EProd, and
CE_EPi. We
also define erasable types such as the coherent polymorphic type
EFor, the top type
ETop, the bottom type
EBot, or recursive
types
EMu. We then define the notions we need to show that recursive
types are equal to their unfolding. And we finally define the semantic
judgment
EJudg and the semantic typing rules of the STLC, such as
ELam_sem. We also define a subtyping rule
ECoer_sem and a
distributivity rule
Edistrib which will be used together to prove
rule
JCoer.
Once that the indexed calculus is defined, we may define the lambda
calculus and the functions to go back and forth between them in file
Llanguage_v. The structure of this file is similar to
Flanguage_v
with the difference that it now contains a
drop and
kfill function
to translate terms from one language to the other. It also contains
the key lemma
drop_red_exists for the bisimulation between the
reduction relation of both languages.
Independently from the indexed calculus and the lambda calculus, we
can define the type part of System Fcc: everything but the term
judgment. This is done in
typesystem_v and is actually shared by
both
Ftypesystem_v and
Ltypesystem_v, which define the term
judgment for the indexed type system and lambda type system
respectively. The last two files are exactly the same up to indices.
All the syntax is gathered is a single Coq inductive, namely
obj.
This simplifies a lot the treatment of operations on the syntax, such
as lifting or substitution, which are defined only once. In order to
keep track of syntactical classes, we define a judgment
cobj to
classify each object in its grammatical class. In the paper version,
we naturally assume that everything is syntactically well-formed,
while we have to state it explicitly in Coq.
We prove the weakening, substitution, and extraction lemmas in
typesystemextra_v. This file also contains the proof that the
vP
and
vF version are equivalent and that the
vS version is a
consequence. This explains why the properties of the
vS version also
hold for the
vP version.
The proof that each judgment of the indexed type system is sound lies
in
Fsoundness_v. We start by defining a notion of semantic objects
sobj. A semantic object is either a set of indexed terms, the unit
object, or a pair of objects. We then define the signature of the
interpretation of each syntactical class in
sem. Kinds are
interpreted as sets of semantic objects, types as semantic objects,
propositions as indexed propositions, type environments as sets of
semantic environments (lists of semantics objects because we use de
Bruijn indices), coinduction environments as indexed propositions, and
finally term environments as semantic term environments (lists of
semantic types, when the syntactical environment is valid). All these
interpretation are parametrized by an surrounding semantic
environment. We define the interpretation function
semobj as a
binary relation, but we show in
semobj_eq that it behaves as a
function. We then prove semantic lifting and substitution properties.
And we finally prove the soundness of each judgment. The soundness of
jfoo is proved in
jfoo_sound.
We finally lift this soundness proof from the indexed type system to
the lambda type system in
Lsoundness_v. We first define when a term
a is sound for a least
k steps in
OKstep and when it is sound
for all number of steps in
OK by coinduction. We prove that these
two notions coincide. We then show how to transpose soundness from the
indexed calculus to the lambda calculus in
term_ge_OK. We prove that
both type systems coincide and finally prove the soundness of System
Fcc in
soundness.
The Coq files
Lsemantics_v and
Lnormalization_v are similar to the
files
Fsemantics_v,
Fsoundness_v, and
Lsoundness_v but deal with
the strong normalization result instead of the soundness result.