 Timestamp:
 May 31, 2011, 6:05:18 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r870 r871 351 351 ∀m, n: nat. ((Vector addressing_mode_tag m ⊎ Vector addressing_mode_tag n) → bool) → bool. 352 352 353 (* 353 354 definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝ 354 355 λP. … … 427 428  @ (instruction_elim INSTR) 428 429 ]. 429 430 *) 431 430 432 (* This establishes the correspondence between pseudo program counters and 431 433 program counters. It is at the heart of the proof. *) … … 550 552 construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None … 551 553 → False. 554 555 lemma BitVectorTrie_O: 556 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0. 557 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??)) 558 [ #w #_ %1 %[@w] % 559  #n #l #r #abs @⊥ // 560  #n #EQ %2 >EQ %] 561 qed. 562 563 lemma BitVectorTrie_Sn: 564 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n). 565 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%) 566 [ #m #abs @⊥ // 567  #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] // 568  #m #EQ %2 // ] 569 qed. 570 571 lemma lookup_prepare_trie_for_insertion_hit: 572 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n. 573 lookup … b (prepare_trie_for_insertion … b v) a = v. 574 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize // 575 qed. 576 577 lemma lookup_insert_hit: 578 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. 579 lookup … b (insert … b v t) a = v. 580 #A #a #v #n #b elim b b n // 581 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t) 582 [ * #l * #r #JMEQ >JMEQ cases hd normalize // 583  #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ] 584 qed. 585 586 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. 587 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) // 588 #n #hd #tl #abs @⊥ // 589 qed. 590 591 lemma BitVector_Sn: ∀n.∀v:BitVector (S n). 592 ∃hd.∃tl.v ≃ VCons bool n hd tl. 593 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))) 594 [ #abs @⊥ // 595  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] 596 qed. 597 598 lemma lookup_prepare_trie_for_insertion_miss: 599 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n. 600 (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a. 601 #A #a #v #n #c elim c 602 [ #b >(BitVector_O … b) normalize #abs @⊥ // 603  #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 604 cases hd cases hd' normalize 605 [2,3: #_ cases tl' // 606 *: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]] 607 qed. 608 609 lemma lookup_insert_miss: 610 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n. 611 (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a. 612 #A #a #v #n #c elim c c n 613 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF // 614  #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 615 #t cases(BitVectorTrie_Sn … t) 616 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 617 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // 618  #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 619 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize 620 [3,4: cases tl' //  *: @lookup_prepare_trie_for_insertion_miss //]]] 621 qed. 552 622 553 623 definition build_maps' ≝
Note: See TracChangeset
for help on using the changeset viewer.