Target Map Example

Question

For my application, I need to use and reason about final maps in Coq. I found googling around about FMapAVL, which seems to be perfect for my needs. The problem is that the documentation is not enough, and I did not understand how I should use it.

As a trivial example, consider the following stupid implementation of a finite mapping 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 km' end. Notation "x |-> y" := (pair xy) (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 can I define and prove similar examples using FMapAVL rather than a list of pairs?

---

Decision

Thanks to the answer from Ptival below , this is a complete working example:

 Require Export FMapAVL. Require Export Coq.Structures.OrderedTypeEx. Module M := FMapAVL.Make(Nat_as_OT). Definition map_nat_nat: Type := Mt 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 kv) (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 an OrderedNat : OrderedType , ask in the comments if you need help with this.

 Module M := FMapAVL.Make(OrderedNat). Definition map_nat_nat := Mt nat. Definition find k (m : nap_nat_nat) := M.find k m. (* you can just use M.find otherwise... *) Notation "x |-> y" := (M.add xy 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 check it right now, but it should be very similar to this.