The topics in this page are not maintained in any particular order, nor are
they related to one another. Note that these are not about the ACL2 system in
general but only about issues related to ACL2 that have caused me grief when I
encountered them, and my understanding of such issues. If you are interested
in ACL2, its logic, or the theorem prover, I recommend that you visit the ACL2 Homepage.
Table of Contents:
[This is a collection of notes that I wrote to remind myself of how to reason
about quantifiers when I just started. Most users after they have gotten a
hang of quantifiers probably will not need this and will be able to have their
intuitions to guide them in the process. But since many ACL2 users are not
used to quantification, I am hoping that this set of notes might help them to
think clearly while reasoning about quantifiers in ACL2.]
Many ACL2 papers start with the sentence "ACL2 is a quantifier-free first-order
logic of recursive functions." That statement is true but only as far as it
goes. The syntax of ACL2 is quantifier-free; every formula is assumed to be
universally quantified over all free variables in the formula. But the logic
in fact does afford arbitrary first-order quantification. This is obtained in
ACL2 using the a construct called defun-sk. [See :DOC defun-sk]
Many ACL2 users do not think in terms of quantifiers. The focus is almost
always on defining recursive functions and reasoning about them using
induction. That is entirely justified, in fact, since proving theorems about
recursive functions by induction plays to the strengths of the theorem
prover. Nevertheless there are situations where it is reasonable and often
useful to think in terms of quantifiers. However, reasoning about quantifiers
requires that you get to the mindset of thinking about theorems in terms of
quantification. This note is about how to do this effectively given ACL2's
implementation of quantification. This does not discuss defun-sk in detail, but
merely shows some examples. A detailed explanation of the implementation is in
the ACL2 documentation [See :DOC defun-sk], and a proof of soundness of the
implementation is in the paper "Structured Theory Development for a Mechanized
Logic" by Matt Kaufmann and J Strother Moore.
[Note: Quantifiers can be used for some pretty cool things in ACL2. Perhaps the
most interesting example is the way of using quantifiers to introduce arbitrary
tail-recursive equations. See the paper "Partial Functions in ACL2" by
Panagiotis Manolios and J Strother Moore to see how quantification is used to
introduce arbitrary tail-recursive equations. This note does not address
applications of quantifiers, but merely how you would reason about them once
you think you want to use them.]
Assume that you have some function P. I have just left P as a unary function
stub below, since I do not care about what P is.
(defstub P (*) => *)
Now suppose you want to somehow specify the concept that "there exists some x
such that (P x) holds". ACL2 allows you to write that directly using
quantifiers.
(defun-sk exists-P () (exists x (P x)))
If you submit the above form in ACL2 you will see that the theorem prover
specifies two functions exists-p and exists-p-witness, and exports the
following constraints:
1. (defun exists-P () (P (exists-P-witness)))
2. (defthm exists-P-suff (implies (p x) (exists-p)))
Here exists-P-witness is a new function symbol in the current ACL2 theory. What
do the constraints above say? Notice the constraint exists-p-suff. It says that
if you can provide any x such that (P x) holds, then you know that exists-p
holds. Think of the other constraint (definition of exists-p) as going the
other way. That is, it says that if exists-p holds, then there is some x, call
it (exists-p-witness), for which P holds. Notice that nothing else is known
about exists-p-witness than the two constraints above.
[Note: exists-p-witness above is actually defined in ACL2 using a special form
called defchoose. [See :DOC defchoose] This note does not talk about
defchoose. So far as this note is concerned, think of the exists-p-witness as a
new function symbol that has been generated somehow in ACL2, about which only
nothing other than the two facts above is known.]
Similarly, you can talk about the concept that "for all x (P x) holds." This
can be specified in ACL2 by the form:
(defun-sk forall-P () (forall x (P x)))
This produces the following two constraints:
1. (defun forall-P () (P (forall-p-witness)))
2. (defthm forall-p-necc (implies (not (P x)) (not (forall-p))))
To understand these, think of for-all-p-witness as producing some x which does
not satisfy P, if such a thing exists. the constraint forall-p-necc merely says
that if forall-p holds then P is satisfied for every x. (To see this more
clearly, just think of the contrapositive of the formula shown.) The other
constraint (definition of forall-p) merely says that if forall-p does not hold
then there is some x, call it (forall-p-witness), which does not satisfy P. To
see this, just consider the following formula which is immediately derevable
from the definition.
(implies (not (forall-p)) (not (P (forall-witness))))
The description above suggests that to reason about quantifiers, the following
rules of thumb are useful:
RT1: To prove (exists-p), construct some object A such that P holds for A and
then use exists-P-suff.
RT2: If you have exists-P as your hypothesis, use the definition of
exists-p to know that P holds for exists-p-witness. To use this to prove a
theorem, you must be able to derive the theorem based on the hypothesis
that P holds for something, whatever the something is.
RT3: To prove forall-P, prove the theorem (P x) (that is, that P holds for an
arbitrary x), and then simply instantiate the definition of forall-p, that
is, show that P holds for the witness.
RT4: If you have forall-p in the hypothesis of the theorem, see how you can
prove your conclusion if indeed you were given (P x) as a
theorem. Possibly for the conclusion to hold, you needed that P holds for
some specific set of x's. Then use the theorem forall-p-necc by
instantiating it for the specific x's you care about.
Perhaps the above is too terse. In the remainder of the note, we will consider
several examples of how this is done to prove theorems with quantifiers in
ACL2.
Let us consider two trivial theorems. Assume that for some unary function r,
you have proved (r x) as a theorem. Let us see how you can prove that (1) there
exists some x such that (r x) holds, and (2) for all x (r x) holds.
We first model these things using defun-sk. Below, r is simply some function so
that we know that (r x) is a theorem.
(encapsulate
(((r *) => *))
(local (defun r (x) (declare (ignore x)) t))
(defthm r-holds (r x)))
(defun-sk exists-r () (exists x (r x)))
(defun-sk forall-r () (forall x (r x)))
ACL2 does not have too much reasoning support for quantifiers. So in most
cases, one would need :use hints to reason about quantifiers. In order to apply
:use hints, it is preferable to keep the function definitions and theorems
disabled.
(in-theory (disable exists-r exists-r-suff forall-r forall-r-necc))
Let us now prove that there is some x such that (r x) holds. Since we want to
prove exists-r, we must use exists-r-suff by RT1. We do not need to construct
any instance here since r holds for all x by the theorem above.
(defthm exists-r-holds
(exists-r)
:hints (("Goal" :use ((:instance exists-r-suff)))))
Let us now prove the theorem that for all x, (r x) holds. By RT3, we must be
able to prove it by definition of forall-r.
(defthm forall-r-holds
(forall-r)
:hints (("Goal" :use ((:instance (:definition forall-r))))))
[Note: No ACL2 user in the right mind would probably prove the theorems
exists-r-holds and forall-r-holds above. The theorems shown are only for
demonstration purposes.]
For the remainder of this note we will assume that we have two stubbed out
unary functions M and N, and we will look at proving some quantified properties
of these functions.
(defstub M (*) => *)
(defstub N (*) => *)
Let us now define the predicates all-M, all-N, ex-M, and ex-N specifying the
various quantifications.
(defun-sk all-M () (forall x (M x)))
(defun-sk all-N () (forall x (N x)))
(defun-sk some-M () (exists x (M x)))
(defun-sk some-N () (exists x (N x)))
(in-theory (disable all-M all-N all-M-necc all-N-necc))
(in-theory (disable some-M some-N some-M-suff some-N-suff))
Let us prove the classic distributive properties of quantifications, namely the
distributivity of universal quantification over conjunction, and distributivity
of existential quantification over disjunction. We can state these properties
informally in "pseudo ACL2" notation as follows:
1. (exists x: (M x)) or (exists x: (N x)) <=> (exists x: (M x) or (N x))
2. (forall x: (M x)) and (forall: x (N x)) <=> (forall x: (M x) and (N x))
To make these notions formal we of course need to define the formulas at the
RHS of 1 and 2. So we define some-MN and all-MN to capture these concepts.
(defun-sk some-MN () (exists x (or (M x) (N x))))
(defun-sk all-MN () (forall x (and (M x) (N x))))
(in-theory (disable all-MN all-MN-necc some-MN some-MN-suff))
First consider proving property 1. The formal statement of this theorem would
be: (iff (some-MN) (or (some-M) (some-N))))
How do we prove this theorem? Looking at RT1-RT4 above, note that they suggest
how one should reason about quantification when one has an "implication". But
here we have an "equivalence". This suggests another rule of thumb.
RT5: Whenever possible think of proving an equivalence by proving two
implications.
Let us apply RT5 to prove the theorems above. So we will first prove: (implies
(some-MN) (or (some-M) (some-N))))
How can we prove this? This involves assuming a quantified predicate (some-MN),
so we must use RT1 and apply the definition of some-MN. Since the conclusion
involves a disjunction of two quantified predicates, by RT2 we must be able to
construct two objects A and B such that either M holds for A or N holds for B,
so that we can then invoke some-M-suff and some-N-suff to prove the conclusion.
But now notice that if some-MN is true, then there is already an object, in
fact some-MN-witness, such that either M holds for it, or N holds for it. And
we know this is the case from the definition of some-MN! So we will simply
prove the theorem instantiating some-M-suff and some-N-suff with this witness.
The conclusion is that the following event will go thru with ACL2.
(defthm le1
(implies (some-MN)
(or (some-M) (some-N)))
:rule-classes nil
:hints (("Goal"
:use ((:instance (:definition some-MN))
(:instance some-M-suff
(x (some-MN-witness)))
(:instance some-n-suff
(x (some-mn-witness)))))))
This also suggests the following rule of thumb:
RT6: If a conjecture involves some existentially quantified predicate that you
have in the hypothesis and some other existentially quantified predicate
that you are trying to prove, use the witness of the existential
quantification in the hypothesis to construct the witness for the
existential quantification in the conclusion.
Let us now try to prove the converse of le1, that is: (implies (or (some-M)
(some-N)) (some-mn))
Since this is a disjunction of hypothesis, we will just prove each case
individually instead of proving the theorem by a :cases hint. So we prove the
following two lemmas.
(defthm le2
(implies (some-M) (some-MN))
:rule-classes nil
:hints (("Goal"
:use ((:instance (:definition some-M))
(:instance some-MN-suff
(x (some-M-witness)))))))
(defthm le3
(implies (some-N) (some-MN))
:rule-classes nil
:hints (("Goal"
:use ((:instance (:definition some-N))
(:instance some-MN-suff
(x (some-N-witness)))))))
Note that the hints above are simply applications of RT5 as in le1. With these
lemmas, of course the main theorem is trivial.
(defthmd |some disjunction|
(iff (some-MN) (or (some-M) (some-N)))
:hints (("Goal"
:use ((:instance le1)
(:instance le2)
(:instance le3)))))
Let us now prove the distributivity of universal quantification over
conjunction, that is, the formula: (iff (all-MN) (and (all-M) (all-N)))
Applying RT5, we will again decompose this into two implications. So consider
the one-way implication: (implies (and (all-M) (all-N)) (all-MN))
Here we get to assume all-M and all-N. Thus by RT4 we can use all-M-necc and
all-N-necc to think as if we are given the formulas (M x) and (N x) as
theorems. The conclusion here is also a universal quantification, namely we
have to prove all-MN. Then RT3 tells us to proceed as follows. Take any
object y. Try to find an instantiation z of the hypothesis (and (M y) (N y))
is a theorem. Then instantiate y with all-MN-witness. Note that the
hypothesis lets us assume (M x) and (N x) to be theorems. Thus to justify we
need to instantiate x with y, and in this case, therefore, with all-MN-witness.
To make the long story short, the following event goes thru with ACL2:
(defthm lf1
(implies (and (all-M) (all-N))
(all-MN))
:rule-classes nil
:hints (("Goal"
:use ((:instance (:definition all-MN))
(:instance all-M-necc (x (all-MN-witness)))
(:instance all-N-necc (x (all-MN-witness)))))))
This suggests the following rule of thumb which is a dual of RT6:
RT7: If a conjecture involves some universal quantifier in the hypothesis and
the conclusion then instantiate the "necessary condition" (forall-mn-necc)
of the hypothesis with the witness of the conclusion to prove the
conjecture.
Applying RT7 now we can easily prove the other theorems that we need to show
that universal quantification distributes over conjunction. Let us just go
through this motion in ACL2.
(defthm lf2
(implies (all-MN)
(all-M))
:rule-classes nil
:hints (("Goal"
:use ((:instance (:definition all-M))
(:instance all-MN-necc
(x (all-M-witness)))))))
(defthm lf3
(implies (all-MN)
(all-N))
:rule-classes nil
:hints (("Goal"
:use ((:instance (:definition all-N))
(:instance all-MN-necc
(x (all-N-witness)))))))
(defthmd |all conjunction|
(iff (all-MN)
(and (all-M) (all-N)))
:hints (("Goal" :use ((:instance lf1)
(:instance lf2)
(:instance lf3)))))
The rules of thumb for universal and existential quantification should make you
realize the duality of their use. Every reasoning method about universal
quantification can be cast as a way of reasoning about existential
quantification. Whether you reason using universal and existential quantifiers
depends on what is natural in a particular context. But just for the sake of
completeness let us prove the duality of universal and existential quantifiers.
So what we want to prove is the following:
1. (forall x (not (M x))) = (not (exists x (M x)))
We first formalize the notion of (forall x (not (M x))) as a quantification.
(defun-sk none-M () (forall x (not (M x))))
(in-theory (disable none-M none-M-necc))
So we now want to prove: (equal (none-M) (not (some-M)))
We should prove this again as a pair of implications. So let us prove first:
(implies (none-M) (not (some-M)))
This seems to have an existential quantification in the conclusion, but it is
not quite. It is actually the "negation" of an existential quantification. We
are now trying to prove that something does not exist. How do we do that? We
can show that nothing satisfies M by just showing that (some-M-witness) does
not satisfy M. This suggests the following rule of thumb:
RT8: When you encounter the negation of an existential quantification think in
terms of a universal quantification and vice-versa.
Ok, so now applying RT8 and RT3 you should be trying to apply the definition of
some-M. The hypothesis is just a pure (non-negated) universal quantification
so you should apply RT4. A blind application lets us prove the theorem as
below.
(defthm nl1
(implies (none-M) (not (some-M)))
:rule-classes nil
:hints (("Goal"
:use ((:instance (:definition some-M))
(:instance none-M-necc (x (some-M-witness)))))))
How about the converse implication? I have deliberately written it as (implies
(not (none-M)) (some-M)) instead of switching the LHS and RHS of nl1, which
would have been equivalent. Again, RH8 tells us how to reason about it, and we
succeed.
(defthm nl2
(implies (not (none-M)) (some-M))
:rule-classes nil
:hints (("Goal"
:use ((:instance (:definition none-M))
(:instance some-M-suff (x (none-M-witness)))))))
So finally we just go through the motions of proving the equality.
(defthmd |exists = not forall not|
(equal (none-M) (not (some-M)))
:hints (("Goal"
:use ((:instance nl1)
(:instance nl2)))))
Let us now see if we can prove a slightly more advanced theorem which can be
stated informally as: If there is a natural number x which satisfies M, then
there is a least natural number y that satisfies M
[Note: Any time I have had to reason about existential quantification I have
had to do this particular style of reasoning and state that if there is
an object satisfying a predicate then there is also a "minimal" object
satisfying the predicate.]
Let us formalize this concept. We first define the concept of existence of a
natural number satisfying x.
(defun-sk some-nat-M () (exists x (and (natp x) (M x))))
(in-theory (disable some-nat-M some-nat-m-suff))
We now talk about what it means to say that x is the least number satisfying M.
(defun-sk none-below (y)
(forall r (implies (and (natp r) (< r y)) (not (M r))))))
(in-theory (disable none-below none-below-necc))
(defun-sk min-M () (exists y (and (M y) (natp y) (none-below y))))
(in-theory (disable min-m min-m-suff))
The predicate none-below says that no natural number less than y satisfies
M. The predicate min-M says that there is some natural number y satisfying M
such that none-below holds for y.
So the formula we want to prove is: (implies (some-nat-M) (min-M))
Since the formula requires that we prove an existential quantification (that is
non-negated), RT1 tells us that we must construct some object so that we can
prove that the predicate we are quantifying over satisfies it. We should then
be able to instantiate min-m-suff with this object. The predicate we are
quantifying over says that the object must be the least natural number that
satisfies M. Since such an object is uniquely computable if we know that there
exists some natural number satisfying M, let us just write a recursive function
to compute it. This function is least-M below.
(defun least-m-aux (i bound)
(declare (xargs :measure (nfix (- (1+ bound) i))))
(cond ((or (not (natp i))
(not (natp bound))
(> i bound))
0)
((M i) i)
(t (least-m-aux (+ i 1) bound))))
(defun least-m (bound) (least-m-aux 0 bound))
Let us now reason about this function as one does typically. So we prove that
this object is indeed the least natural number that satisfies M, assuming that
bound is a natural number that satisfies M.
(defthm least-aux-produces-an-M
(implies (and (natp i)
(natp bound)
(<= i bound)
(M bound))
(M (least-M-aux i bound))))
(defthm least-<=bound
(implies (<= 0 bound)
(<= (least-M-aux i bound) bound)))
(defthm least-aux-produces-least
(implies (and (natp i)
(natp j)
(natp bound)
(<= i j)
(<= j bound)
(M j))
(<= (least-m-aux i bound) j)))
(defthm least-aux-produces-natp
(natp (least-m-aux i bound)))
(defthmd least-is-minimal-satisfying-m
(implies (and (natp bound)
(natp i)
(< i (least-m bound)))
(not (M i)))
:hints (("Goal"
:in-theory (disable least-aux-produces-least least-<=bound)
:use ((:instance least-<=bound
(i 0))
(:instance least-aux-produces-least
(i 0)
(j i))))))
(defthm least-has-m
(implies (and (natp bound)
(m bound))
(m (least-m bound))))
(defthm least-is-natp
(natp (least-m bound)))
So we have done that, and hopefully this is all that we need about least-M. So
we disable everything.
(in-theory (disable least-m natp))
Now of course we note that the statement of the conjecture we are interested in
has two quantifiers, an inner forall and an outer exists. Since ACL2 is not
very good with quantification we hold its hands to reason with the quantifier
part. So we will first prove something about the forall and then use it to
prove what we need about exists.
RT9: When you face nested quantifiers reason about each nesting separately.
So what do we want to prove about the inner quantifier? Looking carefully at
the quantified predicate we see that it is saying that for all natural numbers
r < y, (M r) does not hold. Well, how would we want to use this fact when we
want to prove our final theorem? We expect that we will instantiate min-M-suff
with the object (least-M bound) where we know (via the outermost existential
quantifier) that M holds for bound, and we will then want to show that
none-below holds for (least-M bound). So let us prove that for any natural
number (call it bound), none-below holds for (least-M bound). For the final
theorem we only need it for natural numbers satisfying M, but note that from
the lemma least-is-minimal-satisfying-m we really do not need that bound
satisfies M.
So we are now proving: (implies (natp bound) (none-below (least-m bound)))
Well since this is a standard case of proving a universally quantified
predicate, we just apply RT3. We have proved that for all naturals i <
(least-m bound), i does not satisfy M (lemma least-is-minimal-satisfying-M), so
we merely need the instantiation of that lemma with none-below-witness of the
thing we are trying to prove, that is, (least-M bound). The theorem below thus
goes through.
(defthm least-is-minimal
(implies (natp bound)
(none-below (least-m bound)))
:hints (("Goal"
:use ((:instance (:definition none-below)
(y (least-m bound)))
(:instance least-is-minimal-satisfying-m
(i (none-below-witness (least-m bound))))))))
Finally we are in the outermost existential quantifier, and are in the process
of applying min-m-suff. What object should we instantiate it with? We must
instantiate it with (least-M bound) where bound is an object which must satisfy
M and is a natural. We have such an object, namely (some-nat-M-witness) which
we know have all these qualities given the hypothesis. So the proof now is
just RT1 and RT2.
(defthm |minimal exists|
(implies (some-nat-M) (min-M))
:hints (("Goal"
:use ((:instance min-M-suff
(y (least-m (some-nat-m-witness))))
(:instance (:definition some-nat-m))))))
If you are comfortable with the reasoning above, then you are comfortable with
quantifiers and probably will not need these notes any more. In my opinion,
the best way of dealing with ACL2 is to ask yourself why you think something is
a theorem, and the rules of thumb above are simply guides to the questions that
you need to ask when you are dealing with quantification.
Here is just a simple exercise for you to test if you understand the reasoning
process.
Exercise:
In the example above we showed that if there exists a natural number x
satisfying M then there is another natural number y such that y satisfies M and
for every natural number z < y, z does not. What would happen if we remove the
restriction of x, y, and z being naturals? Of course, we will not talk about <
any more, but suppose you use the total order on all ACL2 objects (from
"books/misc/total-order"). More concretely, consider the definition of some-M
above. Let us now define two other functions:
(include-book "misc/total-order" :dir :system)
(defun-sk none-below-2 (y)
(forall r (implies (<< r y) (not (M r)))))
(defun-sk min-m2 () (exists y (and (M y) (none-below-2 y))))
The question is whether (implies (some-M) (min-m2)) is a theorem. Can you prove
it? Can you disprove it?
[Note: Thanks to Matt Kaufmann for a detailed explanation. This note is based
on my understanding of an email Matt sent me to dispel my misunderstandings
about functional instantiation.]
Suppose you have defined two 0-ary function stubs bar and baz as follows:
(defstub bar () => *)
(defstub baz () => *)
Suppose now, you define a unary function foo, and prove the theorem that (foo
(bar)) holds.
(defthm foo-for-bar
(foo (bar)))
Then you should be able to instantiate this theorem to prove foo-for-baz below,
using functional instantiation. [See :DOC constraint]
(defthm foo-for-baz
(foo (baz)))
This note addresses some issues on trying to formalize this argument in ACL2.
[Note: There is nothing wrong with the above argument. If indeed, you have
proved the theorem foo-for-bar above then you can functionally instantiate the
theorem easily to prove foo-for-baz. This note only addresses the question of
how you formalize the fact that you can do the instantiation in ACL2, and the
complications arising from what I thought was a rather natural formalization.]
To formalize the notion that this is a legal proof method, we can try to
encapsulate a function foo with the constraint foo-for-bar. More precisely,
assume we execute the following set of events in ACL2:
(defstub bar () => *)
(defstub baz () => *)
(encapsulate
(((foo *) => *))
(local (defun foo (n) (declare (ignore n)) t))
(defthm foo-for-bar (foo (bar))))
You might then expect, as I did, that we can apply a functional-instance hint
to prove foo-for-baz. So you might try to write a form in ACL2 as follows:
(defthm foo-for-baz
(foo (baz))
:hints (("Goal"
:use ((:functional-instance foo-for-bar
(bar baz))))))
If you submit this form to ACL2, you will probably see something like the
following (where the indentations are mine).
ACL2 !>>
[Note: A hint was supplied for our processing of the goal above.
Thanks!]
We now augment the goal above by adding the hypothesis indicated by the
:USE hint. This produces a propositional tautology. The hypothesis can
be derived from FOO-FOR-BAR via functional instantiation, provided we can
establish the constraint generated.
Goal'
(FOO (BAZ)).
Normally we would attempt to prove this formula by induction. However, we
prefer in this instance to focus on the original input conjecture rather
than this simplified special case.
You might then, wonder, as I did, why this proof attempt failed. Indeed, it
seems, that ACL2 has added (foo (bar)) as a constraint on bar, which was kind
of unintuitive to me, since foo and bar were in separate encapsulates. So the
rest of this note explains why the original functional instantiation of
foo-for-bar was illegal in this case.
THE REAL ANSWER:
Functional instantiation is a derived rule of inference. That means that it can
be used to derive only first-order consequences. Clearly, (foo (baz)) is not a
first-order consequence of (foo (bar)), so it would have been a soundness bug
if ACL2 could have proven foo-for-baz in the session above, regardless of the
hints.
INTUITIVELY:
The idea of functional substitution is that if we have T |- A for some theory T
and formula A, where |- indicates logical consequence, then if you apply a
functional substitution fs everywhere, then we will have T\fs |- A\fs. In this
case, we have {(foo (bar))} |- (foo (bar)), and thus applying the functional
substitution (mapping bar to baz) we will have {(foo (baz))} |- (foo (baz)),
and not {(foo (bar))} |- (foo (baz)).
Note that the fact that foo and bar are in different encapsulates is not
relevant. What is relevant is the set of all constraints that support the
theorem to be proved, which includes the constraint on foo, which mentions bar.
Thus, one needs to functionally substitute this constraint, and that is how
ACL2 gets the proof obligation (foo (baz)).
THE IMPLEMENTATION:
The following is an excerpt from [:DOC constraint] discussing what is going on.
Suppose that a given theorem, thm, is to be functionally instantiated using
a given functional substitution, alist, as described in :DOC
lemma-instance. (For an example, see *Note
FUNCTIONAL-INSTANTIATION-EXAMPLE::.) What is the set of proof obligations
generated? It is the set obtained by applying alist to all terms, tm, such
that (a) tm mentions some function symbol in the domain of alist, and (b)
either (i) tm arises from the "constraint" on a function symbol ancestral
in thm or in some defaxiom or (ii) tm is the body of a defaxiom. Here, a
function symbol is "ancestral" in thm if either it occurs in thm, or it
occurs in the definition of some function symbol that occurs in thm, and so
on.
In the example, consider tm as (foo (bar)). Then condition (a) holds, since
(foo (bar)) mentions function symbol bar. And (b)(i) holds, since tm arises
from the constraint on foo, which occurs in thm.
Here is ACL2 code that does the above, most of it edited out (with "....") to
emphasize what is going on.
(defun translate-lmi/functional-instance
(formula constraints event-names new-entries substn proved-fnl-insts-alist
ctx wrld state)
....
(er-let*
((alist (translate-functional-substitution substn ctx wrld state)))
(mv-let
(new-constraints new-event-names new-new-entries)
(relevant-constraints formula alist proved-fnl-insts-alist wrld)
....
(sublis-fn-lst alist
new-constraints))
Here are comments in the definition of relevant-constraints that match [:DOC
constraint].
; The relevant theorems are the set of all terms, term, such that
; (a) term mentions some function symbol in the domain of alist,
; AND
; (b) either
; (i) term arises from a definition of or constraint on a function symbol
; ancestral either in thm or in some defaxiom,
; OR
; (ii) term is the body of a defaxiom.
Tracing relevant-constraints, you see the following. The first value
returned is the list of constraints to which we should apply the functional
subtitution.
ACL2 !>(defthm foo-for-baz (foo (baz))
:hints (("Goal"
:use ((:functional-instance foo-for-bar
(bar baz))))))
1> (RELEVANT-CONSTRAINTS (FOO (BAR))
((BAR . BAZ))
NIL |current-acl2-world|)
<1 (RELEVANT-CONSTRAINTS ((FOO (BAR)))
NIL ((FOO ((BAR . BAZ)))))
[Note: A hint was supplied for our processing of the goal above.
Thanks!]
.....
This note addresses the steps to install ACL2 on top of GCL 2.6.5 on Fedora
Core 3. This is only relevant to you if you are using GCL 2.6.5 or below. The
issues have been fixed in GCL 2.6.6 and above.
[Note: Thanks to Camm Maguire for providing detailed instructions and help in the process.]
1. Download the gcl-2.6.5 sources, and unzip and untar them to some
directory gcldir.
2. Append the following code to gcldir/h/386-linux.h:
#ifdef IN_SFASL
#include <sys/mman.h>
#define CLEAR_CACHE {\
void *p,*pe; \
p=(void *)((unsigned long)memory->cfd.cfd_start & ~(PAGESIZE-1)); \
pe=(void *)((unsigned long)(memory->cfd.cfd_start+memory->cfd.cfd_size) & ~(PAGESIZE-1)) + PAGESIZE-1; \
if (mprotect(p,pe-p,PROT_READ|PROT_WRITE|PROT_EXEC)) {\
fprintf(stderr,"%p %p\n",p,pe);\
perror("");\
FEerror("Cannot mprotect", 0);\
}\
}
#endif
Note:
The above code is required since FC3 have made brk() pages
non-executable by default. If you do not apply the patch above you will be able
to compile gcl but when you then go onto compiling ACL2 you will probably see
an error like "Memory may be damaged."
3. Now compile gcl with the following commands:
cd gcldir
./configure --disable-statsysbfd --enable-locbfd
make
make install
Notes:
(i) The options to configure are required since binutils have changed on FC3
since the release of gcl. Thus gcl probably would not compile otherwise.
(ii) "make install" is not necessary but otherwise you must give the entire
pathname for the gcl executable while compiling ACL2 (step 4).
4. Now follow the directions for "Building an Executable Image on a Unix or
Linux System" from the ACL2 home page.