dictionary - 在 Coq 8.6 中使用 FMap 的正确方法？

Question

我正在尝试在 Coq 中使用基于树的 map ，特别是 Coq.FSets.FMapAVL。

我发现了这个 4 年前的问题:Finite map example

查看评论中引用的标准库文档，我看到了这个注释:

NB: This file is here only for compatibility with earlier version of FSets and FMap. Please use Structures/Orders.v directly now.

这是什么意思？当我用谷歌搜索“Structures.v”或“Orders.v”时，我总是会在其他文档页面找到相关的弃用警告。

在 Coq 8.6 中使用 FMap 的正确、未弃用的方法是什么？

Answer 1

自 OrderedTypeEx模块已弃用，我们不会使用 Nat_as_OT定义在里面。

有Nat_as_OT在 OrdersEx (只是 PeanoNat.Nat 的同义词)，这对我们的目的很有用。

不幸的是，下面的代码

Require Import Coq.Structures.OrdersEx.
Module M := FMapAVL.Make Nat_as_OT.

不会工作，因为签名 OrderedType.OrderedType (目前由 FMapAVL 使用)和 Orders.OrderedType不兼容。

然而，OrdersAlt模块包含仿函数，允许从另一种类型构建一个模块。在这种情况下，我们对 Backport_OT 感兴趣.以下代码显示了如何使用 FMapAVL.Make ，其余代码可以从链接的问题中复制:

From Coq Require Import
FSets.FMapAVL Structures.OrdersEx Structures.OrdersAlt.

Module backNat_as_OT := Backport_OT Nat_as_OT.
Module M := FMapAVL.Make backNat_as_OT.

FMapAVL 的情况由 Pierre Letouzey 在 this Coq-Club post 中解释:

the transition between old-style OrderedType and the new one isn't finished yet (some work remain to be done on FMaps for instance), and we cannot simply remove the old-style OrderedType.