Incremental metatheorem development

From The Twelf Project
Jump to: navigation, search

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.