Para mi aplicación, necesito usar y razonar sobre mapas finitos en Coq. He encontrado en Google sobre FMapAVL que parece ser el ajuste perfecto para mis necesidades. El problema es que la documentación es escasa y no he descubierto cómo se supone que debo usarla.

Como ejemplo trivial, considere la siguiente implementación tonta de un mapa finito usando una 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.

¿Cómo podría definir y probar ejemplos similares utilizando FMapAVL en lugar de la lista de pares?

Solución

Gracias arespuesta de Ptival abajo, este es un ejemplo completo de trabajo:

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.