-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcoqrel.Delay.html
329 lines (263 loc) · 29.6 KB
/
coqrel.Delay.html
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
325
326
327
328
329
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<title>coqrel.Delay</title>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Library coqrel.Delay</h1>
<div class="code">
</div>
<div class="doc">
This file implements a tactical <span class="inlinecode"><span class="id" title="var">delaying</span></span> <span class="inlinecode"><span class="id" title="var">tac</span></span> and a tactic
<span class="inlinecode"><a class="idref" href="coqrel.Delay.html#delay"><span class="id" title="definition">delay</span></a></span>, which function in the following way: <span class="inlinecode"><span class="id" title="var">tac</span></span> is able to
invoke <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#delay"><span class="id" title="definition">delay</span></a></span> to solve any subgoal. Assuming the subgoal can be
typed in the context in which <span class="inlinecode"><span class="id" title="var">delaying</span></span> <span class="inlinecode"><span class="id" title="var">tac</span></span> was invoked, the
<span class="inlinecode"><a class="idref" href="coqrel.Delay.html#delay"><span class="id" title="definition">delay</span></a></span> tactic will succeed, and the subgoal will instead become a
subgoal of the encolosing invocation of <span class="inlinecode"><span class="id" title="var">delaying</span></span> <span class="inlinecode"><span class="id" title="var">tac</span></span>.
<div class="paragraph"> </div>
To see why this is useful, consider the way <span class="inlinecode"><span class="id" title="tactic">eauto</span></span> works. Applying
an <span class="inlinecode"><span class="id" title="tactic">eauto</span></span> hint is only considered successful when the generated
subgoal can themselves be solved by <span class="inlinecode"><span class="id" title="tactic">eauto</span></span>. Otherwise, <span class="inlinecode"><span class="id" title="tactic">eauto</span></span>
backtracks and another hint is used. If no hint can be used to solve
the goal completely, then no progress is made.
<div class="paragraph"> </div>
While this behavior is usually appropriate, this means <span class="inlinecode"><span class="id" title="tactic">eauto</span></span>
cannot be used as a base for tactics which make as much progress as
possible, then let the user (or another tactic in a sequence) solve
the remaining subgoals. With the tactics defined below, this can be
accomplished by registering an external hint making use of <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#delay"><span class="id" title="definition">delay</span></a></span>
for strategic subgoals, and invoking <span class="inlinecode"><span class="id" title="var">delaying</span></span> <span class="inlinecode"><span class="id" title="tactic">eauto</span></span>.
<div class="paragraph"> </div>
Additionally, the variant <span class="inlinecode"><span class="id" title="var">delaying_conjunction</span></span> bundles all of the
subgoals solved by <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#delay"><span class="id" title="definition">delay</span></a></span> in a single conjunction of the form
<span class="inlinecode"><a class="idref" href="compcert.lib.Coqlib.html#P1"><span class="id" title="variable">P1</span></a></span> <span class="inlinecode">∧</span> <span class="inlinecode">...</span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" title="var">Pn</span></span> <span class="inlinecode">∧</span> <span class="inlinecode"><a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a></span>. This is useful as it provides a uniform
interface when reifying the effect of a tactic.
<div class="paragraph"> </div>
<a name="lab219"></a><h1 class="section">The <span class="inlinecode"><span class="id" title="var">delayed</span></span>/<span class="inlinecode"><a class="idref" href="coqrel.Delay.html#delay"><span class="id" title="definition">delay</span></a></span> tactics</h1>
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Module</span> <a name="Delay"><span class="id" title="module">Delay</span></a>.<br/>
</div>
<div class="doc">
The <span class="inlinecode"><span class="id" title="var">delaying</span></span> tactical and the <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#delay"><span class="id" title="definition">delay</span></a></span> tactic communicate
through the use of existential variables. Specifically, <span class="inlinecode"><span class="id" title="var">delaying</span></span>
introduces a so-called "open conjunction" to the context. The open
conjunction starts as a hypothesis of type <span class="inlinecode">?<a class="idref" href="compcert.common.Globalenvs.html#Genv.GENV.GLOBALENV_PRINCIPLES.P"><span class="id" title="variable">P</span></a></span>, and remains of
the form <span class="inlinecode"><a class="idref" href="compcert.lib.Coqlib.html#P1"><span class="id" title="variable">P1</span></a></span> <span class="inlinecode">∧</span> <span class="inlinecode">...</span> <span class="inlinecode">∧</span> <span class="inlinecode"><span class="id" title="var">Pn</span></span> <span class="inlinecode">∧</span> <span class="inlinecode">?<a class="idref" href="compcert.lib.Intv.html#FORALL.Q"><span class="id" title="variable">Q</span></a></span> throughout. Each invocation of
<span class="inlinecode"><a class="idref" href="coqrel.Delay.html#delay"><span class="id" title="definition">delay</span></a></span> unifies <span class="inlinecode">?<a class="idref" href="compcert.lib.Intv.html#FORALL.Q"><span class="id" title="variable">Q</span></a></span> with a new node <span class="inlinecode"><span class="id" title="var">Pi</span></span> <span class="inlinecode">∧</span> <span class="inlinecode">?<a class="idref" href="coqrel.RelOperators.html#Q'"><span class="id" title="variable">Q'</span></a></span>. <span class="inlinecode"><span class="id" title="var">Pi</span></span> will be of
the form <span class="inlinecode"><span class="id" title="keyword">∀</span></span> <span class="inlinecode"><a class="idref" href="compcert.lib.Coqlib.html#x1"><span class="id" title="variable">x1</span></a></span> <span class="inlinecode">..</span> <span class="inlinecode"><a class="idref" href="tutorial.queue.AbsQueue.html#xn"><span class="id" title="variable">xn</span></a>,</span> <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#Delay.delayed_goal"><span class="id" title="definition">delayed_goal</span></a></span> <span class="inlinecode"><a class="idref" href="liblayers.lib.Functor.html#G"><span class="id" title="variable">G</span></a></span>, where <span class="inlinecode"><a class="idref" href="liblayers.lib.Functor.html#G"><span class="id" title="variable">G</span></a></span> is the
original goal and the <span class="inlinecode"><span class="id" title="var">xi</span></span>s are the new variables which were
introduced after the open conjunction was created.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">use_conjunction</span> <span class="id" title="var">H</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="var">type</span> <span class="id" title="var">of</span> <span class="id" title="var">H</span> <span class="id" title="keyword">with</span><br/>
| ?<span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> ?<span class="id" title="var">B</span> ⇒<br/>
<span class="id" title="var">use_conjunction</span> (@<a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#proj2"><span class="id" title="lemma">proj2</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">H</span>)<br/>
| <span class="id" title="var">_</span> ⇒<br/>
<span class="id" title="tactic">eapply</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#proj1"><span class="id" title="lemma">proj1</span></a> <span class="id" title="var">H</span>)<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
As much as possible, our open conjunction should remain hidden
from the user's point of view. To avoid interfering with random
tactics such as <span class="inlinecode"><span class="id" title="var">eassumption</span></span>, we wrap it in the following record
type.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Record</span> <a name="Delay.open_conjunction"><span class="id" title="record">open_conjunction</span></a> (<span class="id" title="var">P</span>: <span class="id" title="keyword">Prop</span>) :=<br/>
{<br/>
<a name="Delay.open_conjunction_proj"><span class="id" title="projection">open_conjunction_proj</span></a>: <a class="idref" href="coqrel.Delay.html#P"><span class="id" title="variable">P</span></a><br/>
}.<br/>
<br/>
</div>
<div class="doc">
The evar can only be instantiated to refer to variables that
existed at the point where the evar is spawned. As a consequence,
in order to use it, we must first get rid of all of the new
variables, which the goal potentially depends on. We do this by
reverting the context one variable at a time from the bottom up,
until we hit our <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#Delay.open_conjunction"><span class="id" title="record">open_conjunction</span></a></span>.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">revert_until_conjunction</span> <span class="id" title="var">Hdelayed</span> :=<br/>
<span class="id" title="keyword">match</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| |- <a class="idref" href="coqrel.Delay.html#Delay.open_conjunction"><span class="id" title="record">open_conjunction</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="var">_</span> ⇒<br/>
<span class="id" title="tactic">intro</span> <span class="id" title="var">Hdelayed</span><br/>
| <span class="id" title="var">H</span> : <span class="id" title="var">_</span> |- <span class="id" title="var">_</span> ⇒<br/>
<span class="id" title="var">revert</span> <span class="id" title="var">H</span>;<br/>
<span class="id" title="var">revert_until_conjunction</span> <span class="id" title="var">Hdelayed</span><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
To make sure this operation is reversible, we first wrap the
goal using the following marker.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="Delay.delayed_goal"><span class="id" title="definition">delayed_goal</span></a> (<span class="id" title="var">P</span>: <span class="id" title="keyword">Prop</span>) := <a class="idref" href="coqrel.Delay.html#P"><span class="id" title="variable">P</span></a>.<br/>
<br/>
</div>
<div class="doc">
In some contexts, we actually want a nested saved goal to be
split up further instead. The following marker does that.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="Delay.unpack"><span class="id" title="definition">unpack</span></a> (<span class="id" title="var">P</span>: <span class="id" title="keyword">Prop</span>) := <a class="idref" href="coqrel.Delay.html#P"><span class="id" title="variable">P</span></a>.<br/>
<br/>
</div>
<div class="doc">
Once we're done, we've packaged all of the goals we solved using
<span class="inlinecode"><span class="id" title="var">use_conjunction</span></span> into a single hypothesis. We can use the
following tactic to split up that conjunction into individual
subgoals again.
<div class="paragraph"> </div>
Although we expect the conjunctions produced by <span class="inlinecode"><span class="id" title="var">use_conjunction</span></span>
to be terminated by <span class="inlinecode"><a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a></span> and this should be regarded as the
canonical format, when the last conjunct is a non-<span class="inlinecode"><a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a></span>
proposition we consider it as an additional subgoal. Likewise we
don't require the conclusions to be wrapped in <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#Delay.delayed_goal"><span class="id" title="definition">delayed_goal</span></a></span>.
This allows for some flexibility when dealing with manually
written goals.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">split_conjunction</span> :=<br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">handle_subgoal</span> :=<br/>
<span class="id" title="tactic">intros</span>;<br/>
<span class="id" title="keyword">match</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| |- <a class="idref" href="coqrel.Delay.html#Delay.delayed_goal"><span class="id" title="definition">delayed_goal</span></a> <span class="id" title="var">_</span> ⇒ <span class="id" title="tactic">red</span><br/>
| |- <a class="idref" href="coqrel.Delay.html#Delay.unpack"><span class="id" title="definition">unpack</span></a> <span class="id" title="var">_</span> ⇒ <span class="id" title="tactic">red</span>; <span class="id" title="var">split_conjunction</span><br/>
| |- <span class="id" title="var">_</span> ⇒ <span class="id" title="tactic">idtac</span><br/>
<span class="id" title="keyword">end</span> <span class="id" title="keyword">in</span><br/>
<span class="id" title="keyword">match</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| |- <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <span class="id" title="var">_</span> ⇒ <span class="id" title="tactic">split</span>; [<span class="id" title="var">handle_subgoal</span> | <span class="id" title="var">split_conjunction</span>]<br/>
| |- <span class="id" title="var">_</span> ⇒ <span class="id" title="tactic">exact</span> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#I"><span class="id" title="constructor">I</span></a><br/>
| |- <span class="id" title="var">_</span> ⇒ <span class="id" title="var">handle_subgoal</span><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
Now we can defined <span class="inlinecode"><span class="id" title="var">delayed</span></span>, <span class="inlinecode"><span class="id" title="var">delayed_conjunction</span></span> and <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#delay"><span class="id" title="definition">delay</span></a></span>.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">delay</span> :=<br/>
<span class="id" title="tactic">idtac</span>;<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| <span class="id" title="var">_</span> : <a class="idref" href="coqrel.Delay.html#Delay.open_conjunction"><span class="id" title="record">open_conjunction</span></a> <span class="id" title="var">_</span> |- ?<span class="id" title="var">G</span> ⇒<br/>
<span class="id" title="tactic">change</span> (<a class="idref" href="coqrel.Delay.html#Delay.delayed_goal"><span class="id" title="definition">delayed_goal</span></a> <span class="id" title="var">G</span>);<br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">Hdelayed</span> := <span class="id" title="tactic">fresh</span> "Hdelayed" <span class="id" title="keyword">in</span><br/>
<span class="id" title="var">revert_until_conjunction</span> <span class="id" title="var">Hdelayed</span>;<br/>
<span class="id" title="var">use_conjunction</span> (<a class="idref" href="coqrel.Delay.html#Delay.open_conjunction_proj"><span class="id" title="projection">open_conjunction_proj</span></a> <span class="id" title="var">_</span> <span class="id" title="var">Hdelayed</span>)<br/>
| <span class="id" title="var">_</span> ⇒<br/>
<span class="id" title="tactic">fail</span> "delay can only be used under the 'delayed' tactical"<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">delayed_conjunction</span> <span class="id" title="var">tac</span> :=<br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">Pv</span> := <span class="id" title="tactic">fresh</span> <span class="id" title="keyword">in</span> <span class="id" title="tactic">evar</span> (<span class="id" title="var">Pv</span>: <span class="id" title="keyword">Prop</span>);<br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">P</span> := <span class="id" title="tactic">eval</span> <span class="id" title="tactic">red</span> <span class="id" title="keyword">in</span> <span class="id" title="var">Pv</span> <span class="id" title="keyword">in</span> <span class="id" title="tactic">clear</span> <span class="id" title="var">Pv</span>;<br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">Hdelayed</span> := <span class="id" title="tactic">fresh</span> "Hdelayed" <span class="id" title="keyword">in</span><br/>
<span class="id" title="tactic">cut</span> (<a class="idref" href="coqrel.Delay.html#Delay.open_conjunction"><span class="id" title="record">open_conjunction</span></a> <span class="id" title="var">P</span>);<br/>
[ <span class="id" title="tactic">intro</span> <span class="id" title="var">Hdelayed</span>; <span class="id" title="var">tac</span>; <span class="id" title="tactic">clear</span> <span class="id" title="var">Hdelayed</span> |<br/>
<span class="id" title="tactic">eapply</span> <a class="idref" href="coqrel.Delay.html#Delay.Build_open_conjunction"><span class="id" title="constructor">Build_open_conjunction</span></a> ].<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">delayed</span> <span class="id" title="var">tac</span> :=<br/>
<span class="id" title="var">delayed_conjunction</span> <span class="id" title="var">tac</span>;<br/>
[ .. | <span class="id" title="var">split_conjunction</span> ].<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">undelay</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| <span class="id" title="var">Hdelayed</span> : <a class="idref" href="coqrel.Delay.html#Delay.open_conjunction"><span class="id" title="record">open_conjunction</span></a> <span class="id" title="var">_</span> |- <span class="id" title="var">_</span> ⇒<br/>
<span class="id" title="tactic">clear</span> <span class="id" title="var">Hdelayed</span><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">nondelayed</span> <span class="id" title="var">tac</span> :=<br/>
<span class="id" title="var">undelay</span>; <span class="id" title="var">tac</span>.<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="coqrel.Delay.html#Delay"><span class="id" title="module">Delay</span></a>.<br/>
<br/>
<span class="id" title="keyword">Tactic Notation</span> "delayed" <span class="id" title="var">tactic1</span>(<span class="id" title="var">tac</span>) :=<br/>
<span class="id" title="var">Delay.delayed</span> <span class="id" title="var">tac</span>.<br/>
<br/>
<span class="id" title="keyword">Tactic Notation</span> "nondelayed" <span class="id" title="var">tactic1</span>(<span class="id" title="var">tac</span>) :=<br/>
<span class="id" title="var">Delay.nondelayed</span> <span class="id" title="var">tac</span>.<br/>
<br/>
<span class="id" title="keyword">Tactic Notation</span> "delayed_conjunction" <span class="id" title="var">tactic1</span>(<span class="id" title="var">tac</span>) :=<br/>
<span class="id" title="var">Delay.delayed_conjunction</span> <span class="id" title="var">tac</span>.<br/>
<br/>
<span class="id" title="keyword">Tactic Notation</span> "delay" := <span class="id" title="var">Delay.delay</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab220"></a><h1 class="section">Hints</h1>
<div class="paragraph"> </div>
We hook <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#delay"><span class="id" title="definition">delay</span></a></span> into <span class="inlinecode"><span class="id" title="tactic">eauto</span></span> in two different ways: subgoals
intended to be delayed can be marked with the wrapper below.
Alternately, one can use the <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#delay"><span class="id" title="definition">delay</span></a></span> hint database, which provides a
low-priority delay rule.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="delay"><span class="id" title="definition">delay</span></a> (<span class="id" title="var">P</span>: <span class="id" title="keyword">Prop</span>) := <a class="idref" href="coqrel.Delay.html#P"><span class="id" title="variable">P</span></a>.<br/>
<br/>
<span class="id" title="keyword">Hint Extern</span> 0 (<a class="idref" href="coqrel.Delay.html#delay"><span class="id" title="definition">delay</span></a> <span class="id" title="var">_</span>) ⇒ <span class="id" title="var">delay</span>.<br/>
<br/>
<span class="id" title="keyword">Hint Extern</span> 100 ⇒ <span class="id" title="var">delay</span> : <span class="id" title="var">delay</span>.<br/>
<br/>
</div>
<div class="doc">
This typeclass wrapper is convenient for performing a nested
search outside of a potential "delayed" context.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Class</span> <a name="NonDelayed"><span class="id" title="record">NonDelayed</span></a> (<span class="id" title="var">P</span>: <span class="id" title="keyword">Prop</span>) :=<br/>
<a name="nondelayed"><span class="id" title="projection">nondelayed</span></a> : <a class="idref" href="coqrel.Delay.html#P"><span class="id" title="variable">P</span></a>.<br/>
<br/>
<span class="id" title="keyword">Hint Extern</span> 1 (<a class="idref" href="coqrel.Delay.html#NonDelayed"><span class="id" title="class">NonDelayed</span></a> <span class="id" title="var">_</span>) ⇒<br/>
<span class="id" title="tactic">red</span>; <span class="id" title="tactic">try</span> <span class="id" title="var">Delay.undelay</span> : <span class="id" title="var">typeclass_instances</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab221"></a><h1 class="section">Example: reifying <span class="inlinecode"><span class="id" title="tactic">eapply</span></span></h1>
<div class="paragraph"> </div>
To demonstrate how <span class="inlinecode"><span class="id" title="var">delayed_conjunction</span></span> can be used to reify a
tactic into a typeclass, we define the <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#EApply"><span class="id" title="record">EApply</span></a></span> typeclass. An
instance of <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#EApply"><span class="id" title="record">EApply</span></a></span> <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#HT"><span class="id" title="variable">HT</span></a></span> <span class="inlinecode"><a class="idref" href="compcert.common.Globalenvs.html#Genv.GENV.GLOBALENV_PRINCIPLES.P"><span class="id" title="variable">P</span></a></span> <span class="inlinecode"><a class="idref" href="compcert.lib.Intv.html#FORALL.Q"><span class="id" title="variable">Q</span></a></span> expresses that if <span class="inlinecode"><a class="idref" href="compcert.flocq.Core.Fcore_generic_fmt.html#H"><span class="id" title="variable">H</span></a></span> is a hypothesis of
type <span class="inlinecode"><a class="idref" href="coqrel.Delay.html#HT"><span class="id" title="variable">HT</span></a></span>, then invoking <span class="inlinecode"><span class="id" title="tactic">eapply</span></span> <span class="inlinecode"><a class="idref" href="compcert.flocq.Core.Fcore_generic_fmt.html#H"><span class="id" title="variable">H</span></a></span> on a goal of type <span class="inlinecode"><a class="idref" href="compcert.lib.Intv.html#FORALL.Q"><span class="id" title="variable">Q</span></a></span> will
generate the subgoal conjunction <span class="inlinecode"><a class="idref" href="compcert.common.Globalenvs.html#Genv.GENV.GLOBALENV_PRINCIPLES.P"><span class="id" title="variable">P</span></a></span>.
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Class</span> <a name="EApply"><span class="id" title="record">EApply</span></a> (<span class="id" title="var">HT</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</span>: <span class="id" title="keyword">Prop</span>) :=<br/>
<a name="eapply"><span class="id" title="projection">eapply</span></a> : <a class="idref" href="coqrel.Delay.html#HT"><span class="id" title="variable">HT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="coqrel.Delay.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.6/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="coqrel.Delay.html#Q"><span class="id" title="variable">Q</span></a>.<br/>
<br/>
<span class="id" title="keyword">Hint Extern</span> 1 (<a class="idref" href="coqrel.Delay.html#EApply"><span class="id" title="class">EApply</span></a> ?<span class="id" title="var">HT</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span>) ⇒<br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">H</span> := <span class="id" title="tactic">fresh</span> <span class="id" title="keyword">in</span><br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">HP</span> := <span class="id" title="tactic">fresh</span> "HP" <span class="id" title="keyword">in</span><br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">H</span> <span class="id" title="var">HP</span>;<br/>
<span class="id" title="var">delayed_conjunction</span> <span class="id" title="tactic">solve</span> [<span class="id" title="tactic">eapply</span> <span class="id" title="var">H</span>; <span class="id" title="var">delay</span>];<br/>
<span class="id" title="tactic">eexact</span> <span class="id" title="var">HP</span> :<br/>
<span class="id" title="var">typeclass_instances</span>.<br/>
</div>
</div>
<div id="footer">
<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>