## SKIP-PROOFS

skip proofs for an event -- a quick way to introduce unsoundness
```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 event)
```
where `event` is an event; see events. `Event` is processed as usual except that the proof obligations usually generated are merely assumed.

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 you pay the price of its admission. Note however that you might still have to supply a measure. (Technical note: The measure is used to compute the ``measured subset'' of the formals, which is used when ACL2 does inductions.)

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.