Major Section: MISCELLANEOUS

General Form: ACL2 !>:enable-forcing ; allowed forced case splitsSee force for a discussion of forced case splits.

Enable-forcing is a macro that enables the executable
counterpart of the function symbol `force`

; see force. When
you want to enable forcing in hints, use a form such as:

:in-theory (enable (:executable-counterpart force))

Major Section: MISCELLANEOUS

ACL2 functions, e.g., `if`

, that show `enter-boot-strap-mode`

as their
defining command are in fact primitives. It is impossible for the
system to display defining axioms about these symbols.

`Enter-boot-strap-mode`

is a Common Lisp function but not an ACL2
function. It magically creates from `nil`

an ACL2 property list world
that lets us start the boot-strapping process. That is, once
`enter-boot-strap-mode`

has created its world, it is possible to
process the `defconst`

s, `defun`

s, and `defaxiom`

s, necessary to bring up
the rest of the system. Before that world is created, the attempt
by ACL2 even to translate a `defun`

form, say, would produce an error
because `defun`

is undefined.

Several ACL2 functions show `enter-boot-strap-mode`

as their defining
command. Among them are `if`

, `cons`

, `car`

, and `cdr`

. These functions
are characterized by axioms rather than definitional equations --
axioms that in most cases are built into our code and hence do not
have any explicit representation among the rules and formulas in the
system.

Major Section: MISCELLANEOUS

Example: ACL2 !>:Q

There is no Common Lisp escape feature in the `lp`

. This is part of
the price of purity. To execute a form in Common Lisp as opposed to
ACL2, exit `lp`

with `:`

`q`

, submit the desired forms to the Common Lisp
read-eval-print loop, and reenter ACL2 with `(lp)`

.

`(hide ...)`

as `<hidden>`

Major Section: MISCELLANEOUS

Example: (assign eviscerate-hide-terms t) (assign eviscerate-hide-terms nil)

`Eviscerate-hide-terms`

is a `state`

global variable whose value is
either `t`

or `nil`

. The variable affects how terms are displayed. If
`t`

, terms of the form `(hide ...)`

are printed as `<hidden>`

. Otherwise,
they are printed normally.

Major Section: MISCELLANEOUS

Examples: (:executable-counterpart length)which may be abbreviated in theories as

(length)

Every `defun`

introduces at least two rules used by the theorem
prover. Suppose `fn`

is the name of a `defun`

'd function. Then
`(:definition fn)`

is the rune (see rune) naming the rule that
allows the simplifier to replace calls of `fn`

by its instantiated
body. `(:executable-counterpart fn)`

is the rune for the rule for how
to evaluate the function on known constants.

When typing theories it is convenient to know that `(fn)`

is a runic
designator that denotes `(:executable-counterpart fn)`

.
See theories.

If `(:executable-counterpart fn)`

is enabled, then when applications
of `fn`

to known constants are seen by the simplifier they are
computed out by executing the Common Lisp code for `fn`

(with the
appropriate handling of guards). Suppose `fact`

is defined as the
factorial function. If the executable counterpart rune of `fact`

,
`(:executable-counterpart fact)`

, is enabled when the simplifier
encounters `(fact 12)`

, then that term will be ``immediately''
expanded to `479001600`

.

Such one-step expansions are sometimes counterproductive because
they prevent the anticipated application of certain lemmas about the
subroutines of the expanded function. Such computed expansions can
be prevented by disabling the executable counterpart rune of the
relevant function. For example, if `(:executable-counterpart fact)`

is disabled, `(fact 12)`

will not be expanded by computation. In this
situation, `(fact 12)`

may be rewritten to `(* 12 (fact 11))`

, using the
rule named `(:definition fact)`

, provided the system's heuristics
permit the introduction of the term `(fact 11)`

. Note that lemmas
about multiplication may then be applicable (while such lemmas would
be inapplicable to `479001600`

). In many proofs it is desirable to
disable the executable counterpart runes of certain functions to
prevent their expansion by computation.
See executable-counterpart-theory.

