11. Theorem Prover

Disclaimer: The theorem proving component of Twelf is in an even more experimental stage and currently under active development.

Nonetheless, it can prove a number of interesting examples automatically which illustrate our approach the meta-theorem proving which is described in Schuermann and Pfenning 1998, CADE. These examples include type preservation for Mini-ML, one direction of compiler correctness for different abstract machines, soundness and completeness for logic programming interpreters, and the deduction theorem for Hilbert's formulation of propositional logic. These and other examples can be found in the example directories of the Twelf distribution (see section Examples).

A theorem in Twelf is, properly speaking, a meta-theorem: it expresses a property of objects constructed over a fixed LF signature. Theorems are stated in the meta-logic M2 whose quantifiers range over LF objects. In the simplest case, we may just be asserting the existence of an LF object of a given type. This only requires direct search for a proof term, using methods inspired by logic programming. More generally, we may claim and prove forall/exists statements which allow us to express meta-theorems which require structural induction, such as type preservation under evaluation in a simple functional language (see section Sample Program).

11.1 Theorem Declaration

The theorem proving component of Twelf is in an experimental stage and currently under active development. This documentation describes the present intermediate state.

There are three forms of declarations related to the proving of theorems and meta-theorems. The first, %theorem, states a theorem as a meta-formula (mform) in the meta-logic M2 defined below. The second, %prove, gives a resource bound, a theorem, and an induction ordering and asks Twelf to search for a proof. After a %prove declaration succeeds, the theorem will be made available as a lemma to subsequent proofs. In order to avoid that, Twelf offers the form %establish which is like %prove, but the established theorem will never be used in subsequent proofs.

Note that a well-typed %theorem declaration always succeeds, while the %prove and %establish declarations only succeed if Twelf can find a proof.

dec ::= {id:term}         % x:A
      | {id}              % x

decs ::= dec
       | dec decs

ctx ::= some decs pi decs
      | some decs pi decs | ctx

mform ::= forallG ctx mform  % regular contexts
        | forall* decs mform % implicit universal
        | forall decs mform  % universal
        | exists decs mform  % existential
        | true               % truth

thdecl ::= id : mform        % theorem name a, spec

pdecl ::= nat order callpats % bound, induction order, theorems

decl ::= …
       | %theorem thdecl.  % theorem declaration
       | %prove pdecl.     % prove declaration
       | %establish pdecl.  % prove declaration, do not use as lemma later
       | %assert callpats.  % assert theorem (requires Twelf.unsafe)

The prover only accepts quantifier alternations of the form forall* decs forall decs exists decs true. Note that the implicit quantifiers (which will be suppressed when printing the proof terms) must all be collected in front, but after the specification of the regular contexts.

The syntax and meaning of order and callpats are explained in Termination, since they are also critical notions in the simpler termination checker.

11.2 Sample Theorems

As a first example, we use the theorem prover to establish a simple theorem in first-order logic (namely that A implies A for any proposition A), using the signature for natural deduction (see section Sample Signature).

%theorem
trivI : exists {D:{A:o} nd (A imp A)}
        true.

%prove 2 {} (trivI D).

The empty termination ordering {} instructs Twelf not to use induction to prove the theorem. The declarations above succeed, and with the default setting of 3 for Twelf.chatter we see

%theorem trivI : ({A:o} nd (A imp A)) -> type.
%prove 2 {} (trivI D).
%QED
%skolem trivI#2 : {A:o} nd (A imp A).

The line starting with %theorem shows the way the theorem will be realized as a logic program predicate. In earlier versions this was such a logic program was actually constructed; at present this feature has been disabled while the implementation has been improved to allow regular contexts.

The second example is the type preservation theorem for evaluation in the lambda-calculus. This is a continuation of the example in Section Sample Program in the file `examples/guide/lam.elf'. Type preservation states that if and expression E has type T and E evaluates to V, the V also has type T. This is expressed as the following %theorem declaration.

%theorem
tpsa : forall* {E:exp} {V:exp} {T:tp}
       forall {D:eval E V} {P:of E T}
       exists {Q:of V T}
       true.

The proof proceeds by structural induction on D, the evaluation from E to V. Therefore we can search for the proof with the following declaration (where the size bound of 5 on proof term size is somewhat arbitrary).

%prove 5 D (tpsa D P Q).

Twelf finds and displays the proof easily. The resulting program is installed in the global signature and can then be used to apply type preservation in subsequent proofs (see section Proof Realizations).

The third example illustrates the use of regular contexts. We use the theorem prover to establish a simple theorem, namely that for every input to the copy predicate cp in Totality (see also file `examples/guide/lam.elf') there exists a corresponding output. This essentially is just a reformulation of the totality checking question for cp, except that we use the more heavyweight tool of the theorem prover.

