`defpkg`

s
Major Section: MISCELLANEOUS

Suppose `(defpkg "pkg" imports)`

is the most recently executed
successful definition of `"pkg"`

in this ACL2 session and that it
has since been undone, as by `:`

`ubt`

. Any future attempt in this
session to define `"pkg"`

as a package must specify an identical
imports list.

The restriction stems from the need to implement the reinstallation
of saved logical worlds as in error recovery and the `:`

`oops`

command.
Suppose that the new `defpkg`

attempts to import some symbol, `a::sym`

,
not imported by the previous definition of `"pkg"`

. Because it was
not imported in the original package, the symbol `pkg::sym`

, different
from `a::sym`

, may well have been created and may well be used in some
saved worlds. Those saved worlds are Common Lisp objects being held
for you ``behind the scenes.'' In order to import `a::sym`

into
`"pkg"`

now we would have to unintern `pkg::sym`

, rendering those
saved worlds ill-formed. It is because of saved worlds that we do
not actually clear out a package when it is undone.

At one point we thought it was sound to allow the new `defpkg`

to
import a subset of the old. But that is incorrect. Suppose the old
definition of `"pkg"`

imported `a::sym`

but the new one does not.
Suppose we allowed that and implemented it simply by setting the
imports of `"pkg"`

to the new subset. Then consider the conjecture
`(eq a::sym pkg::sym)`

. This ought not be a theorem because we did
not import `a::sym`

into `"pkg"`

. But in fact in AKCL it is a theorem
because `pkg::sym`

is read as `a::sym`

because of the old imports.

Major Section: MISCELLANEOUS

Examples: (assign print-doc-start-column nil) (assign print-doc-start-column 17)

This state global variable controls the column in which the
``one-liner'' of a formatted documentation string is printed.
Generally, when `:`

`doc`

is used to print a documentation string, the
name of the documented concept is printed and then `:`

`doc`

tabs over to
`print-doc-start-column`

and prints the one-liner. If the name
extends past the desired column, `:`

`doc`

outputs a carriage return and
then tabs over to the column. If `print-doc-start-column`

is `nil`

,
`:`

`doc`

just starts the one-liner two spaces from the end of the name,
on the same line. The initial value of `print-doc-start-column`

is
15.

`ld`

Major Section: MISCELLANEOUS

The prompt printed by ACL2 conveys information about various
``modes.'' See default-print-prompt and see ld-prompt for
details.

`e0-ord-<`

is well-founded on `e0-ordinalp`

s
Major Section: MISCELLANEOUS

The soundness of ACL2 rests in part on the well-foundedness of
`e0-ord-<`

on `e0-ordinalp`

s. This can be taken as obvious if one is
willing to grant that those concepts are simply encodings of the
standard mathematical notions of the ordinals below `epsilon-0`

and
its natural ordering relation. But it is possible to prove that
`e0-ord-<`

is well-founded on `e0-ordinalp`

s without having to assert
any connection to the ordinals and that is what we do here.

We first observe three facts about `e0-ord-<`

on ordinals that have
been proved by ACL2 using only structural induction on lists.

(defthm transitivity (implies (and (e0-ordinalp x) (e0-ordinalp y) (e0-ordinalp z) (e0-ord-< x y) (e0-ord-< y z)) (e0-ord-< x z)) :rule-classes nil)These three properties establish that(defthm non-circularity (implies (and (e0-ordinalp x) (e0-ordinalp y) (e0-ord-< x y)) (not (e0-ord-< y x))) :rule-classes nil)

(defthm trichotomy (implies (and (e0-ordinalp x) (e0-ordinalp y)) (or (equal x y) (e0-ord-< x y) (e0-ord-< y x))) :rule-classes nil)

`e0-ord-<`

orders the
`e0-ordinalp`

s. To put such a statement in the most standard
mathematical nomenclature, we can define the function:
(defun e0-ord-<= (x y) (or (equal x y) (e0-ord-< x y)))and then establish that

`e0-ord-<=`

