总地图
本章中我们的主要工作是建立一个部分映射的定义,该定义在行为上与我们在列表一章中看到的部分映射相似,另外还有关于其行为的伴随引理。
不过,这次我们将使用函数而不是键值对列表来构建映射。这种表示法的优点是它提供了一个更为扩展的映射视图,其中以相同方式响应查询的两个映射将被表示为字面上相同的东西(非常相同的函数),而不仅仅是“等效”的数据结构。这反过来又简化了使用地图的证明。
我们分两步构建部分映射。首先,我们定义一种类型的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.