Changeset 975
 Timestamp:
 Jun 16, 2011, 11:34:26 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r972 r975 1032 1032 qed. 1033 1033 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_list1039 [ #n #abs whd in abs; cases abs1040  #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 1055 1034 lemma occurs_exactly_once_Some: 1056 1035 ∀id,id',i,prefix. … … 1069 1048 qed. 1070 1049 1050 lemma 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 ]]] 1061 qed. 1062 1063 lemma 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 //]] 1074 qed. 1075 1076 lemma 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) % 1082 qed. 1083 1084 lemma 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) // 1091 qed. 1092 1071 1093 axiom tech_pc_sigma00_append_Some: 1072 1094 ∀program,prefix,costs,label,i,pc',code,ppc,pc. … … 1080 1102 construct_costs program … ppc pc (λx.zero 16) (λx. zero 16) costs i = None … 1081 1103 → False. 1104 1105 lemma eq_false_to_notb: ∀b. b = false → ¬ b. 1106 *; // 1107 qed. 1108 1109 lemma 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/] 1111 qed. 1082 1112 1083 1113 definition build_maps' ≝ … … 1125 1155  #id normalize nodelta; labels1; cases label; normalize nodelta 1126 1156 [ #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 //]]] 1129 1163  (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2 1130 1164 @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
Note: See TracChangeset
for help on using the changeset viewer.