%assert
From The Twelf Project
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 Twelf to treat something as true without a proof, Twelf must be in unsafe mode to use this directive.
[edit] 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 (this example cannot be run on the wiki, which uses Twelf in safe mode).
nat : type. s : nat -> nat. z : nat. plus : nat -> nat -> nat -> type. plus/z : plus z N N. plus/s : plus (s N1) N2 (s N3) <- plus N1 N2 N3. %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).
