对于我的应用程序，我需要在 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 而不是对列表来定义和证明类似的示例？
解决方案
感谢 answer from Ptival bellow ，这是一个完整的工作示例:
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.
最佳答案
假设您知道如何创建模块 OrderedNat : OrderedType模块，如果您需要帮助，请在评论中询问。
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) .. ).
我现在无法测试，但它应该与此非常相似。
关于dictionary - 有限 map 示例，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/14489232/