Software Foundations Vol.I : 更多基本策略(Tactics)

本章主要內容包括：

如何在“向前證明”和“向后證明”兩種風格中使用輔助引理；
如何對數據構造子進行論證，特別是，如何利用它們單射且不交的事實；
如何增強歸納假設，以及何時需要增強；
還有通過分類討論進行論證的更多細節。

Apply策略

通常,經常會遇到待證目標與上下文中的前提或已證引理'剛好相同'的情況。

Theorem silly1 : ? (n m o p : nat),
     n = m →
     [n;o] = [n;p] →
     [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  rewrite <- eq1.

此時可以像之前那樣用“rewrite → eq2. reflexivity.”來完成。

apply: 從結論出發,對待證明結論q通過apply模式p->q結合,轉化待證明命題為p.這是一種結論上移的操作.

不過如果使用 apply 策略，只需一步就能完成此證明：

  apply eq2. Qed.

apply 策略也可以配合'條件（Conditional）'假設和引理來使用：如果被應用的語句是一個蘊含式，那么該蘊含式的前提就會被添加到待證子目標列表中。

Theorem silly2 : ? (n m o p : nat),
    n = m →
    (n = m → [n;o] = [m;p]) →
    [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  apply eq2. 
  apply eq1. 
Qed.

通常，當使用 apply H 時，語句 H 會以一個引入了某些 '通用變量（Universal Variables）' 的 ? 開始。在 Coq 針對 H 的結論匹配當前目標時，它會嘗試為這些變量查找適當的值。

例如，當我們在以下證明中執行 apply eq2 時，eq2 中的通用變量 q 會以 n 實例化，而 r 會以 m 實例化。

Theorem silly2a : ? (n m : nat),
     (n,n) = (m,m) →
     (? (q r : nat), (q,q) = (r,r) → [q] = [r]) →
     [n] = [m].
Proof.
  intros n m eq1 eq2.
  apply eq2. 
  apply eq1. 
Qed.

要使用 apply 策略，被應用的事實（的結論）必須精確地匹配證明目標：若當等式的左右兩邊互換后，apply 就無法起效了。

Theorem silly3_firsttry : ? (n : nat),
     true = (n =? 5) →
     (S (S n)) =? 7 = true.
Proof.
  intros n H.

在這里，無法直接使用 apply，若試圖apply H,則會出現如下的報錯:

In environment
n : nat
H : true = (n =? 5)
Unable to unify "true = (n =? 5)" with "(S (S n) =? 7) = true".

不過可以用 symmetry 策略它會交換證明目標中等式的左右兩邊。

  symmetry.
  simpl.
  apply H. 
Qed.

symmetry: 將待證明等式左右兩側互換.

Apply with策略

以下愚蠢的例子在一行中使用了兩次改寫來將 [a;b] 變成 [e;f]。

Example trans_eq_example : ? (a b c d e f : nat),
     [a;b] = [c;d] →
     [c;d] = [e;f] →
     [a;b] = [e;f].
Proof.
  intros a b c d e f eq1 eq2.
  rewrite → eq1. 
  rewrite → eq2. 
  reflexivity. 
Qed.

由于這種模式十分常見，因此一勞永逸地把它作為一條引理記錄下來，即等式具有傳遞性。

Theorem trans_eq : ? (X:Type) (n m o : X),
  n = m → m = o → n = o.
Proof.
  intros X n m o eq1 eq2. 
  rewrite → eq1. 
  rewrite → eq2.
  reflexivity. 
Qed.

現在，按理說應該可以用 trans_eq 來證明前面的例子了。然而，實際上為此還需要稍微改進一下 apply 策略。

Example trans_eq_example' : ? (a b c d e f : nat),
     [a;b] = [c;d] →
     [c;d] = [e;f] →
     [a;b] = [e;f].
Proof.
  intros a b c d e f eq1 eq2.
  apply trans_eq 
    with (m:=[c;d]).
  apply eq1. 
  apply eq2. 
Qed.

這是因為,匹配過程并沒有為 m 確定實例：我們必須在 apply 的調用后面加上 "with (m:=[c,d])" 來顯式地提供一個實例。

apply with: 對于未確定實例的apply模式,指定其中部分變量實例.

（實際上，通常不必在 with 從句中包含名字 m，Coq 一般足夠聰明來確定實例化的變量。因此也可以寫成： apply trans_eq with [c;d]。）

Injection與Discriminate策略

回想自然數的定義：

     Inductive nat : Type :=
       | O
       | S (n : nat).

可從該定義中觀察到，所有的數都是兩種形式之一：

要么是構造子 O，
要么就是將構造子 S 應用到另一個數上。

不過這里還有無法直接看到的：自然數的定義中還蘊含了兩個事實：

構造子 S 是'單射（Injective）'或'一一對應'的。即，如果 S n = S m，那么 n = m 必定成立。
構造子 O 和 S 是'不相交（Disjoint）'的。即，對于任何 n，O 都不等于 S n。

類似的原理同樣適用于所有歸納定義的類型：所有構造子都是單射的，而不同構造子構造出的值絕不可能相等。

對于列表來說，cons 構造子是單射的，而 nil 不同于任何非空列表。

對于布爾值來說，true 和 false 是不同的。因為 true 和 false 二者都不接受任何參數，它們既不在這邊也不在那邊。

其它歸納類型亦是如此。

例如，可以使用定義在 Basics.v 中的 pred 函數來證明 S 的單射性。

Theorem S_injective : ? (n m : nat),
  S n = S m →
  n = m.
Proof.
  intros n m H1.
  assert (H2: n = pred (S n)). {
    reflexivity. 
  }
  rewrite H2. 
  rewrite H1. 
  reflexivity.
Qed.

這個技巧可以通過編寫等價的 pred 來推廣到任意的構造子上 —— 即編寫一個“撤銷”一次構造子調用的函數。

為此，Coq 提供了更加簡便的 injection 策略，它能讓我們利用任意構造子的單射性。

下面是使用 injection 對上面定理的另一種證法：

Theorem S_injective' : ? (n m : nat),
  S n = S m →
  n = m.
Proof.
  intros n m H.
  injection H as Hnm. 
  apply Hnm.
Qed.

通過在此處編寫 injection H as Hmn，讓 Coq 利用構造子的單射性來產生所有它能從 H 所推出的等式（本例中為等式 n = m）。

每一個這樣的等式都作為假設（本例中為 Hmn）被添加到上下文中。

injection: 利用構造子單射性來產生推演.

以下例子展示了一個 injection 如何直接得出多個等式。

Theorem injection_ex1 : ? (n m o : nat),
  [n; m] = [o; o] →
  [n] = [m].
Proof.
  intros n m o H.
  injection H as H1 H2.
  rewrite H1. 
  rewrite H2. 
  reflexivity.
Qed.

另一方面，如果只使用 injection H 而不帶 as 從句，那么所有的等式都會在目標的開頭被轉變為假設。

Theorem injection_ex1 : ? (n m o : nat),
  [n; m] = [o; o] →
  [n] = [m].
Proof.
  intros n m o H.
  injection H.
  intros H1 H2.
  rewrite H1. 
  rewrite H2. 
  reflexivity.
Qed.

關于構造子的injectivity就這么多吧, 來看到其disjointness.

disjointness原則指出,以不同構造子開始的項(如O 與 S,或者true 和 false)永遠不可能相等.

這意味著,當在某個情境中假定兩個這樣的項相等時,都有充分的理由得出任何想要的結論,因為這種假設是毫無意義的(trivial).

discriminate策略體現了這一原則: 其適用于涉及不同構造子之間相等關系的假設(例如 S n=O),并且能夠立即解決當前的目標.

下面是一個例子:

Theorem eqb_0_l : ? n,
   0 =? n = true → n = 0.
Proof.
  intros n.
  destruct n as [| n'] eqn:E.
  - (* n = 0 *)
    intros H. 
    reflexivity.
  - (* n = S n' *)
    simpl.    
    intros H. 
    discriminate H.
Qed.

其中,第二個分支中,假設O=?(S n')=true,那么必須證明 S n'=O.接下來觀察到這個假設本身是無意義的.

如果我們對這個假設使用 discriminate ， Coq 便會確認我們當前正在證明的目標不可行，并同時移除它，不再考慮。

本例是邏輯學原理'爆炸原理'的一個實例，它斷言矛盾的前提會推出任何東西，甚至是假命題！

discriminate: 利用爆炸原理,通過矛盾的前提直接切除分支.

Theorem discriminate_ex1 : ? (n : nat),
  S n = O →
  2 + 2 = 5.
Proof.
  intros n contra. 
  discriminate contra. 
Qed.

Theorem discriminate_ex2 : ? (n m : nat),
  false = true →
  [n] = [m].
Proof.
  intros n m contra. 
  discriminate contra. 
Qed.

爆炸原理可能令人費解，那么請記住上述證明'并不'肯定其后件，而是說明：'如果'荒謬的前件成立，'那么'就會得出荒謬的結論，如此一來我們將生活在一個不一致的宇宙中，這里每個陳述都是正確的。

構造子的單射性能讓我們論證 ? (n m : nat), S n = S m → n = m。此蘊含式的逆形式是一個構造子和函數的更一般的實例，在后面我們會發現它用起來很方便：

Theorem f_equal : ? (A B : Type) 
  (f: A → B) (x y: A),
  x = y → f x = f y.
Proof. 
  intros A B f x y eq. 
  rewrite eq. 
  reflexivity. 
Qed.

Theorem eq_implies_succ_equal : ? (n m : nat),
    n = m → S n = S m.
Proof. 
  intros n m H. 
  apply f_equal. 
  apply H. 
Qed.

此外,還有一種名為"f_equal"的策略可以用來證明此類定理.

對于形如 f a1 ... an=g b1 ... bn的目標,策略"f_equal"會生成形如f=g, a1=b1, ... , an=bn的子目標.同時,任意這些子目標中只要足夠簡單,"f_equal"都會將其自動消去.

Theorem eq_implies_succ_equal' : ? (n m : nat),
    n = m → S n = S m.
Proof. 
  intros n m H. 
  f_equal. 
  apply H. 
Qed.

f_equal: 對于形如 f a1 ... an=g b1 ... bn的目標進行自動檢查的策略.

針對假設的策略

默認情況下，大部分策略會作用于目標公式并保持上下文不變。然而，大部分策略還有對應的變體來對上下文中的語句執行類似的操作。

例如，策略 simpl in H 會對上下文中的假設 H 執行化簡。

Theorem S_inj : ? (n m : nat) (b : bool),
     (S n) =? (S m) = b →
     n =? m = b.
Proof.
  intros n m b H. 
  simpl in H. 
  apply H. 
Qed.

simpl in: 對局部的前提進行簡化.

symmetry in: 對局部的前提進行翻轉.

類似地，apply L in H 會針對上下文中的假設 H 匹配某些（形如 X → Y 中的）條件語句 L。

然而，與一般的 apply 不同（它將匹配 Y 的目標改寫為子目標 X），apply L in H 會針對 X 匹配 H，如果成功，就將其替換為 Y。

換言之，apply L in H 給了我們一種“正向推理”的方式：

根據 X → Y 和一個匹配 X 的假設，它會產生一個匹配 Y 的假設。

作為對比，apply L 是一種“反向推理”：它表示如果我們知道 X → Y 并且試圖證明 Y，那么證明 X 就足夠了。

apply in: 通過X->Y,X的模式,類似于mp方式代入.

下面是前面證明的一種變體，它始終使用正向推理而非反向推理。

Theorem silly3' : ? (n : nat),
  (n =? 5 = true → (S (S n)) =? 7 = true) →
  true = (n =? 5) →
  true = ((S (S n)) =? 7).
Proof.
  intros n eq H.
  symmetry in H. 
  apply eq in H. 
  symmetry in H.
  apply H.   
Qed.

正向推理從'給定'的東西開始（即前提、已證明的定理），根據它們迭代地刻畫結論直到抵達目標。

反向推理從'目標'開始，迭代地推理蘊含目標的東西，直到抵達前提或已證明的定理。

你在數學或計算機科學課上見過的非形式化證明可能傾向于正向推理。

通常，Coq 習慣上傾向于使用反向推理，但在某些情況下，正向推理更易于思考

變換Induction假設

在 Coq 中進行歸納證明時，有時控制歸納假設的確切形式是十分重要的。

特別是，在調用 induction 策略前，需要用 intros 將假設從目標移到上下文中時要十分小心。

例如，假設我們要證明 double 函數是單射的,即將不同的參數映射到不同的結果：

Theorem double_injective: ? n m,
  double n = double m → n = m.
  intros n. 
  induction n.
(*...*)

此證明的開始方式有點微妙：如果我們以intros n. induction n.開頭開始，那么一切都好。

然而假如以intros n m. induction n.開始，就會卡在歸納情況中...

Theorem double_injective_FAILED : ? n m,
     double n = double m →
     n = m.
Proof.
  intros n m. induction n as [| n' IHn'].
  - (* n = O *) 
    simpl. 
    intros eq. 
    destruct m as [| m'] eqn:E.
    + (* m = O *) 
      reflexivity.
    + (* m = S m' *) 
      discriminate eq.
  - (* n = S n' *) 
    intros eq. 
    destruct m as [| m'] eqn:E.
    + (* m = O *) 
      discriminate eq.
    + (* m = S m' *) 
      apply f_equal.
Abort.

此時，歸納假設 IHn' '不會'給出 n' = m',會有個額外的 S 阻礙,因此該目標無法證明。

哪里出了問題？

問題在于，在調用歸納假設的地方已經將 m 引入了上下文中--直觀上，我們已經告訴了 Coq “我們來考慮具體的 n 和 m...”，

而現在必須為那些'具體的' n 和 m 證明 double n = double m，然后才有 n = m。

下一個策略 induction n 告訴 Coq：我們要對 n 歸納來證明該目標。

也就是說，我們要證明對于'所有的' n，命題 P n = "if double n = double m, then n = m"成立，需通過證明

P O （即，若“double O = double m 則 O = m”）和
P n → P (S n) （即，若“double n = double m 則 n = m”蘊含“若 double (S n) = double m 則 S n = m”）

來得出。

如果我們仔細觀察第二個語句，就會發現它說了奇怪的事情：

對于一個'具體的' m，如果我們知道 “若 double n = double m 則 n = m” 那么我們就能證明 “若 double (S n) = double m 則 S n = m”。

但是知道 Q 對于證明 R 來說并沒有任何幫助！

（如果我們試著根據 Q 證明 R，就會以“假設 double (S n) = 10..”這樣的句子開始，不過之后我們就會卡住：知道 double (S n) 為 10 并不能告訴我們 double n 是否為 10。（實際上，它強烈地表示 double n '不是' 10！）因此 Q 是沒有用的。）

當 m 已經在上下文中時，試圖對 n 進行歸納來進行此證明是行不通的，因為我們之后要嘗試證明涉及'每一個' n 的命題，而不只是'單個' m。

對 double_injective 的成功證明將 m 留在了目標語句中 induction 作用于 n 的地方：

注意，此時的證明目標和歸納假設是不同的：證明目標要求我們證明更一般的事情（即，為'每一個' m 證明該語句），而歸納假設 IH 相應地更加靈活，允許我們在應用歸納假設時選擇任何想要的 m。

Theorem double_injective : ? n m,
     double n = double m →
     n = m.
Proof.
  intros n. induction n as [| n' IHn'].
  - (* n = O *) 
    simpl. 
    intros m eq. 
    destruct m as [| m'] eqn:E.
    + (* m = O *) 
      reflexivity.
    + (* m = S m' *) 
      discriminate eq.
  - (* n = S n' *) 
    simpl.
    intros m eq.
    destruct m as [| m'] eqn:E.
    + (* m = O *) 
      simpl.
      discriminate eq.
    + (* m = S m' *)
      apply f_equal.
      apply IHn'. 
      injection eq as goal. 
      apply goal. 
Qed.

到這里，由于我們在 destruct m 的第二個分支中，因此上下文中涉及到的 m' 就是我們開始討論的 m 的前趨。

由于我們也在歸納的 S 分支中，這就很完美了：如果我們在歸納假設中用當前的 m'（此實例由下一步的 apply 自動產生）實例化一般的 m，那么 IHn' 就剛好能給出我們需要的來結束此證明。

從上面的一切中,應當領悟到的是: 在運用induction時,必須謹慎行事,切不可試圖證明過于具體的內容: 在通過關于變量n與m的命題進行歸納證明時,有時必須將變量m設為通用形式,這一點至關重要.

在 induction 之前做一些 intros 來獲得更一般歸納假設并不總是奏效。

有時需要對量化的變量做一下'重排'。例如，假設我們想要通過對 m 而非 n 進行歸納來證明 double_injective。

Theorem double_injective_take2_FAILED : ? n m,
     double n = double m →
     n = m.
Proof.
  intros n m. induction m as [| m' IHm'].
  - (* m = O *) 
    simpl. 
    intros eq. 
    destruct n as [| n'] eqn:E.
    + (* n = O *) 
      reflexivity.
    + (* n = S n' *) 
      discriminate eq.
  - (* m = S m' *) 
    intros eq. 
    destruct n as [| n'] eqn:E.
    + (* n = O *) 
      discriminate eq.
    + (* n = S n' *) 
      apply f_equal.
        (* 和前面一樣，又卡在這兒了。 *)
Abort.

問題在于，要對 m 進行歸納，我們首先必須對 n 歸納。（而如果我們不引入任何東西就執行 induction m，Coq 就會自動為我們引入 n）

我們可以對它做什么？

一種可能就是改寫該引理的陳述使得 m 在 n 之前量化。

這樣是可行的，不過它不夠好：我們不想調整該引理的陳述來適應具體的證明策略！我們更想以最清晰自然的方式陳述它。

我們可以先引入所有量化的變量，然后'重新一般化（re-generalize）' 其中的一個或幾個，選擇性地從上下文中挑出幾個變量并將它們放回證明目標的開始處。

用 generalize dependent 策略就能做到。

Theorem double_injective_take2 : ? n m,
     double n = double m →
     n = m.
Proof.
  intros n m.
  (* n and m are both in the context *)
  generalize dependent n.
  (* 現在 n 回到了目標中，我們可以對 m 進行歸納并得到足夠一般的歸納假設了。 *)
  induction m as [| m' IHm'].
  - (* m = O *) 
    simpl. 
    intros n eq. 
    destruct n as [| n'] eqn:E.
    + (* n = O *) 
      reflexivity.
    + (* n = S n' *) 
      discriminate eq.
  - (* m = S m' *) 
    intros n eq. destruct n as [| n'] eqn:E.
    + (* n = O *) 
      discriminate eq.
    + (* n = S n' *) 
      apply f_equal.
      apply IHm'. 
      injection eq as goal. 
      apply goal. 
Qed.

generalize dependent: 將某個intros的符號變量提取出來一般化,避免實例化帶來的不便.

來看一下此定理的非形式化證明。注意保持 n 的量化狀態并通過歸納證明的命題，對應于形式化證明中依賴的一般化。

'定理'：對于任何自然數 n 和 m，若 double n = double m，則 n = m。
'證明'：令 m 為一個 nat。通過對 m 進行歸納來證明，對于任何 n，若 double n = double m，則 n = m。

首先，設 m = 0，而 n 是一個數使得 double n = double m。我們必須證明 n = 0。

由于 m = 0，根據 double 的定義，有 double n = 0。此時對于 n 需要考慮兩種情況。

若 n = 0，則得證，因為 m = 0 = n，正如所需。
否則，若對于某個 n' 有 n = S n'，我們就會導出矛盾：根據 double 的定義，我們可得出 double n = S (S (double n'))，但它與 double n = 0 相矛盾。

其次，設 m = S m'，而 n 同樣是一個數使得 double n = double m。

必須證明 n = S m'，根據歸納假設，對于任何數 s，若 double s = double m'，則 s = m'。

根據 m = S m' 的事實以及 double 的定義我們有 double n = S (S (double m'))。

此時對于 n 需要考慮兩種情況。

若 n = 0，則根據 double n = 0 的定義會得出矛盾。
故存在 n' 使得 n = S n'。

再次根據 double 之定義，可得 S (S (double n')) = S (S (double m'))。

再由構造子單射可知 double n' = double m'。以n' 代入歸納假設，推得 n' = m'，故顯然 S n' = S m'，其中 S n' = n，S m' = m，所以原命題得證。 ?

展開Definition

有時候我們會需要手動展開一個Definition引入的名稱,以便能夠對它所表示的表達式進行操作.例如:我們試圖定義:

Definition square n := n × n.

...并試圖證明一個關于 square 的簡單事實...

Lemma square_mult : ? n m, 
  square (n × m) = square n × square m.
Proof.
  intros n m.
  simpl.
  unfold square.
  rewrite mult_assoc.
  assert (H : n × m × n = n × n × m). { 
    rewrite mult_comm. 
    apply mult_assoc. 
  }
  rewrite H. 
  rewrite mult_assoc. 
  reflexivity.
Qed.

...那么就會卡住：simpl 無法化簡任何東西，而由于我們尚未證明任何關于 square 的事實，也就沒有任何可以用來 apply 或 rewrite 的東西。為此，可以手動用 unfold 展開 square 的定義.

等式兩邊都是涉及乘法的表達式，有很多可用的關于乘法的事實。特別是它滿足交換性和結合性，該引理據此不難證明。

現在，是時候討論下展開和化簡了。

已經觀察到，像 simpl、reflexivity 和 apply 這樣的策略，通常總會在需要時自動展開函數的定義。

例如，若我們將 foo m 定義為常量 5...

Definition foo (x: nat) := 5.

那么在以下證明中 simpl（或 reflexivity，如果我們忽略 simpl）就會將 foo m 展開為 (fun x ? 5) m 并進一步將其化簡為 5。

Fact silly_fact_1 : ? m, foo m + 1 = foo (m + 1) + 1.
Proof.
  intros m.
  simpl.
  reflexivity.
Qed.

然而，這種自動展開有些保守。例如，若用模式匹配定義稍微復雜點的函數,那么類似的證明就會被卡住：

Definition bar x :=
  match x with
  | O ? 5
  | S _ ? 5
  end.

simpl 沒有進展的原因在于，它注意到在試著展開 bar m 之后會留下被匹配的 m，它是一個變量，因此 match 無法被進一步化簡。

它還沒有聰明到發現 match 的兩個分支是完全相同的。因此它會放棄展開 bar m 并留在那。

類似地，在試著展開 bar (m+1) 時會留下一個 match，被匹配者是一個函數應用（即它本身，即便在展開 + 的定義后也無法被化簡），因此 simpl 會留下它。

此時有兩種方法可以繼續。

一種是用 destruct m 將證明分為兩種情況，每一種都關注于更具體的 m（O vs S _）。在這兩種情況下， bar 中的 match 可以繼續了，證明則很容易完成。

Fact silly_fact_2 : ? m, bar m + 1 = bar (m + 1) + 1.
Proof.
  intros m.
  destruct m eqn:E.
  - simpl. reflexivity.
  - simpl. reflexivity.
Qed.

這種方法是可行的，不過它依賴于我們能發現隱藏在 bar 中的 match 阻礙了證明的進展。一種更直白的方式就是明確地告訴 Coq 去展開 bar。

Fact silly_fact_2' : ? m, bar m + 1 = bar (m + 1) + 1.
Proof.
  intros m.
  unfold bar.
  destruct m eqn:E.
  - reflexivity.
  - reflexivity.
Qed.

對復合表達式使用Destruct

我們已經見過許多通過 destruct 進行情況分析來處理一些變量的值了。

有時需要根據某些'表達式'的結果的情況來進行推理。也可以用 destruct 來做這件事。

下面是一些例子：

Definition sillyfun (n : nat) : bool :=
  if n =? 3 
  then false
  else if n =? 5 then false
  else false.
Theorem sillyfun_false : ? (n : nat),
  sillyfun n = false.
Proof.
  intros n. 
  unfold sillyfun.
  destruct (n =? 3) eqn:E1.
    - (* n =? 3 = true *) 
      reflexivity.
    - (* n =? 3 = false *) 
      destruct (n =? 5) eqn:E2.
      + (* n =? 5 = true *) 
        reflexivity.
      + (* n =? 5 = false *) 
        reflexivity. 
Qed.

在前面的證明中展開 sillyfun 后，我們發現卡在 if (n =? 3) then ... else ... 上了。

但由于 n 要么等于 3 要么不等于，因此我們可以用 destruct (eqb n 3) 來對這兩種情況進行推理。

通常，destruct 策略可用于對任何計算結果進行情況分析。

如果 e 是某個表達式，其類型為歸納定義的類型 T，那么對于 T 的每個構造子 c，destruct e 都會生成一個子目標，其中（即目標和上下文中）所有的 e 都會被替換成 c。

destruct 策略的 eqn: 部分是可選的：目前，大部分時間都會包含它，只是為了文檔的目的。

然而在用 destruct 結構復合表達式時，eqn: 記錄的信息是十分關鍵的：如果我們丟棄它，那么 destruct 會擦除我們完成證明時所需的信息。

例如，假設函數 sillyfun1 定義如下：

Definition sillyfun1 (n : nat) : bool :=
  if n =? 3 
  then true
  else if n =? 5 
  then true
  else false.

現在假設我們想讓coq相信,對于sillyfun1 n來說,只有當n為奇數時其結果才為真值.

如果在證明過程中這樣開始(destruct操作不加上eqn:)就會陷入困境.因為當前的上下文中沒有足夠的信息來證明這一目標!

Theorem sillyfun1_odd_FAILED : ? (n : nat),
     sillyfun1 n = true →
     oddb n = true.
Proof.
  intros n eq. unfold sillyfun1 in eq.
  destruct (n =? 3).
  (* 卡住了... *)
Abort.

問題在于,destruct操作的方式極其粗暴--在這種情況下,它會丟棄所有出現"n=?3"的情況,但我們需要保留對這個表達式以及它是如何被destruct的記憶,因為需要能夠推斷出"n=?3=true"導致必然有"n=3"--據此可以得出n為奇數的結論.

在此的目標是完全替代掉現有的"n=3"這樣的表述,同時在上下文中添加一個方程,用于記錄所處的情況.這是"eqn:"限定符所起到的作用.

Theorem sillyfun1_odd : ? (n : nat),
     sillyfun1 n = true →
     oddb n = true.
Proof.
  intros n eq. 
  unfold sillyfun1 in eq.
  destruct (n =? 3) eqn:Heqe3.
  (* 現在我們的狀態和前面卡住的地方一樣了，除了上下文中包含了額外的相等關系假設，
     它就是我們繼續推進所需要的。 *)
    - (* e3 = true *) 
      apply eqb_true in Heqe3.
      rewrite → Heqe3. 
      reflexivity.
    - (* e3 = false *)
     (* 當我們到達正在推理的函數體中第二個相等關系測試時，我們可以再次使用
        eqn:，以便結束此證明。 *)
      destruct (n =? 5) eqn:Heqe5.
        + (* e5 = true *)
          apply eqb_true in Heqe5.
          rewrite → Heqe5. 
          reflexivity.
        + (* e5 = false *) 
          discriminate eq. 
Qed.

復習

現在我們已經見過 Coq 中最基礎的策略了。

未來的章節中我們還會介紹更多，之后我們會看到一些更加強大的'自動化'策略，它能讓 Coq 幫我們處理底層的細節。

下面是我們已經見過的：

intros：將前提/變量從證明目標移到上下文中
reflexivity：（當目標形如 e = e 時）結束證明
apply：用前提、引理或構造子證明目標
apply... in H：將前提、引理或構造子應用到上下文中的假設上（正向推理）
apply... with...：為無法被模式匹配確定的變量顯式指定值
simpl：化簡目標中的計算
simpl in H：化簡前提中的計算
rewrite：使用相等關系假設（或引理）來改寫目標
rewrite ... in H：使用相等關系假設（或引理）來改寫前提
symmetry：將形如 t=u 的目標改為 u=t
symmetry in H：將形如 t=u 的前提改為 u=t
unfold：用目標中的右式替換定義的常量
unfold... in H：用前提中的右式替換定義的常量
destruct... as...：對歸納定義類型的值進行情況分析
destruct... eqn:...：為添加到上下文中的等式指定名字，記錄情況分析的結果
induction... as...: 對歸納定義類型的值進行歸納
injection: 通過injectivity來分析由歸納定義所對應值之間的相等關系的原理
discriminate: 依據constructors之間的disjointness來對由歸納定義的類型所表示的值之間相等關系進行推理
assert (H: e)（或 assert (e) as H）：引入“局部引理”e 并稱之為 H
generalize dependent x：將變量 x（以及任何依賴它的東西）從上下文中移回目標公式內的前提中

posted @ 2025-10-11 03:56 Mesonoxian 閱讀(5) 評論(0) 收藏舉報

刷新頁面返回頂部

mesonoxian

Software Foundations Vol.I : 更多基本策略(Tactics)

Software Foundations Vol.I : 更多基本策略(Tactics)

Apply策略

Apply with策略

Injection與Discriminate策略

針對假設的策略

變換Induction假設

展開Definition

對復合表達式使用Destruct

復習

公告