Coq Automation

最后一个证明中重复的次数有点烦人。如果算术表达式的语言或被证明合理的优化明显更复杂，那么它将开始成为一个真正的问题。

到目前为止，我们所做的所有证明都只使用了Coq的一小部分策略，而完全忽略了它自动构造部分证明的强大功能。本节将介绍其中的一些设施，我们将在接下来的几章中看到更多内容。习惯它们需要一些精力——Coq的自动化是一个强有力的工具——但它将允许我们扩大我们的工作范围，以获得更复杂的定义和更有趣的属性，而不会被无聊、重复、低级的细节所淹没。

Tacticals

战术是Coq对以其他战术为论据的战术的术语——“高阶战术”，如果你愿意的话。

The try Tactical

如果T是一种策略，那么try T是一种与T类似的策略，只是如果T失败，try T成功地什么都不做（而不是失败）。

Theorem silly1 : forall ae, aeval ae = aeval ae.
Proof. try reflexivity. //这就是反射性。
Qed.

Theorem silly2 : forall (P : Prop), P -> P.
Proof.
  intros P HP.
  try reflexivity. //仅仅是自反性就会失败。
  apply HP.//我们仍然可以用其他方式完成证明。
Qed.

并没有真正的理由在像这样的完全手工校对中使用try，但它对于结合自动化校对是非常有用的；战术，我们接下来展示。

The ; Tactical (Simple Form)

最常见的形式是；战术以两种战术作为论据。复合战术T；T'首先执行T，然后对T生成的每个子目标执行T'。

例如，考虑下面的微不足道引理：

