 Timestamp:
 Jun 29, 2011, 10:47:39 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1043 r1045 1068 1068 insert … (bitvector_of_nat … i) v mem) (Stub Byte 16). 1069 1069 1070 axiom split_elim: 1070 lemma split_zero: 1071 ∀A,m. 1072 ∀v: Vector A m. 1073 〈[[]], v〉 = split A 0 m v. 1074 #A #m #v 1075 elim v 1076 [ % 1077  #n #hd #tl #ih 1078 normalize in ⊢ (???%) % 1079 ] 1080 qed. 1081 1082 lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A. 1083 #A #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) // 1084 #n #hd #tl #abs @⊥ destruct (abs) 1085 qed. 1086 1087 lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n). 1088 ∃hd.∃tl.v ≃ VCons A n hd tl. 1089 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))) 1090 [ #abs @⊥ destruct (abs) 1091  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] 1092 qed. 1093 1094 lemma vector_append_zero: 1095 ∀A,m. 1096 ∀v: Vector A m. 1097 ∀q: Vector A 0. 1098 v = q@@v. 1099 #A #m #v #q 1100 >(Vector_O A q) % 1101 qed. 1102 1103 lemma prod_eq_left: 1104 ∀A: Type[0]. 1105 ∀p, q, r: A. 1106 p = q → 〈p, r〉 = 〈q, r〉. 1107 #A #p #q #r #hyp 1108 >hyp % 1109 qed. 1110 1111 lemma prod_eq_right: 1112 ∀A: Type[0]. 1113 ∀p, q, r: A. 1114 p = q → 〈r, p〉 = 〈r, q〉. 1115 #A #p #q #r #hyp 1116 >hyp % 1117 qed. 1118 1119 corollary prod_vector_zero_eq_left: 1120 ∀A, n. 1121 ∀q: Vector A O. 1122 ∀r: Vector A n. 1123 〈q, r〉 = 〈[[ ]], r〉. 1124 #A #n #q #r 1125 generalize in match (Vector_O A q …) 1126 #hyp 1127 >hyp in ⊢ (??%?) 1128 % 1129 qed. 1130 1131 axiom split_succ: 1132 ∀A, m, n. 1133 ∀l: Vector A m. 1134 ∀r: Vector A n. 1135 ∀v: Vector A (m + n). 1136 ∀hd: A. 1137 v = l@@r → (〈l, r〉 = split A m n v → 〈hd:::l, r〉 = split A (S m) n (hd:::v)). 1138 (* 1139 #A #m 1140 elim m 1141 [ #n #l #r #v #hd #equal #hyp 1142 normalize >(Vector_O A l) >equal 1143 >(Vector_O A l) % 1144  #n' #ih #n #l #r #v #hd 1145 #equal #hyp 1146 cases(Vector_Sn A n' l) 1147 #hd' #exists 1148 cases exists #tl #jmeq 1149 >jmeq *) 1150 1151 lemma split_prod: 1152 ∀A,m,n. 1153 ∀p: Vector A (m + n). 1154 ∀v: Vector A m. 1155 ∀q: Vector A n. 1156 p = v@@q → 〈v, q〉 = split A m n p. 1157 #A #m 1158 elim m 1159 [ #n #p #v #q #hyp 1160 >hyp <(vector_append_zero A n q v) 1161 >(prod_vector_zero_eq_left A …) 1162 @split_zero 1163  #r #ih #n #p #v #q #hyp 1164 >hyp 1165 cases (Vector_Sn A r v) 1166 #hd #exists 1167 cases exists 1168 #tl #jmeq >jmeq 1169 @split_succ [1: % 2: @ih % ] 1170 ] 1171 qed. 1172 1173 lemma split_prod_exists: 1174 ∀A, m, n. 1175 ∀p: Vector A (m + n). 1176 ∃v: Vector A m. 1177 ∃q: Vector A n. 1178 〈v, q〉 = split A m n p. 1179 #A #m #n #p 1180 elim m 1181 @ex_intro 1182 [1: 1183 2: @ex_intro 1184 [1: 1185 2: 1186 ] 1187 ] 1188 1189 lemma split_elim: 1071 1190 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop. 1072 1191 (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v). 1192 #A #l #m #v #P #hyp 1193 normalize 1194 <(split_prod A l m v ? ? ?) 1073 1195 1074 1196 example half_add_SO: … … 1110 1232  cons hd tl ⇒ 1111 1233 let 〈new_pc, byte〉 ≝ next code_memory pc in 1112 hd = byte ∧ encoding_check code_memory new_ pc final_pc tl1234 hd = byte ∧ encoding_check code_memory new_c final_pc tl 1113 1235 ]. 1114 1236
Note: See TracChangeset
for help on using the changeset viewer.