Finally: What do we do about functions that are ``constrained'' rather than defined, such as the following? (See encapsulate.)

(encapsulate (((foo *) => *)) (local (defun foo (x) x)))Does

`foo`

have an executable counterpart? Yes: since the vast
majority of functions have sensible executable counterparts, it was
decided that (defun bar (x) (if (rationalp x) (+ x 1) (foo x)))If the term

`(bar '3)`

is encountered by the ACL2 rewriter during a
proof, and if the `:executable-counterpart`

of `bar`

is enabled, then it
will be invoked to reduce this term to `'4`

. However, if the term
`(bar 'a)`

is encountered during a proof, then since `'a`

is not a
`rationalp`

and since the `:executable-counterpart`

of `foo`

is only a
``trap,'' then this call of the `:executable-counterpart`

of `bar`

will
result in a ``trap.'' In that case, the rewriter will return the
term `(hide (bar 'a))`

so that it never has to go through this process
again. See hide.
Major Section: MISCELLANEOUS

`Exit-boot-strap-mode`

is the last step in creating the ACL2 world in
which the user lives. It has command number `0`

. Commands before it
are part of the system initialization and extend all the way back to
`:`

`min`

. Commands after it are those of the user.

`Exit-boot-strap-mode`

is a Common Lisp function but not an ACL2
function. It is called when every `defconst`

, `defun`

, etc., in our
source code has been processed under ACL2 and the world is all but
complete. `exit-boot-strap-mode`

has only one job: to signal the
completion of the boot-strapping.

Major Section: MISCELLANEOUS

See forcing-round for a background discussion of the notion of forcing rounds. When a proof fails during a forcing round it means that the ``gist'' of the proof succeeded but some ``technical detail'' failed. The first question you must ask yourself is whether the forced goals are indeed theorems. We discuss the possibilities below.

If you believe the forced goals are theorems, you should follow the usual methodology for ``fixing'' failed ACL2 proofs, e.g., the identification of key lemmas and their timely and proper use as rules. See failure and see proof-tree.

The rules designed for the goals of forcing rounds are often just what is needed to prove the forced hypothesis at the time it is forced. Thus, you may find that when the system has been ``taught'' how to prove the goals of the forcing round no forcing round is needed. This is intended as a feature to help structure the discovery of the necessary rules.

If a hint must be provided to prove a goal in a forcing round, the
appropriate ``goal specifier'' (the string used to identify the goal
to which the hint is to be applied) is just the text printed on the
line above the formula, e.g., `"[1]Subgoal *1/3''"`

.
See goal-spec.

If you solve a forcing problem by giving explicit hints for the goals of forcing rounds, you might consider whether you could avoid forcing the assumption in the first place by giving those hints in the appropriate places of the main proof. This is one reason that we print out the origins of each forced assumption. An argument against this style, however, is that an assumption might be forced in hundreds of places in the main goal and proved only once in the forcing round, so that by delaying the proof you actually save time.

We now turn to the possibility that some goal in the forcing round is not a theorem.

There are two possibilities to consider. The first is that the original theorem has insufficient hypotheses to insure that all the forced hypotheses are in fact always true. The ``fix'' in this case is to amend the original conjecture so that it has adequate hypotheses.

A more difficult situation can arise and that is when the conjecture has sufficient hypotheses but they are not present in the forcing round goal. This can be caused by what we call ``premature'' forcing.

Because ACL2 rewrites from the inside out, it is possible that it
will force hypotheses while the context is insufficient to establish
them. Consider trying to prove `(p x (foo x))`

. We first rewrite the
formula in an empty context, i.e., assuming nothing. Thus, we
rewrite `(foo x)`

in an empty context. If rewriting `(foo x)`

forces
anything, that forced assumption will have to be proved in an empty
context. This will likely be impossible.

On the other hand, suppose we did not attack `(foo x)`

until after we
had expanded `p`

