-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathEquiv.html
2693 lines (2156 loc) · 269 KB
/
Equiv.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=utf-8"/>
<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
<title>Equiv: Program Equivalence</title>
<script type="text/javascript" src="jquery-1.8.3.js"></script>
<script type="text/javascript" src="main.js"></script>
</head>
<body>
<div id="page">
<div id="header">
</div>
<div id="main">
<h1 class="libtitle">Equiv<span class="subtitle">Program Equivalence</span></h1>
<div class="code code-tight">
</div>
<div class="doc">
</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/>
<br/>
</div>
<div class="doc">
<a name="lab453"></a><h3 class="section">一些关于练习的一般性建议:</h3>
<div class="paragraph"> </div>
<ul class="doclist">
<li> 这里要进行的大多数Coq证明都与先前我们所提供的相似. 在做作业之前, 花一些时间
（非形式化的在纸上和Coq中）思考我们的证明确保你理解他们的的每一个细节. 这会节省你
大量的时间.
<div class="paragraph"> </div>
</li>
<li> 我们现在进行的Coq证明已经足够复杂，以至于近乎不可能单靠“灵感”或者以随机的尝试误打误撞的完成证明。你需要一个关于为何
某个属性为真以及如何进行证明的概念并从这个概念开始。完成这一项任务的最好的方
法是在开始进行形式化证明之前至少在纸上写出一个非形式化证明的梗概
<ul class="doclist">
<li>-直观的说服自己相信定理成立—然后再进行形式化证明。另外，
</li>
</ul>
你也可以拉来一个好友，尝试说服他相信这条定理成立; 然后试着形式化你刚才的解释。
<div class="paragraph"> </div>
</li>
<li> 使用自动化工具来减少工作量！本章的一些证明练习，如果全部一个个分类去分析的话
会非常长.
</li>
</ul>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab454"></a><h1 class="section">行为的等价性</h1>
<div class="paragraph"> </div>
在上一章中我们讨论了一个非常简单的程序变换的正确性; <span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span> 函数。
这是我们考虑的算数表达式语言的第一个版本—它没有变量—所以很容易定义 <i>什么是</i>
正确的程序变换： 即输出一个求值结果与原程序相同的程序。
<div class="paragraph"> </div>
为了更进一步的讨论整个Imp语言变换的正确性，我们需要考虑状态和变量的作用。
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab455"></a><h2 class="section">定义</h2>
<div class="paragraph"> </div>
对于包含变量的 <span class="inlinecode"><span class="id" type="var">aexp</span></span> 和 <span class="inlinecode"><span class="id" type="var">bexp</span></span>, 我们需要的定义简单明了。在 <i>所有状态</i>
下两个 <span class="inlinecode"><span class="id" type="var">aexp</span></span> 或者 <span class="inlinecode"><span class="id" type="var">bexp</span></span> 的求值结果相同，我们就说他们 <i>行为等价</i> 。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">aequiv</span> (<span class="id" type="var">a1</span> <span class="id" type="var">a2</span> : <span class="id" type="var">aexp</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
<span style="font-family: arial;">∀</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">st</span> <span class="id" type="var">a1</span> = <span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a2</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">bequiv</span> (<span class="id" type="var">b1</span> <span class="id" type="var">b2</span> : <span class="id" type="var">bexp</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
<span style="font-family: arial;">∀</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">st</span> <span class="id" type="var">b1</span> = <span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b2</span>.<br/>
<br/>
</div>
<div class="doc">
对于命令，情况有些微妙。我们不能简单的说：“如果两个指令在相同的初始状态下求值到相同
的终止状态，那么说这两个指令等价。”，因为有些命令（在某些初始状态下）根本不会在任何
状态终止！我们实际上需要的是：“若两个指令在给出任何初始状态时都发散或者终止在相同
的状态上，则这两个指令行为等价。”。简单的说就是：“如果其中一个终止在某
状态上那么另一个也终止在这个状态上，反之亦然。”
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">cequiv</span> (<span class="id" type="var">c1</span> <span class="id" type="var">c2</span> : <span class="id" type="var">com</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
<span style="font-family: arial;">∀</span>(<span class="id" type="var">st</span> <span class="id" type="var">st'</span> : <span class="id" type="var">state</span>), <br/>
(<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">st'</span>) <span style="font-family: arial;">↔</span> (<span class="id" type="var">c2</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st'</span>).<br/>
<br/>
</div>
<div class="doc">
<a name="lab456"></a><h4 class="section">Exercise: 2 stars (equiv_classes)</h4>
<div class="paragraph"> </div>
下面将给出一些程序，请按在<span class="inlinecode"><span class="id" type="var">Imp</span></span>中是否等价将这些程序分组。你的答案应该是一个列表的列表
其中每个子列表代表一组互相等价的程序。例如，你认为除了程序i之外剩下的都是等价的，那么你的答案
应该像这个样子：
<div class="paragraph"> </div>
<div class="paragraph"> </div>
<div class="code code-tight">
[ [<span class="id" type="var">prog_a</span>;<span class="id" type="var">prog_b</span>;<span class="id" type="var">prog_c</span>;<span class="id" type="var">prog_d</span>;<span class="id" type="var">prog_e</span>;<span class="id" type="var">prog_f</span>;<span class="id" type="var">prog_g</span>;<span class="id" type="var">prog_h</span>] ;<br/>
[<span class="id" type="var">prog_i</span>] ]
<div class="paragraph"> </div>
</div>
<div class="paragraph"> </div>
在 <span class="inlinecode"><span class="id" type="var">equiv_classes</span></span> 的定义下面写出你的答案。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_a</span> : <span class="id" type="var">com</span> :=<br/>
<span class="id" type="var">WHILE</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">ANum</span> 0)) <span class="id" type="var">DO</span><br/>
<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)<br/>
<span class="id" type="var">END</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_b</span> : <span class="id" type="var">com</span> :=<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">ANum</span> 0) <span class="id" type="var">THEN</span><br/>
<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);;<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">ANum</span> 1<br/>
<span class="id" type="var">ELSE</span><br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">ANum</span> 0<br/>
<span class="id" type="var">FI</span>;;<br/>
<span class="id" type="var">X</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>);;<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">ANum</span> 0.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_c</span> : <span class="id" type="var">com</span> :=<br/>
<span class="id" type="var">SKIP</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_d</span> : <span class="id" type="var">com</span> :=<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">BNot</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">ANum</span> 0)) <span class="id" type="var">DO</span><br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">APlus</span> (<span class="id" type="var">AMult</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">ANum</span> 1)<br/>
<span class="id" type="var">END</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_e</span> : <span class="id" type="var">com</span> :=<br/>
<span class="id" type="var">Y</span> ::= <span class="id" type="var">ANum</span> 0.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_f</span> : <span class="id" type="var">com</span> :=<br/>
<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);;<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">BNot</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">DO</span><br/>
<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)<br/>
<span class="id" type="var">END</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_g</span> : <span class="id" type="var">com</span> :=<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">BTrue</span> <span class="id" type="var">DO</span><br/>
<span class="id" type="var">SKIP</span><br/>
<span class="id" type="var">END</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_h</span> : <span class="id" type="var">com</span> :=<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">BNot</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">X</span>)) <span class="id" type="var">DO</span><br/>
<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)<br/>
<span class="id" type="var">END</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_i</span> : <span class="id" type="var">com</span> :=<br/>
<span class="id" type="var">WHILE</span> <span class="id" type="var">BNot</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">DO</span><br/>
<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">Y</span>) (<span class="id" type="var">ANum</span> 1)<br/>
<span class="id" type="var">END</span>.<br/>
<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">equiv_classes</span> : <span class="id" type="var">list</span> (<span class="id" type="var">list</span> <span class="id" type="var">com</span>) :=<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" type="var">admit</span>.<br/>
<span class="comment">(* GRADE_TEST 2: check_equiv_classes equiv_classes *)</span><br/>
</div>
<div class="doc">
<font size=-2>☐</font>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab457"></a><h2 class="section">例子</h2>
<div class="paragraph"> </div>
这里有些关于算数表达式和布尔表达式等价的例子.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">aequiv_example</span>:<br/>
<span class="id" type="var">aequiv</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">X</span>)) (<span class="id" type="var">ANum</span> 0).<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">bequiv_example</span>:<br/>
<span class="id" type="var">bequiv</span> (<span class="id" type="var">BEq</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">X</span>)) (<span class="id" type="var">ANum</span> 0)) <span class="id" type="var">BTrue</span>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">beval</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">aequiv_example</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
</div>
<div class="doc">
这里是一些命令等价的例子，让我们从包含<span class="inlinecode"><span class="id" type="var">SKIP</span></span>的简单的程序变换开始:
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">skip_left</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">c</span>,<br/>
<span class="id" type="var">cequiv</span> <br/>
(<span class="id" type="var">SKIP</span>;; <span class="id" type="var">c</span>) <br/>
<span class="id" type="var">c</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(* WORKED IN CLASS *)</span><br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
- <span class="comment">(* -> *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">subst</span>.<br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H2</span>. <span class="id" type="tactic">subst</span>.<br/>
<span class="id" type="tactic">assumption</span>.<br/>
- <span class="comment">(* <- *)</span><br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Seq</span> <span class="id" type="keyword">with</span> <span class="id" type="var">st</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Skip</span>.<br/>
<span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab458"></a><h4 class="section">Exercise: 2 stars (skip_right)</h4>
试证在任一命令后加上SKIP所变换出的新程序与原程序等价。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">skip_right</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">c</span>,<br/>
<span class="id" type="var">cequiv</span> <br/>
(<span class="id" type="var">c</span>;; <span class="id" type="var">SKIP</span>) <br/>
<span class="id" type="var">c</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>
<div class="doc">
<font size=-2>☐</font>
<div class="paragraph"> </div>
类似的，这里是一些简化 <span class="inlinecode"><span class="id" type="var">IFB</span></span> 的简单变换:
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">IFB_true_simple</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">c1</span> <span class="id" type="var">c2</span>,<br/>
<span class="id" type="var">cequiv</span> <br/>
(<span class="id" type="var">IFB</span> <span class="id" type="var">BTrue</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c1</span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c2</span> <span class="id" type="var">FI</span>) <br/>
<span class="id" type="var">c1</span>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">c1</span> <span class="id" type="var">c2</span>.<br/>
<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
- <span class="comment">(* -> *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H5</span>.<br/>
- <span class="comment">(* <- *)</span><br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfTrue</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
</div>
<div class="doc">
当然，一些程序员会尝试以IF的判断条件字面上是否等于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span> 作为优化前提。但一个
更有趣的方式是看IF的判断条件是否等价于真:
<div class="paragraph"> </div>
<i>Theorem</i>: 如果 <span class="inlinecode"><span class="id" type="var">b</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span>, 那么 <span class="inlinecode"><span class="id" type="var">IFB</span></span> <span class="inlinecode"><span class="id" type="var">b</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> 等价于 <span class="inlinecode"><span class="id" type="var">c1</span></span>.
<a name="lab459"></a><h3 class="section"> </h3>
<div class="paragraph"> </div>
<i>Proof</i>:
<div class="paragraph"> </div>
<ul class="doclist">
<li> (<span class="inlinecode"><span style="font-family: arial;">→</span></span>) 我们必须证明, 对于所有 <span class="inlinecode"><span class="id" type="var">st</span></span> 和 <span class="inlinecode"><span class="id" type="var">st'</span></span>, 如果 <span class="inlinecode"><span class="id" type="var">IFB</span></span> <span class="inlinecode"><span class="id" type="var">b</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> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 则 <span class="inlinecode"><span class="id" type="var">c1</span></span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.
<div class="paragraph"> </div>
能够应用于 <span class="inlinecode"><span class="id" type="var">IFB</span></span> <span class="inlinecode"><span class="id" type="var">b</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> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 的证明规则只有两条：
<span class="inlinecode"><span class="id" type="var">E_IfTrue</span></span> 和 <span class="inlinecode"><span class="id" type="var">E_IfFalse</span></span>.
<div class="paragraph"> </div>
<ul class="doclist">
<li> 假设 <span class="inlinecode"><span class="id" type="var">IFB</span></span> <span class="inlinecode"><span class="id" type="var">b</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> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 证明自 <span class="inlinecode"><span class="id" type="var">E_IfTrue</span></span>
这条证明规则. 若使用证明规则 <span class="inlinecode"><span class="id" type="var">E_IfTrue</span></span> 其必备的前提条件 <span class="inlinecode"><span class="id" type="var">c1</span></span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 必为真， 而这正好是
我们的证明所需要的条件。
<div class="paragraph"> </div>
</li>
<li> 另一方面, 假设 <span class="inlinecode"><span class="id" type="var">IFB</span></span> <span class="inlinecode"><span class="id" type="var">b</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> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 证明自
<span class="inlinecode"><span class="id" type="var">E_IfFalse</span></span>. 我们能得知 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span> 和 <span class="inlinecode"><span class="id" type="var">c2</span></span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.
<div class="paragraph"> </div>
之前提到 <span class="inlinecode"><span class="id" type="var">b</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span>, 也就是说对于所有 <span class="inlinecode"><span class="id" type="var">st</span></span>, 有<span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">BTrue</span></span>.
具体的说就是 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span> 成立, 导致 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">BTrue</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span> 成立。
但是与此同时，之前假设 <span class="inlinecode"><span class="id" type="var">E_IfFalse</span></span> 必备的前提条件 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span> 也成立，
这就构成了一组矛盾。从而说明不可能使用了 <span class="inlinecode"><span class="id" type="var">E_IfFalse</span></span> 这条证明规则。
<div class="paragraph"> </div>
</li>
</ul>
</li>
<li> (<span class="inlinecode"><span style="font-family: arial;">←</span></span>) 我们必须证明，对于所有 <span class="inlinecode"><span class="id" type="var">st</span></span> 和 <span class="inlinecode"><span class="id" type="var">st'</span></span>, 如果 <span class="inlinecode"><span class="id" type="var">c1</span></span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span>
则 <span class="inlinecode"><span class="id" type="var">IFB</span></span> <span class="inlinecode"><span class="id" type="var">b</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> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.
<div class="paragraph"> </div>
已知 <span class="inlinecode"><span class="id" type="var">b</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span>, 我们知道 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> = <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">BTrue</span></span> = <span class="inlinecode"><span class="id" type="var">true</span></span>.
结合 <span class="inlinecode"><span class="id" type="var">c1</span></span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 这条假设, 我们能应用 <span class="inlinecode"><span class="id" type="var">E_IfTrue</span></span> 来证明出 <span class="inlinecode"><span class="id" type="var">IFB</span></span> <span class="inlinecode"><span class="id" type="var">b</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> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span>. <font size=-2>☐</font>
</li>
</ul>
<div class="paragraph"> </div>
下面是这个证明的形式化版本:
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">IFB_true</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">b</span> <span class="id" type="var">c1</span> <span class="id" type="var">c2</span>,<br/>
<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BTrue</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">cequiv</span> <br/>
(<span class="id" type="var">IFB</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c1</span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c2</span> <span class="id" type="var">FI</span>) <br/>
<span class="id" type="var">c1</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">c1</span> <span class="id" type="var">c2</span> <span class="id" type="var">Hb</span>.<br/>
<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
- <span class="comment">(* -> *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
+ <span class="comment">(* b 求值得出 true *)</span><br/>
<span class="id" type="tactic">assumption</span>.<br/>
+ <span class="comment">(* b 求值得出 false (矛盾) *)</span><br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H5</span>.<br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H5</span>.<br/>
- <span class="comment">(* <- *)</span><br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfTrue</span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab460"></a><h4 class="section">Exercise: 2 stars (IFB_false)</h4>
</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">IFB_false</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">b</span> <span class="id" type="var">c1</span> <span class="id" type="var">c2</span>,<br/>
<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BFalse</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">cequiv</span> <br/>
(<span class="id" type="var">IFB</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c1</span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c2</span> <span class="id" type="var">FI</span>) <br/>
<span class="id" type="var">c2</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>
<div class="doc">
<font size=-2>☐</font>
<div class="paragraph"> </div>
<a name="lab461"></a><h4 class="section">Exercise: 3 stars (swap_if_branches)</h4>
证明我们可以通过对条件取反来交换 IF 的两个分支
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">swap_if_branches</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">b</span> <span class="id" type="var">e1</span> <span class="id" type="var">e2</span>,<br/>
<span class="id" type="var">cequiv</span><br/>
(<span class="id" type="var">IFB</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">e1</span> <span class="id" type="var">ELSE</span> <span class="id" type="var">e2</span> <span class="id" type="var">FI</span>)<br/>
(<span class="id" type="var">IFB</span> <span class="id" type="var">BNot</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">e2</span> <span class="id" type="var">ELSE</span> <span class="id" type="var">e1</span> <span class="id" type="var">FI</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>
<div class="doc">
<font size=-2>☐</font>
<div class="paragraph"> </div>
<a name="lab462"></a><h3 class="section"> </h3>
<div class="paragraph"> </div>
对于 <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 循环我们能够给出一组相似的定理：当一个循环的条件等价于 <span class="inlinecode"><span class="id" type="var">BFalse</span></span> 的
时候它等价于 <span class="inlinecode"><span class="id" type="var">SKIP</span></span>, 当一个循环的条件等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span> 的时候它等价于
<span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">BTrue</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">SKIP</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> （或者任意不终止的程序）。
前者比较简单.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">WHILE_false</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BFalse</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">cequiv</span><br/>
(<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>)<br/>
<span class="id" type="var">SKIP</span>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">Hb</span>. <span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
- <span class="comment">(* -> *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
+ <span class="comment">(* E_WhileEnd *)</span><br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Skip</span>.<br/>
+ <span class="comment">(* E_WhileLoop *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H2</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H2</span>.<br/>
- <span class="comment">(* <- *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileEnd</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span>.<br/>
<span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
</div>
<div class="doc">
<a name="lab463"></a><h4 class="section">Exercise: 2 stars, advanced, optional (WHILE_false_informal)</h4>
写出 <span class="inlinecode"><span class="id" type="var">WHILE_false</span></span> 的非形式化证明.
<div class="paragraph"> </div>
<span class="comment">(* FILL IN HERE *)</span><br/>
<font size=-2>☐</font>
<div class="paragraph"> </div>
<a name="lab464"></a><h3 class="section"> </h3>
为了证明第2个定理, 我们需要一个辅助定理: <span class="inlinecode"><span class="id" type="var">WHILE</span></span> 循环在条件等价于
<span class="inlinecode"><span class="id" type="var">BTrue</span></span> 的时候循环不会终止:
<div class="paragraph"> </div>
<i>Lemma</i>: 如果 <span class="inlinecode"><span class="id" type="var">b</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span>, 则不可能像
<span class="inlinecode">(<span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span>)</span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 这样会终止。
<div class="paragraph"> </div>
<i>Proof</i>: 假设循环会终止，即 <span class="inlinecode">(<span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span>)</span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span>. 我们将证明在通过
对 <span class="inlinecode">(<span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span>)</span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 使用归纳法可以引出矛盾。
<div class="paragraph"> </div>
<ul class="doclist">
<li> 假设 <span class="inlinecode">(<span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span>)</span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 使用了 <span class="inlinecode"><span class="id" type="var">E_WhileEnd</span></span> 这条证明规则。
那么根据假设得出 <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span> 。但是这和 <span class="inlinecode"><span class="id" type="var">b</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">BTrue</span></span> 矛盾。
<div class="paragraph"> </div>
</li>
<li> 假设 <span class="inlinecode">(<span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span>)</span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 使用了 <span class="inlinecode"><span class="id" type="var">E_WhileLoop</span></span> 这条证明规则.
结果就是给出了一个和 <span class="inlinecode">(<span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span>)</span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 矛盾的假设, 正巧是
我们正要证明的那个!
<div class="paragraph"> </div>
</li>
<li> 由于只有以上的几条规则可以证明出 <span class="inlinecode">(<span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span>)</span> <span class="inlinecode">/</span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span style="font-family: arial;">⇓</span></span> <span class="inlinecode"><span class="id" type="var">st'</span></span> 所以归纳时
的其他的情况会立即导致矛盾。 <font size=-2>☐</font>
</li>
</ul>
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">WHILE_true_nonterm</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>,<br/>
<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BTrue</span> <span style="font-family: arial;">→</span><br/>
~( (<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>) / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st'</span> ).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(* WORKED IN CLASS *)</span><br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">Hb</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="var">remember</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">cw</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqcw</span>.<br/>
<span class="id" type="tactic">induction</span> <span class="id" type="var">H</span>;<br/>
<span class="comment">(* 大多数证明规则不可能应用，我们可以用 反演（inversion）来去除他们 *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqcw</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">clear</span> <span class="id" type="var">Heqcw</span>.<br/>
<span class="comment">(* 我们只关心这两个关于 WHILE 循环的证明规则: *)</span><br/>
- <span class="comment">(* E_WhileEnd *)</span> <span class="comment">(* 矛盾 -- b 总是 true! *)</span><br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>.<br/>
<span class="comment">(* <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span> 能实例化Hb中的变量 <span class="inlinecode"><span class="id" type="var">st</span></span> *)</span><br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
- <span class="comment">(* E_WhileLoop *)</span> <span class="comment">(* 直接使用IH *)</span><br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">IHceval2</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab465"></a><h4 class="section">Exercise: 2 stars, optional (WHILE_true_nonterm_informal)</h4>
试解释 <span class="inlinecode"><span class="id" type="var">WHILE_true_nonterm</span></span> 的意义。
<div class="paragraph"> </div>
<span class="comment">(* FILL IN HERE *)</span><br/>
<font size=-2>☐</font>
<div class="paragraph"> </div>
<a name="lab466"></a><h4 class="section">Exercise: 2 stars (WHILE_true)</h4>
证明下面的定理. <i>提示</i> : 你可能需要使用 <span class="inlinecode"><span class="id" type="var">WHILE_true_nonterm</span></span>.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">WHILE_true</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BTrue</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">cequiv</span> <br/>
(<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>)<br/>
(<span class="id" type="var">WHILE</span> <span class="id" type="var">BTrue</span> <span class="id" type="var">DO</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">END</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>
<div class="doc">
<font size=-2>☐</font>
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">loop_unrolling</span>: <span style="font-family: arial;">∀</span><span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
<span class="id" type="var">cequiv</span><br/>
(<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>)<br/>
(<span class="id" type="var">IFB</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> (<span class="id" type="var">c</span>;; <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>) <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="keyword">Proof</span>.<br/>
<span class="comment">(* WORKED IN CLASS *)</span><br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">Hce</span>.<br/>
- <span class="comment">(* -> *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hce</span>; <span class="id" type="tactic">subst</span>.<br/>
+ <span class="comment">(* 不执行循环 *)</span><br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfFalse</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_Skip</span>.<br/>
+ <span class="comment">(* 执行循环 *)</span><br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfTrue</span>. <span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Seq</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st'</span> := <span class="id" type="var">st'0</span>). <span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">assumption</span>.<br/>
- <span class="comment">(* <- *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hce</span>; <span class="id" type="tactic">subst</span>.<br/>
+ <span class="comment">(* 执行循环 *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H5</span>; <span class="id" type="tactic">subst</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileLoop</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st'</span> := <span class="id" type="var">st'0</span>).<br/>
<span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">assumption</span>.<br/>
+ <span class="comment">(* 不执行循环 *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H5</span>; <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileEnd</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
</div>
<div class="doc">
<a name="lab467"></a><h4 class="section">Exercise: 2 stars, optional (seq_assoc)</h4>
</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">seq_assoc</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">c1</span> <span class="id" type="var">c2</span> <span class="id" type="var">c3</span>,<br/>
<span class="id" type="var">cequiv</span> ((<span class="id" type="var">c1</span>;;<span class="id" type="var">c2</span>);;<span class="id" type="var">c3</span>) (<span class="id" type="var">c1</span>;;(<span class="id" type="var">c2</span>;;<span class="id" type="var">c3</span>)).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>
<div class="doc">
<font size=-2>☐</font>
<div class="paragraph"> </div>
<a name="lab468"></a><h2 class="section">外延公理</h2>
<div class="paragraph"> </div>
最后, 我们来看看含有赋值的简单等价.
比如, 我们也许会希望能够证明 <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">::=</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">SKIP</span></span> 等价。但是，
我们当试着证明它的时候, 我们会以一种很奇妙的方式卡住。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">identity_assignment_first_try</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">X</span>:<span class="id" type="var">id</span>),<br/>
<span class="id" type="var">cequiv</span> (<span class="id" type="var">X</span> ::= <span class="id" type="var">AId</span> <span class="id" type="var">X</span>) <span class="id" type="var">SKIP</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">split</span>; <span class="id" type="tactic">intro</span> <span class="id" type="var">H</span>.<br/>
- <span class="comment">(* -> *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">simpl</span>.<br/>
<span class="id" type="tactic">replace</span> (<span class="id" type="var">update</span> <span class="id" type="var">st</span> <span class="id" type="var">X</span> (<span class="id" type="var">st</span> <span class="id" type="var">X</span>)) <span class="id" type="keyword">with</span> <span class="id" type="var">st</span>.<br/>
<span class="id" type="var">constructor</span>.<br/>
<span class="comment">(* 卡住了... *)</span> <span class="id" type="keyword">Abort</span>.<br/>
<br/>
</div>
<div class="doc">
现在我们卡住了. 虽然结论看起来很合理，但是实际上它是无法证明的! 如果我们回顾在上一章
我们曾证明的有关 <span class="inlinecode"><span class="id" type="var">update</span></span> 的引理, 我们能够看到引理 <span class="inlinecode"><span class="id" type="var">update_same</span></span> 几乎能够完
成它的工作，但是它完成得不彻底：它声称所有的变量在原状态和新状态下的值都
相同，但是从Coq的角度来看，这与声称原状态 <span class="inlinecode">=</span> 新状态并不相同！
<div class="paragraph"> </div>
这里发生了什么? 回顾我们定义的 state ，它只是一个将 id 映射到 值 的函数。在Coq中
函数（化简后）的定义在语法上相同时它们才相同。
(这是能使用归纳命题 <span class="inlinecode"><span class="id" type="var">eq</span></span> 中构造子 <span class="inlinecode"><span class="id" type="var">refl_equal</span></span> 的唯一方法!)
实际上，对于重复使用 <span class="inlinecode"><span class="id" type="var">update</span></span> 构建起来的函数, 只有两个函数使用
<i>相同的</i> <span class="inlinecode"><span class="id" type="var">update</span></span> 构建过程才能证明他们是相同的。
在上面的定理中, 在 <span class="inlinecode"><span class="id" type="var">cequiv</span></span> 中第一个的 update 链比第二个的长，因此它们毫无疑问是不相等
的。
<div class="paragraph"> </div>
<a name="lab469"></a><h3 class="section"> </h3>
这种问题其实挺常见. 比如我们尝试证明比如这样的定理
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">cequiv</span> (<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> + 1;;<br/>
<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> + 1)<br/>
(<span class="id" type="var">X</span> ::= <span class="id" type="var">X</span> + 2)
<div class="paragraph"> </div>
</div>
或者这样的定理
<div class="paragraph"> </div>
<div class="code code-tight">
<span class="id" type="var">cequiv</span> (<span class="id" type="var">X</span> ::= 1;; <span class="id" type="var">Y</span> ::= 2)<br/>
(<span class="id" type="var">y</span> ::= 2;; <span class="id" type="var">X</span> ::= 1)<br/>
<div class="paragraph"> </div>
</div>
我们会以相同的方式卡住: 会有两个对所有输入都有相同行为的函数, 但是我们无法证明它们互相 <span class="inlinecode"><span class="id" type="var">eq</span></span> 。
<div class="paragraph"> </div>
对于这类情况我们使用被人们称为 <i>外延公理</i> ( <i>functional extensionality</i> ）
的推理原则::
<center><table class="infrule">
<tr class="infruleassumption">
<td class="infrule"><span style="font-family: arial;">∀</span>x, f x = g x</td>
<td class="infrulenamecol" rowspan="3">
</td></tr>
<tr class="infrulemiddle">
<td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
<td class="infrule">f = g</td>
<td></td>
</td>
</table></center> 这条原则虽然在Coq内建逻辑中没办法推导, 但是把这条原则当作 <i>公理</i> （ <i>axiom</i> ）
加入到Coq中是安全的。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Axiom</span> <span class="id" type="var">functional_extensionality</span> : <span style="font-family: arial;">∀</span>{<span class="id" type="var">X</span> <span class="id" type="var">Y</span>: <span class="id" type="keyword">Type</span>} {<span class="id" type="var">f</span> <span class="id" type="var">g</span> : <span class="id" type="var">X</span> <span style="font-family: arial;">→</span> <span class="id" type="var">Y</span>},<br/>
(<span style="font-family: arial;">∀</span>(<span class="id" type="var">x</span>: <span class="id" type="var">X</span>), <span class="id" type="var">f</span> <span class="id" type="var">x</span> = <span class="id" type="var">g</span> <span class="id" type="var">x</span>) <span style="font-family: arial;">→</span> <span class="id" type="var">f</span> = <span class="id" type="var">g</span>.<br/>
<br/>
</div>
<div class="doc">
我们可以证明增加这条公理不会破坏Coq的一致性。（从这个角度看, 这与在Coq中添加
古典逻辑中的其中一条诸如排中律公理（<span class="inlinecode"><span class="id" type="var">excluded_middle</span></span>）类似。）
<div class="paragraph"> </div>
多亏了这条公理我们可以证明我们的定理了.
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">identity_assignment</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">X</span>:<span class="id" type="var">id</span>),<br/>
<span class="id" type="var">cequiv</span><br/>
(<span class="id" type="var">X</span> ::= <span class="id" type="var">AId</span> <span class="id" type="var">X</span>)<br/>
<span class="id" type="var">SKIP</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">split</span>; <span class="id" type="tactic">intro</span> <span class="id" type="var">H</span>.<br/>
- <span class="comment">(* -> *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">simpl</span>.<br/>
<span class="id" type="tactic">replace</span> (<span class="id" type="var">update</span> <span class="id" type="var">st</span> <span class="id" type="var">X</span> (<span class="id" type="var">st</span> <span class="id" type="var">X</span>)) <span class="id" type="keyword">with</span> <span class="id" type="var">st</span>.<br/>
<span class="id" type="var">constructor</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">functional_extensionality</span>. <span class="id" type="tactic">intro</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">update_same</span>; <span class="id" type="tactic">reflexivity</span>.<br/>
- <span class="comment">(* <- *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
<span class="id" type="tactic">assert</span> (<span class="id" type="var">st'</span> = (<span class="id" type="var">update</span> <span class="id" type="var">st'</span> <span class="id" type="var">X</span> (<span class="id" type="var">st'</span> <span class="id" type="var">X</span>))).<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">functional_extensionality</span>. <span class="id" type="tactic">intro</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">update_same</span>; <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">H0</span> <span class="id" type="tactic">at</span> 2.<br/>
<span class="id" type="var">constructor</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a name="lab470"></a><h4 class="section">Exercise: 2 stars (assign_aequiv)</h4>
</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">assign_aequiv</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">X</span> <span class="id" type="var">e</span>,<br/>
<span class="id" type="var">aequiv</span> (<span class="id" type="var">AId</span> <span class="id" type="var">X</span>) <span class="id" type="var">e</span> <span style="font-family: arial;">→</span> <br/>
<span class="id" type="var">cequiv</span> <span class="id" type="var">SKIP</span> (<span class="id" type="var">X</span> ::= <span class="id" type="var">e</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(* FILL IN HERE *)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>
<div class="doc">
<font size=-2>☐</font>
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab471"></a><h1 class="section">行为等价的性质</h1>
<div class="paragraph"> </div>
现在我们开始开发之前定义的程序等价中的一些性质.
</div>
<div class="code code-tight">
<br/>
</div>
<div class="doc">
<a name="lab472"></a><h2 class="section">行为等价是一种等价性</h2>
<div class="paragraph"> </div>
首先, 我们验证 <span class="inlinecode"><span class="id" type="var">aexps</span></span>, <span class="inlinecode"><span class="id" type="var">bexps</span></span>, 和 <span class="inlinecode"><span class="id" type="var">com</span></span> 的确满足 <i>等价性</i> （ <i>equivalences</i> ）
也就是说, 它们都满足 自反性（reflexive），对称性（symmetric）和 传递性（transitive）。
这些证明全都不难。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">refl_aequiv</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>), <span class="id" type="var">aequiv</span> <span class="id" type="var">a</span> <span class="id" type="var">a</span>.<br/>
<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">a</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">sym_aequiv</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">a1</span> <span class="id" type="var">a2</span> : <span class="id" type="var">aexp</span>), <br/>
<span class="id" type="var">aequiv</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> <span style="font-family: arial;">→</span> <span class="id" type="var">aequiv</span> <span class="id" type="var">a2</span> <span class="id" type="var">a1</span>.<br/>
<div class="togglescript" id="proofcontrol7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')"><span class="show"></span></div>
<div class="proofscript" id="proof7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">trans_aequiv</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">a1</span> <span class="id" type="var">a2</span> <span class="id" type="var">a3</span> : <span class="id" type="var">aexp</span>), <br/>
<span class="id" type="var">aequiv</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> <span style="font-family: arial;">→</span> <span class="id" type="var">aequiv</span> <span class="id" type="var">a2</span> <span class="id" type="var">a3</span> <span style="font-family: arial;">→</span> <span class="id" type="var">aequiv</span> <span class="id" type="var">a1</span> <span class="id" type="var">a3</span>.<br/>
<div class="togglescript" id="proofcontrol8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')"><span class="show"></span></div>
<div class="proofscript" id="proof8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">aequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> <span class="id" type="var">a3</span> <span class="id" type="var">H12</span> <span class="id" type="var">H23</span> <span class="id" type="var">st</span>.<br/>
<span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H12</span> <span class="id" type="var">st</span>). <span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H23</span> <span class="id" type="var">st</span>). <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">refl_bequiv</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>), <span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">b</span>.<br/>
<div class="togglescript" id="proofcontrol9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')"><span class="show"></span></div>
<div class="proofscript" id="proof9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">sym_bequiv</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">b1</span> <span class="id" type="var">b2</span> : <span class="id" type="var">bexp</span>), <br/>
<span class="id" type="var">bequiv</span> <span class="id" type="var">b1</span> <span class="id" type="var">b2</span> <span style="font-family: arial;">→</span> <span class="id" type="var">bequiv</span> <span class="id" type="var">b2</span> <span class="id" type="var">b1</span>.<br/>
<div class="togglescript" id="proofcontrol10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')"><span class="show"></span></div>
<div class="proofscript" id="proof10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">b1</span> <span class="id" type="var">b2</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">trans_bequiv</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">b1</span> <span class="id" type="var">b2</span> <span class="id" type="var">b3</span> : <span class="id" type="var">bexp</span>), <br/>
<span class="id" type="var">bequiv</span> <span class="id" type="var">b1</span> <span class="id" type="var">b2</span> <span style="font-family: arial;">→</span> <span class="id" type="var">bequiv</span> <span class="id" type="var">b2</span> <span class="id" type="var">b3</span> <span style="font-family: arial;">→</span> <span class="id" type="var">bequiv</span> <span class="id" type="var">b1</span> <span class="id" type="var">b3</span>.<br/>
<div class="togglescript" id="proofcontrol11" onclick="toggleDisplay('proof11');toggleDisplay('proofcontrol11')"><span class="show"></span></div>
<div class="proofscript" id="proof11" onclick="toggleDisplay('proof11');toggleDisplay('proofcontrol11')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">b1</span> <span class="id" type="var">b2</span> <span class="id" type="var">b3</span> <span class="id" type="var">H12</span> <span class="id" type="var">H23</span> <span class="id" type="var">st</span>.<br/>
<span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H12</span> <span class="id" type="var">st</span>). <span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H23</span> <span class="id" type="var">st</span>). <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">refl_cequiv</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">c</span> : <span class="id" type="var">com</span>), <span class="id" type="var">cequiv</span> <span class="id" type="var">c</span> <span class="id" type="var">c</span>.<br/>
<div class="togglescript" id="proofcontrol12" onclick="toggleDisplay('proof12');toggleDisplay('proofcontrol12')"><span class="show"></span></div>
<div class="proofscript" id="proof12" onclick="toggleDisplay('proof12');toggleDisplay('proofcontrol12')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">cequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">iff_refl</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">sym_cequiv</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">c1</span> <span class="id" type="var">c2</span> : <span class="id" type="var">com</span>), <br/>
<span class="id" type="var">cequiv</span> <span class="id" type="var">c1</span> <span class="id" type="var">c2</span> <span style="font-family: arial;">→</span> <span class="id" type="var">cequiv</span> <span class="id" type="var">c2</span> <span class="id" type="var">c1</span>.<br/>
<div class="togglescript" id="proofcontrol13" onclick="toggleDisplay('proof13');toggleDisplay('proofcontrol13')"><span class="show"></span></div>
<div class="proofscript" id="proof13" onclick="toggleDisplay('proof13');toggleDisplay('proofcontrol13')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">cequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">c1</span> <span class="id" type="var">c2</span> <span class="id" type="var">H</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
<span class="id" type="tactic">assert</span> (<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">st'</span> <span style="font-family: arial;">↔</span> <span class="id" type="var">c2</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st'</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">H'</span>.<br/>
{ <span class="comment">(* 断言的证明 *)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. }<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">iff_sym</span>. <span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">iff_trans</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">P1</span> <span class="id" type="var">P2</span> <span class="id" type="var">P3</span> : <span class="id" type="keyword">Prop</span>), <br/>
(<span class="id" type="var">P1</span> <span style="font-family: arial;">↔</span> <span class="id" type="var">P2</span>) <span style="font-family: arial;">→</span> (<span class="id" type="var">P2</span> <span style="font-family: arial;">↔</span> <span class="id" type="var">P3</span>) <span style="font-family: arial;">→</span> (<span class="id" type="var">P1</span> <span style="font-family: arial;">↔</span> <span class="id" type="var">P3</span>).<br/>
<div class="togglescript" id="proofcontrol14" onclick="toggleDisplay('proof14');toggleDisplay('proofcontrol14')"><span class="show"></span></div>
<div class="proofscript" id="proof14" onclick="toggleDisplay('proof14');toggleDisplay('proofcontrol14')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">P1</span> <span class="id" type="var">P2</span> <span class="id" type="var">P3</span> <span class="id" type="var">H12</span> <span class="id" type="var">H23</span>.<br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">H12</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H23</span>.<br/>
<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">A</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">H1</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">A</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">H0</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H2</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">A</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">trans_cequiv</span> : <span style="font-family: arial;">∀</span>(<span class="id" type="var">c1</span> <span class="id" type="var">c2</span> <span class="id" type="var">c3</span> : <span class="id" type="var">com</span>), <br/>
<span class="id" type="var">cequiv</span> <span class="id" type="var">c1</span> <span class="id" type="var">c2</span> <span style="font-family: arial;">→</span> <span class="id" type="var">cequiv</span> <span class="id" type="var">c2</span> <span class="id" type="var">c3</span> <span style="font-family: arial;">→</span> <span class="id" type="var">cequiv</span> <span class="id" type="var">c1</span> <span class="id" type="var">c3</span>.<br/>
<div class="togglescript" id="proofcontrol15" onclick="toggleDisplay('proof15');toggleDisplay('proofcontrol15')"><span class="show"></span></div>
<div class="proofscript" id="proof15" onclick="toggleDisplay('proof15');toggleDisplay('proofcontrol15')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">unfold</span> <span class="id" type="var">cequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">c1</span> <span class="id" type="var">c2</span> <span class="id" type="var">c3</span> <span class="id" type="var">H12</span> <span class="id" type="var">H23</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
<span class="id" type="tactic">apply</span> <span class="id" type="var">iff_trans</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">c2</span> / <span class="id" type="var">st</span> <span style="font-family: arial;">⇓</span> <span class="id" type="var">st'</span>). <span class="id" type="tactic">apply</span> <span class="id" type="var">H12</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H23</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
</div>
<div class="doc">
<a name="lab473"></a><h2 class="section">行为等价是一种一致性</h2>
<div class="paragraph"> </div>
不太明显地, 行为等价也满足 <i>一致性</i> （ <i>congruence</i> ). 也就是说
两个子程序等价那么只有子程序有差异的两个大程序也等价:
<center><table class="infrule">
<tr class="infruleassumption">
<td class="infrule">aequiv a1 a1'</td>
<td class="infrulenamecol" rowspan="3">
</td></tr>
<tr class="infrulemiddle">
<td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
<td class="infrule">cequiv (i ::= a1) (i ::= a1')</td>
<td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
<td class="infrule">cequiv c1 c1'</td>
<td></td>
</td>
<tr class="infruleassumption">
<td class="infrule">cequiv c2 c2'</td>
<td class="infrulenamecol" rowspan="3">
</td></tr>
<tr class="infrulemiddle">
<td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
<td class="infrule">cequiv (c1;;c2) (c1';;c2')</td>
<td></td>
</td>
</table></center> ...等等.
<div class="paragraph"> </div>
(注意我们这里用的推理规则记号并不是定义的一部分, 只是将一些合法的蕴含式用易读的方式写下而已.
接下来我们将证明这些蕴含式.)
<div class="paragraph"> </div>
我们会在接下来的章节（在 <span class="inlinecode"><span class="id" type="var">fold_constants_com_sound</span></span> 的证明中）看到
一些例子能够说明为何这些一致性十分重要。但是它的主要意义在于这些一致性允许我们在用一小部
分程序替换一个大程序中等价的一部分并证明替换前和替换后程序的等价
性时 <i>无需</i> 进行与不变的部分相关的证明；也即是说，程序的改变所产生
的证明的工作量与改变的大小而不是与整个程序的大小成比例。
</div>
<div class="code code-tight">
<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">CAss_congruence</span> : <span style="font-family: arial;">∀</span><span class="id" type="var">i</span> <span class="id" type="var">a1</span> <span class="id" type="var">a1'</span>,<br/>
<span class="id" type="var">aequiv</span> <span class="id" type="var">a1</span> <span class="id" type="var">a1'</span> <span style="font-family: arial;">→</span><br/>
<span class="id" type="var">cequiv</span> (<span class="id" type="var">CAss</span> <span class="id" type="var">i</span> <span class="id" type="var">a1</span>) (<span class="id" type="var">CAss</span> <span class="id" type="var">i</span> <span class="id" type="var">a1'</span>).<br/>
<div class="togglescript" id="proofcontrol16" onclick="toggleDisplay('proof16');toggleDisplay('proofcontrol16')"><span class="show"></span></div>
<div class="proofscript" id="proof16" onclick="toggleDisplay('proof16');toggleDisplay('proofcontrol16')">
<span class="id" type="keyword">Proof</span>.<br/>
<span class="id" type="tactic">intros</span> <span class="id" type="var">i</span> <span class="id" type="var">a1</span> <span class="id" type="var">a2</span> <span class="id" type="var">Heqv</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">Hceval</span>.<br/>
- <span class="comment">(* -> *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hceval</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_Ass</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Heqv</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
- <span class="comment">(* <- *)</span><br/>
<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hceval</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_Ass</span>.<br/>
<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Heqv</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<br/>
</div>
<div class="doc">
循环的一致性更有趣, 因为他需要使用归纳法（induction）.