-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathReferences.html
2783 lines (2386 loc) · 258 KB
/
References.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
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
<!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=iso-8859-1"/>
<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
<title>References: Typing Mutable References</title>
</head>
<script>
<!--
function toggleDisplay(id)
{
var elt = document.getElementById(id);
if (elt.style.display == 'none') {
elt.style.display = 'block';
} else {
elt.style.display = 'none';
}
}
function hideAll(cls)
{
var testClass = new RegExp("(^|s)" + cls + "(s|$)");
var tag = tag || "*";
var elements = document.getElementsByTagName("div");
var current;
var length = elements.length;
for(var i=0; i<length; i++){
current = elements[i];
if(testClass.test(current.className)) {
current.style.display = 'none';
}
}
}
// -->
</script>
<body onLoad="hideAll('proofscript')">
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">References<span class="subtitle">Typing Mutable References</span></h1>
<div class="code code-tight">
</div>
<div class="doc">
</div>
<div class="code code-tight">
<br/>
<span class="comment">(* $Date: 2012-04-23 13:24:50 -0400 (Mon, 23 Apr 2012) $ *)</span><br/>
<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Smallstep</span>.<br/>
<br/>
</div>
<div class="doc">
So far, we have considered a variety of <i>pure</i> language features,
including functional abstraction, basic types such as numbers and
booleans, and structured types such as records and variants. These
features form the backbone of most programming languages — including
purely functional languages such as Haskell, "mostly functional"
languages such as ML, imperative languages such as C, and
object-oriented languages such as Java.
<div class="paragraph"> </div>
Most practical programming languages also include various <i>impure</i>
features that cannot be described in the simple semantic framework
we have used so far. In particular, besides just yielding
results, evaluation of terms in these languages may assign to
mutable variables (reference cells, arrays, mutable record fields,
etc.), perform input and output to files, displays, or network
connections, make non-local transfers of control via exceptions,
jumps, or continuations, engage in inter-process synchronization
and communication, and so on. In the literature on programming
languages, such "side effects" of computation are more generally
referred to as <i>computational effects</i>.
<div class="paragraph"> </div>
In this chapter, we'll see how one sort of computational
effect — mutable references — can be added to the calculi we have
studied. The main extension will be dealing explicitly with a
<i>store</i> (or <i>heap</i>). This extension is straightforward to define;
the most interesting part is the refinement we need to make to the
statement of the type preservation theorem.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab643"></a><h2 class="section">Definitions</h2>
<div class="paragraph"> </div>
Pretty much every programming language provides some form of
assignment operation that changes the contents of a previously
allocated piece of storage. (Coq's internal language is a rare
exception!)
<div class="paragraph"> </div>
In some languages — notably ML and its relatives — the
mechanisms for name-binding and those for assignment are kept
separate. We can have a variable <span class="inlinecode"><span class="id" type="var">x</span></span> whose <i>value</i> is the number
<span class="inlinecode">5</span>, or we can have a variable <span class="inlinecode"><span class="id" type="var">y</span></span> whose value is a
<i>reference</i> (or <i>pointer</i>) to a mutable cell whose current
contents is <span class="inlinecode">5</span>. These are different things, and the difference
is visible to the programmer. We can add <span class="inlinecode"><span class="id" type="var">x</span></span> to another number,
but not assign to it. We can use <span class="inlinecode"><span class="id" type="var">y</span></span> directly to assign a new
value to the cell that it points to (by writing <span class="inlinecode"><span class="id" type="var">y</span>:=84</span>), but we
cannot use it directly as an argument to an operation like <span class="inlinecode">+</span>.
Instead, we must explicitly <i>dereference</i> it, writing <span class="inlinecode">!<span class="id" type="var">y</span></span> to
obtain its current contents.
<div class="paragraph"> </div>
In most other languages — in particular, in all members of the C
family, including Java — <i>every</i> variable name refers to a mutable
cell, and the operation of dereferencing a variable to obtain its
current contents is implicit.
<div class="paragraph"> </div>
For purposes of formal study, it is useful to keep these
mechanisms separate. The development in this chapter will closely
follow ML's model. Applying the lessons learned here to C-like
languages is a straightforward matter of collapsing some
distinctions and rendering some operations such as dereferencing
implicit instead of explicit.
<div class="paragraph"> </div>
In this chapter, we study adding mutable references to the
simply-typed lambda calculus with natural numbers.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab644"></a><h2 class="section">Syntax</h2>
</div>
<div class="code code-space">
<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">STLCRef</span>.<br/>
<br/>
</div>
<div class="doc">
The basic operations on references are <i>allocation</i>,
<i>dereferencing</i>, and <i>assignment</i>.
<div class="paragraph"> </div>
<ul class="doclist">
<li> To allocate a reference, we use the <span class="inlinecode"><span class="id" type="var">ref</span></span> operator, providing
an initial value for the new cell. For example, <span class="inlinecode"><span class="id" type="var">ref</span></span> <span class="inlinecode">5</span>
creates a new cell containing the value <span class="inlinecode">5</span>, and evaluates to
a reference to that cell.
<div class="paragraph"> </div>
</li>
<li> To read the current value of this cell, we use the
dereferencing operator <span class="inlinecode">!</span>; for example, <span class="inlinecode">!(<span class="id" type="var">ref</span></span> <span class="inlinecode">5)</span> evaluates
to <span class="inlinecode">5</span>.
<div class="paragraph"> </div>
</li>
<li> To change the value stored in a cell, we use the assignment
operator. If <span class="inlinecode"><span class="id" type="var">r</span></span> is a reference, <span class="inlinecode"><span class="id" type="var">r</span></span> <span class="inlinecode">:=</span> <span class="inlinecode">7</span> will store the
value <span class="inlinecode">7</span> in the cell referenced by <span class="inlinecode"><span class="id" type="var">r</span></span>. However, <span class="inlinecode"><span class="id" type="var">r</span></span> <span class="inlinecode">:=</span> <span class="inlinecode">7</span>
evaluates to the trivial value <span class="inlinecode"><span class="id" type="var">unit</span></span>; it exists only to have
the <i>side effect</i> of modifying the contents of a cell.
</li>
</ul>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab645"></a><h3 class="section">Types</h3>
<div class="paragraph"> </div>
We start with the simply typed lambda calculus over the
natural numbers. To the base natural number type and arrow types
we need to add two more types to deal with references. First, we
need the <i>unit type</i>, which we will use as the result type of an
assignment operation. We then add <i>reference types</i>. If <span class="inlinecode"><span class="id" type="var">T</span></span> is a type, then <span class="inlinecode"><span class="id" type="var">Ref</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> is the type of references which
point to a cell holding values of type <span class="inlinecode"><span class="id" type="var">T</span></span>.
<pre>
T ::= Nat
| Unit
| T -> T
| Ref T
</pre>
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">ty</span> : <span class="id" type="keyword">Type</span> :=<br/>
| <span class="id" type="var">TNat</span> : <span class="id" type="var">ty</span><br/>
| <span class="id" type="var">TUnit</span> : <span class="id" type="var">ty</span><br/>
| <span class="id" type="var">TArrow</span> : <span class="id" type="var">ty</span> <span style="font-family: arial;">→</span> <span class="id" type="var">ty</span> <span style="font-family: arial;">→</span> <span class="id" type="var">ty</span><br/>
| <span class="id" type="var">TRef</span> : <span class="id" type="var">ty</span> <span style="font-family: arial;">→</span> <span class="id" type="var">ty</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab646"></a><h3 class="section">Terms</h3>
<div class="paragraph"> </div>
Besides variables, abstractions, applications,
natural-number-related terms, and <span class="inlinecode"><span class="id" type="var">unit</span></span>, we need four more sorts
of terms in order to handle mutable references:
<pre>
t ::= ... Terms
| ref t allocation
| !t dereference
| t := t assignment
| l location
</pre>
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">tm</span> : <span class="id" type="keyword">Type</span> :=<br/>
<span class="comment">(* STLC with numbers: *)</span><br/>
| <span class="id" type="var">tvar</span> : <span class="id" type="var">id</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span><br/>
| <span class="id" type="var">tapp</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span><br/>
| <span class="id" type="var">tabs</span> : <span class="id" type="var">id</span> <span style="font-family: arial;">→</span> <span class="id" type="var">ty</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span><br/>
| <span class="id" type="var">tnat</span> : <span class="id" type="var">nat</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span><br/>
| <span class="id" type="var">tsucc</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span><br/>
| <span class="id" type="var">tpred</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span><br/>
| <span class="id" type="var">tmult</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span><br/>
| <span class="id" type="var">tif0</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span><br/>
<span class="comment">(* New terms: *)</span><br/>
| <span class="id" type="var">tunit</span> : <span class="id" type="var">tm</span><br/>
| <span class="id" type="var">tref</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span><br/>
| <span class="id" type="var">tderef</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span><br/>
| <span class="id" type="var">tassign</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span><br/>
| <span class="id" type="var">tloc</span> : <span class="id" type="var">nat</span> <span style="font-family: arial;">→</span> <span class="id" type="var">tm</span>.<br/>
<br/>
</div>
<div class="doc">
Intuitively...
<div class="paragraph"> </div>
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">ref</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span> (formally, <span class="inlinecode"><span class="id" type="var">tref</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span>) allocates a new reference cell
with the value <span class="inlinecode"><span class="id" type="var">t</span></span> and evaluates to the location of the newly
allocated cell;
<div class="paragraph"> </div>
</li>
<li> <span class="inlinecode">!<span class="id" type="var">t</span></span> (formally, <span class="inlinecode"><span class="id" type="var">tderef</span></span> <span class="inlinecode"><span class="id" type="var">t</span></span>) evaluates to the contents of the
cell referenced by <span class="inlinecode"><span class="id" type="var">t</span></span>;
<div class="paragraph"> </div>
</li>
<li> <span class="inlinecode"><span class="id" type="var">t1</span></span> <span class="inlinecode">:=</span> <span class="inlinecode"><span class="id" type="var">t2</span></span> (formally, <span class="inlinecode"><span class="id" type="var">tassign</span></span> <span class="inlinecode"><span class="id" type="var">t1</span></span> <span class="inlinecode"><span class="id" type="var">t2</span></span>) assigns <span class="inlinecode"><span class="id" type="var">t2</span></span> to the
cell referenced by <span class="inlinecode"><span class="id" type="var">t1</span></span>; and
<div class="paragraph"> </div>
</li>
<li> <span class="inlinecode"><span class="id" type="var">l</span></span> (formally, <span class="inlinecode"><span class="id" type="var">tloc</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span>) is a reference to the cell at
location <span class="inlinecode"><span class="id" type="var">l</span></span>. We'll discuss locations later.
</li>
</ul>
<div class="paragraph"> </div>
In informal examples, we'll also freely use the extensions
of the STLC developed in the <span class="inlinecode"><span class="id" type="var">MoreStlc</span></span> chapter; however, to keep
the proofs small, we won't bother formalizing them again here. It
would be easy to do so, since there are no very interesting
interactions between those features and references.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Tactic Notation</span> "t_cases" <span class="id" type="var">tactic</span>(<span class="id" type="var">first</span>) <span class="id" type="var">ident</span>(<span class="id" type="var">c</span>) :=<br/>
<span class="id" type="var">first</span>;<br/>
[ <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tvar" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tapp" <br/>
| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tabs" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tzero" <br/>
| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tsucc" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tpred"<br/>
| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tmult" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tif0"<br/>
| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tunit" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tref" <br/>
| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tderef" | <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tassign" <br/>
| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "tloc" ].<br/>
<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">ExampleVariables</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">x</span> := <span class="id" type="var">Id</span> 0.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">y</span> := <span class="id" type="var">Id</span> 1.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">r</span> := <span class="id" type="var">Id</span> 2.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">s</span> := <span class="id" type="var">Id</span> 3.<br/>
<br/>
<span class="id" type="keyword">End</span> <span class="id" type="var">ExampleVariables</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab647"></a><h3 class="section">Typing (Preview)</h3>
<div class="paragraph"> </div>
Informally, the typing rules for allocation, dereferencing, and
assignment will look like this:
<center><table class="infrule">
<tr class="infruleassumption">
<td class="infrule"><span style="font-family: serif; font-size:85%;">Γ</span> <span style="font-family: arial;">⊢</span> t1 : T1</td>
<td class="infrulenamecol" rowspan="3">
(T_Ref)
</td></tr>
<tr class="infrulemiddle">
<td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
<td class="infrule"><span style="font-family: serif; font-size:85%;">Γ</span> <span style="font-family: arial;">⊢</span> ref t1 : Ref T1</td>
<td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
<td class="infrule"><span style="font-family: serif; font-size:85%;">Γ</span> <span style="font-family: arial;">⊢</span> t1 : Ref T11</td>
<td class="infrulenamecol" rowspan="3">
(T_Deref)
</td></tr>
<tr class="infrulemiddle">
<td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
<td class="infrule"><span style="font-family: serif; font-size:85%;">Γ</span> <span style="font-family: arial;">⊢</span> !t1 : T11</td>
<td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
<td class="infrule"><span style="font-family: serif; font-size:85%;">Γ</span> <span style="font-family: arial;">⊢</span> t1 : Ref T11</td>
<td></td>
</td>
<tr class="infruleassumption">
<td class="infrule"><span style="font-family: serif; font-size:85%;">Γ</span> <span style="font-family: arial;">⊢</span> t2 : T11</td>
<td class="infrulenamecol" rowspan="3">
(T_Assign)
</td></tr>
<tr class="infrulemiddle">
<td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
<td class="infrule"><span style="font-family: serif; font-size:85%;">Γ</span> <span style="font-family: arial;">⊢</span> t1 := t2 : Unit</td>
<td></td>
</td>
</table></center> The rule for locations will require a bit more machinery, and this
will motivate some changes to the other rules; we'll come back to
this later.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab648"></a><h3 class="section">Values and Substitution</h3>
<div class="paragraph"> </div>
Besides abstractions and numbers, we have two new types of values:
the unit value, and locations.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">value</span> : <span class="id" type="var">tm</span> <span style="font-family: arial;">→</span> <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">v_abs</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">t</span>,<br/>
<span class="id" type="var">value</span> (<span class="id" type="var">tabs</span> <span class="id" type="var">x</span> <span class="id" type="var">T</span> <span class="id" type="var">t</span>)<br/>
| <span class="id" type="var">v_nat</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">n</span>,<br/>
<span class="id" type="var">value</span> (<span class="id" type="var">tnat</span> <span class="id" type="var">n</span>)<br/>
| <span class="id" type="var">v_unit</span> : <br/>
<span class="id" type="var">value</span> <span class="id" type="var">tunit</span><br/>
| <span class="id" type="var">v_loc</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">l</span>,<br/>
<span class="id" type="var">value</span> (<span class="id" type="var">tloc</span> <span class="id" type="var">l</span>).<br/>
<br/>
<span class="id" type="keyword">Hint</span> <span class="id" type="var">Constructors</span> <span class="id" type="var">value</span>.<br/>
<br/>
</div>
<div class="doc">
Extending substitution to handle the new syntax of terms is
straightforward.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="tactic">subst</span> (<span class="id" type="var">x</span>:<span class="id" type="var">id</span>) (<span class="id" type="var">s</span>:<span class="id" type="var">tm</span>) (<span class="id" type="var">t</span>:<span class="id" type="var">tm</span>) : <span class="id" type="var">tm</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">t</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">tvar</span> <span class="id" type="var">x'</span> => <br/>
<span class="id" type="keyword">if</span> <span class="id" type="var">beq_id</span> <span class="id" type="var">x</span> <span class="id" type="var">x'</span> <span class="id" type="keyword">then</span> <span class="id" type="var">s</span> <span class="id" type="keyword">else</span> <span class="id" type="var">t</span><br/>
| <span class="id" type="var">tapp</span> <span class="id" type="var">t1</span> <span class="id" type="var">t2</span> => <br/>
<span class="id" type="var">tapp</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t1</span>) (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t2</span>)<br/>
| <span class="id" type="var">tabs</span> <span class="id" type="var">x'</span> <span class="id" type="var">T</span> <span class="id" type="var">t1</span> => <br/>
<span class="id" type="keyword">if</span> <span class="id" type="var">beq_id</span> <span class="id" type="var">x</span> <span class="id" type="var">x'</span> <span class="id" type="keyword">then</span> <span class="id" type="var">t</span> <span class="id" type="keyword">else</span> <span class="id" type="var">tabs</span> <span class="id" type="var">x'</span> <span class="id" type="var">T</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t1</span>)<br/>
| <span class="id" type="var">tnat</span> <span class="id" type="var">n</span> => <br/>
<span class="id" type="var">t</span><br/>
| <span class="id" type="var">tsucc</span> <span class="id" type="var">t1</span> => <br/>
<span class="id" type="var">tsucc</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t1</span>)<br/>
| <span class="id" type="var">tpred</span> <span class="id" type="var">t1</span> => <br/>
<span class="id" type="var">tpred</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t1</span>)<br/>
| <span class="id" type="var">tmult</span> <span class="id" type="var">t1</span> <span class="id" type="var">t2</span> => <br/>
<span class="id" type="var">tmult</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t1</span>) (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t2</span>)<br/>
| <span class="id" type="var">tif0</span> <span class="id" type="var">t1</span> <span class="id" type="var">t2</span> <span class="id" type="var">t3</span> => <br/>
<span class="id" type="var">tif0</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t1</span>) (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t2</span>) (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t3</span>)<br/>
| <span class="id" type="var">tunit</span> => <br/>
<span class="id" type="var">t</span><br/>
| <span class="id" type="var">tref</span> <span class="id" type="var">t1</span> => <br/>
<span class="id" type="var">tref</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t1</span>)<br/>
| <span class="id" type="var">tderef</span> <span class="id" type="var">t1</span> => <br/>
<span class="id" type="var">tderef</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t1</span>)<br/>
| <span class="id" type="var">tassign</span> <span class="id" type="var">t1</span> <span class="id" type="var">t2</span> => <br/>
<span class="id" type="var">tassign</span> (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t1</span>) (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t2</span>)<br/>
| <span class="id" type="var">tloc</span> <span class="id" type="var">_</span> => <br/>
<span class="id" type="var">t</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
<span class="id" type="keyword">Notation</span> "'[' x ':=' s ']' t" := (<span class="id" type="tactic">subst</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> <span class="id" type="var">t</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 20).<br/>
<br/>
</div>
<div class="doc">
<a name="lab649"></a><h1 class="section">Pragmatics</h1>
</div>
<div class="code code-space">
<br/>
</div>
<div class="doc">
<a name="lab650"></a><h2 class="section">Side Effects and Sequencing</h2>
<div class="paragraph"> </div>
The fact that the result of an assignment expression is the
trivial value <span class="inlinecode"><span class="id" type="var">unit</span></span> allows us to use a nice abbreviation for
<i>sequencing</i>. For example, we can write
<pre>
r:=succ(!r); !r
</pre>
as an abbreviation for
<pre>
(\x:Unit. !r) (r := succ(!r)).
</pre>
This has the effect of evaluating two expressions in order and
returning the value of the second. Restricting the type of the first
expression to <span class="inlinecode"><span class="id" type="var">Unit</span></span> helps the typechecker to catch some silly
errors by permitting us to throw away the first value only if it
is really guaranteed to be trivial.
<div class="paragraph"> </div>
Notice that, if the second expression is also an assignment, then
the type of the whole sequence will be <span class="inlinecode"><span class="id" type="var">Unit</span></span>, so we can validly
place it to the left of another <span class="inlinecode">;</span> to build longer sequences of
assignments:
<pre>
r:=succ(!r); r:=succ(!r); r:=succ(!r); r:=succ(!r); !r
</pre>
<div class="paragraph"> </div>
Formally, we introduce sequencing as a "derived form"
<span class="inlinecode"><span class="id" type="var">tseq</span></span> that expands into an abstraction and an application.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">tseq</span> <span class="id" type="var">t1</span> <span class="id" type="var">t2</span> := <br/>
<span class="id" type="var">tapp</span> (<span class="id" type="var">tabs</span> (<span class="id" type="var">Id</span> 0) <span class="id" type="var">TUnit</span> <span class="id" type="var">t2</span>) <span class="id" type="var">t1</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab651"></a><h2 class="section">References and Aliasing</h2>
<div class="paragraph"> </div>
It is important to bear in mind the difference between the
<i>reference</i> that is bound to <span class="inlinecode"><span class="id" type="var">r</span></span> and the <i>cell</i> in the store that
is pointed to by this reference.
<div class="paragraph"> </div>
If we make a copy of <span class="inlinecode"><span class="id" type="var">r</span></span>, for example by binding its value to
another variable <span class="inlinecode"><span class="id" type="var">s</span></span>, what gets copied is only the <i>reference</i>,
not the contents of the cell itself.
<div class="paragraph"> </div>
For example, after evaluating
<pre>
let r = ref 5 in
let s = r in
s := 82;
(!r)+1
</pre>
the cell referenced by <span class="inlinecode"><span class="id" type="var">r</span></span> will contain the value <span class="inlinecode">82</span>, while the
result of the whole expression will be <span class="inlinecode">83</span>. The references <span class="inlinecode"><span class="id" type="var">r</span></span>
and <span class="inlinecode"><span class="id" type="var">s</span></span> are said to be <i>aliases</i> for the same cell.
<div class="paragraph"> </div>
The possibility of aliasing can make programs with references
quite tricky to reason about. For example, the expression
<pre>
r := 5; r := !s
</pre>
assigns <span class="inlinecode">5</span> to <span class="inlinecode"><span class="id" type="var">r</span></span> and then immediately overwrites it with <span class="inlinecode"><span class="id" type="var">s</span></span>'s
current value; this has exactly the same effect as the single
assignment
<pre>
r := !s
</pre>
<i>unless</i> we happen to do it in a context where <span class="inlinecode"><span class="id" type="var">r</span></span> and <span class="inlinecode"><span class="id" type="var">s</span></span> are
aliases for the same cell!
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab652"></a><h2 class="section">Shared State</h2>
<div class="paragraph"> </div>
Of course, aliasing is also a large part of what makes references
useful. In particular, it allows us to set up "implicit
communication channels" — shared state — between different parts
of a program. For example, suppose we define a reference cell and
two functions that manipulate its contents:
<pre>
let c = ref 0 in
let incc = \_:Unit. (c := succ (!c); !c) in
let decc = \_:Unit. (c := pred (!c); !c) in
...
</pre>
<div class="paragraph"> </div>
Note that, since their argument types are <span class="inlinecode"><span class="id" type="var">Unit</span></span>, the
abstractions in the definitions of <span class="inlinecode"><span class="id" type="var">incc</span></span> and <span class="inlinecode"><span class="id" type="var">decc</span></span> are not
providing any useful information to the bodies of the
functions (using the wildcard <span class="inlinecode"><span class="id" type="var">_</span></span> as the name of the bound
variable is a reminder of this). Instead, their purpose is to
"slow down" the execution of the function bodies: since function
abstractions are values, the two <span class="inlinecode"><span class="id" type="keyword">let</span></span>s are executed simply by
binding these functions to the names <span class="inlinecode"><span class="id" type="var">incc</span></span> and <span class="inlinecode"><span class="id" type="var">decc</span></span>, rather
than by actually incrementing or decrementing <span class="inlinecode"><span class="id" type="var">c</span></span>. Later, each
call to one of these functions results in its body being executed
once and performing the appropriate mutation on <span class="inlinecode"><span class="id" type="var">c</span></span>. Such
functions are often called <i>thunks</i>.
<div class="paragraph"> </div>
In the context of these declarations, calling <span class="inlinecode"><span class="id" type="var">incc</span></span> results in
changes to <span class="inlinecode"><span class="id" type="var">c</span></span> that can be observed by calling <span class="inlinecode"><span class="id" type="var">decc</span></span>. For
example, if we replace the <span class="inlinecode">...</span> with <span class="inlinecode">(<span class="id" type="var">incc</span></span> <span class="inlinecode"><span class="id" type="var">unit</span>;</span> <span class="inlinecode"><span class="id" type="var">incc</span></span> <span class="inlinecode"><span class="id" type="var">unit</span>;</span> <span class="inlinecode"><span class="id" type="var">decc</span></span>
<span class="inlinecode"><span class="id" type="var">unit</span>)</span>, the result of the whole program will be <span class="inlinecode">1</span>. <a name="lab653"></a><h2 class="section">Objects</h2>
<div class="paragraph"> </div>
We can go a step further and write a <i>function</i> that creates <span class="inlinecode"><span class="id" type="var">c</span></span>,
<span class="inlinecode"><span class="id" type="var">incc</span></span>, and <span class="inlinecode"><span class="id" type="var">decc</span></span>, packages <span class="inlinecode"><span class="id" type="var">incc</span></span> and <span class="inlinecode"><span class="id" type="var">decc</span></span> together into a
record, and returns this record:
<pre>
newcounter =
\_:Unit.
let c = ref 0 in
let incc = \_:Unit. (c := succ (!c); !c) in
let decc = \_:Unit. (c := pred (!c); !c) in
{i=incc, d=decc}
</pre>
Now, each time we call <span class="inlinecode"><span class="id" type="var">newcounter</span></span>, we get a new record of
functions that share access to the same storage cell <span class="inlinecode"><span class="id" type="var">c</span></span>. The
caller of <span class="inlinecode"><span class="id" type="var">newcounter</span></span> can't get at this storage cell directly,
but can affect it indirectly by calling the two functions. In
other words, we've created a simple form of <i>object</i>.
<pre>
let c1 = newcounter unit in
let c2 = newcounter unit in
// Note that we've allocated two separate storage cells now!
let r1 = c1.i unit in
let r2 = c2.i unit in
r2 // yields 1, not 2!
</pre>
<a name="lab654"></a><h4 class="section">Exercise: 1 star (store_draw)</h4>
Draw (on paper) the contents of the store at the point in
execution where the first two <span class="inlinecode"><span class="id" type="keyword">let</span></span>s have finished and the third
one is about to begin.
</div>
<div class="code code-tight">
<br/>
<span class="comment">(* FILL IN HERE *)</span><br/>
</div>
<div class="doc">
<font size=-2>☐</font>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab655"></a><h2 class="section">References to Compound Types</h2>
<div class="paragraph"> </div>
A reference cell need not contain just a number: the primitives
we've defined above allow us to create references to values of any
type, including functions. For example, we can use references to
functions to give a (not very efficient) implementation of arrays
of numbers, as follows. Write <span class="inlinecode"><span class="id" type="var">NatArray</span></span> for the type
<span class="inlinecode"><span class="id" type="var">Ref</span></span> <span class="inlinecode">(<span class="id" type="var">Nat</span><span style="font-family: arial;">→</span><span class="id" type="var">Nat</span>)</span>.
<div class="paragraph"> </div>
Recall the <span class="inlinecode"><span class="id" type="var">equal</span></span> function from the <span class="inlinecode"><span class="id" type="var">MoreStlc</span></span> chapter:
<pre>
equal =
fix
(\eq:Nat->Nat->Bool.
\m:Nat. \n:Nat.
if m=0 then iszero n
else if n=0 then false
else eq (pred m) (pred n))
</pre>
Now, to build a new array, we allocate a reference cell and fill
it with a function that, when given an index, always returns <span class="inlinecode">0</span>.
<pre>
newarray = \_:Unit. ref (\n:Nat.0)
</pre>
To look up an element of an array, we simply apply
the function to the desired index.
<pre>
lookup = \a:NatArray. \n:Nat. (!a) n
</pre>
The interesting part of the encoding is the <span class="inlinecode"><span class="id" type="var">update</span></span> function. It
takes an array, an index, and a new value to be stored at that index, and
does its job by creating (and storing in the reference) a new function
that, when it is asked for the value at this very index, returns the new
value that was given to <span class="inlinecode"><span class="id" type="var">update</span></span>, and on all other indices passes the
lookup to the function that was previously stored in the reference.
<pre>
update = \a:NatArray. \m:Nat. \v:Nat.
let oldf = !a in
a := (\n:Nat. if equal m n then v else oldf n);
</pre>
References to values containing other references can also be very
useful, allowing us to define data structures such as mutable
lists and trees.
<div class="paragraph"> </div>
<a name="lab656"></a><h4 class="section">Exercise: 2 stars (compact_update)</h4>
If we defined <span class="inlinecode"><span class="id" type="var">update</span></span> more compactly like this
<pre>
update = \a:NatArray. \m:Nat. \v:Nat.
a := (\n:Nat. if equal m n then v else (!a) n)
</pre>
would it behave the same?
</div>
<div class="code code-tight">
<br/>
<span class="comment">(* FILL IN HERE *)</span><br/>
</div>
<div class="doc">
<font size=-2>☐</font>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab657"></a><h2 class="section">Null References</h2>
<div class="paragraph"> </div>
There is one more difference between our references and C-style
mutable variables: in C-like languages, variables holding pointers
into the heap may sometimes have the value <span class="inlinecode"><span class="id" type="var">NULL</span></span>. Dereferencing
such a "null pointer" is an error, and results in an
exception (Java) or in termination of the program (C).
<div class="paragraph"> </div>
Null pointers cause significant trouble in C-like languages: the
fact that any pointer might be null means that any dereference
operation in the program can potentially fail. However, even in
ML-like languages, there are occasionally situations where we may
or may not have a valid pointer in our hands. Fortunately, there
is no need to extend the basic mechanisms of references to achieve
this: the sum types introduced in the <span class="inlinecode"><span class="id" type="var">MoreStlc</span></span> chapter already
give us what we need.
<div class="paragraph"> </div>
First, we can use sums to build an analog of the <span class="inlinecode"><span class="id" type="var">option</span></span> types
introduced in the <span class="inlinecode"><span class="id" type="var">Lists</span></span> chapter. Define <span class="inlinecode"><span class="id" type="var">Option</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> to be an
abbreviation for <span class="inlinecode"><span class="id" type="var">Unit</span></span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">T</span></span>.
<div class="paragraph"> </div>
Then a "nullable reference to a <span class="inlinecode"><span class="id" type="var">T</span></span>" is simply an element of the
type <span class="inlinecode"><span class="id" type="var">Option</span></span> <span class="inlinecode">(<span class="id" type="var">Ref</span></span> <span class="inlinecode"><span class="id" type="var">T</span>)</span>.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab658"></a><h2 class="section">Garbage Collection</h2>
<div class="paragraph"> </div>
A last issue that we should mention before we move on with
formalizing references is storage <i>de</i>-allocation. We have not
provided any primitives for freeing reference cells when they are
no longer needed. Instead, like many modern languages (including
ML and Java) we rely on the run-time system to perform <i>garbage
collection</i>, collecting and reusing cells that can no longer be
reached by the program.
<div class="paragraph"> </div>
This is <i>not</i> just a question of taste in language design: it is
extremely difficult to achieve type safety in the presence of an
explicit deallocation operation. The reason for this is the
familiar <i>dangling reference</i> problem: we allocate a cell holding
a number, save a reference to it in some data structure, use it
for a while, then deallocate it and allocate a new cell holding a
boolean, possibly reusing the same storage. Now we can have two
names for the same storage cell — one with type <span class="inlinecode"><span class="id" type="var">Ref</span></span> <span class="inlinecode"><span class="id" type="var">Nat</span></span> and the
other with type <span class="inlinecode"><span class="id" type="var">Ref</span></span> <span class="inlinecode"><span class="id" type="var">Bool</span></span>.
<div class="paragraph"> </div>
<a name="lab659"></a><h4 class="section">Exercise: 1 star (type_safety_violation)</h4>
Show how this can lead to a violation of type safety.
</div>
<div class="code code-tight">
<br/>
<span class="comment">(* FILL IN HERE *)</span><br/>
</div>
<div class="doc">
<font size=-2>☐</font>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab660"></a><h1 class="section">Operational Semantics</h1>
</div>
<div class="code code-space">
<br/>
</div>
<div class="doc">
<a name="lab661"></a><h2 class="section">Locations</h2>
<div class="paragraph"> </div>
The most subtle aspect of the treatment of references
appears when we consider how to formalize their operational
behavior. One way to see why is to ask, "What should be the
<i>values</i> of type <span class="inlinecode"><span class="id" type="var">Ref</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span>?" The crucial observation that we need
to take into account is that evaluating a <span class="inlinecode"><span class="id" type="var">ref</span></span> operator should
<i>do</i> something — namely, allocate some storage — and the result
of the operation should be a reference to this storage.
<div class="paragraph"> </div>
What, then, is a reference?
<div class="paragraph"> </div>
The run-time store in most programming language implementations is
essentially just a big array of bytes. The run-time system keeps track
of which parts of this array are currently in use; when we need to
allocate a new reference cell, we allocate a large enough segment from
the free region of the store (4 bytes for integer cells, 8 bytes for
cells storing <span class="inlinecode"><span class="id" type="var">Float</span></span>s, etc.), mark it as being used, and return the
index (typically, a 32- or 64-bit integer) of the start of the newly
allocated region. These indices are references.
<div class="paragraph"> </div>
For present purposes, there is no need to be quite so concrete.
We can think of the store as an array of <i>values</i>, rather than an
array of bytes, abstracting away from the different sizes of the
run-time representations of different values. A reference, then,
is simply an index into the store. (If we like, we can even
abstract away from the fact that these indices are numbers, but
for purposes of formalization in Coq it is a bit more convenient
to use numbers.) We'll use the word <i>location</i> instead of
<i>reference</i> or <i>pointer</i> from now on to emphasize this abstract
quality.
<div class="paragraph"> </div>
Treating locations abstractly in this way will prevent us from
modeling the <i>pointer arithmetic</i> found in low-level languages
such as C. This limitation is intentional. While pointer
arithmetic is occasionally very useful, especially for
implementing low-level services such as garbage collectors, it
cannot be tracked by most type systems: knowing that location <span class="inlinecode"><span class="id" type="var">n</span></span>
in the store contains a <span class="inlinecode"><span class="id" type="var">float</span></span> doesn't tell us anything useful
about the type of location <span class="inlinecode"><span class="id" type="var">n</span>+4</span>. In C, pointer arithmetic is a
notorious source of type safety violations.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab662"></a><h2 class="section">Stores</h2>
<div class="paragraph"> </div>
Recall that, in the small-step operational semantics for
IMP, the step relation needed to carry along an auxiliary state in
addition to the program being executed. In the same way, once we
have added reference cells to the STLC, our step relation must
carry along a store to keep track of the contents of reference
cells.
<div class="paragraph"> </div>
We could re-use the same functional representation we used for
states in IMP, but for carrying out the proofs in this chapter it
is actually more convenient to represent a store simply as a
<i>list</i> of values. (The reason we couldn't use this representation
before is that, in IMP, a program could modify any location at any
time, so states had to be ready to map <i>any</i> variable to a value.
However, in the STLC with references, the only way to create a
reference cell is with <span class="inlinecode"><span class="id" type="var">tref</span></span> <span class="inlinecode"><span class="id" type="var">t1</span></span>, which puts the value of <span class="inlinecode"><span class="id" type="var">t1</span></span>
in a new reference cell and evaluates to the location of the newly
created reference cell. When evaluating such an expression, we can
just add a new reference cell to the end of the list representing
the store.)
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">store</span> := <span class="id" type="var">list</span> <span class="id" type="var">tm</span>.<br/>
<br/>
</div>
<div class="doc">
We use <span class="inlinecode"><span class="id" type="var">store_lookup</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> to retrieve the value of the reference
cell at location <span class="inlinecode"><span class="id" type="var">n</span></span> in the store <span class="inlinecode"><span class="id" type="var">st</span></span>. Note that we must give a
default value to <span class="inlinecode"><span class="id" type="var">nth</span></span> in case we try looking up an index which is
too large. (In fact, we will never actually do this, but proving
it will of course require some work!)
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">store_lookup</span> (<span class="id" type="var">n</span>:<span class="id" type="var">nat</span>) (<span class="id" type="var">st</span>:<span class="id" type="var">store</span>) :=<br/>
<span class="id" type="var">nth</span> <span class="id" type="var">n</span> <span class="id" type="var">st</span> <span class="id" type="var">tunit</span>.<br/>
<br/>
</div>
<div class="doc">
To add a new reference cell to the store, we use <span class="inlinecode"><span class="id" type="var">snoc</span></span>.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">snoc</span> {<span class="id" type="var">A</span>:<span class="id" type="keyword">Type</span>} (<span class="id" type="var">l</span>:<span class="id" type="var">list</span> <span class="id" type="var">A</span>) (<span class="id" type="var">x</span>:<span class="id" type="var">A</span>) : <span class="id" type="var">list</span> <span class="id" type="var">A</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">nil</span> => <span class="id" type="var">x</span> :: <span class="id" type="var">nil</span><br/>
| <span class="id" type="var">h</span> :: <span class="id" type="var">t</span> => <span class="id" type="var">h</span> :: <span class="id" type="var">snoc</span> <span class="id" type="var">t</span> <span class="id" type="var">x</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
We will need some boring lemmas about <span class="inlinecode"><span class="id" type="var">snoc</span></span>. The proofs are
routine inductions.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">length_snoc</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">A</span> (<span class="id" type="var">l</span>:<span class="id" type="var">list</span> <span class="id" type="var">A</span>) <span class="id" type="var">x</span>,<br/>
<span class="id" type="var">length</span> (<span class="id" type="var">snoc</span> <span class="id" type="var">l</span> <span class="id" type="var">x</span>) = <span class="id" type="var">S</span> (<span class="id" type="var">length</span> <span class="id" type="var">l</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">l</span>; <span class="id" type="tactic">intros</span>; [ <span class="id" type="tactic">auto</span> | <span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHl</span>; <span class="id" type="tactic">auto</span> ]. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="comment">(* The "solve by inversion" tactic is explained in Stlc.v. *)</span><br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">nth_lt_snoc</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">A</span> (<span class="id" type="var">l</span>:<span class="id" type="var">list</span> <span class="id" type="var">A</span>) <span class="id" type="var">x</span> <span class="id" type="var">d</span> <span class="id" type="var">n</span>,<br/>
<span class="id" type="var">n</span> < <span class="id" type="var">length</span> <span class="id" type="var">l</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">nth</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span> <span class="id" type="var">d</span> = <span class="id" type="var">nth</span> <span class="id" type="var">n</span> (<span class="id" type="var">snoc</span> <span class="id" type="var">l</span> <span class="id" type="var">x</span>) <span class="id" type="var">d</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">l</span> <span class="id" type="keyword">as</span> [|<span class="id" type="var">a</span> <span class="id" type="var">l'</span>]; <span class="id" type="tactic">intros</span>; <span class="id" type="tactic">try</span> <span class="id" type="var">solve</span> <span class="id" type="tactic">by</span> <span class="id" type="tactic">inversion</span>.<br/>
<span class="id" type="var">Case</span> "l = a :: l'".<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">n</span>; <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHl'</span>.<br/>
<span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">lt_S_n</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">nth_eq_snoc</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">A</span> (<span class="id" type="var">l</span>:<span class="id" type="var">list</span> <span class="id" type="var">A</span>) <span class="id" type="var">x</span> <span class="id" type="var">d</span>,<br/>
<span class="id" type="var">nth</span> (<span class="id" type="var">length</span> <span class="id" type="var">l</span>) (<span class="id" type="var">snoc</span> <span class="id" type="var">l</span> <span class="id" type="var">x</span>) <span class="id" type="var">d</span> = <span class="id" type="var">x</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">l</span>; <span class="id" type="tactic">intros</span>; [ <span class="id" type="tactic">auto</span> | <span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHl</span>; <span class="id" type="tactic">auto</span> ].<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
To update the store, we use the <span class="inlinecode"><span class="id" type="tactic">replace</span></span> function, which replaces
the contents of a cell at a particular index.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="tactic">replace</span> {<span class="id" type="var">A</span>:<span class="id" type="keyword">Type</span>} (<span class="id" type="var">n</span>:<span class="id" type="var">nat</span>) (<span class="id" type="var">x</span>:<span class="id" type="var">A</span>) (<span class="id" type="var">l</span>:<span class="id" type="var">list</span> <span class="id" type="var">A</span>) : <span class="id" type="var">list</span> <span class="id" type="var">A</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">nil</span> => <span class="id" type="var">nil</span><br/>
| <span class="id" type="var">h</span> :: <span class="id" type="var">t</span> => <br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">n</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">O</span> => <span class="id" type="var">x</span> :: <span class="id" type="var">t</span><br/>
| <span class="id" type="var">S</span> <span class="id" type="var">n'</span> => <span class="id" type="var">h</span> :: <span class="id" type="tactic">replace</span> <span class="id" type="var">n'</span> <span class="id" type="var">x</span> <span class="id" type="var">t</span><br/>
<span class="id" type="keyword">end</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
</div>