Introduction

Assume a type of values, called val, that's inhabited.

Basic usage of map operations

We can use a map from int to val, and read in that map

We can also write a value in the map; it does not matter whether the key already existed or not.

To reason about a read, we can use the lemma read_update.

Sometimes we need to talk about the domain of a map. dom m is a set of keys, in the sense of LibSet's set. For example, to assert that two maps have the same domain.

To assert that one key is valid for a domain, we use i \in (dom m), which is shortened to i \indom m. The latter is a notation for (x \in (dom m : set _)), with the annotation to help the typechecker.

Similarly, the notation x \notindom m is available. In an inductive definition, it is commonplace to assert that i is in the domain of m and that M[i] = v. The binds predicate captures the conjunction of these two facts. The definition can be unfolded using the following rewriting rule.

Other operations on maps involve:

• empty map (\{} : map A B). The type annotation is often required.
• union of maps m1 \u m2
• removal of a set of keys m \- E
• removal of a key m \-- i, equivalent to m \- \{i}
• map_reduce w.r.t. a function and a monoid, e.g. fold (monoid_make plus zero) f m, which computes f k1 v1 + f k2 v2 + ... + f kn vn + 0.
• inclusion m1 \c m2 is not yet defined, but should be soon.

Lemmas for reasoning about maps can be found in two places: in LibMap.v and in LibContainer.v. The latter contains generic lemmas, that are shared by several data structures, such as sets and maps. The typeclass mechanism used for the sharing is explained next.

Implementation of maps

Finite maps are implemented using the typeclasses defined in LibContainer. The internal implementation is:

The internal definition of read in a map is thus a function that applies the map to the index. When the result is None it returns an arbitrary value.

Doing so requires the type B to be inhabited. Let's look at the error message that we get when trying to work with a map on a type that's not inhabited.

The notation m[i] is defined in LibContainer.v as read m i.

The operation read is a typeclass. It applies to any data structure of type T on which a read operation can be performed using keys of type A to extract a value of type B.

Note that the type of read is: forall A B T {I:BagRead A B T}, T -> A -> B. In other words, read must be applied to an "instance" of the typeclass BagRead, and then the result is a read function for that instance. We'll see further on what this means. The connection between read_impl for type map and the generic read operation is performed through an instance declaration:

In the light of this, let's inspect the interpretation of m[i]. It means @read int val (map int val) read_inst m i.

You can activate Set Printing All or menu "Display all level-level contents" from the view menu in CoqIDE to see the low-level interpretation.

What happens during type-checking is that read_inst gets automatically inferred by the typeclass mechanism, based on the type of m. In other words, before type inference, Coq sees: @read _ _ _ _ m i. From the type of m, it deduces @read _ _ (map int val) (_:BagRead _ _ (map int val)) m i. From typeclass resolution, it finds out that read_inst is the instance that could fill in the argument with type BagRead _ _ (map int val). Now, we can see that the instance inferred is @LibMap.read_inst int val Inhab_val. This instance refers to the instance asserting that val is inhabited. When such an assumption about the result type cannot be found, then the read_inst instance cannot be synthesized. We can investigate the resolution process manually as follows.

The file LibContainer.v contains generic lemmas. For example union_empty_r asserts that m \u \{} = m. This lemma is stated for any data structure of type T that features an empty and a union operation.

The proof that map validates the lemma union_empty_r is derived from the fact that it validates the lemma union_empty_l and commutativity of union

The proof that map validates union_empty_l is itself derived from another lemma, called union_empty_l_of_in_union_eq_and_in_empty_eq. More details can be found in LibContainerDemo, but it is not needed to understand the full setup to use the lemmas over maps.] The point is that rewrite union_empty_r is a tactic that rewrites m \u \{} = m for any data structure m over which the statement of this equality makes sense.