Create a defthm equating a call with its simplification.
For a related tool, see defopen.
(include-book "misc/defopener" :dir :system)
(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.
(IMPLIES (AND (TRUE-LISTP X)
(TRUE-LISTP (CDR X)))
(EQUAL (APPEND X Y)
(IF (NOT X)
(CONS (CAR X) (APPEND (CDR X) Y))))))
In general, the form
attempts to create a theorem of the form
(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:
(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:
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)
(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.