Пример конечной карты
Для моего приложения мне нужно использовать и рассуждать о конечных картах в Coq. Погугливая вокруг яМы нашли FMapAVL, который идеально подходит для моих нужд. Проблема в том, что документации мало, а у меня нетЯ понял, как я должен это использовать.
В качестве тривиального примера рассмотрим следующую глупую реализацию конечного отображения с использованием списка пар.
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.
Как я могу определить и доказать аналогичные примеры, используя FMapAVL, а не список пар?
РешениеБлагодаряответ от Ptival ниже, это полный рабочий пример:
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.