Changeset 2032 for src/ASM/ASM.ma
 Timestamp:
 Jun 8, 2012, 4:32:03 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASM.ma
r1882 r2032 75 75 ]. 76 76 77 lemma eq_a_to_eq: 78 ∀a,b. 79 eq_a a b = true → a = b. 80 #a #b 81 cases a cases b 82 #K 83 try cases (eq_true_false K) 84 % 85 qed. 86 87 lemma eq_a_reflexive: 88 ∀a. eq_a a a = true. 89 #a cases a % 90 qed. 91 92 let rec member_addressing_mode_tag 93 (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag) 94 on v: Prop ≝ 95 match v with 96 [ VEmpty ⇒ False 97  VCons n' hd tl ⇒ 98 bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a 99 ]. 100 101 lemma mem_decidable: 102 ∀n: nat. 103 ∀v: Vector addressing_mode_tag n. 104 ∀element: addressing_mode_tag. 105 mem … eq_a n v element = true ∨ 106 mem … eq_a … v element = false. 107 #n #v #element // 108 qed. 109 110 lemma eq_a_elim: 111 ∀tag. 112 ∀hd. 113 ∀P: bool → Prop. 114 (tag = hd → P (true)) → 115 (tag ≠ hd → P (false)) → 116 P (eq_a tag hd). 117 #tag #hd #P 118 cases tag 119 cases hd 120 #true_hyp #false_hyp 121 try @false_hyp 122 try @true_hyp 123 try % 124 #absurd destruct(absurd) 125 qed. 126 77 127 (* to avoid expansion... *) 78 128 let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝ … … 99 149 ]. 100 150 151 lemma is_a_decidable: 152 ∀hd. 153 ∀element. 154 is_a hd element = true ∨ is_a hd element = false. 155 #hd #element // 156 qed. 101 157 102 158 let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝ … … 106 162 is_a he A ∨ is_in ? tl A ]. 107 163 164 lemma is_a_to_mem_to_is_in: 165 ∀he,a,m,q. 166 is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true. 167 #he #a #m #q 168 elim q 169 [1: 170 #_ #K assumption 171 2: 172 #m' #t #q' #II #H1 #H2 173 normalize 174 change with (orb ??) in H2:(??%?); 175 cases (inclusive_disjunction_true … H2) 176 [1: 177 #K 178 <(eq_a_to_eq … K) >H1 % 179 2: 180 #K 181 >II 182 try assumption 183 cases (is_a t a) 184 normalize 185 % 186 ] 187 ] 188 qed. 189 190 lemma is_a_true_to_is_in: 191 ∀n: nat. 192 ∀x: addressing_mode. 193 ∀tag: addressing_mode_tag. 194 ∀supervector: Vector addressing_mode_tag n. 195 mem addressing_mode_tag eq_a n supervector tag → 196 is_a tag x = true → 197 is_in … supervector x. 198 #n #x #tag #supervector 199 elim supervector 200 [1: 201 #absurd cases absurd 202 2: 203 #n' #hd #tl #inductive_hypothesis 204 whd in match (mem … eq_a (S n') (hd:::tl) tag); 205 @eq_a_elim normalize nodelta 206 [1: 207 #tag_hd_eq #irrelevant 208 whd in match (is_in (S n') (hd:::tl) x); 209 <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta 210 @I 211 2: 212 #tag_hd_neq 213 whd in match (is_in (S n') (hd:::tl) x); 214 change with ( 215 mem … eq_a n' tl tag) 216 in match (fold_right … n' ? false tl); 217 #mem_hyp #is_a_hyp 218 cases(is_a hd x) 219 [1: 220 normalize nodelta // 221 2: 222 normalize nodelta 223 @inductive_hypothesis assumption 224 ] 225 ] 226 ] 227 qed. 228 108 229 record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝ 109 230 { … … 119 240 ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l 120 241 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?. 242 243 lemma is_in_subvector_is_in_supervector: 244 ∀m, n: nat. 245 ∀subvector: Vector addressing_mode_tag m. 246 ∀supervector: Vector addressing_mode_tag n. 247 ∀element: addressing_mode. 248 subvector_with … eq_a subvector supervector → 249 is_in m subvector element → is_in n supervector element. 250 #m #n #subvector #supervector #element 251 elim subvector 252 [1: 253 #subvector_with_proof #is_in_proof 254 cases is_in_proof 255 2: 256 #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof 257 whd in match (is_in … (hd':::tl') element); 258 cases (is_a_decidable hd' element) 259 [1: 260 #is_a_true >is_a_true 261 #irrelevant 262 whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof; 263 @(is_a_true_to_is_in … is_a_true) 264 lapply(subvector_with_proof) 265 cases(mem … eq_a n supervector hd') // 266 2: 267 #is_a_false >is_a_false normalize nodelta 268 #assm 269 @inductive_hypothesis 270 [1: 271 generalize in match subvector_with_proof; 272 whd in match (subvector_with … eq_a (hd':::tl') supervector); 273 cases(mem_decidable n supervector hd') 274 [1: 275 #mem_true >mem_true normalize nodelta 276 #assm assumption 277 2: 278 #mem_false >mem_false #absurd 279 cases absurd 280 ] 281 2: 282 assumption 283 ] 284 ] 285 ] 286 qed. 287 288 289 let rec subaddressing_mode_elim_type 290 (m: nat) (fixed_v: Vector addressing_mode_tag (S m)) (origaddr: fixed_v) 291 (Q: fixed_v → Prop) 292 (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v) 293 on v: Prop ≝ 294 match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with 295 [ VEmpty ⇒ λm_refl. λv_refl. Q origaddr 296  VCons n' hd tl ⇒ λm_refl. λv_refl. 297 let tail_call ≝ subaddressing_mode_elim_type m fixed_v origaddr Q n' tl ? 298 in 299 match hd return λa: addressing_mode_tag. a = hd → ? with 300 [ addr11 ⇒ λhd_refl. (∀w: Word11. Q (ADDR11 w)) → tail_call 301  addr16 ⇒ λhd_refl. (∀w: Word. Q (ADDR16 w)) → tail_call 302  direct ⇒ λhd_refl. (∀w: Byte. Q (DIRECT w)) → tail_call 303  indirect ⇒ λhd_refl. (∀w: Bit. Q (INDIRECT w)) → tail_call 304  ext_indirect ⇒ λhd_refl. (∀w: Bit. Q (EXT_INDIRECT w)) → tail_call 305  acc_a ⇒ λhd_refl. Q ACC_A → tail_call 306  registr ⇒ λhd_refl. (∀w: BitVector 3. Q (REGISTER w)) → tail_call 307  acc_b ⇒ λhd_refl. Q ACC_B → tail_call 308  dptr ⇒ λhd_refl. Q DPTR → tail_call 309  data ⇒ λhd_refl. (∀w: Byte. Q (DATA w)) → tail_call 310  data16 ⇒ λhd_refl. (∀w: Word. Q (DATA16 w)) → tail_call 311  acc_dptr ⇒ λhd_refl. Q ACC_DPTR → tail_call 312  acc_pc ⇒ λhd_refl. Q ACC_PC → tail_call 313  ext_indirect_dptr ⇒ λhd_refl. Q EXT_INDIRECT_DPTR → tail_call 314  indirect_dptr ⇒ λhd_refl. Q INDIRECT_DPTR → tail_call 315  carry ⇒ λhd_refl. Q CARRY → tail_call 316  bit_addr ⇒ λhd_refl. (∀w: Byte. Q (BIT_ADDR w)) → tail_call 317  n_bit_addr ⇒ λhd_refl. (∀w: Byte. Q (N_BIT_ADDR w)) → tail_call 318  relative ⇒ λhd_refl. (∀w: Byte. Q (RELATIVE w)) → tail_call 319 ] (refl … hd) 320 ] (refl … n) (refl_jmeq … v). 321 [20: 322 generalize in match proof; destruct 323 whd in match (subvector_with … eq_a (hd:::tl) fixed_v); 324 cases (mem … eq_a ? fixed_v hd) normalize nodelta 325 [1: 326 whd in match (subvector_with … eq_a tl fixed_v); 327 #assm assumption 328 2: 329 normalize in ⊢ (% → ?); 330 #absurd cases absurd 331 ] 332 ] 333 @(is_in_subvector_is_in_supervector … proof) 334 destruct @I 335 qed. 336 337 lemma subaddressing_mode_elim0: 338 ∀n: nat. 339 ∀v: Vector addressing_mode_tag (S n). 340 ∀addr: v. 341 ∀Q: v → Prop. 342 ∀m,w,H. 343 (∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) → 344 subaddressing_mode_elim_type n v addr Q m w H. 345 #n #v #addr #Q #m #w elim w 346 [ /2/ 347  #n' #hd #tl #IH cases hd #H 348 #INV whd #PO @IH #xaddr cases xaddr * 349 try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV 350 @ALREADYSEEN ] 351 qed. 352 353 lemma subaddressing_mode_elim: 354 ∀n: nat. 355 ∀v: Vector addressing_mode_tag (S n). 356 ∀addr: v. 357 ∀Q: v → Prop. 358 subaddressing_mode_elim_type n v addr Q (S n) v ?. 359 [ #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; // 360  @subvector_with_refl @eq_a_reflexive 361 ] 362 qed. 121 363 122 364 inductive preinstruction (A: Type[0]) : Type[0] ≝
Note: See TracChangeset
for help on using the changeset viewer.