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) .

**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

(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

More broadly, *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.

There are two steps to using

At a high level, when

**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!

We now run through a typical example of setting up

To set up witnessing for

(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

(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

(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

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))))

To set up instantiation of a

(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

(implies (member-equal k a) (member-equal k b))

for each of (possibly) several

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

The terms used to instantiate

(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

To use the scheme we've introduced for reasoning about **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

:hints ((witness :ruleset subsetp-witnessing-rules))

This implicitly waits until the formula is stable-under-simplificationp and then invokes the

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)))

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.

- 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.