		Search-engine friendly clone of the ACL2 documentation.

Miscellaneous

Defopener

Create a defthm equating a call with its simplification.

For a related tool, see defopen.

Example:

(include-book "misc/defopener" :dir :system)
(defopener append-open
  (append x y)
  :hyp (and (true-listp x) (true-listp (cdr x)))
  :hints (("Goal" :expand ((append x y)))))

The above example creates the following theorem.

(DEFTHM APPEND-OPEN
  (IMPLIES (AND (TRUE-LISTP X)
                (TRUE-LISTP (CDR X)))
           (EQUAL (APPEND X Y)
                  (IF (NOT X)
                      Y
                      (CONS (CAR X) (APPEND (CDR X) Y))))))

In general, the form

(defopener name
  term
  :hyp hyp
  ...)

attempts to create a theorem of the form

(DEFTHM NAME
  (IMPLIES HYP
           (EQUAL TERM rhs)))

where rhs is generated by ACL2's simplification routines. If :hyp is omitted, then of course the resulting form has the expected shape:

(DEFTHM NAME
  (EQUAL TERM rhs)).

If an equivalence relation symbol is supplied for :equiv, then EQUAL above will be replaced by that symbol.

The output can be rather verbose. Once rhs as above has been produced, ACL2 will print out the theorem to be proved before starting its proof, indicated as follows.

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

>>> STARTING PROOF OF:

(DEFTHM NAME
        ...)

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

To abbreviate the above message, you can specify an evisc-tuple using the :evisc-tuple keyword of defopener, which is nil by default.

The simplification that takes place uses a prover interface that is also used in the distributed book misc/bash, in which the following hint is automatically generated for "Goal", though they can be overridden if explicitly supplied in the defopener form for "Goal":

:do-not (generalize eliminate-destructors fertilize eliminate-irrelevance)

A suitable :do-not-induct hint is also generated, so that induction is avoided during the simplification process. This too can be overridden.

If you only want to see the generated theorem, and not the attempted proof of it, use :debug t. Alternatively, you may want to run without that addition and then submit :pcb! to grab the generated encapsulate form to put into the book that you are developing. Otherwise, the defopener form will call the ACL2 simplifier twice each time you certify your book: once to generate the theorem, and once to prove it.

The :flatten keyword is t by default, and causes the result to be of the form (cond (c1 v1) (c2 v2) ... (ck vk) (t v)). That result is actually produced from a more primitive tree-based result, of the form (if c v1 v2), where v1 and v2 can themselves be calls of if. If you prefer the more primitive form, use :flatten nil.

None of the arguments of this macro is evaluated.

This tool is heuristic in nature, and failures are possible. The error message might provide debugging clues. Let us consider an example that actually occurred that generated an error message of the following form.

ACL2 Error in (DEFOPENER MY-DEFOPENER-RULE ...):  The last literal
of each clause generated is expected to be of the form (equiv lhs rhs)
for the same equiv and lhs. The equiv for the last literal of the first
clause is EQUAL and its lhs is (HIDE (FOO X Y)) but the last literal of
one clause generated is:

(MY-PREDICATE (HIDE (FOO X Y)))

The message suggests that each goal (i.e., clause) after the first should be of the form (implies ... (equal (HIDE (FOO X Y)) ...)) or simply (equal (HIDE (FOO X Y)) ...); but in this case, one goal was actually of the form (IMPLIES ... (MY-PREDICATE (HIDE (FOO X Y)))). After first executing (set-gag-mode nil) and then running defopener again, the proof log helped to discover a rewrite rule of the following form.

(equal (equal (f1 a)
              b)
       (and (my-predicate b)
            ...))

ACL2 was able to match the term (EQUAL (HIDE (FOO X Y)) (F1 A)) with the left-hand side of the above rule, thus rewriting it to a conjunction whose first conjunct was (MY-PREDICATE (HIDE (FOO X Y))). The error disappeared after that rule was disabled.