有限的地图示例 [英] Finite map example

问题描述

对于我的应用程序，我需要使用和理解Coq中的有限地图。搜索周围我发现关于FMapAVL，这似乎是完美适合我的需要。问题是文档很少，我还没有想出我应该如何使用它。

作为一个琐碎的例子，考虑以下愚蠢的实现使用对列表的有限地图。

 需要导出Bool。 
需要导出列表。 
需要导出Arith.EqNat。 
 
定义map_nat_nat：类型：= list（nat * nat）。 
 
 Fixpoint find（k：nat）（m：map_nat_nat）：= 
匹配m与
 | nil =>无
 | kv :: m'=>如果beq_nat（fst kv）k 
 then some（snd kv）
 else find k m'
 end。 
 
表示法x |  - > y：=（对x y）（60级，无关联性）。 
表示法[]：= nil。 
表示法[p，..，r]：=（cons p ..（cons r nil）..）。 
 
示例ex1：find 3 [1 |  - > 2，3 |  - > 4] =一些4. 
证明。反思。 QED。 
 
示例ex2：find 5 [1 |  - > 2，3 |  - > 4] =无。 
证明。反思。 QED。 
  

如何使用FMapAVL定义和证明类似的示例，而不是列表？

---

解决方案

感谢来自Ptival bellow 的回复，这是一个完整的例子：

 需要导出FMapAVL。 
需要导出Coq.Structures.OrderedTypeEx。 
 
模块M：= FMapAVL.Make（Nat_as_OT）。 
 
定义map_nat_nat：类型：= M.t nat。 
 
定义find k（m：map_nat_nat）：= M.find k m。 
 
定义更新（p：nat * nat）（m：map_nat_nat）：= 
 M.add（fst p）（snd p）m。 
 
表示法k |  - > v：=（对k v）（等级60）。 
表示法[]：=（M.empty nat）。 
表示法[p1，..，pn]：=（更新p1 ..（更新pn（M.empty nat））..）。 
 
示例ex1：find 3 [1 |  - > 2，3 |  - > 4] =一些4. 
证明。反思。 QED。 
 
示例ex2：find 5 [1 |  - > 2，3 |  - > 4] =无。 
证明。反思。 QED。 
  

解决方案

假设你知道如何创建一个模块 OrderedNat：OrderedType 模块，如果您需要帮助，请在评论中。

 模块M：= FMapAVL.Make（OrderedNat）。 
 
定义map_nat_nat：= M.t nat。 
 
定义find k（m：nap_nat_nat）：= M.find k m。 （*你可以使用M.find否则... *）
 
表示法x |  - > y：=（M.add xy M.empty）（在60级，没有关联性）。 
 
表示法[]：= nil。 
 
符号[k1 |  - > d1，..，kn |  - > dn]：=（M.add k1 d1 ..（M.add kn dn M.empty）。 。）。 
  

我现在无法测试，但应该非常类似于此。

For my application, I need to use and reason about finite maps in Coq. Googling around I've found about FMapAVL which seems to be a perfect fit for my needs. The problem is that the documentation is scarce, and I haven't figured out how I am supposed to use it.

As a trivial example, consider the following silly implementation of a finite map 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 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.

How could I define and prove similar examples using FMapAVL rather that the list of pairs?

---

Solution

Thanks to the answer from Ptival bellow, this is a full working example:

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.

解决方案

Assuming you know how to create a module OrderedNat : OrderedType module, ask in the comments if you need help for that.

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) .. ).

I can't test that right now but it should be pretty similar to this.

这篇关于有限的地图示例的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！