Lemma foo : forall n, 0 <=? n = true.
Proof.
  intros.
  destruct n.
    (* Leaves two subgoals, which are discharged identically...  *)
    - (* n=0 *) simpl. reflexivity.
    - (* n=Sn' *) simpl. reflexivity.
Qed.

我们可以使用；策略简化此证明：

Lemma foo' : forall n, 0 <=? n = true.
Proof.
  intros.
  (* [destruct] the current goal *)
  destruct n;
  (* then [simpl] each resulting subgoal *)
  simpl;
  (* and do [reflexivity] on each resulting subgoal *)
  reflexivity.
Qed.

同时使用try和;，我们可以消除刚才困扰我们的证明中的重复。

Theorem optimize_0plus_sound': forall a,
  aeval (optimize_0plus a) = aeval a.
Proof.
  intros a.
  induction a;
    (* Most cases follow directly by the IH... *)
    try (simpl; rewrite IHa1; rewrite IHa2; reflexivity).
    (* ... but the remaining cases -- ANum and APlus --
       are different: *)
  - (* ANum *) reflexivity.
  - (* APlus *)
    destruct a1 eqn:Ea1;
      (* Again, most cases follow directly by the IH: *)
      try (simpl; simpl in IHa1; rewrite IHa1;
           rewrite IHa2; reflexivity).
    (* The interesting case, on which the [try...]
       does nothing, is when [e1 = ANum n]. In this
       case, we have to destruct [n] (to see whether
       the optimization applies) and rewrite with the
       induction hypothesis. *)
    + (* a1 = ANum n *) destruct n eqn:En;
      simpl; rewrite IHa2; reflexivity.   Qed.

Coq专家经常使用这个“……;try……”成语经过一个像归纳法这样的策略，一次处理了许多类似的情况。当然，这种做法在非正式的证明中也有相似之处。例如，下面是优化定理的非正式证明，它与正式定理的结构相匹配：

_Theorem_: For all arithmetic expressions [a],

       aeval (optimize_0plus a) = aeval a.

    _Proof_: By induction on [a].  Most cases follow directly from the
    IH.  The remaining cases are as follows:

      - Suppose [a = ANum n] for some [n].  We must show

          aeval (optimize_0plus (ANum n)) = aeval (ANum n).

        This is immediate from the definition of [optimize_0plus].

      - Suppose [a = APlus a1 a2] for some [a1] and [a2].  We must
        show

          aeval (optimize_0plus (APlus a1 a2)) = aeval (APlus a1 a2).

        Consider the possible forms of [a1].  For most of them,
        [optimize_0plus] simply calls itself recursively for the
        subexpressions and rebuilds a new expression of the same form
        as [a1]; in these cases, the result follows directly from the
        IH.

        The interesting case is when [a1 = ANum n] for some [n].  If
        [n = 0], then

          optimize_0plus (APlus a1 a2) = optimize_0plus a2

        and the IH for [a2] is exactly what we need.  On the other
        hand, if [n = S n'] for some [n'], then again [optimize_0plus]
        simply calls itself recursively, and the result follows from
        the IH. 

然而，这一证明仍然可以改进：第一个案例（对于a=ANum n）非常琐碎——甚至比我们所说的简单地遵循IH的案例更琐碎——但我们选择将其全部写出来。最好是把它放下，在最上面说，“大多数案件要么是直接的，要么是来自IH的。唯一有趣的案件是APlus的案件……”我们也可以在形式证明上做同样的改进。下面是它的外观：

Theorem optimize_0plus_sound'': forall a,
  aeval (optimize_0plus a) = aeval a.
Proof.
  intros a.
  induction a;
    (* Most cases follow directly by the IH *)
    try (simpl; rewrite IHa1; rewrite IHa2; reflexivity);
    (* ... or are immediate by definition *)
    try reflexivity.
  (* The interesting case is when a = APlus a1 a2. *)
  - (* APlus *)
    destruct a1; try (simpl; simpl in IHa1; rewrite IHa1;
                      rewrite IHa2; reflexivity).
    + (* a1 = ANum n *) destruct n;
      simpl; rewrite IHa2; reflexivity. Qed.

The ; Tactical (General Form)

这个战术也有比简单T更一般的形式；我们已经在上面看到了。如果T，T1。。。，Tn是战术，然后是T；[T1 | T2 |…| Tn]是一种策略，首先执行T，然后对T生成的第一个子目标执行T1，对第二个子目标执行T2，等等。

所以T；T’只是所有Ti都是相同策略时的特殊符号；i、 e，T；T’是：T的简写；[T'| T'|…| T']

The repeat Tactical

重复战术采用另一种战术，并持续应用该战术，直到无法取得进展。下面是一个示例，使用repeat显示10在一个长列表中。

Theorem In10

Theorem In10 : In 10 [1;2;3;4;5;6;7;8;9;10].
Proof.
  repeat (try (left; reflexivity); right).
Qed.

战术重复T从不失败：如果战术T不适用于原始目标，那么重复仍然成功，而不改变原始目标（即重复零次）。

Theorem In10' : In 10 [1;2;3;4;5;6;7;8;9;10].
Proof.
  repeat simpl.
  repeat (left; reflexivity).
  repeat (right; try (left; reflexivity)).
Qed.

战术重复T也没有应用T次数的上限。如果T是一个总是成功（并取得进展）的战术，那么重复T将永远循环。

Theorem repeat_loop

Theorem repeat_loop : forall (m n : nat),
  m + n = n + m.
Proof.
  intros m n.
  (* Uncomment the next line to see the infinite loop occur.
     In Proof General, [C-c C-c] will break out of the loop. *)
  (* repeat rewrite Nat.add_comm. *)
Admitted.

虽然Coq术语语言Gallina的评估保证终止，但战术评估不终止！然而，这并不影响Coq的逻辑一致性，因为重复和其他策略的工作是指导Coq构造证明；如果构建过程出现分歧（即，它没有终止），这仅仅意味着我们没有构建证据，而不是我们构建了错误的证据。

Exercise: 3 stars, standard (optimize_0plus_b_sound)

由于optimize_0plus转换不会更改aexps的值，因此我们应该能够将其应用于bexp中出现的所有aexps，而无需更改bexp的值。编写一个在bexps上执行此转换的函数，并证明它是正确的。使用我们刚刚看到的战术，使证据尽可能优雅。

Fixpoint optimize_0plus_b (b : bexp) : bexp
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Theorem optimize_0plus_b_sound : forall b,
  beval (optimize_0plus_b b) = beval b.
Proof.
  (* FILL IN HERE *) Admitted.

Fixpoint optimize_0plus_b (b : bexp) : bexp

Fixpoint optimize_0plus_b (b : bexp) : bexp :=
  match b with
  | BEq l r => BEq (optimize_0plus l) (optimize_0plus r)
  | BLe l r => BLe (optimize_0plus l) (optimize_0plus r)
  | BNot b' => BNot (optimize_0plus_b b')
  | BAnd l r => BAnd (optimize_0plus_b l) (optimize_0plus_b r)
  | _ => b
  end.

Theorem optimize_0plus_b_sound

Theorem optimize_0plus_b_sound : forall b,
  beval (optimize_0plus_b b) = beval b.
Proof.
  intros.
  induction b;
    try (simpl; reflexivity);
    try (simpl; repeat rewrite optimize_0plus_sound; reflexivity).
  - simpl. rewrite IHb. reflexivity.
  - simpl. rewrite IHb1. rewrite IHb2. reflexivity.
Qed.