. We might find that the value of its second
argument, `(foo x)`

, is relevant only in some cases and in those cases
we might be able to establish the hypotheses forced by `(foo x)`

. Our
premature forcing is thus seen to be a consequence of our ``over
eager'' rewriting.

Here, just for concreteness, is an example you can try. In this
example, `(foo x)`

rewrites to `x`

but has a forced hypothesis of
`(rationalp x)`

. `P`

does a case split on that very hypothesis
and uses its second argument only when `x`

is known to be rational.
Thus, the hypothesis for the `(foo x)`

rewrite is satisfied. On
the false branch of its case split, `p`

simplies to `(p1 x)`

which
can be proved under the assumption that `x`

is not rational.

(defun p1 (x) (not (rationalp x))) (defun p (x y)(if (rationalp x) (equal x y) (p1 x))) (defun foo (x) x) (defthm foo-rewrite (implies (force (rationalp x)) (equal (foo x) x))) (in-theory (disable foo))The attempt then to do

`(thm (p x (foo x)))`

forces the unprovable
goal `(rationalp x)`

.
Since all ``formulas'' are presented to the theorem prover as single
terms with no hypotheses (e.g., since `implies`

is a function), this
problem would occur routinely were it not for the fact that the
theorem prover expands certain ``simple'' definitions immediately
without doing anything that can cause a hypothesis to be forced.
See simple. This does not solve the problem, since it is
possible to hide the propositional structure arbitrarily deeply.
For example, one could define `p`

, above, recursively so that the test
that `x`

is rational and the subsequent first ``real'' use of `y`

occurred arbitrarily deeply.

Therefore, the problem remains: what do you do if an impossible goal is forced and yet you know that the original conjecture was adequately protected by hypotheses?

One alternative is to disable forcing entirely. See disable-forcing. Another is to disable the rule that caused the force.

A third alternative is to prove that the negation of the main goal implies the forced hypothesis. For example,

(defthm not-p-implies-rationalp (implies (not (p x (foo x))) (rationalp x)) :rule-classes nil)Observe that we make no rules from this formula. Instead, we merely

`:use`

it in the subgoal where we must establish `(rationalp x)`

.
(thm (p x (foo x)) :hints (("Goal" :use not-p-implies-rationalp)))When we said, above, that

`(p x (foo x))`

is first rewritten in an
empty context we were misrepresenting the situation slightly. When
we rewrite a literal we know what literal we are rewriting and we
implicitly assume it false. This assumption is ``dangerous'' in
that it can lead us to simplify our goal to `nil`

and give up -- we
have even seen people make the mistake of assuming the negation of
what they wished to prove and then via a very complicated series of
transformations convince themselves that the formula is false.
Because of this ``tail biting'' we make very weak use of the
negation of our goal. But the use we make of it is sufficient to
establish the forced hypothesis above.A fourth alternative is to weaken your desired theorem so as to make explicit the required hypotheses, e.g., to prove

(defthm rationalp-implies-main (implies (rationalp x) (p x (foo x))) :rule-classes nil)This of course is unsatisfying because it is not what you originally intended. But all is not lost. You can now prove your main theorem from this one, letting the

`implies`

here provide the
necessary case split.
(thm (p x (foo x)) :hints (("Goal" :use rationalp-implies-main)))

Major Section: MISCELLANEOUS

When ACL2 gives up it does not mean that the submitted conjecture is invalid, even if the last formula ACL2 printed in its proof attempt is manifestly false. Since ACL2 sometimes generalizes the goal being proved, it is possible it adopted an invalid subgoal as a legitimate (but doomed) strategy for proving a valid goal. Nevertheless, conjectures submitted to ACL2 are often invalid and the proof attempt often leads the careful reader to the realization that a hypothesis has been omitted or that some special case has been forgotten. It is good practice to ask yourself, when you see a proof attempt fail, whether the conjecture submitted is actually a theorem.

