Hints on proving theorems in Twelf
Andrew W. Appel
February 2000
1. The mechanics of running Twelf.
The Twelf system is an implementation by Frank Pfenning (and his students)
of the Edinburgh Logical Framework (LF), which is a formalism for expressing
logics, theorems, and proofs. For the Proof-Carrying Code and
Proof-Carrying Authentication projects at Princeton, the logic that
we use (and which we encode in LF) is a variant of Church's Higher-Order
Logic. LF/Twelf is our metalogic; higher-order logic is our object logic.
We use a CVS repository called "logic" to hold our object logic and
our various theories (a "theory" is a set of definitions and theorems
relating to a particular subject area). The core object logic is
kept in the "logic/coreTCB" subdirectory of the repository, commonly used
lemmas are kept in "logic/core", and so on. This tutorial is
self-contained and independent of the repository, so any reference
to the repository is just for reference and not useful to the workings
of the tutorial.
Other information about Twelf can be found at the Twelf home page,
http://www.cs.cmu.edu/~twelf/
The Twelf User's Guide is at
http://www.cs.cmu.edu/~twelf/guide/twelf_toc.html
The Twelf system, and this tutorial, is best run inside Emacs.
To use Twelf, include the following line in your .emacs profile (or
see your system administrator to learn where Twelf 1.3 is located on
your system):
(setq twelf-root "/cmnusr/local/sml/twelf-1-3/")
(load (concat twelf-root "emacs/twelf-init.el"))
Then start or restart Emacs (so that it sees this command when it
starts), and visit this file, "proving.elf". If Emacs seems to freeze
with "fontifying proving.elf" just type control-G to stop the
fontification and let you read the unfontified file.
A Twelf theory (set of definitions and theorems) is described in a
configuration file, for example "sources.cfg". This lists the individual
Twelf program files (i.e., "proving.elf") and also names other configuration
files to be included in this configuration.
Visit the file "coreTCB/sources.cfg" for an example, then come back here.
If you are using Gnu Emacs 20.anything, you should see a menu bar at the
top of the Emacs buffer, and one of the items on that menu should
be Twelf. If you use the mouse to click on Twelf>Check Configuration,
or use the shortcut key control-c control-c, Twelf will load all the
Twelf-code files of the current configuration. If you have no current
configuration, it will prompt you.
Press control-c control-c now, and hit "Enter" for each of the two
questions. You should see a series of #### marks in the bottom line
of the Emacs buffer; this is a progress bar for Twelf loading all the
declarations and definitions specified in the configuration file.
Control-c control-c loads the whole configuration; control-c control-s
reloads just the current file (but neglects to reload any other
files that depend on it -- be careful!). Control-c control-d reloads
just one definition, and is very useful.
Move the cursor into the following definition, and press
control-c control-d:
imp_true : pf B -> pf (A imp B) =
[Q2 : pf B] imp_i [Q : pf A] Q2.
You should see the words "Server OK" in the bottom line of the Emacs
window (the message line). What this means is that Twelf has
processed the definition and has no complaints. Now load the
following definition (i.e., move the cursor into the following
definition, and press control-c control-d):
imp_true : pf B -> pf (A imp B) =
[Q2 : pf B] imp_i [Q : pf A] Q.
You should see "Server ABORT" in the message line, and a
*twelf-server* buffer should pop up with a message like,
imp_true : pf B -> pf (A imp B) =
[Q2 : pf B] imp_i [Q : pf A] Q.%.
stdIn:1.12-1.31 Error:
Type ascription error
Synthesized: {Q2:pf `B} pf (`A imp `A)
Ascribed: pf `B -> pf (`A imp `B)
Free variable clash
stdIn: 1 error found
%% ABORT %%
Press control-c ` (that is, backquote). Emacs will move you exactly
to the point of the error -- or more precisely, to the point reported
by Twelf: line 1, column 12 of the standard input (i.e., of
the individual definition).
2. Proving a theorem.
Let us examine the theorem
imp_true: pf B -> pf (A imp B) = ...
This says that the proof constructor imp_true can take a proof
of "B" and yield a proof of "A implies B", for any A and B.
For example,
b1 = (true imp true).
a1 = (eq (const 5) (const 5)).
pb1: pf b1 = imp_i [P: pf true] P.
pab: pf (a1 imp b1) = imp_true pb1.
For each of these four lines, move the cursor to the line and
load the declaration (i.e., control-c control-d).
The Twelf value b1 is the formula "true implies true".
The value a1 is the formula "5=5".
The value pb1 is a proof of b1.
Then we can construct a proof of "5=5 implies (true implies true)"
by applying the imp_true theorem to pb1; that's what the fourth
line does.
Now, how do we prove the imp_true theorem? Let's derive it.
First, we write
imp_true: pf B -> pf (A imp B) =
% body of proof
.
A percent sign with a space after it in Twelf introduces a comment (lasts
until end of line); the dot . terminates a definition. So all we need
to do now is fill in a Twelf expression to replace "% body of proof".
This must have the right type, namely, "pf B -> pf (A imp B)", which
we pronounce as "function from proof of B to proof of A imp B".
Since the body is a function, it must take an argument of type "pf B".
Formal parameters of functions in Twelf are written in square brackets,
i.e.
imp_true: pf B -> pf (A imp B) =
[p1: pf B]
% rest of proof
.
Now, "rest of proof" must have type "pf (A imp B)". Since we don't have
a term of that type, we will cheat, using our magical proof-constructor
"hole", defined in core/debug.elf. For any formula C, hole(C) is a proof
of C. In Twelf we write this fact as,
hole: {C} pf C.
So now, "rest of proof" is just "hole(A imp B)", thus:
imp_true: pf B -> pf (A imp B) =
[p1: pf B]
(hole (A imp B))
.
Except for the hole, this is (almost) a valid proof.
Load this definition (control-c control-d) and see what happens.
You get the message, "Server ABORT", and in the *twelf-server* window,
stdIn:2.3-3.19 Error:
No strict occurrence of variable p1, use %abbrev
%% ABORT %%
A definition in Twelf must use all of its arguments. Here, we have
not used the argument p1, so Twelf complains. By the time we finish the
proof, we will have used all the arguments, but for now this doesn't
qualify as a legal definition. It does qualify as a legal "abbreviation"
(sort of like a macro in Twelf), if we put the keyword %abbrev before it:
%abbrev
imp_true: pf B -> pf (A imp B) =
[p1: pf B]
(hole (A imp B))
.
Load this definition; you should get "Server OK".
We don't want our proofs to have holes in them, so we must replace
"hole (A imp B)" with something better. To prove an implication
"A imp B" we can use implication-introduction. This is an inference
rule of our object logic; you can find its definition in coreTCB/logic.elf,
and it looks like this:
imp_i : (pf A -> pf B) -> pf (A imp B).
This says, "given a function F from proof of A to proof of B,
imp_i(F) is a proof of A imp B". Our function F will look something
like: [p2: pf A] ...
where the ... is a proof of B. Since square brackets introduce
function-parameters, this value is clearly a function from (pf A) to (pf B).
Since we don't yet know what proof of B to use, we can use "hole B":
%abbrev
imp_true: pf B -> pf (A imp B) =
[p1: pf B]
(imp_i ([p2: pf A] (hole B)))
.
Load this definition and you should get "Server OK".
We still have a hole! But now we can replace "hole B" by a proof of
B, which we happen to have: that is, p1.
%abbrev
imp_true: pf B -> pf (A imp B) =
[p1: pf B]
(imp_i ([p2: pf A] p1))
.
(Load and check this definition.) Since we have now used the argument
p1, this qualifies as a strict definition, so we can remove the %abbrev:
imp_true: pf B -> pf (A imp B) =
[p1: pf B]
(imp_i ([p2: pf A] p1))
.
Function application in Twelf, as in lambda calculus, binds more tightly
than function abstraction. Therefore we can remove parentheses
in this definition without any syntactic ambiguity:
imp_true: pf B -> pf (A imp B) =
[p1: pf B] imp_i [p2: pf A] p1.
There's our theorem. Load this declaration, just to be sure.
3. Organization of the object logic.
The specification of our object logic is divided into three files:
coreTCB/logic.elf
6 type constructors (tp, tm, pf, form, arrow, pair)
7 formula constructors (lam, @, imp, forall, mkpair, fst, snd),
8 proof constructors (imp_i, imp_e, forall_i, forall_e, ...)
coreTCB/arith.elf
axioms of rational and integer arithmetic (0, 1, plus, times, ...)
coreTCB/classic.elf
the law of the excluded middle (not_not_e)
Many logical constructors that are intuitively "primitive" are
in fact constructed as definitions from primitive constructors.
These live in coreTCB/coredefs.elf:
eq, and, or, exists, false, true, not
Also in coredefs.elf are commonly used combinations, such as
quantification over multiple variables.
There are many useful lemmas about the object logic:
core/basiclem.elf
lemmas about primitives defined in coreTCB/logic.elf, coreTCB/coredefs.elf
core/classiclem.elf
lemmas about the basic primitives, but that need the not_not_e rule
core/arithlem.elf
lemmas about rational arithmetic
core/intlem.elf
lemmas about integers
TCB stands for "trusted computing base": the inference rules (proof
constructors) of the logic must be trusted, because there is no way
(within the logic) to check their soundness; but the lemmas need not
be trusted, because they all come with proofs.
In one sense, the definitions in coreTCB/coredefs.elf need not be
trusted, because they are just giving names to existing expressions.
But on the other hand, these names can be used in (trusted) safety
policies, so a misleading name can lead to an unsafe policy.
4. Examples using and, and_i, and_l.
Here's a theorem:
symm_and: pf (A and B) -> pf (B and A) = ...
Let us prove this theorem. We might first proceed by looking up the
definition of "and" in coreTCB/coredefs.elf, but don't! Instead, we
can pretend that "and" is a primitive, and use lemmas about it from
core/basiclem.elf. The basic rules are and-introduction (and_i)
and and-elimination (and_e1, and_e2):
and_i : pf A -> pf B -> pf (A and B) = ...
and_e1 : pf (A and B) -> pf A = ...
and_e2 : pf (A and B) -> pf B = ...
And-introduction says, "given a proof of A and a proof of B we can
construct a proof of (A and B)". And-elimination-1 says, "given
a proof of (A and B) we can construct a proof of A".
Now, to prove symm_and, we first notice that symm_and is a function,
so we can start filling in the formal parameter (a proof
of (A and B)) and the body (a proof of (B and A)):
symm_and: pf (A and B) -> pf (B and A) =
[p1: pf (A and B)]
hole (B and A).
Load this definition. The server ABORTs with the complaint about
"no strict occurrence of variable p1", so we please it with %abbrev:
%abbrev
symm_and: pf (A and B) -> pf (B and A) =
[p1: pf (A and B)]
hole (B and A).
Now, a hole(B and A) can be refined using and_i, as follows:
%abbrev
symm_and: pf (A and B) -> pf (B and A) =
[p1: pf (A and B)]
and_i
(hole B)
(hole A).
(Load this definition.)
We now have two holes. To create a proof of B, we can use and_e2 on the
proof of (A and B):
%abbrev
symm_and: pf (A and B) -> pf (B and A) =
[p1: pf (A and B)]
and_i
(and_e2 p1)
(hole A).
(Load this definition.)
Similarly, we can fill in the proof of A. By this time, we have a strict
use of p1, so we can remove the %abbrev:
symm_and: pf (A and B) -> pf (B and A) =
[p1: pf (A and B)]
and_i
(and_e2 p1)
(and_e1 p1).
When dealing with ands, a useful lemma is "and_l" (so called because it
works like the "and_left" rule of sequent logic):
and_l: pf (A and B) -> (pf A -> pf B -> pf C) -> pf C = ...
Basically, if we have a proof of (A and B) then we can use and_l
to "bind" two new variables, a proof of A and a proof of B:
symm_and: pf (A and B) -> pf (B and A) =
[p1: pf (A and B)]
and_l p1
[p2: pf A]
[p3: pf B]
hole (B and A).
(Load this definition.) Now we can use and_i to finish this proof:
% Preferred proof of symm_and.
symm_and: pf (A and B) -> pf (B and A) =
[p1: pf (A and B)]
and_l p1
[p2: pf A]
[p3: pf B]
and_i p3 p2.
This proof is no more correct than the one that uses and_e1 and
and_e2, but the use of and_l to break apart the conjunction leads
to better labelling of the individual proof components for human
readability.
5. Proof style.
Twelf can do enough type inference so that the type constraints on
bound variables are not usually necessary:
symm_and: pf (A and B) -> pf (B and A) =
[p1] and_l p1 [p2] [p3] and_i p3 p2.
But the type constraints provided important documentation for human
readers of the proof, and should usually be left in.
If we fully parenthesize and indent the proof of symm_and, we get
this monstrosity:
symm_and: pf (A and B) -> pf (B and A) =
([p1: pf (A and B)]
(and_l p1 ([p2: pf A]
([p3: pf B]
(and_i p3 p2))))).
Here are style guidelines:
example_abc: pf (A and B) ->
pf C ->
pf ((B and C) and (A and C)) =
[p1: pf (A and B)] % Small, identical indent
[p2: pf C] % for the premises of the proof.
and_l p1 % After a [binding] no extra indent.
[p3: pf A] % Within a proof, newly bound proofs are
[p4: pf B] % indented 7-9 spaces from proof constructors.
and_i % After a new binding, no new indent.
(and_i p4 % Within a still-open parenthesis,
p2) % indent to "inside the paren" depth.
(and_i p3 p2).
Note that unnecessary parentheses are eliminated. This is not a universal
rule, i.e. the formulas
(A and B or C and D)
( (A and B) or (C and D) )
are equivalent, but in some cases you may prefer the more-parenthesized
version. But in parenthesizing proof-constructors the issue is different.
We would like to read the proof "and_l p1 [p3][p4] ..." as
"bind p3 and p4 to the conjuncts of the and-formula and then continue
the proof", but technically speaking the parentheses would fall as
"and_l p1 ([p3]([p4] ... ))". These parentheses do not aid in the
intuitive understanding of "bind p3 and p4 and then continue".
Visit the file "proving2.elf" to continue.