Changeset 3259 for src/common/ExtraIdentifiers.ma
 Timestamp:
 May 9, 2013, 12:49:38 AM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/ExtraIdentifiers.ma
r3217 r3259 21 21 [//] #i #IH #f #b @IH 22 22 qed. 23 23 24 let rec pm_clean (A : Type[0]) (p : positive_map A) on p : positive_map A ≝ 25 match p with 26 [ pm_leaf ⇒ pm_leaf A 27  pm_node a l r ⇒ let l' ≝ pm_clean A l in 28 let r' ≝ pm_clean A r in 29 if andb (is_none ? a) 30 (andb (is_pm_leaf ? l') (is_pm_leaf ? r')) then 31 pm_leaf A 32 else 33 pm_node ? a l' r' 34 ]. 35 36 lemma lookup_pm_clean : ∀A : Type[0].∀p,p' : positive_map A. 37 (∀i.lookup_opt A i p = lookup_opt A i p') → 38 pm_clean A p = pm_clean A p'. 39 #A #p elim p 40 [ #p' elim p' [ #_ normalize %] * [2: #a] #l #r #IHl #IHr #H normalize 41 [ lapply(H one) normalize #EQ destruct] 42 <IHl [2,4: #i lapply(H (p0 i)) normalize //] normalize 43 <IHr [2,4: #i lapply(H (p1 i)) normalize //] % 44  #opt_a #l #r #IHl #IHr * 45 [ #H normalize lapply(H one) normalize #EQ destruct(EQ) normalize 46 >(IHl (pm_leaf ?)) [2: #i lapply(H (p0 i)) normalize //] normalize 47 >(IHr (pm_leaf ?)) [2: #i lapply(H (p1 i)) normalize //] % 48  #opt_a' #l' #r' #H normalize lapply(H one) normalize #EQ destruct(EQ) 49 >(IHl l') [2: #i lapply(H (p0 i)) normalize //] 50 >(IHr r') [2: #i lapply(H (p1 i)) normalize //] % 51 ] 52 ] 53 qed. 54 55 definition pm_find_all : ∀A : Type[0].positive_map A → 56 (Pos → A → bool) → positive_map A ≝ 57 λA,p,P.fold ?? 58 (λi,a,p'.if P i a then pm_set ? i (Some ? a) p' else p') p (pm_leaf A). 59 60 61 lemma pm_clean_idempotent : ∀A : Type[0].∀p : positive_map A. 62 pm_clean ? p = pm_clean ? (pm_clean ? p). 63 cases daemon 64 qed. 65 66 67 lemma pm_find_all_canonic : ∀A : Type[0].∀p : positive_map A.∀P. 68 pm_find_all A p P = pm_clean A (pm_find_all A p P). 69 #A #p #P whd in match pm_find_all; normalize nodelta 70 @pm_fold_ind 71 [ %] #i #ps #a #b #H #H1 #H2 cases(P i a) normalize 72 [2: assumption] lapply H2 lapply b elim i 73 [ normalize * [ #_ %] #opt_a #l #r 74 normalize nodelta normalize cases opt_a 75 [2: #a1 normalize #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct >e0 in ⊢ (??%?); 76 >e1 in ⊢ (??%?); % ] normalize 77 cases(pm_clean ? l) normalize [2: #opt_a1 #l1 #r1 78 #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct >e0 in ⊢ (??%?); %] 79 cases(pm_clean ? r) normalize [#EQ destruct] #opt_a1 #l1 #r1 80 #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct % 81 *: #x #IH * normalize 82 [1,3: #_ <IH [2,4: % ] 83 inversion(pm_set A x ??) [2,4: #opt_a1 #l1 #r1 #_#_#_ %] 84 #ABS @⊥ cases x in ABS; [1,4: normalize #EQ destruct] #x1 normalize 85 #EQ destruct 86 *: * [2,4: #a1] #l #r normalize 87 [1,2: #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct >e0 in ⊢ (??%?); 88 >e1 in ⊢ (??%?); <IH 89 [ @eq_f3 try % >e1 in ⊢ (???%); % 90  assumption 91  @eq_f3 try % @pm_clean_idempotent 92  @pm_clean_idempotent 93 ] 94 *: inversion(pm_clean A l) normalize 95 [ #H3 inversion(pm_clean A r) normalize [#_ #EQ destruct] #opt_a1 #l1 #r1 96 #_ #_ #H4 #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ <(IH r) 97 [2: cut(r = pm_node A opt_a1 l1 r1) [ destruct %] #H5 98 >H5 in ⊢ (??%?); <H4 % ] inversion(pm_set A x ??) 99 [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct %] 100 #ABS @⊥ cases x in ABS; normalize cases r normalize 101 [ #z #w1 #w2 #x1  #z #w1 #w2 #x1  #x1  #z #w1 #w2 #x1 ] 102 #EQ1 destruct 103  #opt_a1 #l1 #r1 #_ #_ #H3 #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ 104 <(IH r) [destruct %] destruct assumption 105  #H3 cases(pm_clean A r) normalize [#EQ destruct] #opt_a1 #l1 #r1 106 #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ <(IH l) [2: >H3 destruct %] 107 inversion(pm_set A x ??) 108 [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct %] 109 #ABS @⊥ cases x in ABS; normalize cases l normalize 110 [ #z #w1 #w2 #x1  #z #w1 #w2 #x1  #x1  #z #w1 #w2 #x1 ] 111 #EQ1 destruct 112  #opt_a1 #l1 #r1 #_ #_ #H3 #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ 113 <(IH l) [2: >H3 destruct %] inversion(pm_set A x ??) 114 [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct >e0 in ⊢ (??%?); %] 115 #ABS @⊥ cases x in ABS; normalize cases l normalize 116 [ #z #w1 #w2 #x1  #z #w1 #w2 #x1  #x1  #z #w1 #w2 #x1 ] 117 #EQ1 destruct 118 ] 119 ] 120 ] 121 ] 122 qed. 123 24 124 25 125 definition find_all : ∀tag,A. identifier_map tag A → 26 126 (identifier tag → A → bool) → identifier_map tag A ≝ 27 λtag,A,m,P. foldi A (identifier_map tag A) tag28 (λi,a,l.if (P i a) then (add tag A l i a) else l) m (empty_map tag A).29 127 λtag,A,m,P.match m with 128 [an_id_map p ⇒ an_id_map ?? (pm_find_all A p (λx,a.P (an_identifier tag x) a))]. 129 (* 30 130 31 131 lemma find_all_lookup_predicate : ∀tag,A.∀m : identifier_map tag A. … … 33 133 lookup tag A (find_all tag A m P) i = Some ? a → 34 134 lookup tag A m i = Some ? a ∧ (bool_to_Prop (P i a)). 35 #tag #A #m #P #i #a whd in match find_all; normalize nodelta @foldi_ind135 #tag #A * #m #P * #i #a whd in match find_all; normalize @pm_fold_ind 36 136 [ normalize #EQ destruct 37  #k #ks #a1 #b * #H #H1 #H2 inversion(P k a1) 38 [ #H3 normalize nodelta >H3 39 cut(bool_to_Prop (eq_identifier tag i k) ∨ 137  #k #ks #a1 #b * #H #H1 #H2 inversion(P (an_identifier tag i) a1) 138 [ cases(decidable_eq_pos i k) 139 [#EQ destruct #H3 >H3 in H2; normalize >looku 140 141 142 [#EQ destruct inversion( 143 144 [ #H3 normalize nodelta >H3 cases(decidable_eq_pos i k) 145 [ #EQ destruct >H3 in H2; 146 147 148 cut(bool_to_Prop (eq_identifier tag (an_identifier tag i) (an_identifierk) ∨ 40 149 (bool_to_Prop (notb (eq_identifier tag i k)))) 41 150 [@eq_identifier_elim #_ [ %%%2 %]] … … 68 177 ] 69 178 qed. 70 179 *) 71 180 (* 72 181 whd in match (add ?????); whd in match (add ?????); normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.