总地图

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

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

我们分两步构建部分映射。首先,我们定义一种类型的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