 Timestamp:
 May 31, 2011, 5:28:21 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r868 r869 544 544 construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None … 545 545 → False. 546 547 lemma BitVectorTrie_O: 548 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0. 549 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??)) 550 [ #w #_ %1 %[@w] % 551  #n #l #r #abs @⊥ // 552  #n #EQ %2 >EQ %] 553 qed. 554 555 lemma BitVectorTrie_Sn: 556 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n). 557 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%) 558 [ #m #abs @⊥ // 559  #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] // 560  #m #EQ %2 // ] 561 qed. 562 563 lemma lookup_prepare_trie_for_insertion_hit: 564 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n. 565 lookup … b (prepare_trie_for_insertion … b v) a = v. 566 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize // 567 qed. 568 569 lemma lookup_insert_hit: 570 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. 571 lookup … b (insert … b v t) a = v. 572 #A #a #v #n #b elim b b n // 573 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t) 574 [ * #l * #r #JMEQ >JMEQ cases hd normalize // 575  #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ] 576 qed. 577 578 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. 579 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) // 580 #n #hd #tl #abs @⊥ // 581 qed. 582 583 lemma BitVector_Sn: ∀n.∀v:BitVector (S n). 584 ∃hd.∃tl.v ≃ VCons bool n hd tl. 585 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))) 586 [ #abs @⊥ // 587  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] 588 qed. 589 590 lemma lookup_insert_miss: 591 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n. 592 (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a. 593 #A #a #v #n #c elim c c n 594 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF // 595  #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 596 #t cases(BitVectorTrie_Sn … t) 597 [ * #l * #r #JMEQ >JMEQ cases hd #H CSC 598 normalize in H; 599 600 normalize // 601  #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ] 602 qed. 546 603 547 604 definition build_maps' ≝
Note: See TracChangeset
for help on using the changeset viewer.