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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
|
<html>
<head><title>PROOF-TREE-EXAMPLES.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>PROOF-TREE-EXAMPLES</h2>proof tree example
<pre>Major Section: <a href="PROOF-TREE.html">PROOF-TREE</a>
</pre><p>
See <a href="PROOF-TREE.html">proof-tree</a> for an introduction to proof trees, and for a
list of related topics. Here we present a detailed example followed
by a shorter example that illustrates proof by induction.
<p>
Consider the <a href="GUARD.html">guard</a> proof for the definition of a function
<code>cancel_equal_plus</code>; the body of this definition is of no importance
here. The first proof tree display is:
<pre>
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
| <18 subgoals>
</pre>
This is to be read as follows.
<blockquote>
At this stage of the proof we have encountered the top-level goal,
named "Goal", which generated 18 subgoals using the
``preprocess'' process. We have not yet begun to work on those
subgoals.
</blockquote>
The corresponding message from the ordinary prover output is:
<blockquote>
By case analysis we reduce the conjecture to the following 18
conjectures.
</blockquote>
Note that the field just before the name of the goal (<code>"Goal"</code>),
which here contains the number 18, indicates the number of cases
(children) created by the goal using the indicated process. This
number will remain unchanged as long as this goal is displayed.<p>
The next proof tree display is:
<pre>
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
1 | Subgoal 18 simp
| | <1 subgoal>
| <17 more subgoals>
</pre>
which indicates that at this point, the prover has used the
simplification (``simp'') process on Subgoal 18 to create one
subgoal (``<1 subgoal>''). The vertical bar (``|'') below ``Subgoal
18'', accompanied by the line below it, signifies that there are 17
siblings of Subgoal 18 that remain to be processed.<p>
The next proof tree displayed is:
<pre>
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
1 | Subgoal 18 simp
c 2 | | Subgoal 18' ELIM
| | | <2 subgoals>
| <17 more subgoals>
</pre>
Let us focus on the fourth line of this display:
<pre>
c 2 | | Subgoal 18' ELIM
</pre>
The ``c'' field marks this goal as a ``checkpoint'', i.e., a goal
worthy of careful scrutiny. In fact, any goal that creates children
by a process other than ``preprocess'' or ``simp'' is marked as a
checkpoint. In this case, the destructor-elimination (``<a href="ELIM.html">ELIM</a>'')
process has been used to create subgoals of this goal. The
indentation shows that this goal, Subgoal 18', is a child of Subgoal
18. The number ``2'' indicates that 2 subgoals have been created
(by <a href="ELIM.html">ELIM</a>). Note that this information is consistent with the line
just below it, which says ``<2 subgoals>''.<p>
Finally, the last line of this proof tree display,
<pre>
| <17 more subgoals>
</pre>
is connected by vertical bars (``|'') up to the string
<code>"Subgoal 18"</code>, which suggests that there are 17 immediate
subgoals of Goal remaining to process after Subgoal 18. Note that
this line is indented one level from the second line, which is the
line for the goal named <code>"Goal"</code>. The display is intended to
suggest that the subgoals of Goal that remain to be proved consist
of Subgoal 18 together with 17 more subgoals.<p>
The next proof tree display differs from the previous one only in
that now, Subgoal 18' has only one more subgoal to be processed.
<pre>
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
1 | Subgoal 18 simp
c 2 | | Subgoal 18' ELIM
| | | <1 more subgoal>
| <17 more subgoals>
</pre>
Note that the word ``more'' in ``<1 more subgoal>'' tells us that
there was originally more than one subgoal of Subgoal 18. In fact
that information already follows from the line above, which (as
previously explained) says that Subgoal 18' originally created 2
subgoals.<p>
The next proof tree display occurs when the prover completes the
proof of that ``1 more subgoal'' referred to above.
<pre>
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
| <17 more subgoals>
</pre>
Then, Subgoal 17 is processed and creates one subgoal, by
simplification:
<pre>
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
1 | Subgoal 17 simp
| | <1 subgoal>
| <16 more subgoals>
</pre>
... and so on.<p>
Later in the proof one might find the following successive proof
tree displays.
<pre>
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
| <9 more subgoals><p>
( DEFUN CANCEL_EQUAL_PLUS ...)<p>
18 Goal preprocess
0 | Subgoal 9 simp (FORCED)
| <8 more subgoals>
</pre>
These displays tell us that Subgoal 9 simplified to <code>t</code> (note that
the ``0'' shows clearly that no subgoals were created), but that
some rule's hypotheses were <a href="FORCE.html">force</a>d. Although this goal is not
checkpointed (i.e., no ``c'' appears on the left margin), one can
cause such goals to be checkpointed;
see <a href="CHECKPOINT-FORCED-GOALS.html">checkpoint-forced-goals</a>.<p>
In fact, the proof tree displayed at the end of the ``main proof''
(the 0-th forcing round) is as follows.
<pre>
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
0 | Subgoal 9 simp (FORCED)
0 | Subgoal 8 simp (FORCED)
0 | Subgoal 7 simp (FORCED)
0 | Subgoal 6 simp (FORCED)
0 | Subgoal 4 simp (FORCED)
0 | Subgoal 3 simp (FORCED)
</pre>
This is followed by the following proof tree display at the start
of the forcing round.
<pre>
18 Goal preprocess
0 | Subgoal 9 simp (FORCED [1]Subgoal 4)
0 | Subgoal 8 simp (FORCED [1]Subgoal 6)
0 | Subgoal 7 simp (FORCED [1]Subgoal 1)
0 | Subgoal 6 simp (FORCED [1]Subgoal 3)
0 | Subgoal 4 simp (FORCED [1]Subgoal 5)
0 | Subgoal 3 simp (FORCED [1]Subgoal 2)
++++++++++++++++++++++++++++++
6 [1]Goal FORCING-ROUND
2 | [1]Subgoal 6 preprocess
| | <2 subgoals>
| <5 more subgoals>
</pre>
This display shows which goals to ``blame'' for the existence of
each goal in the forcing round. For example, Subgoal 9 is to blame
for the creation of [1]Subgoal 4.<p>
Actually, there is no real goal named <code>"[1]Goal"</code>. However, the
line
<pre>
6 [1]Goal FORCING-ROUND
</pre>
appears in the proof tree display to suggest a ``parent'' of the
six top-level goals in that forcing round. As usual, the numeric
field before the goal name contains the original number of children
of that (virtual, in this case) goal -- in this case, 6.<p>
In our example proof, Subgoal 6 eventually gets proved, without
doing any further forcing. At that point, the proof tree display
looks as follows.
<pre>
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
0 | Subgoal 9 simp (FORCED [1]Subgoal 4)
0 | Subgoal 7 simp (FORCED [1]Subgoal 1)
0 | Subgoal 6 simp (FORCED [1]Subgoal 3)
0 | Subgoal 4 simp (FORCED [1]Subgoal 5)
0 | Subgoal 3 simp (FORCED [1]Subgoal 2)
++++++++++++++++++++++++++++++
6 [1]Goal FORCING-ROUND
| <5 more subgoals>
</pre>
Notice that the line for Subgoal 8,
<pre>
0 | Subgoal 8 simp (FORCED [1]Subgoal 6)
</pre>
no longer appears. That is because the goal [1]Subgoal 6 has been
proved, along with all its children; and hence, the proof of Subgoal
8 no longer depends on any further reasoning.<p>
The final two proof tree displays in our example are as follows.
<pre>
( DEFUN CANCEL_EQUAL_PLUS ...)
18 Goal preprocess
0 | Subgoal 7 simp (FORCED [1]Subgoal 1)
++++++++++++++++++++++++++++++
6 [1]Goal FORCING-ROUND
2 | [1]Subgoal 1 preprocess
1 | | [1]Subgoal 1.1 preprocess
1 | | | [1]Subgoal 1.1' simp
c 3 | | | | [1]Subgoal 1.1'' ELIM
| | | | | <1 more subgoal><p>
( DEFUN CANCEL_EQUAL_PLUS ...)
<<PROOF TREE IS EMPTY>>
</pre>
The explanation for the empty proof tree is simple: once
[1]Subgoal 1.1.1 was proved, nothing further remained to be proved.
In fact, the much sought-after ``Q.E.D.'' appeared shortly after the
final proof tree was displayed.<p>
Let us conclude with a final, brief example that illustrates proof
by induction. Partway through the proof one might come across the
following proof tree display.
<pre>
( DEFTHM PLUS-TREE-DEL ...)
1 Goal preprocess
2 | Goal' simp
c 0 | | Subgoal 2 PUSH *1
| | <1 more subgoal>
</pre>
This display says that in the attempt to prove a theorem called
<code>plus-tree-del</code>, preprocessing created the only child Goal' from Goal,
and Goal' simplified to two subgoals. Subgoal 2 is immediately
pushed for proof by induction, under the name ``*1''. In fact if
Subgoal 1 simplifies to <code>t</code>, then we see the following successive
proof tree displays after the one shown above.
<pre>
( DEFTHM PLUS-TREE-DEL ...)
1 Goal preprocess
2 | Goal' simp
c 0 | | Subgoal 2 PUSH *1<p>
( DEFTHM PLUS-TREE-DEL ...)
1 Goal preprocess
2 | Goal' simp
c 0 | | Subgoal 2 PUSH *1
++++++++++++++++++++++++++++++
c 6 *1 INDUCT
| <5 more subgoals>
</pre>
The separator ``+++++...'' says that we are beginning another trip
through the waterfall. In fact this trip is for a proof by
induction (as opposed to a forcing round), as indicated by the word
``INDUCT''. Apparently *1.6 was proved immediately, because it was
not even displayed; a goal is only displayed when there is some work
left to do either on it or on some goal that it brought (perhaps
indirectly) into existence.<p>
Once a proof by induction is completed, the ``PUSH'' line that
refers to that proof is eliminated (``pruned''). So for example,
when the present proof by induction is completed, the line
<pre>
c 0 | | Subgoal 2 PUSH *1
</pre>
is eliminated, which in fact causes the lines above it to be
eliminated (since they no longer refer to unproved children).
Hence, at that point one might expect to see:
<pre>
( DEFTHM PLUS-TREE-DEL ...)
<<PROOF TREE IS EMPTY>>
</pre>
However, if the proof by induction of *1 necessitates further
proofs by induction or a forcing round, then this ``pruning'' will
not yet be done.
<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>
|
