Software Foundations Vol.I : 歸納證明(Induction)

歸納法證明

我們在上一章中通過基于化簡的簡單論據證明了 0 是 + 的左幺元。 我們也觀察到，當我們打算證明 0 也是 + 的 '右' 幺元時事情就沒這么簡單了

Theorem plus_n_O_firsttry : ? n:nat,
  n = n + 0.
Proof.
  intros n.
  simpl. (* Does nothing! *)
Abort.

只應用 reflexivity 的話不起作用，因為 n + 0 中的 n 是任意未知數，所以在 + 的定義中 match 匹配無法被化簡。

即便用 destruct n 分類討論也不會有所改善：誠然，我們能夠輕易地證明 n = 0 時的情況；但在證明對于某些 n' 而言 n = S n' 時，我們又會遇到和此前相同的問題。

Theorem plus_n_O_secondtry : ? n:nat,
  n = n + 0.
Proof.
  intros n. destruct n as [| n'] eqn:E.
  - (* n = 0 *)
    reflexivity. (* 雖然目前還沒啥問題... *)
  - (* n = S n' *)
    simpl. (* ...不過我們又卡在這兒了 *)
Abort.

雖然還可以用 destruct n' 再推進一步，但由于 n 可以任意大， 如果照這個思路繼續證明的話，我們永遠也證不完。

為了證明這種關于數字、列表等歸納定義的集合的有趣事實， 我們通常需要一個更強大的推理原理：'歸納'。

自然數的歸納法則:

• 證明 P(O) 成立；
• 證明對于任何 n'，若 P(n') 成立，那么 P(S n') 也成立。
• 最后得出 P(n) 對于所有 n 都成立的結論。

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

induction: 通過數學歸納法對命題進行證明的策略.

Coq中也同樣,以證明 P(n) 對于所有 n 都成立的目標開始， 然后（通過應用 induction 策略）把它分為兩個子目標：一個是我們必須證明 P(O) 成立，另一個是我們必須證明 P(n') → P(S n')。

和 destruct 一樣，induction 策略也能通過 as... 從句為引入到 子目標中的變量指定名字。由于這次有兩個子目標，因此 as... 有兩部分，用 | 隔開。

Theorem minus_diag : ? n,
  minus n n = 0.
Proof.
  (* 課上已完成 *)
  intros n. induction n as [| n' IHn'].
  - (* n = 0 *)
    simpl. 
    reflexivity.
  - (* n = S n' *)
    simpl. 
    rewrite → IHn'. 
    reflexivity. 
Qed.

（其實在這些證明中我們并不需要 intros：當 induction 策略被應用到包含量化變量的目標中時，它會自動將需要的變量移到上下文中。）

證明中的證明

和在非形式化的數學中一樣，在 Coq 中，大的證明通常會被分為一系列定理， 后面的定理引用之前的定理。但有時一個證明會需要一些繁雜瑣碎的事實， 而這些事實缺乏普遍性，以至于我們甚至都不應該給它們單獨取頂級的名字。

如果能僅在需要時簡單地陳述并立即證明所需的“子定理”就會很方便。 我們可以用 assert 策略來做到。

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.

assert 策略引入兩個子目標。第一個為斷言本身，通過給它加前綴 H: 我們將該斷言命名為 H。（當然也可以用 as 來命名該斷言，例如 assert (0 + n = n) as H。

第二個目標 與之前執行 assert 時一樣，只是這次在上下文中，我們有了名為 H 的前提 0 + n = n。

舉例來說，假如我們要證明 (n + m) + (p + q) = (m + n) + (p + q)。

Theorem plus_rearrange_firsttry : ? n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  (* 我們只需要將 (m + n) 交換為 (n + m)... 看起來 plus_comm 能搞定！*)
  rewrite → plus_comm.
  (* 搞不定... Coq 選錯了要改寫的加法！ *)
Abort.

為了在需要的地方使用 plus_comm，我們可以（為此這里討論的 m 和 n） 引入一個局部引理來陳述 n + m = m + n，之后用 plus_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 → plus_comm. 
      reflexivity. 
    }
  rewrite → H. 
  reflexivity. 
Qed.

我們不難發現,相比起上面的例子,這里的例子將引理中的符號指定為特定的m與n,解決了問題.

形式化證明 vs 非形式化證明

“'非形式化證明是算法，形式化證明是代碼。'”

由于我們在本課程中使用 Coq，因此會重度使用形式化證明。但這并不意味著我們 可以完全忽略掉非形式化的證明過程！形式化證明在很多方面都非常有用， 不過它們對人類之間的思想交流而言 '并不' 十分高效。

例如，下面是一段加法結合律的證明：

Theorem plus_assoc' : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof. 
  intros n m p. 
  induction n as [| n' IHn']. 
  - reflexivity.
  - simpl. 
    rewrite → IHn'. 
    reflexivity. 
Qed.

Coq 對此表示十分滿意。然而人類卻很難理解它。

一個（迂腐的）數學家可能把證明寫成這樣：

'定理'： 對于任何 n、m 和 p，
$$n + (m + p) = (n + m) + p.$$

'證明'： 對 n 使用歸納法。
首先，設 n = 0。我們必須證明
$$ 0 + (m + p) = (0 + m) + p.$$
此結論可從 + 的定義直接得到。
然后，設 n = S n'，其中
$$ n' + (m + p) = (n' + m) + p.$$
我們必須證明
$$ (S n') + (m + p) = ((S n') + m) + p.$$
根據 + 的定義，該式可寫成
$$ S (n' + (m + p)) = S ((n' + m) + p),$$
它由歸納假設直接得出。'證畢'。