Software Foundations Vol.I : 使用結構化的數據(Lists)

---

數值序對

在 Inductive 類型定義中，每個構造子（Constructor）可以有任意多個參數 —— 可以沒有（如 true 和 O），可以只有一個（如 S），也可以更多 （如 nybble，以及下文所示）：

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

Check (pair 3 5) : natprod.

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

由于二元組十分常用，不妨以標準的數學記法 (x,y) 取代 pair x y。 通過 Notation 向 Coq 聲明該記法：

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

這種新的表示法既可以在表達式中使用,也可以在模式匹配中使用.

Compute (fst (3,5)).
Definition fst' (p : natprod) : nat :=
  match p with
  | (x,y) ? x
  end.
Definition snd' (p : natprod) : nat :=
  match p with
  | (x,y) ? y
  end.
Definition swap_pair (p : natprod) : natprod :=
  match p with
  | (x,y) ? (y,x)
  end.

對一個括號內的元組(如:(x,y)),并非與先前所見的多重匹配語法(如 x,y)混淆.

這種差異雖然不大,但是了解到這一點還是非常必要的.例如,下面的定義就是不正確的:

(* Can't match on a pair with multiple patterns: *)
Definition bad_fst (p : natprod) : nat :=
  match p with
  | x, y ? x
  end.

(* Can't match on multiple values with pair patterns: *)
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.

如果我們以稍顯古怪的方式陳述序對的性質，那么有時只需 reflexivity（及其內建的簡化）即可完成證明。

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

但是，如果我們用一種更為自然的方式來陳述此引理的話，只用 reflexivity 還不夠。

Theorem surjective_pairing_stuck : ? (p : natprod),
  p = (fst p, snd p).
Proof.
  simpl. (* 啥也沒有歸約！ *)
Abort.

我們還需要向 Coq 展示 p 的具體結構，這樣 simpl 才能對 fst 和 snd 做模式匹配。通過 destruct 可以達到這個目的

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

數值列表

通過推廣序對的定義，數值'列表'類型可以這樣描述： “一個列表要么是空的，要么就是由一個數和另一個列表組成的序對。”

Inductive natlist : Type :=
  | nil
  | cons (n : nat) (l : natlist).

例如，這是一個三元素列表：

Definition mylist := cons 1 (cons 2 (cons 3 nil)).

和序對一樣，使用熟悉的編程記法來表示列表會更方便些。 以下兩個聲明能讓我們用 :: 作為中綴的 cons 操作符， 用方括號作為構造列表的“外圍（outfix）”記法。

Notation "x :: l" := (cons x l)
  (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := 
  (cons x .. (cons y nil) ..).

注解 "right associativity" 告訴 Coq 當遇到多個 :: 時如何給表達式加括號，如此一來下面三個聲明做的就是同一件事：

Definition mylist1 := 1 :: (2 :: (3 :: nil)).
Definition mylist2 := 1 :: 2 :: 3 :: nil.
Definition mylist3 := [1;2;3].

"at level 60" 告訴 Coq 當遇到表達式和其它中綴運算符時應該如何加括號。 例如，plus 函數定義了 + 中綴符號，它的優先級是 50：

Notation "x + y" := (plus x y)
  (at level 50, left associativity).

+會比 :: 結合的更緊密，所以 1 + 2 :: [3] 會被解析成 (1 + 2) :: [3] 而非 1 + (2 :: [3])。

Repeat

接下來看幾個用來構造和操作列表的函數。第一個是 repeat 函數，它接受一個數字 n 和一個 count，返回一個長度為 count，每個元素都是 n 的列表。

Fixpoint repeat (n count : nat) : natlist :=
  match count with
  | O ? nil
  | S count' ? n :: (repeat n count')
  end.

Length

length 函數用來計算列表的長度。

Fixpoint length (l:natlist) : nat :=
  match l with
  | nil ? O
  | h :: t ? S (length t)
  end.

Append

app 函數用來把兩個列表聯接起來。

Fixpoint app (l1 l2 : natlist) : natlist :=
  match l1 with
  | nil ? l2
  | h :: t ? h :: (app t l2)
  end.

由于下文中 app 隨處可見，不妨將其定義為中綴運算符。

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).
Example test_app1: [1;2;3] ++ [4;5] = [1;2;3;4;5].
Proof. reflexivity. Qed.
Example test_app2: nil ++ [4;5] = [4;5].
Proof. reflexivity. Qed.
Example test_app3: [1;2;3] ++ nil = [1;2;3].
Proof. reflexivity. Qed.

Head與Tail

下面介紹列表上的兩種運算：hd 函數返回列表的第一個元素（即“head”）； tl 函數返回列表除去第一個元素以外的部分（即“tail”）。由于空表沒有表頭， 我們必須傳入一個參數作為返回的默認值。

Definition hd (default:nat) (l:natlist) : nat :=
  match l with
  | nil ? default
  | h :: t ? h
  end.
Definition tl (l:natlist) : natlist :=
  match l with
  | nil ? nil
  | h :: t ? t
  end.
Example test_hd1: hd 0 [1;2;3] = 1.
Proof. reflexivity. Qed.
Example test_hd2: hd 0 [] = 0.
Proof. reflexivity. Qed.
Example test_tl: tl [1;2;3] = [2;3].
Proof. reflexivity. Qed.

用列表實現口袋（Bag）

bag（或者叫 multiset 多重集）類似于集合，只是其中每個元素都能出現不止一次。 口袋的一種可行的表示是列表。

Definition bag := natlist.

有關列表的論證

和數字一樣，有些列表處理函數的簡單事實僅通過化簡就能證明。

Theorem nil_app : ? l:natlist,
  [] ++ l = l.
Proof. reflexivity. Qed.

...由于 [] 被替換進了 app 定義中相應的“被檢”分支 （即經由匹配“仔細檢查”過值的表達式），整個匹配得以被簡化。

和數字一樣，有時對一個列表做分類討論（是否是空）是非常有用的。

Theorem tl_length_pred : ? l:natlist,
  pred (length l) = length (tl l).
Proof.
  intros l. destruct l as [| n l'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons n l' *)
    reflexivity. Qed.

在這里 nil 的情況能夠工作是因為定義了 tl nil = nil， 而 destruct 策略中 as 注解引入的兩個名字，n 和 l'，分別對應了 cons 構造子的兩個參數（正在構造的列表的頭和尾）。

然而一般來說，許多關于列表的有趣定理都需要用到歸納法來證明。

對列表進行歸納

比起對自然數的歸納，歸納證明 natlist 這樣的數據類型更加陌生。 不過基本思路同樣簡單。每個 Inductive 聲明定義了一組數據值， 這些值可以用聲明過的構造子來構造。

歸納定義的集合中元素的形式 '只能是' 構造子對其它項的應用。這一事實同時也給出了一種對歸納定義的集合進行論證的方法：一個自然數要么是 O，要么就是 S 應用到某個'更小'的自然數上；一個列表要么是 nil， 要么就是 cons 應用到某個數字和某個'更小'的列表上，諸如此類。

• 首先，證明當 l 為 nil 時 P l 成立。

• 然后，證明當 l 為 cons n l' 時 P l 成立，其中 n 是某個自然數，l' 是某個更小的列表，假設 P l' 成立.

由于較大的列表總是能夠分解為較小的列表，最終這個較小的列表會變成 nil，這兩點合在一起就完成了 P 對一切列表 l 成立的證明。下面是個具體的例子：

Theorem app_assoc : forall l1 l2 l3 : natlist,
  (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
Proof.
  intros l1 l2 l3. 
  induction l1 as [| n l1' IHl1'].
  - (* l1 = nil *)
    reflexivity.
  - (* l1 = cons n l1' *)
    simpl. 
    rewrite -> IHl1'. 
    reflexivity. 
Qed.

其使用自然語言描述為:

'定理'：對所有的列表 l1, l2, 和 l3， (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)。
'證明': 通過對 l1 使用歸納法。

首先, 假設 l1 = []。我們必須證明：
$$([] ++ l2) ++ l3 = [] ++ (l2 ++ l3)$$

這可以通過展開 ++ 的定義得到。

然后, 假設 l1 = n::l1'，有：
$$(l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3)$$

（歸納假設）。我們必須證明：
$$((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3)$$

根據 ++ 的定義, 上式等價于：
$$n :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3))$$

該式可通過我們的歸納假設立即證得。 ?

反轉列表

舉一個更加深入的例子來說明對列表的歸納證明：假設使用 app 來定義一個列表反轉函數 rev：

Fixpoint rev (l:natlist) : natlist :=
  match l with
  | nil ? nil
  | h :: t ? rev t ++ [h]
  end.
Example test_rev1: rev [1;2;3] = [3;2;1].
Proof. reflexivity. Qed.
Example test_rev2: rev nil = nil.
Proof. reflexivity. Qed.

為了比目前所見的證明多一點挑戰性， 來證明反轉一個列表不會改變它的長度。

Theorem rev_length_firsttry : ? l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l' IHl'].
  - (* l = nil *)
    reflexivity.
  - (* l = n :: l' *)
    (* 這種情況比較棘手。我們從一般的化簡開始。 *)
    simpl.
    (* 現在我們好像卡住了：目標是要證明涉及 ++ 的等式，
       但是我們在上下文和全局環境下并沒有任何有用的等式！
       通過用 IH 來重寫目標，我們可以推進一點... *)
    rewrite <- IHl'.
    (* ...但也僅此而已。 *)
Abort.

不妨單獨提出引理，闡述 ++ 與 length 形成的等式關系， 以從我們卡住的地方推進證明。

Theorem app_length : ? l1 l2 : natlist,
  length (l1 ++ l2) = (length l1) + (length l2).
Proof.
  (* 課上已完成 *)
  intros l1 l2. 
  induction l1 as [| n l1' IHl1'].
  - (* l1 = nil *)
    reflexivity.
  - (* l1 = cons *)
    simpl. 
    rewrite → IHl1'. 
    reflexivity. 
Qed.

現在可以完成最初的證明了。

Theorem rev_length : ? l : natlist,
  length (rev l) = length l.
Proof.
  intros l. induction l as [| n l' IHl'].
  - (* l = nil *)
    reflexivity.
  - (* l = cons *)
    simpl. 
    rewrite → app_length.
    simpl. 
    rewrite → IHl'. 
    rewrite plus_comm.
    reflexivity.
Qed.

'定理'：對于所有 l，length (rev l) = length l。
'證明'：首先，觀察到 length (l ++ [n]) = S (length l) 對一切 l 成立， 這一點可通過對 l 的歸納直接得到。
當 l = n'::l' 時，通過再次對 l 使用歸納， 然后同時使用之前觀察得到的性質和歸納假設即可證明。 ?

Search 搜索

我們已經見過很多需要使用之前證明過的結論（例如通過 rewrite）來證明的定理了。 但是在引用別的定理時，我們必須事先知道它們的名字。

當然，即使是已被證明的定理本身 我們都不能全部記住，更不用提它們的名字了。

Coq 的 Search 指令在這時就非常有用了。執行 Search foo 會讓 Coq 顯示所有涉及到 foo 的定理。

例如，去掉下面的注釋后， 會看到一個我們證明過的所有關于 rev 的定理的列表：

(*  Search rev. *)

Options 可選類型

假設我們想要寫一個返回某個列表中第 n 個元素的函數。如果我們為它賦予類型 nat → natlist → nat，那么當列表太短時我們仍須返回某個數...

Fixpoint nth_bad (l:natlist) (n:nat) : nat :=
  match l with
  | nil ? 42
  | a :: l' ? match n with
    | 0 ? a
    | S n' ? nth_bad l' n'
    end
  end.

這種方案并不好：如果 nth_bad 返回了 42，那么不經過進一步處理的話， 無法得知該值是否真的出現在了輸入中。

因為無法判斷是什么因素讓它返回了 42.它可能是列表過短時的返回值，同時也可能是（此時列表足夠長）在列表中找到的值

Inductive natoption : Type :=
  | Some (n : nat)
  | None.

可以修改前面 nth_bad 的定義，使其在列表太短時返回 None， 在列表足夠長且 a 在 n 處時返回 Some a。將這個新函數稱為 nth_error 來表明它可以產生帶錯誤的結果。

Fixpoint nth_error (l:natlist) (n:nat) : natoption :=
  match l with
  | nil ? None
  | a :: l' ? match n with
    | O ? Some a
    | S n' ? nth_error l' n'
    end
  end.
Example test_nth_error1 : nth_error [4;5;6;7] 0 = Some 4.
Example test_nth_error2 : nth_error [4;5;6;7] 3 = Some 7.
Example test_nth_error3 : nth_error [4;5;6;7] 9 = None.

Coq 的條件語句和其它語言中的一樣，不過加上了一點更為一般化的特性。

由于 bool 類型不是內建的，因此 Coq 實際上支持在'Any'帶有兩個構造子的， 歸納定義的類型上使用條件表達式。

當斷言（guard）求值為 Inductive 定義中的第一個構造子時，它被認為是真的；當它被求值到第二個構造子時， 則被認為是假的。

Fixpoint nth_error' (l:natlist) (n:nat) : natoption :=
  match l with
  | nil ? None
  | a :: l' ? if n =? O then Some a
    else nth_error' l' (pred n)
  end.

以下函數從 natoption 中取出一個 nat，在遇到 None 時它將返回提供的默認值。

Definition option_elim (d : nat) (o : natoption) : nat :=
  match o with
  | Some n' ? n'
  | None ? d
  end.

Partial Maps 偏映射

下面的例子演示了如何在 Coq 中定義基礎的數據結構。這是一個簡單的 '偏映射' 數據類型，它類似于大多數編程語言中的映射或字典數據結構。

首先，定義一個新的歸納數據類型 id 來用作偏映射的“鍵”。

Inductive id : Type :=
  | Id (n : nat).

本質上來說，id 只是一個數。但通過 Id 標簽封裝自然數來引入新的類型， 能讓定義變得更加可讀，同時也給了我們更多的靈活性。

還需要一個 id 的相等關系測試：

Definition eqb_id (x1 x2 : id) :=
  match x1, x2 with
  | Id n1, Id n2 ? n1 =? n2
  end.

現在定義偏映射的類型：

Inductive partial_map : Type :=
  | empty
  | record (i : id) (v : nat) (m : partial_map).

此聲明可以理解為：“有兩種方式可以構造一個 partial_map：
用構造子 empty 表示一個空的偏映射，
或將構造子 record 應用到一個鍵、一個值和一個既有的 partial_map 來構造一個帶“鍵-值”映射 的 partial_map。”

update 函數用于在部分映射中覆蓋給定的鍵以取締原值（如該鍵尚不存在， 則新建其記錄）。

Definition update (d : partial_map)
  (x : id) (value : nat) : partial_map :=
  record x value d.

最后，find 函數按照給定的鍵搜索一個 partial_map。若該鍵無法找到， 它就返回 None；若該鍵與 val 相關聯，則返回 Some val。 若同一個鍵被映到多個值，find 就會返回它遇到的第一個值。

Fixpoint find (x : id) (d : partial_map) : natoption :=
  match d with
  | empty ? None
  | record y v d' ? if eqb_id x y
    then Some v
    else find x d'
  end.