Using Evidence in Proofs

除了构建数字是偶数的证据外，我们还可以破坏这些证据，这相当于对如何构建数字的推理。

引入带有归纳声明的ev不仅告诉Coq构造函数ev_0和ev_SS是证明某个数字是ev的有效方法，而且这两个构造函数是证明数字是ev的唯一方法。

换句话说，如果有人给我们证据E来证明ev n，那么我们知道E必须是两件事之一：

• E是ev_0（n是O），或

• E是ev_SS n'E'（n是S（sn'），其中E'是ev n'的证据）。

这表明，应该可以像分析归纳定义的数据结构一样，分析ev n形式的假设；特别是，应该能够通过归纳和案例分析对这些证据进行论证。让我们看几个例子，看看这在实践中意味着什么。

Inversion on Evidence 证据倒置

假设我们正在证明一个涉及数字n的事实，并且我们给出了ev n作为一个假设。我们已经知道如何使用析构函数或归纳法对n进行案例分析，为n=O的案例和n=sn'的案例生成单独的子目标。但对于一些证据，我们可能需要直接分析ev n的证据。作为一种工具，我们可以使用析构函数来证明我们对ev n证据的描述。

Theorem ev_inversion

Theorem ev_inversion :
  forall (n : nat), ev n ->
    (n = 0) \/ (exists n', n = S (S n') /\ ev n').
