Witness-cp
Clause processor for quantifier-based reasoning.
- Signature
(witness-cp clause hint state) → (mv err new-clause)
- Arguments
- clause — Guard (pseudo-term-listp clause).
- Returns
- new-clause — Type (pseudo-term-list-listp new-clause), given (pseudo-term-listp clause).
Introduction
Witness-cp is an extensible clause-processor that can apply
user-supplied rules to carry out witnessing transformations on
quantifier-like terms in ACL2 proof goals.
Witness-cp is a general purpose tool that you can configure to work with any
kinds of quantifiers. As a familiar example, consider set reasoning. If we
encounter some proof goal with a hypothesis of the form:
(subsetp-equal x y)
then we may want to use this hypothesis to draw specific conclusions, such
as:
(implies (member-equal k x)
(member-equal k y))
for various k. Similarly if we have a hypothesis of the form:
(not (subsetp-equal y z))
then we may wish to conclude facts such as:
(and (member-equal j y)
(not (member-equal j z)))
for various j. Many theorems in set theory can be proven by choosing
suitable j and k and then carrying out membership reasoning. The
witness-cp clause processor can be configured to automatically try such
j and k in reasonably smart ways.
More broadly, witness-cp is a general purpose tool that can configured
to reason about arbitrary quantified formulas. It knows nothing a
priori about set theory or any other domain, but it can be told about what
predicates are to be taken as universal/existential quantifiers and how they
should be instantiated.
Usage
There are two steps to using witness-cp. First, we must configure it
to understand the desired domain, e.g., for set theory, we would need to
explain that subsetp-equal is the universal quantification of
member-equal. Once the domain is configured, we can instruct ACL2 to
apply the witness-cp clause processor to particular goals that we want to
solve; this is typically done with an explicit witness hint or via default-hints.
At a high level, when witness-cp transforms a proof goal, it carries
out the following steps, each of which need to be configured to understand your
domain:
- Witnessing. Introduce witnesses for negative occurrences of
universally quantified predicates and positive occurrences of existentially
quantified ones. Then, optionally, for better readability, generalize the
newly introduced witness terms into fresh variables. These steps can be
controlled with defwitness.
- Gathering. Find the set of examples with which to instantiate
positive universally quantified and negative existentially quantified
predicates. The predicates to target are controlled by definstantiate.
- Instantiation. Instantiate these predicates with these examples.
The examples are set up using defexample.
Note that witness introduction and instantiation may both be lossy, i.e.,
they may result in a formula that isn't a theorem even if the original formula
is one!
Extended Example: Set Theory
We now run through a typical example of setting up witness-cp to
understand some functions from set theory.
Configuring Witnessing
To set up witnessing for (not (subsetp-equal a b)) hypotheses, we can
issue the following defwitness event. We assume here that
(subsetp-equal-witness a b) is a suitable ``badguy'' function that finds a
member of a that is not in b, if one exists.
(defwitness subsetp-witnessing
:predicate (not (subsetp-equal a b))
:expr (and (member-equal (subsetp-equal-witness a b) a)
(not (member-equal (subsetp-equal-witness a b) b)))
:generalize (((subsetp-equal-witness a b) . ssew))
:hints ('(:in-theory '(subsetp-equal-witness-correct))))
This instructs witness-cp, during the witnessing phase, to search for
hypotheses of the form (not (subsetp-equal a b)). For any such matches,
witness-cp will add the new hypothesis:
(and (member-equal (subsetp-equal-witness a b) a)
(not (member-equal (subsetp-equal-witness a b) b)))
and will then generalize away the term (subsetp-equal-witness a b) to a
fresh variable with a name like SSEW0, SSEW1, etc. After this
generalization we are left with two new hyps:
(member-equal ssew0 a)
(not (member-equal ssew0 b))
The net result of all of this is that we have replaced an existential
assumption with a fresh variable witnessing it. We wrap (hide ...) around
the original hypothesis to leave a trace of what we've done. (Otherwise, it
would likely be rewritten away, since the two new hyps imply it.)
Why is it sound to add these new hypotheses to our main formula? To justify
this step, the defwitness event requires us to prove the following
theorem, using the provided hints:
(implies (not (subsetp-equal a b))
(and (member-equal (subsetp-equal-witness a b) a)
(not (member-equal (subsetp-equal-witness a b) b))))
Configuring Gathering
To set up instantiation of a (subsetp-equal a b) hypotheses, we can
issue the following definstantiate event.
(definstantiate subsetp-equal-instancing
:predicate (subsetp-equal a b)
:vars (k)
:expr (implies (member-equal k a)
(member-equal k b))
:hints ('(:in-theory '(subsetp-member))))
This will mean that, for each (subsetp-equal a b) hypothesis we find,
we'll add hypotheses of the form:
(implies (member-equal k a)
(member-equal k b))
for each of (possibly) several k. The terms we use to instantiate
k are determined by defexample; see below.
To show that it sound to add these hypotheses, the definstantiate
event requires us to prove:
(implies (subsetp-equal a b)
(implies (member-equal k a)
(member-equal k b)))
This is a very easy proof: it is just the quantifier-based definition of
subsetp-equal.
Configuring Instantiation
The terms used to instantiate k above are determined by defexample rules, like the following:
(defexample subsetp-member-template
:pattern (member-equal k a)
:templates (k)
:instance-rulename subsetp-equal-instancing)
This rule means that, after the gathering phase, we'll look through the
clause for expressions (member-equal k a) and, whenever we find one,
include k in the list of examples to use for instantiating using the
subsetp-equal-instance rule.
Defexample doesn't require any proof obligation; it's just a heuristic
that adds to the set of terms used to instantiate universal quantifiers.
Applying the Clause Processor
To use the scheme we've introduced for reasoning about subsetp-equal,
we can introduce a witness ruleset:
(def-witness-ruleset subsetp-witnessing-rules
'(subsetp-witnessing
subsetp-equal-instancing
subsetp-member-template))
Then when we want to use this reasoning strategy, we can give a hint. You
should not call witness-cp directly, but rather using the witness
macro as a computed hint. For example:
:hints ((witness :ruleset subsetp-witnessing-rules))
This implicitly waits until the formula is stable-under-simplificationp and then invokes the witness-cp clause
processor, allowing it to use the witnessing/instancing/example rules
listed.
You may find it useful to define a macro so that you don't have to remember
this syntax, for instance:
(defmacro subset-reasoning ()
'(witness :ruleset subsetp-witnessing-rules))
(defthm foo
...
:hints (("goal" ...)
(subset-reasoning)))
Further Resources
Additional documentation is available for defwitness, definstantiate, and defexample. Also see defquantexpr, which is
a shortcut for the common pattern (as above) of doing both a defwitness and
definstantiate for a certain term, and defquant, which defines a
quantified function (using defun-sk) and sets up
defwitness/definstantiate rules for it.
Subtopics
- Definstantiate
- Add a witness-cp rule showing how to instantiate a universal
quantifier hypothesis (or an existential quantifier conclusion).
- Defexample
- Tell witness-cp how to instantiate the free variables of definstantiate rules.
- Defwitness
- Add a witness-cp rule providing a witness for an existential
quantifier hypothesis (or universal quantifier conclusion).
- Defquantexpr
- Shortcut to perform both a defwitness and definstantiate.
- Def-witness-ruleset
- Name a set of witness-cp rules.
- Witness
- Computed hint for calling the witness-cp clause processor.
- Defquant
- Define a quantified function and corresponding witness-cp
rules.
