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 200 theorems about these relations all with automatically-checked hand-written proofs (using Twelf 1.5R3).

  nat.elf

• Positive rational numbers (represented using continued fractions). The signature requires “nat.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 package includes well over 200 fully-proved theorems.

  rat.elf

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

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

  pair.elf (the functor), natpair.elf (pairs of natural numbers).