Skip to content
STELF
Documentation out of dateLearn more

%assert

The %assert directive instructs the theorem prover to accept a previously stated theorem as true without trying to prove that theorem. This directive is thus analogous to a %trustme%total directive. Because it instructs STELF to treat something as true without a proof, STELF must be in unsafe mode to use this directive.

Example

Section titled “Example”

The example from the theorem prover article can be modified to use %assert instead of %prove for the two lemmas that are needed to establish the commutativity of addition.

%sort nat %.
%term s %pi nat %-> nat %.
%term z nat %.
%sort plus {_ nat} {_ nat} {_ nat} %.
%term plus/z plus z N N %.
%term plus/s %pi (plus (s N1) N2 (s N3)) %<- (plus N1 N2 N3) %.

This website checks STELF in safe mode, so %assert directives cause STELF to display an error.

%theorem plus-z : forall {N nat} exists {D plus N z N} true %.
%assert (plus-z N D) %.
%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 %.
%assert (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

Section titled “See also”