SKIP-PROOFS

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)

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.