Ví dụ về bản đồ hữu hạn

Question

Đối với đơn đăng ký của tôi, tôi cần sử dụng và lý do về các bản đồ hữu hạn trong Coq. Googling xung quanh tôi đã tìm thấy về FMapAVL mà dường như là hoàn toàn phù hợp với nhu cầu của tôi. Vấn đề là tài liệu khan hiếm, và tôi đã không tìm ra cách tôi phải sử dụng nó.

Như một ví dụ nhỏ, hãy xem xét việc triển khai thực hiện ngớ ngẩn sau của một bản đồ hữu hạn bằng cách sử dụng danh sách các cặp.

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. 

Làm cách nào để xác định và chứng minh các ví dụ tương tự bằng cách sử dụng FMapAVL thay vì danh sách các cặp?

---

Giải pháp

Nhờ answer from Ptival bellow, đây là một ví dụ làm việc đầy đủ:

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. 

Answer 1

Giả sử bạn biết làm thế nào để tạo ra một mô-đun mô-đun OrderedNat : OrderedType, hãy hỏi trong các ý kiến ​​nếu bạn cần sự giúp đỡ cho điều đó.

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

Tôi không thể kiểm tra ngay bây giờ nhưng nó sẽ khá giống với điều này.