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.