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.
京公网安备 11010502036488号