Coq基础(三)

定义元组

其实在Coq基础(一)中的NewTypeFromOld中就已经定义过一个叫做nybble类型的元组了，那个类型的元组有四个bit类型的成员，构造器为bits。而这里再次定义一个只有两个自然数类型成员的元组：

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

Check (pair 3 5).

 在这个元组类型上定义函数：

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

(** The new pair notation can be used both in expressions and in
pattern matches. *)

Compute (fst (3,5)).

(* ===> 3 *)

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.

 证明建立在这个元组类型上的推论：

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

 一些更加复杂的推论：

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

这里需要注意的是，在对于自然数(nat)类型的变量使用[destruct]关键字的时候是：destruct n as [| n']，而在这里对元组(natprod)使用[destruct]关键字的时候却是：destruct p as [n m]。

造成这两种类型之间的区别的原因是其相应类型的构造器（或者称为构造函数）不一样：

• 自然数的构造器是 S ，如果S没有参数，则为O，对应的自然数为0；如果S有参数n'，其中n‘是自然数，则相应的构造为S n’，而S n'也是自然数。
• 而元组的构造器是pair，当构造一个元组类型的变量时，构造器pair都必须接收两个参数。

所以语句destruct n as [| n']所表达的含义就是将n分情况讨论：n 是由 S 在不接受输入的情况下构造；或者 n 是由构造器 S 在接收输入 n' 的情况下构造的。

也就是说关键字[destruct]是通过讨论变量的构造器接收参数的情况来实现“case analysis”的功能的。

定义链表

这里所定义的链表是自然数类型的链表，也就是说链表中的元素都是自然数。

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

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

natlist类型的元素有两个构造器，一个是nil，这个构造器不需要参数；另一个构造器是cons，这个构造器需要两个参数，一个自然数类型的参数，一个natlist类型的链表。

在这个链表类型的变量上定义一些比较常见的函数：

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

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

(** Since [app] will be used extensively in what follows, it is
    again convenient to have an infix operator for it. *)

Notation "x ++ y" := (app x y)
                     (right associativity, at level 60).

还可以定义一些其他的函数：

Fixpoint countoddmembers (l:natlist) : nat :=
  match l with
  | nil => O
  | h :: t =>if oddb h then S (countoddmembers t) else countoddmembers t
  end.
Example test_countoddmembers1:
  countoddmembers [1;0;3;1;4;5] = 4.
Proof. reflexivity. Qed.

　Fixpoint alternate (l1 l2 : natlist) : natlist :=
　match l1,l2 with
　| nil,_ => l2
　| _,nil => l1
　| h :: t, h' :: t' => h :: h' :: (alternate t t')
　end.

　Example test_alternate1:
　alternate [1;2;3] [4;5;6] = [1;4;2;5;3;6].
　Proof. reflexivity. Qed. 

同样的，也能在链表类型的变量上进行推论：

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

正如前面所讲的那样，关键字[destruct] 和 [induction] 都是通过分析变量的构造器来进行分情况讨论和归纳假设的，而链表类型的变量有两个构造器：nil 和 cons，第一个不需要参数，第二个需要两个参数，所以在使用前面那两种关键字进行证明的时候也与所做过的变量不同：

Fixpoint remove_one (v:nat) (s:bag) : bag :=
  match s with
  | nil => nil
  | h :: t => if (eqb h v) then t
              else h::(remove_one v t)
  end.

Theorem remove_does_not_increase_count: forall (s : bag),
  (count 0 (remove_one 0 s)) <=? (count 0 s) = true.
Proof.
intros s. induction s as [| n l' IHl'].
-reflexivity.
-destruct n as [| n'].
 +simpl. rewrite leb_n_Sn. reflexivity.
 +simpl. rewrite IHl'. reflexivity.
Qed.

定义natoption

这里要定义一个新的变量，叫做natoption，这并不是某个特殊的数据结构。

假设要构造一个函数，输入一个自然数 n 和一个链表 l ，返回链表中的第 n 个元素，通常会这样定义：

Fixpoint nth_bad (l:natlist) (n:nat) : nat :=
  match l with
  | nil => 42  (* arbitrary! *)
  | a :: l' => match n =? O with
               | true => a
               | false => nth_bad l' (pred n)
               end
  end.

如果链表中不存在第 n 个元素，那么这个函数会返回一个某个默认的自然数。但是这样并不是好的定义方法：并不能从结果中看出函数返回的结果是链表 l 中的第 n 个自然数还是默认的自然数，因为它们都是自然数。

为了优化这个函数，需要定义一个新的变量：

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

这个变量有两个构造器，一个是Some，这个构造器带有一个自然数类型的参数；另一个构造器是None，不带参数。

所以可以利用natoption来重新定义上面的函数：

Fixpoint nth (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类型变量的函数：

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

定义一个PartitialMap

除了前面为了某个特定功能所定义的natoption以外，还可以定义一些别的使用且常见的数据结构。

PartitialMap类似与PHP中的关联数组，也就是说PartitialMap本身也是一个链表，但是访问这个链表中的元素时并不是依靠元素的下标（即在链表中的位置）进行访问，而是依靠某个和该元素相关联的数据。

首先需要定义一个 id 变量类型，依靠这个类型的变量来访问 PartitialMap 中的元素。

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

然后可以再在这个基础上定义PartitialMap：

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

Check empty.
Check record (Id 0) 12 empty.
Check record (Id 1) 13 (record (Id 2) 14 empty).

这个类型的变量有两个构造器，第一个构造器没有参数，第二个构造器有三个参数。

而PartitialMap可以更直观地理解为是一个以二元元组为元素的链表结构。

然后可以在这种类型的变量上定义一些常见的函数：

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


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.