# Theorem prover

The **Twelf theorem prover** is a way of specifying and automatically verifying metatheorems that have the form of ∀∃-statements. It uses the Twelf declarations `%theorem`, `%prove`, `%establish`, and `%assert`. The last of these is an unsafe operation similar to `%trustme`.

The current theorem prover is buggy, sometimes does not terminate, and does not output a total logic program that can be used to witness the ∀∃-statement as described in Proof realizations in the User's Guide. Because of this, it cannot interact with the technique of verifying metatheorems by writing totality assertions, and its use is not recommended.

## Contents

## Example - commutativity of addition

### Object language

We start with the standard presentation of the natural numbers with addition.

nat : type. s : nat -> nat. z : nat. plus : nat -> nat -> nat -> type. p-z : plus z N N. p-s : plus (s N1) N2 (s N3) <- plus N1 N2 N3.

### Establishing ∀∃-metatheorems with totality assertions

A simple metatheorem about this object language is the ∀∃-statement that for all natural numbers , there exists a derivation of . This translates into LF as a ∀∃-statement that for all objects `N` with type `nat`, there exists an object `D` of type `plus N z N`.

The "usual" way of proving this kind of metatheorem in Twelf is to define a type family which represents a relation, translate the cases of the inductive proof into LF objects in that type family, and use a `%mode` directive and `%worlds` directive to specify a totality assertion that corresponds to the ∀∃-statement. The totality assertion for type family `plus-z-thm` below establishes the ∀∃-statement that is stated above.

plus-z-thm : {N: nat} plus N z N -> type. - : plus-z-thm z p-z. - : plus-z-thm (s N) (p-s D) <- plus-z-thm N D. %mode plus-z-thm +N -D. %worlds () (plus-z-thm _ _). %total T (plus-z-thm T _).See Twelf's output

### Establishing ∀∃-metatheorems with the theorem prover

The equivalent of the type family definition for `plus-z-thm` and the `%mode` declaration from the above code can be stated with a `%theorem`.

%theorem plus-z : forall {N: nat} exists {D: plus N z N} true.

(Side note: some versions of Twelf allow the `%theorem` declaration above to be used in lieu of the type family definition and `%mode` declaration; John Boyland utilizes this in his tutorial and code examples, but it is not a supported feature and may break in future versions of Twelf!)

Given the `%theorem` declaration, we can ask Twelf to try to establish the metatheorem it states by using a `%prove` declaration.

%prove 5 N (plus-z N D).

Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)%prove 5 N (plus-z N D). %mode +{N:nat} -{D:plus N z N} (plus-z N D). %QED %skolem plus-z#1 : {N:nat} plus N z N.

%% OK %%

We can also include the equivalent of implicit parameters in our metatheorem statements, but unlike the standard method where we define a new type family, all our implicit parameters must be listed after the `forall*` keyword. We can then prove two more metatheorems (the second is the commutativity of addition).

%theorem plus-s : forall* {N1: nat}{N2: nat}{N3: nat} forall {D1: plus N1 N2 N3} exists {D2: plus N1 (s N2) (s N3)} true. %prove 5 D1 (plus-s D1 D2). %theorem plus-comm : forall* {N1: nat}{N2: nat}{N3: nat} forall {D1: plus N1 N2 N3} exists {D2: plus N2 N1 N3} true. %prove 5 D1 (plus-comm D1 D2).

## See also

- Theorem Prover in the User's Guide