Changeset 2415 for src/common/PositiveMap.ma
- Timestamp:
- Oct 23, 2012, 3:57:02 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/PositiveMap.ma
r2335 r2415 590 590 λA,B,t,f,b. pm_fold_inf_aux A B t f t (λx.x) b (λp. refl ??). 591 591 592 (* Find an entry in the map matching the given predicate *) 593 594 let rec pm_find_aux (pre: Pos → Pos) (A:Type[0]) (t: positive_map A) (p:Pos → A → bool) on t : option (Pos × A) ≝ 595 match t with 596 [ pm_leaf ⇒ None ? 597 | pm_node a l r ⇒ 598 let x ≝ match a with 599 [ Some a ⇒ if p (pre one) a then Some ? 〈pre one, a〉 else None ? 600 | None ⇒ None ? 601 ] in 602 match x with 603 [ Some x ⇒ Some ? x 604 | None ⇒ 605 match pm_find_aux (λx. pre (p0 x)) A l p with 606 [ None ⇒ pm_find_aux (λx. pre (p1 x)) A r p 607 | Some y ⇒ Some ? y 608 ] 609 ] 610 ]. 611 612 definition pm_find : ∀A:Type[0]. positive_map A → (Pos → A → bool) → option (Pos × A) ≝ 613 pm_find_aux (λx.x). 614 615 lemma pm_find_aux_pre : ∀A,t,pre,p,q,a. 616 pm_find_aux pre A t p = Some ? 〈q,a〉 → 617 ∃q'. q = pre q'. 618 #A #t elim t 619 [ normalize #pre #p #q #a #E destruct 620 | * [2:#a] #l #r #IHl #IHr #pre #p #q #a' normalize 621 [ cases (p (pre one) a) normalize [ #E destruct /2/ ] ] 622 lapply (IHl (λx. pre (p0 x)) p) 623 cases (pm_find_aux ?? l ?) 624 [ 1,3: #_ normalize 625 lapply (IHr (λx. pre (p1 x)) p) 626 cases (pm_find_aux ?? r ?) 627 [ 1,3: #_ #E destruct 628 | *: * #q' #a'' #H #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/ 629 ] 630 | *: * #q' #a'' #H normalize #E destruct cases (H ?? (refl ??)) #q'' #E destruct /2/ 631 ] 632 ] qed. 633 634 (* XXX: Hmm... destruct doesn't work properly with this, not sure why *) 635 lemma option_pair_f_eq : ∀A,B:Type[0].∀a,a',b,b'. ∀f:A → A. 636 (∀a,a'. f a = f a' → a = a') → 637 Some (A×B) 〈f a,b〉 = Some ? 〈f a',b'〉 → 638 a = a' ∧ b = b'. 639 #A #B #a #a' #b #b' #f #EXT #E 640 cut (f a = f a') [ destruct (E) destruct (e0) @e2 (* WTF? *) ] 641 #E' >(EXT … E') in E ⊢ %; #E destruct /2/ 642 qed. 643 644 lemma pm_find_lookup : ∀A,p,q,a,t. 645 pm_find A t p = Some ? 〈q,a〉 → 646 lookup_opt A q t = Some ? a. 647 #A #p #q #a normalize #t 648 change with ((λx.x) q) in match q in ⊢ (% → ?); 649 cut (∀y,z:Pos. (λx.x) y = (λx.x) z → y = z) // 650 generalize in match q; -q generalize in match (λx.x); 651 elim t 652 [ #pre #q #_ normalize #E destruct 653 | * [2:#a'] #l #r #IHl #IHr #pre #q #PRE 654 normalize [ cases (p (pre one) a') normalize [ #E cases (option_pair_f_eq … pre PRE E) #E1 #E2 destruct normalize % ] ] 655 lapply (IHl (λx.pre (p0 x))) 656 lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p) 657 cases (pm_find_aux ?? l ?) 658 [ 1,3: #_ #_ normalize 659 lapply (IHr (λx.pre (p1 x))) 660 lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p) 661 cases (pm_find_aux ?? r ?) 662 [ 1,3: #_ #_ #E destruct 663 | *: * #q' #a' #H1 #H2 #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct 664 whd in ⊢ (??%?); @H2 // 665 #y #z #E lapply (PRE … E) #E' destruct // 666 ] 667 | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 ?? (refl ??)) #q'' #E lapply (PRE … E) #E' destruct 668 whd in ⊢ (??%?); @H2 // 669 #y #z #E lapply (PRE … E) #E' destruct // 670 ] 671 ] qed. 672 673 lemma pm_find_predicate : ∀A,t,p,q,a. 674 pm_find A t p = Some ? 〈q,a〉 → 675 p q a. 676 #A #t #p normalize #q 677 change with ((λx.x) q) in match q; generalize in match q; -q generalize in match (λx.x); 678 elim t 679 [ normalize #pre #q #a #E destruct 680 | * [2:#a'] #l #r #IHl #IHr #pre #q #a normalize 681 [ lapply (refl ? (p (pre one) a')) cases (p (pre one) a') in ⊢ (???% → %); 682 [ #E normalize #E' 683 cut (pre one = pre q) [ destruct (E') destruct (e0) @e2 (* XXX ! *) ] 684 #E'' <E'' in E' ⊢ %; #E' destruct >E % 685 | #_ normalize 686 ] 687 ] 688 lapply (IHl (λx.pre (p0 x))) 689 lapply (pm_find_aux_pre A l (λx.pre (p0 x)) p) 690 cases (pm_find_aux ?? l ?) 691 [ 1,3: #_ #_ normalize 692 lapply (IHr (λx.pre (p1 x))) 693 lapply (pm_find_aux_pre A r (λx.pre (p1 x)) p) 694 cases (pm_find_aux ?? r ?) 695 [ 1,3: #_ #_ #E destruct 696 | *: * #q' #a' #H1 #H2 #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E % 697 ] 698 | *: * #q' #a' #H1 #H2 normalize #E destruct cases (H1 … (refl ??)) #q'' #E >E @H2 >E % 699 ] 700 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.