Theorem prover

The STELF theorem prover is a way of specifying and automatically verifying metatheorems that have the form of ∀∃-statements. It uses the STELF 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 Lexical Conventions (guide §10.62). Because of this, it cannot interact with the recommended technique of verifying metatheorems by writing totality assertions, and its use is not recommended.

Example - commutativity of addition

Object language

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

%sort nat %.
%term s %pi nat %-> nat %.
%term z nat %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%term p-z plus z N N %.
%term p-s %pi (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 $N$, there exists a derivation of $\mathsf{plus}(N,0,N)$. 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 STELF 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 _).

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 STELF 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 STELF!)

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

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

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 (guide §10.57)