Правильный способ использования FMap в Coq 8.6?

Question

Я пытаюсь использовать карту на основе дерева в Coq, в частности Coq.FSets.FMapAVL.

Я нашел этот 4-летний вопрос: Finite map example

Глядя на стандартную Lib документации, ссылки в комментариях, я вижу эту заметку:

NB: Этот файл находится здесь только для совместимости с ранее версия FSets и FMap. Пожалуйста, используйте Structures/Orders.v прямо сейчас.

Что это значит? Когда я google «Structures.v» или «Orders.v», я всегда попадаю на другие страницы документации со связанными предупреждениями об устаревании.

Каков правильный, не устаревший способ использования FMap в Coq 8.6?

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:

переход между старый OrderedType, а новый - не (некоторые работы еще предстоит сделать на FMaps), , и мы не можем просто удалить старый стиль OrderedType.