好久沒寫隨筆了,隨便投投.這里的內容主要取至《軟件基礎》第一卷https://coq-zh.github.io/.

我補充了一部分習題的答案,在https://github.com/mesonoxian-yao/softwareFoudations-volume1-coqLearn可以看看.

Software Foundations Vol.I : Coq函數式編程(Basics)

---

數據與函數

枚舉類型

Coq 的一個不同尋常之處在于它'極小'的內建特性集合。 比如，Coq 并未提供通常的原語（atomic）類型（如布爾、整數、字符串等）， 而是提供了一種極為強大的，可以從頭定義新的數據類型的機制 —— 上面所有常見的類型都是由它定義而產生的實例。

當然，Coq 發行版同時也提供了內容豐富的標準庫，其中定義了布爾值、 數值，以及如列表、散列表等許多通用的數據結構。 不過這些庫中的定義并沒有任何神秘之處，也沒有原語（Primitive）的特點。 為了說明這一點，我們并未在本課程中直接使用標準庫中的數據類型， 而是在整個教程中重新定義了其中的絕大部分。

下面是一個例子,說明了Coq中如何使用Inductive與Definition:

Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

Definition next_weekday (d:day) : day :=
  match d with
  | monday ? tuesday
  | tuesday ? wednesday
  | wednesday ? thursday
  | thursday ? friday
  | friday ? monday
  | saturday ? monday
  | sunday ? monday
  end.

Inductive: 其中,Inductive通過歸納聲明了一個Type,類似于如下:

Inductive type_name:Type:=
  | x1
  | x2.

Definition: Definition為聲明各類函數與關系提供了途徑:

Definition func(para:type_name):=
  match para with
  | x1=>x2
  end.

而為了計算函數,下面的例子展示了如何使用Compute代入函數:

Compute (next_weekday friday).
(* ==> monday : day *)
Compute (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)

Compute: Compute把右側的參數提供給左側的函數:

Compute (func x1).

下面的例子為我們揭示了如何使用Example來表示某個猜想,并且通過Proof證明它:

Example test_next_weekday:
  (next_weekday (next_weekday saturday)) = tuesday.
Proof. simpl. reflexivity. Qed.

布爾值

下面綜合上面的語法,為邏輯謂詞及布爾值運算相關內容提供了案例.

布爾型類型聲明如下:

Inductive bool : Type :=
  | true
  | false.

謂詞定義如下:

Definition negb (b:bool) : bool :=
  match b with
  | true ? false
  | false ? true
  end.
Definition andb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true ? b2
  | false ? false
  end.
Definition orb (b1:bool) (b2:bool) : bool :=
  match b1 with
  | true ? true
  | false ? b2
  end.

這里需要注意的是,對于coq,有以下語法對應關系:

• ?: =>
• →: ->
• ?: <->
• ?: exists
• ?!: exists!
• ?: forall
• ?!: forall!
• ∧: /\
• ∨: /
• ≠: <>
• ×: *

下面是一些附加的驗證:

Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. simpl. reflexivity. Qed.

同時,下面通過Notation指令為既定的定義提供了新的符號記法.

Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).
Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.

Notation: 通過Notation對已有定義進行簡化處理.

Notation "- x" := (func x).
Example test_example2 : -x1=x2.
Proof. simpl. reflexivity. Qed.

值得注意的是,在雙引號中,能夠與變量組合的符號應該是coq內部支持的,而非自己定義.

類型

Coq 中的每個表達式都有類型，它描述了該表達式所計算的東西的類別。 Check 指令會讓 Coq 顯示一個表達式的類型。

Check true.
(* ===> true : bool *)

如果在被 Check 的表達式后加上一個分號和你想驗證的類型，那么 Coq 會 驗證該表達式是否屬于你提供的類型。當兩者不一致時，Coq 會報錯并終止執行。

Check true:bool.
Check (negb true):bool.

像 negb 這樣的函數本身也是數據值，就像 true 和 false 一樣。 它們的類型被稱為'函數類型'，用帶箭頭的類型表示。

Check negb:bool->bool.

negb 的類型寫作 bool → bool，讀做“bool 箭頭 bool”， 可以理解為“給定一個 bool 類型的輸入，該函數產生一個 bool 類型的輸出。” 同樣，andb 的類型寫作 bool → bool → bool，可以理解為 “給定兩個 bool 類型的輸入，該函數產生一個 bool 類型的輸出。”

由舊類型構造新類型

下面是通過Constructor構造新類型的方式:

