One of the most common structures used in programming are key/value maps, also
called hash maps, dictionaries, association lists, or simply functions. These
maps generally provide a way to add new values, lookup keys, iterate over the
collection, etc. Yet in Coq, even though this facility exists in the standard
library under the module `FMap`

, it can be quite difficult to get started with.
This post intends to clarify the typical patterns in a way that is easy to
copy into your own project, based on the four different ways this library is
typically used.

# Using a known key type and map structure

Very often, one maps from a known, ordered type, like `nat`

, to some other type,
using one of the concrete structures offered by the `FMap`

library. In that
case, the code you want to start with looks like this:

```
Require Import
Coq.FSets.FMapList
Coq.Structures.OrderedTypeEx.
Module Import M := FMapList.Make(Nat_as_OT).
```

You can now create a map using `M.t A`

, where `A`

is your value type. You can
prefix the map-related functions with `M.`

, or just call them directly. Some
common function to use on maps are as follows:

`empty`

`add`

`remove`

`find`

`mem`

`is_empty`

`map`

`mapi`

`map2`

`fold`

There are also several relations you can use to phrase theorems about maps and map membership:

`In`

`MapsTo`

`Equal`

`Equiv`

`Equivb`

`Empty`

# Additional functions and lemmas

In order to complete most proofs concerning maps, there are additional lemmas and functions you’ll want to include:

```
Require Import
Coq.FSets.FMapFacts.
Module P := WProperties_fun N_as_OT M.
Module F := P.F.
```

This provides two new prefixes, `P.`

and `F.`

, which bring into scope many more
helper functions and lemmas:

`P.of_list`

`P.to_list`

`P.filter`

`P.for_all`

`P.exists_`

`P.partition`

`P.update`

`P.restrict`

`P.diff`

Helper lemmas in the `F`

module are generally best found using `SearchAbout`

for
the specific lemma you need. There are too many to list here, and they’re
often quite specific in their use, such as `F.find_mapsto_iff`

to reflect
between the fact of a successful `find`

operation, and its equivalent `MapsTo`

relation.

# Proofs involving maps

There are several induction principles you will need for completing inductive proofs over maps:

`P.map_induction`

`P.map_induction_bis`

`P.fold_rec`

`P.fold_rec_bis`

`P.fold_rec_nodep`

`P.fold_rec_weak`

The `P.map_induction`

induction principle treats each intermediate map as an `Add`

relation over a previous map, until it reaches the base `Empty`

map. The `_bis`

variant expresses the same information as successive calls to `add`

down to an
`empty`

map.

`P.fold_rec`

should be applied if the goal has the form of a call to `M.fold`

over
a map. If you use this, be sure to `revert`

into the goal any hypotheses
referring to the same map, since you’ll likely want to use those facts as part
of the induction.

Note that these two sets of principles are used somewhat differently from each other:

```
-- Applies to any evidence in the context involving [m].
induction m using P.map_induction bis.
-- Applies only to evidence in the goal, thus sometimes
-- requiring use of [revert].
apply P.fold_rec.
```

# Rewriting with maps

Since the internal structure of maps is not exposed by the `FMap`

interface,
rewriting can sometimes be a little confusing. Equality between maps is
expressed by the equivalence `Equal`

, which states that anything found in the
first map is found at the same key in the second map. In other words:

```
forall k v, M.MapsTo k v m1 <-> M.MapsTo k v m2
```

This isn’t a problem if the terms you’re rewriting involve functions from the
`FMap`

modules, but if you create a new function that operates on maps, you’ll
need to accompany it with a proof relating it to `Equal`

. For example:

```
Definition map_operation `(m : M.t A) : M.t A := ...
Lemma map_operation_Proper :
Proper (Equal ==> Equal) map_operation.
```

Now you can `rewrite`

the arguments in a `map_operation`

, provided you know they
are `Equal`

.

Also, if you find yourself facing difficulties using `rewrite`

with folds, note
that in addition to establishing a proof that the fold function is `Proper`

for
its arguments and result, you must also show that the final result is
independent of the order of evaluation, since it’s not known from the `FMap`

interface whether the contents of a map are reordered during insertion or not.

# Abstracting the map implementation

Often when using maps, it’s not necessary to pick an implementation, you just need the map interface over a known key type. To do this, you just need to place your code in a module that itself requires and passes along the implementation module:

```
Require Import
Coq.FSets.FMapFacts
Coq.Structures.OrderedTypeEx.
Module MyModule (M : WSfun Nat_as_OT).
Module P := WProperties_fun Nat_as_OT M.
Module F := P.F.
...
End MyModule.
```

To later instantiate such a module functor using a map implementation, you’d write:

```
Require Import
Coq.FSets.FMapFacts
MyModule.
Module Import M := FMapList.Make(Nat_as_OT).
Module Import MyMod := MyModule M.
```

# Abstracting over both map and key

When implementing generic algorithms that are applicable to any map, you’ll also need to abstract over the key type. In this case, you have two choices: Do you need to know that the key type is ordered, or do you only need to know that it’s decidable? Often the latter suffices, making the algorithm even more general.

In both cases, you may refer to the key type as either `E.key`

or `M.key`

(since
the `M`

module re-exports `key`

), and you can check for key equality using `E.eq`

:

```
Require Import
Coq.FSets.FMapFacts
Coq.Structures.DecidableTypeEx.
Module MoreFacts (E : DecidableType) (M : WSfun E).
Global Program Instance filter_Proper {elt} : forall P,
Proper (E.eq ==> eq ==> eq) P
-> Proper (M.Equal (elt:=elt) ==> M.Equal) (@P.filter elt P).
...
End MoreFacts.
```

To require an ordered type, which makes `E.lt`

available, use:

```
Require Import
Coq.FSets.FMapFacts
Coq.Structures.OrderedTypeEx.
Module MoreFacts (E : OrderedType) (M : WSfun E).
...
End MoreFacts.
```

# Putting it all together

Since you probably came here just wondering how to construct a map, add stuff to it, and then search for what you added, here is a complete example you can cut and paste to start off with:

```
Require Import
Coq.FSets.FMapAVL
Coq.FSets.FMapFacts
Coq.Structures.OrderedTypeEx
PeanoNat.
Module Import M := FMapAVL.Make(Nat_as_OT).
Module P := WProperties_fun Nat_as_OT M.
Module F := P.F.
Compute M.find 1 (M.add 1 10 (M.empty _)).
Compute P.for_all (fun k _ => k <? 10) (M.add 1 10 (M.empty _)).
```

Also note that there is `N_as_OT`

, which is much faster to compute with if you
are using large constants, but it requires familiarity with the `NArith`

library.