局部映射 Partial Maps

作为在Coq中如何定义数据结构的最后一个例子，这里有一个simple _partial map_data类型，类似于大多数编程语言中的map或dictionary数据结构。

首先，我们定义一个新的归纳数据类型id作为部分映射的“键”。

Inductive id

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

在内部，id只是一个数字。通过使用标记Id包装每个nat，引入一个单独的类型，使定义更具可读性，并为我们提供了更大的灵活性。

我们还需要对ids进行平等性测试：

Definition eqb_id

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

现在我们定义部分映射的类型：

Inductive partial_map

Module PartialMap.
Export NatList.

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

该声明可以理解为：“有两种方法可以构造部分映射：使用构造函数empty来表示空的部分映射，或者将构造函数记录应用于键、值和现有的部分映射来构造具有附加键到值映射的部分映射。”

update函数通过使用新项对局部映射中的给定项进行阴影覆盖来覆盖该项（如果给定项尚未存在，则只需添加一个新项）。

Definition update

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

最后，find函数在局部映射中搜索给定的键。如果找不到键，则返回None；如果键与val关联，则返回某个val。如果同一键映射到多个值，则find将返回它遇到的第一个值。

Fixpoint 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.

41: 1 star, standard (eqb_id_refl)

Theorem eqb_id_refl

Theorem eqb_id_refl : forall x, eqb_id x x = true.
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Search (?n =? ?n).
Theorem eqb_id_refl : forall x, eqb_id x x = true.
Proof.
intros []. induction n as [| n' IHn'].
- simpl. reflexivity.
- simpl. rewrite -> eqb_refl. reflexivity.
Qed.

42: 1 star, standard (update_eq)

Theorem update_eq

Theorem update_eq :
forall (d : partial_map) (x : id) (v: nat),
  find x (update d x v) = Some v.
Proof.
(* FILL IN HERE *) Admitted.

Coq代码

Theorem update_eq :
forall (d : partial_map) (x : id) (v: nat),
  find x (update d x v) = Some v.
Proof.
intros d x v.
simpl. rewrite -> eqb_id_refl.
reflexivity.
Qed.

43: 1 star, standard (update_neq)

Theorem update_neq

Theorem update_neq :
forall (d : partial_map) (x y : id) (o: nat),
  eqb_id x y = false -> find x (update d y o) = find x d.
Proof.
(* FILL IN HERE *) Admitted.

End PartialMap.

Coq代码

Theorem update_neq :
forall (d : partial_map) (x y : id) (o: nat),
  eqb_id x y = false -> find x (update d y o) = find x d.
Proof.
intros d x v o.
intros H.
simpl. rewrite -> H.
reflexivity.
Qed.

44: 2 stars, standard, optional (baz_num_elts)

考虑下面的归纳定义：

Inductive baz : Type :=
  | Baz1 (x : baz)
  | Baz2 (y : baz) (b : bool).

baz类型有多少个元素？（用文字或评论进行解释。）

(* FILL IN HERE *)

(* Do not modify the following line: *)
Definition manual_grade_for_baz_num_elts : option (nat*string) := None.