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 ⇒ xend.
Definition snd (p : natprod) : nat :=match p with| pair x y ⇒ yend.
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) ⇒ xend.
Definition snd' (p : natprod) : nat :=match p with| (x,y) ⇒ yend.
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 ⇒ xend.(* 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 ⇒ hend.
Definition tl (l:natlist) : natlist :=match l with| nil ⇒ nil| h :: t ⇒ tend.
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'endend.
这种方案并不好：如果 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'endend.
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 aelse nth_error' l' (pred n)end.
以下函数从 natoption 中取出一个 nat，在遇到 None 时它将返回提供的默认值。
Definition option_elim (d : nat) (o : natoption) : nat :=match o with| Some n' ⇒ n'| None ⇒ dend.
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 =? n2end.
现在定义偏映射的类型：
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 ythen Some velse find x d'end.
)
)