If you think the conjecture is a theorem, then you must figure out from ACL2's output what you know that ACL2 doesn't about the functions in the conjecture and how to impart that knowledge to ACL2 in the form of rules. Books could be written about this, but they haven't been yet. However, see proof-tree for a utility that may be very helpful in locating parts of the failed proof that are of particular interest. See also the discussion of how to read Nqthm proofs and how to use Nqthm rules in ``A Computational Logic Handbook'' by Boyer and Moore (Academic Press, 1988).

If the failure occurred during a forcing round,
see failed-forcing.

Major Section: MISCELLANEOUS

General Form: (find-rules-of-rune rune wrld)

This function finds all the rules in `wrld`

with `:`

`rune`

rune. It
returns a list of rules in their internal form (generally as
described by the corresponding `defrec`

). Decyphering these rules is
difficult since one cannot always look at a rule object and decide
what kind of record it is without exploiting many system invariants
(e.g., that `:`

`rewrite`

runes only name rewrite-rules).

At the moment this function returns `nil`

if the rune in question is a
`:`

`refinement`

rune, because there is no object representing
`:`

`refinement`

rules. (`:`

`refinement`

rules cause changes in the
`'coarsenings`

properties.) In addition, if the rune is an
`:`

`equivalence`

rune, then congruence rules with that rune will be
returned -- because `:`

`equivalence`

lemmas generate some congruence
rules -- but the fact that a certain function is now known to be an
equivalence relation is not represented by any rule object and so no
such rule is returned. (The fact that the function is an
equivalence relation is encoded entirely in its presence as a
`'coarsening`

of `equal`

.)

Major Section: MISCELLANEOUS

When a hypothesis of a conditional rule has the form `(force hyp)`

it
is logically equivalent to `hyp`

but has a pragmatic effect. In
particular, when the rule is considered, the needed instance of the
hypothesis, `hyp'`

, is assumed and a special case is generated,
requiring the system to prove that `hyp'`

is true in the current
context. The proofs of all such ``forced assumptions'' are delayed
until the successful completion of the main goal.
See forcing-round.

Forcing should only be used on hypotheses that are always expected
to be true, such as the guards of functions. All the power of the
theorem prover is brought to bear on a forced hypothesis and no
backtracking is possible. If the `:`

`executable-counterpart`

of the
function `force`

is disabled, then no hypothesis is forced.
See enable-forcing and see disable-forcing. Forced goals can be
attacked immediately (see immediate-force-modep) or in a subsequent
forcing round (see forcing-round). See also see case-split.

It sometimes happens that a conditional rule is not applied because
some hypothesis, `hyp`

, could not be relieved, even though the
required instance of `hyp`

, `hyp'`

, can be shown true in the context.
This happens when insufficient resources are brought to bear on `hyp'`

at the time we try to relieve it. A sometimes desirable alternative
behavior is for the system to assume `hyp'`

, apply the rule, and to
generate explicitly a special case to show that `hyp'`

is true in the
context. This is called ``forcing'' `hyp`

. It can be arranged by
restating the rule so that the offending hypothesis, `hyp`

, is
embedded in a call of `force`

, as in `(force hyp)`

. By using the
`:`

`corollary`

field of the `rule-classes`

entry, a hypothesis
can be forced without changing the statement of the theorem from
which the rule is derived.

Technically, `force`

is just a function of one argument that returns
that argument. It is generally enabled and hence evaporates during
simplification. But its presence among the hypotheses of a
conditional rule causes case splitting to occur if the hypothesis
cannot be conventionally relieved.

Since a forced hypothesis must be provable whenever the rule is otherwise applicable, forcing should be used only on hypotheses that are expected always to be true. A common situation is when the hypothesis is in fact a guard (or part of a guard) of some function involved in the pattern that triggers the rule. Intuitively, if that pattern term occurs in the current conjecture, then its guards had better be true, since otherwise nothing is known about the term.

