一些关于习题的建议：

• 这里要进行的大多数 Coq 证明都与我们之前提供的类似。在做作业之前， 请先花点时间，非形式化地在纸上以及在 Coq 中思考我们的证明， 确保你完全理解了其中的每个细节。这会节省你大量的时间。
• 我们现在进行的 Coq 证明已经足够复杂，几乎不可能再单靠“感觉” 或乱撞的方式来完成证明了。你需要以“为何某个属性为真”以及“如何进行证明” 的想法开始。完成此任务的最佳方式是在开始形式化证明前，至少先在纸上写出 非形式化证明的梗概，即以直观的方式说服自己相信该定理成立， 然后再进行形式化证明。或者，你也可以拉一个好友，尝试说服他此定理成立， 然后形式化你的解释。
• 请使用自动化工具来减少工作量！如果你全部显式地写出证明中的所有情况， 那么本章中的证明会非常长。

行为的等价关系

在前面的章节中，我们探讨了一个非常简单的程序变换，即 optimize_0plus 函数的正确性。我们考虑的编程语言为算术表达式语言的第一版，它没有变量， 因此在该环境下，程序变换正确的意义非常容易定义：它产生的程序的求值结果 应当总是与原始程序产生的数字相等。 为了讨论整个 Imp 语言中程序变换，特别是赋值的正确性， 我们需要考虑变量和状态的作用。

定义

对于包含变量的 aexp 和 bexp 而言，我们所需的定义简单明了。 只要在所有状态下，两个 aexp 或 bexp 的求值结果相同， 我们就说他们的'行为等价（behaviorally equivalent）'。

下面是一些算术和布尔表达式等价的简单例子。

对指令而言，情况则有些微妙。我们无法简单地说“如果在相同的初始状态下， 两个指令求值的停机状态相同，那么这两个指令等价”， 因为有些指令在某些初始状态下运行时根本不会在任何状态下停机！ 我们实际上需要的是：“若两个指令在任何给定的初始状态下，要么发散， 要么在相同的状态下停机，则二者行为等价。”简单来说，就是： “若其中一个指令在某状态下停机，那么另一个也在该状态下停机，反之亦然。”

简单示例

下面是一些指令等价的例子，我们首先从包含 SKIP 的简单程序变换开始：

练习：2 星, standard (skip_right)

请证明在某条指令之后添加 SKIP 后，两程序会等价

同样，下面是一个优化 TEST 的简单程序变换：

当然，人类程序员是不会写把断言（guard）直接写成 true 的条件分支的。 不过当断言'等价于真'的情况时就会写出来： '定理'：若 b 等价于 BTrue，则 TEST b THEN c₁ ELSE c₂ FI 等价于 c₁。 '证明'：

• (→) 我们必须证明，对于所有的 st 和 st'，若 st =[ TEST b THEN c₁ ELSE c₂ FI ]=> st' 则 st =[ c₁ ]=> st'。
  能够应用于 st =[ TEST b THEN c₁ ELSE c₂ FI ]=> st' 的证明规则只有两条： E_IfTrue 和 E_IfFalse。
  • 假设 st =[ TEST b THEN c₁ ELSE c₂ FI ]=> st' 证明自 E_IfTrue 这条证明规则。若使用证明规则 E_IfTrue 其必备的前提条件 st =[ c₁ ]=> st' 必为真，而这正好是我们的证明所需要的条件。
  • 另一方面, 假设 st =[ TEST b THEN c₁ ELSE c₂ FI ]=> st' 证明自 E_IfFalse。我们能得知 beval st b = false 和 st =[ c₂ ]=> 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 =[ c₁ ]=> st' 则 IFB b THEN c₁ ELSE c₂ FI / st \\ st'。
  已知 b 等价于 BTrue，我们知道 beval st b = beval st BTrue = true。 结合 st =[ c₁ ]=> st' 这条假设，我们能应用 E_IfTrue 来证明 st =[ TEST b THEN c₁ ELSE c₂ FI ]=> st'。 ☐

下面是这个证明的形式化版本：

练习：2 星, standard, recommended (TEST_false)

练习：3 星, standard (swap_if_branches)

证明我们可以通过对断言取反来交换 IF 的两个分支

对于 WHILE 循环，我们能够给出一组相似的定理：当循环的断言等价于 BFalse 时它等价于 SKIP；当循环的断言等价于 BTrue 时它等价于 WHILE BTrue DO SKIP END（或任意不停机的程序）。前者比较简单。

