Changeset 977


Ignore:
Timestamp:
Jun 16, 2011, 12:12:59 PM (8 years ago)
Author:
sacerdot
Message:

#$%@#$@#$

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r975 r977  
    10741074qed.
    10751075
     1076lemma index_of_internal_Some_hit: ∀i,id.
     1077 ∀instr_list,n.
     1078  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
     1079   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n
     1080  = |instr_list| + n.
     1081 #i #id #instr_list elim instr_list
     1082  [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl %
     1083  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
     1084    [ >does_not_occur_absurd #abs cases abs | #H applyS (IH (S n)) //]]
     1085qed.
     1086
    10761087lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
    10771088 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
     
    10891100 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
    10901101 >(index_of_internal_Some_miss … H) //
     1102qed.
     1103
     1104lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
     1105  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
     1106   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
     1107   = bitvector_of_nat … (|instr_list|).
     1108 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
     1109 >(index_of_internal_Some_hit … H) //
    10911110qed.
    10921111
     
    11201139      let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
    11211140      let 〈pc',costs〉 ≝ pc_costs in
     1141       ppc' = length … pre ∧
    11221142       tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
    11231143       ∀id. occurs_exactly_once id pre →
     
    11491169   let 〈pc, costs〉 ≝ pc_costs in
    11501170    〈labels, costs〉.
    1151  [3: whd % // #id normalize in ⊢ (% → ?) #abs @⊥ //
    1152  | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2
    1153    cases construct in p4 #PC #CODE #JMEQ %
    1154    [ @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
     1171 [3: whd % [%] // #id normalize in ⊢ (% → ?) #abs @⊥ //
     1172 | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * #IH0 #IH1 #IH2
     1173   cases construct in p4 #PC #CODE #JMEQ % [%]
     1174   [ >length_append <IH0 normalize; //
     1175   | @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
    11551176   | #id normalize nodelta; -labels1; cases label; normalize nodelta
    11561177     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 //
    11571178     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
    11581179       generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
    1159         [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit
    1160          
     1180        [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit
     1181          <IH0
    11611182        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: /2/]
    11621183          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 //]]]
    1163  | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2
     1184 | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2
    11641185   @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
    11651186qed.
Note: See TracChangeset for help on using the changeset viewer.