Changeset 2439 for src/common/PositiveMap.ma
 Timestamp:
 Nov 7, 2012, 4:42:02 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/PositiveMap.ma
r2420 r2439 25 25 ]. 26 26 27 let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝27 let rec pm_set (A:Type[0]) (b:Pos) (a:option A) (t:positive_map A) on b : positive_map A ≝ 28 28 match b with 29 29 [ one ⇒ 30 30 match t with 31 [ pm_leaf ⇒ pm_node A (Some ? a)(pm_leaf A) (pm_leaf A)32  pm_node _ l r ⇒ pm_node A (Some ? a)l r31 [ pm_leaf ⇒ pm_node A a (pm_leaf A) (pm_leaf A) 32  pm_node _ l r ⇒ pm_node A a l r 33 33 ] 34 34  p0 tl ⇒ 35 35 match t with 36 [ pm_leaf ⇒ pm_node A (None ?) ( insert A tl a (pm_leaf A)) (pm_leaf A)37  pm_node x l r ⇒ pm_node A x ( insert A tl a l) r36 [ pm_leaf ⇒ pm_node A (None ?) (pm_set A tl a (pm_leaf A)) (pm_leaf A) 37  pm_node x l r ⇒ pm_node A x (pm_set A tl a l) r 38 38 ] 39 39  p1 tl ⇒ 40 40 match t with 41 [ pm_leaf ⇒ pm_node A (None ?) (pm_leaf A) (insert A tl a (pm_leaf A)) 42  pm_node x l r ⇒ pm_node A x l (insert A tl a r) 43 ] 44 ]. 41 [ pm_leaf ⇒ pm_node A (None ?) (pm_leaf A) (pm_set A tl a (pm_leaf A)) 42  pm_node x l r ⇒ pm_node A x l (pm_set A tl a r) 43 ] 44 ]. 45 46 definition insert : ∀A:Type[0]. Pos → A → positive_map A → positive_map A ≝ 47 λA,p,a. pm_set A p (Some ? a). 45 48 46 49 let rec update (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : option (positive_map A) ≝ … … 62 65 ] 63 66 ]. 67 68 lemma lookup_opt_pm_set_hit : 69 ∀A:Type[0].∀v:option A.∀b:Pos.∀t:positive_map A. 70 lookup_opt … b (pm_set … b v t) = v. 71 #A #v #b elim b 72 [ * // 73  #tl #IH * 74 [ whd in ⊢ (??%%); @IH 75  #x #l #r @IH 76 ] 77  #tl #IH * 78 [ whd in ⊢ (??%%); @IH 79  #x #l #r @IH 80 ] 81 ] qed. 64 82 65 83 lemma lookup_opt_insert_hit : … … 87 105 #A #v #b #t #d whd in ⊢ (??%?); >lookup_opt_insert_hit % 88 106 qed. 107 108 lemma lookup_opt_pm_set_miss: 109 ∀A:Type[0].∀v:option A.∀b,c:Pos.∀t:positive_map A. 110 b ≠ c → lookup_opt … b (pm_set … c v t) = lookup_opt … b t. 111 #A #v #b elim b 112 [ * [ #t * #H elim (H (refl …)) 113  *: #c' #t #NE cases t // 114 ] 115  #b' #IH * 116 [ * [ #NE @refl  #x #l #r #NE @refl ] 117  #c' * [ #NE whd in ⊢ (??%%); @IH /2/ 118  #x #l #r #NE whd in ⊢ (??%%); @IH /2/ 119 ] 120  #c' * // 121 ] 122  #b' #IH * 123 [ * [ #NE @refl  #x #l #r #NE @refl ] 124  #c' * // 125  #c' * [ #NE whd in ⊢ (??%%); @IH /2/ 126  #x #l #r #NE whd in ⊢ (??%%); @IH /2/ 127 ] 128 ] 129 ] qed. 89 130 90 131 lemma lookup_opt_insert_miss: … … 856 897 ] qed. 857 898 899 lemma pm_find_aux_none : ∀A,t,pre,p,q,a. 900 pm_find_aux pre A t p = None ? → 901 lookup_opt A q t = Some ? a → 902 ¬ p (pre q) a. 903 #A #t elim t 904 [ #pre #p #q #a #_ normalize #E destruct 905  #oa #l #r #IHl #IHr #pre #p * 906 [ #a cases oa 907 [ #_ normalize #E destruct 908  #a' #F whd in F:(??%?); whd in F:(??match % with [_⇒?_⇒?]?); 909 #E normalize in E; destruct 910 cases (p (pre one) a) in F ⊢ %; // 911 normalize #E destruct 912 ] 913  #q #a #F #L @(IHr (λx. pre (p1 x)) p q a ? L) 914 whd in F:(??%?); cases oa in F; 915 [2: #a' normalize cases (p (pre one) a') [ normalize #E destruct ] ] 916 normalize cases (pm_find_aux ?? l p) normalize // 917 #x #E destruct 918  #q #a #F #L @(IHl (λx. pre (p0 x)) p q a ? L) 919 whd in F:(??%?); cases oa in F; 920 [2: #a' normalize cases (p (pre one) a') [ normalize #E destruct ] ] 921 normalize cases (pm_find_aux ?? l p) normalize // 922 ] 923 ] qed. 924 925 lemma pm_find_none : ∀A,t,p,q,a. 926 pm_find A t p = None ? → 927 lookup_opt A q t = Some ? a → 928 ¬ p q a. 929 #A #t 930 @(pm_find_aux_none A t (λx.x)) 931 qed. 932 858 933 lemma pm_find_predicate : ∀A,t,p,q,a. 859 934 pm_find A t p = Some ? 〈q,a〉 →
Note: See TracChangeset
for help on using the changeset viewer.