Skip-proofs
Skip proofs for a given form — a quick way to introduce unsoundness
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: The use of skip-proofs carries an implicit promise by
the user that the ensuing proof obligations are indeed theorems of the current
theory. When that is not the case, skip-proofs can even allow
inconsistent events to be admitted to the logic. Use it at your own
risk! If your intention is truly to extend the current logical theory,
consider using defaxiom instead.
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.