练习：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. 存在某个 st₀ 使得 st =[ c ]=> st₀ 且 st₀ =[ WHILE b DO c END ]=> st'， 3. 以及我们给出了导致矛盾的归纳假设 st₀ =[ WHILE b DO c END ]=> st'， 我们根据 2 和 3 会得到矛盾。 ☐

练习：2 星, standard, optional (WHILE_true_nonterm_informal)

试解释 WHILE_true_nonterm 的含义。 (* 请在此处解答 *)
☐

练习：2 星, standard, recommended (WHILE_true)

请证明以下定理。'提示'：你可能需要使用 WHILE_true_nonterm 。

关于 WHILE 指令的更有趣的事实是，任何数量的循环体的副本在不改变意义 的情况下均可被“展开”。循环展开在实际的编译器中是种常见的变换。

练习：2 星, standard, optional (seq_assoc)

证明涉及赋值的程序的属性经常会用到这一事实，即程序状态会根据其外延性 （如 x !-> m x ; m 和 m 是相等的映射）来对待。

练习：2 星, standard, recommended (assign_aequiv)

练习：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 的定义下方写出你的答案。

行为等价的性质

接下来我们考虑程序等价的一些基本性质。

行为等价是一种等价关系

首先, 我们验证 aexps、bexps 和 com 的确满足'等价关系（equivalences）' -- 也就是说，它同时满足自反性（reflexive）、对称性（symmetric）和传递性 （transitive）。这些证明都很容易。

行为等价是一种一致性

虽然不太明显，但行为等价也满足'一致性（congruence）'。 即，如果两个子程序等价，那么当二者所在的更大的程序中只有二者不同时， 这两个更大的程序也等价：

aequiv a1 a1'
cequiv (x ::= a1) (x ::= a1')

cequiv c1 c1'
cequiv c2 c2'
cequiv (c1;;c2) (c1';;c2')

...以及这些指令的更多其它形式。 （注意这里使用的推理规则的记法并不是定义的成部分，只是将一些 合法的蕴含式用易读的方式写下而已。接下来我们将证明这些蕴含式。） 在接下来的章节（fold_constants_com_sound 的证明）中，我们会用 具体例子来说明这种一致性多么重要。不过它最主要意义在于，当我们在用 一小部分程序替换大程序中等价的部分并证明替换前后程序的等价关系时， '无需'进行与不变的部分相关的证明。也就是说，程序的改变所产生的证明的工作量 与改变的大小而非整个程序的大小成比例。

循环的一致性更有趣, 因为它需要使用归纳法。 '定理': 对于 WHILE，等价关系是一种一致性 -- 即，若 b₁ 等价于 b₁' 且 c₁ 等价于 c₁'，那么 WHILE b₁ DO c₁ END 等价于 WHILE b₁' DO c₁' END。 '证明': 假设 b₁ 等价于 b₁' 且 c₁ 等价于 c₁'。我们必须证明， 对于每个 st 和 st'，st =[ WHILE b₁ DO c₁ END ]=> st' 当且仅当 st =[ WHILE b₁' DO c₁' END ]=> st'。我们把两个方向分开考虑。

• (→) 我们通过对 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 时才需要进行特别讨论。
  • E_WhileFalse：此时我们拥有假设的必备条件 beval st b₁ = false 和 st = st'。但是，由于 b₁ 和 b₁' 等价，我们有 beval st b₁' = false，然后应用 E-WhileFalse 得出我们需要的 st =[ WHILE b₁' DO c₁' END ]=> st'。
  • E_WhileTrue：此时我们拥有假设的必备条件 beval st b₁ = true，以及 对于某些状态 st'0 的 st =[ c₁ ]=> st'0 和 st'0 =[ WHILE b₁ DO c₁ END ]=> st'，还有归纳假设 st'0 =[ WHILE b₁' DO c₁' END ]=> st'。
    由于 c₁ 和 c₁' 等价，我们有 st =[ c₁' ]=> st'0； 由于 b₁ 和 b₁' 等价，我们有 beval st b₁' = true。现在应用 E-WhileTrue，得出我们所需的 st =[ WHILE b₁' DO c₁' END ]=> st'。
• (<-) 反之亦然。 ☐

练习：3 星, standard, optional (CSeq_congruence)

练习：3 星, standard (CIf_congruence)

例如，下面是两个等价的程序和它们等价关系的证明...

