forked from Coq-zh/SF-zh
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Maps.html
566 lines (469 loc) · 84.1 KB
/
Maps.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
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
<!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="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>Maps: 全映射与偏映射</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<div id="page">
<div id="header">
<div id='logoinheader'><a href='https://coq-zh.github.io/SF-zh/'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 1: 逻辑基础</a></div>
<ul id='menu'>
<li class='section_name'><a href='toc.html'>目录</a></li>
<li class='section_name'><a href='coqindex.html'>索引</a></li>
<li class='section_name'><a href='deps.html'>路线</a></li>
</ul>
</div>
<div id="main">
<h1 class="libtitle">Maps<span class="subtitle">全映射与偏映射</span></h1>
<div class="code">
</div>
<div class="doc">
<div class="paragraph"> </div>
<i>'映射（Map）'</i>（或<i>'字典（Dictionary）'</i>）是一种非常普遍的数据结构，
在编程语言理论中尤甚，而之后的章节中我们会多次用到它。
映射也适合运用之前学过的概念进行研究，包括如何在高阶函数之外构建数据结构
（见 <span class="inlinecode"><span class="id" title="var">Basics</span></span> 和 <span class="inlinecode"><span class="id" title="var">Poly</span></span>）以及通过互映来精简证明（见 <span class="inlinecode"><span class="id" title="var">IndProp</span></span>）。
<div class="paragraph"> </div>
我们会定义两种映射：在查找的键不存在时，<i>'全映射'</i>会返回“默认”元素，
而<i>'偏映射'</i>则会返回一个 <span class="inlinecode"><span class="id" title="var">option</span></span> 来指示成功还是失败。后者根据前者来定义，
它使用 <span class="inlinecode"><span class="id" title="var">None</span></span> 默认元素。
</div>
<div class="doc">
<a name="lab255"></a><h1 class="section">Coq 标准库</h1>
<div class="paragraph"> </div>
开始前的小插话...
<div class="paragraph"> </div>
和我们目前学过的章节不同，本章无需通过 <span class="inlinecode"><span class="id" title="keyword">Require</span></span> <span class="inlinecode"><span class="id" title="keyword">Import</span></span> 导入之前的章节
（自然也就不会间接导入更早的章节）。从本章开始，我们我们将直接从
Coq 标准库中导入需要的定义和定理。然而应该不会注意到多大差别，
因为我们一直小心地将自己的定义和定理的命名与标准库中的部分保持一致，
无论它们在哪里重复。
</div>
<div class="code">
<br/>
<span class="id" title="var">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Arith.Arith.html#"><span class="id" title="library">Arith.Arith</span></a>.<br/>
<span class="id" title="var">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Bool.Bool.html#"><span class="id" title="library">Bool.Bool</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#"><span class="id" title="library">Coq.Strings.String</span></a>.<br/>
<span class="id" title="var">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Logic.FunctionalExtensionality.html#"><span class="id" title="library">Logic.FunctionalExtensionality</span></a>.<br/>
<span class="id" title="var">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#"><span class="id" title="library">Lists.List</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">ListNotations</span>.<br/>
</div>
<div class="doc">
标准库的文档见
<a href="https://coq.inria.fr/library/">https://coq.inria.fr/library/</a>。
<div class="paragraph"> </div>
<span class="inlinecode"><span class="id" title="keyword">Search</span></span> 指令可用于查找涉及具体类型对象的定理。我们花点时间来熟悉一下它。
</div>
<div class="doc">
<a name="lab256"></a><h1 class="section">标识符</h1>
<div class="paragraph"> </div>
首先我们需要键的类型来对映射进行索引。在 <span class="inlinecode"><span class="id" title="var">Lists.v</span></span> 中，
我们为类似的目的引入了 <span class="inlinecode"><span class="id" title="var">id</span></span> 类型。而在<i>'《软件基础》'</i>后面的部分，
我们会使用 Coq 标准库中的 <span class="inlinecode"><span class="id" title="var">string</span></span> 类型。
<div class="paragraph"> </div>
为了比较字符串，我们定义了 <span class="inlinecode"><span class="id" title="var">eqb_string</span></span> 函数，它在内部使用 Coq
字符串库中的 <span class="inlinecode"><span class="id" title="var">string_dec</span></span> 函数。
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="eqb_string"><span class="id" title="definition">eqb_string</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/>
<span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string_dec"><span class="id" title="definition">string_dec</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#y"><span class="id" title="variable">y</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
</div>
<div class="doc">
（函数 <span class="inlinecode"><span class="id" title="var">string_dec</span></span> 来自于 Coq 的字符串标准库。如果你查看
<span class="inlinecode"><span class="id" title="var">string_dec</span></span> 的结果类型，就会发现其返回值的类型并不是 <span class="inlinecode"><span class="id" title="var">bool</span></span>，
而是一个形如 <span class="inlinecode">{<span class="id" title="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">y</span>}</span> <span class="inlinecode">+</span> <span class="inlinecode">{<span class="id" title="var">x</span></span> <span class="inlinecode">≠</span> <span class="inlinecode"><span class="id" title="var">y</span>}</span> 的类型，叫做 <span class="inlinecode"><span class="id" title="var">sumbool</span></span> 类型，
它可以看做“带有证据的布尔类型”。形式上来说，一个 <span class="inlinecode">{<span class="id" title="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">y</span>}</span> <span class="inlinecode">+</span> <span class="inlinecode">{<span class="id" title="var">x</span></span> <span class="inlinecode">≠</span> <span class="inlinecode"><span class="id" title="var">y</span>}</span>
类型的元素要么是 <span class="inlinecode"><span class="id" title="var">x</span></span> 和 <span class="inlinecode"><span class="id" title="var">y</span></span> 的相等的证明，要么就是它们不相等的证明，
与一个标签一起来指出具体是哪一个。不过就目前来说，你可以把它当做一个
花哨的 <span class="inlinecode"><span class="id" title="var">bool</span></span>。）
<div class="paragraph"> </div>
现在我们需要一些关于字符串相等性的基本性质...
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a name="eqb_string_refl"><span class="id" title="lemma">eqb_string_refl</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>, <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Maps.html#eqb_string"><span class="id" title="definition">eqb_string</span></a> <a class="idref" href="Maps.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="Maps.html#s"><span class="id" title="variable">s</span></a>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">s</span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="Maps.html#eqb_string"><span class="id" title="definition">eqb_string</span></a>.<br/>
<span class="id" title="tactic">destruct</span> (<a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string_dec"><span class="id" title="definition">string_dec</span></a> <span class="id" title="var">s</span> <span class="id" title="var">s</span>) <span class="id" title="keyword">as</span> [<span class="id" title="var">Hs_eq</span> | <span class="id" title="var">Hs_not_eq</span>].<br/>
- <span class="id" title="tactic">reflexivity</span>.<br/>
- <span class="id" title="tactic">destruct</span> <span class="id" title="var">Hs_not_eq</span>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>
<div class="doc">
两个字符串在 <span class="inlinecode"><span class="id" title="var">eqb_string</span></span> 的意义上相等，当且仅当它们在
<span class="inlinecode">=</span> 的意义上相等。因此 <span class="inlinecode"><span class="id" title="var">eqb_string</span></span> 中反映了 <span class="inlinecode">=</span>，<a href="IndProp.html"><span class="inlineref">IndProp</span></a>
一章中讨论了「互映」的意义。
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Theorem</span> <a name="eqb_string_true_iff"><span class="id" title="lemma">eqb_string_true_iff</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>,<br/>
<a class="idref" href="Maps.html#eqb_string"><span class="id" title="definition">eqb_string</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">↔</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Maps.html#y"><span class="id" title="variable">y</span></a>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>.<br/>
<span class="id" title="tactic">unfold</span> <a class="idref" href="Maps.html#eqb_string"><span class="id" title="definition">eqb_string</span></a>.<br/>
<span class="id" title="tactic">destruct</span> (<a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string_dec"><span class="id" title="definition">string_dec</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) <span class="id" title="keyword">as</span> [<span class="id" title="var">Hs_eq</span> | <span class="id" title="var">Hs_not_eq</span>].<br/>
- <span class="id" title="tactic">rewrite</span> <span class="id" title="var">Hs_eq</span>. <span class="id" title="tactic">split</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="tactic">reflexivity</span>.<br/>
- <span class="id" title="tactic">split</span>.<br/>
+ <span class="id" title="tactic">intros</span> <span class="id" title="var">contra</span>. <span class="id" title="tactic">discriminate</span> <span class="id" title="var">contra</span>.<br/>
+ <span class="id" title="tactic">intros</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">H</span> <span class="id" title="tactic">in</span> <span class="id" title="var">Hs_not_eq</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">Hs_not_eq</span>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>
<div class="doc">
类似地：
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Theorem</span> <a name="eqb_string_false_iff"><span class="id" title="lemma">eqb_string_false_iff</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>,<br/>
<a class="idref" href="Maps.html#eqb_string"><span class="id" title="definition">eqb_string</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">↔</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc<sub>9</sub>"><span class="id" title="notation">≠</span></a> <a class="idref" href="Maps.html#y"><span class="id" title="variable">y</span></a>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>. <span class="id" title="tactic">rewrite</span> <- <a class="idref" href="Maps.html#eqb_string_true_iff"><span class="id" title="lemma">eqb_string_true_iff</span></a>.<br/>
<span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Bool.Bool.html#not_true_iff_false"><span class="id" title="lemma">not_true_iff_false</span></a>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>
<div class="doc">
以下便于使用的变体只需通过改写就能得出：
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Theorem</span> <a name="false_eqb_string"><span class="id" title="lemma">false_eqb_string</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>,<br/>
<a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc<sub>9</sub>"><span class="id" title="notation">≠</span></a> <a class="idref" href="Maps.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Maps.html#eqb_string"><span class="id" title="definition">eqb_string</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="Maps.html#eqb_string_false_iff"><span class="id" title="lemma">eqb_string_false_iff</span></a>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">H</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
<span class="comment">(* /HIDEFROMHTML *)</span><br/>
</div>
<div class="doc">
<a name="lab257"></a><h1 class="section">全映射</h1>
<div class="paragraph"> </div>
在本章中，我们的主要任务就是构建一个偏映射的定义，其行为类似于我们之前在
<a href="Lists.html"><span class="inlineref">Lists</span></a> 一章中看到的那个，再加上伴随其行为的引理。
<div class="paragraph"> </div>
不过这一次，我们将使用<i>'函数'</i>而非“键-值”对的列表来构建映射。
这种表示方法的优点在于它提供了映射更具<i>'外延性'</i>的视角，
即以相同方式回应查询的两个映射将被表示为完全相同的东西（即一模一样的函数），
而非只是“等价”的数据结构。这反过来简化了使用映射的证明。
<div class="paragraph"> </div>
我们会分两步构建偏映射。首先，我们定义一个<i>'全映射'</i>类型，
它在某个映射中查找不存在的键时会返回默认值。
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="total_map"><span class="id" title="definition">total_map</span></a> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>.<br/>
</div>
<div class="doc">
直观上来说，一个元素类型为 <span class="inlinecode"><span class="id" title="var">A</span></span> 的全映射不过就是个根据 <span class="inlinecode"><span class="id" title="var">string</span></span>
来查找 <span class="inlinecode"><span class="id" title="var">A</span></span> 的函数。
<div class="paragraph"> </div>
给定函数 <span class="inlinecode"><span class="id" title="var">t_empty</span></span> 一个默认元素，它会产生一个空的全映射。
此映射在应用到任何字符串时都会返回默认元素。
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="t_empty"><span class="id" title="definition">t_empty</span></a> {<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>} (<span class="id" title="var">v</span> : <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>) : <a class="idref" href="Maps.html#total_map"><span class="id" title="definition">total_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a> :=<br/>
(<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a>).<br/>
</div>
<div class="doc">
更有趣的是 <span class="inlinecode"><span class="id" title="var">update</span></span> 函数，它和之前一样，接受一个映射 <span class="inlinecode"><span class="id" title="var">m</span></span>、一个键 <span class="inlinecode"><span class="id" title="var">x</span></span>
以及一个值 <span class="inlinecode"><span class="id" title="var">v</span></span>，并返回一个将 <span class="inlinecode"><span class="id" title="var">x</span></span> 映射到 <span class="inlinecode"><span class="id" title="var">v</span></span> 的新映射；其它键则与
<span class="inlinecode"><span class="id" title="var">m</span></span> 中原来的保持一致。
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="t_update"><span class="id" title="definition">t_update</span></a> {<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>} (<span class="id" title="var">m</span> : <a class="idref" href="Maps.html#total_map"><span class="id" title="definition">total_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>)<br/>
(<span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) (<span class="id" title="var">v</span> : <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>) :=<br/>
<span class="id" title="keyword">fun</span> <span class="id" title="var">x'</span> ⇒ <span class="id" title="keyword">if</span> <a class="idref" href="Maps.html#eqb_string"><span class="id" title="definition">eqb_string</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#x'"><span class="id" title="variable">x'</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Maps.html#x'"><span class="id" title="variable">x'</span></a>.<br/>
</div>
<div class="doc">
此定义是个高阶编程的好例子：<span class="inlinecode"><span class="id" title="var">t_update</span></span> 接受一个<i>'函数'</i> <span class="inlinecode"><span class="id" title="var">m</span></span>
并产生一个新的函数 <span class="inlinecode"><span class="id" title="keyword">fun</span></span> <span class="inlinecode"><span class="id" title="var">x'</span></span> <span class="inlinecode">⇒</span> <span class="inlinecode">...</span>，它的表现与所需的映射一致。
<div class="paragraph"> </div>
例如，我们可以构建一个从 <span class="inlinecode"><span class="id" title="var">string</span></span> 到 <span class="inlinecode"><span class="id" title="var">bool</span></span> 的映射，其中 <span class="inlinecode">"<span class="id" title="var">foo</span>"</span>
和 <span class="inlinecode">"<span class="id" title="var">bar</span>"</span> 映射到 <span class="inlinecode"><span class="id" title="var">true</span></span>，其它键则映射到 <span class="inlinecode"><span class="id" title="var">false</span></span>，就像这样：
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="examplemap"><span class="id" title="definition">examplemap</span></a> :=<br/>
<a class="idref" href="Maps.html#t_update"><span class="id" title="definition">t_update</span></a> (<a class="idref" href="Maps.html#t_update"><span class="id" title="definition">t_update</span></a> (<a class="idref" href="Maps.html#t_empty"><span class="id" title="definition">t_empty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>) "foo" <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>)<br/>
"bar" <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/>
</div>
<div class="doc">
接下来，我们引入一些新的记法来方便映射的使用。
<div class="paragraph"> </div>
首先，我们会使用以下记法，根据一个默认值来创建空的全映射。
</div>
<div class="code">
<span class="id" title="keyword">Notation</span> <a name="bc1c5e34127128228512ba20d13f5577"><span class="id" title="notation">"</span></a>'_' '!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span>' v" := (<a class="idref" href="Maps.html#t_empty"><span class="id" title="definition">t_empty</span></a> <span class="id" title="var">v</span>)<br/>
(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 100, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a name="example_empty"><span class="id" title="definition">example_empty</span></a> := (<a class="idref" href="Maps.html#bc1c5e34127128228512ba20d13f5577"><span class="id" title="notation">_</span></a> <a class="idref" href="Maps.html#bc1c5e34127128228512ba20d13f5577"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>).<br/>
</div>
<div class="doc">
然后，我们引入一种方便的记法，通过一些绑定来扩展现有的映射。
</div>
<div class="code">
<span class="id" title="keyword">Notation</span> <a name="8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">"</span></a>x '!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span>' v ';' m" := (<a class="idref" href="Maps.html#t_update"><span class="id" title="definition">t_update</span></a> <span class="id" title="var">m</span> <span class="id" title="var">x</span> <span class="id" title="var">v</span>)<br/>
(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 100, <span class="id" title="var">v</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/>
</div>
<div class="doc">
前面的 <span class="inlinecode"><span class="id" title="var">examplemap</span></span> 现在可以定义如下：
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="examplemap'"><span class="id" title="definition">examplemap'</span></a> :=<br/>
( "bar" <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a><br/>
"foo" <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a><br/>
<a class="idref" href="Maps.html#bc1c5e34127128228512ba20d13f5577"><span class="id" title="notation">_</span></a> <a class="idref" href="Maps.html#bc1c5e34127128228512ba20d13f5577"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><br/>
).<br/>
</div>
<div class="doc">
到这里就完成了全映射的定义。注意我们无需定义 <span class="inlinecode"><span class="id" title="var">find</span></span> 操作，
因为它不过就是个函数应用！
</div>
<div class="doc">
为了在后面的章节中使用映射，我们需要一些关于其表现的基本事实。
<div class="paragraph"> </div>
即便你没有进行下面的练习，也要确保透彻地理解以下引理的陈述！
<div class="paragraph"> </div>
（其中有些证明需要函数的外延性公理，我们在 <a href="Logic.html"><span class="inlineref">Logic</span></a> 一节中讨论过它）。
<div class="paragraph"> </div>
<a name="lab258"></a><h4 class="section">练习：1 星, standard, optional (t_apply_empty)</h4>
首先，空映射对于所有的键都会返回默认元素（即，空映射总是返回默认元素）：
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Lemma</span> <a name="t_apply_empty"><span class="id" title="lemma">t_apply_empty</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) (<span class="id" title="var">v</span> : <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>),<br/>
(<a class="idref" href="Maps.html#bc1c5e34127128228512ba20d13f5577"><span class="id" title="notation">_</span></a> <a class="idref" href="Maps.html#bc1c5e34127128228512ba20d13f5577"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a>) <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* 请在此处解答 *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a name="lab259"></a><h4 class="section">练习：2 星, standard, optional (t_update_eq)</h4>
接着，如果将映射 <span class="inlinecode"><span class="id" title="var">m</span></span> 的键 <span class="inlinecode"><span class="id" title="var">x</span></span> 关联的值更新为 <span class="inlinecode"><span class="id" title="var">v</span></span>，然后在 <span class="inlinecode"><span class="id" title="var">update</span></span>
产生的新映射中查找 <span class="inlinecode"><span class="id" title="var">x</span></span>，就会得到 <span class="inlinecode"><span class="id" title="var">v</span></span>（即，更新某个键的映射，
查找它就会得到更新后的值）：
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Lemma</span> <a name="t_update_eq"><span class="id" title="lemma">t_update_eq</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">m</span> : <a class="idref" href="Maps.html#total_map"><span class="id" title="definition">total_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>) <span class="id" title="var">x</span> <span class="id" title="var">v</span>,<br/>
(<a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* 请在此处解答 *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a name="lab260"></a><h4 class="section">练习：2 星, standard, optional (t_update_neq)</h4>
此外，如果将映射 <span class="inlinecode"><span class="id" title="var">m</span></span> 的键 <span class="inlinecode"><span class="id" title="var">x<sub>1</sub></span></span> 更新后在返回的结果中查找<i>'另一个'</i>键
<span class="inlinecode"><span class="id" title="var">x<sub>2</sub></span></span>，那么得到的结果与在 <span class="inlinecode"><span class="id" title="var">m</span></span> 中查找它的结果相同
（即，更新某个键的映射，不影响其它键的映射）：
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Theorem</span> <a name="t_update_neq"><span class="id" title="lemma">t_update_neq</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">m</span> : <a class="idref" href="Maps.html#total_map"><span class="id" title="definition">total_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>) <span class="id" title="var">x<sub>1</sub></span> <span class="id" title="var">x<sub>2</sub></span> <span class="id" title="var">v</span>,<br/>
<a class="idref" href="Maps.html#x<sub>1</sub>"><span class="id" title="variable">x<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc<sub>9</sub>"><span class="id" title="notation">≠</span></a> <a class="idref" href="Maps.html#x<sub>2</sub>"><span class="id" title="variable">x<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="Maps.html#x<sub>1</sub>"><span class="id" title="variable">x<sub>1</sub></span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="Maps.html#x<sub>2</sub>"><span class="id" title="variable">x<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Maps.html#x<sub>2</sub>"><span class="id" title="variable">x<sub>2</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* 请在此处解答 *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a name="lab261"></a><h4 class="section">练习：2 星, standard, optional (t_update_shadow)</h4>
如果将映射 <span class="inlinecode"><span class="id" title="var">m</span></span> 的键 <span class="inlinecode"><span class="id" title="var">x</span></span> 关联的值更新为 <span class="inlinecode"><span class="id" title="var">v<sub>1</sub></span></span> 后，又将同一个键 <span class="inlinecode"><span class="id" title="var">x</span></span>
更新为另一个值 <span class="inlinecode"><span class="id" title="var">v<sub>2</sub></span></span>，那么产生的映射与仅将第二次 <span class="inlinecode"><span class="id" title="var">update</span></span> 应用于 <span class="inlinecode"><span class="id" title="var">m</span></span>
所得到的映射表现一致（即二者应用到同一键时产生的结果相同）：
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Lemma</span> <a name="t_update_shadow"><span class="id" title="lemma">t_update_shadow</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">m</span> : <a class="idref" href="Maps.html#total_map"><span class="id" title="definition">total_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>) <span class="id" title="var">x</span> <span class="id" title="var">v<sub>1</sub></span> <span class="id" title="var">v<sub>2</sub></span>,<br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="Maps.html#v<sub>2</sub>"><span class="id" title="variable">v<sub>2</sub></span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="Maps.html#v<sub>1</sub>"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="Maps.html#v<sub>2</sub>"><span class="id" title="variable">v<sub>2</sub></span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* 请在此处解答 *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
对于最后两个全映射的引理而言，用 <a href="IndProp.html"><span class="inlineref">IndProp</span></a> 一章中引入的互映法
（Reflection idioms）来证明会十分方便。我们首先通过证明基本的<i>'互映引理'</i>，
将字符串上的相等关系命题与布尔函数 <span class="inlinecode"><span class="id" title="var">eqb_string</span></span> 关联起来。
<div class="paragraph"> </div>
<a name="lab262"></a><h4 class="section">练习：2 星, standard, optional (eqb_stringP)</h4>
请仿照 <a href="IndProp.html"><span class="inlineref">IndProp</span></a> 一章中对 <span class="inlinecode"><span class="id" title="var">eqb_natP</span></span> 的证明来证明以下引理：
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Lemma</span> <a name="eqb_stringP"><span class="id" title="lemma">eqb_stringP</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>,<br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Bool.Bool.html#reflect"><span class="id" title="inductive">reflect</span></a> (<a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Maps.html#y"><span class="id" title="variable">y</span></a>) (<a class="idref" href="Maps.html#eqb_string"><span class="id" title="definition">eqb_string</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#y"><span class="id" title="variable">y</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* 请在此处解答 *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
现在，给定 <span class="inlinecode"><span class="id" title="var">string</span></span> 类型的字符串 <span class="inlinecode"><span class="id" title="var">x<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" title="var">x<sub>2</sub></span></span>，我们可以在使用策略
<span class="inlinecode"><span class="id" title="tactic">destruct</span></span> <span class="inlinecode">(<span class="id" title="var">eqb_stringP</span></span> <span class="inlinecode"><span class="id" title="var">x<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">x<sub>2</sub></span>)</span> 对 <span class="inlinecode"><span class="id" title="var">eqb_string</span></span> <span class="inlinecode"><span class="id" title="var">x<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">x<sub>2</sub></span></span>
的结果进行分类讨论的同时，生成关于 <span class="inlinecode"><span class="id" title="var">x<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" title="var">x<sub>2</sub></span></span> （在 <span class="inlinecode">=</span> 的意义上）
的相等关系前提。
<div class="paragraph"> </div>
<a name="lab263"></a><h4 class="section">练习：2 星, standard (t_update_same)</h4>
请仿照 <a href="IndProp.html"><span class="inlineref">IndProp</span></a> 一章中的示例，用 <span class="inlinecode"><span class="id" title="var">eqb_stringP</span></span> 来证明以下定理，
它陈述了：如果我们用映射 <span class="inlinecode"><span class="id" title="var">m</span></span> 中已经与键 <span class="inlinecode"><span class="id" title="var">x</span></span> 相关联的值更新了 <span class="inlinecode"><span class="id" title="var">x</span></span>，
那么其结果与 <span class="inlinecode"><span class="id" title="var">m</span></span> 相等：
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Theorem</span> <a name="t_update_same"><span class="id" title="lemma">t_update_same</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">m</span> : <a class="idref" href="Maps.html#total_map"><span class="id" title="definition">total_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>) <span class="id" title="var">x</span>,<br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* 请在此处解答 *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a name="lab264"></a><h4 class="section">练习：3 星, standard, recommended (t_update_permute)</h4>
使用 <span class="inlinecode"><span class="id" title="var">eqb_stringP</span></span> 来证明最后一个 <span class="inlinecode"><span class="id" title="var">update</span></span> 函数的性质：
如果我们更新了映射 <span class="inlinecode"><span class="id" title="var">m</span></span> 中两个不同的键，那么更新的顺序无关紧要。
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Theorem</span> <a name="t_update_permute"><span class="id" title="lemma">t_update_permute</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">m</span> : <a class="idref" href="Maps.html#total_map"><span class="id" title="definition">total_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>)<br/>
<span class="id" title="var">v<sub>1</sub></span> <span class="id" title="var">v<sub>2</sub></span> <span class="id" title="var">x<sub>1</sub></span> <span class="id" title="var">x<sub>2</sub></span>,<br/>
<a class="idref" href="Maps.html#x<sub>2</sub>"><span class="id" title="variable">x<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc<sub>9</sub>"><span class="id" title="notation">≠</span></a> <a class="idref" href="Maps.html#x<sub>1</sub>"><span class="id" title="variable">x<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="Maps.html#x<sub>1</sub>"><span class="id" title="variable">x<sub>1</sub></span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="Maps.html#v<sub>1</sub>"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#x<sub>2</sub>"><span class="id" title="variable">x<sub>2</sub></span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="Maps.html#v<sub>2</sub>"><span class="id" title="variable">v<sub>2</sub></span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a><br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a><br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="Maps.html#x<sub>2</sub>"><span class="id" title="variable">x<sub>2</sub></span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="Maps.html#v<sub>2</sub>"><span class="id" title="variable">v<sub>2</sub></span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#x<sub>1</sub>"><span class="id" title="variable">x<sub>1</sub></span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="Maps.html#v<sub>1</sub>"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* 请在此处解答 *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<a name="lab265"></a><h1 class="section">偏映射</h1>
<div class="paragraph"> </div>
最后，我们在全映射之上定义<i>'偏映射'</i>。元素类型为 <span class="inlinecode"><span class="id" title="var">A</span></span> 的偏映射不过就是个
元素类型为 <span class="inlinecode"><span class="id" title="var">option</span></span> <span class="inlinecode"><span class="id" title="var">A</span></span>，默认元素为 <span class="inlinecode"><span class="id" title="var">None</span></span> 的全映射。
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a name="partial_map"><span class="id" title="definition">partial_map</span></a> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) := <a class="idref" href="Maps.html#total_map"><span class="id" title="definition">total_map</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a name="empty"><span class="id" title="definition">empty</span></a> {<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>} : <a class="idref" href="Maps.html#partial_map"><span class="id" title="definition">partial_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a> :=<br/>
<a class="idref" href="Maps.html#t_empty"><span class="id" title="definition">t_empty</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a name="update"><span class="id" title="definition">update</span></a> {<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>} (<span class="id" title="var">m</span> : <a class="idref" href="Maps.html#partial_map"><span class="id" title="definition">partial_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>)<br/>
(<span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) (<span class="id" title="var">v</span> : <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>) :=<br/>
(<a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>></span></span></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="Maps.html#8d30c24efec4c4217ffea53676b55c2e"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a>).<br/>
</div>
<div class="doc">
我们为偏映射引入类似的记法。
</div>
<div class="code">
<span class="id" title="keyword">Notation</span> <a name="413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation">"</span></a>x '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span>' v ';' m" := (<a class="idref" href="Maps.html#update"><span class="id" title="definition">update</span></a> <span class="id" title="var">m</span> <span class="id" title="var">x</span> <span class="id" title="var">v</span>)<br/>
(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 100, <span class="id" title="var">v</span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>, <span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>).<br/>
</div>
<div class="doc">
当最后一种情况为空时，我们也可以隐藏它。
</div>
<div class="code">
<span class="id" title="keyword">Notation</span> <a name="02007db97cbde7d2bc4092cba36f71b<sub>6</sub>"><span class="id" title="notation">"</span></a>x '<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span>' v" := (<a class="idref" href="Maps.html#update"><span class="id" title="definition">update</span></a> <a class="idref" href="Maps.html#empty"><span class="id" title="definition">empty</span></a> <span class="id" title="var">x</span> <span class="id" title="var">v</span>)<br/>
(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 100).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a name="examplepmap"><span class="id" title="definition">examplepmap</span></a> :=<br/>
("Church" <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation">;</span></a> "Turing" <a class="idref" href="Maps.html#02007db97cbde7d2bc4092cba36f71b<sub>6</sub>"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>).<br/>
</div>
<div class="doc">
现在我们将所有关于全映射的基本引理直接转换成对应的偏映射引理。
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Lemma</span> <a name="apply_empty"><span class="id" title="lemma">apply_empty</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>),<br/>
@<a class="idref" href="Maps.html#empty"><span class="id" title="definition">empty</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="Maps.html#empty"><span class="id" title="definition">empty</span></a>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="Maps.html#t_apply_empty"><span class="id" title="axiom">t_apply_empty</span></a>.<br/>
<span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="update_eq"><span class="id" title="lemma">update_eq</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">m</span> : <a class="idref" href="Maps.html#partial_map"><span class="id" title="definition">partial_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>) <span class="id" title="var">x</span> <span class="id" title="var">v</span>,<br/>
(<a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span></span></a> <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a>.<br/>
<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="Maps.html#update"><span class="id" title="definition">update</span></a>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="Maps.html#t_update_eq"><span class="id" title="axiom">t_update_eq</span></a>.<br/>
<span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="update_neq"><span class="id" title="lemma">update_neq</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">m</span> : <a class="idref" href="Maps.html#partial_map"><span class="id" title="definition">partial_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>) <span class="id" title="var">x<sub>1</sub></span> <span class="id" title="var">x<sub>2</sub></span> <span class="id" title="var">v</span>,<br/>
<a class="idref" href="Maps.html#x<sub>2</sub>"><span class="id" title="variable">x<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc<sub>9</sub>"><span class="id" title="notation">≠</span></a> <a class="idref" href="Maps.html#x<sub>1</sub>"><span class="id" title="variable">x<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
(<a class="idref" href="Maps.html#x<sub>2</sub>"><span class="id" title="variable">x<sub>2</sub></span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span></span></a> <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="Maps.html#x<sub>1</sub>"><span class="id" title="variable">x<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Maps.html#x<sub>1</sub>"><span class="id" title="variable">x<sub>1</sub></span></a>.<br/>
<div class="togglescript" id="proofcontrol7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')"><span class="show"></span></div>
<div class="proofscript" id="proof7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')">
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">m</span> <span class="id" title="var">x<sub>1</sub></span> <span class="id" title="var">x<sub>2</sub></span> <span class="id" title="var">v</span> <span class="id" title="var">H</span>.<br/>
<span class="id" title="tactic">unfold</span> <a class="idref" href="Maps.html#update"><span class="id" title="definition">update</span></a>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="Maps.html#t_update_neq"><span class="id" title="axiom">t_update_neq</span></a>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="tactic">apply</span> <span class="id" title="var">H</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" title="keyword">Lemma</span> <a name="update_shadow"><span class="id" title="lemma">update_shadow</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">m</span> : <a class="idref" href="Maps.html#partial_map"><span class="id" title="definition">partial_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>) <span class="id" title="var">x</span> <span class="id" title="var">v<sub>1</sub></span> <span class="id" title="var">v<sub>2</sub></span>,<br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span></span></a> <a class="idref" href="Maps.html#v<sub>2</sub>"><span class="id" title="variable">v<sub>2</sub></span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span></span></a> <a class="idref" href="Maps.html#v<sub>1</sub>"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span></span></a> <a class="idref" href="Maps.html#v<sub>2</sub>"><span class="id" title="variable">v<sub>2</sub></span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
<div class="togglescript" id="proofcontrol8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')"><span class="show"></span></div>
<div class="proofscript" id="proof8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')">
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">m</span> <span class="id" title="var">x</span> <span class="id" title="var">v<sub>1</sub></span> <span class="id" title="var">v<sub>2</sub></span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="Maps.html#update"><span class="id" title="definition">update</span></a>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="Maps.html#t_update_shadow"><span class="id" title="axiom">t_update_shadow</span></a>.<br/>
<span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="update_same"><span class="id" title="lemma">update_same</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">m</span> : <a class="idref" href="Maps.html#partial_map"><span class="id" title="definition">partial_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>) <span class="id" title="var">x</span> <span class="id" title="var">v</span>,<br/>
<a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="Maps.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span></span></a> <a class="idref" href="Maps.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a>.<br/>
<div class="togglescript" id="proofcontrol9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')"><span class="show"></span></div>
<div class="proofscript" id="proof9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')">
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">m</span> <span class="id" title="var">x</span> <span class="id" title="var">v</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="Maps.html#update"><span class="id" title="definition">update</span></a>. <span class="id" title="tactic">rewrite</span> <- <span class="id" title="var">H</span>.<br/>
<span class="id" title="tactic">apply</span> <a class="idref" href="Maps.html#t_update_same"><span class="id" title="axiom">t_update_same</span></a>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" title="keyword">Theorem</span> <a name="update_permute"><span class="id" title="lemma">update_permute</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">A</span> : <span class="id" title="keyword">Type</span>) (<span class="id" title="var">m</span> : <a class="idref" href="Maps.html#partial_map"><span class="id" title="definition">partial_map</span></a> <a class="idref" href="Maps.html#A"><span class="id" title="variable">A</span></a>)<br/>
<span class="id" title="var">x<sub>1</sub></span> <span class="id" title="var">x<sub>2</sub></span> <span class="id" title="var">v<sub>1</sub></span> <span class="id" title="var">v<sub>2</sub></span>,<br/>
<a class="idref" href="Maps.html#x<sub>2</sub>"><span class="id" title="variable">x<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#32263a1c8b01baecdff9deb038955bc<sub>9</sub>"><span class="id" title="notation">≠</span></a> <a class="idref" href="Maps.html#x<sub>1</sub>"><span class="id" title="variable">x<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="Maps.html#x<sub>1</sub>"><span class="id" title="variable">x<sub>1</sub></span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span></span></a> <a class="idref" href="Maps.html#v<sub>1</sub>"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#x<sub>2</sub>"><span class="id" title="variable">x<sub>2</sub></span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span></span></a> <a class="idref" href="Maps.html#v<sub>2</sub>"><span class="id" title="variable">v<sub>2</sub></span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="Maps.html#x<sub>2</sub>"><span class="id" title="variable">x<sub>2</sub></span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span></span></a> <a class="idref" href="Maps.html#v<sub>2</sub>"><span class="id" title="variable">v<sub>2</sub></span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#x<sub>1</sub>"><span class="id" title="variable">x<sub>1</sub></span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>⊢</span><span style='font-size:90%;'>></span></span></span></span></span></a> <a class="idref" href="Maps.html#v<sub>1</sub>"><span class="id" title="variable">v<sub>1</sub></span></a> <a class="idref" href="Maps.html#413fa44b816aeb6f565da2a108290ead"><span class="id" title="notation">;</span></a> <a class="idref" href="Maps.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
<div class="togglescript" id="proofcontrol10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')"><span class="show"></span></div>
<div class="proofscript" id="proof10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')">
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">m</span> <span class="id" title="var">x<sub>1</sub></span> <span class="id" title="var">x<sub>2</sub></span> <span class="id" title="var">v<sub>1</sub></span> <span class="id" title="var">v<sub>2</sub></span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="Maps.html#update"><span class="id" title="definition">update</span></a>.<br/>
<span class="id" title="tactic">apply</span> <a class="idref" href="Maps.html#t_update_permute"><span class="id" title="axiom">t_update_permute</span></a>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="comment">(* 2021-08-22 05:49:31 (UTC+00) *)</span><br/>
</div>
</div>
<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>
</div>
</body>
</html>