The Twelf Meta-Theorem Prover

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 the Church-Rosser theorem for the untyped lambda-calculus, cut-elimination for full first-order intutionistic logic, and the equivalence of the Hilbert calculus and the natural deduction calculus. These and other examples can be found here.

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 (the name might change) 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 the Church-Rosser theorem.

Theorem Declaration

There are two 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.

Note that a well-typed %theorem declaration always succeeds, while the %prove declaration only succeeds 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      % Quantification over 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, make as lemma available
       | %establish pdecl. % prove declaration, don't make as lemma available
       | %assert callpats  % assert theorems (Twelf.Options.unsafe required)

The prover only accepts quantifier alternations of the form forallG ctx 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 behind the quantifier for the regular contexts.

The syntax and meaning of order and callpats are explained in Section 7 Termination of the Twelf User's guide, since they are also critical notions in the simpler termination checker.

Sample Theorems

As a first example, we use the theorem prover to establish a simple theorem: If we have to different but structurally identical formulations of the lambda-calculus (exp, exp'), and a relation that shows how we can copy from one to the other, than this relation is total. In words, this theorem reads as: If E is an expression then there exists an expression E', s.t. E' is a structurally identical copy to E.

exp : type.

app : exp -> exp -> exp.
lam : (exp -> exp) -> exp.

exp' : type.

app' : exp' -> exp' -> exp'.
lam' : (exp' -> exp') -> exp'.

cp : exp -> exp' -> type.
cp_app : cp (app D1 D2) (app' E1 E2) 
         <- cp D1 E1
         <- cp D2 E2.
cp_lam : cp (lam ([x:exp] D x)) (lam' ([y:exp'] E y))
         <- ({x:exp} {y:exp'} cp x y -> cp (D x) (E y)). 


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

It is easy to see, that the E and the E' cannot be assumed to be closed, because otherwise the induction hypothesis cannot be applied. In this situation, the induction hypothesis must be applied to an object under some additional assumptions, which are x:exp, y:exp', u:cp x y, and which we call a context block. Clearly, one context block is not enough; in general E can occur in any context regularly built out of these blocks. The forallG allows an inductive definition of a context scheme, abstractly describing the form of real contexts. Each context block consists of a some part which declares additional variables which are instantiated with some well-typed object in a real instance of a context, and a pi part which describes the parameters.

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

Different from the previous version, this meta-theorem prover does currently not construct any proof terms, but we are planning on adding them in near future.

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 nevers 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 paramater Twelf.Prover.maxSplit bounds the number of times a variable may be split.

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.