本章介绍了几个额外的证明策略和策略，使我们能够开始证明函数程序更有趣的属性。

我们将看到：

  • 如何在“向前”和“向后”证明中使用辅助引理；
  • 如何对数据构造函数进行推理——特别是如何利用它们是内射的和不相交的事实；
  • 如何强化归纳假设，以及何时需要强化；和
  • 关于如何通过案例分析进行推理的更多详细信息。

应用策略 The apply Tactic

我们经常遇到这样的情况，即需要证明的目标与上下文中的某个假设或之前证明的引理完全相同。

Theorem silly1 : forall (n m : nat),
  n = m ->
  n = m.
Proof.
  intros n m eq.
  //在这里，我们可以用“重写”来结束→ 正如我们以前多次做的那样。或者，我们可以使用应用策略在一个步骤中完成：
  apply eq.  Qed.

应用策略也适用于条件假设和引理：如果应用的语句是一个蕴涵，那么这个蕴涵的前提将被添加到需要证明的子目标列表中。

Theorem silly2 : forall (n m o p : nat),
  n = m ->
  (n = m -> [n;o] = [m;p]) ->
  [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  apply eq2. apply eq1.  Qed.

通常，当我们使用apply H时，语句H将以∀ 这引入了一些普遍量化的变量。当Coq与当前目标和H的结论相匹配时，它将尝试为这些变量找到合适的值。例如，当我们在下面的证明中应用eq2时，eq2中的通用变量q用n实例化，r用m实例化。

Theorem silly2a : forall (n m : nat),
  (n,n) = (m,m)  ->
  (forall (q r : nat), (q,q) = (r,r) -> [q] = [r]) ->
  [n] = [m].
Proof.
  intros n m eq1 eq2.
  apply eq2. apply eq1.  Qed.

要使用apply策略，所应用的（结论）事实必须与目标完全匹配——例如，如果等式的左右两边被交换，apply将不起作用。

Theorem silly3 : forall (n m : nat),
  n = m ->
  m = n.
Proof.
  intros n m H.
  //这里我们不能直接使用apply。。。
  Fail apply H.
  //但我们可以使用对称策略，在目标中切换相等的左右两侧。
  symmetry. apply H. Qed.

练习 Exercise

65: 2 stars, standard, optional (silly_ex)

仅使用介绍和应用完成以下证明。

Theorem silly_ex : forall p,
  (forall n, even n = true -> even (S n) = false) ->
  (forall n, even n = false -> odd n = true) ->
  even p = true ->
  odd (S p) = true.
Proof. (* FILL IN HERE *) Admitted.
Solution
Theorem silly_ex : forall p,
  (forall n, even n = true -> even (S n) = false) ->
  (forall n, even n = false -> odd n = true) ->
  even p = true ->
  odd (S p) = true.
Proof.
 intros.  apply H0. apply H. apply H1.
Qed.

66: 3 stars, standard (apply_exercise1)

提示：您还可以将apply用于先前定义的引理，而不仅仅是上下文中的假设。你可能会发现早期的引理如app_nil_r、app_assoc、rev_app_distr、rev_involutive等都很有用。另外，记住搜索是你的朋友（尽管如果它们是可选问题，而你选择不完成证明，它可能找不到早期的引理）。

Theorem rev_exercise1 : forall (l l' : list nat),
  l = rev l' ->
  l' = rev l.
Proof.
  (* FILL IN HERE *) Admitted.
Solution
Theorem rev_exercise1 : forall (l l' : list nat),
  l = rev l' ->
  l' = rev l.
Proof.
  intros.
  rewrite -> H.
  symmetry.
  apply rev_involutive.
Qed.

67: 1 star, standard, optional (apply_rewrite)

简要说明应用和重写策略之间的区别。在什么情况下两者都可以有效地应用？

(* FILL IN HERE *)
Solution