Finite map example

Question

For my application, I need to use and reason about finite maps in Coq. Googling around I've found about FMapAVL which seems to be a perfect fit for my needs. The problem is that the documentation is scarce, and I haven't figured out how I am supposed to use it.

As a trivial example, consider the following silly implementation of a finite map using a list of pairs.

Require Export Bool.
Require Export List.
Require Export Arith.EqNat.

Definition map_nat_nat: Type := list (nat * nat).

Fixpoint find (k: nat) (m: map_nat_nat) :=
match m with
| nil => None
| kv :: m' => if beq_nat (fst kv) k 
                then Some (snd kv)
                else find k m'
end.

Notation "x |-> y" := (pair x y) (at level 60, no associativity).
Notation "[ ]" := nil.
Notation "[ p , .. , r ]" := (cons p .. (cons r nil) .. ).

Example ex1: find 3 [1 |-> 2, 3 |-> 4] = Some 4.
Proof. reflexivity. Qed.

Example ex2: find 5 [1 |-> 2, 3 |-> 4] = None.
Proof. reflexivity. Qed.

How could I define and prove similar examples using FMapAVL rather that the list of pairs?

---

Solution

Thanks to the answer from Ptival bellow, this is a full working example:

Require Export FMapAVL.
Require Export Coq.Structures.OrderedTypeEx.

Module M := FMapAVL.Make(Nat_as_OT).

Definition map_nat_nat: Type := M.t nat.

Definition find k (m: map_nat_nat) := M.find k m.

Definition update (p: nat * nat) (m: map_nat_nat) :=
  M.add (fst p) (snd p) m.

Notation "k |-> v" := (pair k v) (at level 60).
Notation "[ ]" := (M.empty nat).
Notation "[ p1 , .. , pn ]" := (update p1 .. (update pn (M.empty nat)) .. ).

Example ex1: find 3 [1 |-> 2, 3 |-> 4] = Some 4.
Proof. reflexivity. Qed.

Example ex2: find 5 [1 |-> 2, 3 |-> 4] = None.
Proof. reflexivity. Qed.

Answer 1

Assuming you know how to create a module OrderedNat : OrderedType module, ask in the comments if you need help for that.

Module M := FMapAVL.Make(OrderedNat).

Definition map_nat_nat := M.t nat.

Definition find k (m : nap_nat_nat) := M.find k m. (* you can just use M.find otherwise... *)

Notation "x |-> y" := (M.add x y M.empty) (at level 60, no associativity).

Notation "[ ]" := nil.

Notation "[ k1 |-> d1 , .. , kn |-> dn ]" := (M.add k1 d1 .. (M.add kn dn M.empty) .. ).

I can't test that right now but it should be pretty similar to this.