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

Question

我正在尝试在 Coq 中使用基于树的地图，特别是 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.

这是什么意思？当我 google "Structures.v" 或 "Orders.v" 时，我总是会在其他文档页面上看到相关的弃用警告。

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

Answer 1

由于 OrderedTypeEx 模块已弃用，我们不会使用其中定义的 Nat_as_OT。

OrdersEx中有Nat_as_OT（只是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.

Pierre Letouzey 在 this Coq-Club post 中解释了 FMapAVL 的情况：

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.

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

Proper way to use FMap in Coq 8.6?

dictionary

coq