Changeset 1516 for src/ASM/BitVectorTrie.ma
 Timestamp:
 Nov 19, 2011, 12:38:20 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVectorTrie.ma
r1479 r1516 61 61 (P → Q) → (∀a,t',P,Q.(P → Q) → f a t' P → f a t' Q) → fold A ? n f t P → fold A ? n f t Q. 62 62 #A #n #f #t #P #Q #H 63 generalize in match (refl ? n) generalize in match H H; generalize in match Q Q; generalize in match PP;64 elim t in f ⊢ (? → ? → ? → ???% → ? → ???%%%? → ???%%%?) 63 generalize in match (refl ? n); generalize in match H; H; generalize in match Q; Q; generalize in match P; P; 64 elim t in f ⊢ (? → ? → ? → ???% → ? → ???%%%? → ???%%%?); 65 65 [ #a #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(Hf (zero 0) a P Q HPQ HP) 66 66  #h #l #r #Hl #Hr #f #P #Q #HPQ #_ #Hf #HP normalize normalize in HP; @(Hl ? (fold A Prop h (λx.f (true:::x)) r P) (fold A Prop h (λx.f (true:::x)) r Q) ? (refl ? h) ?) … … 79 79 ∀P: Prop. 80 80 (∀a,t',P.f a t' P → P) → fold A Prop n f t P → P. 81 #A #n #f #t #P #H generalize in match (refl ? n) generalize in match H H; generalize in match PP;82 elim t in f ⊢ (? → ? → ???% → ???%%%? → ?) t81 #A #n #f #t #P #H generalize in match (refl ? n); generalize in match H; H; generalize in match P; P; 82 elim t in f ⊢ (? → ? → ???% → ???%%%? → ?); t 83 83 [ #a #f #P #Hf #_ normalize @(Hf [[]]) 84 84  #h #l #r #Hl #Hr #f #P #Hf #_ normalize #HP @(Hr (λx.f (true:::x))) … … 107 107  #n #t' #X #Y #HXY #HX %1 108 108 [ @(proj1 ? ? HX)  @HXY @(proj2 ? ? HX) ] 109  whd in Hl @Hl ]109  whd in Hl; @Hl ] 110 110 qed. 111 111 … … 170 170 ∀P:BitVector n → A → Prop. 171 171 forall A n t P → ∀a:A.∀b.lookup_opt A n b t = Some ? a → P b a. 172 #A #n #t #P generalize in match (refl ? n) elim t in P ⊢ (???% → ??%%? → ? → ? → ??(??%%%)? → ?)172 #A #n #t #P generalize in match (refl ? n); elim t in P ⊢ (???% → ??%%? → ? → ? → ??(??%%%)? → ?); 173 173 [ #x #f #_ #Hf #a #b whd in Hf; #Hb normalize in Hb; destruct >(BitVector_O b) @(proj1 ? ? Hf) 174 174  #h #l #r #Hl #Hr #f #_ #Hf #a #b #Hb cases (BitVector_Sn h b) … … 306 306 lemma BitVectorTrie_O: 307 307 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0. 308 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))308 #A #v generalize in match (refl … O); cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??)); 309 309 [ #w #_ %1 %[@w] % 310 310  #n #l #r #abs @⊥ destruct(abs) … … 314 314 lemma BitVectorTrie_Sn: 315 315 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n). 316 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)316 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%); 317 317 [ #m #abs @⊥ destruct(abs) 318 318  #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] // … … 350 350 (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a. 351 351 #A #a #v #n #c elim c c n 352 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //352 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF; // 353 353  #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 354 354 #t cases(BitVectorTrie_Sn … t) 355 355 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 356 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //356 [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // 357 357  #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 358 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize358 [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize 359 359 [3,4: cases tl' //  *: @lookup_prepare_trie_for_insertion_miss //]]] 360 360 qed. … … 363 363 ∀A.∀n.∀b.∀a. 364 364 lookup A n b (Stub A ?) a = a. 365 #A #n #b #a cases n in b ⊢ (??(??%%%?)?) 365 #A #n #b #a cases n in b ⊢ (??(??%%%?)?); 366 366 [ #b >(BitVector_O b) normalize @refl 367 367  #h #b cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb >Hb cases hd … … 375 375 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A. 376 376 lookup_opt A n b t = None A → ∀x.lookup A n b t x = x. 377 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?)377 #A #n #b #t #a generalize in match (refl ? n); elim t in b ⊢ (???% → ??(??%%%)? → ? → ?); 378 378 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct 379 379  #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb … … 389 389 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A. 390 390 lookup_opt A n b t = Some A a → ∀x.lookup A n b t x = a. 391 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?)391 #A #n #b #t #a generalize in match (refl ? n); elim t in b ⊢ (???% → ??(??%%%)? → ? → ?); 392 392 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct @refl 393 393  #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb … … 403 403 ∀A.∀n.∀b.∀t.∀x,a. 404 404 lookup A n b t x = a → x ≠ a → lookup_opt A n b t = Some A a. 405 #A #n #b #t #x #a generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ?)405 #A #n #b #t #x #a generalize in match (refl ? n); elim t in b ⊢ (???% → ? → ?); 406 406 [ #z #B #_ #H #Hx >(BitVector_O B) in H; normalize #H >H @refl 407 407  #h #l #r #Hl #Hr #B #_ #H #Hx cases (BitVector_Sn h B) #hd #X elim X; X #tl #HB … … 436 436 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. 437 437 lookup_opt … b (insert … b v t) = Some A v. 438 #A #v #n #b #t elim t in b ⊢ (??(??%%%)?) 438 #A #v #n #b #t elim t in b ⊢ (??(??%%%)?); 439 439 [ #x #b >(BitVector_O b) normalize @refl 440 440  #h #l #r #Hl #Hr #b cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb >Hb cases hd … … 442 442  normalize @Hl 443 443 ] 444  #n' #b cases n' in b ⊢ ? 444  #n' #b cases n' in b ⊢ ?; 445 445 [ #b >(BitVector_O b) normalize @refl 446 446  #m #b cases (BitVector_Sn m b) #hd #X elim X X; #tl #Hb >Hb cases hd … … 454 454 (notb (eq_bv ? b c)) → lookup_opt … b (insert … c v t) = lookup_opt … b t. 455 455 #A #v #n #c elim c c n 456 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //456 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF; // 457 457  #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 458 458 #t cases(BitVectorTrie_Sn … t) 459 459 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 460 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //460 [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // 461 461  #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 462 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize462 [1,4: change in H; with (bool_to_Prop (notb (eq_bv ???))) ] normalize 463 463 [3,4: cases tl' //  *: @lookup_opt_prepare_trie_for_insertion_miss //]]] 464 464 qed. … … 476 476 ] 477 477  #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize 478 [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %) #Heq3478 [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %); #Heq3 479 479 [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_prepare_trie_for_insertion_hit #X destruct (X) %2 // 480 2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H 480 2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H; 481 481 [1,3: #X %1 // 482 482 2,4: >Heq3 // … … 499 499 ∀A:Type[0].∀n:nat.∀b.∀a.∀t.∀P. 500 500 lookup_opt A n b t = (None A) → forall A n (insert A n b a t) P → forall A n t P. 501 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ??(??%%%)? → ??%%% → ??%%%)501 #A #n #b #a #t generalize in match (refl ? n); elim t in b ⊢ (???% → ? → ??(??%%%)? → ??%%% → ??%%%); 502 502 [ #x #b #_ #P >(BitVector_O b) normalize #H destruct 503 503  #h #l #r #Hl #Hr #b #_ #P cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb >Hb cases hd #Hlookup #H … … 527 527 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P:(BitVector n → A → Prop). 528 528 (∀x.(lookup_opt A n b t = Some A x) → P b x) → forall A n (insert A n b a t) P → forall A n t P. 529 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ? → ??%%% → ?)529 #A #n #b #a #t generalize in match (refl ? n); elim t in b ⊢ (???% → % → ? → ??%%% → ?); 530 530 [ #x #b #_ #P >(BitVector_O b) normalize #HP #Hf %1 [ @HP @refl  @(proj2 ? ? Hf) ] 531 531  #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb >Hb cases hd #P #HP #Hf … … 565 565 ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P. 566 566 forall A n t P → P b a → forall A n (insert A n b a t) P. 567 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ??%%% → %%? → ??%%%)567 #A #n #b #a #t generalize in match (refl ? n); elim t in b ⊢ (???% → % → ??%%% → %%? → ??%%%); 568 568 [ #x #b #_ #P >(BitVector_O b) normalize #H1 #H2 /2/ 569 569  #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X X; #tl #Hb >Hb cases hd #P #Hf #HP … … 587 587 ] 588 588 ] 589  #n #b #_ elim b in t ⊢ (% → ? → ? → ??%%%) 589  #n #b #_ elim b in t ⊢ (% → ? → ? → ??%%%); 590 590 [ #b #P #Hf #HP normalize %1 [ @HP  // ] 591 591  #h #hd #tl #H #b #P #Hf cases hd #HP normalize @(forall_prepare_tree_for_insertion A h tl a ? HP) … … 603 603 ] 604 604  #m #IH #b @(vector_inv_n … b) #hd #tl #a #t cases (BitVectorTrie_Sn … t) 605 [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?) 605 [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?); 606 606 #X lapply (option_map_none … X) @IH 607 607  #E >E normalize // … … 622 622 cases (BitVectorTrie_Sn … t) 623 623 [ * #t1 * #t2 #E' >E' 624 whd in ⊢ (??%? → ??%?) cases bhd #U624 whd in ⊢ (??%? → ??%?); cases bhd #U 625 625 cases (option_map_some ????? U) 626 626 #tn' * #U' #E'' <E'' 627 whd in ⊢ (??%?) whd in ⊢ (??(???%%)?)627 whd in ⊢ (??%?); whd in ⊢ (??(???%%)?); 628 628 @(IH … U') 629 629  #E >E normalize #E' destruct … … 642 642 @(vector_inv_n … b) #bhd #btl 643 643 cases (BitVectorTrie_Sn … t) 644 [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?) cases bhd644 [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?); cases bhd 645 645 #U cases (option_map_some ????? U) #tn' * #U' #E' <E' 646 646 #b' @(vector_inv_n … b') #bhd' #btl' 647 647 cases bhd' 648 648 [ 2,3: #_ @refl 649  *: #NE whd in ⊢ (??%%) whd in ⊢ (??(???%%)(???%%))650 @(IH … U') % #E'' >E'' in NE * #H @H @refl649  *: #NE whd in ⊢ (??%%); whd in ⊢ (??(???%%)(???%%)); 650 @(IH … U') % #E'' >E'' in NE; * #H @H @refl 651 651 ] 652  #E >E whd in ⊢ (??%? → ?) #NE destruct652  #E >E whd in ⊢ (??%? → ?); #NE destruct 653 653 ] 654 654 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.