Changeset 861


Ignore:
Timestamp:
May 31, 2011, 1:39:47 AM (8 years ago)
Author:
sacerdot
Message:

Statement of the lemma fixed (again!)
Some preliminary work on additional lemmas.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r860 r861  
    11include "ASM/Assembly.ma".
    22include "ASM/Interpret.ma".
     3
     4(* RUSSEL **)
     5
     6include "basics/jmeq.ma".
     7
     8notation > "hvbox(a break ≃ b)"
     9  non associative with precedence 45
     10for @{ 'jmeq ? $a ? $b }.
     11
     12notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
     13  non associative with precedence 45
     14for @{ 'jmeq $t $a $u $b }.
     15
     16interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
     17
     18lemma eq_to_jmeq:
     19  ∀A: Type[0].
     20  ∀x, y: A.
     21    x = y → x ≃ y.
     22  //
     23qed.
     24
     25definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
     26definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
     27
     28coercion inject nocomposites: ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
     29coercion eject nocomposites: ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
     30
     31axiom VOID: Type[0].
     32axiom assert_false: VOID.
     33definition bigbang: ∀A:Type[0].False → VOID → A.
     34 #A #abs cases abs
     35qed.
     36
     37coercion bigbang nocomposites: ∀A:Type[0].False → ∀v:VOID.A ≝ bigbang on _v:VOID to ?.
     38
     39lemma sig2: ∀A.∀P:A → Prop. ∀p:Σx:A.P x. P (eject … p).
     40 #A #P #p cases p #w #q @q
     41qed.
     42
     43lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
     44 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
     45qed.
     46
     47coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
     48
     49(* END RUSSELL **)
    350
    451let rec foldl_strong_internal
     
    59106qed.
    60107
    61 include "basics/jmeq.ma".
    62 
    63 notation > "hvbox(a break ≃ b)"
    64   non associative with precedence 45
    65 for @{ 'jmeq ? $a ? $b }.
    66 
    67 notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
    68   non associative with precedence 45
    69 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 
    80108axiom vector_associativity_of_append:
    81109  ∀A: Type[0].
     
    94122  ∀v: Vector A n.
    95123    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 ?=?.
    102124
    103125lemma super_rewrite2:
     
    234256  *)
    235257
     258(*
    236259let rec list_addressing_mode_tags_elim
    237260  (n: nat) (l: Vector addressing_mode_tag (S n)) on l: (l → bool) → bool ≝
     
    273296      ]
    274297  ].
    275 (*
    276298
    277299definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
     
    308330*)
    309331 
    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 abs
    322 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 @q
    328 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 
    338332(* This establishes the correspondence between pseudo program counters and
    339333   program counters. It is at the heart of the proof. *)
     
    397391axiom occurs_exactly_once: Identifier → list labelled_instruction → Prop.
    398392
     393lemma 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    ]]
     404qed.
     405
     406lemma 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
    399412definition build_maps' ≝
    400413  λpseudo_program.
     
    407420      let 〈labels,pc_costs〉 ≝ res in
    408421      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))
    411424    instr_list
    412425    (λprefix,i,tl,prf,t.
     
    437450   >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) #IH1
    438451   whd in ⊢ (??(????%?)?) -labels1;
    439    cases label
    440     [ whd in ⊢ (??(????%?)?)
     452   cases label in Hid
     453    [ #Hid whd in ⊢ (??(????%?)?)
    441454      (* COMPLETARE *)
    442       >IH1
     455      >IH1 -IH1
     456       [       
     457       |
     458       ]
    443459    | -label #label whd in ⊢ (??(????%?)?)
    444460     
Note: See TracChangeset for help on using the changeset viewer.