案例分析证明 Proof by Case Analysis

中止 Abort

当然，并不是所有的东西都能通过简单的计算和重写来证明：一般来说，未知的假设值（任意数字、布尔值、列表等）可以阻止简化。例如，如果我们试图用上面的 simpl 策略来证明以下事实，我们就会陷入困境。（然后，我们使用 Abort 命令暂时放弃它。）

Theorem plus_1_neq_0_firsttry

Theorem plus_1_neq_0_firsttry : forall n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros n.
  simpl.  (* does nothing! *)
Abort.

原因是 eqb 和 + 的定义都是从第一个参数上执行 match 开始的。但在这里，第一个参数到 + 是未知数字 n 和 eqb 的参数是复合表示 n + 1 ;两者都不能简化。

Proof.

1 subgoal
______________________________________(1/1)
forall n : nat, (n + 1 =? 0) = false

intros n.

1 subgoal
n : nat
______________________________________(1/1)
(n + 1 =? 0) = false

析构 Destruct

为了取得进展，我们需要单独考虑可能的 n 形式。如果 n 是 O ，那么我们可以计算 (n + 1) =? 0 的最终结果，并检查它是否确实是 false 的。如果对某个 n' 有 n = S n'，那么，虽然我们不知道 n + 1 的确切代表什么，但我们可以计算，至少，它将从一个S开始，这足以再次计算某个 (n + 1) =? 0 将产生虚假的。

告诉 Coq 分别考虑 n = O和 n = S n' 称为 destruct 的案例的策略。

Theorem plus_1_neq_0

