-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPE.html
2145 lines (1846 loc) · 325 KB
/
PE.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>PE: Partial Evaluation</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">PE<span class="subtitle">Partial Evaluation</span></h1>
<div class="code code-tight">
</div>
<div class="doc">
</div>
<div class="code code-tight">
<br/>
<span class="comment">(* $Date: 2012-03-30 20:39:34 -0400 (Fri, 30 Mar 2012) $ *)</span><br/>
<span class="comment">(* Chapter author/maintainer: Chung-chieh Shan *)</span><br/>
<br/>
</div>
<div class="doc">
Equiv.v introduced constant folding as an example of a program
transformation and proved that it preserves the meaning of the
program. Constant folding operates on manifest constants such
as <span class="inlinecode"><span class="id" type="var">ANum</span></span> expressions. For example, it simplifies the command
<span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">::=</span> <span class="inlinecode"><span class="id" type="var">APlus</span></span> <span class="inlinecode">(<span class="id" type="var">ANum</span></span> <span class="inlinecode">3)</span> <span class="inlinecode">(<span class="id" type="var">ANum</span></span> <span class="inlinecode">1)</span> to the command <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">::=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode">4</span>.
However, it does not propagate known constants along data flow.
For example, it does not simplify the sequence
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">X</span> ::= <span class="id" type="var">ANum</span> 3; <span class="id" type="var">Y</span> ::= <span class="id" type="var">APlus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">ANum</span> 1)
<div class="paragraph"> </div>
</div>
to
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">X</span> ::= <span class="id" type="var">ANum</span> 3; <span class="id" type="var">Y</span> ::= <span class="id" type="var">ANum</span> 4
<div class="paragraph"> </div>
</div>
because it forgets that <span class="inlinecode"><span class="id" type="var">X</span></span> is <span class="inlinecode">3</span> by the time it gets to <span class="inlinecode"><span class="id" type="var">Y</span></span>.
<div class="paragraph"> </div>
We naturally want to enhance constant folding so that it
propagates known constants and uses them to simplify programs.
Doing so constitutes a rudimentary form of <i>partial evaluation</i>.
As we will see, partial evaluation is so called because it is
like running a program, except only part of the program can be
evaluated because only part of the input to the program is known.
For example, we can only simplify the program
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">X</span> ::= <span class="id" type="var">ANum</span> 3; <span class="id" type="var">Y</span> ::= <span class="id" type="var">AMinus</span> (<span class="id" type="var">APlus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">ANum</span> 1)) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>)
<div class="paragraph"> </div>
</div>
to
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">X</span> ::= <span class="id" type="var">ANum</span> 3; <span class="id" type="var">Y</span> ::= <span class="id" type="var">AMinus</span> (<span class="id" type="var">ANum</span> 4) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>)
<div class="paragraph"> </div>
</div>
without knowing the initial value of <span class="inlinecode"><span class="id" type="var">Y</span></span>.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Imp</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">FunctionalExtensionality</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab912"></a><h1 class="section">Generalizing Constant Folding</h1>
<div class="paragraph"> </div>
The starting point of partial evaluation is to represent our
partial knowledge about the state. For example, between the two
assignments above, the partial evaluator may know only that <span class="inlinecode"><span class="id" type="var">X</span></span> is
<span class="inlinecode">3</span> and nothing about any other variable.
<div class="paragraph"> </div>
<a name="lab913"></a><h2 class="section">Partial States</h2>
<div class="paragraph"> </div>
Conceptually speaking, we can think of such partial states as the
type <span class="inlinecode"><span class="id" type="var">id</span></span> <span class="inlinecode"><span style="font-family: arial;">→</span></span> <span class="inlinecode"><span class="id" type="var">option</span></span> <span class="inlinecode"><span class="id" type="var">nat</span></span> (as opposed to the type <span class="inlinecode"><span class="id" type="var">id</span></span> <span class="inlinecode"><span style="font-family: arial;">→</span></span> <span class="inlinecode"><span class="id" type="var">nat</span></span> of
concrete, full states). However, in addition to looking up and
updating the values of individual variables in a partial state, we
may also want to compare two partial states to see if and where
they differ, to handle conditional control flow. It is not possible
to compare two arbitrary functions in this way, so we represent
partial states in a more concrete format: as a list of <span class="inlinecode"><span class="id" type="var">id</span></span> <span class="inlinecode">*</span> <span class="inlinecode"><span class="id" type="var">nat</span></span>
pairs.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">pe_state</span> := <span class="id" type="var">list</span> (<span class="id" type="var">id</span> * <span class="id" type="var">nat</span>).<br/>
<br/>
</div>
<div class="doc">
The idea is that a variable <span class="inlinecode"><span class="id" type="var">id</span></span> appears in the list if and only
if we know its current <span class="inlinecode"><span class="id" type="var">nat</span></span> value. The <span class="inlinecode"><span class="id" type="var">pe_lookup</span></span> function thus
interprets this concrete representation. (If the same variable
<span class="inlinecode"><span class="id" type="var">id</span></span> appears multiple times in the list, the first occurrence
wins, but we will define our partial evaluator to never construct
such a <span class="inlinecode"><span class="id" type="var">pe_state</span></span>.)
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">pe_lookup</span> (<span class="id" type="var">pe_st</span> : <span class="id" type="var">pe_state</span>) (<span class="id" type="var">V</span>:<span class="id" type="var">id</span>) : <span class="id" type="var">option</span> <span class="id" type="var">nat</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">pe_st</span> <span class="id" type="keyword">with</span><br/>
| [] => <span class="id" type="var">None</span><br/>
| (<span class="id" type="var">V'</span>,<span class="id" type="var">n'</span>)::<span class="id" type="var">pe_st</span> => <span class="id" type="keyword">if</span> <span class="id" type="var">beq_id</span> <span class="id" type="var">V</span> <span class="id" type="var">V'</span> <span class="id" type="keyword">then</span> <span class="id" type="var">Some</span> <span class="id" type="var">n'</span><br/>
<span class="id" type="keyword">else</span> <span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
For example, <span class="inlinecode"><span class="id" type="var">empty_pe_state</span></span> represents complete ignorance about
every variable — the function that maps every <span class="inlinecode"><span class="id" type="var">id</span></span> to <span class="inlinecode"><span class="id" type="var">None</span></span>.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">empty_pe_state</span> : <span class="id" type="var">pe_state</span> := [].<br/>
<br/>
</div>
<div class="doc">
More generally, if the <span class="inlinecode"><span class="id" type="var">list</span></span> representing a <span class="inlinecode"><span class="id" type="var">pe_state</span></span> does not
contain some <span class="inlinecode"><span class="id" type="var">id</span></span>, then that <span class="inlinecode"><span class="id" type="var">pe_state</span></span> must map that <span class="inlinecode"><span class="id" type="var">id</span></span> to
<span class="inlinecode"><span class="id" type="var">None</span></span>. Before we prove this fact, we first define a useful
tactic for reasoning with <span class="inlinecode"><span class="id" type="var">id</span></span> equality. The tactic
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">compare</span> <span class="id" type="var">V</span> <span class="id" type="var">V'</span> <span class="id" type="var">SCase</span>
<div class="paragraph"> </div>
</div>
means to reason by cases whether <span class="inlinecode"><span class="id" type="var">beq_id</span></span> <span class="inlinecode"><span class="id" type="var">V</span></span> <span class="inlinecode"><span class="id" type="var">V'</span></span> is <span class="inlinecode"><span class="id" type="var">true</span></span> or
<span class="inlinecode"><span class="id" type="var">false</span></span>. In the case where <span class="inlinecode"><span class="id" type="var">beq_id</span></span> <span class="inlinecode"><span class="id" type="var">V</span></span> <span class="inlinecode"><span class="id" type="var">V'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>, the tactic
substitutes <span class="inlinecode"><span class="id" type="var">V</span></span> for <span class="inlinecode"><span class="id" type="var">V'</span></span> throughout.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Tactic Notation</span> "compare" <span class="id" type="var">ident</span>(<span class="id" type="var">i</span>) <span class="id" type="var">ident</span>(<span class="id" type="var">j</span>) <span class="id" type="var">ident</span>(<span class="id" type="var">c</span>) :=<br/>
<span class="id" type="keyword">let</span> <span class="id" type="var">H</span> := <span class="id" type="tactic">fresh</span> "Heq" <span class="id" type="var">i</span> <span class="id" type="var">j</span> <span class="id" type="keyword">in</span><br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">i</span> <span class="id" type="var">j</span>) <span class="id" type="keyword">as</span> [|]<span class="id" type="var">_eqn</span>:<span class="id" type="var">H</span>;<br/>
[ <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "equal"; <span class="id" type="tactic">symmetry</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">beq_id_eq</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span> <span class="id" type="var">j</span><br/>
| <span class="id" type="var">Case_aux</span> <span class="id" type="var">c</span> "not equal" ].<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_domain</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">n</span>,<br/>
<span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> = <span class="id" type="var">Some</span> <span class="id" type="var">n</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">true</span> = <span class="id" type="var">existsb</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span>) (<span class="id" type="var">map</span> (@<span class="id" type="var">fst</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span>) <span class="id" type="var">pe_st</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">n</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">pe_st</span> <span class="id" type="keyword">as</span> [| [<span class="id" type="var">V'</span> <span class="id" type="var">n'</span>] <span class="id" type="var">pe_st</span>].<br/>
<span class="id" type="var">Case</span> "[]". <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="var">Case</span> "::". <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">simpl</span>. <span class="id" type="var">compare</span> <span class="id" type="var">V</span> <span class="id" type="var">V'</span> <span class="id" type="var">SCase</span>; <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab914"></a><h2 class="section">Arithmetic Expressions</h2>
<div class="paragraph"> </div>
Partial evaluation of <span class="inlinecode"><span class="id" type="var">aexp</span></span> is straightforward — it is basically
the same as constant folding, <span class="inlinecode"><span class="id" type="var">fold_constants_aexp</span></span>, except that
sometimes the partial state tells us the current value of a
variable and we can replace it by a constant expression.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">pe_aexp</span> (<span class="id" type="var">pe_st</span> : <span class="id" type="var">pe_state</span>) (<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>) : <span class="id" type="var">aexp</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">a</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">ANum</span> <span class="id" type="var">n</span> => <span class="id" type="var">ANum</span> <span class="id" type="var">n</span><br/>
| <span class="id" type="var">AId</span> <span class="id" type="var">i</span> => <span class="id" type="keyword">match</span> <span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">i</span> <span class="id" type="keyword">with</span> <span class="comment">(* <----- NEW *)</span><br/>
| <span class="id" type="var">Some</span> <span class="id" type="var">n</span> => <span class="id" type="var">ANum</span> <span class="id" type="var">n</span><br/>
| <span class="id" type="var">None</span> => <span class="id" type="var">AId</span> <span class="id" type="var">i</span><br/>
<span class="id" type="keyword">end</span><br/>
| <span class="id" type="var">APlus</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> =><br/>
<span class="id" type="keyword">match</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a1</span>, <span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a2</span>) <span class="id" type="keyword">with</span><br/>
| (<span class="id" type="var">ANum</span> <span class="id" type="var">n1</span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n2</span>) => <span class="id" type="var">ANum</span> (<span class="id" type="var">n1</span> + <span class="id" type="var">n2</span>)<br/>
| (<span class="id" type="var">a1'</span>, <span class="id" type="var">a2'</span>) => <span class="id" type="var">APlus</span> <span class="id" type="var">a1'</span> <span class="id" type="var">a2'</span><br/>
<span class="id" type="keyword">end</span><br/>
| <span class="id" type="var">AMinus</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> => <br/>
<span class="id" type="keyword">match</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a1</span>, <span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a2</span>) <span class="id" type="keyword">with</span><br/>
| (<span class="id" type="var">ANum</span> <span class="id" type="var">n1</span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n2</span>) => <span class="id" type="var">ANum</span> (<span class="id" type="var">n1</span> - <span class="id" type="var">n2</span>)<br/>
| (<span class="id" type="var">a1'</span>, <span class="id" type="var">a2'</span>) => <span class="id" type="var">AMinus</span> <span class="id" type="var">a1'</span> <span class="id" type="var">a2'</span><br/>
<span class="id" type="keyword">end</span><br/>
| <span class="id" type="var">AMult</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> =><br/>
<span class="id" type="keyword">match</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a1</span>, <span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a2</span>) <span class="id" type="keyword">with</span><br/>
| (<span class="id" type="var">ANum</span> <span class="id" type="var">n1</span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n2</span>) => <span class="id" type="var">ANum</span> (<span class="id" type="var">n1</span> * <span class="id" type="var">n2</span>)<br/>
| (<span class="id" type="var">a1'</span>, <span class="id" type="var">a2'</span>) => <span class="id" type="var">AMult</span> <span class="id" type="var">a1'</span> <span class="id" type="var">a2'</span><br/>
<span class="id" type="keyword">end</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
This partial evaluator folds constants but does not apply the
associativity of addition.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_pe_aexp1</span>:<br/>
<span class="id" type="var">pe_aexp</span> [(<span class="id" type="var">X</span>,3)] (<span class="id" type="var">APlus</span> (<span class="id" type="var">APlus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">ANum</span> 1)) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>))<br/>
= <span class="id" type="var">APlus</span> (<span class="id" type="var">ANum</span> 4) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">text_pe_aexp2</span>:<br/>
<span class="id" type="var">pe_aexp</span> [(<span class="id" type="var">Y</span>,3)] (<span class="id" type="var">APlus</span> (<span class="id" type="var">APlus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">ANum</span> 1)) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>))<br/>
= <span class="id" type="var">APlus</span> (<span class="id" type="var">APlus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">ANum</span> 1)) (<span class="id" type="var">ANum</span> 3).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
Now, in what sense is <span class="inlinecode"><span class="id" type="var">pe_aexp</span></span> correct? It is reasonable to
define the correctness of <span class="inlinecode"><span class="id" type="var">pe_aexp</span></span> as follows: whenever a full
state <span class="inlinecode"><span class="id" type="var">st</span>:<span class="id" type="var">state</span></span> is <i>consistent</i> with a partial state
<span class="inlinecode"><span class="id" type="var">pe_st</span>:<span class="id" type="var">pe_state</span></span> (in other words, every variable to which <span class="inlinecode"><span class="id" type="var">pe_st</span></span>
assigns a value is assigned the same value by <span class="inlinecode"><span class="id" type="var">st</span></span>), evaluating
<span class="inlinecode"><span class="id" type="var">a</span></span> and evaluating <span class="inlinecode"><span class="id" type="var">pe_aexp</span></span> <span class="inlinecode"><span class="id" type="var">pe_st</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> in <span class="inlinecode"><span class="id" type="var">st</span></span> yields the same
result. This statement is indeed true.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">pe_consistent</span> (<span class="id" type="var">st</span>:<span class="id" type="var">state</span>) (<span class="id" type="var">pe_st</span>:<span class="id" type="var">pe_state</span>) :=<br/>
<span style="font-family: arial;">∀</span><span class="id" type="var">V</span> <span class="id" type="var">n</span>, <span class="id" type="var">Some</span> <span class="id" type="var">n</span> = <span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span style="font-family: arial;">→</span> <span class="id" type="var">st</span> <span class="id" type="var">V</span> = <span class="id" type="var">n</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_aexp_correct_weak</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">st</span> <span class="id" type="var">pe_st</span>, <span class="id" type="var">pe_consistent</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span> <span style="font-family: arial;">→</span><br/>
<span style="font-family: arial;">∀</span><span class="id" type="var">a</span>, <span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a</span> = <span class="id" type="var">aeval</span> <span class="id" type="var">st</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">pe_consistent</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">H</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="var">aexp_cases</span> (<span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>) <span class="id" type="var">Case</span>; <span class="id" type="tactic">simpl</span>;<br/>
<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>;<br/>
<span class="id" type="tactic">try</span> (<span class="id" type="tactic">destruct</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a1</span>);<br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a2</span>);<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
<span class="comment">(* Compared to fold_constants_aexp_sound,<br/>
the only interesting case is AId *)</span><br/>
<span class="id" type="var">Case</span> "AId".<br/>
<span class="id" type="var">remember</span> (<span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">i</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">l</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">l</span>.<br/>
<span class="id" type="var">SCase</span> "Some". <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">n</span>:=<span class="id" type="var">n</span>) <span class="id" type="tactic">by</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">Heql</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">SCase</span> "None". <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
However, we will soon want our partial evaluator to remove
assignments. For example, it will simplify
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">X</span> ::= <span class="id" type="var">ANum</span> 3; <span class="id" type="var">Y</span> ::= <span class="id" type="var">AMinus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>); <span class="id" type="var">X</span> ::= <span class="id" type="var">ANum</span> 4
<div class="paragraph"> </div>
</div>
to just
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">Y</span> ::= <span class="id" type="var">AMinus</span> (<span class="id" type="var">ANum</span> 3) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>); <span class="id" type="var">X</span> ::= <span class="id" type="var">ANum</span> 4
<div class="paragraph"> </div>
</div>
by delaying the assignment to <span class="inlinecode"><span class="id" type="var">X</span></span> until the end. To accomplish
this simplification, we need the result of partial evaluating
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">pe_aexp</span> [(<span class="id" type="var">X</span>,3)] (<span class="id" type="var">AMinus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>))
<div class="paragraph"> </div>
</div>
to be equal to <span class="inlinecode"><span class="id" type="var">AMinus</span></span> <span class="inlinecode">(<span class="id" type="var">ANum</span></span> <span class="inlinecode">3)</span> <span class="inlinecode">(<span class="id" type="var">AId</span></span> <span class="inlinecode"><span class="id" type="var">Y</span>)</span> and <i>not</i> the original
expression <span class="inlinecode"><span class="id" type="var">AMinus</span></span> <span class="inlinecode">(<span class="id" type="var">AId</span></span> <span class="inlinecode"><span class="id" type="var">X</span>)</span> <span class="inlinecode">(<span class="id" type="var">AId</span></span> <span class="inlinecode"><span class="id" type="var">Y</span>)</span>. After all, it would be
incorrect, not just inefficient, to transform
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">X</span> ::= <span class="id" type="var">ANum</span> 3; <span class="id" type="var">Y</span> ::= <span class="id" type="var">AMinus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>); <span class="id" type="var">X</span> ::= <span class="id" type="var">ANum</span> 4
<div class="paragraph"> </div>
</div>
to
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">Y</span> ::= <span class="id" type="var">AMinus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>); <span class="id" type="var">X</span> ::= <span class="id" type="var">ANum</span> 4
<div class="paragraph"> </div>
</div>
even though the output expressions <span class="inlinecode"><span class="id" type="var">AMinus</span></span> <span class="inlinecode">(<span class="id" type="var">ANum</span></span> <span class="inlinecode">3)</span> <span class="inlinecode">(<span class="id" type="var">AId</span></span> <span class="inlinecode"><span class="id" type="var">Y</span>)</span> and
<span class="inlinecode"><span class="id" type="var">AMinus</span></span> <span class="inlinecode">(<span class="id" type="var">AId</span></span> <span class="inlinecode"><span class="id" type="var">X</span>)</span> <span class="inlinecode">(<span class="id" type="var">AId</span></span> <span class="inlinecode"><span class="id" type="var">Y</span>)</span> both satisfy the correctness criterion
that we just proved. Indeed, if we were to just define <span class="inlinecode"><span class="id" type="var">pe_aexp</span></span>
<span class="inlinecode"><span class="id" type="var">pe_st</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">a</span></span> then the theorem <span class="inlinecode"><span class="id" type="var">pe_aexp_correct'</span></span> would already
trivially hold.
<div class="paragraph"> </div>
Instead, we want to prove that the <span class="inlinecode"><span class="id" type="var">pe_aexp</span></span> is correct in a
stronger sense: evaluating the expression produced by partial
evaluation (<span class="inlinecode"><span class="id" type="var">aeval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">(<span class="id" type="var">pe_aexp</span></span> <span class="inlinecode"><span class="id" type="var">pe_st</span></span> <span class="inlinecode"><span class="id" type="var">a</span>)</span>) must not depend on those
parts of the full state <span class="inlinecode"><span class="id" type="var">st</span></span> that are already specified in the
partial state <span class="inlinecode"><span class="id" type="var">pe_st</span></span>. To be more precise, let us define a
function <span class="inlinecode"><span class="id" type="var">pe_override</span></span>, which updates <span class="inlinecode"><span class="id" type="var">st</span></span> with the contents of
<span class="inlinecode"><span class="id" type="var">pe_st</span></span>. In other words, <span class="inlinecode"><span class="id" type="var">pe_override</span></span> carries out the
assignments listed in <span class="inlinecode"><span class="id" type="var">pe_st</span></span> on top of <span class="inlinecode"><span class="id" type="var">st</span></span>.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">pe_override</span> (<span class="id" type="var">st</span>:<span class="id" type="var">state</span>) (<span class="id" type="var">pe_st</span>:<span class="id" type="var">pe_state</span>) : <span class="id" type="var">state</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">pe_st</span> <span class="id" type="keyword">with</span><br/>
| [] => <span class="id" type="var">st</span><br/>
| (<span class="id" type="var">V</span>,<span class="id" type="var">n</span>)::<span class="id" type="var">pe_st</span> => <span class="id" type="var">update</span> (<span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span>) <span class="id" type="var">V</span> <span class="id" type="var">n</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_pe_override</span>:<br/>
<span class="id" type="var">pe_override</span> (<span class="id" type="var">update</span> <span class="id" type="var">empty_state</span> <span class="id" type="var">Y</span> 1) [(<span class="id" type="var">X</span>,3),(<span class="id" type="var">Z</span>,2)]<br/>
= <span class="id" type="var">update</span> (<span class="id" type="var">update</span> (<span class="id" type="var">update</span> <span class="id" type="var">empty_state</span> <span class="id" type="var">Y</span> 1) <span class="id" type="var">Z</span> 2) <span class="id" type="var">X</span> 3.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
Although <span class="inlinecode"><span class="id" type="var">pe_override</span></span> operates on a concrete <span class="inlinecode"><span class="id" type="var">list</span></span> representing
a <span class="inlinecode"><span class="id" type="var">pe_state</span></span>, its behavior is defined entirely by the <span class="inlinecode"><span class="id" type="var">pe_lookup</span></span>
interpretation of the <span class="inlinecode"><span class="id" type="var">pe_state</span></span>.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_override_correct</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">st</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V0</span>,<br/>
<span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V0</span> =<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V0</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">Some</span> <span class="id" type="var">n</span> => <span class="id" type="var">n</span><br/>
| <span class="id" type="var">None</span> => <span class="id" type="var">st</span> <span class="id" type="var">V0</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">pe_st</span> <span class="id" type="keyword">as</span> [| [<span class="id" type="var">V</span> <span class="id" type="var">n</span>] <span class="id" type="var">pe_st</span>]. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> *. <span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">beq_id_sym</span>.<br/>
<span class="id" type="var">compare</span> <span class="id" type="var">V0</span> <span class="id" type="var">V</span> <span class="id" type="var">Case</span>; <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
We can relate <span class="inlinecode"><span class="id" type="var">pe_consistent</span></span> to <span class="inlinecode"><span class="id" type="var">pe_override</span></span> in two ways.
First, overriding a state with a partial state always gives a
state that is consistent with the partial state. Second, if a
state is already consistent with a partial state, then overriding
the state with the partial state gives the same state.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_override_consistent</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">st</span> <span class="id" type="var">pe_st</span>,<br/>
<span class="id" type="var">pe_consistent</span> (<span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span>) <span class="id" type="var">pe_st</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">n</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">pe_override_correct</span>.<br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span>); <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_consistent_override</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">st</span> <span class="id" type="var">pe_st</span>,<br/>
<span class="id" type="var">pe_consistent</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span> <span style="font-family: arial;">→</span> <span style="font-family: arial;">∀</span><span class="id" type="var">V</span>, <span class="id" type="var">st</span> <span class="id" type="var">V</span> = <span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">H</span> <span class="id" type="var">V</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">pe_override_correct</span>.<br/>
<span class="id" type="var">remember</span> (<span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">l</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">l</span>; <span class="id" type="tactic">auto</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
Now we can state and prove that <span class="inlinecode"><span class="id" type="var">pe_aexp</span></span> is correct in the
stronger sense that will help us define the rest of the partial
evaluator.
<div class="paragraph"> </div>
Intuitively, running a program using partial evaluation is a
two-stage process. In the first, <i>static</i> stage, we partially
evaluate the given program with respect to some partial state to
get a <i>residual</i> program. In the second, <i>dynamic</i> stage, we
evaluate the residual program with respect to the rest of the
state. This dynamic state provides values for those variables
that are unknown in the static (partial) state. Thus, the
residual program should be equivalent to <i>prepending</i> the
assignments listed in the partial state to the original program.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_aexp_correct</span>: <span style="font-family: arial;">∀</span>(<span class="id" type="var">pe_st</span>:<span class="id" type="var">pe_state</span>) (<span class="id" type="var">a</span>:<span class="id" type="var">aexp</span>) (<span class="id" type="var">st</span>:<span class="id" type="var">state</span>),<br/>
<span class="id" type="var">aeval</span> (<span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span>) <span class="id" type="var">a</span> = <span class="id" type="var">aeval</span> <span class="id" type="var">st</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a</span> <span class="id" type="var">st</span>.<br/>
<span class="id" type="var">aexp_cases</span> (<span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>) <span class="id" type="var">Case</span>; <span class="id" type="tactic">simpl</span>;<br/>
<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>;<br/>
<span class="id" type="tactic">try</span> (<span class="id" type="tactic">destruct</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a1</span>);<br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a2</span>);<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
<span class="comment">(* Compared to fold_constants_aexp_sound, the only <br/>
interesting case is AId. *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">pe_override_correct</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">i</span>); <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab915"></a><h2 class="section">Boolean Expressions</h2>
<div class="paragraph"> </div>
The partial evaluation of boolean expressions is similar. In
fact, it is entirely analogous to the constant folding of boolean
expressions, because our language has no boolean variables.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">pe_bexp</span> (<span class="id" type="var">pe_st</span> : <span class="id" type="var">pe_state</span>) (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>) : <span class="id" type="var">bexp</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">b</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">BTrue</span> => <span class="id" type="var">BTrue</span><br/>
| <span class="id" type="var">BFalse</span> => <span class="id" type="var">BFalse</span><br/>
| <span class="id" type="var">BEq</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> => <br/>
<span class="id" type="keyword">match</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a1</span>, <span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a2</span>) <span class="id" type="keyword">with</span><br/>
| (<span class="id" type="var">ANum</span> <span class="id" type="var">n1</span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n2</span>) => <span class="id" type="keyword">if</span> <span class="id" type="var">beq_nat</span> <span class="id" type="var">n1</span> <span class="id" type="var">n2</span> <span class="id" type="keyword">then</span> <span class="id" type="var">BTrue</span> <span class="id" type="keyword">else</span> <span class="id" type="var">BFalse</span><br/>
| (<span class="id" type="var">a1'</span>, <span class="id" type="var">a2'</span>) => <span class="id" type="var">BEq</span> <span class="id" type="var">a1'</span> <span class="id" type="var">a2'</span><br/>
<span class="id" type="keyword">end</span><br/>
| <span class="id" type="var">BLe</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> =><br/>
<span class="id" type="keyword">match</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a1</span>, <span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a2</span>) <span class="id" type="keyword">with</span><br/>
| (<span class="id" type="var">ANum</span> <span class="id" type="var">n1</span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n2</span>) => <span class="id" type="keyword">if</span> <span class="id" type="var">ble_nat</span> <span class="id" type="var">n1</span> <span class="id" type="var">n2</span> <span class="id" type="keyword">then</span> <span class="id" type="var">BTrue</span> <span class="id" type="keyword">else</span> <span class="id" type="var">BFalse</span><br/>
| (<span class="id" type="var">a1'</span>, <span class="id" type="var">a2'</span>) => <span class="id" type="var">BLe</span> <span class="id" type="var">a1'</span> <span class="id" type="var">a2'</span><br/>
<span class="id" type="keyword">end</span><br/>
| <span class="id" type="var">BNot</span> <span class="id" type="var">b1</span> => <br/>
<span class="id" type="keyword">match</span> (<span class="id" type="var">pe_bexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">b1</span>) <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">BTrue</span> => <span class="id" type="var">BFalse</span><br/>
| <span class="id" type="var">BFalse</span> => <span class="id" type="var">BTrue</span><br/>
| <span class="id" type="var">b1'</span> => <span class="id" type="var">BNot</span> <span class="id" type="var">b1'</span><br/>
<span class="id" type="keyword">end</span><br/>
| <span class="id" type="var">BAnd</span> <span class="id" type="var">b1</span> <span class="id" type="var">b2</span> =><br/>
<span class="id" type="keyword">match</span> (<span class="id" type="var">pe_bexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">b1</span>, <span class="id" type="var">pe_bexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">b2</span>) <span class="id" type="keyword">with</span><br/>
| (<span class="id" type="var">BTrue</span>, <span class="id" type="var">BTrue</span>) => <span class="id" type="var">BTrue</span><br/>
| (<span class="id" type="var">BTrue</span>, <span class="id" type="var">BFalse</span>) => <span class="id" type="var">BFalse</span><br/>
| (<span class="id" type="var">BFalse</span>, <span class="id" type="var">BTrue</span>) => <span class="id" type="var">BFalse</span><br/>
| (<span class="id" type="var">BFalse</span>, <span class="id" type="var">BFalse</span>) => <span class="id" type="var">BFalse</span><br/>
| (<span class="id" type="var">b1'</span>, <span class="id" type="var">b2'</span>) => <span class="id" type="var">BAnd</span> <span class="id" type="var">b1'</span> <span class="id" type="var">b2'</span><br/>
<span class="id" type="keyword">end</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_pe_bexp1</span>:<br/>
<span class="id" type="var">pe_bexp</span> [(<span class="id" type="var">X</span>,3)] (<span class="id" type="var">BNot</span> (<span class="id" type="var">BLe</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">ANum</span> 3)))<br/>
= <span class="id" type="var">BFalse</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_pe_bexp2</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">b</span>,<br/>
<span class="id" type="var">b</span> = <span class="id" type="var">BNot</span> (<span class="id" type="var">BLe</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">APlus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">ANum</span> 1))) <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">pe_bexp</span> [] <span class="id" type="var">b</span> = <span class="id" type="var">b</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">rewrite</span> <span style="font-family: arial;">→</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
The correctness of <span class="inlinecode"><span class="id" type="var">pe_bexp</span></span> is analogous to the correctness of
<span class="inlinecode"><span class="id" type="var">pe_aexp</span></span> above.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_bexp_correct</span>: <span style="font-family: arial;">∀</span>(<span class="id" type="var">pe_st</span>:<span class="id" type="var">pe_state</span>) (<span class="id" type="var">b</span>:<span class="id" type="var">bexp</span>) (<span class="id" type="var">st</span>:<span class="id" type="var">state</span>),<br/>
<span class="id" type="var">beval</span> (<span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span>) <span class="id" type="var">b</span> = <span class="id" type="var">beval</span> <span class="id" type="var">st</span> (<span class="id" type="var">pe_bexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">b</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">b</span> <span class="id" type="var">st</span>.<br/>
<span class="id" type="var">bexp_cases</span> (<span class="id" type="tactic">induction</span> <span class="id" type="var">b</span>) <span class="id" type="var">Case</span>; <span class="id" type="tactic">simpl</span>;<br/>
<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>;<br/>
<span class="id" type="tactic">try</span> (<span class="id" type="var">remember</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">a'</span>;<br/>
<span class="id" type="var">remember</span> (<span class="id" type="var">pe_aexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">a0</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">a0'</span>;<br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">Ha</span>: <span class="id" type="var">aeval</span> (<span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span>) <span class="id" type="var">a</span> = <span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a'</span>);<br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">Ha0</span>: <span class="id" type="var">aeval</span> (<span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span>) <span class="id" type="var">a0</span> = <span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a0'</span>);<br/>
<span class="id" type="tactic">try</span> (<span class="id" type="tactic">subst</span>; <span class="id" type="tactic">apply</span> <span class="id" type="var">pe_aexp_correct</span>);<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">a'</span>; <span class="id" type="tactic">destruct</span> <span class="id" type="var">a0'</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">Ha</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">Ha0</span>;<br/>
<span class="id" type="tactic">simpl</span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">destruct</span> (<span class="id" type="var">beq_nat</span> <span class="id" type="var">n</span> <span class="id" type="var">n0</span>); <span class="id" type="tactic">try</span> <span class="id" type="tactic">destruct</span> (<span class="id" type="var">ble_nat</span> <span class="id" type="var">n</span> <span class="id" type="var">n0</span>);<br/>
<span class="id" type="tactic">reflexivity</span>);<br/>
<span class="id" type="tactic">try</span> (<span class="id" type="tactic">destruct</span> (<span class="id" type="var">pe_bexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">b</span>); <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHb</span>; <span class="id" type="tactic">reflexivity</span>);<br/>
<span class="id" type="tactic">try</span> (<span class="id" type="tactic">destruct</span> (<span class="id" type="var">pe_bexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">b1</span>);<br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">pe_bexp</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">b2</span>);<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHb1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHb2</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab916"></a><h1 class="section">Partial Evaluation of Commands, Without Loops</h1>
<div class="paragraph"> </div>
What about the partial evaluation of commands? The analogy
between partial evaluation and full evaluation continues: Just as
full evaluation of a command turns an initial state into a final
state, partial evaluation of a command turns an initial partial
state into a final partial state. The difference is that, because
the state is partial, some parts of the command may not be
executable at the static stage. Therefore, just as <span class="inlinecode"><span class="id" type="var">pe_aexp</span></span>
returns a residual <span class="inlinecode"><span class="id" type="var">aexp</span></span> and <span class="inlinecode"><span class="id" type="var">pe_bexp</span></span> returns a residual <span class="inlinecode"><span class="id" type="var">bexp</span></span>
above, partially evaluating a command yields a residual command.
<div class="paragraph"> </div>
Another way in which our partial evaluator is similar to a full
evaluator is that it does not terminate on all commands. It is
not hard to build a partial evaluator that terminates on all
commands; what is hard is building a partial evaluator that
terminates on all commands yet automatically performs desired
optimizations such as unrolling loops. Often a partial evaluator
can be coaxed into terminating more often and performing more
optimizations by writing the source program differently so that
the separation between static and dynamic information becomes more
apparent. Such coaxing is the art of <i>binding-time improvement</i>.
The binding time of a variable tells when its value is known —
either "static", or "dynamic."
<div class="paragraph"> </div>
Anyway, for now we will just live with the fact that our partial
evaluator is not a total function from the source command and the
initial partial state to the residual command and the final
partial state. To model this non-termination, just as with the
full evaluation of commands, we use an inductively defined
relation. We write
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">c1</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">c1'</span> / <span class="id" type="var">st'</span>
<div class="paragraph"> </div>
</div>
to mean that partially evaluating the source command <span class="inlinecode"><span class="id" type="var">c1</span></span> in the
initial partial state <span class="inlinecode"><span class="id" type="var">st</span></span> yields the residual command <span class="inlinecode"><span class="id" type="var">c1'</span></span> and
the final partial state <span class="inlinecode"><span class="id" type="var">st'</span></span>. For example, we want something like
<div class="paragraph"> </div>
<div class="code code-tight">
(<span class="id" type="var">X</span> ::= <span class="id" type="var">ANum</span> 3 ; <span class="id" type="var">Y</span> ::= <span class="id" type="var">AMult</span> (<span class="id" type="var">AId</span> <span class="id" type="var">Z</span>) (<span class="id" type="var">APlus</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>)))<br/>
/ [] <span style="font-family: arial;">⇓</span> (<span class="id" type="var">Y</span> ::= <span class="id" type="var">AMult</span> (<span class="id" type="var">AId</span> <span class="id" type="var">Z</span>) (<span class="id" type="var">ANum</span> 6)) / [(<span class="id" type="var">X</span>,3)]
<div class="paragraph"> </div>
</div>
to hold. The assignment to <span class="inlinecode"><span class="id" type="var">X</span></span> appears in the final partial state,
not the residual command.
<div class="paragraph"> </div>
<a name="lab917"></a><h2 class="section">Assignment</h2>
<div class="paragraph"> </div>
Let's start by considering how to partially evaluate an
assignment. The two assignments in the source program above needs
to be treated differently. The first assignment <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">::=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode">3</span>,
is <i>static</i>: its right-hand-side is a constant (more generally,
simplifies to a constant), so we should update our partial state
at <span class="inlinecode"><span class="id" type="var">X</span></span> to <span class="inlinecode">3</span> and produce no residual code. (Actually, we produce
a residual <span class="inlinecode"><span class="id" type="var">SKIP</span></span>.) The second assignment <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">::=</span> <span class="inlinecode"><span class="id" type="var">AMult</span></span> <span class="inlinecode">(<span class="id" type="var">AId</span></span> <span class="inlinecode"><span class="id" type="var">Z</span>)</span>
<span class="inlinecode">(<span class="id" type="var">APlus</span></span> <span class="inlinecode">(<span class="id" type="var">AId</span></span> <span class="inlinecode"><span class="id" type="var">X</span>)</span> <span class="inlinecode">(<span class="id" type="var">AId</span></span> <span class="inlinecode"><span class="id" type="var">X</span>))</span> is <i>dynamic</i>: its right-hand-side does
not simplify to a constant, so we should leave it in the residual
code and remove <span class="inlinecode"><span class="id" type="var">Y</span></span>, if present, from our partial state. To
implement these two cases, we define the functions <span class="inlinecode"><span class="id" type="var">pe_add</span></span> and
<span class="inlinecode"><span class="id" type="var">pe_remove</span></span>. Like <span class="inlinecode"><span class="id" type="var">pe_override</span></span> above, these functions operate on
a concrete <span class="inlinecode"><span class="id" type="var">list</span></span> representing a <span class="inlinecode"><span class="id" type="var">pe_state</span></span>, but the theorems
<span class="inlinecode"><span class="id" type="var">pe_add_correct</span></span> and <span class="inlinecode"><span class="id" type="var">pe_remove_correct</span></span> specify their behavior by
the <span class="inlinecode"><span class="id" type="var">pe_lookup</span></span> interpretation of the <span class="inlinecode"><span class="id" type="var">pe_state</span></span>.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">pe_remove</span> (<span class="id" type="var">pe_st</span>:<span class="id" type="var">pe_state</span>) (<span class="id" type="var">V</span>:<span class="id" type="var">id</span>) : <span class="id" type="var">pe_state</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">pe_st</span> <span class="id" type="keyword">with</span><br/>
| [] => []<br/>
| (<span class="id" type="var">V'</span>,<span class="id" type="var">n'</span>)::<span class="id" type="var">pe_st</span> => <span class="id" type="keyword">if</span> <span class="id" type="var">beq_id</span> <span class="id" type="var">V</span> <span class="id" type="var">V'</span> <span class="id" type="keyword">then</span> <span class="id" type="var">pe_remove</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span><br/>
<span class="id" type="keyword">else</span> (<span class="id" type="var">V'</span>,<span class="id" type="var">n'</span>) :: <span class="id" type="var">pe_remove</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_remove_correct</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">V0</span>,<br/>
<span class="id" type="var">pe_lookup</span> (<span class="id" type="var">pe_remove</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span>) <span class="id" type="var">V0</span><br/>
= <span class="id" type="keyword">if</span> <span class="id" type="var">beq_id</span> <span class="id" type="var">V</span> <span class="id" type="var">V0</span> <span class="id" type="keyword">then</span> <span class="id" type="var">None</span> <span class="id" type="keyword">else</span> <span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V0</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">V0</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">pe_st</span> <span class="id" type="keyword">as</span> [| [<span class="id" type="var">V'</span> <span class="id" type="var">n'</span>] <span class="id" type="var">pe_st</span>].<br/>
<span class="id" type="var">Case</span> "[]". <span class="id" type="tactic">destruct</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span> <span class="id" type="var">V0</span>); <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">Case</span> "::". <span class="id" type="tactic">simpl</span>. <span class="id" type="var">compare</span> <span class="id" type="var">V</span> <span class="id" type="var">V'</span> <span class="id" type="var">SCase</span>.<br/>
<span class="id" type="var">SCase</span> "equal". <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHpe_st</span>.<br/>
<span class="id" type="tactic">replace</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V0</span> <span class="id" type="var">V</span>) <span class="id" type="keyword">with</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span> <span class="id" type="var">V0</span>) <span class="id" type="tactic">by</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">beq_id_sym</span>.<br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span> <span class="id" type="var">V0</span>); <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">SCase</span> "not equal". <span class="id" type="tactic">simpl</span>. <span class="id" type="var">compare</span> <span class="id" type="var">V0</span> <span class="id" type="var">V'</span> <span class="id" type="var">SSCase</span>.<br/>
<span class="id" type="var">SSCase</span> "equal". <span class="id" type="tactic">rewrite</span> <span class="id" type="var">HeqVV'</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">SSCase</span> "not equal". <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHpe_st</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">pe_add</span> (<span class="id" type="var">pe_st</span>:<span class="id" type="var">pe_state</span>) (<span class="id" type="var">V</span>:<span class="id" type="var">id</span>) (<span class="id" type="var">n</span>:<span class="id" type="var">nat</span>) : <span class="id" type="var">pe_state</span> :=<br/>
(<span class="id" type="var">V</span>,<span class="id" type="var">n</span>) :: <span class="id" type="var">pe_remove</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_add_correct</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">n</span> <span class="id" type="var">V0</span>,<br/>
<span class="id" type="var">pe_lookup</span> (<span class="id" type="var">pe_add</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">n</span>) <span class="id" type="var">V0</span><br/>
= <span class="id" type="keyword">if</span> <span class="id" type="var">beq_id</span> <span class="id" type="var">V</span> <span class="id" type="var">V0</span> <span class="id" type="keyword">then</span> <span class="id" type="var">Some</span> <span class="id" type="var">n</span> <span class="id" type="keyword">else</span> <span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V0</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">n</span> <span class="id" type="var">V0</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">pe_add</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">beq_id_sym</span>.<br/>
<span class="id" type="var">compare</span> <span class="id" type="var">V</span> <span class="id" type="var">V0</span> <span class="id" type="var">Case</span>.<br/>
<span class="id" type="var">Case</span> "equal". <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">Case</span> "not equal". <span class="id" type="tactic">rewrite</span> <span class="id" type="var">pe_remove_correct</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">HeqVV0</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
We will use the two theorems below to show that our partial
evaluator correctly deals with dynamic assignments and static
assignments, respectively.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_override_update_remove</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">st</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">n</span>,<br/>
<span class="id" type="var">update</span> (<span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span>) <span class="id" type="var">V</span> <span class="id" type="var">n</span> =<br/>
<span class="id" type="var">pe_override</span> (<span class="id" type="var">update</span> <span class="id" type="var">st</span> <span class="id" type="var">V</span> <span class="id" type="var">n</span>) (<span class="id" type="var">pe_remove</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">n</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">functional_extensionality</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">V0</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>. <span class="id" type="tactic">rewrite</span> !<span class="id" type="var">pe_override_correct</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">pe_remove_correct</span>.<br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span> <span class="id" type="var">V0</span>); <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_override_update_add</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">st</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">n</span>,<br/>
<span class="id" type="var">update</span> (<span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span>) <span class="id" type="var">V</span> <span class="id" type="var">n</span> =<br/>
<span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> (<span class="id" type="var">pe_add</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">n</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="var">n</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">functional_extensionality</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">V0</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">update</span>. <span class="id" type="tactic">rewrite</span> !<span class="id" type="var">pe_override_correct</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">pe_add_correct</span>.<br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span> <span class="id" type="var">V0</span>); <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab918"></a><h2 class="section">Conditional</h2>
<div class="paragraph"> </div>
Trickier than assignments to partially evaluate is the
conditional, <span class="inlinecode"><span class="id" type="var">IFB</span></span> <span class="inlinecode"><span class="id" type="var">b1</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c1</span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c2</span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span>. If <span class="inlinecode"><span class="id" type="var">b1</span></span> simplifies to
<span class="inlinecode"><span class="id" type="var">BTrue</span></span> or <span class="inlinecode"><span class="id" type="var">BFalse</span></span> then it's easy: we know which branch will be
taken, so just take that branch. If <span class="inlinecode"><span class="id" type="var">b1</span></span> does not simplify to a
constant, then we need to take both branches, and the final
partial state may differ between the two branches!
<div class="paragraph"> </div>
The following program illustrates the difficulty:
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">X</span> ::= <span class="id" type="var">ANum</span> 3;<br/>
<span class="id" type="var">IFB</span> <span class="id" type="var">BLe</span> (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>) (<span class="id" type="var">ANum</span> 4) <span class="id" type="var">THEN</span><br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">ANum</span> 4;<br/>
<span class="id" type="var">IFB</span> <span class="id" type="var">BEq</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>) <span class="id" type="var">THEN</span> <span class="id" type="var">Y</span> ::= <span class="id" type="var">ANum</span> 999 <span class="id" type="var">ELSE</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">FI</span><br/>
<span class="id" type="var">ELSE</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">FI</span>
<div class="paragraph"> </div>
</div>
Suppose the initial partial state is empty. We don't know
statically how <span class="inlinecode"><span class="id" type="var">Y</span></span> compares to <span class="inlinecode">4</span>, so we must partially evaluate
both branches of the (outer) conditional. On the <span class="inlinecode"><span class="id" type="var">THEN</span></span> branch,
we know that <span class="inlinecode"><span class="id" type="var">Y</span></span> is set to <span class="inlinecode">4</span> and can even use that knowledge to
simplify the code somewhat. On the <span class="inlinecode"><span class="id" type="var">ELSE</span></span> branch, we still don't
know the exact value of <span class="inlinecode"><span class="id" type="var">Y</span></span> at the end. What should the final
partial state and residual program be?
<div class="paragraph"> </div>
One way to handle such a dynamic conditional is to take the
intersection of the final partial states of the two branches. In
this example, we take the intersection of <span class="inlinecode">(<span class="id" type="var">Y</span>,4),(<span class="id" type="var">X</span>,3)</span> and
<span class="inlinecode">(<span class="id" type="var">X</span>,3)</span>, so the overall final partial state is <span class="inlinecode">(<span class="id" type="var">X</span>,3)</span>. To
compensate for forgetting that <span class="inlinecode"><span class="id" type="var">Y</span></span> is <span class="inlinecode">4</span>, we need to add an
assignment <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode">::=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode">4</span> to the end of the <span class="inlinecode"><span class="id" type="var">THEN</span></span> branch. So,
the residual program will be something like
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">SKIP</span>;<br/>
<span class="id" type="var">IFB</span> <span class="id" type="var">BLe</span> (<span class="id" type="var">AId</span> <span class="id" type="var">Y</span>) (<span class="id" type="var">ANum</span> 4) <span class="id" type="var">THEN</span><br/>
<span class="id" type="var">SKIP</span>;<br/>
<span class="id" type="var">SKIP</span>;<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">ANum</span> 4<br/>
<span class="id" type="var">ELSE</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">FI</span>
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
Programming this case in Coq calls for several auxiliary
functions: we need to compute the intersection of two <span class="inlinecode"><span class="id" type="var">pe_state</span></span>s
and turn their difference into sequences of assignments.
<div class="paragraph"> </div>
First, we show how to compute whether two <span class="inlinecode"><span class="id" type="var">pe_state</span></span>s to disagree
at a given variable. In the theorem <span class="inlinecode"><span class="id" type="var">pe_disagree_domain</span></span>, we
prove that two <span class="inlinecode"><span class="id" type="var">pe_state</span></span>s can only disagree at variables that
appear in at least one of them.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">pe_disagree_at</span> (<span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span> : <span class="id" type="var">pe_state</span>) (<span class="id" type="var">V</span>:<span class="id" type="var">id</span>) : <span class="id" type="var">bool</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">V</span>, <span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">Some</span> <span class="id" type="var">x</span>, <span class="id" type="var">Some</span> <span class="id" type="var">y</span> => <span class="id" type="var">negb</span> (<span class="id" type="var">beq_nat</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>)<br/>
| <span class="id" type="var">None</span>, <span class="id" type="var">None</span> => <span class="id" type="var">false</span><br/>
| <span class="id" type="var">_</span>, <span class="id" type="var">_</span> => <span class="id" type="var">true</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">existsb_app</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">X</span> (<span class="id" type="var">f</span>:<span class="id" type="var">X</span><span style="font-family: arial;">→</span><span class="id" type="var">bool</span>) <span class="id" type="var">l1</span> <span class="id" type="var">l2</span>,<br/>
<span class="id" type="var">existsb</span> <span class="id" type="var">f</span> (<span class="id" type="var">l1</span> ++ <span class="id" type="var">l2</span>) = <span class="id" type="var">orb</span> (<span class="id" type="var">existsb</span> <span class="id" type="var">f</span> <span class="id" type="var">l1</span>) (<span class="id" type="var">existsb</span> <span class="id" type="var">f</span> <span class="id" type="var">l2</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">X</span> <span class="id" type="var">f</span> <span class="id" type="var">l1</span> <span class="id" type="var">l2</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">l1</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHl1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">orb_assoc</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_disagree_domain</span>: <span style="font-family: arial;">∀</span>(<span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span> : <span class="id" type="var">pe_state</span>) (<span class="id" type="var">V</span>:<span class="id" type="var">id</span>),<br/>
<span class="id" type="var">true</span> = <span class="id" type="var">pe_disagree_at</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">true</span> = <span class="id" type="var">existsb</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span>) (<span class="id" type="var">map</span> (@<span class="id" type="var">fst</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span>) <span class="id" type="var">pe_st1</span> ++<br/>
<span class="id" type="var">map</span> (@<span class="id" type="var">fst</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span>) <span class="id" type="var">pe_st2</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">pe_disagree_at</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">existsb_app</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">orb_true_intro</span>.<br/>
<span class="id" type="var">remember</span> (<span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">V</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">lookup1</span>.<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">lookup1</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">n1</span>|]. <span class="id" type="var">left</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">pe_domain</span> <span class="id" type="keyword">with</span> <span class="id" type="var">n1</span>. <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="var">remember</span> (<span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">lookup2</span>.<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">lookup2</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">n2</span>|]. <span class="id" type="var">right</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">pe_domain</span> <span class="id" type="keyword">with</span> <span class="id" type="var">n2</span>. <span class="id" type="tactic">auto</span>.<br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
We define the <span class="inlinecode"><span class="id" type="var">pe_compare</span></span> function to list the variables where
two given <span class="inlinecode"><span class="id" type="var">pe_state</span></span>s disagree. This list is exact, according to
the theorem <span class="inlinecode"><span class="id" type="var">pe_compare_correct</span></span>: a variable appears on the list
if and only if the two given <span class="inlinecode"><span class="id" type="var">pe_state</span></span>s disagree at that
variable. Furthermore, we use the <span class="inlinecode"><span class="id" type="var">pe_unique</span></span> function to
eliminate duplicates from the list.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">pe_unique</span> (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">id</span>) : <span class="id" type="var">list</span> <span class="id" type="var">id</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
| [] => []<br/>
| <span class="id" type="var">x</span>::<span class="id" type="var">l</span> => <span class="id" type="var">x</span> :: <span class="id" type="var">filter</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">y</span> => <span class="id" type="var">negb</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>)) (<span class="id" type="var">pe_unique</span> <span class="id" type="var">l</span>)<br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">existsb_beq_id_filter</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">V</span> <span class="id" type="var">f</span> <span class="id" type="var">l</span>,<br/>
<span class="id" type="var">existsb</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span>) (<span class="id" type="var">filter</span> <span class="id" type="var">f</span> <span class="id" type="var">l</span>) = <span class="id" type="var">andb</span> (<span class="id" type="var">existsb</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span>) <span class="id" type="var">l</span>) (<span class="id" type="var">f</span> <span class="id" type="var">V</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">V</span> <span class="id" type="var">f</span> <span class="id" type="var">l</span>. <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">h</span> <span class="id" type="var">l</span>].<br/>
<span class="id" type="var">Case</span> "[]". <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">Case</span> "h::l". <span class="id" type="tactic">simpl</span>. <span class="id" type="var">remember</span> (<span class="id" type="var">f</span> <span class="id" type="var">h</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">fh</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">fh</span>.<br/>
<span class="id" type="var">SCase</span> "true = f h". <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="var">compare</span> <span class="id" type="var">V</span> <span class="id" type="var">h</span> <span class="id" type="var">SSCase</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span style="font-family: arial;">←</span> <span class="id" type="var">Heqfh</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">SCase</span> "false = f h". <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHl</span>. <span class="id" type="var">compare</span> <span class="id" type="var">V</span> <span class="id" type="var">h</span> <span class="id" type="var">SSCase</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span style="font-family: arial;">←</span> <span class="id" type="var">Heqfh</span>. <span class="id" type="tactic">rewrite</span> !<span class="id" type="var">andb_false_r</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_unique_correct</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">l</span> <span class="id" type="var">x</span>,<br/>
<span class="id" type="var">existsb</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">x</span>) <span class="id" type="var">l</span> = <span class="id" type="var">existsb</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">x</span>) (<span class="id" type="var">pe_unique</span> <span class="id" type="var">l</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">l</span> <span class="id" type="var">x</span>. <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">h</span> <span class="id" type="var">t</span>]. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> *. <span class="id" type="var">compare</span> <span class="id" type="var">x</span> <span class="id" type="var">h</span> <span class="id" type="var">Case</span>.<br/>
<span class="id" type="var">Case</span> "equal". <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">Case</span> "not equal".<br/>
<span class="id" type="tactic">rewrite</span> <span style="font-family: arial;">→</span> <span class="id" type="var">existsb_beq_id_filter</span>, <span style="font-family: arial;">←</span> <span class="id" type="var">IHt</span>, <span style="font-family: arial;">→</span> <span class="id" type="var">beq_id_sym</span>, <span style="font-family: arial;">→</span> <span class="id" type="var">Heqxh</span>,<br/>
<span style="font-family: arial;">→</span> <span class="id" type="var">andb_true_r</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">pe_compare</span> (<span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span> : <span class="id" type="var">pe_state</span>) : <span class="id" type="var">list</span> <span class="id" type="var">id</span> :=<br/>
<span class="id" type="var">pe_unique</span> (<span class="id" type="var">filter</span> (<span class="id" type="var">pe_disagree_at</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span>)<br/>
(<span class="id" type="var">map</span> (@<span class="id" type="var">fst</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span>) <span class="id" type="var">pe_st1</span> ++ <span class="id" type="var">map</span> (@<span class="id" type="var">fst</span> <span class="id" type="var">_</span> <span class="id" type="var">_</span>) <span class="id" type="var">pe_st2</span>)).<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_compare_correct</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span>,<br/>
<span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">V</span> = <span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span> <span style="font-family: arial;">↔</span><br/>
<span class="id" type="var">false</span> = <span class="id" type="var">existsb</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span>) (<span class="id" type="var">pe_compare</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">pe_compare</span>. <span class="id" type="tactic">rewrite</span> <span style="font-family: arial;">←</span> <span class="id" type="var">pe_unique_correct</span>, <span style="font-family: arial;">→</span> <span class="id" type="var">existsb_beq_id_filter</span>.<br/>
<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">Heq</span>.<br/>
<span class="id" type="var">Case</span> "<span style="font-family: arial;">→</span>".<br/>
<span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">andb_false_intro2</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">pe_disagree_at</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">Heq</span>.<br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span>).<br/>
<span class="id" type="tactic">rewrite</span> <span style="font-family: arial;">←</span> <span class="id" type="var">beq_nat_refl</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="var">Case</span> "<span style="font-family: arial;">←</span>".<br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">Hagree</span>: <span class="id" type="var">pe_disagree_at</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span> = <span class="id" type="var">false</span>).<br/>
<span class="id" type="var">SCase</span> "Proof of assertion".<br/>
<span class="id" type="var">remember</span> (<span class="id" type="var">pe_disagree_at</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">disagree</span>.<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">disagree</span>; [| <span class="id" type="tactic">reflexivity</span>].<br/>
<span class="id" type="tactic">rewrite</span> <span style="font-family: arial;">→</span> <span class="id" type="var">andb_true_r</span>, <span style="font-family: arial;">←</span> <span class="id" type="var">pe_disagree_domain</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Heq</span>.<br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heq</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">Heqdisagree</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">pe_disagree_at</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hagree</span>.<br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">V</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">n1</span>|];<br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">n2</span>|];<br/>
<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</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="tactic">rewrite</span> <span class="id" type="var">beq_nat_eq</span> <span class="id" type="keyword">with</span> <span class="id" type="var">n1</span> <span class="id" type="var">n2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span style="font-family: arial;">←</span> <span class="id" type="var">negb_involutive</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hagree</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
The intersection of two partial states is the result of removing
from one of them all the variables where the two disagree. We
define the function <span class="inlinecode"><span class="id" type="var">pe_removes</span></span>, in terms of <span class="inlinecode"><span class="id" type="var">pe_remove</span></span> above,
to perform such a removal of a whole list of variables at once.
<div class="paragraph"> </div>
The theorem <span class="inlinecode"><span class="id" type="var">pe_compare_removes</span></span> testifies that the <span class="inlinecode"><span class="id" type="var">pe_lookup</span></span>
interpretation of the result of this intersection operation is the
same no matter which of the two partial states we remove the
variables from. Because <span class="inlinecode"><span class="id" type="var">pe_override</span></span> only depends on the
<span class="inlinecode"><span class="id" type="var">pe_lookup</span></span> interpretation of partial states, <span class="inlinecode"><span class="id" type="var">pe_override</span></span> also
does not care which of the two partial states we remove the
variables from; that theorem <span class="inlinecode"><span class="id" type="var">pe_compare_override</span></span> is used in the
correctness proof shortly.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">pe_removes</span> (<span class="id" type="var">pe_st</span>:<span class="id" type="var">pe_state</span>) (<span class="id" type="var">ids</span> : <span class="id" type="var">list</span> <span class="id" type="var">id</span>) : <span class="id" type="var">pe_state</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">ids</span> <span class="id" type="keyword">with</span><br/>
| [] => <span class="id" type="var">pe_st</span><br/>
| <span class="id" type="var">V</span>::<span class="id" type="var">ids</span> => <span class="id" type="var">pe_remove</span> (<span class="id" type="var">pe_removes</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">ids</span>) <span class="id" type="var">V</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_removes_correct</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">pe_st</span> <span class="id" type="var">ids</span> <span class="id" type="var">V</span>,<br/>
<span class="id" type="var">pe_lookup</span> (<span class="id" type="var">pe_removes</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">ids</span>) <span class="id" type="var">V</span> =<br/>
<span class="id" type="keyword">if</span> <span class="id" type="var">existsb</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span>) <span class="id" type="var">ids</span> <span class="id" type="keyword">then</span> <span class="id" type="var">None</span> <span class="id" type="keyword">else</span> <span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">ids</span> <span class="id" type="var">V</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">ids</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">V'</span> <span class="id" type="var">ids</span>]. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">pe_remove_correct</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHids</span>.<br/>
<span class="id" type="tactic">replace</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V'</span> <span class="id" type="var">V</span>) <span class="id" type="keyword">with</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span> <span class="id" type="var">V'</span>) <span class="id" type="tactic">by</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">beq_id_sym</span>.<br/>
<span class="id" type="tactic">destruct</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span> <span class="id" type="var">V'</span>); <span class="id" type="tactic">destruct</span> (<span class="id" type="var">existsb</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span>) <span class="id" type="var">ids</span>); <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_compare_removes</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span>,<br/>
<span class="id" type="var">pe_lookup</span> (<span class="id" type="var">pe_removes</span> <span class="id" type="var">pe_st1</span> (<span class="id" type="var">pe_compare</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span>)) <span class="id" type="var">V</span> =<br/>
<span class="id" type="var">pe_lookup</span> (<span class="id" type="var">pe_removes</span> <span class="id" type="var">pe_st2</span> (<span class="id" type="var">pe_compare</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span>)) <span class="id" type="var">V</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">V</span>. <span class="id" type="tactic">rewrite</span> !<span class="id" type="var">pe_removes_correct</span>.<br/>
<span class="id" type="var">remember</span> (<span class="id" type="var">existsb</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span>) (<span class="id" type="var">pe_compare</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span>)) <span class="id" type="keyword">as</span> <span class="id" type="var">b</span>.<br/>
<span class="id" type="tactic">destruct</span> <span class="id" type="var">b</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">pe_compare_correct</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Heqb</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">Heqb</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pe_compare_override</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span> <span class="id" type="var">st</span>,<br/>
<span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> (<span class="id" type="var">pe_removes</span> <span class="id" type="var">pe_st1</span> (<span class="id" type="var">pe_compare</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span>)) =<br/>
<span class="id" type="var">pe_override</span> <span class="id" type="var">st</span> (<span class="id" type="var">pe_removes</span> <span class="id" type="var">pe_st2</span> (<span class="id" type="var">pe_compare</span> <span class="id" type="var">pe_st1</span> <span class="id" type="var">pe_st2</span>)).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">functional_extensionality</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">V</span>.<br/>
<span class="id" type="tactic">rewrite</span> !<span class="id" type="var">pe_override_correct</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">pe_compare_removes</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
Finally, we define an <span class="inlinecode"><span class="id" type="var">assign</span></span> function to turn the difference
between two partial states into a sequence of assignment commands.
More precisely, <span class="inlinecode"><span class="id" type="var">assign</span></span> <span class="inlinecode"><span class="id" type="var">pe_st</span></span> <span class="inlinecode"><span class="id" type="var">ids</span></span> generates an assignment command
for each variable listed in <span class="inlinecode"><span class="id" type="var">ids</span></span>.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">assign</span> (<span class="id" type="var">pe_st</span> : <span class="id" type="var">pe_state</span>) (<span class="id" type="var">ids</span> : <span class="id" type="var">list</span> <span class="id" type="var">id</span>) : <span class="id" type="var">com</span> :=<br/>
<span class="id" type="keyword">match</span> <span class="id" type="var">ids</span> <span class="id" type="keyword">with</span><br/>
| [] => <span class="id" type="var">SKIP</span><br/>
| <span class="id" type="var">V</span>::<span class="id" type="var">ids</span> => <span class="id" type="keyword">match</span> <span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">Some</span> <span class="id" type="var">n</span> => (<span class="id" type="var">assign</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">ids</span>; <span class="id" type="var">V</span> ::= <span class="id" type="var">ANum</span> <span class="id" type="var">n</span>)<br/>
| <span class="id" type="var">None</span> => <span class="id" type="var">assign</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">ids</span><br/>
<span class="id" type="keyword">end</span><br/>
<span class="id" type="keyword">end</span>.<br/>
<br/>
</div>
<div class="doc">
The command generated by <span class="inlinecode"><span class="id" type="var">assign</span></span> always terminates, because it is
just a sequence of assignments. The (total) function <span class="inlinecode"><span class="id" type="var">assigned</span></span>
below computes the effect of the command on the (dynamic state).
The theorem <span class="inlinecode"><span class="id" type="var">assign_removes</span></span> then confirms that the generated
assignments perfectly compensate for removing the variables from
the partial state.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">assigned</span> (<span class="id" type="var">pe_st</span>:<span class="id" type="var">pe_state</span>) (<span class="id" type="var">ids</span> : <span class="id" type="var">list</span> <span class="id" type="var">id</span>) (<span class="id" type="var">st</span>:<span class="id" type="var">state</span>) : <span class="id" type="var">state</span> :=<br/>
<span class="id" type="keyword">fun</span> <span class="id" type="var">V</span> => <span class="id" type="keyword">match</span> <span class="id" type="var">existsb</span> (<span class="id" type="var">beq_id</span> <span class="id" type="var">V</span>) <span class="id" type="var">ids</span>, <span class="id" type="var">pe_lookup</span> <span class="id" type="var">pe_st</span> <span class="id" type="var">V</span> <span class="id" type="keyword">with</span><br/>
| <span class="id" type="var">true</span>, <span class="id" type="var">Some</span> <span class="id" type="var">n</span> => <span class="id" type="var">n</span><br/>
| <span class="id" type="var">_</span>, <span class="id" type="var">_</span> => <span class="id" type="var">st</span> <span class="id" type="var">V</span><br/>