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
|
<html>
<head><title>FORCING-ROUND.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>FORCING-ROUND</h2>a section of a proof dealing with <a href="FORCE.html">force</a>d assumptions
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
If ACL2 ``<a href="FORCE.html">force</a>s'' some hypothesis of some rule to be true, it is
obliged later to prove the hypothesis. See <a href="FORCE.html">force</a>. ACL2 delays
the consideration of <a href="FORCE.html">force</a>d hypotheses until the main goal has been
proved. It then undertakes a new round of proofs in which the main
goal is essentially the conjunction of all hypotheses <a href="FORCE.html">force</a>d in the
preceding proof. Call this round of proofs the ``Forcing Round.''
Additional hypotheses may be <a href="FORCE.html">force</a>d by the proofs in the Forcing
Round. The attempt to prove these hypotheses is delayed until the
Forcing Round has been successfully completed. Then a new Forcing
Round is undertaken to prove the recently <a href="FORCE.html">force</a>d hypotheses and this
continues until no hypotheses are <a href="FORCE.html">force</a>d. Thus, there is a
succession of Forcing Rounds.
<p>
The Forcing Rounds are enumerated starting from 1. The Goals and
Subgoals of a Forcing Round are printed with the round's number
displayed in square brackets. Thus, <code>"[1]Subgoal 1.3"</code> means that
the goal in question is Subgoal 1.3 of the 1st forcing round. To
supply a hint for use in the proof of that subgoal, you should use
the goal specifier <code>"[1]Subgoal 1.3"</code>. See <a href="GOAL-SPEC.html">goal-spec</a>.<p>
When a round is successfully completed -- and for these purposes you
may think of the proof of the main goal as being the 0th forcing
round -- the system collects all of the assumptions <a href="FORCE.html">force</a>d by the
just-completed round. Here, an assumption should be thought of as
an implication, <code>(implies context hyp)</code>, where context describes the
context in which hyp was assumed true. Before undertaking the
proofs of these assumptions, we try to ``clean them up'' in an
effort to reduce the amount of work required. This is often
possible because the <a href="FORCE.html">force</a>d assumptions are generated by the same
rule being applied repeatedly in a given context.<p>
For example, suppose the main goal is about some term
<code>(pred (xtrans i) i)</code> and that some rule rewriting <code>pred</code> contains a
<a href="FORCE.html">force</a>d hypothesis that the first argument is a <code>good-inputp</code>.
Suppose that during the proof of Subgoal 14 of the main goal,
<code>(good-inputp (xtrans i))</code> is <a href="FORCE.html">force</a>d in a context in which <code>i</code> is
an <code><a href="INTEGERP.html">integerp</a></code> and <code>x</code> is a <code><a href="CONSP.html">consp</a></code>. (Note that <code>x</code> is
irrelevant.) Suppose finally that during the proof of Subgoal 28,
<code>(good-inputp (xtrans i))</code> is <a href="FORCE.html">force</a>d ``again,'' but this time in a
context in which <code>i</code> is a <code><a href="RATIONALP.html">rationalp</a></code> and <code>x</code> is a <code><a href="SYMBOLP.html">symbolp</a></code>.
Since the <a href="FORCE.html">force</a>d hypothesis does not mention <code>x</code>, we deem the
contextual information about <code>x</code> to be irrelevant and discard it
from both contexts. We are then left with two <a href="FORCE.html">force</a>d assumptions:
<code>(implies (integerp i) (good-inputp (xtrans i)))</code> from Subgoal 14,
and <code>(implies (rationalp i) (good-inputp (xtrans i)))</code> from Subgoal
28. Note that if we can prove the assumption required by Subgoal 28
we can easily get that for Subgoal 14, since the context of Subgoal
28 is the more general. Thus, in the next forcing round we will
attempt to prove just
<pre>
(implies (rationalp i) (good-inputp (xtrans i)))
</pre>
and ``blame'' both Subgoal 14 and Subgoal 28 of the previous round
for causing us to prove this.<p>
By delaying and collecting the <code>forced</code> assumptions until the
completion of the ``main goal'' we gain two advantages. First, the
user gets confirmation that the ``gist'' of the proof is complete
and that all that remains are ``technical details.'' Second, by
delaying the proofs of the <a href="FORCE.html">force</a>d assumptions ACL2 can undertake the
proof of each assumption only once, no matter how many times it was
<a href="FORCE.html">force</a>d in the main goal.<p>
In order to indicate which proof steps of the previous round were
responsible for which <a href="FORCE.html">force</a>d assumptions, we print a sentence
explaining the origins of each newly <a href="FORCE.html">force</a>d goal. For example,
<pre>
[1]Subgoal 1, below, will focus on
(GOOD-INPUTP (XTRANS I)),
which was forced in
Subgoal 14, above,
by applying (:REWRITE PRED-CRUNCHER) to
(PRED (XTRANS I) I),
and
Subgoal 28, above,
by applying (:REWRITE PRED-CRUNCHER) to
(PRED (XTRANS I) I).
</pre>
<p>
In this entry, ``[1]Subgoal 1'' is the name of a goal which will be
proved in the next forcing round. On the next line we display the
<a href="FORCE.html">force</a>d hypothesis, call it <code>x</code>, which is
<code>(good-inputp (xtrans i))</code> in this example. This term will be the
conclusion of the new subgoal. Since the new subgoal will be
printed in its entirety when its proof is undertaken, we do not here
exhibit the context in which <code>x</code> was <a href="FORCE.html">force</a>d. The sentence then
lists (possibly a succession of) a goal name from the just-completed
round and some step in the proof of that goal that <a href="FORCE.html">force</a>d <code>x</code>. In
the example above we see that Subgoals 14 and 28 of the
just-completed proof <a href="FORCE.html">force</a>d <code>(good-inputp (xtrans i))</code> by applying
<code>(:rewrite pred-cruncher)</code> to the term <code>(pred (xtrans i) i)</code>.<p>
If one were to inspect the theorem prover's description of the proof
steps applied to Subgoals 14 and 28 one would find the word
``<a href="FORCE.html">force</a>d'' (or sometimes ``forcibly'') occurring in the commentary.
Whenever you see that word in the output, you know you will get a
subsequent forcing round to deal with the hypotheses <a href="FORCE.html">force</a>d.
Similarly, if at the beginning of a forcing round a <a href="RUNE.html">rune</a> is blamed
for causing a <a href="FORCE.html">force</a> in some subgoal, inspection of the commentary
for that subgoal will reveal the word ``<a href="FORCE.html">force</a>d'' after the rule name
blamed.<p>
Most <a href="FORCE.html">force</a>d hypotheses come from within the prover's simplifier.
When the simplifier encounters a hypothesis of the form <code>(force hyp)</code>
it first attempts to establish it by rewriting <code>hyp</code> to, say, <code>hyp'</code>.
If the truth or falsity of <code>hyp'</code> is known, forcing is not required.
Otherwise, the simplifier actually <a href="FORCE.html">force</a>s <code>hyp'</code>. That is, the <code>x</code>
mentioned above is <code>hyp'</code>, not <code>hyp</code>, when the <a href="FORCE.html">force</a>d subgoal was
generated by the simplifier.<p>
Once the system has printed out the origins of the newly <a href="FORCE.html">force</a>d
goals, it proceeds to the next forcing round, where those goals are
individually displayed and attacked.<p>
At the beginning of a forcing round, the <a href="ENABLE.html">enable</a>d structure defaults
to the global <a href="ENABLE.html">enable</a>d structure. For example, suppose some <a href="RUNE.html">rune</a>,
<code>rune</code>, is globally <a href="ENABLE.html">enable</a>d. Suppose in some event you <a href="DISABLE.html">disable</a> the
<a href="RUNE.html">rune</a> at <code>"Goal"</code> and successfully prove the goal but <a href="FORCE.html">force</a> <code>"[1]Goal"</code>.
Then during the proof of <code>"[1]Goal"</code>, <a href="RUNE.html">rune</a> is <a href="ENABLE.html">enable</a>d ``again.'' The
right way to think about this is that the <a href="RUNE.html">rune</a> is ``still'' <a href="ENABLE.html">enable</a>d.
That is, it is <a href="ENABLE.html">enable</a>d globally and each forcing round resumes with
the global <a href="ENABLE.html">enable</a>d structure.
<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>
|