Inductive rgb : Type :=
  | red
  | green
  | blue.
Inductive color : Type :=
  | black
  | white
  | primary (p : rgb).

其中primary為Constructor表達式.

• 我們從有限的一組'構造子'開始。例如 red、primary、true、false、monday 等等都是構造子。
• '構造子表達式'通過將構造子應用到一個或多個構造子表達式上構成。例如 red、true、primary、primary red、red primary、red true、 primary (primary primary) 等等
• 每個 Inductive 定義都刻畫了一個構造子表達式的子集并賦予了它們名字，如 bool、rgb 或 color。

具體來說，rgb 和 color 的定義描述了如何構造這兩個集合中的構造子表達式：

• 構造子表達式 red、green 和 blue 屬于集合 rgb；
• 構造子表達式 black 和 white 屬于集合 color；
• 若 p 是屬于 rgb 的構造子表達式，則 primary p（讀作“構造子 primary 應用于參數 p）是屬于集合 color 的構造子表達式；且
• 通過這些方式構造的構造子表達式'只屬于'集合 rgb 和 color。

我們可以像之前的 day 和 bool 那樣用模式匹配為 color 定義函數。

Definition monochrome (c : color) : bool :=
  match c with
  | black ? true
  | white ? true
  | primary p ? false
  end.

鑒于 primary 構造子接收一個參數，匹配到 primary 的模式應當帶有一個 變量或常量。變量可以取任意名稱，如上文所示；常量需有適當的類型，例如：

Definition isred (c : color) : bool :=
  match c with
  | black ? false
  | white ? false
  | primary red ? true
  | primary _ ? false
  end.

其中_為通配的啞(dummy)變量

元組

一個多參數的單構造子可以用來創建元組類型,下面提供了一個例子,其描述了使用半字節表示四個比特:

Inductive bit : Type :=
  | B0
  | B1.
Inductive nybble : Type :=
  | bits (b0 b1 b2 b3 : bit).
Check (bits B1 B0 B1 B0)
    : nybble.

這里的 bit 構造子起到了對它內容的包裝作用。 解包可以通過模式匹配來實現

Definition all_zero (nb : nybble) : bool :=
  match nb with
    | (bits B0 B0 B0 B0) ? true
    | (bits _ _ _ _) ? false
  end.
Compute (all_zero (bits B1 B0 B1 B0)).
(* ===> false : bool *)
Compute (all_zero (bits B0 B0 B0 B0)).
(* ===> true : bool *)

模塊

如果將一組定義放在 Module X 和 End X 標記之間，那么在文件中的 End 之后，我們就可以通過像 X.foo 這樣的名字來引用，而不必直接用 foo 了

Module logic_sys.

End logic_sys.

Module: 使用Module可以創建模塊來管理聲明定義:

Module logic_sys.
(*...*)
End logic_sys.

Compute (logic_sys.func logic_sys.x1).

數值

枚舉集合都是有限的,而一般自然數都是無限的,為了表示自然數,需要用一種更強大的方式聲明它們.

為了在 Coq 中表示一進制數，我們使用兩個構造子。 大寫的 O 構造子用來表示“零”

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

在這種定義下， 0 被表示為 O, 1 則被表示為 S O, 2 則是 S (S O)，以此類推

也可以把 O 寫為 tick,這些記號的'解釋'完全取決于我們如何用它進行計算。