%theorem cpt : forallG (pi {x:exp} {y:cp x x})
               forall {D:exp}
	       exists {F:exp} {C:cp E F}
               true.
%prove 5 E (cpt E _ _).

The termination ordering E instructs Twelf to do induction over E to prove the theorem. The %prove command executes the proof search. In addition, if a proof has been found, the lemma is made accessible to the proof search evoked by subsequent theorems and lemmas, and which might slow it down accordingly. If a lemma is not used in subsequent proofs, the user can use %establish instead of %prove and it will not be made available.

For certain theorems, the theorem prover will not be able to find a proof, even that it should. This behavior could be caused by an incompleteness in the implementation (which still exist, but which should be removed in the next release of Twelf), or a enormously huge search space, which disallows the underlying LF theorem to construct a proof term. In these situations, one can still try to prove subsequent theorem and lemmas by asserting the correctness of the lemma in question. This is done by the %assert command. For the theorem above, one could

%assert (cpt _ _ _).

after the Twelf.unsafe mode has been activated.

11.3 Proof Steps

We expect the proof search component of Twelf to undergo major changes in the near future, so we only briefly review the current state.

Proving proceeds using three main kinds of steps:

Filling

Using iterative deepening, Twelf searches directly for objects to fill the existential quantifiers, given all the constants in the signature and the universally quantified variables in the theorem. The number of constructors in the answer substitution for each existential quantifier is bounded by the size which is given as part of the %prove declaration, thus guaranteeing termination (in principle).

Recursion

Based on the termination ordering, Twelf appeals to the induction hypothesis on smaller arguments. If there are several ways to use the induction hypothesis, Twelf non-deterministically picks one which has not yet been used. Since there may be infinitely many different ways to apply the induction hypothesis, the parameter Twelf.Prover.maxRecurse bounds the number of recursion steps in each case of the proof.

Splitting

Based on the types of the universally quantified variables, Twelf distinguishes all possible cases by considering all constructors in the signatures. It never splits a variable which appears as an index in an input argument, and if there are several possibilities it picks the one with fewest resulting cases. Splitting can go on indefinitely, so the parameter Twelf.Prover.maxSplit bounds the number of times a variable may be split.

11.4 Search Strategies

The basic proof steps of filling, recursion, and splitting are sequentialized in a simple strategy which never backtracks. First we attempt to fill all existential variables simultaneously. If that fails we recurse by trying to find new ways to appeal to the induction hypothesis. If this is not possible, we pick a variable to distinguish cases and then prove each subgoal in turn. If none of the steps are possible we fail.

This behavior can be changed with the parameter Twelf.Prover.strategy which defaults to Twelf.Prover.FRS (which means Filling-Recursion-Splitting). When set to Twelf.Prover.RFS Twelf will first try recursion, then filling, followed by splitting. This is often faster, but fails in some cases where the default strategy succeeds.

11.5 Proof Realizations

Proofs of meta-theorems can be realized as logic programs. This is presently disabled. We still describe the possibility below in anticipation of future versions. On the other hand, theorems that have been proved will be skolemized and used in proof of subsequent theorems. However, they will not be used for search.

A logic program is a relational representation of the constructive proof and can be executed to generate witness terms for the existentials from given instances of the universal quantifiers. As an example, we consider once more type preservation (see section Sample Theorems).

After the declarations,

%theorem
tpsa : forall* {E:exp} {V:exp} {T:tp}
       forall {D:eval E V} {P:of E T}
       exists {Q:of V T}
       true.

%prove 5 D (tpsa D P Q).

Twelf answers

/tps/tp_lam/ev_lam/: 
   tps ev_lam (tp_lam ([x:exp] [P2:of x T1] P1 x P2))
      (tp_lam ([x:exp] [P3:of x T1] P1 x P3)).

/tps/tp_app/ev_app/tp_lam/: 
   tps (ev_app D1 D2 D3) (tp_app P1 P2) P6
      <- tps D3 P2 (tp_lam ([x:exp] [P4:of x T2] P3 x P4))
      <- tps D2 P1 P5
      <- tps D1 (P3 E5 P5) P6.

which is the proof of type preservation expressed as a logic program with two clauses: one for evaluation of a lambda-abstraction, and one for application. Using the %solve declaration (see section Solve Declaration) we can, for example, evaluate and type-check the identity applied to itself and then use type preservation to obtain a typing derivation for the resulting value.

e0 = (app (lam [x] x) (lam [y] y)).
%solve p0 : of e0 T.
%solve d0 : eval e0 V.
%solve tps0 : tps d0 p0 Q.

Recall that %solve c : V executes the query V and defines the constant c to abbreviate the resulting proof term.

This document was generated by Florian Rabe on April, 3 2009 using texi2html 1.76.