-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathEquiv.v
1611 lines (1343 loc) · 56.4 KB
/
Equiv.v
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
(** * Equiv: Program Equivalence *)
(** * Equiv: 程序等价性 *)
Require Export Imp.
(** *** 一些关于练习的一般性建议:
- 这里要进行的大多数Coq证明都与先前我们所提供的相似. 在做作业之前, 花一些时间
（非形式化的在纸上和Coq中）思考我们的证明确保你理解他们的的每一个细节. 这会节省你
大量的时间.
- 我们现在进行的Coq证明已经足够复杂，以至于近乎不可能单靠“灵感”或者以随机的尝试误打误撞的完成证明。你需要一个关于为何
某个属性为真以及如何进行证明的概念并从这个概念开始。完成这一项任务的最好的方
法是在开始进行形式化证明之前至少在纸上写出一个非形式化证明的梗概
--直观的说服自己相信定理成立--然后再进行形式化证明。另外，
你也可以拉来一个好友，尝试说服他相信这条定理成立; 然后试着形式化你刚才的解释。
- 使用自动化工具来减少工作量！本章的一些证明练习，如果全部一个个分类去分析的话
会非常长. *)
(* ####################################################### *)
(** * 行为的等价性 *)
(** 在上一章中我们讨论了一个非常简单的程序变换的正确性; [optimize_0plus] 函数。
这是我们考虑的算数表达式语言的第一个版本--它没有变量--所以很容易定义 _（什么是）_
正确的程序变换： 即输出一个求值结果与原程序相同的程序。
为了更进一步的讨论整个Imp语言变换的正确性，我们需要考虑状态和变量的作用。 *)
(* ####################################################### *)
(** ** 定义 *)
(** 对于包含变量的 [aexp] 和 [bexp], 我们需要的定义简单明了。在 _（所有状态）_
下两个 [aexp] 或者 [bexp] 的求值结果相同，我们就说他们 _（行为等价）_ 。*)
Definition aequiv (a1 a2 : aexp) : Prop :=
forall (st:state),
aeval st a1 = aeval st a2.
Definition bequiv (b1 b2 : bexp) : Prop :=
forall (st:state),
beval st b1 = beval st b2.
(** 对于命令，情况有些微妙。我们不能简单的说：“如果两个指令在相同的初始状态下求值到相同
的终止状态，那么说这两个指令等价。”，因为有些命令（在某些初始状态下）根本不会在任何
状态终止！我们实际上需要的是：“若两个指令在给出任何初始状态时都发散或者终止在相同
的状态上，则这两个指令行为等价。”。简单的说就是：“如果其中一个终止在某
状态上那么另一个也终止在这个状态上，反之亦然。” *)
Definition cequiv (c1 c2 : com) : Prop :=
forall (st st' : state),
(c1 / st || st') <-> (c2 / st || st').
(** **** Exercise: 2 stars (equiv_classes) *)
(** 下面将给出一些程序，请按在[Imp]中是否等价将这些程序分组。你的答案应该是一个列表的列表
其中每个子列表代表一组互相等价的程序。例如，你认为除了程序i之外剩下的都是等价的，那么你的答案
应该像这个样子：
[ [prog_a;prog_b;prog_c;prog_d;prog_e;prog_f;prog_g;prog_h] ;
[prog_i] ]
在 [equiv_classes] 的定义下面写出你的答案。 *)
Definition prog_a : com :=
WHILE BNot (BLe (AId X) (ANum 0)) DO
X ::= APlus (AId X) (ANum 1)
END.
Definition prog_b : com :=
IFB BEq (AId X) (ANum 0) THEN
X ::= APlus (AId X) (ANum 1);;
Y ::= ANum 1
ELSE
Y ::= ANum 0
FI;;
X ::= AMinus (AId X) (AId Y);;
Y ::= ANum 0.
Definition prog_c : com :=
SKIP.
Definition prog_d : com :=
WHILE BNot (BEq (AId X) (ANum 0)) DO
X ::= APlus (AMult (AId X) (AId Y)) (ANum 1)
END.
Definition prog_e : com :=
Y ::= ANum 0.
Definition prog_f : com :=
Y ::= APlus (AId X) (ANum 1);;
WHILE BNot (BEq (AId X) (AId Y)) DO
Y ::= APlus (AId X) (ANum 1)
END.
Definition prog_g : com :=
WHILE BTrue DO
SKIP
END.
Definition prog_h : com :=
WHILE BNot (BEq (AId X) (AId X)) DO
X ::= APlus (AId X) (ANum 1)
END.
Definition prog_i : com :=
WHILE BNot (BEq (AId X) (AId Y)) DO
X ::= APlus (AId Y) (ANum 1)
END.
Definition equiv_classes : list (list com) :=
(* FILL IN HERE *) admit.
(* GRADE_TEST 2: check_equiv_classes equiv_classes *)
(** [] *)
(* ####################################################### *)
(** ** 例子 *)
(** 这里有些关于算数表达式和布尔表达式等价的例子. *)
Theorem aequiv_example:
aequiv (AMinus (AId X) (AId X)) (ANum 0).
Proof.
intros st. simpl. omega.
Qed.
Theorem bequiv_example:
bequiv (BEq (AMinus (AId X) (AId X)) (ANum 0)) BTrue.
Proof.
intros st. unfold beval.
rewrite aequiv_example. reflexivity.
Qed.
(** 这里是一些命令等价的例子，让我们从包含[SKIP]的简单的程序变换开始: *)
Theorem skip_left: forall c,
cequiv
(SKIP;; c)
c.
Proof.
(* WORKED IN CLASS *)
intros c st st'.
split; intros H.
- (* -> *)
inversion H. subst.
inversion H2. subst.
assumption.
- (* <- *)
apply E_Seq with st.
apply E_Skip.
assumption.
Qed.
(** **** Exercise: 2 stars (skip_right) *)
(** 试证在任一命令后加上SKIP所变换出的新程序与原程序等价。 *)
Theorem skip_right: forall c,
cequiv
(c;; SKIP)
c.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** 类似的，这里是一些简化 [IFB] 的简单变换: *)
Theorem IFB_true_simple: forall c1 c2,
cequiv
(IFB BTrue THEN c1 ELSE c2 FI)
c1.
Proof.
intros c1 c2.
split; intros H.
- (* -> *)
inversion H; subst. assumption. inversion H5.
- (* <- *)
apply E_IfTrue. reflexivity. assumption. Qed.
(** 当然，一些程序员会尝试以IF的判断条件字面上是否等于 [BTrue] 作为优化前提。但一个
更有趣的方式是看IF的判断条件是否等价于真:
_Theorem_: 如果 [b] 等价于 [BTrue], 那么 [IFB b THEN c1
ELSE c2 FI] 等价于 [c1].
*)
(** *** *)
(**
_Proof_:
- ([->]) 我们必须证明, 对于所有 [st] 和 [st'], 如果 [IFB b
THEN c1 ELSE c2 FI / st || st'] 则 [c1 / st || st'].
能够应用于 [IFB b THEN c1 ELSE c2 FI / st || st'] 的证明规则只有两条：
[E_IfTrue] 和 [E_IfFalse].
- 假设 [IFB b THEN c1 ELSE c2 FI / st || st'] 证明自 [E_IfTrue]
这条证明规则. 若使用证明规则 [E_IfTrue] 其必备的前提条件 [c1 / st || st'] 必为真， 而这正好是
我们的证明所需要的条件。
- 另一方面, 假设 [IFB b THEN c1 ELSE c2 FI / st || st'] 证明自
[E_IfFalse]. 我们能得知 [beval st b = false] 和 [c2 / st || st'].
之前提到 [b] 等价于 [BTrue], 也就是说对于所有 [st], 有[beval st b = beval st BTrue].
具体的说就是 [beval st b = true] 成立, 导致 [beval st BTrue = true] 成立。
但是与此同时，之前假设 [E_IfFalse] 必备的前提条件 [beval st b = false] 也成立，
这就构成了一组矛盾。从而说明不可能使用了 [E_IfFalse] 这条证明规则。
- ([<-]) 我们必须证明，对于所有 [st] 和 [st'], 如果 [c1 / st || st']
则 [IFB b THEN c1 ELSE c2 FI / st || st'].
已知 [b] 等价于 [BTrue], 我们知道 [beval st b] = [beval st BTrue] = [true].
结合 [c1 / st || st'] 这条假设, 我们能应用 [E_IfTrue] 来证明出 [IFB b THEN
c1 ELSE c2 FI / st || st']. []
下面是这个证明的形式化版本: *)
Theorem IFB_true: forall b c1 c2,
bequiv b BTrue ->
cequiv
(IFB b THEN c1 ELSE c2 FI)
c1.
Proof.
intros b c1 c2 Hb.
split; intros H.
- (* -> *)
inversion H; subst.
+ (* b 求值得出 true *)
assumption.
+ (* b 求值得出 false (矛盾) *)
unfold bequiv in Hb. simpl in Hb.
rewrite Hb in H5.
inversion H5.
- (* <- *)
apply E_IfTrue; try assumption.
unfold bequiv in Hb. simpl in Hb.
rewrite Hb. reflexivity. Qed.
(** **** Exercise: 2 stars (IFB_false) *)
Theorem IFB_false: forall b c1 c2,
bequiv b BFalse ->
cequiv
(IFB b THEN c1 ELSE c2 FI)
c2.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 3 stars (swap_if_branches) *)
(** 证明我们可以通过对条件取反来交换 IF 的两个分支 *)
Theorem swap_if_branches: forall b e1 e2,
cequiv
(IFB b THEN e1 ELSE e2 FI)
(IFB BNot b THEN e2 ELSE e1 FI).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** *** *)
(** 对于 [WHILE] 循环我们能够给出一组相似的定理：当一个循环的条件等价于 [BFalse] 的
时候它等价于 [SKIP], 当一个循环的条件等价于 [BTrue] 的时候它等价于
[WHILE BTrue DO SKIP END] （或者任意不终止的程序）。
前者比较简单. *)
Theorem WHILE_false : forall b c,
bequiv b BFalse ->
cequiv
(WHILE b DO c END)
SKIP.
Proof.
intros b c Hb. split; intros H.
- (* -> *)
inversion H; subst.
+ (* E_WhileEnd *)
apply E_Skip.
+ (* E_WhileLoop *)
rewrite Hb in H2. inversion H2.
- (* <- *)
inversion H; subst.
apply E_WhileEnd.
rewrite Hb.
reflexivity. Qed.
(** **** Exercise: 2 stars, advanced, optional (WHILE_false_informal) *)
(** 写出 [WHILE_false] 的非形式化证明.
(* FILL IN HERE *)
[]
*)
(** *** *)
(** 为了证明第2个定理, 我们需要一个辅助定理: [WHILE] 循环在条件等价于
[BTrue] 的时候循环不会终止:
_Lemma_: 如果 [b] 等价于 [BTrue], 则不可能像
[(WHILE b DO c END) / st || st'] 这样会终止。
_Proof_: 假设循环会终止，即 [(WHILE b DO c END) / st || st']. 我们将证明在通过
对 [(WHILE b DO c END) / st || st'] 使用归纳法可以引出矛盾。
- 假设 [(WHILE b DO c END) / st || st'] 使用了 [E_WhileEnd] 这条证明规则。
那么根据假设得出 [beval st b = false] 。但是这和 [b] 等价于 [BTrue] 矛盾。
- 假设 [(WHILE b DO c END) / st || st'] 使用了 [E_WhileLoop] 这条证明规则.
结果就是给出了一个和 [(WHILE b DO c END) / st || st'] 矛盾的假设, 正巧是
我们正要证明的那个!
- 由于只有以上的几条规则可以证明出 [(WHILE b DO c END) / st || st'] 所以归纳时
的其他的情况会立即导致矛盾。 [] *)
Lemma WHILE_true_nonterm : forall b c st st',
bequiv b BTrue ->
~( (WHILE b DO c END) / st || st' ).
Proof.
(* WORKED IN CLASS *)
intros b c st st' Hb.
intros H.
remember (WHILE b DO c END) as cw eqn:Heqcw.
induction H;
(* 大多数证明规则不可能应用，我们可以用 反演（inversion）来去除他们 *)
inversion Heqcw; subst; clear Heqcw.
(* 我们只关心这两个关于 WHILE 循环的证明规则: *)
- (* E_WhileEnd *) (* 矛盾 -- b 总是 true! *)
unfold bequiv in Hb.
(* [rewrite] 能实例化Hb中的变量 [st] *)
rewrite Hb in H. inversion H.
- (* E_WhileLoop *) (* 直接使用IH *)
apply IHceval2. reflexivity. Qed.
(** **** Exercise: 2 stars, optional (WHILE_true_nonterm_informal) *)
(** 试解释 [WHILE_true_nonterm] 的意义。
(* FILL IN HERE *)
*)
(** [] *)
(** **** Exercise: 2 stars (WHILE_true) *)
(** 证明下面的定理. _（提示）_ : 你可能需要使用 [WHILE_true_nonterm]. *)
Theorem WHILE_true: forall b c,
bequiv b BTrue ->
cequiv
(WHILE b DO c END)
(WHILE BTrue DO SKIP END).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
Theorem loop_unrolling: forall b c,
cequiv
(WHILE b DO c END)
(IFB b THEN (c;; WHILE b DO c END) ELSE SKIP FI).
Proof.
(* WORKED IN CLASS *)
intros b c st st'.
split; intros Hce.
- (* -> *)
inversion Hce; subst.
+ (* 不执行循环 *)
apply E_IfFalse. assumption. apply E_Skip.
+ (* 执行循环 *)
apply E_IfTrue. assumption.
apply E_Seq with (st' := st'0). assumption. assumption.
- (* <- *)
inversion Hce; subst.
+ (* 执行循环 *)
inversion H5; subst.
apply E_WhileLoop with (st' := st'0).
assumption. assumption. assumption.
+ (* 不执行循环 *)
inversion H5; subst. apply E_WhileEnd. assumption. Qed.
(** **** Exercise: 2 stars, optional (seq_assoc) *)
Theorem seq_assoc : forall c1 c2 c3,
cequiv ((c1;;c2);;c3) (c1;;(c2;;c3)).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** ** 外延公理 *)
(** 最后, 我们来看看含有赋值的简单等价.
比如, 我们也许会希望能够证明 [X ::= AId X] 和 [SKIP] 等价。但是，
我们当试着证明它的时候, 我们会以一种很奇妙的方式卡住。*)
Theorem identity_assignment_first_try : forall (X:id),
cequiv (X ::= AId X) SKIP.
Proof.
intros. split; intro H.
- (* -> *)
inversion H; subst. simpl.
replace (update st X (st X)) with st.
constructor.
(* 卡住了... *) Abort.
(** 现在我们卡住了. 虽然结论看起来很合理，但是实际上它是无法证明的! 如果我们回顾在上一章
我们曾证明的有关 [update] 的引理, 我们能够看到引理 [update_same] 几乎能够完
成它的工作，但是它完成得不彻底：它声称所有的变量在原状态和新状态下的值都
相同，但是从Coq的角度来看，这与声称原状态 [=] 新状态并不相同！ *)
(** 这里发生了什么? 回顾我们定义的 state ，它只是一个将 id 映射到 值 的函数。在Coq中
函数（化简后）的定义在语法上相同时它们才相同。
(这是能使用归纳命题 [eq] 中构造子 [refl_equal] 的唯一方法!)
实际上，对于重复使用 [update] 构建起来的函数, 只有两个函数使用
_（相同的）_ [update] 构建过程才能证明他们是相同的。
在上面的定理中, 在 [cequiv] 中第一个的 update 链比第二个的长，因此它们毫无疑问是不相等
的。 *)
(** *** *)
(** 这种问题其实挺常见. 比如我们尝试证明比如这样的定理
cequiv (X ::= X + 1;;
X ::= X + 1)
(X ::= X + 2)
或者这样的定理
cequiv (X ::= 1;; Y ::= 2)
(y ::= 2;; X ::= 1)
我们会以相同的方式卡住: 会有两个对所有输入都有相同行为的函数, 但是我们无法证明它们互相 [eq] 。
对于这类情况我们使用被人们称为 _（外延公理）_ ( _functional extensionality_ ）
的推理原则::
forall x, f x = g x
-------------------
f = g
这条原则虽然在Coq内建逻辑中没办法推导, 但是把这条原则当作 _（公理）_ （ _axiom_ ）
加入到Coq中是安全的。 *)
Axiom functional_extensionality : forall {X Y: Type} {f g : X -> Y},
(forall (x: X), f x = g x) -> f = g.
(** 我们可以证明增加这条公理不会破坏Coq的一致性。（从这个角度看, 这与在Coq中添加
古典逻辑中的其中一条诸如排中律公理（[excluded_middle]）类似。） *)
(** 多亏了这条公理我们可以证明我们的定理了. *)
Theorem identity_assignment : forall (X:id),
cequiv
(X ::= AId X)
SKIP.
Proof.
intros. split; intro H.
- (* -> *)
inversion H; subst. simpl.
replace (update st X (st X)) with st.
constructor.
apply functional_extensionality. intro.
rewrite update_same; reflexivity.
- (* <- *)
inversion H; subst.
assert (st' = (update st' X (st' X))).
apply functional_extensionality. intro.
rewrite update_same; reflexivity.
rewrite H0 at 2.
constructor. reflexivity.
Qed.
(** **** Exercise: 2 stars (assign_aequiv) *)
Theorem assign_aequiv : forall X e,
aequiv (AId X) e ->
cequiv SKIP (X ::= e).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(* ####################################################### *)
(** * 行为等价的性质 *)
(** 现在我们开始开发之前定义的程序等价中的一些性质. *)
(* ####################################################### *)
(** ** 行为等价是一种等价性 *)
(** 首先, 我们验证 [aexps], [bexps], 和 [com] 的确满足 _（等价性）_ （ _equivalences_ ）
-- 也就是说, 它们都满足 自反性（reflexive），对称性（symmetric）和 传递性（transitive）。
这些证明全都不难。 *)
Lemma refl_aequiv : forall (a : aexp), aequiv a a.
Proof.
intros a st. reflexivity. Qed.
Lemma sym_aequiv : forall (a1 a2 : aexp),
aequiv a1 a2 -> aequiv a2 a1.
Proof.
intros a1 a2 H. intros st. symmetry. apply H. Qed.
Lemma trans_aequiv : forall (a1 a2 a3 : aexp),
aequiv a1 a2 -> aequiv a2 a3 -> aequiv a1 a3.
Proof.
unfold aequiv. intros a1 a2 a3 H12 H23 st.
rewrite (H12 st). rewrite (H23 st). reflexivity. Qed.
Lemma refl_bequiv : forall (b : bexp), bequiv b b.
Proof.
unfold bequiv. intros b st. reflexivity. Qed.
Lemma sym_bequiv : forall (b1 b2 : bexp),
bequiv b1 b2 -> bequiv b2 b1.
Proof.
unfold bequiv. intros b1 b2 H. intros st. symmetry. apply H. Qed.
Lemma trans_bequiv : forall (b1 b2 b3 : bexp),
bequiv b1 b2 -> bequiv b2 b3 -> bequiv b1 b3.
Proof.
unfold bequiv. intros b1 b2 b3 H12 H23 st.
rewrite (H12 st). rewrite (H23 st). reflexivity. Qed.
Lemma refl_cequiv : forall (c : com), cequiv c c.
Proof.
unfold cequiv. intros c st st'. apply iff_refl. Qed.
Lemma sym_cequiv : forall (c1 c2 : com),
cequiv c1 c2 -> cequiv c2 c1.
Proof.
unfold cequiv. intros c1 c2 H st st'.
assert (c1 / st || st' <-> c2 / st || st') as H'.
{ (* 断言的证明 *) apply H. }
apply iff_sym. assumption.
Qed.
Lemma iff_trans : forall (P1 P2 P3 : Prop),
(P1 <-> P2) -> (P2 <-> P3) -> (P1 <-> P3).
Proof.
intros P1 P2 P3 H12 H23.
inversion H12. inversion H23.
split; intros A.
apply H1. apply H. apply A.
apply H0. apply H2. apply A. Qed.
Lemma trans_cequiv : forall (c1 c2 c3 : com),
cequiv c1 c2 -> cequiv c2 c3 -> cequiv c1 c3.
Proof.
unfold cequiv. intros c1 c2 c3 H12 H23 st st'.
apply iff_trans with (c2 / st || st'). apply H12. apply H23. Qed.
(* ######################################################## *)
(** ** 行为等价是一种一致性 *)
(** 不太明显地, 行为等价也满足 _（一致性）_ （ _congruence_ ). 也就是说
两个子程序等价那么只有子程序有差异的两个大程序也等价:
aequiv a1 a1'
-----------------------------
cequiv (i ::= a1) (i ::= a1')
cequiv c1 c1'
cequiv c2 c2'
------------------------
cequiv (c1;;c2) (c1';;c2')
...等等.
(注意我们这里用的推理规则记号并不是定义的一部分, 只是将一些合法的蕴含式用易读的方式写下而已.
接下来我们将证明这些蕴含式.) *)
(** 我们会在接下来的章节（在 [fold_constants_com_sound] 的证明中）看到
一些例子能够说明为何这些一致性十分重要。但是它的主要意义在于这些一致性允许我们在用一小部
分程序替换一个大程序中等价的一部分并证明替换前和替换后程序的等价
性时 _（无需）_ 进行与不变的部分相关的证明；也即是说，程序的改变所产生
的证明的工作量与改变的大小而不是与整个程序的大小成比例。 *)
Theorem CAss_congruence : forall i a1 a1',
aequiv a1 a1' ->
cequiv (CAss i a1) (CAss i a1').
Proof.
intros i a1 a2 Heqv st st'.
split; intros Hceval.
- (* -> *)
inversion Hceval. subst. apply E_Ass.
rewrite Heqv. reflexivity.
- (* <- *)
inversion Hceval. subst. apply E_Ass.
rewrite Heqv. reflexivity. Qed.
(** 循环的一致性更有趣, 因为他需要使用归纳法（induction）.
_Theorem_: 对于 [WHILE] ，等价性是一种一致性 -- 也就是说, 如果 [b1] 等价于 [b1']
同时 [c1] 等价于 [c1'] ，那么 [WHILE b1 DO c1 END] 等价于
[WHILE b1' DO c1' END] 。
_Proof_: 假设 [b1] 等价于 [b1'] 同时 [c1] 等价于 [c1'] 。
我们要证明，对于所有 [st] 和 [st'] ， [WHILE b1 DO c1 END / st || st']
当且仅当 [WHILE b1' DO c1' END / st || st'] 。我们把两个方向分开考虑。
- ([->]) 我们证明 [WHILE b1 DO c1 END / st || st'] 蕴涵
[WHILE b1' DO c1' END / st || st'] ，对 [WHILE b1 DO c1 END / st || st']
使用归纳法。只有推导最后所使用的规则是 [E_WhileEnd] 和 [E_WhileLoop] 情况才需要
特别进行讨论。
- [E_WhileEnd]: 在这种情况时, 我们拥有假设的必备条件 [beval st b1 = false]
和 [st = st'] 。但是，因为 [b1] 和 [b1'] 是等价的，
我们有 [beval st b1' = false], 然后应用 [E-WhileEnd] ，
得出我们需要的 [WHILE b1' DO c1' END / st || st'] 。
- [E_WhileLoop]: 在这种情况时, 我们拥有假设的必备条件 [beval st b1 = true] ，
[c1 / st || st'0] 和 以及对某个状态 [st'0] 而言，有假设 [WHILE b1 DO c1 END / st'0 || st']
，另外还有归纳假设 [WHILE b1' DO c1' END / st'0 || st'] 。
因为 [c1] 和 [c1'] 等价，推导出 [c1' / st || st'0] 。
然后因为 [b1] 和 [b1'] 等价，推导出 [beval st b1' = true] ，
最后应用 [E-WhileLoop] ，得出我们
需要的 [WHILE b1' DO c1' END / st || st'] 。
- ([<-]) 反之亦然. [] *)
Theorem CWhile_congruence : forall b1 b1' c1 c1',
bequiv b1 b1' -> cequiv c1 c1' ->
cequiv (WHILE b1 DO c1 END) (WHILE b1' DO c1' END).
Proof.
(* WORKED IN CLASS *)
unfold bequiv,cequiv.
intros b1 b1' c1 c1' Hb1e Hc1e st st'.
split; intros Hce.
- (* -> *)
remember (WHILE b1 DO c1 END) as cwhile eqn:Heqcwhile.
induction Hce; inversion Heqcwhile; subst.
+ (* E_WhileEnd *)
apply E_WhileEnd. rewrite <- Hb1e. apply H.
+ (* E_WhileLoop *)
apply E_WhileLoop with (st' := st').
* (* show loop runs *) rewrite <- Hb1e. apply H.
* (* body execution *)
apply (Hc1e st st'). apply Hce1.
* (* subsequent loop execution *)
apply IHHce2. reflexivity.
- (* <- *)
remember (WHILE b1' DO c1' END) as c'while eqn:Heqc'while.
induction Hce; inversion Heqc'while; subst.
+ (* E_WhileEnd *)
apply E_WhileEnd. rewrite -> Hb1e. apply H.
+ (* E_WhileLoop *)
apply E_WhileLoop with (st' := st').
* (* show loop runs *) rewrite -> Hb1e. apply H.
* (* body execution *)
apply (Hc1e st st'). apply Hce1.
* (* subsequent loop execution *)
apply IHHce2. reflexivity. Qed.
(** **** Exercise: 3 stars, optional (CSeq_congruence) *)
Theorem CSeq_congruence : forall c1 c1' c2 c2',
cequiv c1 c1' -> cequiv c2 c2' ->
cequiv (c1;;c2) (c1';;c2').
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** **** Exercise: 3 stars (CIf_congruence) *)
Theorem CIf_congruence : forall b b' c1 c1' c2 c2',
bequiv b b' -> cequiv c1 c1' -> cequiv c2 c2' ->
cequiv (IFB b THEN c1 ELSE c2 FI) (IFB b' THEN c1' ELSE c2' FI).
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)
(** *** *)
(** 比如, 这里有两个等价的程序, 和他们的等价性证明... *)
Example congruence_example:
cequiv
(* Program 1: *)
(X ::= ANum 0;;
IFB (BEq (AId X) (ANum 0))
THEN
Y ::= ANum 0
ELSE
Y ::= ANum 42
FI)
(* Program 2: *)
(X ::= ANum 0;;
IFB (BEq (AId X) (ANum 0))
THEN
Y ::= AMinus (AId X) (AId X) (* <--- 这里有改动 *)
ELSE
Y ::= ANum 42
FI).
Proof.
apply CSeq_congruence.
apply refl_cequiv.
apply CIf_congruence.
apply refl_bequiv.
apply CAss_congruence. unfold aequiv. simpl.
symmetry. apply minus_diag.
apply refl_cequiv.
Qed.
(* ####################################################### *)
(** * 程序变换 *)
(** _（程序变换）_ （ _program transformation_ ）是一种以任意程序
作为输入并且输出这个程序的某种变体的函数。比如编译中的常量折叠优化就是
一个典型的例子，但是程序变换不限于此。 *)
(** 如果一个程序变换的输出持有与其输入程序相同的行为，那么这个程序变换
是 _（健全）_ （ _sound_ ）的.
我们可以定义出 [aexp], [bexp], 和 [com] 的健全性的概念。 *)
Definition atrans_sound (atrans : aexp -> aexp) : Prop :=
forall (a : aexp),
aequiv a (atrans a).
Definition btrans_sound (btrans : bexp -> bexp) : Prop :=
forall (b : bexp),
bequiv b (btrans b).
Definition ctrans_sound (ctrans : com -> com) : Prop :=
forall (c : com),
cequiv c (ctrans c).
(* ######################################################## *)
(** ** 常量折叠变换 *)
(** 如果一个表达式不引用变量, 那么他就是 _（常量）_ （ _constant_ ）.
常量折叠是这样一种优化方式：找到常量表达式然后用它们的值替换它们. *)
Fixpoint fold_constants_aexp (a : aexp) : aexp :=
match a with
| ANum n => ANum n
| AId i => AId i
| APlus a1 a2 =>
match (fold_constants_aexp a1, fold_constants_aexp a2) with
| (ANum n1, ANum n2) => ANum (n1 + n2)
| (a1', a2') => APlus a1' a2'
end
| AMinus a1 a2 =>
match (fold_constants_aexp a1, fold_constants_aexp a2) with
| (ANum n1, ANum n2) => ANum (n1 - n2)
| (a1', a2') => AMinus a1' a2'
end
| AMult a1 a2 =>
match (fold_constants_aexp a1, fold_constants_aexp a2) with
| (ANum n1, ANum n2) => ANum (n1 * n2)
| (a1', a2') => AMult a1' a2'
end
end.
Example fold_aexp_ex1 :
fold_constants_aexp
(AMult (APlus (ANum 1) (ANum 2)) (AId X))
= AMult (ANum 3) (AId X).
Proof. reflexivity. Qed.
(** 注意这个版本的常量折叠不包括优化显而易见的加法等. -- 为了简单起见我们先
把注意力集中在一个优化上. 把其他简化表达式的优化合并进来也不难; 只是
定义和证明会更长. *)
Example fold_aexp_ex2 :
fold_constants_aexp
(AMinus (AId X) (APlus (AMult (ANum 0) (ANum 6)) (AId Y)))
= AMinus (AId X) (APlus (ANum 0) (AId Y)).
Proof. reflexivity. Qed.
(** *** *)
(** 我们不仅可以把 [fold_constants_aexp] 优化到 [bexp] (比如在某些 [BEq]
和 [BLe] 的时候), 我们也能找到一些 _（布尔）_ （ _boolean_ ）表达式的常量
在原地化简他们. *)
Fixpoint fold_constants_bexp (b : bexp) : bexp :=
match b with
| BTrue => BTrue
| BFalse => BFalse
| BEq a1 a2 =>
match (fold_constants_aexp a1, fold_constants_aexp a2) with
| (ANum n1, ANum n2) => if beq_nat n1 n2 then BTrue else BFalse
| (a1', a2') => BEq a1' a2'
end
| BLe a1 a2 =>
match (fold_constants_aexp a1, fold_constants_aexp a2) with
| (ANum n1, ANum n2) => if ble_nat n1 n2 then BTrue else BFalse
| (a1', a2') => BLe a1' a2'
end
| BNot b1 =>
match (fold_constants_bexp b1) with
| BTrue => BFalse
| BFalse => BTrue
| b1' => BNot b1'
end
| BAnd b1 b2 =>
match (fold_constants_bexp b1, fold_constants_bexp b2) with
| (BTrue, BTrue) => BTrue
| (BTrue, BFalse) => BFalse
| (BFalse, BTrue) => BFalse
| (BFalse, BFalse) => BFalse
| (b1', b2') => BAnd b1' b2'
end
end.
Example fold_bexp_ex1 :
fold_constants_bexp (BAnd BTrue (BNot (BAnd BFalse BTrue)))
= BTrue.
Proof. reflexivity. Qed.
Example fold_bexp_ex2 :
fold_constants_bexp
(BAnd (BEq (AId X) (AId Y))
(BEq (ANum 0)
(AMinus (ANum 2) (APlus (ANum 1) (ANum 1)))))
= BAnd (BEq (AId X) (AId Y)) BTrue.
Proof. reflexivity. Qed.
(** *** *)
(** 为了化简程序中的常量, 我们需要在所有子表达式上使用适当的函数. *)
Fixpoint fold_constants_com (c : com) : com :=
match c with
| SKIP =>
SKIP
| i ::= a =>
CAss i (fold_constants_aexp a)
| c1 ;; c2 =>
(fold_constants_com c1) ;; (fold_constants_com c2)
| IFB b THEN c1 ELSE c2 FI =>
match fold_constants_bexp b with
| BTrue => fold_constants_com c1
| BFalse => fold_constants_com c2
| b' => IFB b' THEN fold_constants_com c1
ELSE fold_constants_com c2 FI
end
| WHILE b DO c END =>
match fold_constants_bexp b with
| BTrue => WHILE BTrue DO SKIP END
| BFalse => SKIP
| b' => WHILE b' DO (fold_constants_com c) END
end
end.
(** *** *)
Example fold_com_ex1 :
fold_constants_com
(* 原程序: *)
(X ::= APlus (ANum 4) (ANum 5);;
Y ::= AMinus (AId X) (ANum 3);;
IFB BEq (AMinus (AId X) (AId Y)) (APlus (ANum 2) (ANum 4)) THEN
SKIP
ELSE
Y ::= ANum 0
FI;;
IFB BLe (ANum 0) (AMinus (ANum 4) (APlus (ANum 2) (ANum 1))) THEN
Y ::= ANum 0
ELSE
SKIP
FI;;
WHILE BEq (AId Y) (ANum 0) DO
X ::= APlus (AId X) (ANum 1)
END)
= (* 常量折叠后: *)
(X ::= ANum 9;;
Y ::= AMinus (AId X) (ANum 3);;
IFB BEq (AMinus (AId X) (AId Y)) (ANum 6) THEN
SKIP
ELSE
(Y ::= ANum 0)
FI;;
Y ::= ANum 0;;
WHILE BEq (AId Y) (ANum 0) DO
X ::= APlus (AId X) (ANum 1)
END).
Proof. reflexivity. Qed.
(* ################################################### *)
(** ** 常量折叠的健全性 *)
(** 现在我们证明之前所做的事情的正确性. *)
(** 这是对算数表达式的证明: *)
Theorem fold_constants_aexp_sound :
atrans_sound fold_constants_aexp.
Proof.
unfold atrans_sound. intros a. unfold aequiv. intros st.
induction a; simpl;
(* ANum 和 AId 很显然 *)
try reflexivity;
(* 从IH和下面的观察出发很容易完成 APlus , Aminus 和 AMult 的情况的证明：
aeval st (APlus a1 a2)
= ANum ((aeval st a1) + (aeval st a2))
= aeval st (ANum ((aeval st a1) + (aeval st a2)))
(之后的s AMinus/minus 和 AMult/mult 同理) *)
try (destruct (fold_constants_aexp a1);
destruct (fold_constants_aexp a2);
rewrite IHa1; rewrite IHa2; reflexivity). Qed.
(** **** Exercise: 3 stars, optional (fold_bexp_Eq_informal) *)
(** 这里有一个 “布尔表达式常量折叠中 [BEq] 的健全性” 的非形式化证明。认真读完
再和下面的形式化证明做比较。然后补充完整下面 [BLe] 的情况的形式化证明 （尽量
不看之前的 [BEq] 的情况的证明 ）。
_Theorem_: 布尔表达式的常量折叠函数 [fold_constants_bexp] ，有健全性。
_Proof_: 我们必须证明 对于所有 [b] ， [fold_constants_bexp] 有健全性。
我们在 [b] 上使用归纳法. 这里只给出 [b] 有 [BEq a1 a2] 的形式的证明。
在本例中, 我们需要证明
beval st (BEq a1 a2)
= beval st (fold_constants_bexp (BEq a1 a2)).
有两种情况需要讨论：
- 首先，假设对于某些 [n1] 和 [n2] 而言有 [fold_constants_aexp a1 = ANum n1] 和
[fold_constants_aexp a2 = ANum n2] 成立。
在这种情况下，我们有
fold_constants_bexp (BEq a1 a2)
= if beq_nat n1 n2 then BTrue else BFalse
和
beval st (BEq a1 a2)
= beq_nat (aeval st a1) (aeval st a2).
由于算数表达式的健全性(定理 [fold_constants_aexp_sound])，可得
aeval st a1
= aeval st (fold_constants_aexp a1)
= aeval st (ANum n1)
= n1
和
aeval st a2
= aeval st (fold_constants_aexp a2)
= aeval st (ANum n2)
= n2,
所以
beval st (BEq a1 a2)
= beq_nat (aeval a1) (aeval a2)
= beq_nat n1 n2.
同时, 容易看出 （在分别考虑 [n1 = n2] 和 [n1 <> n2] 的情况之后）
beval st (if beq_nat n1 n2 then BTrue else BFalse)
= if beq_nat n1 n2 then beval st BTrue else beval st BFalse
= if beq_nat n1 n2 then true else false
= beq_nat n1 n2.
所以
beval st (BEq a1 a2)
= beq_nat n1 n2.
= beval st (if beq_nat n1 n2 then BTrue else BFalse),
]]
正是所需的假设。
- 另一方面，假设 [fold_constants_aexp a1] 和 [fold_constants_aexp a2]
之中有一个不是常量。这种情况我们需要证明
beval st (BEq a1 a2)
= beval st (BEq (fold_constants_aexp a1)
(fold_constants_aexp a2)),
根据 [beval] 的定义，它等同于证明
beq_nat (aeval st a1) (aeval st a2)
= beq_nat (aeval st (fold_constants_aexp a1))
(aeval st (fold_constants_aexp a2)).
但是，由于算数表达式的健全性（定理 [fold_constants_aexp_sound]），可得出
aeval st a1 = aeval st (fold_constants_aexp a1)
aeval st a2 = aeval st (fold_constants_aexp a2),
本例证毕。 []
*)
Theorem fold_constants_bexp_sound:
btrans_sound fold_constants_bexp.
Proof.
unfold btrans_sound. intros b. unfold bequiv. intros st.
induction b;
(* BTrue 和 BFalse 是显然的 *)
try reflexivity.
- (* BEq *)
(* 当存在许多构造子时使用归纳法会使得认为指定变量名成为
一件琐事，然而Coq并不总是能够选择足够漂亮的变量名。
我们可以使用 重命名（[rename]）策略: [rename a into a1]
会把当前目标和上下文中的 [a] 替换成 [a1]. *)
rename a into a1. rename a0 into a2. simpl.
remember (fold_constants_aexp a1) as a1' eqn:Heqa1'.
remember (fold_constants_aexp a2) as a2' eqn:Heqa2'.
replace (aeval st a1) with (aeval st a1') by
(subst a1'; rewrite <- fold_constants_aexp_sound; reflexivity).
replace (aeval st a2) with (aeval st a2') by
(subst a2'; rewrite <- fold_constants_aexp_sound; reflexivity).
destruct a1'; destruct a2'; try reflexivity.
(* 唯一有趣的情况是 a1 和 a2 在折叠后同时变为常量 *)
simpl. destruct (beq_nat n n0); reflexivity.
- (* BLe *)
(* FILL IN HERE *) admit.
- (* BNot *)
simpl. remember (fold_constants_bexp b) as b' eqn:Heqb'.
rewrite IHb.
destruct b'; reflexivity.
- (* BAnd *)
simpl.
remember (fold_constants_bexp b1) as b1' eqn:Heqb1'.
remember (fold_constants_bexp b2) as b2' eqn:Heqb2'.
rewrite IHb1. rewrite IHb2.
destruct b1'; destruct b2'; reflexivity. Qed.
(** [] *)
(** **** Exercise: 3 stars (fold_constants_com_sound) *)
(** 补充以下证明的有关 [WHILE] 的部分. *)
Theorem fold_constants_com_sound :
ctrans_sound fold_constants_com.
Proof.
unfold ctrans_sound. intros c.
induction c; simpl.
- (* SKIP *) apply refl_cequiv.
- (* ::= *) apply CAss_congruence. apply fold_constants_aexp_sound.
- (* ;; *) apply CSeq_congruence; assumption.
- (* IFB *)