Changeset 2420 for src/RTLabs/CostInj.ma
 Timestamp:
 Oct 30, 2012, 12:32:31 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/CostInj.ma
r2418 r2420 48 48 ]. 49 49 50 definition domain_of_pm : ∀A. positive_map A → positive_map unit ≝51 λA,t. fold A (positive_map unit) (λp,a,b. insert unit p it b) t (pm_leaf unit).52 53 lemma pm_fold_ignore_adding_junk : ∀A. ∀m. ∀f,g:Pos → Pos. ∀s.54 (∀p,q. f p ≠ g q) →55 ∀p. lookup_opt unit (f p) (fold A ? (λx,a,b. insert unit (g x) it b) m s) = lookup_opt unit (f p) s.56 #A #m elim m57 [ normalize //58  #oa #l #r #IHl #IHr59 #f #g #s #not_g #p60 normalize61 >IHr62 [ >IHl63 [ cases oa64 [ normalize %65  #a normalize >(lookup_opt_insert_miss ?? (f p)) [ %  @not_g ]66 ]67  #x #y % #E cases (not_g x (p0 y)) #H @H @E68 ]69  #x #y % #E cases (not_g x (p1 y)) #H @H @E70 ]71 ] qed.72 73 lemma pm_fold_ind_gen : ∀A,B,m,f,b.74 ∀pre:Pos→Pos. (∀x,y.pre x = pre y → x = y) → ∀ps. (∀p. lookup_opt ? (pre p) ps = None ?) →75 ∀P:B → positive_map unit → Prop.76 P b ps →77 (∀p,ps,a,b. lookup_opt unit (pre p) ps = None unit → lookup_opt A p m = Some A a → P b ps → P (f (pre p) a b) (insert unit (pre p) it ps)) →78 P (fold A B (λx. f (pre x)) m b) (fold ?? (λp,a,b. insert unit (pre p) it b) m ps).79 #A #B #m elim m80 [ //81  #oa #l #r #IHl #IHr82 #f #b #pre #PRE #ps #PS #P #emp #step whd in ⊢ (?%%);83 @IHr84 [ #x #y #E lapply (PRE … E) #E' destruct //85  #p change with ((λx. pre (p1 x)) p) in match (pre (p1 p)); >pm_fold_ignore_adding_junk86 [ cases oa [ @PS  #a >(lookup_opt_insert_miss ?? (pre (p1 p))) [ @PS  % #E lapply (PRE … E) #E' destruct ] ]87  #p #q % #E lapply (PRE … E) #E' destruct88 ]89  @IHl90 [ #x #y #E lapply (PRE … E) #E' destruct //91  #p cases oa [ @PS  #a >(lookup_opt_insert_miss ?? (pre (p0 p))) [ @PS  % #E lapply (PRE … E) #E' destruct ] ]92  cases oa in step ⊢ %; [ #_ @emp  #a #step normalize @step [ @PS  %  @emp ] ]93  #p #ps' #a #b' @step94 ]95  #p #ps' #a #b' @step96 ]97 ] qed.98 99 lemma pm_fold_ext : ∀A,B,m,f,b.100 fold A B f m b = fold A B (λx:Pos. f x) m b.101 #A #B #m elim m /4/102 qed.103 104 lemma pm_fold_ind : ∀A,B,f,m,b. ∀P:B → positive_map unit → Prop.105 P b (pm_leaf unit) →106 (∀p,ps,a,b. lookup_opt unit p ps = None unit → lookup_opt A p m = Some A a → P b ps → P (f p a b) (insert unit p it ps)) →107 P (fold A B f m b) (domain_of_pm A m).108 #A #B #f #m #b #P #emp #step109 >pm_fold_ext110 whd in ⊢ (??%);111 @(pm_fold_ind_gen A B m f b (λx.x) ? (pm_leaf unit) ???)112 [ //113  //114  @emp115  @step116 ] qed.117 118 lemma pm_fold_eq : ∀A,B,b,f.119 (∀p,k:Pos. ∀a,s1,s2. lookup_opt B p s1 = lookup_opt B p s2 → lookup_opt B p (f k a s1) = lookup_opt B p (f k a s2)) →120 ∀p,s1,s2.121 lookup_opt B p s1 = lookup_opt B p s2 →122 lookup_opt B p (fold A (positive_map B) f b s1) = lookup_opt B p (fold A (positive_map B) f b s2).123 #A #B #b elim b124 [ #f #H #p #s1 #s2 #H @H125  #oa #l #r #IHl #IHr #f #H #p #s1 #s2 #H'126 whd in match (fold ???? s1);127 whd in match (fold ???? s2);128 @IHr [ #q #k #a #s1' #s2' #H'' @H @H'' ]129 @IHl [ #q #k #a #s1' #s2' #H'' @H @H'' ]130 cases oa [ @H'  #a @H @H' ]131 ] qed.132 133 134 135 lemma pm_fold_ignore_prefix : ∀A. ∀m. ∀pre:Pos → Pos. (∀x,y. pre x = pre y → x = y) →136 ∀p. ∀pre'.137 lookup_opt unit (pre p) (fold A ? (λx,a,b. insert unit (pre (pre' x)) it b) m (pm_leaf ?)) =138 lookup_opt unit p (fold A ? (λx,a,b. insert unit (pre' x) it b) m (pm_leaf ?)).139 #A #m #pre #PRE140 cut (∀p. lookup_opt unit (pre p) (pm_leaf unit) = lookup_opt unit p (pm_leaf unit)) [ // ]141 generalize in match (pm_leaf unit) in ⊢ ((? → ??%?) → ? → ? → ??%?);142 generalize in match (pm_leaf unit);143 elim m144 [ #s1 #s2 #S #p #pre' @S145  #oa #l #r #IHl #IHr146 #s1 #s2 #S #p #pre'147 whd in ⊢ (??(???%)(???%));148 @(IHr ???? (λx. pre' (p1 x)))149 #p' @IHl150 #p'' cases oa151 [ @S152  #a cases (decidable_eq_pos p'' (pre' one))153 [ #E destruct154 >(lookup_opt_insert_hit ?? (pre (pre' one)))155 >(lookup_opt_insert_hit ?? (pre' one))156 %157  #NE >(lookup_opt_insert_miss ??? (pre (pre' one)))158 [ >(lookup_opt_insert_miss ??? (pre' one)) //159  % #E @(absurd … (PRE … E) NE)160 ]161 ]162 ]163 ] qed.164 165 lemma domain_of_pm_present : ∀A,m,p.166 lookup_opt A p m ≠ None ? ↔ lookup_opt unit p (domain_of_pm A m) ≠ None ?.167 168 #A #m whd in match (domain_of_pm ??);169 elim m170 [ #p normalize /3/171  #oa #l #r #IHl #IHr172 whd in match (fold ???? (pm_leaf unit));173 *174 [ change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?)));175 >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ]176 change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?)));177 >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ]178 cases oa179 [ normalize /3/180  #a change with (insert unit one ??) in ⊢ (??(?(??(???%)?)));181 >(lookup_opt_insert_hit ?? one) normalize182 % #_ % #E destruct183 ]184  #p >(pm_fold_eq ??????? (pm_leaf unit))185 [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ]186 @IHr187  >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ]188 cases oa189 [ %190  #a >(lookup_opt_insert_miss ?? (p1 p)) [2: % #E destruct ]191 %192 ]193  #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p1 y))194 [ #E destruct195 >(lookup_opt_insert_hit ?? (p1 y))196 >(lookup_opt_insert_hit ?? (p1 y))197 %198  #NE >(lookup_opt_insert_miss ?? x … NE)199 >(lookup_opt_insert_miss ?? x … NE)200 @S201 ]202 ]203  #p204 >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ]205 >(pm_fold_eq ??????? (pm_leaf unit))206 [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ]207 @IHl208  cases oa209 [ %210  #a >(lookup_opt_insert_miss ?? (p0 p)) [2: % #E destruct ]211 %212 ]213  #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p0 y))214 [ #E destruct215 >(lookup_opt_insert_hit ?? (p0 y))216 >(lookup_opt_insert_hit ?? (p0 y))217 %218  #NE >(lookup_opt_insert_miss ?? x … NE)219 >(lookup_opt_insert_miss ?? x … NE)220 @S221 ]222 ]223 ]224 ] qed.225 226 227 (* Returns the domain of a map as the canonical set (one made only from the228 empty set and addition. *)229 definition domain_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝230 λtag,A,m. an_id_map tag unit (domain_of_pm A (match m with [ an_id_map m ⇒ m ])).231 lemma domain_of_map_present : ∀tag,A,m,id.232 present tag A m id ↔ present tag unit (domain_of_map … m) id.233 #tag #A * #m * #p @domain_of_pm_present234 qed.235 236 lemma foldi_ind : ∀A,B,tag,f,m,b. ∀P:B → identifier_set tag → Prop.237 P b (empty_set …) →238 (∀k,ks,a,b. ¬present ?? ks k → lookup ?? m k = Some ? a → P b ks → P (f k a b) (add_set tag ks k)) →239 P (foldi A B tag f m b) (domain_of_map … m).240 #A #B #tag #f * #m #b #P #P0 #STEP241 whd in match (foldi ??????); change with (an_id_map ?? (domain_of_pm A m)) in match (domain_of_map ???);242 @pm_fold_ind243 [ @P0244  #p #ps #a #b0 #FR #L #pre @(STEP (an_identifier tag p) (an_id_map tag unit ps))245 [ normalize >FR /3/246  @L247  @pre248 ]249 ] qed.250 251 lemma foldi_ind' : ∀A,B,tag,f,m,b,b'. ∀P:B → identifier_set tag → Prop.252 P b (empty_set …) →253 (∀k,ks,a,b. ¬present ?? ks k → lookup ?? m k = Some ? a → P b ks → P (f k a b) (add_set tag ks k)) →254 foldi A B tag f m b = b' →255 P b' (domain_of_map … m).256 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct @foldi_ind /2/257 qed.258 50 259 51 lemma reverse_label_map_ok : ∀g,r.
Note: See TracChangeset
for help on using the changeset viewer.