Changeset 2590 for src/common/PositiveMap.ma
- Timestamp:
- Jan 24, 2013, 7:52:38 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/PositiveMap.ma
r2541 r2590 458 458 [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a 459 459 | pm_node o' l' r' ⇒ 460 pm_node ? (choice o o') 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) 461 471 (merge … choice l l') 462 472 (merge … choice r r') 463 473 ] 464 ] .474 ]]. 465 475 466 476 lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p. … … 470 480 #A#B#C#choice#a elim a 471 481 [ normalize #b 472 | #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /] 473 ] 474 #p#choice_good >lookup_opt_map 482 | #o#l#r#Hil#Hir * [2: #o'#l'#r' * [2,3: #x] normalize cases(choice o o') normalize /2 by / 483 [3: cases (merge A B C choice l l') normalize /2 by / cases(merge A B C choice r r') 484 normalize /2 by / 485 |*: #H [<Hir|<Hil] /2 by / cases(merge A B C choice l l') normalize /2 by / 486 cases (merge A B C choice r r') normalize /2 by / 487 ] 488 ]] 489 #p #choice_good >lookup_opt_map 475 490 elim (lookup_opt ???) 476 491 normalize // 477 qed. 492 qed. 478 493 479 494 let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
Note: See TracChangeset
for help on using the changeset viewer.