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 14 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 5.6 Sample Program).
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 section 8 Termination, since they are also critical notions in the
simpler termination checker.
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 3.6 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
section 5.6 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 tps : 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 (tps 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 9.5 Proof Realizations).
The third example illustrates the use of regular contexts.
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 regular context, abstractly
describing the form of actual 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 _ _ _).
after the Twelf.unsafe
mode has been activated.
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:
%prove
declaration, thus guaranteeing termination (in principle).
Twelf.Prover.maxRecurse
bounds the number of recursion steps in
each case of the proof.
Twelf.Prover.maxSplit
bounds
the number of times a variable may be split.
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.
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 9.2 Sample Theorems).
After the declarations,
%theorem tps : 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 (tps 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 5.2 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.
Go to the first, previous, next, last section, table of contents.