Changeset 2599 for src/common
 Timestamp:
 Jan 31, 2013, 5:15:49 PM (8 years ago)
 Location:
 src/common
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Identifiers.ma
r2541 r2599 341 341 #tag #A * #m * #id * #id' #NE 342 342 @lookup_opt_pm_set_miss 343 /2 /343 /2 by not_to_not/ 344 344 qed. 345 345 … … 511 511 lapply (lookup_add_cases tag ?????? Some_eq_hyp) * 512 512 [1: 513 * #k_eq_hyp @⊥ /2 /513 * #k_eq_hyp @⊥ /2 by absurd/ 514 514 2: 515 #Some_eq_hyp' /2 /515 #Some_eq_hyp' /2 by / 516 516 ] 517 517 qed. … … 537 537 #tag #A #map #k #v #k' normalize 538 538 cases (identifier_eq ? k k') 539 [ #E /2 /540  #NE >lookup_add_miss /3 /539 [ #E /2 by or_introl/ 540  #NE >lookup_add_miss /3 by or_intror, conj, absurd, nmk/ 541 541 ] qed. 542 542 … … 675 675 [ %  #x %{x} % ] 676 676 qed. 677 677 (* 678 678 lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s. 679 679 #tag * normalize #m >map_opt_id_eq_ext // * % … … 694 694 >map_opt_id >map_opt_id // 695 695 qed. 696 696 *) 697 697 lemma mem_set_union : ∀tag.∀i : identifier tag.∀s,s' : identifier_set tag. 698 698 i ∈ (s ∪ s') = (i ∈ s ∨ i ∈ s'). … … 1015 1015 [ whd in C:(??%?); cases (pm_choose A m) in C ⊢ %; normalize [ #E destruct  * * #x #y #z #E destruct % ] ] 1016 1016 * * * #L1 #L2 #L3 #_ 1017 % [ % [ @L1  @L2 ]  * #id' cases (L3 id') [ /2 /  #L4 %2 @L4 ] ]1017 % [ % [ @L1  @L2 ]  * #id' cases (L3 id') [ /2 by or_introl/  #L4 %2 @L4 ] ] 1018 1018 qed. 1019 1019 … … 1063 1063 [ whd in C:(??%?); cases (pm_try_remove A id m) in C ⊢ %; normalize [ #E destruct  * #x #y #E destruct % ] ] 1064 1064 * * * #L1 #L2 #L3 #_ 1065 % [ % [ @L1  @L2 ]  * #id' cases (L3 id') [ /2 /  #L4 %2 @L4 ] ]1065 % [ % [ @L1  @L2 ]  * #id' cases (L3 id') [ /2 by or_introl/  #L4 %2 @L4 ] ] 1066 1066 qed. 1067 1067 … … 1140 1140 Exists ? (λid'. id = id') l. 1141 1141 #tag #l #id whd in match (set_of_list ??); 1142 cut (¬present ?? ∅ id) [ /3 / ]1142 cut (¬present ?? ∅ id) [ /3 by refl, absurd, nmk/ ] 1143 1143 generalize in match ∅; 1144 1144 elim l … … 1146 1146  #id' #tl #IH #s #F #PR whd in PR:(???%?); 1147 1147 cases (identifier_eq … id id') 1148 [ #E destruct /2 /1148 [ #E destruct /2 by or_introl/ 1149 1149  #NE %2 @(IH … PR) 1150 @(not_to_not … F) /2 /1150 @(not_to_not … F) /2 by present_add_present/ 1151 1151 ] 1152 1152 ] qed. … … 1173 1173 [ @P0 1174 1174  #p #ps #a #b0 #FR #L #pre @(STEP (an_identifier tag p) (an_id_map tag unit ps)) 1175 [ normalize >FR /3 /1175 [ normalize >FR /3 by absurd, nmk/ 1176 1176  @L 1177 1177  @pre … … 1184 1184 foldi A B tag f m b = b' → 1185 1185 P b' (domain_of_map … m). 1186 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct @foldi_ind /2 /1187 qed. 1188 1186 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct @foldi_ind /2 by / 1187 qed. 1188 
src/common/PositiveMap.ma
r2590 r2599 422 422 include "utilities/option.ma". 423 423 424 definition is_none : ∀A.option A → bool ≝ λA,o.match o with [ None ⇒ true  _ ⇒ false ]. 425 definition is_pm_leaf : ∀A.positive_map A → bool ≝ λA,m.match m with [ pm_leaf ⇒ true  _ ⇒ false ]. 426 424 427 let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝ 425 428 match b with 426 429 [ pm_leaf ⇒ pm_leaf ? 427  pm_node a l r ⇒ pm_node ? (!x ← a ; f x) 428 (map_opt ?? f l) 429 (map_opt ?? f r) 430  pm_node a l r ⇒ 431 let a' ≝ !x ← a ; f x in 432 let l' ≝ map_opt ?? f l in 433 let r' ≝ map_opt ?? f r in 434 if is_none … a' ∧ is_pm_leaf … l' ∧ is_pm_leaf … r' then 435 pm_leaf ? 436 else 437 pm_node ? a' l' r' 430 438 ]. 431 439 432 440 definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)). 441 442 lemma andb_false_r : ∀b.(b∧false)=false. *% qed. 433 443 434 444 lemma lookup_opt_map : ∀A,B,f,b,p. 435 445 lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x. 436 446 #A#B#f#b elim b [//] 437 #a #l #r #Hil #Hir * [//] 438 #p 439 whd in ⊢ (??(???%)(????%?)); 440 whd in ⊢ (??%?); // 441 qed. 442 447 #a #l #r #IHl #IHr * [2,3: #p ] 448 whd in match (map_opt ????); whd in match (lookup_opt ???) in ⊢ (???%); 449 [3: cases (! x ← a ; f x) [2: #x] try % cases (?∧?) % ] 450 inversion (map_opt ??? l) 451 [2,4: #lo #ll #lr #_ #_ >andb_false_r normalize nodelta #EQl <EQl 452 whd in ⊢ (??%?); // ] 453 #EQl 454 inversion (map_opt ??? r) 455 [2,4: #ro #rl #rr #_ #_ >andb_false_r normalize nodelta #EQr <EQr <EQl 456 whd in ⊢ (??%?); // ] 457 #EQr 458 [ <IHr >EQr  <IHl >EQl ] cases (?∧?) % 459 qed. 460 461 (* 443 462 lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m. 444 463 #A #m #f #Hf elim m [//] … … 449 468 #A #m @map_opt_id_eq_ext // 450 469 qed. 470 *) 451 471 452 472 let rec merge A B C (choice : option A → option B → option C) … … 458 478 [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a 459 479  pm_node o' l' r' ⇒ 460 match (choice o o') with 461 [None ⇒ 462 match (merge … choice l l') with 463 [pm_leaf ⇒ match (merge … choice r r') with 464 [pm_leaf ⇒ pm_leaf ? 465 _ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r') 466 ] 467 _ ⇒ pm_node ? (None ?) (merge … choice l l') (merge … choice r r') 468 ] 469 Some x ⇒ 470 pm_node ? (Some ? x) 471 (merge … choice l l') 472 (merge … choice r r') 473 ] 474 ]]. 480 let o'' ≝ choice o o' in 481 let l'' ≝ merge … choice l l' in 482 let r'' ≝ merge … choice r r' in 483 if is_none … o'' ∧ is_pm_leaf … l'' ∧ is_pm_leaf … r'' then 484 pm_leaf ? 485 else 486 pm_node ? o'' l'' r'' 487 ] 488 ]. 475 489 476 490 lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p. … … 478 492 lookup_opt … p (merge A B C choice a b) = 479 493 choice (lookup_opt … p a) (lookup_opt … p b). 480 #A#B#C#choice#a elim a 481 [ normalize#b494 #A#B#C#choice#a elim a a 495 [ #b 482 496  #o#l#r#Hil#Hir * [2: #o'#l'#r' * [2,3: #x] normalize cases(choice o o') normalize /2 by / 483 497 [3: cases (merge A B C choice l l') normalize /2 by / cases(merge A B C choice r r') … … 490 504 elim (lookup_opt ???) 491 505 normalize // 492 qed. 506 qed. 493 507 494 508 let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝ … … 504 518 interpretation "positive map size" 'card p = (domain_size ? p). 505 519 520 (* 506 521 lemma map_opt_size : ∀A,B,f,b.map_opt A B f b ≤ b. 507 522 #A#B#f#b elim b [//] … … 510 525 @le_plus assumption 511 526 qed. 527 *) 512 528 513 529 lemma map_size : ∀A,B,f,b.map A B f b = b. 514 530 #A#B#f#b elim b [//] 515 *[2:#x]#l#r#Hil#Hir normalize 516 >Hil >Hir @refl 531 *[2:#x]#l#r#Hil#Hir 532 [ normalize >Hil >Hir @refl ] 533 whd in match (map ????); 534 inversion (map_opt ??? l) 535 [2: #lo #ll #lr #_ #_ >andb_false_r normalize nodelta #EQl <EQl 536 whd in ⊢ (??%?); normalize nodelta >Hil >Hir % ] 537 #EQl 538 inversion (map_opt ??? r) 539 [2,4: #ro #rl #rr #_ #_ >andb_false_r normalize nodelta #EQr <EQr <EQl 540 whd in ⊢ (??%?); normalize nodelta >Hil >Hir % ] 541 #EQr normalize nodelta normalize 542 <Hil <Hir whd in match map; normalize nodelta >EQl >EQr % 517 543 qed. 518 544
Note: See TracChangeset
for help on using the changeset viewer.