Major Section: DEFUN-SK
ACL2 supports first-order quantifiers
forall by way of
defun-sk event. However, proof support for quantification is quite
limited. Therefore, you may prefer using recursion in place of
when possible (following common ACL2 practice).
p'' can be defined either with recursion or explicit quantification, but proofs may be simpler when recursion is used. We illustrate this point with two proofs of the same informal claim, one of which uses recursion which the other uses explicit quantification. Notice that with recursion, the proof goes through fully automatically; but this is far from true with explicit quantification (especially notable is the ugly hint).
The informal claim for our examples is: If every member
a of each
of two lists satisfies the predicate
(p a), then this holds of their
append; and, conversely.
See quantifiers-using-recursion for a solution to this example using recursion.
See quantifiers-using-defun-sk for a solution to this example using
defun-sk. Also See quantifiers-using-defun-sk-extended for an
elaboration on that solution.
But perhaps first, see defun-sk for an ACL2 utility to introduce first-order
quantification in a direct way. Examples of the use of
defun-sk are also
available: see defun-sk-example and see Tutorial4-Defun-Sk-Example for
basic examples, and see quantifier-tutorial for a more complete, careful
beginner's introduction that takes you through typical kinds of
quantifier-based reasoning in ACL2.