总地图

本章中我们的主要工作是建立一个部分映射的定义，该定义在行为上与我们在列表一章中看到的部分映射相似，另外还有关于其行为的伴随引理。

不过，这次我们将使用函数而不是键值对列表来构建映射。这种表示法的优点是它提供了一个更为扩展的映射视图，其中以相同方式响应查询的两个映射将被表示为字面上相同的东西（非常相同的函数），而不仅仅是“等效”的数据结构。这反过来又简化了使用地图的证明。

我们分两步构建部分映射。首先，我们定义一种类型的total maps，当我们查找map中不存在的键时，它将返回一个默认值。

Definition total_map (A : Type) := string -> A.

直观地说，元素类型A上的总映射只是一个可用于查找字符串的函数，产生如下结果。

函数t_empty在给定默认元素的情况下生成一个空的总映射；当应用于任何字符串时，此映射始终返回默认元素。。

Definition t_empty {A : Type} (v : A) : total_map A :=
  (fun _ => v).

更有趣的是update函数，它（像以前一样）获取一个映射m、一个键x和一个值v，并返回一个新映射，该映射将x带到v，并将每个其他键带到m所做的任何事情。

Definition t_update {A : Type} (m : total_map A)
                    (x : string) (v : A) :=
  fun x' => if eqb_string x x' then v else m x'.

这个定义是高阶编程的一个很好的例子：t_update接受一个函数m并产生一个新函数fun x'⇒ ... 其行为类似于所需的贴图。

例如，我们可以构建一个将字符串映射到bools的映射，其中“foo”和“bar”映射为true，其他每个键映射为false，如下所示：

Definition examplemap :=
  t_update (t_update (t_empty false) "foo" true)
           "bar" true.

接下来，让我们介绍一些新的符号，以便于使用地图。

首先，我们将使用以下符号创建一个带有默认值的空total map。

Notation "'_' '!->' v" := (t_empty v)
  (at level 100, right associativity).
  
  Example example_empty := (_ !-> false).

然后，我们引入一种方便的表示法，用于使用一些绑定扩展现有映射。

Notation "x '!->' v ';' m" := (t_update m x v)
                              (at level 100, v at next level, right associativity).

上面的examplemap现在可以定义如下：

Definition examplemap' :=
  ( "bar" !-> true;
    "foo" !-> true;
    _     !-> false
  ).

这就完成了总地图的定义。注意，我们不需要定义find操作，因为它只是一个函数应用程序！

Example update_example1 : examplemap' "baz" = false.
Proof. reflexivity. Qed.

Example update_example2 : examplemap' "foo" = true.
Proof. reflexivity. Qed.

Example update_example3 : examplemap' "quux" = false.
Proof. reflexivity. Qed.

Example update_example4 : examplemap' "bar" = true.
Proof. reflexivity. Qed.

为了在后面的章节中使用地图，我们需要一些关于它们行为的基本事实。

即使你没有做下面的练习，也要确保你完全理解引理的陈述！

（有些证明需要函数可拓性公理，这将在逻辑一章中讨论。）

Exercise: 1 star, standard, optional (t_apply_empty)

首先，空映射返回所有键的默认元素：

Lemma t_apply_empty : forall (A : Type) (x : string) (v : A),
  (_ !-> v) x = v.
Proof.
  (* FILL IN HERE *) Admitted.

Solution

Exercise: 2 stars, standard, optional (t_update_eq)

接下来，如果我们用新值v更新键x处的映射m，然后在更新后的映射中查找x，则返回v：

Lemma t_update_eq : forall (A : Type) (m : total_map A) x v,
  (x !-> v ; m) x = v.
Proof.
  (* FILL IN HERE *) Admitted.

Solution

Exercise: 2 stars, standard, optional (t_update_neq)

另一方面，如果我们在键x1处更新映射m，然后在结果映射中查找不同的键x2，我们将得到与m相同的结果：

Theorem t_update_neq : forall (A : Type) (m : total_map A) x1 x2 v,
  x1 <> x2 ->
  (x1 !-> v ; m) x2 = m x2.
Proof. 
  (* FILL IN HERE *) Admitted.

Solution