When ACL2 succeeds in proving a theorem, it guarantees that, for any
substitution of ACL2 values (subject to guard constraints) for undefined variables, the value of the formula
defining the theorem is not NIL. Theorems may be useful or not, depending on how
they are defined.
Note on guard constraints: All bets are off if an ACL2 value is
substituted for a function argument and fails to satisfy a guard on that
argument.
Vacuous theorems. A theorem expressed as an implication
"(implies hypothesis conclusion)" is vacuous if there
are no circumstances under which the hypothesis of the
theorem is not NIL. A precaution that sometimes exposes a vacuous
theorems is to state another theorem with the same hypothesis, but with the conclusion
negated, as in the following example:
(defthm vacuous
(implies hypothesis (> x (max x y))))
(defthm vacuous-exposed (implies hypothesis (not (> x (max x y)))))
If ACL2 can also prove the new theorem, then the original one is vacuous. Of
course, ACL2 may fail to prove the new theorem, in which case all bets are off.
The original theorem could still be vacuous. Another approach is to ask ACL2 to
prove the negation of the hypothesis. A successful proof of the negation of the
hypothesis guarantees that the original theorem is vacuous.
(defthm vacuous (not hypothesis))
Figuring out that you have proved a nonsensical theorem takes careful thought and a good understanding of the domain of applicability of all of the formulas involved.
"Not a theorem" message. After a proof attempt, ACL2 sometimes reports "We suspect that this conjecture is not a theorem." Take this message seriously. ACL2 is usually (but not always) right when it issues this warning. In stating theorems, it is easy to leave out assumptions that seem obvious to you, but without which the property you are trying to confirm sometimes fails to hold..