dictionary - 在 Coq 中创建字典/ map

Question

我希望能够在 Coq 中拥有从任何类型到任何类型的映射。到目前为止，我使用标准库中的 Coq.FSets.FMapList 取得了一些成功，但我只能通过执行以下操作来创建键为自然数的映射。

Require Import Coq.FSets.FMapList.
Require Import Coq.Structures.OrderedTypeEx.

Module Import NatMap := FMapList.Make(Nat_as_OT).

(* whatever I want to do with my NatMap *)

我知道 NatMap := FMapList.Make(Nat_as_OT). 声明我想使用键为 Nat_as_OT 的 map 。但是，FMapList.Make 将只接受一个 OrderedType 作为参数。有没有办法让我自己制作 OrderedType？或者是否有更好的创建 map 的方法？

Answer 1

您不会轻易找到从任何类型到任何类型的映射，因为要使这样的映射起作用，您至少需要能够区分用于键的类型的两个元素。如果你只有这个能力(测试两个元素是否相同)，那么映射可以以一种相当低效的方式实现:你基本上处理一个列表对 (key, value) 和成本平均而言，检索与键关联的值与映射中已处理的键数成正比。

如果你想稍微提高一点效率，通常的技巧是使用散列键，但你需要能够计算散列值，所以你的类型不能完全是任意的。

最后，有可能使用基于具有顺序的类型的映射。在这种情况下，很容易实现映射，即检索一个键的值，平均成本是键数的对数。

现在，如何创建 OrderedType 对象？您需要实例化模块类型 MiniOrderedType。因此，对于您的类型，您需要说明什么函数将扮演 eq、lt 的角色，并显示 MiniOrderedType 中列出的各种重要属性> 模块类型(参见 this file)。 this example file 中有几个这种结构的例子。 ).