Changeset 2420 for src/common
 Timestamp:
 Oct 30, 2012, 12:32:31 PM (8 years ago)
 Location:
 src/common
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Identifiers.ma
r2418 r2420 326 326 ]. 327 327 328 (* Fold over the entries in a map. There are some lemmas to help reason about 329 this near the bottom of the file (they require sets). *) 330 328 331 definition foldi: 329 332 ∀A, B: Type[0]. … … 1120 1123 1121 1124 1122 1125 (* Returns the domain of a map as the canonical set (one made only from the 1126 empty set and addition. *) 1127 definition domain_of_map : ∀tag,A. identifier_map tag A → identifier_set tag ≝ 1128 λtag,A,m. an_id_map tag unit (domain_of_pm A (match m with [ an_id_map m ⇒ m ])). 1129 lemma domain_of_map_present : ∀tag,A,m,id. 1130 present tag A m id ↔ present tag unit (domain_of_map … m) id. 1131 #tag #A * #m * #p @domain_of_pm_present 1132 qed. 1133 1134 (* Some lemmas for reasoning about folds. *) 1135 1136 lemma foldi_ind : ∀A,B,tag,f,m,b. ∀P:B → identifier_set tag → Prop. 1137 P b (empty_set …) → 1138 (∀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)) → 1139 P (foldi A B tag f m b) (domain_of_map … m). 1140 #A #B #tag #f * #m #b #P #P0 #STEP 1141 whd in match (foldi ??????); change with (an_id_map ?? (domain_of_pm A m)) in match (domain_of_map ???); 1142 @pm_fold_ind 1143 [ @P0 1144  #p #ps #a #b0 #FR #L #pre @(STEP (an_identifier tag p) (an_id_map tag unit ps)) 1145 [ normalize >FR /3/ 1146  @L 1147  @pre 1148 ] 1149 ] qed. 1150 1151 lemma foldi_ind' : ∀A,B,tag,f,m,b,b'. ∀P:B → identifier_set tag → Prop. 1152 P b (empty_set …) → 1153 (∀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)) → 1154 foldi A B tag f m b = b' → 1155 P b' (domain_of_map … m). 1156 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct @foldi_ind /2/ 1157 qed. 1158 
src/common/PositiveMap.ma
r2415 r2420 120 120 fold A B (λx.f (p1 x)) r b 121 121 ]. 122 123 definition domain_of_pm : ∀A. positive_map A → positive_map unit ≝ 124 λA,t. fold A (positive_map unit) (λp,a,b. insert unit p it b) t (pm_leaf unit). 125 126 (* Build some results about fold using domain_of_pm. *) 127 128 lemma pm_fold_ignore_adding_junk : ∀A. ∀m. ∀f,g:Pos → Pos. ∀s. 129 (∀p,q. f p ≠ g q) → 130 ∀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. 131 #A #m elim m 132 [ normalize // 133  #oa #l #r #IHl #IHr 134 #f #g #s #not_g #p 135 normalize 136 >IHr 137 [ >IHl 138 [ cases oa 139 [ normalize % 140  #a normalize >(lookup_opt_insert_miss ?? (f p)) [ %  @not_g ] 141 ] 142  #x #y % #E cases (not_g x (p0 y)) #H @H @E 143 ] 144  #x #y % #E cases (not_g x (p1 y)) #H @H @E 145 ] 146 ] qed. 147 148 lemma pm_fold_ind_gen : ∀A,B,m,f,b. 149 ∀pre:Pos→Pos. (∀x,y.pre x = pre y → x = y) → ∀ps. (∀p. lookup_opt ? (pre p) ps = None ?) → 150 ∀P:B → positive_map unit → Prop. 151 P b ps → 152 (∀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)) → 153 P (fold A B (λx. f (pre x)) m b) (fold ?? (λp,a,b. insert unit (pre p) it b) m ps). 154 #A #B #m elim m 155 [ // 156  #oa #l #r #IHl #IHr 157 #f #b #pre #PRE #ps #PS #P #emp #step whd in ⊢ (?%%); 158 @IHr 159 [ #x #y #E lapply (PRE … E) #E' destruct // 160  #p change with ((λx. pre (p1 x)) p) in match (pre (p1 p)); >pm_fold_ignore_adding_junk 161 [ cases oa [ @PS  #a >(lookup_opt_insert_miss ?? (pre (p1 p))) [ @PS  % #E lapply (PRE … E) #E' destruct ] ] 162  #p #q % #E lapply (PRE … E) #E' destruct 163 ] 164  @IHl 165 [ #x #y #E lapply (PRE … E) #E' destruct // 166  #p cases oa [ @PS  #a >(lookup_opt_insert_miss ?? (pre (p0 p))) [ @PS  % #E lapply (PRE … E) #E' destruct ] ] 167  cases oa in step ⊢ %; [ #_ @emp  #a #step normalize @step [ @PS  %  @emp ] ] 168  #p #ps' #a #b' @step 169 ] 170  #p #ps' #a #b' @step 171 ] 172 ] qed. 173 174 lemma pm_fold_ext : ∀A,B,m,f,b. 175 fold A B f m b = fold A B (λx:Pos. f x) m b. 176 #A #B #m elim m /4/ 177 qed. 178 179 (* Main result about folds. (Rather than producing a result about just the 180 domain of m we could use the whole mapping, but we'd need a function to 181 canonicalise maps because their representation can contain some junk.) *) 182 183 lemma pm_fold_ind : ∀A,B,f,m,b. ∀P:B → positive_map unit → Prop. 184 P b (pm_leaf unit) → 185 (∀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)) → 186 P (fold A B f m b) (domain_of_pm A m). 187 #A #B #f #m #b #P #emp #step 188 >pm_fold_ext 189 whd in ⊢ (??%); 190 @(pm_fold_ind_gen A B m f b (λx.x) ? (pm_leaf unit) ???) 191 [ // 192  // 193  @emp 194  @step 195 ] qed. 196 197 lemma pm_fold_eq : ∀A,B,b,f. 198 (∀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)) → 199 ∀p,s1,s2. 200 lookup_opt B p s1 = lookup_opt B p s2 → 201 lookup_opt B p (fold A (positive_map B) f b s1) = lookup_opt B p (fold A (positive_map B) f b s2). 202 #A #B #b elim b 203 [ #f #H #p #s1 #s2 #H @H 204  #oa #l #r #IHl #IHr #f #H #p #s1 #s2 #H' 205 whd in match (fold ???? s1); 206 whd in match (fold ???? s2); 207 @IHr [ #q #k #a #s1' #s2' #H'' @H @H'' ] 208 @IHl [ #q #k #a #s1' #s2' #H'' @H @H'' ] 209 cases oa [ @H'  #a @H @H' ] 210 ] qed. 211 212 213 lemma pm_fold_ignore_prefix : ∀A. ∀m. ∀pre:Pos → Pos. (∀x,y. pre x = pre y → x = y) → 214 ∀p. ∀pre'. 215 lookup_opt unit (pre p) (fold A ? (λx,a,b. insert unit (pre (pre' x)) it b) m (pm_leaf ?)) = 216 lookup_opt unit p (fold A ? (λx,a,b. insert unit (pre' x) it b) m (pm_leaf ?)). 217 #A #m #pre #PRE 218 cut (∀p. lookup_opt unit (pre p) (pm_leaf unit) = lookup_opt unit p (pm_leaf unit)) [ // ] 219 generalize in match (pm_leaf unit) in ⊢ ((? → ??%?) → ? → ? → ??%?); 220 generalize in match (pm_leaf unit); 221 elim m 222 [ #s1 #s2 #S #p #pre' @S 223  #oa #l #r #IHl #IHr 224 #s1 #s2 #S #p #pre' 225 whd in ⊢ (??(???%)(???%)); 226 @(IHr ???? (λx. pre' (p1 x))) 227 #p' @IHl 228 #p'' cases oa 229 [ @S 230  #a cases (decidable_eq_pos p'' (pre' one)) 231 [ #E destruct 232 >(lookup_opt_insert_hit ?? (pre (pre' one))) 233 >(lookup_opt_insert_hit ?? (pre' one)) 234 % 235  #NE >(lookup_opt_insert_miss ??? (pre (pre' one))) 236 [ >(lookup_opt_insert_miss ??? (pre' one)) // 237  % #E @(absurd … (PRE … E) NE) 238 ] 239 ] 240 ] 241 ] qed. 242 243 (* Link the domain of a map (used in the result about fold) to the original 244 map. *) 245 246 lemma domain_of_pm_present : ∀A,m,p. 247 lookup_opt A p m ≠ None ? ↔ lookup_opt unit p (domain_of_pm A m) ≠ None ?. 248 249 #A #m whd in match (domain_of_pm ??); 250 elim m 251 [ #p normalize /3/ 252  #oa #l #r #IHl #IHr 253 whd in match (fold ???? (pm_leaf unit)); 254 * 255 [ change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?))); 256 >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ] 257 change with ((λx:Pos. one) one) in ⊢ (??(?(??(??%?)?))); 258 >pm_fold_ignore_adding_junk [2: #p #q % #E destruct ] 259 cases oa 260 [ normalize /3/ 261  #a change with (insert unit one ??) in ⊢ (??(?(??(???%)?))); 262 >(lookup_opt_insert_hit ?? one) normalize 263 % #_ % #E destruct 264 ] 265  #p >(pm_fold_eq ??????? (pm_leaf unit)) 266 [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ] 267 @IHr 268  >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ] 269 cases oa 270 [ % 271  #a >(lookup_opt_insert_miss ?? (p1 p)) [2: % #E destruct ] 272 % 273 ] 274  #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p1 y)) 275 [ #E destruct 276 >(lookup_opt_insert_hit ?? (p1 y)) 277 >(lookup_opt_insert_hit ?? (p1 y)) 278 % 279  #NE >(lookup_opt_insert_miss ?? x … NE) 280 >(lookup_opt_insert_miss ?? x … NE) 281 @S 282 ] 283 ] 284  #p 285 >pm_fold_ignore_adding_junk [2: #x #y % #E destruct ] 286 >(pm_fold_eq ??????? (pm_leaf unit)) 287 [ >pm_fold_ignore_prefix [2: #x #y #E destruct % ] 288 @IHl 289  cases oa 290 [ % 291  #a >(lookup_opt_insert_miss ?? (p0 p)) [2: % #E destruct ] 292 % 293 ] 294  #x #y #a #s1 #s2 #S cases (decidable_eq_pos x (p0 y)) 295 [ #E destruct 296 >(lookup_opt_insert_hit ?? (p0 y)) 297 >(lookup_opt_insert_hit ?? (p0 y)) 298 % 299  #NE >(lookup_opt_insert_miss ?? x … NE) 300 >(lookup_opt_insert_miss ?? x … NE) 301 @S 302 ] 303 ] 304 ] 305 ] qed. 306 122 307 123 308 lemma update_fail : ∀A,b,a,t.
Note: See TracChangeset
for help on using the changeset viewer.