在 Coq 中创建字典/地图答案

【问题标题】：Creating a dictionary/map in Coq在 Coq 中创建字典/地图
【发布时间】：2018-05-01 22:15:08
【问题描述】：

我希望能够在 Coq 中拥有从任何类型到任何类型的映射。到目前为止，我已经从标准库中获得了一些成功 using 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 的映射。但是，FMapList.Make 将只接受 OrderedType 作为参数。有没有办法让我自己制作OrderedType？或者有没有更好的方法来创建地图？

【问题讨论】：

标签： dictionary coq formal-verification

【解决方案1】：

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

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

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

现在，如何创建OrderedType 对象？您需要实例化模块类型MiniOrderedType。因此，对于您的类型，您需要说明eq、lt 的作用是什么函数，并显示MiniOrderedType 模块类型中列出的各种重要属性（参见this file）。在this example file中有几个这种构造的例子。

【讨论】：

【解决方案2】：

从任何类型到 Coq 中任何类型的映射

为了完善 Yves 的答案，在 Coq 中从任何类型 A 到任何类型 B 的唯一映射是函数空间 A -> B（或 A -> option B）

话虽如此，一旦添加了功能扩展性，这对于地图来说并不是一个糟糕的类型，但当然它缺少一些可以通过一些努力添加的基本操作。

【讨论】：

为什么不建议编辑 Yves 的答案而不是添加部分答案？
嗯，有趣的一点，我不确定，我想我会留给 Yves 的标准。
@ejgallego 是否有特定原因无法创建可以使用任何键的映射，例如 C++ 中的 std::map 呢？还是只是它没有在标准库中实现？另外，您所说的“功能扩展性”是什么意思？
啊。我刚想起来。 C++ 要求键具有排序...这与FMapList 给出的要求完全相同。我想我已经弄清楚了那部分。不过，我仍然不确定您所说的“功能扩展性”是什么意思。
@setholopolus 确实有一个特定的原因。在 Coq 中，类型 T 可能比 C++ 中的类型复杂得多。例如，费马大定理的陈述是 Coq 中的一个类型。因此，正如 Yves 所暗示的，您希望将地图的域限制为至少可以比较的类型。请注意，std::map 不能在任意对象上创建映射，因为您的类需要提供 < 运算符。