Major Section: OTHER

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

`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 by providing the keyword argument `:skip-proofs-okp t`

to the
`certify-book`

command. 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.

We conclude with a technical note. `Skip-proofs`

works by binding the
`ld`

special `ld-skip-proofsp`

to `t`

unless it is already bound to
a non-`nil`

value; see ld-skip-proofsp.