A particularly common situation in which some hypotheses should be forced is in ``most general'' type-prescription lemmas. If a single lemma describes the ``expected'' type of a function, for all ``expected'' arguments, then it is probably a good idea to force the hypotheses of the lemma. Thus, every time a term involving the function arises, the term will be given the expected type and its arguments will be required to be of the expected type. In applying this advice it might be wise to avoid forcing those hypotheses that are in fact just type predicates on the arguments, since the routine that applies type-prescription lemmas has fairly thorough knowledge of the types of all terms.

`Force`

can have the additional benefit of causing the ACL2 typing
mechanism to interact with the ACL2 rewriter to establish the
hypotheses of type-prescription rules. To understand this remark,
think of the ACL2 type reasoning system as a rather primitive
rule-based theorem prover for questions about Common Lisp types,
e.g., ``does this expression produce a `consp`

?'' ``does this
expression produce some kind of ACL2 number, e.g., an `integerp`

, a
`rationalp`

, or a `complex-rationalp`

?'' etc. It is driven by
type-prescription rules. To relieve the hypotheses of such rules,
the type system recursively invokes itself. This can be done for
any hypothesis, whether it is ``type-like'' or not, since any
proposition, `p`

, can be phrased as the type-like question ``does `p`

produce an object of type `nil`

?'' However, as you might expect, the
type system is not very good at establishing hypotheses that are not
type-like, unless they happen to be assumed explicitly in the
context in which the question is posed, e.g., ``If `p`

produces a
`consp`

then does `p`

produce `nil`

?'' If type reasoning alone is
insufficient to prove some instance of a hypothesis, then the
instance will not be proved by the type system and a
type-prescription rule with that hypothesis will be inapplicable in
that case. But by embedding such hypotheses in `force`

expressions
you can effectively cause the type system to ``punt'' them to the
rest of the theorem prover. Of course, as already noted, this
should only be done on hypotheses that are ``always true.'' In
particular, if rewriting is required to establish some hypothesis of
a type-prescription rule, then the rule will be found inapplicable
because the hypothesis will not be established by type reasoning
alone.

The ACL2 rewriter uses the type reasoning system as a subsystem. It is therefore possible that the type system will force a hypothesis that the rewriter could establish. Before a forced hypothesis is reported out of the rewriter, we try to establish it by rewriting.

This makes the following surprising behavior possible: A
type-prescription rule fails to apply because some true hypothesis
is not being relieved. The user changes the rule so as to **force** the
hypothesis. The system then applies the rule but reports no
forcing. How can this happen? The type system ``punted'' the
forced hypothesis to the rewriter, which established it.

Finally, we should mention that the rewriter is never willing to
force when there is an `if`

term present in the goal being simplified.
Since `and`

and `or`

terms are merely abbreviations for `if`

terms, they
also prevent forcing.

Major Section: MISCELLANEOUS

If ACL2 ``forces'' some hypothesis of some rule to be true, it is obliged later to prove the hypothesis. See force. ACL2 delays the consideration of forced hypotheses until the main goal has been proved. It then undertakes a new round of proofs in which the main goal is essentially the conjunction of all hypotheses forced in the preceding proof. Call this round of proofs the ``Forcing Round.'' Additional hypotheses may be forced by the proofs in the Forcing Round. The attempt to prove these hypotheses is delayed until the Forcing Round has been successfully completed. Then a new Forcing Round is undertaken to prove the recently forced hypotheses and this continues until no hypotheses are forced. Thus, there is a succession of Forcing Rounds.

The Forcing Rounds are enumerated starting from 1. The Goals and
Subgoals of a Forcing Round are printed with the round's number
displayed in square brackets. Thus, `"[1]Subgoal 1.3"`

means that
the goal in question is Subgoal 1.3 of the 1st forcing round. To
supply a hint for use in the proof of that subgoal, you should use
the goal specifier `"[1]Subgoal 1.3"`

. See goal-spec.

When a round is successfully completed -- and for these purposes you
may think of the proof of the main goal as being the 0th forcing
round -- the system collects all of the assumptions forced by the
just-completed round. Here, an assumption should be thought of as
an implication, `(implies context hyp)`

