functions with defun-mode of :program considered unsound
Parent topic: MISCELLANEOUS Home
Technically speaking, in the current implementation, the execution
of functions having defun-mode :program may damage the ACL2 system
in a way that renders it unsound. See defun-mode for a
discussion of defun-modes. That discussion describes an imagined
implementation that is slightly different from this one. This note
explains that the current implementation is open to unsoundness.
For discussion of a different soundness issue that is also related to function execution, see generalized-booleans.
The execution of a function having defun-mode :program may violate
Common Lisp guards on the subroutines used. (This may be true even
for calls of a function on arguments that satisfy its guard, because
ACL2 has not verified that its guard is sufficient to protect its
subroutines.) When a guard is violated at runtime all bets are off.
That is, no guarantees are made either about the answer being
``right'' or about the continued rationality of the ACL2 system
itself.
For example, suppose you make the following defun:
(defun crash (i) (declare (xargs :mode :program :guard (integerp i))) (car i))
Note that the declared guard does not in fact adequately protect the
subroutines in the body of crash; indeed, satisfying the guard to
crash will guarantee that the car expression is in violation
of its guard. Because this function is admitted in
:program-mode, no checks are made concerning the suitability
of the guard. Furthermore, in the current ACL2 implementation,
crash is executed directly in Common Lisp. Thus if you call
crash on an argument satisfying its guard you will cause an
erroneous computation to take place.
ACL2 !>(crash 7) Error: Caught fatal error [memory may be damaged] ...There is no telling how much damage is done by this errant computation. In some lisps your ACL2 job may actually crash back to the operating system. In other lisps you may be able to recover from the ``hard error'' and resume ACL2 in a damaged but apparently functional image.
THUS, HAVING A FUNCTION WITH DEFUN-MODE :PROGRAM IN YOUR SYSTEM
ABSOLVES US, THE ACL2 IMPLEMENTORS, FROM RESPONSIBILITY FOR THE
SOUNDNESS OF OUR SYSTEM.
Furthermore
ACL2 DOES NOT YET PROVIDE ANY MEANS OF REGAINING ASSURANCES OF
SOUNDNESS AFTER THE INTRODUCTION OF A FUNCTION IN :PROGRAM MODE,
EVEN IF IT IS ULTIMATELY CONVERTED TO :LOGIC MODE (since its
execution could have damaged the system in a way that makes it
possible to verify its termination and guards unsoundly).
Finally,
THE VAST MAJORITY OF ACL2 SYSTEM CODE IS IN :PROGRAM MODE AND SO ALL
BETS ARE OFF FROM BEFORE YOU START!
This hopeless state of current affairs will change, we think. We
think we have defined our functions ``correctly'' in the sense that
they can be converted, without ``essential'' modification, to
:logic mode. We think it very unlikely that a mis-guarded
function in :program mode (whether ours or yours) will cause
unsoundness without some sort of hard lisp error accompanying it.
We think that ultimately we can make it possible to execute your
functions (interpretively) without risk to the system, even when some have
:program mode. In that imagined implementation, code using
functions having :program mode would run more slowly, but safely.
These functions could be introduced into the logic ex post facto,
whereupon the code's execution would speed up because Common Lisp
would be allowed to execute it directly. We therefore ask that you
simply pretend that this is that imagined implementation, introduce
functions in :program mode, use them as convenient and perhaps
ultimately introduce some of them in :logic mode and prove their
properties. If you use the system this way we can develop (or
dismiss) this style of formal system development. BUT BE ON THE
LOOKOUT FOR SCREWUPS DUE TO DAMAGE CAUSED BY THE EXECUTION OF YOUR
FUNCTIONS HAVING :PROGRAM MODE!
an alternative to mutual-recursion
Parent topic: MISCELLANEOUS Home
Example: (DEFUNS (evenlp (x) (if (consp x) (oddlp (cdr x)) t)) (oddlp (x) (if (consp x) (evenlp (cdr x)) nil)))is equivalent toGeneral Form: (DEFUNS defuns-tuple1 ... defuns-tuplen)
(MUTUAL-RECURSION (DEFUN . defuns-tuple1) ... (DEFUN . defuns-tuplen))In fact,
defuns is the more primitive of the two and
mutual-recursion is just a macro that expands to a call of defun
after stripping off the defun at the car of each argument to
mutual-recursion. We provide and use mutual-recursion rather than
defuns because by leaving the defuns in place, mutual-recursion
forms can be processed by the Emacs tags program.
See mutual-recursion.
to disallow forced case splits
Parent topic: MISCELLANEOUS Home
General Form: ACL2 !>:disable-forcing ; disallow forced case splitsSee force for a discussion of forced case splits.
Disable-forcing is a macro that disables the executable
counterpart of the function symbol force; see force. When
you want to disable forcing in hints, use a form such as:
:in-theory (disable (:executable-counterpart force))
determine whether a given name or rune is disabled
Parent topic: MISCELLANEOUS Home
Examples::disabledp foo ; returns a list of all disabled runes whose base ; symbol is foo (see rune) (disabledp 'foo) ; same as above (i.e., :disabledp foo) :disabledp (:rewrite bar . 1) ; returns t if the indicated rune is ; disabled, else nil (disabledp (:rewrite bar . 1)); same as immediately above
Also see pr, which gives much more information about the rules associated with a given event.
Disabledp takes one argument, an event name or a rune. In the
former case it returns the list of disabled runes associated with
that name (in the sense that the rune's ``base symbol'' is that
name; see rune). In the latter case it returns t if the given
rune is disabled, and nil otherwise.
the well-founded less-than relation on ordinals up to epsilon-0
Parent topic: MISCELLANEOUS Home
If x and y are both e0-ordinalps (see e0-ordinalp) then
(e0-ord-< x y) is true iff x is strictly less than y. e0-ord-< is
well-founded on the e0-ordinalps. When x and y are both nonnegative
integers, e0-ord-< is just the familiar < relation.
e0-ord-< plays a key role in the formal underpinnings of the ACL2
logic. In order for a recursive definition to be admissible it must
be proved to ``terminate.'' By terminate we mean that the arguments to
the function ``get smaller'' as the function recurses and this sense
of size comparison must be such that there is no ``infinitely
descending'' sequence of ever smaller arguments. That is, the
relation used to compare successive arguments must be well-founded
on the domain being measured.
The most basic way ACL2 provides to prove termination requires the
user to supply (perhaps implicitly) a mapping of the argument tuples
into the ordinals with some ``measure'' expression in such a way
that the measures of the successive argument tuples produced by
recursion decrease according to the relation e0-ord-<. The validity
of this method rests on the well-foundedness of e0-ord-< on the
e0-ordinalps.
Without loss of generality, suppose the definition in question
introduces the function f, with one formal parameter x (which might
be a list of objects). Then we require that there exist a measure
expression, (m x), that always produces an e0-ordinalp.
Furthermore, consider any recursive call, (f (d x)), in the body of
the definition. Let hyps be the conjunction terms (each of which is
either the test of an if in the body or else the negation of such a
test) describing the path through the body to the recursive call in
question. Then it must be a theorem that
(IMPLIES hyps (E0-ORD-< (m (d x)) (m x))).When we say
e0-ord-< is ``well-founded'' on the e0-ordinalps we
mean that there is no infinite sequence of e0-ordinalps such that
each is smaller than its predecessor in the sequence. Thus, the
theorems that must be proved about f when it is introduced establish
that it cannot recur forever because each time a recursive call is
taken (m x) gets smaller. From this, and the syntactic restrictions
on definitions, it can be shown (as on page 44 in ``A Computational
Logic'', Boyer and Moore, Academic Press, 1979) that there exists a
function satisfying the definition; intuitively, the value assigned
to any given x by the alleged function is that computed by a
sufficiently large machine. Hence, the logic is consistent if the
axiom defining f is added.See e0-ordinalp for a discussion of the ordinals and how to compare two ordinals.
The definitional principle permits the use of relations other than
e0-ord-< but they must first be proved to be well-founded on some
domain. See well-founded-relation. Roughly put, alternative
relations are shown well-founded by providing an order-preserving
mapping from their domain into the ordinals. See defun for
details on how to specify which well-founded relation is to be
used.
a recognizer for the ordinals up to epsilon-0
Parent topic: MISCELLANEOUS Home
Using the nonnegative integers and lists we can represent the
ordinals up to epsilon-0. The ACL2 notion of ordinal is the same as
that found in nqthm-1992 and both are very similar to the
development given in ``New Version of the Consistency Proof for
Elementary Number Theory'' in The Collected Papers of Gerhard
Gentzen, ed. M.E. Szabo, North-Holland Publishing Company,
Amsterdam, 1969, pp 132-213.
The following essay is intended to provide intuition about ordinals.
The truth, of course, lies simply in the ACL2 definitions of
e0-ordinalp and e0-ord-<.
Very intuitively, think of each non-zero natural number as by being denoted by a series of the appropriate number of strokes, i.e.,
0 0 1 | 2 || 3 ||| 4 |||| ... ...Then ``
omega,'' here written as w, is the ordinal that might be
written as
w |||||...,i.e., an infinite number of strokes. Addition here is just concatenation. Observe that adding one to the front of
w in the
picture above produces w again, which gives rise to a standard
definition of w: w is the least ordinal such that adding another
stroke at the beginning does not change the ordinal.
We denote by w+w or w*2 the ``doubly infinite'' sequence that we
might write as follows.
w*2 |||||... |||||...One way to think of
w*2 is that it is obtained by replacing each
stroke in 2 (||) by w. Thus, one can imagine w*3, w*4, etc., which
leads ultimately to the idea of ``w*w,'' the ordinal obtained by
replacing each stroke in w by w. This is also written as ``omega
squared'' or w^2, or:
2 w |||||... |||||... |||||... |||||... |||||... ...We can analogously construct
w^3 by replacing each stroke in w by
w^2 (which, it turns out, is the same as replacing each stroke in
w^2 by w). That is, we can construct w^3 as w copies of w^2,
3 2 2 2 2 w w ... w ... w ... w ... ...Then we can construct
w^4 as w copies of w^3, w^5 as w copies of
w^4, etc., ultimately suggesting w^w. We can then stack omegas,
i.e., (w^w)^w etc. Consider the ``limit'' of all of those stacks,
which we might display as follows.
.
.
.
w
w
w
w
w
That is epsilon-0.
Below we begin listing some ordinals up to epsilon-0; the reader can
fill in the gaps at his or her leisure. We show in the left column
the conventional notation, using w as ``omega,'' and in the right
column the ACL2 object representing the corresponding ordinal.
ordinal ACL2 representationObserve that the sequence of0 0 1 1 2 2 3 3 ... ... w '(1 . 0) w+1 '(1 . 1) w+2 '(1 . 2) ... ... w*2 '(1 1 . 0) (w*2)+1 '(1 1 . 1) ... ... w*3 '(1 1 1 . 0) (w*3)+1 '(1 1 1 . 1) ... ...
2 w '(2 . 0) ... ...
2 w +w*4+3 '(2 1 1 1 1 . 3) ... ...
3 w '(3 . 0) ... ...
w w '((1 . 0) . 0) ... ...
w 99 w +w +4w+3 '((1 . 0) 99 1 1 1 1 . 3) ... ...
2 w w '((2 . 0) . 0)
... ...
w w w '(((1 . 0) . 0) . 0) ... ...
e0-ordinalps starts with the
nonnegative integers. This is convenient because it means that if a
term, such as a measure expression for justifying a recursive
function (see e0-ord-<) must produce an e0-ordinalp it suffices
for it to produce a nonnegative integer.
The ordinals listed above are listed in ascending order. This is
the ordering tested by e0-ord-<.
The ``epsilon-0 ordinals'' of ACL2 are recognized by the recursively
defined function e0-ordinalp. The base case of the recursion tells
us that positive integers are epsilon-0 ordinals. Otherwise, an
epsilon-0 ordinal is a cons pair (o1 . o2), where o1 is a non-0
epsilon-0 ordinal, o2 is an epsilon-0 ordinal, and if o2 is not an
integer then its car (which, by the foregoing, must be an epsilon-0
ordinal) is no greater than o1. Thus, if you think of a
(non-integer) epsilon-0 ordinal as a list, each element is an non-0
epsilon-0 ordinal, the ordinals are listed in weakly descending
order, and the final cdr of the list is an integer.
The function e0-ord-< compares two epsilon-0 ordinals, x and y. If
both are integers, e0-ord-< is just x<y. If one is an integer and
the other is a cons, the integer is the smaller. Otherwise, the
ordinals in their cars are compared recursively and determines which
is smaller unless the cars are equal, in which case the ordinals in
their cdrs are compared.
Fundamental to ACL2 is the fact that e0-ord-< is well-founded on
epsilon-0 ordinals. That is, there is no ``infinitely descending
chain'' of such ordinals. See proof-of-well-foundedness.
forms that may be embedded in other events
Parent topic: MISCELLANEOUS Home
Examples:
(defun hd (x) (if (consp x) (car x) 0))
(local (defthm lemma23 ...))
(progn (defun fn1 ...)
(local (defun fn2 ...))
...)
General Form:
An embedded event form is a term, x, such that
x is a call of an event function other than DEFPKG (see the
documentation for `events' for a listing of the event functions);
x is of the form (LOCAL x1) where x1 is an embedded event form;
x is of the form (PROGN x1 ... xn), where each xi is an embedded
event form;
x is of the form (VALUE &), where & is any term;
x macroexpands to one of the forms above.
An exception: an embedded event form may not set the
acl2-defaults-table when in the context of local. Thus for example,
the form
(local (table acl2-defaults-table :defun-mode :program))is not an embedded event form, nor is the form
(local (program)),
since the latter sets the acl2-defaults-table implicitly. An
example at the end of the discussion below illustrates why there is
this restriction.
When an embedded event is executed while ld-skip-proofsp is
'include-book, those parts of it inside local forms are ignored.
Thus,
(progn (defun f1 () 1)
(local (defun f2 () 2))
(defun f3 () 3))
will define f1, f2, and f3 when ld-skip-proofsp is nil but will
define only f1 and f3 when ld-skip-proofsp is 'include-book.Discussion:
Encapsulate and include-book place restrictions on the kinds of
forms that may be processed. These restrictions insure that the
non-local events (which will ultimately be processed with
ld-skip-proofs t) are indeed admissible provided that the sequence
of local and non-local events is admissible when ld-skip-proofs is
nil.
Local permits the hiding of an event or group of events in the sense
that local events are processed when we are trying to establish the
admissibility of a sequence of embedded events but are ignored when
we are constructing the world produced by assuming that sequence.
Thus, for example, a particularly ugly and inefficient :rewrite rule
might be made local to an encapsulate that ``exports'' a desirable
theorem whose proof requires the ugly lemma.
To see why we can't allow just anything in as an embedded event, consider allowing the form
(if (ld-skip-proofsp state)
(defun foo () 2)
(defun foo () 1))
followed by
(defthm foo-is-1 (equal (foo) 1)).When we process the events with
ld-skip-proofsp, nil the second
defun is executed and the defthm succeeds. But when we process the
events with ld-skip-proofsp 'include-book, the second defun is
executed, so that foo no longer has the same definition it did when
we proved foo-is-1. Thus, an invalid formula is assumed when we
process the defthm while skipping proofs. Thus, the first form
above is not a legal embedded event form.
Defpkg is not allowed because it affects how things are read after
it is executed. But all the forms embedded in an event are read
before any are executed. That is,
(encapsulate nil
(defpkg "MY-PKG" nil)
(defun foo () 'my-pkg::bar))
makes no sense since my-pkg::bar must have been read before the
defpkg for "MY-PKG" was executed.
Finally, let us elaborate on the restriction mentioned earlier
related to the acl2-defaults-table. Consider the following form.
(encapsulate
()
(local (program))
(defun foo (x)
(if (equal 0 x)
0
(1+ (foo (- x))))))
See local-incompatibility for a discussion of how encapsulate
processes event forms. Briefly, on the first pass through the
events the definition of foo will be accepted in defun mode
:program, and hence accepted. But on the second pass the form
(local (program)) is skipped because it is marked as local, and
hence foo is accepted in defun mode :logic. Yet, no proof has been
performed in order to admit foo, and in fact, it is not hard to
prove a contradiction from this definition!
to allow forced case splits
Parent topic: MISCELLANEOUS Home
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))
The first millisecond of the Big Bang
Parent topic: MISCELLANEOUS Home
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 defconsts, defuns, and defaxioms, 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.
escaping to Common Lisp
Parent topic: MISCELLANEOUS Home
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).
to print (hide ...) as <hidden>
Parent topic: MISCELLANEOUS Home
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.
a rule for computing the value of a function
Parent topic: MISCELLANEOUS Home
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 (x) t))
(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 all functions, even such ``constrained'' ones, have
executable counterparts. We essentially ``trap'' when such calls
are inappropriate. Thus, consider for example:
(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.
the end of pre-history
Parent topic: MISCELLANEOUS Home
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.
how to deal with a proof failure in a forcing round
Parent topic: MISCELLANEOUS Home
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)))
how to deal with a proof failure
Parent topic: MISCELLANEOUS Home
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.