Inductive nat' : Type :=
  | stop
  | tick (foo : nat').

編寫一個函數來對上述自然數的表示進行模式匹配。 例如，以下為前趨函數

Definition pred (n : nat) : nat :=
  match n with
    | O ? O
    | S n' ? n'
  end.

第二個分支可以讀作：“如果 n 對于某個 n' 的形式為 S n'， 那么就返回 n'。”

為了讓自然數使用起來更加自然，Coq 內建了一小部分解析打印功能： 普通的十進制數可視為“一進制”自然數的另一種記法，以代替 S 與 O 構造子； 反過來，Coq 也會默認將自然數打印為十進制形式：

Check (S (S (S (S O)))).
(* ===> 4 : nat *)

Definition minustwo (n : nat) : nat :=
  match n with
    | O ? O
    | S O ? O
    | S (S n') ? n'
  end.

Compute (minustwo (S (S (S (S O))))).
(* ===> 2 : nat *)

注意:現在上面描述的內容必須通過Datatypes.nat來實現了.

構造子 S 的類型為 nat → nat，與 pred 和 minustwo 之類的函數相同：

Check S : nat→nat.
Check pred : nat→nat.
Check minustwo : nat→nat.

以上三個對象均可作用于自然數，并產生nat結果，但第一個 S 與后兩者有本質區別：pred 和 minustwo 這類函數是通過給定的'計算規則'定義的

簡單的模式匹配不足以描述很多有趣的數值運算，我們還需要遞歸定義。 例如：給定自然數 n，欲判定其是否為偶數，則需遞歸檢查 n-2 是否為偶數。 關鍵字 Fixpoint 可用于定義此類函數。

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O ? true
  | S O ? false
  | S (S n') ? evenb n'
  end.

Fixpoint: 通過Fixpoint,可以在函數中遞歸地使用函數來聲明.

Fixpoint fix_func(para:type_name):type_name:=
  match para with
  | x1=>x2
  | x2=>x1
  | y x1=>x1
  | y x2=>x2
  | y (y n)=>(fix_func n)
  end.

Compute (fix_func (y(y(y(y(x1)))))).
(*logic_sys.x2:logic_sys.type_name*)

我們可以使用類似的 Fixpoint 聲明來定義 odd 函數， 不過還有種更簡單方式：

Definition oddb (n:nat) : bool :=
  negb (evenb n).
Example test_oddb1: oddb (S O) = true.
Proof. simpl. reflexivity. Qed.
Example test_oddb2: oddb (S (S (S (S O)))) = false.
Proof. simpl. reflexivity. Qed.

當然，也可以用遞歸定義多參函數。

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
    | O ? m
    | S n' ? S (plus n' m)
  end.

三加二等于五，不出意料。

Compute (plus (S (S (S O))) (S (S O))).
(* ===> 5 : nat *)

Coq 所執行的化簡步驟如下所示：

(*   plus 3 2
i.e. plus (S (S (S O))) (S (S O))
 ==> S (plus (S (S O)) (S (S O)))
      （根據第二個 match 子句）
 ==> S (S (plus (S O) (S (S O))))
      （根據第二個 match 子句）
 ==> S (S (S (plus O (S (S O)))))
      （根據第二個 match 子句）
 ==> S (S (S (S (S O))))
      （根據第一個 match 子句）
i.e. 5  *)

為了書寫方便，如果兩個或更多參數具有相同的類型，那么它們可以寫在一起。

在下面的定義中，(n m : nat) 的意思與 (n : nat) (m : nat) 相同。

Fixpoint mult (n m : nat) : nat :=
  match n with
    | O ? O
    | S n' ? plus m (mult n' m)
  end.

Example test_mult1: (mult (S (S (S O))) (S (S (S O)))) 
  = (S (S (S (S (S (S (S (S (S O))))))))).
Proof. simpl. reflexivity. Qed.

你可以在兩個表達式之間添加逗號來同時匹配它們：

Fixpoint minus (n m:nat) : nat :=
  match n, m with
  | O , _ ? O
  | S _ , O ? n
  | S n', S m' ? minus n' m'
  end.
End NatPlayground2.
Fixpoint exp (base power : nat) : nat :=
  match power with
    | O ? S O
    | S p ? mult base (exp base p)
  end.

可以通過引入加法、乘法和減法的Notation來讓數字表達式更加易讀。

Notation "x + y" := (plus x y)
                       (at level 50, left associativity)
                       : nat_scope.
Notation "x - y" := (minus x y)
                       (at level 50, left associativity)
                       : nat_scope.
Notation "x * y" := (mult x y)
                       (at level 40, left associativity)
                       : nat_scope.
Check ((0 + 1) + 1) : nat.

（level、associativity 和 nat_scope 標記控制著 Coq 語法分析器如何處理上述記法。

Coq 幾乎不包含任何內置定義，甚至連數值間的相等關系都是由用戶來實現。

Fixpoint eqb (n m : nat) : bool :=
  match n with
  | O ? match m with
         | O ? true
         | S m' ? false
         end
  | S n' ? match m with
            | O ? false
            | S m' ? eqb n' m'
            end
  end.

上面的例子既為我們提供了一個多分支match1的很好的例子,又為我們提供了一個用于說明eq關系的案例

類似地，leb 函數檢驗其第一個參數是否小于等于第二個參數，以布爾值表示。

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O ? true
  | S n' ?
      match m with
      | O ? false
      | S m' ? leb n' m'
      end
  end.
Example test_leb1: leb 2 2 = true.
Proof. simpl. reflexivity. Qed.
Example test_leb2: leb 2 4 = true.
Proof. simpl. reflexivity. Qed.
Example test_leb3: leb 4 2 = false.
Proof. simpl. reflexivity. Qed.

提供一種中綴記法:

Notation "x =? y" := (eqb x y) (at level 70) : nat_scope.
Notation "x <=? y" := (leb x y) (at level 70) : nat_scope.

Example test_leb3': (4 <=? 2) = false.
Proof. simpl. reflexivity. Qed.

基于化簡的證明

前幾節中的每個 Example 都對幾個函數在某些特定輸入上的行為做出了準確的斷言。這些斷言的證明方法都一樣： 使用 simpl 來化簡等式兩邊，然后用 reflexivity 來檢查兩邊是否具有相同的值。

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
  intros n. simpl. reflexivity. Qed.

在前面的例子中，其實并不需要調用 simpl ，因為 reflexivity 在檢查等式兩邊是否相等時會自動做一些化簡,simpl 只是為了看到中間狀態

在 Coq 中，關鍵字 Example 和 Theorem（以及 Lemma、Fact 和 Remark等）都表示完全一樣的東西。

關鍵字 intros、simpl 和 reflexivity 都是'策略（Tactic）'的例子。 策略是一條可以用在 Proof（證明）和 Qed（證畢）之間的指令，它告訴 Coq 如何來檢驗我們所下的一些斷言的正確性。

其它類似的定理可通過相同的模式證明。

Theorem plus_1_l : ? n:nat, 1 + n = S n.
Proof.
  intros n. reflexivity. Qed.
Theorem mult_0_l : ? n:nat, 0 × n = 0.
Proof.
  intros n. reflexivity. Qed.

上述定理名稱的后綴 _l 讀作“在左邊”。

基于改寫的證明

該定理并未對自然數 n 和 m 所有可能的值做全稱斷言，而是討論了僅當 n = m 時這一更加特定情況。箭頭符號讀作“蘊含”。

Theorem plus_id_example : ? n m:nat,
  n = m →
  n + n = m + m.

由于n與m都為nat,所以無法通過形式上的簡化來證明此定理,因此,觀察發現,若將n替換為m或m替換為n,那么就可以證明,這種策略被叫做rewrite.

Proof.
  (* 將兩個量詞移到上下文中： *)
  intros n m.
  (* 將前提移到上下文中并改寫為H *)
  intros H.
  (* 用前提改寫目標： *)
  rewrite → H.
  reflexivity. Qed.

rewrite 中的箭頭與蘊含無關：它指示 Coq 從左往右地應用改寫。 若要從右往左改寫，可以使用 rewrite <-

intros: intros用于將量詞,前提引入到上下文中.同時,也可以將形如a->b結構的a拆分出來作為H.

Theorem th1 : forall n:nat,
    n = n ->
    n = n.
Proof.
    intros n.
    reflexivity.
Qed.

Admitted 指令告訴 Coq 我們想要跳過此定理的證明，而將其作為已知條件， 這在開發較長的證明時很有用。

Admitted: 告訴coq,此處的證明作為已知條件.

Check 命令也可用來檢查以前聲明的引理和定理。

Check: 用于判斷類型,斷言,引理,定理等是否正確.

Check mult_n_O.
(* ===> forall n : nat, 0 = n * 0 *)
Check mult_n_Sm.
(* ===> forall n m : nat, n * m + n = n * S m *)

除了上下文中現有的假設外，還可以通過 rewrite 策略來運用前期證明過的定理。

如果前期證明的定理的語句中包含量詞變量，Coq 會通過匹配當前的證明目標來嘗試實例化（Instantiate）它們。

Theorem mult_n_0_m_0 : ? n m : nat,
  (n × 0) + (m × 0) = 0.
Proof.
  intros n m.
  rewrite <- mult_n_O.
  rewrite <- mult_n_O.
  reflexivity. Qed.

利用分類討論來證明

并非一切都能通過簡單的計算和改寫來證明,未知的、假定的值,如數值、布爾值、列表等會阻礙化簡。

例如:

Theorem plus_1_neq_0_firsttry : ? n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros n.
  simpl. (* 無能為力! *)
Abort.

這里通過Abort來放棄證明.

原因在于：根據 eqb 和 + 的定義，其第一個參數先被 match 匹配。 但此處 + 的第一個參數 n 未知，而 eqb 的第一個參數 n + 1 是復合表達式，二者均無法化簡。

欲進行規約，則需分情況討論 n 的所有可能構造。告訴 Coq 分別對 n = 0 和 n = S n' 這兩種情況進行分析的策略，叫做 destruct。

Theorem plus_1_neq_0 : ? n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros n. destruct n as [| n'] eqn:E.
  - reflexivity.
  - reflexivity. Qed.

eqn:E記號告知Coq以E來命名這些假設.destruct 策略會生成兩個子目標,我們必須接下來證明這兩個子目標。

eqn: 對相關假設進行命名

destruct: 通過destruct來構造子證明對目標constructor進行分類討論的策略

as [| n'] 這種標注被稱為 '引入模式'。它告訴 Coq 應當在每個子目標中 使用什么樣的變量名。總體而言，在方括號之間的是一個由 | 隔開的 '列表的列表'（譯者注：list of lists）。

在上面的例子中，第一個元素是 一個空列表，因為 O 構造子是一個空構造子（它沒有任何參數）

第二行和第三行中的 - 符號叫做'標號'，它標明了這兩個生成的子目標所對應的證明部分。

destruct 策略可用于任何歸納定義的數據類型，下面證明對布爾值而言取反是自身的逆運算

Theorem negb_involutive : ? b : bool,
  negb (negb b) = b.
Proof.
  intros b. destruct b eqn:E.
  - reflexivity.
  - reflexivity. 
Qed.

這里的 destruct 沒有 as 子句，因為此處 destruct 生成的子分類均無需綁定任何變量

有時在一個子目標內調用 destruct，產生出更多的證明義務（Proof Obligation） 也非常有用。這時候，我們使用不同的標號來標記目標的不同“層級”，比如：

Theorem andb_commutative : ? b c, 
  andb b c = andb c b.
Proof.
  intros b c. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
Qed.

除了 - 和 + 之外，還可以使用 ×（星號）或任何重復的標號符（如 -- 或 ***）作為標號。我們也可以用花括號將每個子證明目標括起來：

Theorem andb_commutative' : ? b c, 
  andb b c = andb c b.
Proof.
  intros b c. 
  destruct b eqn:Eb.
  { destruct c eqn:Ec.
    { reflexivity. }
    { reflexivity. } }
  { destruct c eqn:Ec.
    { reflexivity. }
    { reflexivity. } }
Qed.

花括號還允許我們在一個證明中的多個層級下使用同一個標號。 使用大括號、標號還是二者結合都純粹是個人偏好問題。

Theorem andb3_exchange :
  ? b c d, andb (andb b c) d = andb (andb b d) c.
Proof.
  intros b c d. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
  - destruct c eqn:Ec.
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
    { destruct d eqn:Ed.
      - reflexivity.
      - reflexivity. }
Qed.

在本章結束之前，我們最后再說一種簡便寫法。或許你已經注意到了， 很多證明在引入變量之后會立即對它進行情況分析：

       intros x y. destruct y as [|y] eqn:E.

這種寫法是如此的常見以至于 Coq 為它提供了一種簡寫：我們可以在引入 一個變量的同時對他使用'引入模式'來進行分類討論

Theorem plus_1_neq_0' : ? n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros [|n].
  - reflexivity.
  - reflexivity. 
Qed.

以下兩種形式是等價的:

intros x y. destruct y as [|y] eqn:E.

intros [|y].

如果沒有需要命名的constructor參數，我們只需寫上 [] 即可進行情況分析。

Theorem andb_commutative'' :
  ? b c, andb b c = andb c b.
Proof.
  intros [] [].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
Qed.

關于記法

回憶一下中綴加法和乘法的記法定義：

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

對于 Coq 中的每個記法符號，我們可以指定它的 '優先級' 和 '結合性'。 優先級 n 用 at level n 來表示.Coq 使用 0 到 100 的優先級等級，同時支持 '左結合'、'右結合' 和 '不結合' 三種結合性

每個記法符號還與 '記法范圍（Notation Scope）'相關。Coq 會嘗試根據上下文來猜測 你所指的范圍

不動點Fixpoint與結構化遞歸

以下是加法定義的一個副本：

Fixpoint plus' (n : nat) (m : nat) : nat :=
  match n with
  | O ? m
  | S n' ? S (plus' n' m)
  end.

當 Coq 查看此定義時，它會注意到“plus' 的第一個參數是遞減的”。 這意味著我們對參數 n 執行了'結構化遞歸'。

換言之，我們僅對嚴格遞減的 n 值進行遞歸調用。這一點蘊含了“對 plus' 的調用最終會停止”。

這項要求是 Coq 的基本特性之一，它保證了 Coq 中定義的所有函數對于所有輸入都會終止。