AUTHOR
François Pottier, INRIA. 2013.
LICENSE
GNU GPL. See the file LICENSE.
REQUIREMENTS
Coq 8.4. (Tested with Coq 8.4pl2.)
WHAT IS DBLIB?
The dblib library offers facilities for working with de Bruijn indices in
Coq. The basic idea is as follows:
1- The client manually defines the syntax of terms (or types, or whatever
syntax she is interested in) as usual, as an inductive type;
2- The client manually defines a higher-order "traverse" function, which can
be thought of as a generic, capture-avoiding substitution function. Its
job is (i) to apply a user-supplied function f at every variable, and
(ii) to inform f about the number of binders that have been entered. By
defining "traverse", the client effectively defines the binding structure.
3- The client proves that the "traverse" function is well-behaved, i.e., it
satisfies half a dozen reasonable properties. This proof is usually
trivial, because the library provides tailor-made tactics for this
purpose.
4- The library defines weakening ("lift") and substitution ("subst") in
terms of "traverse", and proves a rather large number of properties of
these functions.
5- The functions "lift" and "subst" are opaque, so an application of these
functions cannot be reduced by Coq's builtin tactic "simpl". The library
provides "simpl_lift_goal" and "simpl_subst_goal" for this purpose (plus
a few variants of these tactics that perform simplification within a
hypothesis, or within all hypotheses).
6- The library also provides hint databases, to be used with [eauto], that
can prove many of the typical equalities that arise when proving
weakening or substitution lemmas.
7- The library defines a "closed" term as one that is invariant under
lifting (and substitution), and provides lemmas/tactics for reasoning
about this notion.
Everything is based on type classes: "traverse", "lift", "subst", etc. are
overloaded, so the whole process can be repeated, if desired, for another
inductive type.
The library *does* support multiple *independent* namespaces: for instance, it
is possible to have terms that contain term variables and types that contain
type variables.
The library does *not* support multiple namespaces when there is interaction
between them: for instance, it is *not* possible to have terms that contain
both term variables and type variables, as in a standard presentation of
System F. A possible work-around is to define a single namespace of
"variables" and to use a separate well-kindedness judgement in order to
distinguish between "term" variables and "type" variables. I have used this
approach in a large proof where it has turned out to be extremely beneficial.
LIBRARY FILES
The library consists of the following files:
DblibTactics.v
A small number of hints and tactics that are used in the library.
The end user should not need to worry about them, but can go and
have a look.
DeBruijn.v
The core library. The end user is encouraged to read the first
two parts of this file, which present 1- the operations and
properties that the client is expected to provide; and 2- the
operations and properties that the library provides. These two
parts extend up to the first double dashed line, near line 432.
Environments.v
This auxiliary library defines a notion of environment, which
is typically useful when defining a typing judgement. The use
of this library is optional.
DEMO FILES
The documentation takes the form of a few demo files:
DemoLambda.v
Small-step operational semantics and typing judgement for the
simply-typed lambda-calculus. Proof of type preservation and
of a few other basic lemmas.
DemoValueTerm.v
Short demo of how to use the library in the case where there
are two distinct syntactic categories of things in which we
substitute (e.g., terms) and things that we substitute (e.g.,
values).
DemoExplicitSystemF.v
Proof of type preservation for System F, in a version where
the presence of type abstractions and type applications is
explicit in the syntax of terms. (Still, terms do not refer
to types!)
DemoImplicitSystemF.v
Proof of type preservation for System F, in a version where
type abstraction and type application are implicit, i.e.,
the syntax of terms is untyped. This proof is trickier than
the one above, in that it requires induction over the height
of type derivations. But as far as binding is concerned, no
new problems arise.