		Search-engine friendly clone of the ACL2 documentation.

Proof-builder

Verify

Enter the interactive proof-builder

For proof-builder command summaries, see proof-builder.

Examples:
(VERIFY (implies (and (true-listp x) (true-listp y))
                      (equal (append (append x y) z)
                             (append x (append y z)))))
   -- Attempt to prove the given term interactively.

(VERIFY (p x)
        :event-name p-always-holds
        :rule-classes (:rewrite :generalize)
        :instructions ((rewrite p-always-holds-lemma)
                       change-goal))
   -- Attempt to prove (p x), where the intention is to call the
      resulting DEFTHM event by the name p-always-holds, with
      rule-classes as indicated.  The two indicated instructions
      will be run immediately to start the proof.

(VERIFY)
   -- Re-enter the interactive proof-builder in the state at which
      it was most recently left.

General Form:
(VERIFY &OPTIONAL raw-term
        &KEY
        event-name
        rule-classes
        instructions)

Verify is the function used for entering the interactive proof-builder's read-eval-print loop.

Note that you can use verify to create an event, by using the exit command (see ACL2-pc::exit). For example, after evaluating

(verify (equal y y) :instructions (s (exit foo nil t)))

we can see that the expected event was successfully created:

ACL2 !>:pe foo
           1:x(VERIFY (EQUAL Y Y) :INSTRUCTIONS ...)
              
>              (DEFTHM FOO (EQUAL Y Y)
                       :RULE-CLASSES NIL
                       :INSTRUCTIONS (:S))
ACL2 !>

That said, it's probably not a good idea to save events with :instructions. There are at least two general reasons to avoid :instructions: (1) to encourage the development of rewrite rules and other ways to help with later proofs, and (2) to make the proofs less brittle, that is, more likely to survive when there are small changes to earlier events.