证明中的证明 Proofs Within Proofs

在Coq中,就像在非正式数学中一样,大的证明常常被分解成一系列定理,后面的证明引用了前面的定理。但有时,一个证明将需要一些杂七杂八的事实,这些事实太琐碎,也没有太多的普遍兴趣,以至于懒得给它起自己的顶级名称。在这种情况下,可以方便地在使用“子定理”的地方简单地陈述和证明所需的“子定理”。断言策略允许我们这样做。

Theorem mult_0_plus' : ∀ n m : nat,
  (0 + n) × m = n × m.
Proof.
  intros n m.
  assert (H: 0 + n = n). { reflexivity. }
  rewrite → H.
  reflexivity. Qed.

断言策略引入了两个子目标。第一个是断言本身;通过在断言前面加上H:我们将断言命名为H(我们也可以像上面用析构函数和归纳法一样,将断言(0+n=n)命名为H)。请注意,我们用大括号{…}围绕该断言的证明,这两方面都是为了可读性,因此,在交互使用Coq时,当我们完成这个子证明时,我们可以更容易地看到。第二个目标与我们调用assert时的目标相同,只是在上下文中,我们现在假设H为0+n=n。也就是说,断言生成一个子目标,我们必须在其中证明断言的事实,第二个子目标,我们可以使用断言的事实在我们试图证明的任何事情上取得进展。

例如,假设我们想证明(n+m)+(p+q)=(m+n)+(p+q)。=两边的唯一区别是,第一个内部+的参数m和n被交换,因此我们似乎应该能够使用加法的交换性(add_comm)将一个重写为另一个。然而,重写策略在应用重写的地方不是很聪明。+在这里有三种用途,结果是重写→ “添加命令”将仅影响外部命令。。。

Theorem plus_rearrange_firsttry : ∀ n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  (* We just need to swap (n + m) for (m + n)... seems
     like add_comm should do the trick! *)
  rewrite add_comm.
  (* Doesn't work... Coq rewrites the wrong plus! :-( *)
Abort.

要在需要的地方使用add_comm,我们可以引入一个局部引理,说明n+m=m+n(对于我们在这里讨论的特定m和n),使用add_comm证明这个引理,然后使用它进行所需的重写。

Theorem plus_rearrange : ∀ n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  assert (H: n + m = m + n).
  { rewrite add_comm. reflexivity. }
  rewrite H. reflexivity. Qed.

正式与非正式证明 Formal vs. Informal Proof

“非正式证明是算法;正式证明是代码。”

什么构成一个数学主张的成功证明?这个问题已经向哲学家们提出了数千年的挑战,但一个粗略而现成的定义可能是这样的:数学命题P的证明是一个书面(或口头)文本,它向读者或听者灌输P为真的确定性——P的真理的一个无懈可击的论点。也就是说,证明是一种交流行为。

沟通行为可能涉及不同类型的读者。一方面,“读者”可以是一个类似Coq的程序,在这种情况下,灌输的“信念”是P可以从一组形式逻辑规则中机械地派生出来,而证明是一个指导程序检查这一事实的方法。这些食谱是正式的证明。

或者,读者可以是人,在这种情况下,证据将用英语或其他自然语言书写,因此必然是非正式的。在这里,成功的标准没有明确规定。一个“有效”的证据是让读者相信P的证据。但是同一个证据可能会被许多不同的读者阅读,其中一些人可能会被一种特殊的论点措辞说服,而另一些人可能不会。有些读者可能特别迂腐,缺乏经验,或者只是头脑简单;要说服他们,唯一的办法就是详细阐述这个论点。但其他读者,更熟悉这一领域,可能会发现所有这些细节如此压倒性,他们失去了整体线索;他们只想被告知主要想法,因为对他们来说,自己填写细节比费力地完成书面陈述要容易得多。归根结底,没有一个通用的标准,因为没有一种单一的方式来写一个非正式的证明,保证能说服每一个可能的读者。

然而,在实践中,数学家们已经形成了一套丰富的约定和习语,用于书写复杂的数学对象——至少在某个社区内——使交流相当可靠。这种程式化交流形式的惯例为判断证据的好坏提供了一个相当明确的标准。

因为我们在本课程中使用Coq,我们将大量使用正式证明。但这并不意味着我们可以完全忘记非正式的事情!形式证明在许多方面都是有用的,但它们并不是人与人之间交流思想的非常有效的方式。

例如,这里证明了加法是关联的:

  n + (m + p) = (n + m) + p.
Proof. intros n m p. induction n as [| n' IHn']. reflexivity.
  simpl. rewrite IHn'. reflexivity. Qed.

Coq对此非常满意。然而,对于人类来说,很难理解它。我们可以使用注释和项目符号来更清楚地显示结构。。。

Theorem add_assoc'' : ∀ n m p : nat,
n + (m + p) = (n + m) + p.
Proof.
intros n m p. induction n as [| n' IHn'].
- (* n = 0 *)
  reflexivity.
- (* n = S n' *)
  simpl. rewrite IHn'. reflexivity. Qed.
  ```
  ... 如果你已经习惯了Coq,你也许可以在脑海中一个接一个地思考战术,想象每一点的背景和目标堆栈的状态,但是如果证明更复杂一点,这几乎是不可能的。

(学究式的)数学家可能会这样写证明:

(** - Theorem: For any [n], [m] and [p],

  n + (m + p) = (n + m) + p.

_Proof_: By induction on [n].

- First, suppose [n = 0].  We must show that

    0 + (m + p) = (0 + m) + p.

  This follows directly from the definition of [+].

- Next, suppose [n = S n'], where

    n' + (m + p) = (n' + m) + p.

  We must now show that

    (S n') + (m + p) = ((S n') + m) + p.

  By the definition of [+], this follows from

    S (n' + (m + p)) = S ((n' + m) + p),

  which is immediate from the induction hypothesis.  _Qed_. *)
  ```
  证明的整体形式基本上是相似的,当然这不是偶然的:Coq的设计使其归纳策略产生了与数学家所写要点相同的子目标,顺序相同。但在细节上存在显著差异:正式证明在某些方面更加明确(例如,使用自反性),但在其他方面则不那么明确(特别是,Coq证明中任何给定点的“证明状态”都是完全隐含的,而非正式证明则多次提醒读者事情的现状)。

18: 2 stars, advanced, especially useful (add_comm_informal)

将您的add_comm解决方案转换为非正式证明:

定理:加法是交换的。

Theorem: Addition is commutative.

    Proof: (* FILL IN HERE *)

19: 2 stars, standard, optional (eqb_refl_informal)

使用add_assoc的非正式证明作为模型,编写以下定理的非正式证明。不要只是将Coq策略译成英语!

Theorem: (n =? n) = true for any n.
Proof: (* FILL IN HERE *)