is a relation that is a simple,
complete (i.e., total) order on ordinals by the following three
lemmas, which have been proved:
(defthm antisymmetry (implies (and (e0-ordinalp x) (e0-ordinalp y) (e0-ord-<= x y) (e0-ord-<= y x)) (equal x y)) :rule-classes nil :hints (("Goal" :use non-circularity)))Crucially important to the proof of the well-foundedness of(defthm e0-ord-<=-transitivity (implies (and (e0-ordinalp x) (e0-ordinalp y) (e0-ordinalp z) (e0-ord-<= x y) (e0-ord-<= y z)) (e0-ord-<= x z)) :rule-classes nil :hints (("Goal" :use transitivity)))

(defthm trichotomy-of-e0-ord-< (implies (and (e0-ordinalp x) (e0-ordinalp y)) (or (e0-ord-<= x y) (e0-ord-<= y x))) :rule-classes nil :hints (("Goal" :use trichotomy)))

`e0-ord-<`

on `e0-ordinalp`

s is the concept of ordinal-depth,
abbreviated `od`

:
(defun od (l) (if (atom l) 0 (1+ (od (car l)))))If the

`od`

of an `e0-ordinalp`

`x`

is smaller than that of an
`e0-ordinalp`

`y`

, then `x`

is `e0-ord-<`

`y`

:
(defthm od-implies-ordlessp (implies (and (e0-ordinalp x) (e0-ordinalp y) (< (od x) (od y))) (e0-ord-< x y)))Remark. A consequence of this lemma is the fact that if

`s = s(1)`

,
`s(2)`

, ... is an infinite, `e0-ord-<`

descending sequence, then
`od(s(1))`

, `od(s(2))`

, ... is a ``weakly'' descending sequence of
non-negative integers: `od(s(i))`

is greater than or equal to
`od(s(i+1))`

.
*Lemma Main.* For each non-negative integer `n`

, `e0-ord-<`

well-orders
the set of `e0-ordinalp`

s with `od`

less than or equal to `n`

.

Base Case. n = 0. The e0-ordinalps with 0 od are the non-negative integers. On the non-negative integers, e0-ord-< is the same as <.Theorem.Induction Step. n > 0. We assume that e0-ord-< well-orders the e0-ordinalps with od less than n.

If e0-ord-< does not well-order the e0-ordinalps with od less than or equal to n, we may let O be the e0-ord-<-least e0-ordinalp which is the car of the first member of an infinite, e0-ord-< descending sequence of e0-ordinalps of od less than or equal to n. The od of O is n-1.

Let k be the least integer > 0 such that for some infinite, e0-ord-< descending sequence s of e0-ordinalps with od less than or equal to n, the first element of s begins with k occurrences of O but not k+1 occurrences of O.

Having fixed O and k, let s = s(1), s(2), ... be an infinite, e0-ord-< descending sequence of e0-ordinalps with od less than or equal to n such that O occurs exactly k times at the beginning of s(1).

O occurs exactly k times at the beginning of each s(i). For suppose that s(j) is the first member of s with exactly m occurrences of O at the beginning, m /= k. If m = 0, then the first member of s(j) must be e0-ord-< O, contradicting the minimality of O. If 0 < m < k, then the fact that the sequence beginning at s(j) is infinitely descending contradicts the minimality of k. If m > k, then s(j) is greater than its predecessor, which has only k occurrences of O at the beginning; but this contradicts the fact that s is descending.

Let t = t(1), t(2), ... be the sequence of e0-ordinalps that is obtained by letting t(i) be the result of removing O from the front of s(i) exactly k times. t is infinitely descending. Furthermore, t(1) begins with an e0-ordinalp O' that is e0-ord-< O, and hence has od at most N-1 by the lemma od-implies-ordlessp. But this contradicts the minimality of O. Q.E.D.

`e0-ord-<`

well-orders the `e0-ordinalp`

s. Proof. Every
infinite,` e0-ord-<`

descending sequence of `e0-ordinalp`

s has the
property that each member has `od`

less than or equal to the `od`

, `n`

, of
the first member of the sequence. This contradicts Lemma Main.
Q.E.D.
Major Section: MISCELLANEOUS