练习：3 星, advanced, optional (not_congr)

我们已经证明了 cequiv 关系对指令同时满足等价关系和一致性。 你能想出一个对于指令满足等价关系但'不满足'一致性的关系吗？

程序变换

'程序变换（program transformation）'是一种以某个程序作为输入， 产生该程序的某种变体作为输出的函数。编译器优化中的常量折叠就是个经典的例子， 然而程序变换并不仅限如此。 如果一个程序变换保留了其原始行为，那么它就是'可靠（sound）'的。

常量折叠变换

不引用变量的表达式为'常量（constant）'。 常量折叠是一种找到常量表达式并把它们替换为其值的优化方法。

注意此版本的常量折叠不包括优化平凡的加法等 -- 为简单起见， 我们把注意力集中到单个优化上来。将其它简化表达式的方法加进来也不难， 只是定义和证明会更长。

我们不仅可以将 fold_constants_aexp 优化成 bexp（如在 BEq 和 BLe 的情况下），还可以查找常量'布尔'表达式并原地求值。

为了折叠指令中的常量，我们需要对所有内嵌的表达式应用适当的折叠函数。

常量折叠的可靠性

现在我们需要证明之前所做事情的正确性。 下面是对算术表达式的证明：

练习：3 星, standard, optional (fold_bexp_Eq_informal)

下面是布尔表达式常量折叠中 BEq 情况的可靠性的证明。 请认真读完它再和之后的形式化证明作比较，然后补充完 BLe 情况的形式化证明 （尽量不看之前 BEq 情况的证明）。 '定理'：布尔值的常量折叠函数 fold_constants_bexp 是可靠的。 '证明'：我们必须证明对于所有的布尔表达式 b，b 都等价于 fold_constants_bexp b。我们对 b 使用归纳法。这里只给出了 b 形如 BEq a₁ a₂ 的情况。 在本情况中，我们必须证明
       beval st (BEq a₁ a₂)
     = beval st (fold_constants_bexp (BEq a₁ a₂)).

有两种情况需要考虑：

• 首先，假设对于某些 n₁ 和 n₂ 而言有 fold_constants_aexp a₁ = ANum n₁ 和 fold_constants_aexp a₂ = ANum n₂。
  在此情况下，我们有
             fold_constants_bexp (BEq a₁ a₂)
           = if n₁ =? n₂ then BTrue else BFalse
  和
             beval st (BEq a₁ a₂)
           = (aeval st a₁) =? (aeval st a₂).
  根据算术表达式常量折叠的健全性（引理 fold_constants_aexp_sound）可得
             aeval st a₁
           = aeval st (fold_constants_aexp a₁)
           = aeval st (ANum n₁)
           = n₁
  和
             aeval st a₂
           = aeval st (fold_constants_aexp a₂)
           = aeval st (ANum n₂)
           = n₂,
  因此
             beval st (BEq a₁ a₂)
           = (aeval a₁) =? (aeval a₂)
           = n₁ =? n₂.
  此外，在分别考虑 n₁ = n₂ 和 n₁ ≠ n₂ 的情况后，容易看出
             beval st (if n₁ =? n₂ then BTrue else BFalse)
           = if n₁ =? n₂ then beval st BTrue else beval st BFalse
           = if n₁ =? n₂ then true else false
           = n₁ =? n₂.
  因此
             beval st (BEq a₁ a₂)
           = n₁ =? n₂.
           = beval st (if n₁ =? n₂ then BTrue else BFalse),
  正是所需的假设。
• 另一方面，假设 fold_constants_aexp a₁ 和 fold_constants_aexp a₂ 之一并非常量。此时，我们必须证明
             beval st (BEq a₁ a₂)
           = beval st (BEq (fold_constants_aexp a₁)
                           (fold_constants_aexp a₂)),
  根据 beval 的定义，它等同于证明
             (aeval st a₁) =? (aeval st a₂)
           = (aeval st (fold_constants_aexp a₁)) =?
                     (aeval st (fold_constants_aexp a₂)).
  但是，由于算术表达式的可靠性（定理 fold_constants_aexp_sound）可得出
           aeval st a₁ = aeval st (fold_constants_aexp a₁)
           aeval st a₂ = aeval st (fold_constants_aexp a₂),
  本例证毕。 ☐

