Para meu aplicativo, preciso usar e raciocinar sobre mapas finitos no Coq. Pesquisando no Google, encontrei o FMapAVL, que parece ser perfeito para minhas necessidades. O problema é que a documentação é escassa e ainda não descobri como devo usá-la.

Como um exemplo trivial, considere a seguinte implementação tola de um mapa finito usando uma lista de pares.

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.

Como eu poderia definir e provar exemplos semelhantes usando o FMapAVL em vez da lista de pares?

Solução

Graças aoresposta de Ptival abaixo, este é um exemplo completo de trabalho:

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.