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

From Coq Require Export String.

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.

数对 Pairs of Numbers

在归纳类型定义中，每个构造函数可以接受任意数量的参数——无（如true和O）、一个（如S）或多个（如Nyble，此处）：

Inductive natprod

Inductive natprod : Type :=
  | pair (n1 n2 : nat).

该声明可以理解为：“构造一对数字的唯一方法是将构造函数对应用于nat类型的两个参数。”

Check (pair 3 5) : natprod.

下面是用于提取一对的第一和第二分量的简单函数。

Definition fst

Definition fst (p : natprod) : nat :=
  match p with
  | pair x y ⇒ x
  end.

Definition snd

Definition snd (p : natprod) : nat :=
match p with
| pair x y ⇒ y
end.
Compute (fst (pair 3 5)).
(* ===> 3 *)

由于在下面的内容中将大量使用对，因此能够使用标准数学符号（x，y）而不是 pair x y 来编写它们是很好的。我们可以告诉Coq允许使用符号声明。

Notation "( x , y )"

Notation "( x , y )" := (pair x y).

新符号既可以用于表达式，也可以用于模式匹配。

Compute (fst (3,5)).

Definition fst'

Definition fst' (p : natprod) : nat :=
  match p with
  | (x,y) ⇒ x
  end.

Definition snd'

Definition snd' (p : natprod) : nat :=
match p with
| (x,y) ⇒ y
end.

Definition swap_pair

Definition swap_pair (p : natprod) : natprod :=
match p with
| (x,y) ⇒ (y,x)
end.

请注意，配对上的模式匹配（带括号：（x，y））不能与我们前面看到的“多模式”语法（不带括号：x，y）混淆。上面的示例说明了对元素x和y的模式匹配，而例如，“基本”中的减号定义对值n和m执行模式匹配：

Fixpoint minus (n m : nat) : nat :=
       match n, m with
       | O   , _    ⇒ O
       | S _ , O    ⇒ n
       | S n', S m' ⇒ minus n' m'
       end.

区别很小，但值得知道的是，它们并不相同。例如，以下定义格式不正确：

Definition bad_fst

(* 一对多模式不能匹配： *)
       Definition bad_fst (p : natprod) : nat :=
         match p with
         | x, y ⇒ x
         end.

Definition bad_minus

        (* 无法匹配具有成对模式的多个值: *)
        Definition bad_minus (n m : nat) : nat :=
          match n, m with
          | (O   , _   ) ⇒ O
          | (S _ , O   ) ⇒ n
          | (S n', S m') ⇒ bad_minus n' m'
          end.

现在，让我们来证明一些关于配对的简单事实。

如果我们以一种稍微奇特的方式陈述对的性质，我们有时可以用自反性（及其内置的简化）来完成它们的证明：

Theorem surjective_pairing'

Theorem surjective_pairing' : ∀ (n m : nat),
  (n,m) = (fst (n,m), snd (n,m)).
Proof.
  reflexivity. Qed.

但是，如果我们以更自然的方式陈述引理，那么自反性是不够的：

Theorem surjective_pairing_stuck : ∀ (p : natprod),
  p = (fst p, snd p).
Proof.
  simpl. (* Doesn't reduce anything! *)
Abort.

相反，我们需要公开p的结构，以便siml可以在fst和snd中执行模式匹配。我们可以用析构函数来实现这一点。

Theorem surjective_pairing : ∀ (p : natprod),
  p = (fst p, snd p).
Proof.
  intros p. destruct p as [n m]. simpl. reflexivity. Qed.

请注意，与NAT的行为不同，它在NAT中生成两个子目标，而destruct在这里只生成一个子目标。这是因为natprods只能以一种方式构造。

26: 1 star, standard (snd_fst_is_swap)

Theorem snd_fst_is_swap : ∀ (p : natprod),
  (snd p, fst p) = swap_pair p.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem snd_fst_is_swap : forall (p : natprod),
(snd p, fst p) = swap_pair p.
Proof.
intros p. destruct p as [n m]. simpl. reflexivity. Qed.

27: 1 star, standard, optional (fst_swap_is_snd)

Theorem fst_swap_is_snd : ∀ (p : natprod),
  fst (swap_pair p) = snd p.
Proof.
  (* FILL IN HERE *) Admitted.

Coq代码

Theorem fst_swap_is_snd : forall (p : natprod),
fst (swap_pair p) = snd p.
Proof.
intros p. destruct p as [n m]. simpl. reflexivity. Qed.