定義一個類型
在coq中，一個變量的類型往往表示為 var_name : var_type，即變量名后面的一個冒號后是變量的類型
Inductive type_name : Type :=
constructor 1
constructor 2
...
constructor n. (*注意最后一個constructor的后面還有一個 . *)
即創建一個名為 type_name 的類型，該類型的變量的取值只能是{constructor 1, ..., constructor n}之中的一個。
eg：
Inductive day : Type := | monday | tuesday | wednesday | thursday | friday | saturday | sunday.
上面語句創建了一個名為 day 的類型，該類型中的變量取值范圍為：{monday，tuesday，wednesday，thursday，friday，saturday，sunday}
定義一個函數
有了類型，可以在這個類型上定義一個函數：
Definition func_name (agrv1 : type1, argv2 : type1...) : ret_type :=
match argv1 with
| case 1 => ret1
| case 2 => ret2
| ...
end.
創建一個函數名為func_name的函數，其形參分別為argv1，argv2，並且形參的變量類型分別為type1和type2，最后的返回值的類型為ret_type
eg：
Definition next_weekday (d:day) : day := match d with | monday => tuesday | tuesday => wednesday | wednesday => thursday | thursday => friday | friday => monday | saturday => monday | sunday => monday end.
Compute語句
定義好了函數之后，可以使用關鍵字Compute 來計算函數的返回值
Compute (next_weekday friday).
計算的結果為：monday : day
Example語句
eg：
Example test_next_weekday:
(next_weekday (next_weekday saturday)) = tuesday.
上面的語句會做兩件事：作出一個假設“Saturday后的兩個工作日是Tuesday”；然后賦予這個假設一個名稱，以便后面可以繼續參考。
在做出了假設之后，可以調用coq來進行驗證：
Proof. simpl. reflexivity. Qed.
上面的語句可以簡單的理解為：“剛才所做的斷言可以通過觀察等式兩邊經過某種簡化后得到相同的值來證明。”
New Type From Old
在定義一個新的類型的時候，也可以調用之前定義好了的類型：
Inductive bit : Type := | B0 | B1. Inductive nybble : Type := | bits (b0 b1 b2 b3 : bit).
(*上面的語句定義了一個元組類型*)
Check (bits B1 B0 B1 B0). (* ==> bits B1 B0 B1 B0 : nybble *)
在定義一個函數的時候可以調用其他函數來完成函數的功能，不過在調用其他函數的時候需要注意變量的類型需要與函數聲明中的類型保持一致
eg：
Inductive bool : Type := | true | false. Definition andb (b1:bool) (b2:bool) : bool := match b1 with | true => b2 | false => false end. Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool := match b1 with | true => andb b2 b3 | false => false end. Example test_andb31: (andb3 true true true) = true. Proof. simpl. reflexivity. Qed. Example test_andb32: (andb3 false true true) = false. Proof. simpl. reflexivity. Qed.
coq的函數定義是枚舉各個可能的case然后定義每個case下的返回值，但有時並不需要枚舉所有的case。這種情況下可以用 "_"符號來代替所有除了前面所枚舉過的case的其他case。
eg：
Inductive rgb : Type := | red | green | blue. Inductive color : Type := | black | white | primary (p : rgb). （*color類型是一個從已經定義好的類型上重新定義的新的類型*） （*color類型的變量可能的取值有： black, white, primary red, primary green, primary bule*） Definition isgreen (c: color) : bool := match c with | primary green => true | _ => false end.
Check語句
coq中的每個表達式都有相應的類型，用於描述其計算類型。可以使用check命令來調用coq打印一個表達式的類型
eg：
Definition negb (b:bool) : bool := match b with | true => false | false => true end. Check true. (*打印的內容為：true : bool*) Check (negb true). (*打印的內容為：negb true : bool*) Check negb. (*打印的內容為：negb : bool -> bool*)
定義自然數
幾乎前面所定義的所有類型都是通過枚舉定義的，這與此處所定義的自然數類型不同。因為並不能通過一個一個的枚舉自然數所有可能取的值，所以這里通過兩條規則來規約自然數類型的變量：
- 0是一個自然數，對應的自然數值為0
- 如果n‘是自然數，那么S n’就是自然數，對應的自然數值為n'+1
Module NatPlayground.
Inductive nat : Type := | O | S (n : nat).
End NatPlayground.
這樣的定義方法中：自然數 0 表示為[O]，1 表示為[S O]，2 表示為[S (S O)]，然后以此類推...
為了構造一個自然數的集合，上面的構造語句相當於定義了下面幾個構造規則：
- 函數[O] 和 [S] 是自然數集合[nat]的構造函數 ;
- 表達式[O]是集合 [nat]中的一個元素;
- 如果表達式[n]屬於集合[nat], 則表達式 [S n]也屬於集合[nat];
- 通過上面個兩條規則構造出來的表達式只屬於集合[nat].
由於自然數是一種非常普遍的數據類型，所以Coq為解析和打印提供了一點點內置的魔術類型，可以用普通的十進制數字來代替由構造函數[S]和[O]定義的“一元”符號。coq在默認情況下打印十進制數字:
Check (S (S (S (S O)))). (*打印結果為：4 : nat*)
在這樣的自然數定義下可以定義相應的函數：
Definition pred (n : nat) : nat := match n with | O => O | S n' => n' end. (** The second branch can be read: "if [n] has the form [S n'] for some [n'], then return [n']." *) Definition minustwo (n : nat) : nat := match n with | O => O | S O => O | S (S n') => n' end. Compute (minustwo 4). (* ===> 2 : nat *)
定義一個遞歸調用函數
在coq中定義遞歸調用的函數的語句與定義普通的函數的語句不同：定義遞歸調用的函數需要使用關鍵字Fixpoint來定義
Fixpoint func_name (argv1 : type1, argv2:type2...) : ret_type :=
match argv1 with
| case1 => ret1
| case2 => ret2
| ...
end.
eg:
Fixpoint evenb (n:nat) : bool := match n with | O => true | S O => false | S (S n') => evenb n' end. Fixpoint plus (n : nat) (m : nat) : nat := match n with | O => m | S n' => S (plus n' m) end. (** Adding three to two now gives us five, as we'd expect. *) Compute (plus 3 1). (** The simplification that Coq performs to reach this conclusion can be visualized as follows: *) (* [plus (S (S (S O))) (S (S O))] ==> [S (plus (S (S O)) (S (S O)))] by the second clause of the [match] ==> [S (S (plus (S O) (S (S O))))] by the second clause of the [match] ==> [S (S (S (plus O (S (S O)))))] by the second clause of the [match] ==> [S (S (S (S (S O))))] by the first clause of the [match] *)
Notation語句
coq中可以使用Notation來對某些函數進行重命名從而簡化運算語句
Notation語句類似於C語言中的 #Define 語句
eg：
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).
在Notation語句中的關鍵字[level]、[associativity]以及[nat_scope]用於描述Coq解釋程序如何處理這些Notation語句。
其中[level]數值越低，則運算的優先級越高；[associativity]解釋該運算操作是左結合還是右結合。
Notation語句並不會改變運算操作的定義，coq解釋程序會使用 [plus x y] 來代替[x+y]
定義遞歸函數時的復雜case
在定義函數的時候可以在一個變量里的case里面討論另一個變量的case，如下，定義一個自然數小於或等於的函數：
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.
定義遞歸函數的時候需要注意，case 的左邊的參數一定要嚴格的大於右邊的參數：
(*Fibonacc series*)
(*wrong definition!*） Fixpoint fibonacc (n:nat) : nat := match n with | S(S n') => plus (fibonacc n') (fibonacc (S n')) | _ => (S O) end.
(* error message: fibonacc : nat -> nat n : nat n0 : nat n' : nat Recursive call to fibonacc has principal argument equal to "S n'" instead of one of the following variables: "n0" "n'". *) (*correct definition*) Fixpoint fibonacc (n:nat) : nat := match n with | O => 1 | S n' => match n' with | O => 1 | S n'' => plus (fibonacc n') (fibonacc n'') end end. Example test_fibonacc1: (fibonacc 2) = 2. Proof. simpl. reflexivity. Qed. Example test_fibonacc2: (fibonacc 5) = 8. Proof. simpl. reflexivity. Qed.