अंतिम नक्शा उदाहरण

Question

मेरे आवेदन के लिए, मुझे कोक में सीमित नक्शे के बारे में उपयोग करने और तर्क करने की आवश्यकता है। चारों ओर घूमते हुए मुझे 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. 

Answer 1

मान लिया जाये कि आप जानते हैं कि एक मॉड्यूल 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) ..). 

मैं अभी इसका परीक्षण नहीं कर सकता लेकिन यह इसके समान ही होना चाहिए।