 Timestamp:
 May 31, 2011, 1:39:47 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r860 r861 1 1 include "ASM/Assembly.ma". 2 2 include "ASM/Interpret.ma". 3 4 (* RUSSEL **) 5 6 include "basics/jmeq.ma". 7 8 notation > "hvbox(a break ≃ b)" 9 non associative with precedence 45 10 for @{ 'jmeq ? $a ? $b }. 11 12 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)" 13 non associative with precedence 45 14 for @{ 'jmeq $t $a $u $b }. 15 16 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y). 17 18 lemma eq_to_jmeq: 19 ∀A: Type[0]. 20 ∀x, y: A. 21 x = y → x ≃ y. 22 // 23 qed. 24 25 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p. 26 definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w]. 27 28 coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?. 29 coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?. 30 31 axiom VOID: Type[0]. 32 axiom assert_false: VOID. 33 definition bigbang: ∀A:Type[0].False → VOID → A. 34 #A #abs cases abs 35 qed. 36 37 coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?. 38 39 lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p). 40 #A #P #p cases p #w #q @q 41 qed. 42 43 lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y. 44 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) % 45 qed. 46 47 coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?. 48 49 (* END RUSSELL **) 3 50 4 51 let rec foldl_strong_internal … … 59 106 qed. 60 107 61 include "basics/jmeq.ma".62 63 notation > "hvbox(a break ≃ b)"64 non associative with precedence 4565 for @{ 'jmeq ? $a ? $b }.66 67 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"68 non associative with precedence 4569 for @{ 'jmeq $t $a $u $b }.70 71 interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).72 73 lemma eq_to_jmeq:74 ∀A: Type[0].75 ∀x, y: A.76 x = y → x ≃ y.77 //78 qed.79 80 108 axiom vector_associativity_of_append: 81 109 ∀A: Type[0]. … … 94 122 ∀v: Vector A n. 95 123 a ::: v = [[ a ]] @@ v. 96 97 lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.98 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %99 qed.100 101 coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.102 124 103 125 lemma super_rewrite2: … … 234 256 *) 235 257 258 (* 236 259 let rec list_addressing_mode_tags_elim 237 260 (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝ … … 273 296 ] 274 297 ]. 275 (*276 298 277 299 definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝ … … 308 330 *) 309 331 310 (* RUSSEL **)311 312 definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.313 definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].314 315 coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.316 coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.317 318 axiom VOID: Type[0].319 axiom assert_false: VOID.320 definition bigbang: ∀A:Type[0].False → VOID → A.321 #A #abs cases abs322 qed.323 324 coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.325 326 lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).327 #A #P #p cases p #w #q @q328 qed.329 330 lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.331 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %332 qed.333 334 coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.335 336 (* END RUSSELL **)337 338 332 (* This establishes the correspondence between pseudo program counters and 339 333 program counters. It is at the heart of the proof. *) … … 397 391 axiom occurs_exactly_once: Identifier → list labelled_instruction → Prop. 398 392 393 lemma index_of_internal_None: ∀i,id,instr_list,n. 394 occurs_exactly_once id (instr_list@[〈None …,i〉]) → 395 index_of_internal ? (address_of_word_labels_internal id) instr_list n = 396 index_of_internal ? (address_of_word_labels_internal id) (instr_list@[〈None …,i〉]) n. 397 #i #id #instr_list elim instr_list 398 [ #n #abs (* ASSURDO *) 399  #hd #tl #IH #n #H whd in ⊢ (??%%) cases (address_of_word_labels_internal id hd) 400 whd in ⊢ (??%%) 401 [ % 402  @IH 403 ]] 404 qed. 405 406 lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list. 407 occurs_exactly_once id (instr_list@[〈None …,i〉]) → 408 address_of_word_labels_code_mem instr_list id = 409 address_of_word_labels_code_mem (instr_list@[〈None …,i〉]) id. 410 #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?)) 411 399 412 definition build_maps' ≝ 400 413 λpseudo_program. … … 407 420 let 〈labels,pc_costs〉 ≝ res in 408 421 let 〈ignore,costs〉 ≝ pc_costs in 409 ∀id. occurs_exactly_once id instr_list→410 lookup ?? id labels (zero …) = sigma pre' ( \snd (fetch_pseudo_instruction pre id)))422 ∀id. occurs_exactly_once id pre → 423 lookup ?? id labels (zero …) = sigma pre' (address_of_word_labels_code_mem pre id)) 411 424 instr_list 412 425 (λprefix,i,tl,prf,t. … … 437 450 >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) #IH1 438 451 whd in ⊢ (??(????%?)?) labels1; 439 cases label 440 [ whd in ⊢ (??(????%?)?)452 cases label in Hid 453 [ #Hid whd in ⊢ (??(????%?)?) 441 454 (* COMPLETARE *) 442 >IH1 455 >IH1 IH1 456 [ 457  458 ] 443 459  label #label whd in ⊢ (??(????%?)?) 444 460
Note: See TracChangeset
for help on using the changeset viewer.