Changeset 975


Ignore:
Timestamp:
Jun 16, 2011, 11:34:26 AM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r972 r975  
    10321032qed.
    10331033
    1034 lemma index_of_internal_None: ∀i,id,instr_list,n.
    1035  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
    1036   index_of_internal ? (instruction_matches_identifier id) instr_list n =
    1037    index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
    1038  #i #id #instr_list elim instr_list
    1039   [ #n #abs whd in abs; cases abs
    1040   | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
    1041     cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
    1042     [ #H %
    1043     | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
    1044       [ #_ % | #abs cases abs ]]]
    1045 qed.
    1046 
    1047 lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
    1048  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
    1049   address_of_word_labels_code_mem instr_list id =
    1050   address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
    1051  #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
    1052  >(index_of_internal_None … H) %
    1053 qed.
    1054 
    10551034lemma occurs_exactly_once_Some:
    10561035 ∀id,id',i,prefix.
     
    10691048qed.
    10701049
     1050lemma index_of_internal_None: ∀i,id,instr_list,n.
     1051 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
     1052  index_of_internal ? (instruction_matches_identifier id) instr_list n =
     1053   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
     1054 #i #id #instr_list elim instr_list
     1055  [ #n #abs whd in abs; cases abs
     1056  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
     1057    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
     1058    [ #H %
     1059    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
     1060      [ #_ % | #abs cases abs ]]]
     1061qed.
     1062
     1063lemma index_of_internal_Some_miss: ∀i,id,id'.
     1064 eq_bv ? id' id = false →
     1065 ∀instr_list,n.
     1066 occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
     1067  index_of_internal ? (instruction_matches_identifier id) instr_list n =
     1068   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id',i〉]) n.
     1069 #i #id #id' #EQ #instr_list #n #H generalize in match (occurs_exactly_once_Some … H) in ⊢ ?; >EQ
     1070 change with (occurs_exactly_once ?? → ?) generalize in match n; -n H; elim instr_list
     1071  [ #n #abs cases abs
     1072  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
     1073    [ // | #K @IH //]]
     1074qed.
     1075
     1076lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
     1077 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
     1078  address_of_word_labels_code_mem instr_list id =
     1079  address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id.
     1080 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
     1081 >(index_of_internal_None … H) %
     1082qed.
     1083
     1084lemma address_of_word_labels_code_mem_Some_miss: ∀i,id,id',instr_list.
     1085 eq_bv ? id' id = false →
     1086  occurs_exactly_once id (instr_list@[〈Some ? id',i〉]) →
     1087   address_of_word_labels_code_mem instr_list id =
     1088   address_of_word_labels_code_mem (instr_list@[〈Some … id',i〉]) id.
     1089 #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
     1090 >(index_of_internal_Some_miss … H) //
     1091qed.
     1092
    10711093axiom tech_pc_sigma00_append_Some:
    10721094 ∀program,prefix,costs,label,i,pc',code,ppc,pc.
     
    10801102   construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
    10811103    → False.
     1104
     1105lemma eq_false_to_notb: ∀b. b = false → ¬ b.
     1106 *; //
     1107qed.
     1108
     1109lemma eq_bv_sym: ∀n,v1,v2. eq_bv n v1 v2 = eq_bv n v2 v1.
     1110 #n #v1 #v2 @(eq_bv_elim … v1 v2) [// | #H >eq_bv_false /2/]
     1111qed.
    10821112
    10831113definition build_maps' ≝
     
    11251155   | #id normalize nodelta; -labels1; cases label; normalize nodelta
    11261156     [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 //
    1127      | #l
    1128      ]]
     1157     | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
     1158       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         
     1161        | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: /2/]
     1162          <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 //]]]
    11291163 | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2
    11301164   @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
Note: See TracChangeset for help on using the changeset viewer.