单独编译 Separate Compilation

在开始本章之前，我们需要从上一章中导入我们的所有定义：

From Coq Require Export String.

Fixpoint even (n:nat) : bool :=
  match n with
  | O        => true
  | S O      => false
  | S (S n') => even n'
  end.

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => leb n' m'
      end
  end.

归纳法证明 Proof by Induction

我们可以用自反性证明0是+左边的中性元素。但证明它也是右边的中性元素的证据。。。

Theorem add_0_r_firsttry : ∀ n:nat,
  n + 0 = n.

不能用同样简单的方法来做。仅仅应用自反性是行不通的，因为n+0中的n是一个任意的未知数，所以不能简化+定义中的匹配。

Proof.
  intros n.
  simpl. (* Does nothing! *)
Abort.

使用析构函数n进行案例推理并没有让我们走得更远：我们假设 n = 0 的案例分析分支可以顺利通过，但在 n = S n' 的分支中，对于某些n'我们会以完全相同的方式陷入困境。

Theorem add_0_r_secondtry : ∀ n:nat,
  n + 0 = n.
Proof.
  intros n. destruct n as [| n'] eqn:E.
  - (* n = 0 *)
    reflexivity. (* so far so good... *)
  - (* n = S n' *)
    simpl. (* ...but here we are stuck again *)
Abort.

我们可以使用析构函数n'更进一步，但是，因为n可以任意大，如果我们继续这样下去，我们永远不会得到所有的结果。

为了证明有关数字、列表和其他归纳定义集的有趣事实，我们通常需要一个更强大的推理原则：归纳。

回想一下（高中，离散数学课程等）自然数归纳的原理：如果P（n）是一个涉及自然数n的命题，我们想证明P对所有数字n都成立，我们可以这样推理：

• 证明P（O）成立；
• 证明，对于任何n'，如果P（n'）成立，那么P（S n'）也成立；
• 得出P（n）适用于所有n的结论。

在Coq中，步骤是相同的：我们从证明所有n的P（n）的目标开始，并将其分解为两个单独的子目标（通过应用归纳策略）：一个是我们必须显示P（O），另一个是我们必须显示P（n'）→ P（sn'）。下面是这个定理的工作原理：

Theorem add_0_r : ∀ n:nat, n + 0 = n.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *) reflexivity.
  - (* n = S n' *) simpl. rewrite → IHn'. reflexivity. Qed.

就像析构函数一样，归纳函数也需要一个as……子句，指定要在子目标中引入的变量的名称。由于有两个子目标，“as…”子句有两部分，由|分隔。（严格地说，我们可以省略as…子句，Coq将为我们选择名称。实际上，这是一个坏主意，因为Coq的自动选择往往令人困惑。）

在第一个子目标中，n被0替换。没有引入新变量（因此as…的第一部分为空），目标变为0=0+0，随后进行简化。

在第二个子目标中，n被sn'替换，假设n'+0=n'被添加到上下文中，并命名为IHn'（即，n'的归纳假设）。这两个名称在as。。。条款本例中的目标是sn'=（sn'）+0，这将简化为sn'=S（n'+0），然后再从IHn'开始。

Theorem minus_n_n : ∀ n,
  minus n n = 0.
Proof.
  (* WORKED IN CLASS *)
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *)
    simpl. reflexivity.
  - (* n = S n' *)
    simpl. rewrite → IHn'. reflexivity. Qed.

（在这些证明中使用介绍策略实际上是多余的。当应用于包含量化变量的目标时，归纳策略将根据需要自动将其移动到上下文中。）

14: 2 stars, standard, especially useful (basic_induction)

使用归纳法证明以下内容。您可能需要以前验证过的结果。

Theorem mul_0_r

Theorem mul_0_r : ∀ n:nat,
  n × 0 = 0.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem mul_0_r : forall n:nat,
n * 0 = 0.
Proof.
intros n. induction n as [| n' IHn'].
- (* n = 0 *)
  simpl. reflexivity.
- (* n = S n' *)
  simpl. rewrite -> IHn'. reflexivity.  Qed.

Theorem plus_n_Sm

Theorem plus_n_Sm : ∀ n m : nat,
S (n + m) = n + (S m).
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Theorem plus_n_Sm : forall n m : nat,
S (n + m) = n + (S m).
Proof.
intros n. induction n as [| n' IHn'].
- intros m. induction m as [| m' IHm'].
  -- simpl. reflexivity.
  -- simpl. reflexivity.
- intros m. induction m as [| m' IHm'].
  -- simpl. rewrite -> IHn'. reflexivity. 
  -- simpl. rewrite -> IHn'. reflexivity. Qed.

Theorem add_comm

Theorem add_comm : ∀ n m : nat,
n + m = m + n.
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Theorem add_comm : forall n m : nat,
n + m = m + n.
Proof.
induction n as [| n' IHn'].
- induction m as [| m' IHm'].
  -- simpl. reflexivity.
  -- simpl. rewrite <- IHm'. simpl. reflexivity.
- induction m as [| m' IHm']. 
  -- simpl. rewrite -> IHn'. simpl. reflexivity.
  -- simpl. rewrite <- IHm'. rewrite -> IHn'. simpl. rewrite -> IHn'. reflexivity.
Qed.

Theorem add_assoc

Theorem add_assoc : ∀ n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Theorem add_assoc : forall n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
induction n as [| n' IHn'].
- induction m as [| m' IHm'].
  -- induction p as [| p' IHp'].
  	--- simpl. reflexivity.
  	--- simpl. reflexivity.
  -- induction p as [| p' IHp'].
  	--- simpl. reflexivity.
  	--- simpl. reflexivity.
- induction m as [| m' IHm'].
  -- simpl. induction p as [| p' IHp'].
  	--- rewrite <- IHn'. simpl. reflexivity.
  	--- rewrite <- IHn'. simpl. reflexivity.
  -- simpl. induction p as [| p' IHp'].
  	--- rewrite <- IHn'. simpl. reflexivity.
  	--- rewrite <- IHn'. simpl. reflexivity.
Qed.

15: 2 stars, standard (double_plus)

考虑下面的函数，它的论点加倍：

Fixpoint double (n:nat) :=
match n with
| O ⇒ O
| S n' ⇒ S (S (double n'))
end.

使用归纳法来证明关于双重的这一简单事实：

Lemma double_plus : ∀ n, double n = n + n .
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Lemma double_plus : forall n, double n = n + n .
Proof.
intros. induction n as [| n' IHn'].
- simpl. reflexivity.
- simpl. rewrite -> IHn'. rewrite -> plus_n_Sm. reflexivity.
Qed.

16: 2 stars, standard, optional (even_S)

偶数n定义的一个不方便的方面是对n-2的递归调用。这使得关于n的证明在n上进行归纳时更加困难，因为我们可能需要一个关于n-2的归纳假设。下面的引理给出了偶数（sn）的另一种特征，这种特征在归纳法中效果更好：

Theorem even_S : ∀ n : nat,
even (S n) = negb (even n).
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Theorem even_S : forall n : nat,
even (S n) = negb (even n).
Proof.
intros. induction n as [| n' IHn'].
- simpl. reflexivity.
- rewrite -> IHn'. simpl. rewrite -> negb_involutive. reflexivity.
Qed.

17: 1 star, standard, optional (destruct_induction)

简要说明析构函数和归纳的区别。

(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_destruct_induction : option (nat×string) := None.