Example Forms: (pseudo-termp '(car (cons x 'nil))) ; has value t (pseudo-termp '(car x y z)) ; also has value t! (pseudo-termp '(delta (h x))) ; has value t (pseudo-termp '(delta (h x) . 7)) ; has value nil (not a true-listp) (pseudo-termp '((lambda (x) (car x)) b)) ; has value t (pseudo-termp '(if x y 123)) ; has value nil (123 is not quoted) (pseudo-termp '(if x y '123)) ; has value tIf

`x`

is the quotation of a term, then `(pseudo-termp x)`

is `t`

.
However, if `x`

is not the quotation of a term it is not necessarily
the case that `(pseudo-termp x)`

is `nil`

.
See term for a discussion of the various meanings of the word
``term'' in ACL2. In its most strict sense, a term is either a
legal variable symbol, a quoted constant, or the application of an
`n`

-ary function symbol or closed `lambda`

-expression to `n`

terms. By
``legal variable symbol'' we exclude constant symbols, such as `t`

,
`nil`

, and `*ts-rational*`

. By ``quoted constants'' we include `'t`

(aka
`(quote t)`

), `'nil`

, `'31`

, etc., and exclude constant names such as `t`

,
`nil`

and `*ts-rational*`

, unquoted constants such as `31`

or `1/2`

, and
ill-formed `quote`

expressions such as `(quote 3 4)`

. By ``closed
lambda expression'' we exclude expressions, such as
`(lambda (x) (cons x y))`

, containing free variables in their bodies.
Terms typed by the user are translated into strict terms for
internal use in ACL2.

The predicate `termp`

checks this strict sense of ``term'' with
respect to a given ACL2 logical world; See world. Many ACL2
functions, such as the rewriter, require certain of their arguments
to satisfy `termp`

. However, as of this writing, `termp`

is in `:`

`program`

mode and thus cannot be used effectively in conjectures to be
proved. Furthermore, if regarded simply from the perspective of an
effective guard for a term-processing function, `termp`

checks many
irrelevant things. (Does it really matter that the variable symbols
encountered never start and end with an asterisk?) For these
reasons, we have introduced the notion of a ``pseudo-term'' and
embodied it in the predicate `pseudo-termp`

, which is easier to
check, does not require the logical world as input, has `:`

`logic`

mode, and is often perfectly suitable as a guard on term-processing
functions.

A `pseudo-termp`

is either a symbol, a true list of length 2
beginning with the word `quote`

, the application of an `n`

-ary
pseudo-`lambda`

expression to a true list of `n`

pseudo-terms, or
the application of a symbol to a true list of `n`

`pseudo-termp`

s.
By an ```n`

-ary pseudo-`lambda`

expression'' we mean an expression
of the form `(lambda (v1 ... vn) pterm)`

, where the `vi`

are
symbols (but not necessarily distinct legal variable symbols) and
`pterm`

is a `pseudo-termp`

.

Metafunctions may use `pseudo-termp`

as a guard.

Major Section: MISCELLANEOUS

Example and General Form: ACL2 !>:redefThis command sets

`ld-redefinition-action`

to `'(:query . :overwrite)`

.
As explained elsewhere (see ld-redefinition-action), this
allows redefinition of functions and other events without undoing.
A query will be made every time a redefinition is commanded; the
user must explicitly acknowledge that the redefinition is
intentional. It is possible to set `ld-redefinition-action`

so that
the redefinition of non-system functions occurs quietly.
See ld-redefinition-action.

Major Section: MISCELLANEOUS

Example and General Form: ACL2 !>:redef! ACL2 p!>This command sets

`ld-redefinition-action`

to `'(:warn! . :overwrite)`

and sets the default defun-mode to `:`

`program`

.
This is the ACL2 system hacker's redefinition command. Note that
even system functions can be redefined with a mere warning. Be
careful!

Major Section: MISCELLANEOUS

Example and General Forms: (redefined-names state)

This function collects names that have been redefined in the current ACL2
state. `:`

`Program`

mode functions that were reclassified to
`:`

`logic`

functions are not collected, since such reclassification
cannot imperil soundness because it is allowed only when the new and old
definitions are identical.

Thus, if `(redefined-names state)`

returns `nil`

then no unsafe
definitions have been made, regardless of `ld-redefinition-action`

.
See ld-redefinition-action.

Major Section: MISCELLANEOUS

Sometimes an event will announce that it is ``redundant''. When this happens, no change to the logical world has occurred. This happens when the logical name being defined is already defined and has exactly the same definition, from the logical point of view. This feature permits two independent books, each of which defines some name, to be included sequentially provided they use exactly the same definition.

When are two logical-name definitions considered exactly the same? It depends upon the kind of name being defined.

A `deflabel`

event is never redundant. This means that if you have a
`deflabel`

in a book and that book has been included (without error),
then references to that label denote the point in history at which
the book introduced the label. See the note about shifting logical
names, below.

A `defun`

or `mutual-recursion`

(or `defuns`

) event is redundant if for
each function to be introduced, there has already been introduced a
function with the same name, the same formals, and syntactically
identical `guard`

, type declarations, and `body`

(before
macroexpansion).

A `verify-guards`

event is redundant if the function has already had
its guards verified.

A `defaxiom`

or `defthm`

event is redundant if there is already an axiom
or theorem of the given name and both the formula (after
macroexpansion) and the rule-classes are syntactically identical.
Note that a `defaxiom`

can make a subsequent `defthm`

redundant, and a
`defthm`

can make a subsequent `defaxiom`

redundant as well.

A `defconst`

is redundant if the name has been defined to have the
same value.

A `defstobj`

is never redundant. Blah blah...

A `defmacro`

is redundant if there is already a macro defined with the
same name and syntactically identical arguments, guard, and body.

A `defpkg`

is redundant if a package of the same name with exactly the
same imports has been defined.

A `deftheory`

is never redundant. The ``natural'' notion of
equivalent `deftheory`

s is that the names and values of the two theory
expressions are the same. But since most theory expressions are
sensitive to the context in which they occur, it seems unlikely to
us that two `deftheory`

s coming from two sequentially included books
will ever have the same values. So we prohibit redundant theory
definitions. If you try to define the same theory name twice, you
will get a ``name in use'' error.

An `in-theory`

event is never redundant because it doesn't define any
name.

A `push-untouchable`

event is redundant if every name supplied is
already a member of the untouchable symbols.

`Table`

and `defdoc`

events are never redundant because they don't
define any name.

An `encapsulate`

event is redundant if and only if a syntactically
identical `encapsulate`

has already been executed under the same
`default-defun-mode`

.

An `include-book`

is redundant if the book has already been included.

*Note About Shifting Logical Names:*

Suppose a book defines a function `fn`

and later uses `fn`

as a logical
name in a theory expression. Consider the value of that theory
expression in two different sessions. In session A, the book is
included in a world in which `fn`

is not already defined, i.e., in a
world in which the book's definition of `fn`

is not redundant. In
session B, the book is included in a world in which `fn`

is already
identically defined. In session B, the book's definition of `fn`

is
redundant. When `fn`

is used as a logical name in a theory
expression, it denotes the point in history at which `fn`

was
introduced. Observe that those points are different in the two
sessions. Hence, it is likely that theory expressions involving `fn`

will have different values in session A than in session B.

This may adversely affect the user of your book. For example,
suppose your book creates a theory via `deftheory`

that is advertised
just to contain the names generated by the book. But suppose you
compute the theory as the very last event in the book using:

(set-difference-theories (universal-theory :here) (universal-theory fn))where

`fn`

is the very first event in the book and happens to be a
`defun`

event. This expression returns the advertised set if `fn`

is
not already defined when the book is included. But if `fn`

were
previously (identically) defined, the theory is larger than
advertised.
The moral of this is simple: when building books that other people
will use, it is best to describe your theories in terms of logical
names that will not shift around when the books are included. The
best such names are those created by `deflabel`

.

Major Section: MISCELLANEOUS

Examples: ACL2 !>:Q >(make-lib "file") ... >(note-lib "file") >(LP) ACL2 !>

To save the current ACL2 logical world to a file, exit ACL2 with `:`

`q`

and invoke `(make-lib "file")`

in Common Lisp. This creates a file
`"file.lib"`

and a file `"file.lisp"`

. The latter will be compiled.
It generally takes half an hour to save an ACL2 logical world and
creates a 20Mb file. All things considered it is probably better to
just save your core image.

To restore such a saved ACL2 world, invoke `(note-lib "file")`

from
Common Lisp, and then enter ACL2 with `(lp)`

. We do not save the `io`

system, the stacks, or the global table, hence bindings of your
globals will not be restored.

This save/restore mechanism is a temporary expedient. We know of
faster mechanisms, mechanisms that consume less disk space, and
mechanisms that provide more functionality. We don't know of good
compromises between these various desirable features.

Major Section: MISCELLANEOUS

Examples: ((hd *) => *) ((printer * state) => (mv * * state)) ((mach * mach-state * state) => (mv * mach-state)General Form: ((fn ...) => *) ((fn ...) => stobj) or ((fn ...) => (mv ...))

where `fn`

is the constrained function symbol, `...`

is a list
of asterisks and/or the names of single-threaded objects and
`stobj`

is a single-threaded object name. ACL2 also supports an
older style of signature described below after we describe the
preferred style.

Signatures specify three syntactic aspects of a function symbol: (1)
the ``arity'' or how many arguments the function takes, (2) the
``multiplicity'' or how many results it returns via `MV`

, and (3)
which of those arguments and results are single-threaded objects and
which objects they are.

For a discussion of single-threaded objects, see stobj. For
the current purposes it is sufficient to know that every single-
threaded object has a unique symbolic name and that `state`

is
the name of the only built-in single-threaded object. All other
stobjs are introduced by the user via `defstobj`

. An object that
is not a single-threaded object is said to be ``ordinary.''

The general form of a signature is `((fn x1 ... xn) => val)`

. So
a signature has two parts, separated by the symbol ``=>''. The
first part, `(fn x1 ... xn)`

, is suggestive of a call of the
constrained function. The number of ``arguments,'' `n`

, indicates
the arity of `fn`

. Each `xi`

must be a symbol. If a given
`xi`

is the symbol ``*'' then the corresponding argument must be
ordinary. If a given `xi`

is any other symbol, that symbol must
be the name of a single-threaded object and the corresponding
argument must be that object. No stobj name may occur twice among the
`xi`

.

The second part, `val`

, of a signature is suggestive of a term and
indicates the ``shape'' of the output of `fn`

. If `val`

is a
symbol then it must be either the symbol ``*'' or the name of a
single-threaded object. In either case, the multiplicity of `fn`

is 1 and `val`

indicates whether the result is ordinary or a
stobj. Otherwise, `val`

is of the form `(mv y1 ... yk)`

, where
`k`

> 1. Each `yi`

must be either the symbol ``*'' or the name
of a stobj. Such a `val`

indicates that `fn`

has multiplicity
`k`

and the `yi`

indicate which results are ordinary and which
are stobjs. No stobj name may occur twice among the `yi`

.

Finally, a stobj name may appear in `val`

only if appears among the
`xi`

.

Before ACL2 supported user-declared single-threaded objects there
was only one single-threaded object: ACL2's built-in notion of
`state`

. The notion of signature supported then gave a special
role to the symbol `state`

and all other symbols were considered
to denote ordinary objects. ACL2 still supports the old form of
signature, but it is limited to functions that operate on ordinary
objects or ordinary objects and `state`

.

Old-Style General Form: (fn formals result)

where `fn`

is the constrained function symbol, `formals`

is a
suitable list of formal parameters for it, and `result`

is either
a symbol denoting that the function returns one result or else
`result`

is an `mv`

expression, `(mv s1 ... sn)`

, where
`n>1`

, each `si`

is a symbol, indicating that the function
returns `n`

results. At most one of the formals may be the symbol
`STATE`

, indicating that corresponding argument must be ACL2's
built-in `state`

. If `state`

appears in `formals`

then
`state`

may appear once in `result`

. All ``variable symbols''
other than `state`

in old style signatures denote ordinary
objects, regardless of whether the symbol has been defined to be a
single-threaded object name!

We also support a variation on old style signatures allowing the user
to declare which symbols (besides `state`

) are to be considered
single-threaded object names. This form is

(fn formals result :stobjs names)where

`names`

is either the name of a single-threaded object or else
is a list of such names. Every name in `names`

must have been
previously defined as a stobj via `defstobj`

.
`:`

`definition`

and `:`

`rewrite`

rules used in preprocessing
Major Section: MISCELLANEOUS

Example of simple rewrite rule: (equal (car (cons x y)) x)Examples of simple definition: (defun file-clock-p (x) (integerp x)) (defun naturalp (x) (and (integerp x) (>= x 0)))

The theorem prover output sometimes refers to ``simple'' definitions
and rewrite rules. These rules can be used by the preprocessor,
which is one of the theorem prover's ``processes'' understood by the
`:do-not`

hint; see hints.

The preprocessor expands certain definitions and uses certain
rewrite rules that it considers to be ``fast''. There are two ways
to qualify as fast. One is to be an ``abbreviation'', where a
rewrite rule with no hypotheses or loop stopper is an
``abbreviation'' if the right side contains no more variable
occurrences than the left side, and the right side does not call the
functions `if`

, `not`

or `implies`

. Definitions and rewrite rules can
both be abbreviations; the criterion for definitions is similar,
except that the definition must not be recursive. The other way to
qualify applies only to a non-recursive definition, and applies when
its body is a disjunction or conjunction, according to a perhaps
subtle criterion that is intended to avoid case splits.

Major Section: MISCELLANEOUS

Occasionally the ACL2 theorem prover reports that the current goal simplifies to itself or to a set including itself. Such simplifications are said to be ``specious'' and are ignored in the sense that the theorem prover acts as though no simplification were possible and tries the next available proof technique. Specious simplifications are almost always caused by forcing.

The simplification of a formula proceeds primarily by the local
application of `:`

`rewrite`

, `:`

`type-prescription`

, and other rules to its
various subterms. If no rewrite rules apply, the formula cannot be
simplified and is passed to the next ACL2 proof technique, which is
generally the elimination of destructors. The experienced ACL2 user
pays special attention to such ``maximally simplified'' formulas;
the presence of unexpected terms in them indicates the need for
additional rules or the presence of some conflict that prevents
existing rules from working harmoniously together.

However, consider the following interesting possibility: local
rewrite rules apply but, when applied, reproduce the goal as one of
its own subgoals. How can rewrite rules apply and reproduce the
goal? Of course, one way is for one rule application to undo the
effect of another, as when commutativity is applied twice in
succession to the same term. Another kind of example is when rules
conflict and undermine each other. For example, under suitable
hypotheses, `(length x)`

might be rewritten to `(+ 1 (length (cdr x)))`

by the `:`

`definition`

of `length`

and then a `:`

`rewrite`

rule might be used
to ``fold'' that back to `(length x)`

. Generally speaking the
presence of such ``looping'' rewrite rules causes ACL2's simplifier
either to stop gracefully because of heuristics such as that
described in the documentation for `loop-stopper`

or to cause a
stack overflow because of indefinite recursion.

A more insidious kind of loop can be imagined: two rewrites in different parts of the formula undo each other's effects ``at a distance,'' that is, without ever being applied to one another's output. For example, perhaps the first hypothesis of the formula is simplified to the second, but then the second is simplified to the first, so that the end result is a formula propositionally equivalent to the original one but with the two hypotheses commuted. This is thought to be impossible unless forcing or case-splitting occurs, but if those features are exploited (see force and see case-split) it can be made to happen relatively easily.

Here is a simple example. Declare `foo`

to be a function of one
argument returning one result:

(defstub foo (x) t)Add the following

`:`

`type-prescription`

rule about `foo`

:
(defaxiom forcer (implies (force (not (true-listp x))) (equal (foo x) t)) :rule-classes :type-prescription)Note that we could define a

`foo`

with this property; `defstub`

and
`defaxiom`

are only used here to get to the gist of the problem
immediately. Consider the proof attempt for the following formula.
(thm (implies (and (consp x) ; hyp 1 (true-listp (cdr x)) ; hyp 2 (true-listp x)) ; hyp 3 (foo x))) ; conclWhen we simplify this goal,

`hyp 1`

cannot be simplified. `Hyp 2`

simplifies to `t`

, because `x`

is known to be a non-`nil`

true list so its
`cdr`

is a true list by type reasoning; because true hypotheses are
dropped, `hyp 2`

simply disappears. `Hyp 3`

simplifies to
`(true-listp (cdr x))`

by opening up the `:`

`definition`

of
`true-listp`

. Note that `hyp 3`

has simplified to the old `hyp 2`

.
So at this point, the ``current (intermediate) goal'' is
(implies (and (consp x) ; rewritten hyp 1 (true-listp (cdr x))) ; rewritten hyp 3 (foo x)) ; unrewritten concland we are working on

`(foo x)`

. But the `:`

`type-prescription`

rule
above tells us that `(foo x)`

is `t`

if the hypothesis of the rule is
true. Thus, in the case that the hypothesis of the rule is true, we
are done. It remains to prove the current intermediate goal under
the assumption that the hypothesis of the rule is false. This is
done by adding the negation of the `:`

`type-prescription`

rule's
hypothesis to the current intermediate goal. This is what `force`

does in this situation. The negation of the hypothesis is
`(true-listp x)`

. Adding it to the current goal produces the subgoal
(implies (and (consp x) ; rewritten hyp 1 (true-listp (cdr x)) ; rewritten hyp 3 (true-listp x)) ; FORCEd hyp (foo x)). ; unrewritten conclObserve that this is just our original goal. Despite all the rewriting, no progress was made! In more common cases, the original goal may simplify to a set of subgoals, one of which includes the original goal.

If ACL2 were to adopt the new set of subgoals, it would loop indefinitely. Therefore, it checks whether the input goal is a member of the output subgoals. If so, it announces that the simplification is ``specious'' and pretends that no simplification occurred.

``Maximally simplified'' formulas that produce specious simplifications are maximally simplified in a very technical sense: were ACL2 to apply every applicable rule to them, no progress would be made. Since ACL2 can only apply every applicable rule, it cannot make further progress with the formula. But the informed user can perhaps identify some rule that should not be applied and make it inapplicable by disabling it, allowing the simplifier to apply all the others and thus make progress.

When specious simplifications are a problem it might be helpful to disable all forcing (including case-splits) and resubmit the formula to observe whether forcing is involved in the loop or not. See force. The commands

ACL2 !>:disable-forcing and ACL2 !>:enable-forcingdisable and enable the pragmatic effects of both

`force`

and `case-split`

. If the loop is broken when forcing is
disabled, then it is very likely some forced hypothesis of
some rule is ``undoing'' a prior simplification. The most common
cause of this is when we force a hypothesis that is actually
false but whose falsity is somehow temporarily hidden (more below).
To find the offending rule, compare the specious simplification with
its non-specious counterpart and look for rules that were speciously
applied that are not applied in the non-specious case. Most likely
you will find at least one such rule and it will have a `force`

d
hypothesis. By disabling that rule, at least for the subgoal in
question, you may allow the simplifier to make progress on the
subgoal.
To illustrate what we mean by the claim that specious
simplifications often arise because the system forces a false
hypothesis, reconsider the example above. At the time we used the
`:`

`type-prescription`

rule, the known assumptions were `(consp x)`

and
`(true-listp (cdr x))`

. Observe that this tells us that `x`

is a true
list. But the hypothesis forced to be true was
`(not (true-listp x))`

. Why was the falsity of this hypothesis
missed? The most immediate reason is that the encoding of the two
assumptions above does not produce a context (``type-alist'') in
which `x`

is recorded to be a true-list. When we look up
`(not (true-listp x))`

in that context, we are not told that it is
false. More broadly, the problem stems from the fact that when we
force a hypothesis we do not bring to bear on it all of the
resources of the theorem prover. Thus it could be -- as here --
that the hypothesis could be proved false in the current context but
is not obviously so. No matter how sophisticated we made the
forcing mechanism, the unavoidable incompleteness of the theorem
prover would still permit the occasional specious simplification.
While that does not excuse us from trying to avoid specious
simplifications when we can -- and we may well strengthen the type
mechanism to deal with the problem illustrated here -- specious
simplifications will probably remain a problem deserving of the
user's attention.