Proper way to use FMap in Coq 8.6?

Question

I am trying to use a tree based map in Coq, specifically Coq.FSets.FMapAVL.

I found this 4 year old question: Finite map example

Looking at the standard lib documentation referenced in the comments, I see this note:

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

What does this mean? When I google "Structures.v" or "Orders.v" I always end up at other documentation pages with related deprecation warnings.

What is the proper, non-deprecated way to use an FMap in Coq 8.6?

Answer 1

Since the OrderedTypeEx module is deprecated, we won't use Nat_as_OT defined in it.

There is Nat_as_OT in OrdersEx (just a synonym for PeanoNat.Nat), which is useful for our purposes.

Unfortunately, the following code

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

won't work, because signatures OrderedType.OrderedType (currently used by FMapAVL) and Orders.OrderedType are not compatible.

However, the OrdersAlt module contains functors, which allow to build a module of one type from another. In this case, we are interested in Backport_OT. The following code shows how to use FMapAVL.Make, the rest of the code can be copied from the linked question:

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.

The situation with FMapAVL was explained by Pierre Letouzey in 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.