Quantifiers
Issues about quantification in ACL2
ACL2 supports first-order quantifiers exists and forall by way of the defun-sk event. However, proof support for
quantification is quite limited. Therefore, you may prefer using recursion in
place of defun-sk when possible (following common ACL2 practice).
For example, the notion ``every member of x has property 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.
Subtopics
- Quantifiers-using-defun-sk
- Quantification example
- Quantifiers-using-defun-sk-extended
- Quantification example with details
- Quantifiers-using-recursion
- Recursion for implementing quantification