, where context describes the
context in which hyp was assumed true. Before undertaking the
proofs of these assumptions, we try to ``clean them up'' in an
effort to reduce the amount of work required. This is often
possible because the forced assumptions are generated by the same
rule being applied repeatedly in a given context.

For example, suppose the main goal is about some term
`(pred (xtrans i) i)`

and that some rule rewriting `pred`

contains a
forced hypothesis that the first argument is a `good-inputp`

.
Suppose that during the proof of Subgoal 14 of the main goal,
`(good-inputp (xtrans i))`

is forced in a context in which `i`

is
an `integerp`

and `x`

is a `consp`

. (Note that `x`

is
irrelevant.) Suppose finally that during the proof of Subgoal 28,
`(good-inputp (xtrans i))`

is forced ``again,'' but this time in a
context in which `i`

is a `rationalp`

and `x`

is a `symbolp`

.
Since the forced hypothesis does not mention `x`

, we deem the
contextual information about `x`

to be irrelevant and discard it
from both contexts. We are then left with two forced assumptions:
`(implies (integerp i) (good-inputp (xtrans i)))`

from Subgoal 14,
and `(implies (rationalp i) (good-inputp (xtrans i)))`

from Subgoal
28. Note that if we can prove the assumption required by Subgoal 28
we can easily get that for Subgoal 14, since the context of Subgoal
28 is the more general. Thus, in the next forcing round we will
attempt to prove just

(implies (rationalp i) (good-inputp (xtrans i)))and ``blame'' both Subgoal 14 and Subgoal 28 of the previous round for causing us to prove this.

By delaying and collecting the `forced`

assumptions until the
completion of the ``main goal'' we gain two advantages. First, the
user gets confirmation that the ``gist'' of the proof is complete
and that all that remains are ``technical details.'' Second, by
delaying the proofs of the forced assumptions ACL2 can undertake the
proof of each assumption only once, no matter how many times it was
forced in the main goal.

In order to indicate which proof steps of the previous round were responsible for which forced assumptions, we print a sentence explaining the origins of each newly forced goal. For example,

[1]Subgoal 1, below, will focus on (GOOD-INPUTP (XTRANS I)), which was forced in Subgoal 14, above, by applying (:REWRITE PRED-CRUNCHER) to (PRED (XTRANS I) I), and Subgoal 28, above, by applying (:REWRITE PRED-CRUNCHER) to (PRED (XTRANS I) I).

In this entry, ``[1]Subgoal 1'' is the name of a goal which will be
proved in the next forcing round. On the next line we display the
forced hypothesis, call it `x`

, which is
`(good-inputp (xtrans i))`

in this example. This term will be the
conclusion of the new subgoal. Since the new subgoal will be
printed in its entirety when its proof is undertaken, we do not here
exhibit the context in which `x`

was forced. The sentence then
lists (possibly a succession of) a goal name from the just-completed
round and some step in the proof of that goal that forced `x`

. In
the example above we see that Subgoals 14 and 28 of the
just-completed proof forced `(good-inputp (xtrans i))`

by applying
`(:rewrite pred-cruncher)`

to the term `(pred (xtrans i) i)`

.

If one were to inspect the theorem prover's description of the proof steps applied to Subgoals 14 and 28 one would find the word ``forced'' (or sometimes ``forcibly'') occurring in the commentary. Whenever you see that word in the output, you know you will get a subsequent forcing round to deal with the hypotheses forced. Similarly, if at the beginning of a forcing round a rune is blamed for causing a force in some subgoal, inspection of the commentary for that subgoal will reveal the word ``forced'' after the rule name blamed.

Most forced hypotheses come from within the prover's simplifier.
When the simplifier encounters a hypothesis of the form `(force hyp)`

it first attempts to establish it by rewriting `hyp`

to, say, `hyp'`

.
If the truth or falsity of `hyp'`