（当存在许多构造子时，使用归纳法会让给变量取名编程一件琐事， 然而 Coq 并不总是能够选择足够好的变量名。我们可以使用 rename 重命名： 策略 rename a into a₁ 会将当前目标和上下文中的 a 重命名为 a₁。）

练习：3 星, standard (fold_constants_com_sound)

完成以下证明的 WHILE 情况。

再论 (0 + n) 优化的可靠性

练习：4 星, advanced, optional (optimize_0plus)

回顾'逻辑基础' Imp 一章中 optimize_0plus 的定义：
    Fixpoint optimize_0plus (e:aexp) : aexp :=
      match e with
      | ANum n ⇒
          ANum n
      | APlus (ANum 0) e₂ ⇒
          optimize_0plus e₂
      | APlus e₁ e₂ ⇒
          APlus (optimize_0plus e₁) (optimize_0plus e₂)
      | AMinus e₁ e₂ ⇒
          AMinus (optimize_0plus e₁) (optimize_0plus e₂)
      | AMult e₁ e₂ ⇒
          AMult (optimize_0plus e₁) (optimize_0plus e₂)
      end.

注意此函数是针对无状态的 aexp 编写的。 请为 aexp bexp 和 com 都写一个带状态的新版本：
     optimize_0plus_aexp
     optimize_0plus_bexp
     optimize_0plus_com

请证明这三个函数都具有可靠性，就像之前证明 fold_constants_× 那样。在 optimize_0plus_com 的证明中你需要一致性引理 -- 否则证明过程会'很长'！ 接下来为指令定义一个优化器，它首先使用常量折叠（fold_constants_com）然后优化掉 0 + n 项（使用 optimize_0plus_com）。

• 请为此优化器写一个有意义的测试用例。
• 证明此优化程序有可靠性。（这部分应该会'很简单' 。）

证明程序不等价

假设 c₁ 是形如 X ::= a₁;; Y ::= a₂ 的指令，并且 c₂ 是形如 X ::= a₁;; Y ::= a₂' 的指令，a₂' 是把 a₂ 中所有 X 都替换为 a₁ 后的结果。比如，c₁ 和 c₂ 可以像这样：
       c₁ = (X ::= 42 + 53;;
               Y ::= Y + X)
       c₂ = (X ::= 42 + 53;;
               Y ::= Y + (42 + 53))

很明显，在这个'特定的例子中' c₁ 和 c₂ 是等价的。但是对一般程序而言， 此结果是否成立？ 我们马上就会发现这是不行的。不过且慢，现在， 看你自己能否找出一个反例来。 以下形式化的定义描述了如何在算术表达式 a 中， 将某个变量 x 的所有引用都替换成另一个表达式 u ：

而这里是一个我们感兴趣的性质：它断言类似上述形式的 c₁ 和 c₂ 总是等价的。

遗憾的是, 这个性质'并不'总是成立 -- 即，它并不是对所有的 x₁、x₂、a₁ 和 a₂ 都成立。
      cequiv (x₁ ::= a₁;; x₂ ::= a₂)
             (x₁ ::= a₁;; x₂ ::= subst_aexp x₁ a₁ a₂).

我们使用反证法来证明这一点。假设对于所有的 x₁、x₂、a₁ 和 a₂，我们有
      cequiv (x₁ ::= a₁;; x₂ ::= a₂)
             (x₁ ::= a₁;; x₂ ::= subst_aexp x₁ a₁ a₂).

考虑以下程序：
      X ::= X + 1;; Y ::= X

注意
      empty_st =[ X ::= X + 1;; Y ::= X ]=> st₁,

其中 st₁ = (Y !-> 1 ; X !-> 1). 根据假设，我们知道
      cequiv (X ::= X + 1;;
              Y ::= X)
             (X ::= X + 1;;
              Y ::= X + 1)

同时，根据 cequiv 的定义，我们有
      empty_st =[ X ::= X + 1;; Y ::= X + 1 ]=> st₁.

但是我们也能推导出
      empty_st =[ X ::= X + 1;; Y ::= X + 1 ]=> st₂,

其中 st₂ = (Y !-> 2 ; X !-> 1)。但由于 ceval 是确定性的，而 st₁ ≠ st₂ ，这就造成了矛盾！ ☐

练习：4 星, standard, optional (better_subst_equiv)

之前我们思考的等价关系也不全是妄言 -- 只要再增加一个条件， 即变量 X 不在第一个赋值语句的右边出现，它就是正确的了。

使用 var_not_used_in_aexp，形式化并证明正确版本的 subst_equiv_property。