Theorem plus_1_neq_0 : forall n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros n. destruct n as [| n'] eqn:E.
  - simpl. reflexivity.
  - simpl. reflexivity.   Qed.

destruct n as [| n'] eqn:E.

2 subgoals
n : nat
E : n = 0
______________________________________(1/2)
(0 + 1 =? 0) = false
______________________________________(2/2)
(S n' + 1 =? 0) = false

-

1 subgoal
n : nat
E : n = 0
______________________________________(1/1)
(0 + 1 =? 0) = false

simpl.

1 subgoal
n : nat
E : n = 0
______________________________________(1/1)
false = false

reflexivity.

This subproof is complete, but there are some unfocused goals:

______________________________________(1/1)
(S n' + 1 =? 0) = false

-

1 subgoal
n, n' : nat
E : n = S n'
______________________________________(1/1)
(S n' + 1 =? 0) = false

simpl.

1 subgoal
n, n' : nat
E : n = S n'
______________________________________(1/1)
false = false

析构函数生成两个子目标，然后我们必须分别证明这两个子目标，以使Coq接受该定理。

intro 模式 as[|n']

注释“as[|n']”称为 intro 模式。它告诉Coq在每个子目标中引入哪些变量名。一般来说，方括号之间是一个名称列表，用|分隔。在本例中，第一个组件是空的，因为O构造函数是空的（它没有任何参数）。第二个组件给出了一个名称 n'，因为 S 是一元构造函数。

eqn:E 注释

在每个子目标中，Coq 记住与该子目标相关的关于 n 的假设——对于某些 n，n = 0 或 n = s n'。eqn:E注释告诉destruct给这个方程命名为E。省略eqn:E注释会导致Coq在子目标中省略这些假设。这稍微简化了没有明确使用假设的证明，但是为了文档的目的保留它们是更好的做法，因为它们可以帮助您在处理子目标时保持方向性。

- 符号 bullets

第二行和第三行上的-符号称为项目符号，它们标记了与生成的两个子目标相对应的证明部分。 - 后面的证明脚本部分是对应子目标的完整证明。在这个例子中，每个子目标都很容易通过一次使用自反性来证明，自反性本身执行一些简化——例如，第二个通过先将（s n'+1）重写为S（n'+1），然后展开eqb简化了（s n'+1）=？0 到 false。

用项目符号标记案例是可选的：如果项目符号不存在，Coq只要求您按顺序证明每个子目标，一次一个。但使用项目符号是个好主意。一方面，它们使证明的结构更加明显，提高了可读性。此外，项目符号指示Coq在尝试验证下一个子目标之前确保子目标已完成，以防止不同子目标的证明混淆。这些问题在大型开发中变得尤为重要，因为脆弱的证明会导致长时间的调试会话。

对于如何在Coq中格式化校样，并没有硬性规定——例如，在哪里应该断行，以及校样的各个部分应该如何缩进以指示其嵌套结构。但是，如果生成多个子目标的位置在行的开头用明确的项目符号标记，那么无论对布局的其他方面做了什么选择，证明都是可读的。

这也是一个很好的地方来提及另一条关于线路长度的明显建议。刚开始使用Coq的用户有时会走向极端，要么在自己的一行上写下每种策略，要么在一行上写下整个证明。好的风格就在中间。一个合理的准则是将自己限制在80个字符的行内。

destruct 策略可以用于任何归纳定义的数据类型。例如，我们接下来用它来证明布尔否定是对合的——也就是说，否定是它自己的逆。

Theorem negb_involutive

Theorem negb_involutive : forall b : bool,
  negb (negb b) = b.
Proof.
  intros b. destruct b eqn:E.
  - reflexivity.
  - reflexivity.  Qed.

请注意，此处的 destruct 没有 as 子句，因为 destruct 的子类不需要绑定任何变量，因此无需指定任何名称。事实上，我们可以从任何 destruct 中省略 as 子句，Coq 将自动填写变量名。这通常被认为是糟糕的风格，因为 Coq 经常在留给自己的设备时做出令人困惑的名称选择。

有时在子目标内调用 destruct 是有用的，从而产生更多的证明义务。在这种情况下，我们使用不同类型的项目符号在不同的"级别"上标记目标。例如：

Theorem andb_commutative 项目符号

Theorem andb_commutative : forall b c, andb b c = andb c b.
Proof.
  intros b c. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
Qed.

对 reflexivity 的每一对调用都对应于在其正上方执行 destruct c 后生成的子目标。

除了 - 和 + ，我们还可以使用 ×（星号）或任何重复的项目符号（例如，-- 或 *** ）作为项目符号。我们也可以在花键中附上子证明：

Theorem andb_commutative' 花键

Theorem andb_commutative' : forall b c, andb b c = andb c b.
Proof.
  intros b c. destruct b eqn:Eb.
  { destruct c eqn:Ec.
    { reflexivity. }
    { reflexivity. } }
  { destruct c eqn:Ec.
    { reflexivity. }
    { reflexivity. } }
Qed.

由于大括号标记了证明的开始和结束，因此它们可用于多个子目标级别，如本示例所示。此外，大括号允许我们在多个级别上重复使用相同的项目符号作为证明。大括号、项目符号或两者的组合的选择纯粹是品味问题。

Theorem andb3_exchange 花键和项目符号的组合

Theorem andb3_exchange :
  forall b c d, andb (andb b c) d = andb (andb b d) c.
Proof.
  intros b c d. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
  - destruct c eqn:Ec.
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
Qed.

练习 Exercise

7: 2 stars, standard (andb_true_elim2)

证明以下声明，在使用 destruct 时用项目符号标记案例（和子案例）。提示：延迟引入假设，直到你有机会简化它。

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Proof.
intros b c . destruct b eqn:Eb.
  - destruct c eqn:Ec. 
    + intros A. reflexivity.
    + intros B. rewrite <- B. reflexivity.
  - destruct c eqn:Ec. 
    + intros C. reflexivity.
    + intros D. rewrite <- D. reflexivity.

  Qed.

Coq运行截图

8: 1 star, standard (zero_nbeq_plus_1)

最后的便利 Final Convenience

在结束这一章之前，让我们来提一下最后的便利。正如你可能已经注意到的，许多证据在介绍后立即对一个变量进行案例分析：

intros x y. destruct y as [|y] eqn:E.

此模式非常常见，Coq 为它提供了速记：在引入变量时，我们可以使用介绍模式而不是可变名称对变量进行案例分析。例如，下面是上述 plus_1_neq_0 定理的较短证明。（您还会注意到此速记的一个缺点：我们丢失了记录我们在每个子行中做出的假设的方程，我们以前从 eqn：E 注释中获得了该方程。

Theorem plus_1_neq_0'

Theorem plus_1_neq_0' : forall n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros [|n].
  - reflexivity.
  - reflexivity.  Qed.

intros [|n].

2 subgoals
______________________________________(1/2)
(0 + 1 =? 0) = false
______________________________________(2/2)
(S n + 1 =? 0) = false

-

1 subgoal
______________________________________(1/1)
(0 + 1 =? 0) = false

simpl.

1 subgoal
______________________________________(1/1)
false = false

Theorem andb_commutative''

如果没有需要名称的构造参数，我们可以只编写[]来获取案例分析。

Theorem andb_commutative'' :
  forall b c, andb b c = andb c b.
Proof.
  intros [] [].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

intros [] [].

4 subgoals
______________________________________(1/4)
true && true = true && true
______________________________________(2/4)
true && false = false && true
______________________________________(3/4)
false && true = true && false
______________________________________(4/4)
false && false = false && false

Coq题目

Theorem zero_nbeq_plus_1 : forall n : nat,
  0 =? (n + 1) = false.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Proof.
intros [].
  - reflexivity.
  - reflexivity.
Qed.

Coq运行截图