Set-constraint-tracking
Generate markers to indicate origins of constraints
General Form:
(set-constraint-tracking flg)
where flg is Boolean.
When flg is t the constraint subgoals generated by the
:functional-instance hint (see hints and lemma-instance)
have an additional hypothesis of the form (extra-info :constraint ...)
where the second argument to extra-info is a quoted expression that
indicates where the constraint came from. Since extra-info is a disabled
defined function that always returns t, the addition of this hypothesis
does not change the meaning of the formula.
Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so recorded. It
uses the ACL2-defaults-table, and hence its effect is local to
the book or encapsulate form in which it occurs.
We expect this facility to be used only when a proof involving functional
instantiation is failing and inspection of the subgoals or checkpoints leaves
you asking the question ``why is it trying to prove this?'' But turning on
this facility can cause a failing proof to fail even earlier because the
extra-info hypotheses may change the course of the proof. We discuss
some ways of handling this below.
But first we give an example of the output that might be seen when the
constraint-tracking flag is set. This example is intended
to give you an idea of how to read the extra-info — which of course
is only visible if gag-mode is nil or a checkpoint is printed.
Because the ``quoted expression that indicates where the constraint came
from'' is entirely informal, we do not give you a formal syntax and semantics
for it. Just study the examples. Furthermore, as this facility matures we
may well change the quoted expressions to be more informative.
Recall the example use of :functional-instance in functional-instantiation-example. (To understand what follows you really
ought to read the example just cited.) In particular, after we use encapsulate to constrain some functions and then prove a few useful lemmas,
we prove the following by functional instantiation. We include the entire
un-gagged proof output below from a session in which the
constraint-tracking flag has been set.
ACL2 !>(DEFTHM TIMES-LIST-REV
(IMPLIES (NUMBER-LISTP X)
(EQUAL (TIMES-LIST (REV X))
(TIMES-LIST X)))
:HINTS
(("Goal"
:USE
((:FUNCTIONAL-INSTANCE AC-FN-LIST-REV
(AC-FN *)
(AC-FN-ROOT (LAMBDA NIL 1))
(AC-FN-DOMAIN ACL2-NUMBERP)
(AC-FN-LIST TIMES-LIST)
(AC-FN-DOMAIN-LIST NUMBER-LISTP))))))
[Note: A hint was supplied for the goal above. Thanks!]
We augment the goal with the hypothesis provided by the :USE hint.
The hypothesis can be derived from AC-FN-LIST-REV via functional in-
stantiation, provided we can establish the seven constraints generated;
the constraints can be simplified using the :executable-counterparts
of IF and TAU-SYSTEM and the simple :rewrite rules ASSOCIATIVITY-OF-*
and UNICITY-OF-1. We are left with the following four subgoals.
Subgoal 4
(IMPLIES (EXTRA-INFO :CONSTRAINT '((DEFUN AC-FN-LIST)
((AC-FN BINARY-*)
(AC-FN-LIST TIMES-LIST)
(AC-FN-ROOT (LAMBDA NIL '1)))))
(EQUAL (TIMES-LIST X)
(IF (ATOM X)
1
(* (CAR X) (TIMES-LIST (CDR X)))))).
But simplification reduces this to T, using the :definitions ATOM and
TIMES-LIST and primitive type reasoning.
Subgoal 3
(IMPLIES (AND (EXTRA-INFO :CONSTRAINT '((THEOREM AC-FN-ID)
((AC-FN BINARY-*)
(AC-FN-DOMAIN ACL2-NUMBERP)
(AC-FN-ROOT (LAMBDA NIL '1)))))
(ACL2-NUMBERP X))
(EQUAL (FIX X) X)).
But simplification reduces this to T, using the :definition FIX and
primitive type reasoning.
Subgoal 2
(IMPLIES (EXTRA-INFO :CONSTRAINT '((THEOREM AC-FN-COMM)
((AC-FN BINARY-*)
(AC-FN-DOMAIN ACL2-NUMBERP)
(AC-FN-ROOT (LAMBDA NIL '1)))))
(EQUAL (* X Y) (* Y X))).
But simplification reduces this to T, using primitive type reasoning
and the :rewrite rule COMMUTATIVITY-OF-*.
Subgoal 1
(IMPLIES (EXTRA-INFO :CONSTRAINT '((DEFUN AC-FN-DOMAIN-LIST)
((AC-FN-DOMAIN ACL2-NUMBERP)
(AC-FN-DOMAIN-LIST NUMBER-LISTP))))
(EQUAL (NUMBER-LISTP X)
(COND ((ATOM X) T)
((ACL2-NUMBERP (CAR X))
(NUMBER-LISTP (CDR X)))
(T NIL)))).
But simplification reduces this to T, using the :definitions ATOM and
NUMBER-LISTP and primitive type reasoning.
Q.E.D.
Note the EXTRA-INFO hypotheses. For example, in Subgoal 1, just
above, the hypothesis is
(EXTRA-INFO :CONSTRAINT '((DEFUN AC-FN-DOMAIN-LIST)
((AC-FN-DOMAIN ACL2-NUMBERP)
(AC-FN-DOMAIN-LIST NUMBER-LISTP))))
which indicates that Subgoal 1 is the functional instantiation
of the defining equation for constrained function AC-FN-DOMAIN-LIST
under the functional substitution shown. Subgoal 1 establishes that
NUMBER-LISTP satisfies the constraint on AC-FN-DOMAIN-LIST.
You can view the definition of AC-FN-DOMAIN-LIST with the
:pe command.
By inspecting the extra-info in Subgoal 2, above,
(EXTRA-INFO :CONSTRAINT '((THEOREM AC-FN-COMM)
((AC-FN BINARY-*)
(AC-FN-DOMAIN ACL2-NUMBERP)
(AC-FN-ROOT (LAMBDA NIL '1)))))
you should be able to recognize that it establishes that multiplication is
commutative, which is required by the constraining THEOREM named
AC-FN-COMM, since we are replacing AC-FN by multiplication. You can
view the named theorem with the :pe command.
You might occasionally see something like this
(EXTRA-INFO :CONSTRAINT '((:THEOREM <term>) <fn-substitution>))
Note that this occurrence of the word ``THEOREM'' is as a keyword and what
follows it is a term rather than a name. This stems from the use of the
:THEOREM lemma-instance in the :functional-instance hint. In
this case, the constraint is the term shown.
The presence of these additional hypotheses may break some proofs that
formerly worked! For example, if constraint-tracking is
off, the events in the ACL2 Community Book
/books/centaur/misc/tailrec.lisp can be processed successfully. But if
the flag is on the proofs fails because the book is employing a very
restrictive proof strategy designed to deal exactly with proving certain
mechanically generated formulas and the extra-info hypothesis makes the
subgoals unrecognizable to that strategy.
One way of dealing with this is to issue ``bye'' hints, e.g., :by
nil, to subgoals that are failing before the one you want to see.
Alternatively, you might use the :otf-flg option to allow failing
subgoals to be pushed so the prover can carry on to later subgoals.
A third way to deal with this is to prove the rewrite rule
(defthm drop-extra-info-constraints
(implies (equal x :constraint)
(equal (extra-info x y) t))
:hints (("Goal" :in-theory (enable extra-info))))
which will cause the extra-info hypotheses to rewrite to t by the
first simplification. (Aside: The corresponding unconditional rewrite
rule, (equal (extra-info :constraint y) t), is undesirable because it
causes the extra-info hypotheses to be simplified to t before the
goals are displayed to the user.) So for example, if a
:functional-instance hint produced several immediate goals, one of which
is Subgoal 3, and the constraint tracking flag is set, then Subgoal
3 will have an extra-info hypothesis indicating the origin of that
subgoal. If the rewrite rule above is available, the extra-info will
have disappeared in the descendents of Subgoal 3. So if you find
yourself asking ``Where did this goal come from?'' you might refer back to
the parent, Subgoal 3, produced by the functional instance
hint. (Remember, descendent subgoals, e.g., Subgoal 3.17'', have clause-identifiers that indicate their parentage, Subgoal 3.)
That said, some proof strategies employed in the regression (including the
one in the tailrec.lisp book cited above) are so automatic and thus so
tightly restricted that you may not find a way to get over the obstacles
created by the extra-info hypotheses! However, of the thousands of books
in the regression, as of Version 8.6, only three books fail to recertify when
the constraint tracking flag is turned on, and one of those three succeeds if
the rewrite rule above is included. So we await further experience with this
utility before investing more time in it.
