Ignore:
Timestamp:
Jun 3, 2011, 6:36:00 PM (9 years ago)
Author:
sacerdot
Message:

Merged done well.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r877 r883  
    439439 ∀P. instruction_elim P = true → ∀i. P i = true.
    440440
    441 definition eq_instruction ≝
     441(*definition eq_instruction ≝
    442442  λi, j: instruction.
    443     true.
    444    
     443    true.*)
     444axiom eq_instruction: instruction → instruction → bool.
    445445let rec vect_member
    446446  (A: Type[0]) (n: nat) (eq: A → A → bool)
     
    495495    # A15 # A16 # A17 # A18 # A19 # X
    496496    cases X
    497     # SUB
     497    # SUB cases daemon ] qed.(*
    498498    cases SUB
    499499    [ # BYTE
     
    577577    cases (is_a hd (subaddressing_modeel y tl H)) whd // ]
    578578qed.
    579 
     579*)
    580580(*
    581581lemma test:
     
    590590 ]*)
    591591
     592lemma BitVectorTrie_O:
     593 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
     594 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
     595  [ #w #_ %1 %[@w] %
     596  | #n #l #r #abs @⊥ //
     597  | #n #EQ %2 >EQ %]
     598qed.
     599
     600lemma BitVectorTrie_Sn:
     601 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
     602 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
     603  [ #m #abs @⊥ //
     604  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
     605  | #m #EQ %2 // ]
     606qed.
     607
     608lemma lookup_prepare_trie_for_insertion_hit:
     609 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
     610  lookup … b (prepare_trie_for_insertion … b v) a = v.
     611 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
     612qed.
     613 
     614lemma lookup_insert_hit:
     615 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
     616  lookup … b (insert … b v t) a = v.
     617 #A #a #v #n #b elim b -b -n //
     618 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
     619  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
     620  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
     621qed.
     622
     623lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
     624 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
     625 #n #hd #tl #abs @⊥ //
     626qed.
     627
     628lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
     629 ∃hd.∃tl.v ≃ VCons bool n hd tl.
     630 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
     631 [ #abs @⊥ //
     632 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
     633qed.
     634
     635coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
     636
     637lemma lookup_prepare_trie_for_insertion_miss:
     638 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
     639  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
     640 #A #a #v #n #c elim c
     641  [ #b >(BitVector_O … b) normalize #abs @⊥ //
     642  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     643    cases hd cases hd' normalize
     644    [2,3: #_ cases tl' //
     645    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
     646qed.
     647 
     648lemma lookup_insert_miss:
     649 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
     650  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
     651 #A #a #v #n #c elim c -c -n
     652  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
     653  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     654    #t cases(BitVectorTrie_Sn … t)
     655    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     656     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
     657    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     658     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
     659     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
     660qed.
     661
     662definition load_code_memory_aux ≝
     663 fold_left_i_aux … (
     664   λi, mem, v.
     665     insert … (bitvector_of_nat … i) v mem) (Stub Byte 16).
     666
     667axiom split_elim:
     668 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
     669  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
     670
     671axiom half_add_SO:
     672 ∀pc.
     673 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
     674
     675axiom not_eqvb_S:
     676 ∀pc.
     677 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))).
     678
     679axiom not_eqvb_SS:
     680 ∀pc.
     681 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))).
     682
    592683lemma test:
    593   ∀i.
    594       (let assembled ≝ assembly1 i in
    595       let code_memory ≝ load_code_memory assembled in
    596       let fetched ≝ fetch code_memory ? in
     684  ∀pc,i.
     685     (let assembled ≝ assembly1 i in
     686      let code_memory ≝ load_code_memory_aux pc assembled in
     687      let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
    597688      let 〈instr_pc, ticks〉 ≝ fetched in
    598689        eq_instruction (\fst instr_pc)) i = true.
    599  [ #i cases i #arg try #arg2 whd in ⊢ (??%?)
    600    [2: whd in ⊢ (??(match ? (? %) ?with [ _ ⇒ ?] ?)?)
     690 #pc #i cases i #arg try #arg2 whd in ⊢ (??%?)
     691   [2,4: @(list_addressing_mode_tags_elim_prop ? [[addr16]] ???????????????????? arg) whd try % #XX
     692         whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)
    601693       cases arg #sam cases sam #XX try #PP normalize in PP; try cases PP;
    602        whd in ⊢ (??(match ? (? %) ? with [ _ ⇒ ?] ?)?)
     694       whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) try cases PP normalize in XX;
     695       [1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17: cases XX
     696       |*:@split_elim #b1 #b2 #EQ >EQ -EQ;
     697        change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??)
     698        whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?)
     699        >lookup_insert_miss //
     700        >lookup_insert_miss //
     701        >lookup_insert_hit
     702        whd in ⊢ (??(match % with [ _ ⇒ ?] ?)?)
     703        whd in ⊢ (??%?) whd in ⊢ (??(?%?)?)
     704        >half_add_SO >half_add_SO
     705        >lookup_insert_miss [2,4: @not_eqvb_S]
     706        >lookup_insert_hit >lookup_insert_hit]
     707   |
     708       
     709       
     710         
    603711 
    604712   [2: #addr whd in ⊢ (??%?)
     
    698806qed.
    699807
    700 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
    701 
    702808lemma index_of_internal_None: ∀i,id,instr_list,n.
    703809 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
     
    733839    → False.
    734840
    735 lemma BitVectorTrie_O:
    736  ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
    737  #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
    738   [ #w #_ %1 %[@w] %
    739   | #n #l #r #abs @⊥ //
    740   | #n #EQ %2 >EQ %]
    741 qed.
    742 
    743 lemma BitVectorTrie_Sn:
    744  ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
    745  #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
    746   [ #m #abs @⊥ //
    747   | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
    748   | #m #EQ %2 // ]
    749 qed.
    750 
    751 lemma lookup_prepare_trie_for_insertion_hit:
    752  ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
    753   lookup … b (prepare_trie_for_insertion … b v) a = v.
    754  #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
    755 qed.
    756  
    757 lemma lookup_insert_hit:
    758  ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
    759   lookup … b (insert … b v t) a = v.
    760  #A #a #v #n #b elim b -b -n //
    761  #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
    762   [ * #l * #r #JMEQ >JMEQ cases hd normalize //
    763   | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
    764 qed.
    765 
    766 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.
    767  #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //
    768  #n #hd #tl #abs @⊥ //
    769 qed.
    770 
    771 lemma BitVector_Sn: ∀n.∀v:BitVector (S n).
    772  ∃hd.∃tl.v ≃ VCons bool n hd tl.
    773  #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))
    774  [ #abs @⊥ //
    775  | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
    776 qed.
    777 
    778 lemma lookup_prepare_trie_for_insertion_miss:
    779  ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
    780   (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
    781  #A #a #v #n #c elim c
    782   [ #b >(BitVector_O … b) normalize #abs @⊥ //
    783   | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    784     cases hd cases hd' normalize
    785     [2,3: #_ cases tl' //
    786     |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
    787 qed.
    788  
    789 lemma lookup_insert_miss:
    790  ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
    791   (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
    792  #A #a #v #n #c elim c -c -n
    793   [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
    794   | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
    795     #t cases(BitVectorTrie_Sn … t)
    796     [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    797      [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
    798     | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
    799      [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
    800      [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
    801 qed.
    802841
    803842definition build_maps' ≝
Note: See TracChangeset for help on using the changeset viewer.