is known, forcing is not required.
Otherwise, the simplifier actually forces `hyp'`

. That is, the `x`

mentioned above is `hyp'`

, not `hyp`

, when the forced subgoal was
generated by the simplifier.

Once the system has printed out the origins of the newly forced goals, it proceeds to the next forcing round, where those goals are individually displayed and attacked.

At the beginning of a forcing round, the enabled structure defaults
to the global enabled structure. For example, suppose some rune,
`rune`

, is globally enabled. Suppose in some event you disable the
rune at `"Goal"`

and successfully prove the goal but force `"[1]Goal"`

.
Then during the proof of `"[1]Goal"`

, rune is enabled ``again.'' The
right way to think about this is that the rune is ``still'' enabled.
That is, it is enabled globally and each forcing round resumes with
the global enabled structure.

Major Section: MISCELLANEOUS

The discussion below outlines a potential source of unsoundness in ACL2. Although to our knowledge there is no existing Lisp implementation in which this problem can arise, nevertheless we feel compelled to explain this situation.

Consider for example the question: What is the value of
`(equal 3 3)`

? According to the ACL2 axioms, it's `t`

. And as
far as we know, based on considerable testing, the value is `t`

in
every Common Lisp implementation. However, according the Common
Lisp draft proposed ANSI standard, any non-`nil`

value could result.
Thus for example, `(equal 3 3)`

is allowed by the standard to be `17`

.

The Common Lisp standard specifies (or soon will) that a number of
Common Lisp functions that one might expect to return Boolean values
may, in fact, return arbitrary values. Examples of such functions
are `equal`

, `rationalp`

, and `<`

; a much more complete list is
given below. Indeed, we dare to say that every Common Lisp function
that one may believe returns only Booleans is, nevertheless, not
specified by the standard to have that property, with the exceptions
of the functions `not`

and `null`

. The standard refers to such
arbitrary values as ``generalized Booleans,'' but in fact this
terminology makes no restriction on those values. Rather, it merely
specifies that they are to be viewed, in an informal sense, as being
either `nil`

or not `nil`

.

This situation is problematic for ACL2, which axiomatizes these
functions to return Booleans. The problem is that because (for
efficiency and simplicity) ACL2 makes very direct use of compiled
Common Lisp functions to support the execution of its functions,
there is in principle a potential for unsoundness due to these
``generalized Booleans.'' For example, ACL2's `equal`

function is
defined to be Common Lisp's `equal`

. Hence if in Common Lisp the
form `(equal 3 3)`

were to evaluate to 17, then in ACL2 we could
prove (using the `:`

`executable-counterpart`

of `equal`

)
`(equal (equal 3 3) 17)`

. However, ACL2 can also prove
`(equal (equal x x) t)`

, and these two terms together are
contradictory, since they imply (instantiating `x`

in the second
term by `3`

) that `(equal 3 3)`

is both equal to `17`

and to
`t`

.

To make matters worse, the standard allows `(equal 3 3)`

to evaluate
to *different* non-`nil`

values every time. That is: `equal`

need not even be a function!

Fortunately, no existing Lisp implementation takes advantage of the flexibility to have (most of) its predicates return generalized Booleans, as far as we know. We may implement appropriate safeguards in future releases of ACL2, in analogy to (indeed, probably extending) the existing safeguards by way of guards (see guard). For now, we'll sleep a bit better knowing that we have been up-front about this potential problem.

The following list of functions contains all those that are defined
in Common Lisp to return generalized Booleans but are assumed by
ACL2 to return Booleans. In addition, the functions `acl2-numberp`

and `complex-rationalp`

are directly defined in terms of
respective Common Lisp functions `numberp`

and `complexp`

.

/= < = alpha-char-p atom char-equal char< char<= char> char>= characterp consp digit-char-p endp eq eql equal evenp integerp keywordp listp logbitp logtest lower-case-p minusp oddp plusp rationalp standard-char-p string-equal string< string<= string> string>= stringp subsetp symbolp upper-case-p zerop