Proof.
  intros n E.
  destruct E as [ | n' E'] eqn:EE.
  - (* E = ev_0 : ev 0 *)
    left. reflexivity.
  - (* E = ev_SS n' E' : ev (S (S n')) *)
    right. exists n'. split. reflexivity. apply E'.
Qed.

像这样的事实通常被称为“反转引理”，因为它们允许我们“反转”一些给定的信息，从而对所有不同的推导方法进行推理。

这里，有两种方法可以证明一个数是ev，反演引理使这一点变得明确。

下面的定理可以很容易地用证据的析构函数来证明。

Theorem ev_minus2

Theorem ev_minus2 : forall n,
  ev n -> ev (pred (pred n)).
Proof.
  intros n E.
  destruct E as [| n' E'] eqn:EE.
  - (* E = ev_0 *) simpl. apply ev_0.
  - (* E = ev_SS n' E' *) simpl. apply E'.
Qed.

然而，仅使用析构函数无法轻松处理这种变化。

Theorem evSS_ev

Theorem evSS_ev : forall n,
  ev (S (S n)) -> ev n.

直觉上，我们知道假设的证据不能仅仅由ev_0构造器组成，因为O和S是nat类型的不同构造器；因此，ev_SS是唯一适用的情况。不幸的是，destruct不够聪明，无法实现这一点，它仍然会生成两个子目标。更糟糕的是，这样做，它保持了最终目标不变，没有提供任何有用的信息来完成证明。

Proof.
  intros n E.
  destruct E as [| n' E'] eqn:EE.
  - (* E = ev_0. *)
    (* We must prove that [n] is even from no assumptions! *)
Abort.

到底发生了什么事？调用析构函数的效果是用对应于每个构造函数的值替换所有出现的属性参数。这在ev_minus 2的情况下就足够了，因为在最终目标中直接提到了参数n。然而，这对evSS_ev没有帮助，因为被替换的术语（S（S n））在任何地方都没有提及。

如果我们还记得S（S n）这个词，证明就通过了。（我们将在下面更详细地讨论记住。）

Theorem evSS_ev_remember

Theorem evSS_ev_remember : forall n,
  ev (S (S n)) -> ev n.
Proof.
  intros n E. remember (S (S n)) as k eqn:Hk.
  destruct E as [|n' E'] eqn:EE.
  - (* E = ev_0 *)
    (* Now we do have an assumption, in which [k = S (S n)] has been
       rewritten as [0 = S (S n)] by [destruct]. That assumption
       gives us a contradiction. *)
    discriminate Hk.
  - (* E = ev_S n' E' *)
    (* This time [k = S (S n)] has been rewritten as [S (S n') = S (S n)]. *)
    injection Hk as Heq. rewrite <- Heq. apply E'.
Qed.

或者，使用我们上面证明的反演引理，证明是简单的。

Theorem evSS_ev

Theorem evSS_ev : forall n, ev (S (S n)) -> ev n.
Proof.
  intros n H. apply ev_inversion in H.
  destruct H as [H0|H1].
  - discriminate H0.
  - destruct H1 as [n' [Hnm Hev]]. injection Hnm as Heq.
    rewrite Heq. apply Hev.
Qed.

注意两种证明如何产生两个子目标，这两个子目标对应于证明ev的两种方法。第一个子目标是一个带有歧视性的矛盾。第二个子目标使用注入和重写。Coq提供了一种称为反转（inversion）的简便策略，可以将常见模式排除在外。

反转策略可以检测（1）第一种情况（n=0）不适用，（2）ev_SS情况中出现的n'必须与n相同。它有一个类似于析构函数的“as”变量，允许我们分配名称，而不是让Coq选择名称。

Theorem evSS_ev' : forall n,
  ev (S (S n)) -> ev n.
Proof.
  intros n E.
  inversion E as [| n' E' Heq].
  (* We are in the [E = ev_SS n' E'] case now. *)
  apply E'.
Qed.

反演策略可以将爆炸原理应用于涉及归纳定义属性的“明显矛盾”假设，这需要使用我们的反演引理做更多的工作。例如：

Theorem one_not_even

Theorem one_not_even : ~ ev 1.
Proof.
  intros H. apply ev_inversion in H.
  destruct H as [ | [m [Hm _]]].
    - discriminate H.
  - discriminate Hm.
Qed.

Theorem one_not_even' : ~ ev 1.
Proof.
  intros H.
  inversion H. 
Qed.

Exercise: 1 star, standard (inversion_practice)

用反演方法证明以下结果。（为了进行额外的练习，您还可以使用反转引理来证明它。）

Theorem SSSSev__even : forall n,
  ev (S (S (S (S n)))) -> ev n.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem SSSSev__even

Theorem SSSSev__even : forall n,
  ev (S (S (S (S n)))) -> ev n.
Proof.
 intros.
 inversion H.
 apply evSS_ev' in H1.
 apply H1.
Qed.

Exercise: 1 star, standard (ev5_nonsense)

用反演方法证明以下结果。

Theorem ev5_nonsense :
  ev 5 -> 2 + 2 = 9.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem ev5_nonsense

Theorem ev5_nonsense :
  ev 5 -> 2 + 2 = 9.
Proof.
 intros.
 inversion H.
 inversion H1.
 inversion H3.
Qed.

反转策略做了很多工作。例如，当应用于一个等式假设时，它同时进行判别和注入。此外，它还执行注入时通常需要的介绍和重写。它还可以更普遍地用于分析归纳定义命题的证据。作为例子，我们将用它来重新证明战术一章中的一些定理。（在这里，我们有点懒惰，因为我们在反转中省略了as子句，从而要求Coq为它引入的变量和假设选择名称。）

Theorem inversion_ex1

Theorem inversion_ex1 : forall (n m o : nat),
  [n; m] = [o; o] ->
  [n] = [m].
Proof.
  intros n m o H. inversion H. reflexivity. Qed.

Theorem inversion_ex2

Theorem inversion_ex2 : forall (n : nat),
  S n = O ->
  2 + 2 = 5.
Proof.
  intros n contra. inversion contra. Qed.

下面是反转一般的工作原理。假设名称H指的是当前上下文中的假设P，其中P由归纳声明定义。然后，对于P的每个构造器，反演H生成一个子目标，其中H已被该构造器可用于证明P的确切特定条件所取代。其中一些子目标将自相矛盾；反转会把这些扔掉。剩下的例子代表了必须证明的案例，以确立最初的目标。对于这些，反演将所有方程添加到证明上下文中，该证明上下文必须包含给定给P的参数（例如，在evSS_ev的证明中S（S n'）=n）。

上面的ev_double练习表明，我们对均匀性的新概念是由前面的两个概念所暗示的（因为，通过《逻辑》一章中的偶数bool_道具，我们已经知道它们是等价的）。为了证明这三者是一致的，我们只需要下面的引理。

Lemma ev_Even_firsttry : forall n,
  ev n -> Even n.
Proof.
  (* WORKED IN CLASS *)
  unfold Even.

我们可以尝试通过案例分析或归纳法对n进行分析。但由于ev是在一个前提中提到的，因此这种策略可能会导致一条死胡同，因为（正如我们之前所指出的）归纳法假设将讨论n-1（这不是偶数！）。因此，似乎最好先根据ev的证据尝试反转。事实上，第一个案例可以简单地解决。我们似乎可以在第二种情况下用辅助引理取得进展。

  intros n E. inversion E as [EQ' | n' E' EQ'].
  - (* E = ev_0 *)
    exists 0. reflexivity.
  - (* E = ev_SS n' E' *)

不幸的是，第二种情况更难。我们需要展示∃ n0，S（sn'）=double n0，但唯一可用的假设是E'，表示ev n'保持不变。因为这不是直接有用的，所以我们似乎陷入了困境，在E上执行案例分析是浪费时间。

然而，如果我们更仔细地观察我们的第二个目标，我们可以看到发生了一些有趣的事情：通过对E进行案例分析，我们能够将原始结果简化为一个类似的结果，其中涉及到ev的不同证据：即E’。更正式地说，我们可以通过证明∃ k'，n'=double k'，

这与原始陈述相同，但用n'代替n。事实上，不难让Coq相信这个中间结果就足够了。

    assert (H: (exists k', n' = double k') -> (exists n0, S (S n') = double n0)).
    { intros [k' EQ'']. exists (S k'). simpl. rewrite <- EQ''. reflexivity. }
    apply H.

不幸的是，现在我们陷入了困境。为了说明这一点，让我们从假设中回到目标。

generalize dependent E'.

现在很明显，我们正试图证明我们开始证明的同一个定理的另一个例子。此实例使用n'，而不是n，其中n'是比n小的自然数。

Abort.

Induction on Evidence 证据归纳法

如果这看起来很熟悉，那也不是巧合：我们在归纳一章中遇到了类似的问题，当时我们试图使用案例分析来证明需要归纳的结果。再一次，解决办法是。。。就职

对证据的归纳行为与对数据的归纳行为相同：它使Coq为可能用于构建该证据的每个构造函数生成一个子目标，同时为相关属性的每次递归出现提供归纳假设。

为了证明所有数的n保持性，我们可以对ev n使用归纳法。这要求我们证明两件事，对应于ev n的两种构造方式。如果它是由ev_0构造的，则n=0，并且该属性必须保持0。如果它是由ev_SS构造的，那么ev n的证据的形式为ev_SS n'E'，其中n=S（sn'），E'是ev n'的证据。在这种情况下，归纳假设说，我们试图证明的性质对n'成立。

让我们再次尝试当前引理：

Lemma ev_Even

Lemma ev_Even : forall n,
  ev n -> Even n.
Proof.
  intros n E.
  induction E as [|n' E' IH].
  - (* E = ev_0 *)
    unfold Even. exists 0. reflexivity.
  - (* E = ev_SS n' E'
       with IH : Even E' *)
    unfold Even in IH.
    destruct IH as [k Hk].
    rewrite Hk.
    unfold Even. exists (S k). simpl. reflexivity.
Qed.

在这里，我们可以看到Coq产生了一个IH，对应于E'，在其自身定义中ev的单一递归出现。由于E'提到n'，归纳假设谈论的是n'，而不是n或其他数字。

现在，均匀度的第二个和第三个定义是等价的。

Theorem ev_Even_iff

Theorem ev_Even_iff : forall n,
  ev n <-> Even n.
Proof.
  intros n. split.
  - (* -> *) apply ev_Even.
  - (* <- *) unfold Even. intros [k Hk]. rewrite Hk. apply ev_double.
Qed.

正如我们将在后面的章节中看到的，证据归纳是一种在许多领域反复出现的技术，特别是在形式化编程语言的语义时，其中许多感兴趣的属性都是归纳式定义的。

以下练习提供了此技巧的简单示例，以帮助您熟悉它。

Exercise: 2 stars, standard (ev_sum)

Theorem ev_sum : forall n m, ev n -> ev m -> ev (n + m).
Proof.
  (* FILL IN HERE *) Admitted.

Theorem ev_sum

Theorem ev_sum : forall n m, ev n -> ev m -> ev (n + m).
Proof.
intros.
induction H as [|n' H' IH].
- simpl. apply H0.
- simpl. apply ev_SS. apply IH.
Qed.

Exercise: 4 stars, advanced, optional (ev'_ev)

一般来说，归纳式定义属性可能有多种方式。例如，以下是ev的一个（稍微做作的）替代定义：

Inductive ev' : nat -> Prop :=
  | ev'_0 : ev' 0
  | ev'_2 : ev' 2
  | ev'_sum n m (Hn : ev' n) (Hm : ev' m) : ev' (n + m).

证明此定义在逻辑上与旧定义等价。为了简化证明，请使用将定理应用于参数的技术（从逻辑上），并注意同样的技术适用于归纳定义命题的构造函数。

Theorem ev'_ev : forall n, ev' n <-> ev n.
Proof.
 (* FILL IN HERE *) Admitted.

Exercise: 3 stars, advanced, especially useful (ev_ev__ev)

这里有两条证据你可以尝试归纳。如果一个不行，试试另一个。

Theorem ev_ev__ev : forall n m,
  ev (n+m) -> ev n -> ev m.
Proof.
  (* FILL IN HERE *) Admitted.

Exercise: 3 stars, standard, optional (ev_plus_plus)

此练习可以在不进行归纳或案例分析的情况下完成。但是，您需要一个聪明的断言和一些乏味的重写。提示：（n+m）+（n+p）是偶数吗？

Theorem ev_plus_plus : forall n m p,
  ev (n+m) -> ev (n+p) -> ev (m+p).
Proof.
  (* FILL IN HERE *) Admitted.