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 15 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
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 10.5 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 section 9.3 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.
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 10.2 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 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.