练习：3 星, standard (inequiv_exercise)

证明无限循环不等价于 SKIP

扩展练习：非确定性 Imp

正如之前所见（Imp 一章中的 ceval_deterministic），Imp 的求值关系是确定性的。然而在一些实际的编程语言定义中，'非确定性' 也是十分重要的一部分。例如，在很多指令式语言中（如 C 系的语言）， 函数参数的求值顺序是未指定的。程序片段
      x = 0;;
      f(++x, x)

调用 f 时所用的参数可能是 (1, 0) 或者 (1, 1)，取决于编译器的选择。 这可能会让程序员感到困惑，但给了编译器作者选择实现的自由。 在此练习中，我们会用一个简单的非确定性指令来扩展 Imp， 研究这种改变会对程序等价关系产生何种影响。新指令的语法为 HAVOC X， 其中 X 是一个标识符。执行 HAVOC X 会为变量 X 赋予一个不确定的 '任意' 数值。例如，在执行完程序
      HAVOC Y;;
      Z ::= Y × 2

后，Y 的值可以是任何数，而 Z 的值是 Y 的两倍（因此 Z 总是偶数）。 注意，我们并未讨论输出值的'概率'，在执行完此非确定性代码后， 会有无穷多可能的不同输出。 某种意义上来说，HAVOC 所作用的变量大致相当于 C 之类的低级语言中的 未初始化变量。经过了 HAVOC 的变量会保存一个固定但任意的数值。 语言定义中的大部分非确定性来源于程序员对语言所做的选择不那么关心 （好处是能让编译器选择更快的运行方式）。 我们称这个心语言为'Himp'（“用 HAVOC 扩展的 Imp”）。

为了形式化 Himp，我们首先在指令定义中增加一条从句。

练习：2 星, standard (himp_ceval)

现在，我们必须扩展操作语义。前面我们已经提过了 ceval 关系的模版， 指定了大步语义。为了形式化 HAVOC 指令的行为，我们还需要在 ceval 的定义中添加哪些规则？

作为合理性检查，以下断言对于你的定义来说应该是可证的：

最后，我们重新定义和之前等价的指令：

我们应用此定义来证明一些非确定性程序是否等价。

练习：3 星, standard (havoc_swap)

以下两个程序是否等价？

请证明你的想法。

练习：4 星, standard, optional (havoc_copy)

以下两个程序是否等价？

请证明你的想法。（提示：你可能会用到 assert 的略。）

我们在这里使用的程序等价关系的定义对无限循环的程序来说有点复杂。因为 cequiv 描述的是两个等价的程序在'停机'时输出的集合是相同的。然而， 在像 Himp 这类带有非确定的语言中，有些程序总会停机，有些程序总会发散， 还有些程序会非确定地在某些时候停机而在其它时候发散。 以下练习的最后一部分展示了这种现象。

练习：4 星, advanced (p1_p2_term)

考虑一下指令：

直觉上来说，p₁ 和 p₂ 的停机行为相同：要么无限循环，要么以相同的状态开始， 就在相同的状态下停机。我们可以用以下引理分别刻画 p₁ 和 p₂ 的停机行为：

练习：4 星, advanced (p1_p2_equiv)

使用这两个引理来证明 p₁ 和 p₂ 确实等价。

练习：4 星, advanced (p3_p4_inequiv)

证明以下程序'不等价'（提示：当 p₃ 停机时 Z 的值是什么？当 p₄ 停机时呢？）

练习：5 星, advanced, optional (p5_p6_equiv)

证明以下指令等价。（提示：正如我们之前提到的，我们为 Himp 定义的 cequiv 只考虑了可能的停机配置的集合：对于两个拥有相同起始状态 st 的程序而言，当且仅当二者可能的停机状态的集合相同时，二者才等价。 若 p₅ 停机，那么最终状态应当是什么？反过来说，p₅ 总是会停机吗？）

附加练习

练习：4 星, standard, optional (for_while_equiv)

此练习是 Imp 一章中可选练习 add_for_loop 的扩展， 就是那个让你扩展出类似 C 风格的 for 循环指令的练习。请证明指令：
      for (c₁ ; b ; c₂) {
          c₃
      }

等价于：
       c₁ ;
       WHILE b DO
         c₃ ;
         c₂
       END

练习：3 星, standard, optional (swap_noninterfering_assignments)

（提示：这里你需要 functional_extensionality。）