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 STELF provide a direct way to create such holes. Users of earlier versions may take advantage of a curious feature.

STELF CVS: %trustme

The %trustme declaration instructs STELF 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 STELF is in unsafe mode, it will accept %trustme before the %total directive of a metatheorem with an incomplete proof. STELF will consider such metatheorems total for the purpose of the totality checks of subsequent metatheorems. The following is an example of %trustme in action.

%sort nat %.
%term nat/z nat %.
%term nat/s %pi nat %-> nat %.
%sort nat-less {_ nat} {_ nat} %.
%term nat-less/z nat-less nat/z (nat/s N) %.
%term nat-less/s %pi (nat-less (nat/s N1) (nat/s N2)) %<- (nat-less N1 N2) %.
%sort nat-less-immsucc {N nat} {_ nat-less N (nat/s N)} %.
%mode nat-less-immsucc %in %out %.
%term _ nat-less-immsucc nat/z nat-less/z %.
%worlds () (nat-less-immsucc _ _) %.
%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 STELF server.

set unsafe false

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

STELF 1.5R1 and earlier

In older versions of STELF, 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 STELF tries to check the line %total I (foo I _). and fails, it will actually allow foo to be used to check bar’s totality.

%sort thing %.
%term a thing %.
%term b thing %.
%sort foo {_ thing} {_ thing} %.
%mode foo %in %out %.
%worlds () (foo _ _) %.
%total I (foo I _) %.
%sort bar {_ thing} {_ thing} %.
%term _ %pi (bar I O) %<- (foo I O) %.
%mode bar %in %out %.
%worlds () (bar _ _) %.
%total I (bar I _) %.

To reiterate, in order to use this “feature” you get STELF 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.