10

私のアプリケーションでは、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 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.
4

1 に答える 1

7

モジュールモジュールの作成方法を知っていると仮定して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) .. ).

今はテストできませんが、これとかなり似ているはずです。

于 2013-01-23T21:38:07.083 に答える