# Incremental metatheorem development

Typically, metatheorems must be verified as total before they can be used to prove other metatheorems. However, one often wishes to develop a proof without first proving some intermediate lemmas. For example, suppose a programmer believes that if metatheorem A is true, he will be able to prove B. However, A may be difficult to prove, and the effort to prove it may be wasted if it does not lead to a proof of B. Instead, the programmer wants to prove B first (assuming A) and then, if successful, proceed to prove A. Therefore, he would like to create a proof of B with a "hole" for A, but still be able to check B.

The newest versions of Twelf provide a direct way to create such holes. Users of earlier versions may take advantage of a curious feature.

## Twelf CVS: %trustme

The `%trustme` declaration instructs Twelf to run the immediately following declaration but suppress any errors that occur. It is commonly used on `%total` declarations to introduce lemmas that have not yet been proved, in order to develop a proof without first proving some necessary lemmas.

If Twelf is in unsafe mode, it will accept `%trustme` before the `%total` directive of a metatheorem with an incomplete proof. Twelf will consider such metatheorems total for the purpose of the totality checks of subsequent metatheorems. The following is an example of `%trustme` in action.

nat : type. nat/z : nat. nat/s : nat -> nat. nat-less : nat -> nat -> type. nat-less/z : nat-less nat/z (nat/s N). nat-less/s : nat-less (nat/s N1) (nat/s N2) <- nat-less N1 N2. nat-less-immsucc : {N:nat} nat-less N (nat/s N) -> type. %mode nat-less-immsucc +D1 -D2. - : nat-less-immsucc nat/z nat-less/z. %worlds () (nat-less-immsucc _ _). %trustme %total (D1) (nat-less-immsucc D1 _).

When `%trustme` directives are no longer needed, unsafe mode can be disabled by inputting the following line into the Twelf server.

`set unsafe false`

As of 22 September, 2006, `%trustme` is only available in the Subversion version of Twelf.

The %trustme declaration makes Twelf's deductions unsound, of course, so should only be thought of as a development and debugging tool.

## Twelf 1.5R1 and earlier

In older versions of Twelf, the following technique can be used. In the following code, "foo" is obviously not a total relation—it has no cases at all defined. However, after Twelf tries to check the line `%total I (foo I _).` and fails, it will actually allow `foo` to be used to check `bar`'s totality.

thing : type. a : thing. b : thing. foo : thing -> thing -> type. %mode foo +I -O. %worlds () (foo _ _). %total I (foo I _). bar : thing -> thing -> type. - : bar I O <- foo I O. %mode bar +I -O. %worlds () (bar _ _). %total I (bar I _).

To reiterate, in order to use this "feature" you get Twelf to reject the `%total` declaration for foo. Then, it will believe that foo is total in checking *subsequent* theorems. It won't believe that foo is total if you try to rerun `%total` for foo itself—if you re-check the `%total`, it reruns the totality check, and finds that foo still isn't total.

Read more Twelf tutorials and other Twelf documentation.