forked from DeepSpec/sf
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathMultiset.html
More file actions
556 lines (412 loc) · 53.8 KB
/
Multiset.html
File metadata and controls
556 lines (412 loc) · 53.8 KB
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
<!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>Multiset: Insertion Sort Verified With Multisets</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/vfa.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<div id="page">
<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 3: Verified Functional Algorithms</a></div>
<ul id='menu'>
<li class='section_name'><a href='toc.html'>Table of Contents</a></li>
<li class='section_name'><a href='coqindex.html'>Index</a></li>
<li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>
<div id="main">
<h1 class="libtitle">Multiset<span class="subtitle">Insertion Sort Verified With Multisets</span></h1>
<div class="doc">
<div class="paragraph"> </div>
Our specification of <span class="inlinecode"><span class="id" title="var">sorted</span></span> in <a href="Sort.html"><span class="inlineref">Sort</span></a> was based in
part on permutations, which enabled us to express the idea that
sorting rearranges list elements but does not add or remove any.
<div class="paragraph"> </div>
Another way to express that idea is to use multisets, aka bags. A
<i>set</i> is like a list in which element order is irrelevant, and in
which no duplicate elements are permitted. That is, an element can
either be <i>in</i> the set or not in the set, but it can't be in the
set multiple times. A <i>multiset</i> relaxes that restriction: an
element can be in the multiset multiple times. The number of
times the element occurs in the multiset is the element's
<i>multiplicity</i>.
<div class="paragraph"> </div>
For example:
<div class="paragraph"> </div>
<ul class="doclist">
<li> <span class="inlinecode">{1,</span> <span class="inlinecode">2}</span> is a set, and is the same as set <span class="inlinecode">{2,</span> <span class="inlinecode">1}</span>.
<div class="paragraph"> </div>
</li>
<li> <span class="inlinecode">[1;</span> <span class="inlinecode">1;</span> <span class="inlinecode">2]</span> is a list, and is different than list <span class="inlinecode">[2;</span> <span class="inlinecode">1;</span> <span class="inlinecode">1]</span>.
<div class="paragraph"> </div>
</li>
<li> <span class="inlinecode">{1,</span> <span class="inlinecode">1,</span> <span class="inlinecode">2}</span> is a multiset and the same as multiset <span class="inlinecode">{2,</span> <span class="inlinecode">1,</span> <span class="inlinecode">1}</span>.
</li>
</ul>
<div class="paragraph"> </div>
In this chapter we'll explore using multisets to specify
sortedness.
</div>
<div class="doc">
<a id="lab39"></a><h1 class="section">Multisets</h1>
<div class="paragraph"> </div>
We will represent multisets as functions: if <span class="inlinecode"><span class="id" title="var">m</span></span> is a
multiset, then <span class="inlinecode"><span class="id" title="var">m</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> will be the multiplicity of <span class="inlinecode"><span class="id" title="var">n</span></span> in <span class="inlinecode"><span class="id" title="var">m</span></span>.
Since we are sorting lists of natural numbers, the type of
multisets would be <span class="inlinecode"><span class="id" title="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">nat</span></span>. The input is the value, the output is
its multiplicity. To help avoid confusion between those two uses
of <span class="inlinecode"><span class="id" title="var">nat</span></span>, we'll introduce a synonym, <span class="inlinecode"><span class="id" title="var">value</span></span>.
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="value" class="idref" href="#value"><span class="id" title="definition">value</span></a> := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="multiset" class="idref" href="#multiset"><span class="id" title="definition">multiset</span></a> := <a class="idref" href="Multiset.html#value"><span class="id" title="definition">value</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
</div>
<div class="doc">
The <span class="inlinecode"><span class="id" title="var">empty</span></span> multiset has multiplicity <span class="inlinecode">0</span> for every value.
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="empty" class="idref" href="#empty"><span class="id" title="definition">empty</span></a> : <a class="idref" href="Multiset.html#multiset"><span class="id" title="definition">multiset</span></a> :=<br/>
<span class="id" title="keyword">fun</span> <a id="x:1" class="idref" href="#x:1"><span class="id" title="binder">x</span></a> ⇒ 0.<br/>
</div>
<div class="doc">
Multiset <span class="inlinecode"><span class="id" title="var">singleton</span></span> <span class="inlinecode"><span class="id" title="var">v</span></span> contains only <span class="inlinecode"><span class="id" title="var">v</span></span>, and exactly once.
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="singleton" class="idref" href="#singleton"><span class="id" title="definition">singleton</span></a> (<a id="v:2" class="idref" href="#v:2"><span class="id" title="binder">v</span></a>: <a class="idref" href="Multiset.html#value"><span class="id" title="definition">value</span></a>) : <a class="idref" href="Multiset.html#multiset"><span class="id" title="definition">multiset</span></a> :=<br/>
<span class="id" title="keyword">fun</span> <a id="x:3" class="idref" href="#x:3"><span class="id" title="binder">x</span></a> ⇒ <span class="id" title="keyword">if</span> <a class="idref" href="Multiset.html#x:3"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Arith.PeanoNat.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> <a class="idref" href="Multiset.html#v:2"><span class="id" title="variable">v</span></a> <span class="id" title="keyword">then</span> 1 <span class="id" title="keyword">else</span> 0.<br/>
</div>
<div class="doc">
The union of two multisets is their <i>pointwise</i> sum.
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="union" class="idref" href="#union"><span class="id" title="definition">union</span></a> (<a id="a:4" class="idref" href="#a:4"><span class="id" title="binder">a</span></a> <a id="b:5" class="idref" href="#b:5"><span class="id" title="binder">b</span></a> : <a class="idref" href="Multiset.html#multiset"><span class="id" title="definition">multiset</span></a>) : <a class="idref" href="Multiset.html#multiset"><span class="id" title="definition">multiset</span></a> :=<br/>
<span class="id" title="keyword">fun</span> <a id="x:6" class="idref" href="#x:6"><span class="id" title="binder">x</span></a> ⇒ <a class="idref" href="Multiset.html#a:4"><span class="id" title="variable">a</span></a> <a class="idref" href="Multiset.html#x:6"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Multiset.html#b:5"><span class="id" title="variable">b</span></a> <a class="idref" href="Multiset.html#x:6"><span class="id" title="variable">x</span></a>.<br/>
</div>
<div class="doc">
<a id="lab40"></a><h4 class="section">Exercise: 1 star, standard (union_assoc)</h4>
<div class="paragraph"> </div>
Prove that multiset union is associative.
<div class="paragraph"> </div>
To prove that one multiset equals another we use the axiom of
functional extensionality, which was introduced in
<a href="https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html"><span class="inlineref">Logic</span></a>. We begin the proof below by using Coq's tactic
<span class="inlinecode"><span class="id" title="tactic">extensionality</span></span>, which applies that axiom.
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a id="union_assoc" class="idref" href="#union_assoc"><span class="id" title="lemma">union_assoc</span></a>: <span class="id" title="keyword">∀</span> <a id="a:7" class="idref" href="#a:7"><span class="id" title="binder">a</span></a> <a id="b:8" class="idref" href="#b:8"><span class="id" title="binder">b</span></a> <a id="c:9" class="idref" href="#c:9"><span class="id" title="binder">c</span></a> : <a class="idref" href="Multiset.html#multiset"><span class="id" title="definition">multiset</span></a>,<br/>
<a class="idref" href="Multiset.html#union"><span class="id" title="definition">union</span></a> <a class="idref" href="Multiset.html#a:7"><span class="id" title="variable">a</span></a> (<a class="idref" href="Multiset.html#union"><span class="id" title="definition">union</span></a> <a class="idref" href="Multiset.html#b:8"><span class="id" title="variable">b</span></a> <a class="idref" href="Multiset.html#c:9"><span class="id" title="variable">c</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#union"><span class="id" title="definition">union</span></a> (<a class="idref" href="Multiset.html#union"><span class="id" title="definition">union</span></a> <a class="idref" href="Multiset.html#a:7"><span class="id" title="variable">a</span></a> <a class="idref" href="Multiset.html#b:8"><span class="id" title="variable">b</span></a>) <a class="idref" href="Multiset.html#c:9"><span class="id" title="variable">c</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span>.<br/>
<span class="id" title="tactic">extensionality</span> <span class="id" title="var">x</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a id="lab41"></a><h4 class="section">Exercise: 1 star, standard (union_comm)</h4>
<div class="paragraph"> </div>
Prove that multiset union is commutative.
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a id="union_comm" class="idref" href="#union_comm"><span class="id" title="lemma">union_comm</span></a>: <span class="id" title="keyword">∀</span> <a id="a:10" class="idref" href="#a:10"><span class="id" title="binder">a</span></a> <a id="b:11" class="idref" href="#b:11"><span class="id" title="binder">b</span></a> : <a class="idref" href="Multiset.html#multiset"><span class="id" title="definition">multiset</span></a>,<br/>
<a class="idref" href="Multiset.html#union"><span class="id" title="definition">union</span></a> <a class="idref" href="Multiset.html#a:10"><span class="id" title="variable">a</span></a> <a class="idref" href="Multiset.html#b:11"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#union"><span class="id" title="definition">union</span></a> <a class="idref" href="Multiset.html#b:11"><span class="id" title="variable">b</span></a> <a class="idref" href="Multiset.html#a:10"><span class="id" title="variable">a</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a id="lab42"></a><h4 class="section">Exercise: 2 stars, standard (union_swap)</h4>
<div class="paragraph"> </div>
Prove that the multisets in a nested union can be swapped.
You do not need <span class="inlinecode"><span class="id" title="tactic">extensionality</span></span> if you use the previous
two lemmas.
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a id="union_swap" class="idref" href="#union_swap"><span class="id" title="lemma">union_swap</span></a> : <span class="id" title="keyword">∀</span> <a id="a:12" class="idref" href="#a:12"><span class="id" title="binder">a</span></a> <a id="b:13" class="idref" href="#b:13"><span class="id" title="binder">b</span></a> <a id="c:14" class="idref" href="#c:14"><span class="id" title="binder">c</span></a> : <a class="idref" href="Multiset.html#multiset"><span class="id" title="definition">multiset</span></a>,<br/>
<a class="idref" href="Multiset.html#union"><span class="id" title="definition">union</span></a> <a class="idref" href="Multiset.html#a:12"><span class="id" title="variable">a</span></a> (<a class="idref" href="Multiset.html#union"><span class="id" title="definition">union</span></a> <a class="idref" href="Multiset.html#b:13"><span class="id" title="variable">b</span></a> <a class="idref" href="Multiset.html#c:14"><span class="id" title="variable">c</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#union"><span class="id" title="definition">union</span></a> <a class="idref" href="Multiset.html#b:13"><span class="id" title="variable">b</span></a> (<a class="idref" href="Multiset.html#union"><span class="id" title="definition">union</span></a> <a class="idref" href="Multiset.html#a:12"><span class="id" title="variable">a</span></a> <a class="idref" href="Multiset.html#c:14"><span class="id" title="variable">c</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
Note that this is not an efficient implementation of multisets.
We wouldn't want to use it for programs with high performance
requirements. But we are using multisets for specifications, not
for programs. We don't intend to build large multisets, only to
use them in verifying algorithms such as insertion sort. So this
inefficiency is not a problem.
<div class="paragraph"> </div>
<a id="lab43"></a><h1 class="section">Specification of Sorting</h1>
<div class="paragraph"> </div>
A sorting algorithm must rearrange the elements into a list
that is totally ordered. Using multisets, we can restate that as:
the algorithm must produce a list <i>with the same multiset of
values</i>, and this list must be totally ordered. Let's formalize
that idea.
<div class="paragraph"> </div>
The <i>contents</i> of a list are the elements it contains, without
any notion of order. Function <span class="inlinecode"><span class="id" title="var">contents</span></span> extracts the contents
of a list as a multiset.
</div>
<div class="code">
<span class="id" title="keyword">Fixpoint</span> <a id="contents" class="idref" href="#contents"><span class="id" title="definition">contents</span></a> (<a id="al:15" class="idref" href="#al:15"><span class="id" title="binder">al</span></a>: <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Multiset.html#value"><span class="id" title="definition">value</span></a>) : <a class="idref" href="Multiset.html#multiset"><span class="id" title="definition">multiset</span></a> :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="Multiset.html#al:15"><span class="id" title="variable">al</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> ⇒ <a class="idref" href="Multiset.html#empty"><span class="id" title="definition">empty</span></a><br/>
| <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">bl</span> ⇒ <a class="idref" href="Multiset.html#union"><span class="id" title="definition">union</span></a> (<a class="idref" href="Multiset.html#singleton"><span class="id" title="definition">singleton</span></a> <span class="id" title="var">a</span>) (<a class="idref" href="Multiset.html#contents:16"><span class="id" title="definition">contents</span></a> <span class="id" title="var">bl</span>)<br/>
<span class="id" title="keyword">end</span>.<br/>
</div>
<div class="doc">
The insertion-sort program <span class="inlinecode"><span class="id" title="var">sort</span></span> from <a href="Sort.html"><span class="inlineref">Sort</span></a> preserves
the contents of a list. Here's an example of that:
</div>
<div class="code">
<span class="id" title="keyword">Example</span> <a id="sort_pi_same_contents" class="idref" href="#sort_pi_same_contents"><span class="id" title="definition">sort_pi_same_contents</span></a>:<br/>
<a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> (<a class="idref" href="Sort.html#sort"><span class="id" title="definition">sort</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a>3<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>1<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>4<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>1<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>5<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>9<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>2<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>6<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>5<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>3<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>5<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a>3<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>1<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>4<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>1<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>5<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>9<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>2<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>6<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>5<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>3<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a>5<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">extensionality</span> <span class="id" title="var">x</span>.<br/>
<span class="id" title="tactic">repeat</span> (<span class="id" title="tactic">destruct</span> <span class="id" title="var">x</span>; <span class="id" title="tactic">try</span> <span class="id" title="tactic">reflexivity</span>).<br/>
<span class="comment">(* Why does this work? Try it step by step, without <span class="inlinecode"><span class="id" title="tactic">repeat</span></span>. *)</span><br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
<div class="doc">
A sorting algorithm must preserve contents and totally order the
list.
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="is_a_sorting_algorithm'" class="idref" href="#is_a_sorting_algorithm'"><span class="id" title="definition">is_a_sorting_algorithm'</span></a> (<a id="f:18" class="idref" href="#f:18"><span class="id" title="binder">f</span></a>: <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) := <span class="id" title="keyword">∀</span> <a id="al:19" class="idref" href="#al:19"><span class="id" title="binder">al</span></a>,<br/>
<a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <a class="idref" href="Multiset.html#al:19"><span class="id" title="variable">al</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> (<a class="idref" href="Multiset.html#f:18"><span class="id" title="variable">f</span></a> <a class="idref" href="Multiset.html#al:19"><span class="id" title="variable">al</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="Sort.html#sorted"><span class="id" title="inductive">sorted</span></a> (<a class="idref" href="Multiset.html#f:18"><span class="id" title="variable">f</span></a> <a class="idref" href="Multiset.html#al:19"><span class="id" title="variable">al</span></a>).<br/>
</div>
<div class="doc">
That definition is similar to <span class="inlinecode"><span class="id" title="var">is_a_sorting_algorithm</span></span> from <a href="Sort.html"><span class="inlineref">Sort</span></a>,
except that we're now using <span class="inlinecode"><span class="id" title="var">contents</span></span> instead of <span class="inlinecode"><span class="id" title="var">Permutation</span></span>.
<div class="paragraph"> </div>
<a id="lab44"></a><h1 class="section">Verification of Insertion Sort</h1>
<div class="paragraph"> </div>
The following series of exercises will take you through a
verification of insertion sort using multisets.
<div class="paragraph"> </div>
<a id="lab45"></a><h4 class="section">Exercise: 3 stars, standard (insert_contents)</h4>
<div class="paragraph"> </div>
Prove that insertion sort's <span class="inlinecode"><span class="id" title="var">insert</span></span> function produces the same
contents as merely prepending the inserted element to the front of
the list.
<div class="paragraph"> </div>
Proceed by induction. You do not need <span class="inlinecode"><span class="id" title="tactic">extensionality</span></span> if you
make use of the above lemmas about <span class="inlinecode"><span class="id" title="var">union</span></span>.
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a id="insert_contents" class="idref" href="#insert_contents"><span class="id" title="lemma">insert_contents</span></a>: <span class="id" title="keyword">∀</span> <a id="x:20" class="idref" href="#x:20"><span class="id" title="binder">x</span></a> <a id="l:21" class="idref" href="#l:21"><span class="id" title="binder">l</span></a>,<br/>
<a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> (<a class="idref" href="Sort.html#insert"><span class="id" title="definition">insert</span></a> <a class="idref" href="Multiset.html#x:20"><span class="id" title="variable">x</span></a> <a class="idref" href="Multiset.html#l:21"><span class="id" title="variable">l</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> (<a class="idref" href="Multiset.html#x:20"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Multiset.html#l:21"><span class="id" title="variable">l</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a id="lab46"></a><h4 class="section">Exercise: 2 stars, standard (sort_contents)</h4>
<div class="paragraph"> </div>
Prove that insertion sort preserves contents. Proceed by
induction. Make use of <span class="inlinecode"><span class="id" title="var">insert_contents</span></span>.
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="sort_contents" class="idref" href="#sort_contents"><span class="id" title="lemma">sort_contents</span></a>: <span class="id" title="keyword">∀</span> <a id="l:22" class="idref" href="#l:22"><span class="id" title="binder">l</span></a>,<br/>
<a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <a class="idref" href="Multiset.html#l:22"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> (<a class="idref" href="Sort.html#sort"><span class="id" title="definition">sort</span></a> <a class="idref" href="Multiset.html#l:22"><span class="id" title="variable">l</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a id="lab47"></a><h4 class="section">Exercise: 1 star, standard (insertion_sort_correct)</h4>
<div class="paragraph"> </div>
Finish the proof of correctness!
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="insertion_sort_correct" class="idref" href="#insertion_sort_correct"><span class="id" title="lemma">insertion_sort_correct</span></a> :<br/>
<a class="idref" href="Multiset.html#is_a_sorting_algorithm'"><span class="id" title="definition">is_a_sorting_algorithm'</span></a> <a class="idref" href="Sort.html#sort"><span class="id" title="definition">sort</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a id="lab48"></a><h4 class="section">Exercise: 1 star, standard (permutations_vs_multiset)</h4>
Compare your proofs of <span class="inlinecode"><span class="id" title="var">insert_perm</span>,</span> <span class="inlinecode"><span class="id" title="var">sort_perm</span></span> with your proofs
of <span class="inlinecode"><span class="id" title="var">insert_contents</span>,</span> <span class="inlinecode"><span class="id" title="var">sort_contents</span></span>. Which proofs are simpler?
<div class="paragraph"> </div>
<ul class="doclist">
<li> <span class="inlinecode"></span> <span class="inlinecode"></span> easier with permutations
</li>
<li> <span class="inlinecode"></span> <span class="inlinecode"></span> easier with multisets
</li>
<li> <span class="inlinecode"></span> <span class="inlinecode"></span> about the same
</li>
</ul>
<div class="paragraph"> </div>
Regardless of "difficulty", which do you prefer or find easier to
think about?
<ul class="doclist">
<li> <span class="inlinecode"></span> <span class="inlinecode"></span> permutations
</li>
<li> <span class="inlinecode"></span> <span class="inlinecode"></span> multisets
</li>
</ul>
<div class="paragraph"> </div>
Put an X in one box in each list.
</div>
<div class="code">
<span class="comment">(* Do not modify the following line: *)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_permutations_vs_multiset" class="idref" href="#manual_grade_for_permutations_vs_multiset"><span class="id" title="definition">manual_grade_for_permutations_vs_multiset</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="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><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#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a id="lab49"></a><h1 class="section">Equivalence of Permutation and Multiset Specifications</h1>
<div class="paragraph"> </div>
We have developed two specifications of sorting, one based
on permutations (<span class="inlinecode"><span class="id" title="var">is_a_sorting_algorithm</span></span>) and one based on
multisets (<span class="inlinecode"><span class="id" title="var">is_a_sorting_algorithm'</span></span>). These two specifications
are actually equivalent, which will be the final theorem in this
chapter.
<div class="paragraph"> </div>
One reason for that equivalence is that permutations and multisets
are closely related. We'll begin by proving:
<div class="paragraph"> </div>
<br/>
<span class="inlinecode"> <span class="id" title="var">Permutation</span> <span class="id" title="var">al</span> <span class="id" title="var">bl</span> ↔ <span class="id" title="var">contents</span> <span class="id" title="var">al</span> = <span class="id" title="var">contents</span> <span class="id" title="var">bl</span>
</span>
<div class="paragraph"> </div>
The forward direction is relatively easy, but the backward
direction is surprisingly difficult.
<div class="paragraph"> </div>
<a id="lab50"></a><h2 class="section">The Forward Direction</h2>
<div class="paragraph"> </div>
<a id="lab51"></a><h4 class="section">Exercise: 3 stars, standard (perm_contents)</h4>
<div class="paragraph"> </div>
The forward direction is the easier one. Proceed by induction on
the evidence for <span class="inlinecode"><span class="id" title="var">Permutation</span></span> <span class="inlinecode"><span class="id" title="var">al</span></span> <span class="inlinecode"><span class="id" title="var">bl</span></span>:
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a id="perm_contents" class="idref" href="#perm_contents"><span class="id" title="lemma">perm_contents</span></a>: <span class="id" title="keyword">∀</span> <a id="al:23" class="idref" href="#al:23"><span class="id" title="binder">al</span></a> <a id="bl:24" class="idref" href="#bl:24"><span class="id" title="binder">bl</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>,<br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Sorting.Permutation.html#Permutation"><span class="id" title="inductive">Permutation</span></a> <a class="idref" href="Multiset.html#al:23"><span class="id" title="variable">al</span></a> <a class="idref" href="Multiset.html#bl:24"><span class="id" title="variable">bl</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <a class="idref" href="Multiset.html#al:23"><span class="id" title="variable">al</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <a class="idref" href="Multiset.html#bl:24"><span class="id" title="variable">bl</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a id="lab52"></a><h2 class="section">The Backward Direction (Advanced)</h2>
<div class="paragraph"> </div>
The backward direction is surprisingly difficult. This proof
approach is due to Zhong Sheng Hu. The first three lemmas are
used to prove the fourth one. Don't forget that <span class="inlinecode"><span class="id" title="var">union</span></span>,
<span class="inlinecode"><span class="id" title="var">singleton</span></span>, and <span class="inlinecode"><span class="id" title="var">empty</span></span> must be explicitly unfolded to access
their definitions.
<div class="paragraph"> </div>
<a id="lab53"></a><h4 class="section">Exercise: 2 stars, advanced (contents_nil_inv)</h4>
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a id="contents_nil_inv" class="idref" href="#contents_nil_inv"><span class="id" title="lemma">contents_nil_inv</span></a> : <span class="id" title="keyword">∀</span> <a id="l:25" class="idref" href="#l:25"><span class="id" title="binder">l</span></a>, <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <a id="x:26" class="idref" href="#x:26"><span class="id" title="binder">x</span></a>, 0 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <a class="idref" href="Multiset.html#l:25"><span class="id" title="variable">l</span></a> <a class="idref" href="Multiset.html#x:26"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Multiset.html#l:25"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nil"><span class="id" title="constructor">nil</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a id="lab54"></a><h4 class="section">Exercise: 3 stars, advanced (contents_cons_inv)</h4>
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a id="contents_cons_inv" class="idref" href="#contents_cons_inv"><span class="id" title="lemma">contents_cons_inv</span></a> : <span class="id" title="keyword">∀</span> <a id="l:27" class="idref" href="#l:27"><span class="id" title="binder">l</span></a> <a id="x:28" class="idref" href="#x:28"><span class="id" title="binder">x</span></a> <a id="n:29" class="idref" href="#n:29"><span class="id" title="binder">n</span></a>,<br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Multiset.html#n:29"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <a class="idref" href="Multiset.html#l:27"><span class="id" title="variable">l</span></a> <a class="idref" href="Multiset.html#x:28"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a><br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <a id="l<sub>1</sub>:30" class="idref" href="#l<sub>1</sub>:30"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:31" class="idref" href="#l<sub>2</sub>:31"><span class="id" title="binder">l<sub>2</sub></span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a><br/>
<a class="idref" href="Multiset.html#l:27"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#l<sub>1</sub>:30"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Multiset.html#x:28"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Multiset.html#l<sub>2</sub>:31"><span class="id" title="variable">l<sub>2</sub></span></a><br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> (<a class="idref" href="Multiset.html#l<sub>1</sub>:30"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Multiset.html#l<sub>2</sub>:31"><span class="id" title="variable">l<sub>2</sub></span></a>) <a class="idref" href="Multiset.html#x:28"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#n:29"><span class="id" title="variable">n</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a id="lab55"></a><h4 class="section">Exercise: 2 stars, advanced (contents_insert_other)</h4>
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a id="contents_insert_other" class="idref" href="#contents_insert_other"><span class="id" title="lemma">contents_insert_other</span></a> : <span class="id" title="keyword">∀</span> <a id="l<sub>1</sub>:32" class="idref" href="#l<sub>1</sub>:32"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:33" class="idref" href="#l<sub>2</sub>:33"><span class="id" title="binder">l<sub>2</sub></span></a> <a id="x:34" class="idref" href="#x:34"><span class="id" title="binder">x</span></a> <a id="y:35" class="idref" href="#y:35"><span class="id" title="binder">y</span></a>,<br/>
<a class="idref" href="Multiset.html#y:35"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'<>'_x"><span class="id" title="notation">≠</span></a> <a class="idref" href="Multiset.html#x:34"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> (<a class="idref" href="Multiset.html#l<sub>1</sub>:32"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Multiset.html#x:34"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Multiset.html#l<sub>2</sub>:33"><span class="id" title="variable">l<sub>2</sub></span></a>) <a class="idref" href="Multiset.html#y:35"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> (<a class="idref" href="Multiset.html#l<sub>1</sub>:32"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="Multiset.html#l<sub>2</sub>:33"><span class="id" title="variable">l<sub>2</sub></span></a>) <a class="idref" href="Multiset.html#y:35"><span class="id" title="variable">y</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a id="lab56"></a><h4 class="section">Exercise: 3 stars, advanced (contents_perm)</h4>
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a id="contents_perm" class="idref" href="#contents_perm"><span class="id" title="lemma">contents_perm</span></a>: <span class="id" title="keyword">∀</span> <a id="al:36" class="idref" href="#al:36"><span class="id" title="binder">al</span></a> <a id="bl:37" class="idref" href="#bl:37"><span class="id" title="binder">bl</span></a>,<br/>
<a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <a class="idref" href="Multiset.html#al:36"><span class="id" title="variable">al</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <a class="idref" href="Multiset.html#bl:37"><span class="id" title="variable">bl</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Sorting.Permutation.html#Permutation"><span class="id" title="inductive">Permutation</span></a> <a class="idref" href="Multiset.html#al:36"><span class="id" title="variable">al</span></a> <a class="idref" href="Multiset.html#bl:37"><span class="id" title="variable">bl</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">al</span> <span class="id" title="var">bl</span> <span class="id" title="var">H<sub>0</sub></span>.<br/>
<span class="id" title="tactic">assert</span> (<span class="id" title="var">H</span>: <span class="id" title="keyword">∀</span> <a id="x:39" class="idref" href="#x:39"><span class="id" title="binder">x</span></a>, <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <span class="id" title="var">al</span> <a class="idref" href="Multiset.html#x:38"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <span class="id" title="var">bl</span> <a class="idref" href="Multiset.html#x:38"><span class="id" title="variable">x</span></a>).<br/>
{ <span class="id" title="tactic">rewrite</span> <span class="id" title="var">H<sub>0</sub></span>. <span class="id" title="tactic">auto</span>. }<br/>
<span class="id" title="tactic">clear</span> <span class="id" title="var">H<sub>0</sub></span>.<br/>
<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">bl</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
<a id="lab57"></a><h2 class="section">The Main Theorem</h2>
<div class="paragraph"> </div>
With both directions proved, we can establish the correspondence
between multisets and permutations.
<div class="paragraph"> </div>
<a id="lab58"></a><h4 class="section">Exercise: 1 star, standard (same_contents_iff_perm)</h4>
<div class="paragraph"> </div>
Use <span class="inlinecode"><span class="id" title="var">contents_perm</span></span> (even if you haven't proved it) and
<span class="inlinecode"><span class="id" title="var">perm_contents</span></span> to quickly prove the next theorem.
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="same_contents_iff_perm" class="idref" href="#same_contents_iff_perm"><span class="id" title="lemma">same_contents_iff_perm</span></a>: <span class="id" title="keyword">∀</span> <a id="al:40" class="idref" href="#al:40"><span class="id" title="binder">al</span></a> <a id="bl:41" class="idref" href="#bl:41"><span class="id" title="binder">bl</span></a>,<br/>
<a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <a class="idref" href="Multiset.html#al:40"><span class="id" title="variable">al</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Multiset.html#contents"><span class="id" title="definition">contents</span></a> <a class="idref" href="Multiset.html#bl:41"><span class="id" title="variable">bl</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'<->'_x"><span class="id" title="notation">↔</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Sorting.Permutation.html#Permutation"><span class="id" title="inductive">Permutation</span></a> <a class="idref" href="Multiset.html#al:40"><span class="id" title="variable">al</span></a> <a class="idref" href="Multiset.html#bl:41"><span class="id" title="variable">bl</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
Therefore the two specifications are equivalent.
<div class="paragraph"> </div>
<a id="lab59"></a><h4 class="section">Exercise: 2 stars, standard (sort_specifications_equivalent)</h4>
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="sort_specifications_equivalent" class="idref" href="#sort_specifications_equivalent"><span class="id" title="lemma">sort_specifications_equivalent</span></a>: <span class="id" title="keyword">∀</span> <a id="sort:42" class="idref" href="#sort:42"><span class="id" title="binder">sort</span></a>,<br/>
<a class="idref" href="Sort.html#is_a_sorting_algorithm"><span class="id" title="definition">is_a_sorting_algorithm</span></a> <a class="idref" href="Multiset.html#sort:42"><span class="id" title="variable">sort</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'<->'_x"><span class="id" title="notation">↔</span></a> <a class="idref" href="Multiset.html#is_a_sorting_algorithm'"><span class="id" title="definition">is_a_sorting_algorithm'</span></a> <a class="idref" href="Multiset.html#sort:42"><span class="id" title="variable">sort</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>☐</font>
</div>
<div class="doc">
<div class="paragraph"> </div>
That means we can verify sorting algorithms using either
permutations or multisets, whichever we find more convenient.
</div>
<div class="code">
<span class="comment">(* 2024-12-27 01:32 *)</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>