1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
<html>
<head><title>SKIP-PROOFS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>SKIP-PROOFS</h2>skip proofs for a given form -- a quick way to introduce unsoundness
<pre>Major Section: <a href="OTHER.html">OTHER</a>
</pre><p>
<pre>
Example Form:
(skip-proofs
(defun foo (x)
(if (atom x) nil (cons (car x) (foo (reverse (cdr x)))))))<p>
General Form:
(skip-proofs form)
</pre>
where <code>form</code> is processed as usual except that the proof obligations
usually generated are merely assumed.<p>
Normally <code>form</code> is an event; see <a href="EVENTS.html">events</a>. If you want to put
<code>skip-proofs</code> around more than one event, consider the following
(see <a href="PROGN.html">progn</a>): <code>(skip-proofs (progn event1 event2 ... eventk))</code>.<p>
WARNING: Skip-proofs allows inconsistent <a href="EVENTS.html">events</a> to be admitted to
the logic. Use it at your own risk!
<p>
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 <code>skip-proofs</code> 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 <code>skip-proofs</code> useful.<p>
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
<code><a href="DEFUN.html">defun</a></code> event in a <code>skip-proofs</code> you can ``admit'' the
function and experiment with theorems about it before undoing
(see <a href="UBT.html">ubt</a>) 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 <code>(:? v1 ... vk)</code>, where <code>(v1 ... vk)</code> enumerates the
measured subset.<p>
2. You intend eventually to verify the <a href="GUARD.html">guard</a>s for a definition but
do not want to take the time now to pursue that. By embedding the
<code><a href="VERIFY-GUARDS.html">verify-guards</a></code> event in a <code>skip-proofs</code> you can get the system to
behave as though the <a href="GUARD.html">guard</a>s were verified.<p>
3. You are repeatedly recertifying a book while making many
experimental changes. A certain <code><a href="DEFTHM.html">defthm</a></code> 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 <code><a href="DEFTHM.html">defthm</a></code> event in a
<code>skip-proofs</code> you allow the theorem to be assumed without proof
during the experimental recertifications.<p>
4. You are constructing a proof top-down and wish to defer the proof
of a <code><a href="DEFTHM.html">defthm</a></code> until you are convinced of its utility. You can
embed the <code>defthm</code> in a <code>skip-proofs</code>. Of course, you may find
later (when you attempt prove the theorem) that the proposed <code>defthm</code>
is not a theorem.<p>
Unsoundness or Lisp errors may result if the presumptions underlying
a use of <code>skip-proofs</code> are incorrect. Therefore, <code>skip-proofs</code>
must be considered a dangerous (though useful) tool in system
development.<p>
Roughly speaking, a <code><a href="DEFTHM.html">defthm</a></code> embedded in a <code>skip-proofs</code> is
essentially a <code><a href="DEFAXIOM.html">defaxiom</a></code>, except that it is not noted as an axiom
for the purposes of functional instantiation
(see <a href="LEMMA-INSTANCE.html">lemma-instance</a>). But a skipped <code><a href="DEFUN.html">defun</a></code> 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 <code>skip-proofs</code> <a href="EVENTS.html">events</a> are
within the scope of an <code><a href="ENCAPSULATE.html">encapsulate</a></code> 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 <code>skip-proofs</code> should be
regarded as work-in-progress, not as a completed proof with some
unproved assumptions. A <code>skip-proofs</code> event represents a promise
by the author to admit the given event without further axioms. In
other words, <code>skip-proofs</code> should only be used when the belief is
that the proof obligations are indeed theorems in the existing ACL2
logical <a href="WORLD.html">world</a>.<p>
ACL2 allows the certification of <a href="BOOKS.html">books</a> containing <code>skip-proofs</code>
<a href="EVENTS.html">events</a>. This is contrary to the spirit of certified <a href="BOOKS.html">books</a>, since
one is supposedly assured by a valid <a href="CERTIFICATE.html">certificate</a> that a book has
been ``blessed.'' But certification, too, takes the view of
<code>skip-proofs</code> as ``work-in-progress'' and so allows the author of
the book to promise to finish. When such <a href="BOOKS.html">books</a> are certified, a
warning to the author is printed, reminding him or her of the
incurred obligation. When <a href="BOOKS.html">books</a> containing <code>skip-proofs</code> 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 <code>:skip-proofs-okp</code>
is <code>nil</code> in the <code><a href="INCLUDE-BOOK.html">include-book</a></code> form; see <a href="INCLUDE-BOOK.html">include-book</a>.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
