Changeset 1134 for Deliverables/D3.3/idlookupbranch/ASM/BitVectorTrie.ma
 Timestamp:
 Aug 29, 2011, 5:45:03 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/ASM/BitVectorTrie.ma
r1074 r1134 524 524 ] 525 525 qed. 526 527 lemma update_fail : ∀A,n,b,a,t. 528 update A n b a t = None ? → 529 lookup_opt A n b t = None ?. 530 #A #n elim n 531 [ #b @(vector_inv_n … b) #a #t cases (BitVectorTrie_O … t) 532 [ * #x #E >E normalize #NE destruct 533  #E >E normalize // 534 ] 535  #m #IH #b @(vector_inv_n … b) #hd #tl #a #t cases (BitVectorTrie_Sn … t) 536 [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?) 537 #X lapply (option_map_none … X) @IH 538  #E >E normalize // 539 ] 540 ] qed. 541 542 lemma update_lookup_opt_same : ∀A,n,b,a,t,t'. 543 update A n b a t = Some ? t' → 544 lookup_opt A n b t' = Some ? a. 545 #A #n elim n 546 [ #b #a #t #t' @(vector_inv_n … b) 547 cases (BitVectorTrie_O … t) 548 [ * #x #E >E normalize #E' destruct @refl 549  #E >E normalize #E' destruct 550 ] 551  #m #IH #b #a #t #t' 552 @(vector_inv_n … b) #bhd #btl 553 cases (BitVectorTrie_Sn … t) 554 [ * #t1 * #t2 #E' >E' 555 whd in ⊢ (??%? → ??%?) cases bhd #U 556 cases (option_map_some ????? U) 557 #tn' * #U' #E'' <E'' 558 whd in ⊢ (??%?) whd in ⊢ (??(???%%)?) 559 @(IH … U') 560  #E >E normalize #E' destruct 561 ] 562 ] qed. 563 564 lemma update_lookup_opt_other : ∀A,n,b,a,t,t'. 565 update A n b a t = Some ? t' → 566 ∀b'. b ≠ b' → 567 lookup_opt A n b' t = lookup_opt A n b' t'. 568 #A #n elim n 569 [ #b #a #t #t' #E #b' 570 @(vector_inv_n … b) @(vector_inv_n … b') 571 * #NE cases (NE (refl ??)) 572  #m #IH #b #a #t #t' 573 @(vector_inv_n … b) #bhd #btl 574 cases (BitVectorTrie_Sn … t) 575 [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?) cases bhd 576 #U cases (option_map_some ????? U) #tn' * #U' #E' <E' 577 #b' @(vector_inv_n … b') #bhd' #btl' 578 cases bhd' 579 [ 2,3: #_ @refl 580  *: #NE whd in ⊢ (??%%) whd in ⊢ (??(???%%)(???%%)) 581 @(IH … U') % #E'' >E'' in NE * #H @H @refl 582 ] 583  #E >E whd in ⊢ (??%? → ?) #NE destruct 584 ] 585 ] qed. 586
Note: See TracChangeset
for help on using the changeset viewer.