Major Section: OTHER

Example Form: (skip-proofs (defun foo (x) (if (atom x) nil (cons (car x) (foo (reverse (cdr x)))))))whereGeneral Form: (skip-proofs form)

`form`

is processed as usual except that the proof obligations
usually generated are merely assumed.
Normally `form`

is an event; see events. If you want to put
`skip-proofs`

around more than one event, consider the following
(see progn): `(skip-proofs (progn event1 event2 ... eventk))`

.

WARNING: Skip-proofs allows inconsistent events to be admitted to the logic. Use it at your own risk!

Sometimes in the development of a formal model or proof it is
convenient to skip the proofs required by a given event. By
embedding the event in a `skip-proofs`

form, you can avoid the
proof burdens generated by the event, at the risk of introducing
unsoundness. Below we list four illustrative situations in which
you might find `skip-proofs`

useful.

1. The termination argument for a proposed function definition is
complicated. You presume you could admit it, but are not sure that
your definition has the desired properties. By embedding the
`defun`

event in a `skip-proofs`

you can ``admit'' the
function and experiment with theorems about it before undoing
(see ubt) and then paying the price of its admission. Note however
that you might still have to supply a measure. The set of formals
used in some valid measure, known as the ``measured subset'' of the
set of formals, is used by ACL2's induction heuristics and therefore
needs to be suitably specified. You may wish to specify the special
measure of `(:? v1 ... vk)`

, where `(v1 ... vk)`

enumerates the
measured subset.

2. You intend eventually to verify the guards for a definition but
do not want to take the time now to pursue that. By embedding the
`verify-guards`

event in a `skip-proofs`

you can get the system to
behave as though the guards were verified.

3. You are repeatedly recertifying a book while making many
experimental changes. A certain `defthm`

in the book takes a very
long time to prove and you believe the proof is not affected by the
changes you are making. By embedding the `defthm`

event in a
`skip-proofs`

you allow the theorem to be assumed without proof
during the experimental recertifications.

4. You are constructing a proof top-down and wish to defer the proof
of a `defthm`

until you are convinced of its utility. You can
embed the `defthm`

in a `skip-proofs`

. Of course, you may find
later (when you attempt prove the theorem) that the proposed `defthm`

is not a theorem.

Unsoundness or Lisp errors may result if the presumptions underlying
a use of `skip-proofs`

are incorrect. Therefore, `skip-proofs`

must be considered a dangerous (though useful) tool in system
development.

Roughly speaking, a `defthm`

embedded in a `skip-proofs`

is
essentially a `defaxiom`

, except that it is not noted as an axiom
for the purposes of functional instantiation
(see lemma-instance). But a skipped `defun`

is much more
subtle since not only is the definitional equation being assumed but
so are formulas relating to termination and type. The situation is
also difficult to characterize if the `skip-proofs`

events are
within the scope of an `encapsulate`

in which constrained functions
are being introduced. In such contexts no clear logical story is
maintained; in particular, constraints aren't properly tracked for
definitions. A proof script involving `skip-proofs`

should be
regarded as work-in-progress, not as a completed proof with some
unproved assumptions. A `skip-proofs`

event represents a promise
by the author to admit the given event without further axioms. In
other words, `skip-proofs`

should only be used when the belief is
that the proof obligations are indeed theorems in the existing ACL2
logical world.

ACL2 allows the certification of books containing `skip-proofs`

events. This is contrary to the spirit of certified books, since
one is supposedly assured by a valid certificate that a book has
been ``blessed.'' But certification, too, takes the view of
`skip-proofs`

as ``work-in-progress'' and so allows the author of
the book to promise to finish. When such books are certified, a
warning to the author is printed, reminding him or her of the
incurred obligation. When books containing `skip-proofs`

are
included into a session, a warning to the user is printed, reminding
the user that the book is in fact incomplete and possibly
inconsistent. This warning is in fact an error if `:skip-proofs-okp`

is `nil`

in the `include-book`

form; see include-book.