		Search-engine friendly clone of the ACL2 documentation.

Defthmg

Variant of defthm supporting guard verification

After a defthm event introduces a name, verify-guards can be called on that theorem name, just as it can be called on a function symbol. However, the proof obligation for verifying guards is often not a theorem. After presenting the general form for defthmg, we give a running example, which illustrates a problem with implies for guard verification and how defthmg solves that problem.

Example Form:
(defthmg true-listp-member-equal
  (implies (true-listp x)
           (true-listp (member-equal a x))))

General Form:
(defthmg name
  body
;;; defthm arguments:
  :rule-classes  rule-classes
  :instructions  instructions
  :hints         hints
  :otf-flg       otf-flg
;;; new arguments:
  :verify-guards verify-guards
  :guard-hints   guard-hints)

where all but the last two keyword arguments are exactly as for defthm. If :verify-guards is supplied then it must be t or nil, indicating that a call of verify-guards on name will or won't be attempted, respectively. If :verify-guards is omitted, then its value is normally treated as t; but it is treated as nil if the default-verify-guards-eagerness is 0 (rather than either 2 or its usual value of 1, as we will assume for the rest of this documentation topic). Finally, if :guard-hints is supplied and verify-guards is attempted on name, then the specified guard-hints will become the value of :hints for that verify-guards event.

We now consider in some detail the example displayed above. Consider it again, but this time with defthm instead of defthmg.

(defthm true-listp-member-equal
  (implies (true-listp x)
           (true-listp (member-equal a x))))

The proof succeeds, after which we might try to call verify-guards. But verify-guards would guarantee that the indicated form will evaluate without a Lisp guard violation for all values of a and x, and that's not always the case! Suppose for example that x is 17. Since implies is an ordinary function, evaluation will take place for both its arguments, even though (true-listp x) is false. The call (member-equal a 17) will cause a guard violation, regardless of the value of a, since the guard for member-equal requires that its second argument satisfy true-listp.

A way to allow guard verification for such a theorem is to replace implies by the macro, impliez, whose calls expand to calls of IF, for example as follows (see trans1).

ACL2 !>:trans1 (impliez (true-listp x)
                        (true-listp (member-equal a x)))
 (IF (TRUE-LISTP X)
     (TRUE-LISTP (MEMBER-EQUAL A X))
     T)
ACL2 !>

When x is 17, evaluation of the form above (either the impliez version or its expansion to an IF call) will not lead to evaluation of the member-equal call. Guard verification will then be possible.

But simply changing implies to impliez doesn't work.

ACL2 !>(defthm true-listp-member-equal
         (impliez (true-listp x)
                  (true-listp (member-equal a x))))


ACL2 Error in ( DEFTHM TRUE-LISTP-MEMBER-EQUAL ...):  A :REWRITE rule
generated from TRUE-LISTP-MEMBER-EQUAL is illegal because it rewrites
the IF-expression (IF (TRUE-LISTP X) (TRUE-LISTP (MEMBER-EQUAL A X)) 'T).
For general information about rewrite rules in ACL2, see :DOC rewrite.

The error message is basically telling us that we need implies, not impliez (or IF), in order to store the indicated theorem as a rewrite rule, which is the default. We can overcome this problem by supplying an explicit :corollary equal to the original theorem, as follows.

(defthm true-listp-member-equal
  (impliez (true-listp x)
           (true-listp (member-equal a x)))
  :rule-classes
  ((:rewrite :corollary
             (implies (true-listp x)
                      (true-listp (member-equal a x))))))

Now the intended rewrite rule is stored, and also we can verify guards, since the guard proof obligation is based on the body of the defthm event (with impliez), not the corollary.

(verify-guards true-listp-member-equal)

The purpose of defthmg is to automate the process described above. Our example defthmg call generates a progn containing the defthm and verify-guards forms displayed just above (except for the addition of suitable :hints to streamline the process).

(DEFTHM TRUE-LISTP-MEMBER-EQUAL
  (IMPLIEZ (TRUE-LISTP X)
           (TRUE-LISTP (MEMBER-EQUAL A X)))
  :RULE-CLASSES
  ((:REWRITE
    :COROLLARY (IMPLIES (TRUE-LISTP X)
                        (TRUE-LISTP (MEMBER-EQUAL A X)))
    :HINTS (("Goal" :IN-THEORY (THEORY 'MINIMAL-THEORY))))))

(VERIFY-GUARDS TRUE-LISTP-MEMBER-EQUAL)

If :rule-classes are supplied explicitly, these will be handled appropriately: for each rule class, if a :corollary is supplied explicitly then that rule class is not changed, and otherwise a :corollary is specified to be the original theorem (hence with implies, not changed to impliez), and the :in-theory hint displayed just above will be generated in order to make the proof of the corollary very fast.

The following more complex (but rather nonsensical) example illustrates the various arguments of defthmg.

(defthmg true-listp-member-equal
  (implies (true-listp x)
           (true-listp (member-equal a x)))
  :verify-guards t
  :guard-hints (("Goal" :use car-cons))
  :hints (("Goal" :induct (member-equal a x)))
  :rule-classes
  (:rewrite
   (:rewrite ; awful rule with free variable
    :corollary (implies (not (true-listp (member-equal a x)))
                        (not (true-listp x))))
   :type-prescription)
  :otf-flg t)

Here are the two events generated after successfully evaluating the form above. Notice that the rule class with an explicit :corollary is not modified.

(DEFTHM TRUE-LISTP-MEMBER-EQUAL
  (IMPLIEZ (TRUE-LISTP X)
           (TRUE-LISTP (MEMBER-EQUAL A X)))
  :RULE-CLASSES
  ((:REWRITE
    :COROLLARY (IMPLIES (TRUE-LISTP X)
                        (TRUE-LISTP (MEMBER-EQUAL A X)))
    :HINTS (("Goal" :IN-THEORY (THEORY 'MINIMAL-THEORY))))
   (:REWRITE
    :COROLLARY (IMPLIES (NOT (TRUE-LISTP (MEMBER-EQUAL A X)))
                        (NOT (TRUE-LISTP X))))
   (:TYPE-PRESCRIPTION
    :COROLLARY (IMPLIES (TRUE-LISTP X)
                        (TRUE-LISTP (MEMBER-EQUAL A X)))
    :HINTS (("Goal" :IN-THEORY (THEORY 'MINIMAL-THEORY)))))
  :HINTS (("Goal" :INDUCT (MEMBER-EQUAL A X)))
  :OTF-FLG T)

(VERIFY-GUARDS TRUE-LISTP-MEMBER-EQUAL
  :HINTS (("Goal" :USE CAR-CONS)))