地图（或字典）是普遍存在的数据结构，尤其是在编程语言理论中；在接下来的章节中，我们将在许多地方需要它们。他们还利用我们在前几章中看到的思想做了一个很好的案例研究，包括用高阶函数构建数据结构（从基础和多边形）和使用反射来简化证明（从IndProp）。

我们将定义两种类型的映射：total maps（总映射）和partial maps（部分映射），前者包括在不存在要查找的键时返回的“默认”元素，后者返回一个指示成功或失败的选项。后者是根据前者定义的，使用None作为默认元素。

Coq标准库

在我们开始之前有一点离题。。。

与我们到目前为止看到的章节不同，本章不需要导入之前的章节（以及之前的所有章节）。相反，在本章以及从现在开始，我们将直接从Coq的标准库中导入我们需要的定义和定理。不过，您不应该注意到太多的差异，因为我们一直小心地将自己的定义和定理命名为与标准库中的对应定义和定理相同的名称，无论它们在哪里重叠。

From Coq Require Import Arith.Arith.
From Coq Require Import Bool.Bool.
Require Export Coq.Strings.String.
From Coq Require Import Logic.FunctionalExtensionality.
From Coq Require Import Lists.List.
Import ListNotations.

有关标准库的文档，请访问https://coq.inria.fr/library/.

搜索命令是查找涉及特定类型对象的定理的好方法。有关如何使用它的提示，请参见列表。

如果要了解符号是如何定义的或在何处定义的，则Locate命令非常有用。例如，标准库中定义的自然加法操作在哪里？

Locate "+".

这种符号有几种用途，但对自然只有一种。

Print Init.Nat.add.