forked from Coq-zh/SF-zh
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathEquiv.v
1536 lines (1219 loc) · 49 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: 程序的等价关系 *)
Set Warnings "-notation-overridden,-parsing".
From PLF Require Import Maps.
From Coq Require Import Bool.Bool.
From Coq Require Import Arith.Arith.
From Coq Require Import Init.Nat.
From Coq Require Import Arith.PeanoNat. Import Nat.
From Coq Require Import Arith.EqNat.
From Coq Require Import omega.Omega.
From Coq Require Import Lists.List.
From Coq Require Import Logic.FunctionalExtensionality.
Import ListNotations.
From PLF Require Import Imp.
(** *** 一些关于习题的建议：
- 这里要进行的大多数 Coq 证明都与我们之前提供的类似。在做作业之前，
请先花点时间，非形式化地在纸上以及在 Coq 中思考我们的证明，
确保你完全理解了其中的每个细节。这会节省你大量的时间。
- 我们现在进行的 Coq 证明已经足够复杂，几乎不可能再单靠“感觉”
或乱撞的方式来完成证明了。你需要以“为何某个属性为真”以及“如何进行证明”
的想法开始。完成此任务的最佳方式是在开始形式化证明前，至少先在纸上写出
非形式化证明的梗概，即以直观的方式说服自己相信该定理成立，
然后再进行形式化证明。或者，你也可以拉一个好友，尝试说服他此定理成立，
然后形式化你的解释。
- 请使用自动化工具来减少工作量！如果你全部显式地写出证明中的所有情况，
那么本章中的证明会非常长。 *)
(* ################################################################# *)
(** * 行为的等价关系 *)
(** 在前面的章节中，我们探讨了一个非常简单的程序变换，即 [optimize_0plus]
函数的正确性。我们考虑的编程语言为算术表达式语言的第一版，它没有变量，
因此在该环境下，程序变换正确的意义非常容易定义：它产生的程序的求值结果
应当总是与原始程序产生的数字相等。
为了讨论整个 Imp 语言中程序变换，特别是赋值的正确性，
我们需要考虑变量和状态的作用。 *)
(* ================================================================= *)
(** ** 定义 *)
(** 对于包含变量的 [aexp] 和 [bexp] 而言，我们所需的定义简单明了。
只要在所有状态下，两个 [aexp] 或 [bexp] 的求值结果相同，
我们就说他们的_'行为等价（behaviorally equivalent）'_。 *)
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.
(** 下面是一些算术和布尔表达式等价的简单例子。 *)
Theorem aequiv_example: aequiv (X - X) 0.
Proof.
intros st. simpl. omega.
Qed.
Theorem bequiv_example: bequiv (X - X = 0) true.
Proof.
intros st. unfold beval.
rewrite aequiv_example. reflexivity.
Qed.
(** 对指令而言，情况则有些微妙。我们无法简单地说“如果在相同的初始状态下，
两个指令求值的停机状态相同，那么这两个指令等价”，
因为有些指令在某些初始状态下运行时根本不会在任何状态下停机！
我们实际上需要的是：“若两个指令在任何给定的初始状态下，要么发散，
要么在相同的状态下停机，则二者行为等价。”简单来说，就是：
“若其中一个指令在某状态下停机，那么另一个也在该状态下停机，反之亦然。” *)
Definition cequiv (c1 c2 : com) : Prop :=
forall (st st' : state),
(st =[ c1 ]=> st') <-> (st =[ c2 ]=> st').
(* ================================================================= *)
(** ** 简单示例 *)
(** 下面是一些指令等价的例子，我们首先从包含 [SKIP] 的简单程序变换开始： *)
Theorem skip_left : forall c,
cequiv
(SKIP;; c)
c.
Proof.
(* 课上已完成 *)
intros c st st'.
split; intros H.
- (* -> *)
inversion H; subst.
inversion H2. subst.
assumption.
- (* <- *)
apply E_Seq with st.
apply E_Skip.
assumption.
Qed.
(** **** 练习：2 星, standard (skip_right)
请证明在某条指令之后添加 [SKIP] 后，两程序会等价 *)
Theorem skip_right : forall c,
cequiv
(c ;; SKIP)
c.
Proof.
(* 请在此处解答 *) Admitted.
(** [] *)
(** 同样，下面是一个优化 [TEST] 的简单程序变换： *)
Theorem TEST_true_simple : forall c1 c2,
cequiv
(TEST true 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.
(** 当然，人类程序员是不会写把断言（guard）直接写成 [true] 的条件分支的。
不过当断言_'等价于真'_的情况时就会写出来：
_'定理'_：若 [b] 等价于 [BTrue]，则 [TEST b THEN c1 ELSE c2 FI] 等价于 [c1]。
_'证明'_：
- ([->]) 我们必须证明，对于所有的 [st] 和 [st']，若 [st =[
TEST b THEN c1 ELSE c2 FI ]=> st'] 则 [st =[ c1 ]=> st']。
能够应用于 [st =[ TEST b THEN c1 ELSE c2 FI ]=> st'] 的证明规则只有两条：
[E_IfTrue] 和 [E_IfFalse]。
- 假设 [st =[ TEST b THEN c1 ELSE c2 FI ]=> st'] 证明自 [E_IfTrue]
这条证明规则。若使用证明规则 [E_IfTrue] 其必备的前提条件 [st =[ c1 ]=> st']
必为真，而这正好是我们的证明所需要的条件。
- 另一方面, 假设 [st =[ TEST b THEN c1 ELSE c2 FI ]=> st'] 证明自
[E_IfFalse]。我们能得知 [beval st b = false] 和 [st =[ c2 ]=> 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']，若[st =[ c1 ]=> st']
则 [IFB b THEN c1 ELSE c2 FI / st \\ st']。
已知 [b] 等价于 [BTrue]，我们知道 [beval st b] = [beval st BTrue] = [true]。
结合 [st =[ c1 ]=> st'] 这条假设，我们能应用 [E_IfTrue] 来证明
[st =[ TEST b THEN c1 ELSE c2 FI ]=> st']。 []
下面是这个证明的形式化版本： *)
Theorem TEST_true: forall b c1 c2,
bequiv b BTrue ->
cequiv
(TEST 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.
(** **** 练习：2 星, standard, recommended (TEST_false) *)
Theorem TEST_false : forall b c1 c2,
bequiv b BFalse ->
cequiv
(TEST b THEN c1 ELSE c2 FI)
c2.
Proof.
(* 请在此处解答 *) Admitted.
(** [] *)
(** **** 练习：3 星, standard (swap_if_branches)
证明我们可以通过对断言取反来交换 IF 的两个分支 *)
Theorem swap_if_branches : forall b e1 e2,
cequiv
(TEST b THEN e1 ELSE e2 FI)
(TEST BNot b THEN e2 ELSE e1 FI).
Proof.
(* 请在此处解答 *) 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_WhileFalse *)
apply E_Skip.
+ (* E_WhileTrue *)
rewrite Hb in H2. inversion H2.
- (* <- *)
inversion H; subst.
apply E_WhileFalse.
rewrite Hb.
reflexivity. Qed.
(** **** 练习：2 星, advanced, optional (WHILE_false_informal)
写出 [WHILE_false] 的非形式化证明。
(* 请在此处解答 *)
*)
(** [] *)
(** 为了证明第二个定理，我们需要一个辅助引理：[WHILE] 循环在其断言等价于 [BTrue]
时不会停机。 *)
(** _'引理'_：若 [b] 等价于 [BTrue]，则无法出现
[st =[ WHILE b DO c END ]=> st'] 的情况。
_'证明'_：假设 [st =[ WHILE b DO c END ]=> st']。我们将证明通过对
[st =[ WHILE b DO c END ]=> st'] 使用归纳法会导出矛盾。需要考虑只有
[E_WhileFalse] 和 [E_WhileTrue] 两种情况，其它情况则矛盾。
- 假设 [st =[ WHILE b DO c END ]=> st'] 使用规则 [E_WhileFalse] 证明。
那么根据假设得出 [beval st b = false]。但它与 [b] 等价于 [BTrue] 矛盾。
- 假设 [st =[ WHILE b DO c END ]=> st'] 使用规则 [E_WhileTrue]证明。
我们必有：
1. [beval st b = true]，
2. 存在某个 [st0] 使得 [st =[ c ]=> st0] 且
[st0 =[ WHILE b DO c END ]=> st']，
3. 以及我们给出了导致矛盾的归纳假设 [st0 =[ WHILE b DO c END ]=> st']，
我们根据 2 和 3 会得到矛盾。 [] *)
Lemma WHILE_true_nonterm : forall b c st st',
bequiv b BTrue ->
~( st =[ WHILE b DO c END ]=> st' ).
Proof.
(* 课上已完成 *)
intros b c st st' Hb.
intros H.
remember (WHILE b DO c END)%imp as cw eqn:Heqcw.
induction H;
(* 大多数证明规则无法应用，我们可通过反演（inversion）来去除它们： *)
inversion Heqcw; subst; clear Heqcw.
(* 我们只关心这两个关于 WHILE 循环的证明规则： *)
- (* E_WhileFalse *) (* 矛盾 -- b 总为真！ *)
unfold bequiv in Hb.
(* [rewrite] 能实例化 [st] 中的量词 *)
rewrite Hb in H. inversion H.
- (* E_WhileTrue *) (* 直接使用 IH *)
apply IHceval2. reflexivity. Qed.
(** **** 练习：2 星, standard, optional (WHILE_true_nonterm_informal)
试解释 [WHILE_true_nonterm] 的含义。
(* 请在此处解答 *)
*)
(** [] *)
(** **** 练习：2 星, standard, recommended (WHILE_true)
请证明以下定理。_'提示'_：你可能需要使用 [WHILE_true_nonterm] 。 *)
Theorem WHILE_true : forall b c,
bequiv b true ->
cequiv
(WHILE b DO c END)
(WHILE true DO SKIP END).
Proof.
(* 请在此处解答 *) Admitted.
(** [] *)
(** 关于 [WHILE] 指令的更有趣的事实是，任何数量的循环体的副本在不改变意义
的情况下均可被“展开”。循环展开在实际的编译器中是种常见的变换。 *)
Theorem loop_unrolling : forall b c,
cequiv
(WHILE b DO c END)
(TEST b THEN (c ;; WHILE b DO c END) ELSE SKIP FI).
Proof.
(* 课上已完成 *)
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_WhileTrue with (st' := st'0).
assumption. assumption. assumption.
+ (* 不执行循环 *)
inversion H5; subst. apply E_WhileFalse. assumption. Qed.
(** **** 练习：2 星, standard, optional (seq_assoc) *)
Theorem seq_assoc : forall c1 c2 c3,
cequiv ((c1;;c2);;c3) (c1;;(c2;;c3)).
Proof.
(* 请在此处解答 *) Admitted.
(** [] *)
(** 证明涉及赋值的程序的属性经常会用到这一事实，即程序状态会根据其外延性
（如 [x !-> m x ; m] 和 [m] 是相等的映射）来对待。 *)
Theorem identity_assignment : forall x,
cequiv
(x ::= x)
SKIP.
Proof.
intros.
split; intro H; inversion H; subst.
- (* -> *)
rewrite t_update_same.
apply E_Skip.
- (* <- *)
assert (Hx : st' =[ x ::= x ]=> (x !-> st' x ; st')).
{ apply E_Ass. reflexivity. }
rewrite t_update_same in Hx.
apply Hx.
Qed.
(** **** 练习：2 星, standard, recommended (assign_aequiv) *)
Theorem assign_aequiv : forall (x : string) e,
aequiv x e ->
cequiv SKIP (x ::= e).
Proof.
(* 请在此处解答 *) Admitted.
(** [] *)
(** **** 练习：2 星, standard (equiv_classes) *)
(** 给定下列程序，请按照它们在 [Imp] 中是否等价将这些程序分组。
你的答案应该是一个列表的列表，其中每个子列表都表示一组等价的程序。
例如，如果你认为程序 (a) 至 (h) 都互相等价，但不等价于 (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 ~(X <= 0) DO
X ::= X + 1
END)%imp.
Definition prog_b : com :=
(TEST X = 0 THEN
X ::= X + 1;;
Y ::= 1
ELSE
Y ::= 0
FI;;
X ::= X - Y;;
Y ::= 0)%imp.
Definition prog_c : com :=
SKIP%imp.
Definition prog_d : com :=
(WHILE ~(X = 0) DO
X ::= (X * Y) + 1
END)%imp.
Definition prog_e : com :=
(Y ::= 0)%imp.
Definition prog_f : com :=
(Y ::= X + 1;;
WHILE ~(X = Y) DO
Y ::= X + 1
END)%imp.
Definition prog_g : com :=
(WHILE true DO
SKIP
END)%imp.
Definition prog_h : com :=
(WHILE ~(X = X) DO
X ::= X + 1
END)%imp.
Definition prog_i : com :=
(WHILE ~(X = Y) DO
X ::= Y + 1
END)%imp.
Definition equiv_classes : list (list com)
(* 将本行替换成 ":= _你的_定义_ ." *). Admitted.
(* 请勿修改下面这一行： *)
Definition manual_grade_for_equiv_classes : option (nat*string) := None.
(** [] *)
(* ################################################################# *)
(** * 行为等价的性质 *)
(** 接下来我们考虑程序等价的一些基本性质。 *)
(* ================================================================= *)
(** ** 行为等价是一种等价关系 *)
(** 首先, 我们验证 [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 (st =[ c1 ]=> st' <-> st =[ c2 ]=> st') as H'.
{ (* Proof of assertion *) 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 (st =[ c2 ]=> st'). apply H12. apply H23. Qed.
(* ================================================================= *)
(** ** 行为等价是一种一致性 *)
(** 虽然不太明显，但行为等价也满足_'一致性（congruence）'_。
即，如果两个子程序等价，那么当二者所在的更大的程序中只有二者不同时，
这两个更大的程序也等价：
aequiv a1 a1'
-----------------------------
cequiv (x ::= a1) (x ::= a1')
cequiv c1 c1'
cequiv c2 c2'
--------------------------
cequiv (c1;;c2) (c1';;c2')
...以及这些指令的更多其它形式。 *)
(** （注意这里使用的推理规则的记法并不是定义的成部分，只是将一些
合法的蕴含式用易读的方式写下而已。接下来我们将证明这些蕴含式。） *)
(** 在接下来的章节（[fold_constants_com_sound] 的证明）中，我们会用
具体例子来说明这种一致性多么重要。不过它最主要意义在于，当我们在用
一小部分程序替换大程序中等价的部分并证明替换前后程序的等价关系时，
_'无需'_进行与不变的部分相关的证明。也就是说，程序的改变所产生的证明的工作量
与改变的大小而非整个程序的大小成比例。 *)
Theorem CAss_congruence : forall x a1 a1',
aequiv a1 a1' ->
cequiv (CAss x a1) (CAss x a1').
Proof.
intros x 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.
(** 循环的一致性更有趣, 因为它需要使用归纳法。
_'定理'_: 对于 [WHILE]，等价关系是一种一致性 -- 即，若 [b1] 等价于 [b1'] 且 [c1]
等价于 [c1']，那么 [WHILE b1 DO c1 END] 等价于 [WHILE b1' DO c1' END]。
_'证明'_: 假设 [b1] 等价于 [b1'] 且 [c1] 等价于 [c1']。我们必须证明，
对于每个 [st] 和 [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']。
只有推导的最后所使用的规则为 [E_WhileFalse] 或 [E_WhileTrue]
时才需要进行特别讨论。
- [E_WhileFalse]：此时我们拥有假设的必备条件 [beval st b1 = false]
和 [st = st']。但是，由于 [b1] 和 [b1'] 等价，我们有
[beval st b1' = false]，然后应用 [E-WhileFalse] 得出我们需要的
[st =[ WHILE b1' DO c1' END ]=> st']。
- [E_WhileTrue]：此时我们拥有假设的必备条件 [beval st b1 = true]，以及
对于某些状态 [st'0] 的 [st =[ c1 ]=> st'0] 和 [st'0 =[ WHILE b1 DO c1
END ]=> st']，还有归纳假设 [st'0 =[ WHILE b1' DO c1' END ]=> st']。
由于 [c1] 和 [c1'] 等价，我们有 [st =[ c1' ]=> st'0]；
由于 [b1] 和 [b1'] 等价，我们有 [beval st b1' = true]。现在应用
[E-WhileTrue]，得出我们所需的 [st =[ WHILE b1' DO c1' END ]=> 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.
(* 课上已完成 *)
unfold bequiv,cequiv.
intros b1 b1' c1 c1' Hb1e Hc1e st st'.
split; intros Hce.
- (* -> *)
remember (WHILE b1 DO c1 END)%imp as cwhile
eqn:Heqcwhile.
induction Hce; inversion Heqcwhile; subst.
+ (* E_WhileFalse *)
apply E_WhileFalse. rewrite <- Hb1e. apply H.
+ (* E_WhileTrue *)
apply E_WhileTrue with (st' := st').
* (* 执行展示循环 *) rewrite <- Hb1e. apply H.
* (* 执行主体 *)
apply (Hc1e st st'). apply Hce1.
* (* 执行之后的循环 *)
apply IHHce2. reflexivity.
- (* <- *)
remember (WHILE b1' DO c1' END)%imp as c'while
eqn:Heqc'while.
induction Hce; inversion Heqc'while; subst.
+ (* E_WhileFalse *)
apply E_WhileFalse. rewrite -> Hb1e. apply H.
+ (* E_WhileTrue *)
apply E_WhileTrue with (st' := st').
* (* 执行展示循环 *) rewrite -> Hb1e. apply H.
* (* 执行主体 *)
apply (Hc1e st st'). apply Hce1.
* (* 执行之后的循环 *)
apply IHHce2. reflexivity. Qed.
(** **** 练习：3 星, standard, optional (CSeq_congruence) *)
Theorem CSeq_congruence : forall c1 c1' c2 c2',
cequiv c1 c1' -> cequiv c2 c2' ->
cequiv (c1;;c2) (c1';;c2').
Proof.
(* 请在此处解答 *) Admitted.
(** [] *)
(** **** 练习：3 星, standard (CIf_congruence) *)
Theorem CIf_congruence : forall b b' c1 c1' c2 c2',
bequiv b b' -> cequiv c1 c1' -> cequiv c2 c2' ->
cequiv (TEST b THEN c1 ELSE c2 FI)
(TEST b' THEN c1' ELSE c2' FI).
Proof.
(* 请在此处解答 *) Admitted.
(** [] *)
(** 例如，下面是两个等价的程序和它们等价关系的证明... *)
Example congruence_example:
cequiv
(* 程序 1： *)
(X ::= 0;;
TEST X = 0
THEN
Y ::= 0
ELSE
Y ::= 42
FI)
(* 程序 1： *)
(X ::= 0;;
TEST X = 0
THEN
Y ::= X - X (* <--- 这里不同 *)
ELSE
Y ::= 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.
(** **** 练习：3 星, advanced, optional (not_congr)
我们已经证明了 [cequiv] 关系对指令同时满足等价关系和一致性。
你能想出一个对于指令满足等价关系但_'不满足'_一致性的关系吗？ *)
(* 请在此处解答
[] *)
(* ################################################################# *)
(** * 程序变换 *)
(** _'程序变换（program transformation）'_是一种以某个程序作为输入，
产生该程序的某种变体作为输出的函数。编译器优化中的常量折叠就是个经典的例子，
然而程序变换并不仅限如此。 *)
(** 如果一个程序变换保留了其原始行为，那么它就是_'可靠（sound）'_的。 *)
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 x => AId x
| 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 ((1 + 2) * X)
= (3 * X)%imp.
Proof. reflexivity. Qed.
(** 注意此版本的常量折叠不包括优化平凡的加法等 -- 为简单起见，
我们把注意力集中到单个优化上来。将其它简化表达式的方法加进来也不难，
只是定义和证明会更长。 *)
Example fold_aexp_ex2 :
fold_constants_aexp (X - ((0 * 6) + Y))%imp = (X - (0 + Y))%imp.
Proof. reflexivity. Qed.
(** 我们不仅可以将 [fold_constants_aexp] 优化成 [bexp]（如在 [BEq] 和 [BLe]
的情况下），还可以查找常量_'布尔'_表达式并原地求值。 *)
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 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 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 (true && ~(false && true))%imp
= true.
Proof. reflexivity. Qed.
Example fold_bexp_ex2 :
fold_constants_bexp ((X = Y) && (0 = (2 - (1 + 1))))%imp
= ((X = Y) && true)%imp.
Proof. reflexivity. Qed.
(** 为了折叠指令中的常量，我们需要对所有内嵌的表达式应用适当的折叠函数。 *)
Open Scope imp.
Fixpoint fold_constants_com (c : com) : com :=
match c with
| SKIP =>
SKIP
| x ::= a =>
x ::= (fold_constants_aexp a)
| c1 ;; c2 =>
(fold_constants_com c1) ;; (fold_constants_com c2)
| TEST b THEN c1 ELSE c2 FI =>
match fold_constants_bexp b with
| BTrue => fold_constants_com c1
| BFalse => fold_constants_com c2
| b' => TEST 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.
Close Scope imp.
Example fold_com_ex1 :
fold_constants_com
(* 原程序： *)
(X ::= 4 + 5;;
Y ::= X - 3;;
TEST (X - Y) = (2 + 4) THEN SKIP
ELSE Y ::= 0 FI;;
TEST 0 <= (4 - (2 + 1)) THEN Y ::= 0
ELSE SKIP FI;;
WHILE Y = 0 DO
X ::= X + 1
END)%imp
= (* 常量折叠后： *)
(X ::= 9;;
Y ::= X - 3;;
TEST (X - Y) = 6 THEN SKIP
ELSE Y ::= 0 FI;;
Y ::= 0;;
WHILE Y = 0 DO
X ::= X + 1
END)%imp.
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)))
（AMinus/minus 和 AMult/mult 同理） *)
try (destruct (fold_constants_aexp a1);
destruct (fold_constants_aexp a2);
rewrite IHa1; rewrite IHa2; reflexivity). Qed.
(** **** 练习：3 星, standard, optional (fold_bexp_Eq_informal)
下面是布尔表达式常量折叠中 [BEq] 情况的可靠性的证明。
请认真读完它再和之后的形式化证明作比较，然后补充完 [BLe] 情况的形式化证明
（尽量不看之前 [BEq] 情况的证明）。
_'定理'_：布尔值的常量折叠函数 [fold_constants_bexp] 是可靠的。
_'证明'_：我们必须证明对于所有的布尔表达式 [b]，[b] 都等价于
[fold_constants_bexp b]。我们对 [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 n1 =? n2 then BTrue else BFalse
和
beval st (BEq a1 a2)
= (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)
= (aeval a1) =? (aeval a2)
= n1 =? n2.
此外，在分别考虑 [n1 = n2] 和 [n1 <> n2] 的情况后，容易看出
beval st (if n1 =? n2 then BTrue else BFalse)
= if n1 =? n2 then beval st BTrue else beval st BFalse
= if n1 =? n2 then true else false
= n1 =? n2.
因此
beval st (BEq a1 a2)
= n1 =? n2.
= beval st (if 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] 的定义，它等同于证明
(aeval st a1) =? (aeval st a2)
= (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 *)
simpl.
(** （当存在许多构造子时，使用归纳法会让给变量取名编程一件琐事，
然而 Coq 并不总是能够选择足够好的变量名。我们可以使用 [rename] 重命名：
策略 [rename a into a1] 会将当前目标和上下文中的 [a] 重命名为 [a1]。） *)
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 (n =? n0); reflexivity.
- (* BLe *)
(* 请在此处解答 *) 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.
(* 请在此处解答 *) Admitted.
(** [] *)
(** **** 练习：3 星, standard (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.
- (* TEST *)
assert (bequiv b (fold_constants_bexp b)). {
apply fold_constants_bexp_sound. }
destruct (fold_constants_bexp b) eqn:Heqb;
try (apply CIf_congruence; assumption).
(* （如果 if 没有被优化掉，那么我们很容易使用 IH 和
[fold_constants_bexp_sound] 来得出证明。） *)
+ (* b 总为真 *)
apply trans_cequiv with c1; try assumption.
apply TEST_true; assumption.
+ (* b 总为假 *)
apply trans_cequiv with c2; try assumption.
apply TEST_false; assumption.
- (* WHILE *)