Using Twelf

I have been learning how to use Twelf. In the process, I have written a tutorial (PDF) on using Twelf to prove type theorems. The tutorial reflects my personal biases and lack of experience.

I also have been working to implement 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.

• 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.

  bool.elf

• 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).

  nat.elf

• 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.

  rat.elf 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 involving them.

  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 200 fully proved theorems about these operations.

  set.elf

• 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."

  multiset.elf

• 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).