This report describes the current LEGO library, which was designed as
a basis upon which users can develop their own work, and also some
example proof developments using this library.
An earlier version of the library was developed
by Savi Maharaj for use by students being introduced
to the LEGO system
. We hope that this version
will provide useful preliminaries for all users.
We have received contributions from: Thorsten Altenkirch; Petr Cizek; Adriana Compagnoni; Healf Goguen; Martin Hofmann; Claire Jones; Savi Maharaj; James McKinna; Randy Pollack; Thomas Schreiber.
The LEGO proof development tool is flexible -- users can make various basic choices in how to use the type system to encode their reasoning. We want the library to support this flexibility. Ideally, it should be possible for someone to use the library with any reasonable encoding of e.g. equality and logic, and to choose where in the type hierarchy the basic datatypes should be. We believe that the current library achieves all of these goals with the exception that we cater for only one encoding of logic.
The LEGO library contains around 250 definitions and 400 theorems, and covers both the common datatypes such as natural numbers, list, booleans, products, sums, unit, empty and some more unusual ones such as integers, sigma types, quotient types, finite sets, vectors. There is also a directory which contains some examples of proof developments using the library.
The library exploits the new module
system of LEGO so that loading a library file will
automatically load the files on which it depends and
two library files which depend on
some common files will have the common files loaded
only once. So users don't need to know anything about the
dependency structure of the library, only where to find
the theorems they want. For faster loading, the library also stores
``compiled'' versions of most files which can be accessed by using
the Make command in LEGO.
The library files are organised into directories by datatype. Some files rely on more than one datatype in which case they are put in whatever directory seems most appropriate. The basic datatypes are given inductively with their elimination and reduction rules. Library standards include deriving also recursor, iterator, induction principle and the double elimination rule for each datatype and also the appropriate characterisation theorems (e.g. disjointness of constructors).
In this document we will describe each file briefly and then give a list of the definitions made and theorems proved in each file.