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.
