While learning to use
I wrote an under-informed and biased
tutorial (PDF) on using Twelf to
prove type theorems. This tutorial is over 3 years old (in late 2010)
and should be updated to be a better introduction.
More importantly, I implemented library “signatures”.
To make up for a lack of a module system, some of these signatures
are produced through use of the C preprocessor.
I also fake a module system, using backquote `
since . is (correctly) not legal in a name.
All of these signatures (in one compressed tar) and sources of generated
ELF code are offered without restriction to anyone who
wishes to use them in any way. (Last update: November 27, 2010.)
- Some simple definitions that should be standard.
std.elf (The name is an overreach!)
- Boolean constants. This includes some standard equality
and inequality theorems (such as the transitivity of equality)
that I try to prove for all data types.
- Natural numbers (composed using z and s).
The signature includes plus, times,
eq, gt (greater than), and a number of other
mainly derived relations
(minus, ge, lt etc).
It also includes a divrem operation for integer
division with remainder.
The package includes over 300 theorems about these
relations all with automatically-checked hand-written proofs
(using Twelf 1.5R3).
- Pairs. This trivial "functor" of pairs. There is an
instantiation for pairs of natural numbers that includes
an isomorphism from pairs to natural numbers, so that pairs
can be (indirectly) used as keys to maps (q.v.).
pair.elf (the functor),
natpair.elf (pairs of natural numbers).
- Positive rational numbers (represented using continued fractions).
The signature requires “nat.elf” and "natpair.elf"
and includes add,
mul, equ, grt and derived relations,
including similar relations as above, but also a div
relation. Division is a total operation over the positive
rationals. The signature includes an isomorphism from positive
rationals to the natural numbers which enables rational numbers
to serve as the domain of a map (q.v.).
The package includes well over 300 fully-proved theorems.
rat0.elf (non-negative rational numbers)
- Partial maps. This signature represents maps from natural
numbers to an unspecified datatype data. It must be
customized before use. It includes over 55 fully-proved
theorems. Additionally, if the "data" datatype supports
leq,join and/or meet operations, there are definitions
of these operations for maps and over 100 extra theorems
map.elf (the signature, hand-written),
map.tgz (all of the map theorems).
- Sets of natural numbers. This signature implements finite sets
of natural numbers. As above, the representation is "adequate":
two sets are equivalent iff they are equal. The signature
is mainly generated by instantiating the "map" "functor"
with "data" being "unit". Among other operations are
member, not-member, leq, union,
intersection, add (single
element) and remove (sets). The signature includes well over 300
fully proved theorems about these operations.
- Multisets of natural numbers. This signature implements
multisets as maps to natural numbers. The union
operation does an `max' operation. It is implemented using
that map "functor."
- Vectors (with length). This is a "functor" over a type
with both "add" an "mul" operations defined. The length is used
to ensure there is no attempt made to compare (eq), add or dot
vectors of different length. The "dot" operation is provided
only if the underlying data type includes a zero.
vector.elf (the functor),
rat0vector.elf (vectors of
non-negative rational numbers).
Using Twelf / firstname.lastname@example.org