我希望能够在 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 的方法?
最佳答案
您不会轻易找到从任何类型到任何类型的映射,因为要使这样的映射起作用,您至少需要能够区分用于键的类型的两个元素。如果你只有这个能力(测试两个元素是否相同),那么映射可以以一种相当低效的方式实现:你基本上处理一个列表对 (key, value)
和成本平均而言,检索与键关联的值与映射中已处理的键数成正比。
如果你想稍微提高一点效率,通常的技巧是使用散列键,但你需要能够计算散列值,所以你的类型不能完全是任意的。
最后,有可能使用基于具有顺序的类型的映射。在这种情况下,很容易实现映射,即检索一个键的值,平均成本是键数的对数。
现在,如何创建 OrderedType
对象?您需要实例化模块类型 MiniOrderedType
。因此,对于您的类型,您需要说明什么函数将扮演 eq
、lt
的角色,并显示 MiniOrderedType
中列出的各种重要属性> 模块类型(参见 this file)。 this example file 中有几个这种结构的例子。 ).
关于dictionary - 在 Coq 中创建字典/ map ,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/47362451/