Ignore:
Timestamp:
Mar 11, 2013, 1:02:02 PM (7 years ago)
Author:
piccolo
Message:

1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrUtils.ma

    r2801 r2843  
    2929
    3030definition sigma_map ≝  block → label → option label.
    31 definition lbl_funct ≝  block → label → option (list label).
    32 definition regs_funct ≝ block → label → option (list register).
     31definition lbl_funct ≝  block → label → (list label).
     32definition regs_funct ≝ block → label → (list register).
    3333
    3434(*TO BE MOVED*)
     
    4949! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl);
    5050!〈res,s〉 ← find ?? (joint_if_code … fn)
    51                 (λlbl.λ_. match f_lbls bl lbl with
    52                           [None ⇒ false
    53                           |Some lbls ⇒
    54                              match split_on_last … lbls with
    55                                 [None ⇒ eq_identifier … searched lbl
    56                                 |Some x ⇒ eq_identifier … searched (\snd x)
    57                                 ]
     51                (λlbl.λ_. match split_on_last … (f_lbls bl lbl) with
     52                          [None ⇒ eq_identifier … searched lbl
     53                          |Some x ⇒ eq_identifier … searched (\snd x)
    5854                          ]);
    5955return res.
     
    682678∀globals : list ident.∀fn,f_regs,r.
    683679(∀lbl. code_has_label p globals (joint_if_code … fn) lbl →
    684        opt_All … (λl.¬(bool_to_Prop (r ∈ l))) (f_regs lbl)) →
     680       ¬(bool_to_Prop (r ∈ (f_regs lbl)))) →
    685681¬ (r ∈ (set_from_list RegisterTag (added_registers p globals fn f_regs))).
    686682#p #globals #fn #f_regs #r #H whd in match added_registers; normalize nodelta
     
    689685lapply(H lbl ?)
    690686 [whd in match code_has_label; whd in match code_has_point; normalize nodelta
    691   whd in match (stmt_at ????); >EQstmt @I] cases(f_regs lbl)
    692   [ #_ @notb_Prop % assumption]
    693 #l whd in ⊢ (% → ?); normalize nodelta * #H1 @notb_elim @if_elim [2: #_ @I] #ABS
     687  whd in match (stmt_at ????); >EQstmt @I]
     688* #H1 @notb_elim @if_elim [2: #_ @I] #ABS
    694689lapply(mem_list_as_set … ABS) #ABS' cases(Exists_append … ABS') #ABS''
    695 [ @H1 @Exists_memb lapply ABS'' elim l [ *] #hd #tl #IH whd in ⊢ (% → %);
     690[ @H1 @Exists_memb lapply ABS'' elim (f_regs lbl) [ *] #hd #tl #IH whd in ⊢ (% → %);
    696691  * [ #EQ >EQ % %] #H %2 @IH @H
    697692| @IH @list_as_set_mem assumption
     
    699694qed.
    700695
     696lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀a : A.In A l1 a → In A (l1@l2) a.
     697#A #l1 elim l1 [#l2 #a *] #hd #tl #IH *
     698[#a normalize * [#H % assumption | #H %2 >append_nil assumption]]
     699#hd1 #tl1 #a normalize * [#H % assumption | #H %2 @IH assumption]
     700qed.
     701
     702lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀a : A.In A l2 a → In A (l1@l2) a.
     703#A #l1 #l2 lapply l1 -l1 elim l2 [#l1 #a *] #hd #tl #IH *
     704[#a normalize * [#H %1 assumption| #H %2 assumption]]
     705#hd1 #tl1 #a normalize *
     706[ #H %2 >append_cons @Exists_append1 >H elim tl1 [% %] #hd2 #tl2 #H1 normalize %2 //
     707| #H %2 >append_cons @IH assumption]
     708qed.
     709
     710lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
     711All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.
     712#A #P #l1 elim l1
     713[ #l2 change with l2 in ⊢ (???% → ?); #H % //]
     714#a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);
     715* #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //
     716qed.
     717
     718include alias "common/PositiveMap.ma".
     719
     720lemma added_register_pm : ∀A,B. ∀m : positive_map A.
     721∀f : Pos → list B.∀b.
     722let added ≝ fold A (list B) (λp.λ_.λacc.(f p)@acc) m [ ] in
     723All B (λx.x≠b) added →
     724(∀i. lookup_opt unit i (domain_of_pm A m) ≠ None ? → All B (λx.x≠b) (f i)).
     725#A #B #m #f #b normalize nodelta @pm_fold_ind
     726[ #_ #i normalize * #H @⊥ @H %
     727| #p #ps #a #lst #H #H1 #H2 #H3 #i cases(decidable_eq_pos i p)
     728  [1,3: #EQ destruct(EQ) #_ cases(append_All … H3) //
     729  |*: #Hi >lookup_opt_insert_miss [2,4: assumption] @H2
     730      cases(append_All … H3) //
     731  ]
     732]
     733qed.
     734
     735lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → 
     736decidable (In A l a).
     737#A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC)
     738[ #H % %2 assumption | * #H cases (DEC hd)
     739[ #H1 %1 %1 assumption | * #H1 %2 % * [ #H2 @H1 assumption | #H2 @H assumption]]
     740qed.
     741
     742lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l.
     743#A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption]
     744% #H1 @H % >H1 %
     745qed.
     746
     747lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a.
     748#A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % *
     749[ #H3 @H1 >H3 % | cases(IH a H2) #H3 #H4 @H3 assumption]
     750qed.
     751
     752lemma added_register_aux : ∀tag,A,B.∀m : identifier_map tag A.
     753∀f : identifier tag → list B.(∀b,b' : B.decidable (b=b')) →
     754let added ≝ foldi A (list B) tag (λl.λ_.λacc. (f l)@acc) m [ ] in
     755∀i,a,b.lookup tag A m i = Some ? a → In B (f i) b → In B added b.
     756#tag #A #B * #m #f #DEC * #i #a #b whd in ⊢ (??%? → ?); normalize nodelta
     757#H #H1
     758cases(decidable_In ? (foldi A (list B) tag
     759            (λl.λ_.λacc.(f l)@acc)
     760              (an_id_map tag A m) []) b (DEC b)) [//]
     761#H3 @⊥ lapply(In_all ??? H3) -H3 #H3
     762lapply(added_register_pm ?? m ?? H3 i ?)
     763[cases(domain_of_pm_present ? m i) #H4 #_ @H4 >H % #EQ destruct]
     764lapply H1 elim (f ?) [*] #hd #tl #IH * [#EQ * >EQ * #H4 #_ @H4 %]
     765#H4 * #_ @IH assumption
     766qed.
     767
     768lemma in_added_registers : ∀p : graph_params.
     769∀globals : list ident.∀fn,f_regs,r.
     770∀lbl.code_has_label p globals (joint_if_code … fn) lbl →
     771 In ? (f_regs lbl) r →
     772In ? (added_registers p globals fn f_regs) r.
     773#p #globals #fn #f_regs #r #lbl whd in match code_has_label;
     774whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
     775inversion(lookup LabelTag ???) [ #_ *] #stmt #EQstmt #_
     776#H @(added_register_aux …  EQstmt H)
     777* #p * #p' cases(decidable_eq_pos p p') [ #EQ destruct % % | * #H1 %2 % #EQ destruct @H1 %]
     778qed.
     779
    701780
    702781include alias "basics/lists/listb.ma".
    703782
    704 check eval_seq_no_pc
    705 
    706 xxxxxxxxxxxxxxxxxxxxxxxx
     783(*
     784definition get_internal_function_from_ident :
     785∀ p: sem_params. ∀ globals : list ident . ∀ge : genv_t (joint_function p globals).
     786ident → option (joint_closed_internal_function p globals) ≝
     787λp,globals,ge,id.
     788! bl  ← (find_symbol (joint_function p globals) ge id);
     789! bl' ← (code_block_of_block bl);
     790! 〈f,fn〉 ← res_to_opt … (fetch_internal_function ? ge bl');
     791return fn.
     792
     793lemma get_internal_function_from_ident_ok :
     794∀p : sem_params. ∀globals : list ident. ∀ge : genv_t (joint_function p globals).
     795∀bl,f,fn. fetch_internal_function ? ge bl = return 〈f,fn〉 →
     796get_internal_function_from_ident p globals ge f= return fn.
     797#p #globals #ge #bl #f #fn #EQf
     798@('bind_inversion EQf) * #f1 * #fn1 whd in match fetch_function;
     799normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H
     800#f2 #EQf2 #H @('bind_inversion H) -H #fn2 #EQfn2 whd in ⊢ (??%% → ??%% → ?);
     801#EQ1 #EQ2 destruct whd in match get_internal_function_from_ident; normalize nodelta
     802>(symbol_of_block_rev … EQf2) >m_return_bind
     803cut(code_block_of_block bl = return bl)
     804 [ whd in match code_block_of_block; normalize nodelta @match_reg_elim
     805   [ >(pi2 ?? bl) #ABS destruct] elim bl #bl1 #EQ #prf % ] #EQbl >EQbl
     806>m_return_bind >EQf %
     807qed.
     808*)
    707809
    708810lemma eval_seq_no_pc_no_call_ok :
     
    712814∀stack_size.
    713815∀bl.∀id.
    714 ∀seq.
    715 (∀fn : joint_closed_internal_function ERTL (prog_var_names … prog).
    716 ∀l. code_has_label … (joint_if_code … fn) l → 
    717 opt_All …
    718        (λlabs.(All … (λreg.bool_to_Prop(¬(reg ∈ labs)))
    719               (get_used_registers_from_seq … (functs … ERTL) seq)))
    720        (f_regs bl l))  →
     816∀fn : joint_closed_internal_function ERTL (prog_var_names … prog).∀seq.
     817(∀l. code_has_label … (joint_if_code … fn) l → 
     818(All … (λreg.bool_to_Prop(¬(reg ∈ (f_regs bl l))))
     819       (get_used_registers_from_seq … (functs … ERTL) seq)))  →
    721820   preserving1 ?? res_preserve1 ????
    722821      (sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
     
    729828             (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size))
    730829             id (seq_embed … seq)).
    731 #prog #f_lbls #f_regs #stack_size #bl #f #seq #fresh_regs
     830#prog #f_lbls #f_regs #stack_size #bl #f #fn #seq #fresh_regs
    732831cases seq in fresh_regs;
    733832[ #c #_ #st @mfr_return1
     
    738837       * [#r1 | #R1] #m_src [2: #_ @I] normalize nodelta #fresh_regs
    739838       @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    740        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H
     839       whd in ⊢ (% → %); * #H #_ @Prop_notb @H
    741840  | | #regs  @mfr_return_eq1 %
    742841  ]
     
    744843  [2:  @pop_ok |
    745844  | * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1
    746     [2: @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
    747        lapply(fresh_regs lbl Hlbl)
    748        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    749     | #regs  @mfr_return_eq1 %
     845    [2: @ps_reg_store_ok       
     846        @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
     847       whd in ⊢ (% → %); * #H #_ @Prop_notb @H
    750848    ]
    751849  ]
     
    769867       change with (sigma_beval prog f_lbls (BVptr …))
    770868                                               in ⊢ (???????(?????%?)?);
    771        @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    772        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
     869       @ps_reg_store_ok
     870              @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
     871       whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    773872    | #regs  @mfr_return_eq1 %
    774873    ]
     
    781880                                               in ⊢ (???????(?????%?)?);
    782881      @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    783        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #_ whd in ⊢ (% → ?); * #H
    784        #_ @Prop_notb @H|
     882       whd in ⊢ (% → %); * #_ * #H #_ @Prop_notb @H |
    785883    | #regs  @mfr_return_eq1 %
    786884    ]
     
    798896       | whd in match acca_store; normalize nodelta @mfr_bind1
    799897         [2: @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
    800              lapply(fresh_regs lbl Hlbl)
    801              cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
     898             lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    802899         | #regs  @mfr_return_eq1 %
    803900         ]
     
    805902         [2: whd in match sigma_state; normalize nodelta
    806903            @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
    807             lapply(fresh_regs lbl Hlbl)
    808             cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #_ * #H #_
    809             @Prop_notb @H |
     904            lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #_ * #H #_ @Prop_notb @H |
    810905         | #regs  @mfr_return_eq1 %
    811906         ]         
     
    823918      [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
    824919          @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    825        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
     920       whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    826921      | #regs  @mfr_return_eq1 %
    827922      ]
     
    837932        [ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
    838933        | whd in match acca_store; normalize nodelta @mfr_bind1
    839           [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok 
     934          [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
    840935              @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    841               cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
     936              whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    842937          | #regs  @mfr_return_eq1 %
    843938          ]
     
    860955        | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
    861956          [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
    862               @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    863               cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
     957          @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
     958          whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    864959          | #regs  @mfr_return_eq1 %
    865960          ]
     
    898993          change with (sigma_beval prog f_lbls (BVByte ?))
    899994               in ⊢ (???????(??%?)?);
    900           @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    901           cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H
    902       |
     995          @ps_reg_store_ok  @not_in_added_registers #lbl #Hlbl
     996          lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    903997      | #regs @mfr_return_eq1 %
    904998      ]
    905     ]
     999    ] 
    9061000  ]     
    9071001]
     1002#regs @mfr_return_eq1 %
    9081003qed.
    9091004
     
    9211016#H @('bind_inversion H) -H * #lbl2' #stmt2 #H2
    9221017whd in ⊢ (??%? → ?); #EQ destruct lapply(find_predicate ?????? H1)
    923 lapply(find_predicate ?????? H2) cases(good ??) normalize nodelta [*]
    924 *
     1018lapply(find_predicate ?????? H2) cases(good ??) normalize nodelta
    9251019  [ normalize nodelta @eq_identifier_elim #EQ1 *
    9261020    @eq_identifier_elim #EQ2 * >EQ1 >EQ2 %
     
    11891283qed.
    11901284
    1191 lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
    1192 All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.
    1193 #A #P #l1 elim l1
    1194 [ #l2 change with l2 in ⊢ (???% → ?); #H % //]
    1195 #a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);
    1196 * #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //
    1197 qed.
    1198 
    11991285include alias "common/Identifiers.ma".
    12001286
     
    12041290 ∀f_bl_r.
    12051291 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    1206      translate_data prog f_bl_r f_lbls f_regs →
     1292     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
    12071293∀id,fn,bl,pt,stmt.
    12081294fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 →
    12091295stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt → 
    1210 f_lbls bl pt = return [ ] → get_sigma prog f_lbls bl pt = return pt.
     1296f_lbls bl pt = [ ] → get_sigma prog f_lbls bl pt = return pt.
    12111297#prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #EQfn #EQstmt #EQlabels
    12121298cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
    12131299#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
    12141300[2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_
    1215 #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H * #lbls * #regs ** >EQlabels
    1216 whd in ⊢ (??%? → ?); #EQ destruct(EQ) #EQregs cases stmt in EQstmt; normalize nodelta
    1217 [3: * |2: * [#lbl || *] #EQstmt * #bl * whd in ⊢ (% → ?); cases regs in EQregs;
    1218     [2,4: #x #y #_ *] #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (%→?);
    1219     * #pref * #mid ** #EQmid whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
    1220     whd in ⊢ (% → ?); #EQt_stmt
     1301#_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H cases stmt in EQstmt;
     1302[3: *
     1303|2: * [#lbl || *] #EQstmt normalize nodelta * #bl * whd in ⊢ (% → ?);
     1304   inversion (f_regs ??) [2,4: #x #y #_ #_ *] #EQregs normalize nodelta
     1305   #EQ destruct(EQ) whd in ⊢ (%→?); * #pref * #mid ** #EQmid whd in ⊢ (% → ?);
     1306   * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); #EQt_stmt
    12211307| * [#c | * [#c_id|#c_ptr] #args #dest | #r #lbl | #seq ] #nxt #EQstmt
    12221308  whd in ⊢ (% → ?); * #bl >if_merge_right [2,4,6,8,10: %] * whd in ⊢ (% → ?);
    1223   cases regs in  EQregs; normalize nodelta
    1224   [2,4,5,8,10: [1,2,4,5: #x #y] #_ *|6: #r * [2: #x #y] ]
    1225   #EQregs [1,2: whd in ⊢ (% → ?); [*]] #EQ destruct(EQ) whd in ⊢ (% → ?);
     1309  inversion(f_regs ??) normalize nodelta
     1310  [2,4,5,8,10: [1,2,4,5: #x #y] #_ [1,2,3,4: #_] *|6: #r * [2: #x #y] ]
     1311  [1,2: #_] #EQregs [1,2: whd in ⊢ (% → ?); [*]] #EQ destruct(EQ) whd in ⊢ (% → ?);
    12261312  * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (%→ ?);
    12271313  [ * #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 *
    12281314    #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    12291315    whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ)
    1230      whd in EQmid1 : (???%); destruct(EQmid1) whd in e0 : (???%);
    1231      destruct(e0) ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%);
    1232      destruct(EQmid1) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt #EQ destruct(EQ)
    1233      whd in ⊢ (% → ?); * #_ #EQ destruct(EQ)
    1234 ] whd in match get_sigma; normalize nodelta >code_block_of_block_eq >m_return_bind
     1316     whd in EQmid1 : (???%); destruct(EQmid1) whd in e0 : (???%); >EQlabels in e0;
     1317    #e0 destruct(e0) ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%);
     1318     destruct(EQmid1) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt
     1319     change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
     1320     * #_ #EQ destruct(EQ) ]
     1321whd in match get_sigma; normalize nodelta >code_block_of_block_eq >m_return_bind
    12351322>EQfn >m_return_bind inversion(find ????)
    12361323[1,3,5,7,9,11: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQlabels
    12371324  normalize nodelta @eq_identifier_elim [1,3,5,7,9,11: #_ * |*: * #H #_ @H %]]
    12381325* #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
    1239 inversion(f_lbls ??) [1,3,5,7,9,11: #_ *] #l @(list_elim_left … l …)
    1240 normalize nodelta [1,3,5,7,9,11: #_ @eq_identifier_elim
    1241                          [1,3,5,7,9,11: #EQ destruct(EQ) #_ % |*: #_ *]]
    1242 #last #pre #_ #EQlbl >split_on_last_append normalize nodelta @eq_identifier_elim
     1326inversion(f_lbls ??)
     1327[1,3,5,7,9,11: #_ normalize nodelta @eq_identifier_elim [2,4,6,8,10,12: #_ *] #EQ #_ >EQ %]
     1328#lb #l @(list_elim_left … l …) normalize nodelta
     1329[1,3,5,7,9,11: #_ #EQlb @eq_identifier_elim
     1330               [1,3,5,7,9,11: #EQ destruct(EQ) #_ @⊥ |*: #_ *]
     1331               lapply(fresh_labs lbl) >EQlb *** #H #_ #_ @H
     1332               @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
     1333               whd in match code_has_point; normalize nodelta >EQstmt @I ]
     1334#last #pre #_ #_ #EQlbl >(split_on_last_append … (lb::pre) last)
     1335normalize nodelta @eq_identifier_elim
    12431336[2,4,6,8,10,12: #_ *] #EQ lapply EQlbl destruct(EQ) #EQlbl #_ @⊥
    1244 lapply(fresh_labs lbl) >EQlbl whd in ⊢ (% → ?); #H lapply(append_All … H) -H
     1337lapply(fresh_labs lbl) >EQlbl whd in ⊢ (% → ?); * #_ #H lapply(append_All … H) -H
    12451338* #_ whd in ⊢ (% → ?); *** #H #_ #_ @H -H @(code_is_in_universe … (pi2 ?? fn))
    12461339whd in match code_has_label; whd in match code_has_point; normalize nodelta
     
    12611354qed.
    12621355
     1356
    12631357lemma get_sigma_last :
    12641358∀prog : ertl_program.
     
    12661360 ∀f_bl_r.
    12671361 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    1268      translate_data prog f_bl_r f_lbls f_regs →
     1362     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
    12691363∀id,fn,bl,pt,stmt,pre,last.
    12701364fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 →
    12711365stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt → 
    1272 f_lbls bl pt = return (pre@[last]) → get_sigma prog f_lbls bl last = return pt.
     1366f_lbls bl pt = pre@[last] → get_sigma prog f_lbls bl last = return pt.
    12731367#prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #pre #last
    12741368#EQfn #EQstmt #EQlabels
    12751369cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
    12761370#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
    1277 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs
    1278 #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H * #lbls * #regs ** >EQlabels
    1279 whd in ⊢ (??%? → ?); #EQ destruct(EQ) #EQregs cases stmt in EQstmt; normalize nodelta
     1371[2: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs
     1372#_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H normalize nodelta
     1373cases stmt in EQstmt; normalize nodelta
    12801374[3: *
    12811375|2: * [#lbl || *] #EQstmt whd in ⊢ (%→ ?); * #bl *
    12821376|*: * [#c | * [ #c_id | #c_ptr] #args #dest | #r #lbl | #seq ] #nxt #EQstmt
    12831377    >if_merge_right [2,4,6,8,10: %] whd in ⊢ (% → ?); * #bl *
    1284 ] whd in ⊢ (% → ?); cases regs in EQregs; normalize nodelta
    1285 [2,4,6,8,9,12,14: [1,2,3,4,6,7: #x #y] #_ *|10: #r #tl] #EQregs
     1378]
     1379whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta
     1380[2,4,6,8,9,12,14: [1,2,3,4,6,7: #x #y #_] #_ *|10: #r #tl #_] #EQregs
    12861381[ whd in ⊢ (% → ?); cases tl in EQregs; normalize nodelta [2: #x #y #_ *] #EQregs]
    12871382#EQbl destruct(EQbl) whd in ⊢ (%→?); [2,3: * #pref * #mid **|*: * #l1 * #mid1 * #mid2 * #l2 ***]
    12881383#EQmid1 whd in ⊢ (% → ?);
    1289 [1,2,4,5,6,7: * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
     1384[1,2,4,5,6,7: * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)              
    12901385[3,4,5,6: whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt  #EQ destruct(EQ) ]
    1291 whd in ⊢ (% → ?); * [1,2,3,4: #e0] @⊥ @(append_absurd ??? e0)]
     1386whd in ⊢ (% → ?); * [1,2,3,4: #e0] @⊥ >EQlabels in e0; #e0 @(append_absurd ??? e0)]
    12921387* #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_
    12931388change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
     
    13041399>code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
    13051400inversion(find ????)
    1306 [ #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQlabels
     1401[ #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >e0
    13071402  normalize nodelta @eq_identifier_elim [ #_ *] * #H #_ @H
    1308   whd in EQmid1 : (??%%); destruct(EQmid1) @(last_append_eq ????? e1) ]
     1403  >(last_append_eq ????? EQlabels) % ]
    13091404* #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
    1310 inversion(f_lbls ??) [ #_ normalize nodelta *] #labels
    1311 @(list_elim_left … labels …) -labels normalize nodelta
    1312 [ #EQl @eq_identifier_elim [2: #_ *] #EQ lapply EQl destruct(EQ) #EQl
    1313   lapply(fresh_labs pt) >EQlabels <e0 whd in ⊢ (% → ?);
    1314   #H lapply(append_All … H) -H * #_ whd in ⊢ (% → ?); *** #H #_ #_ #_ @⊥ @H
    1315   @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
     1405inversion(f_lbls ??)
     1406[ #EQlbl normalize nodelta @eq_identifier_elim [2: #_ *] #EQ destruct(EQ)
     1407  lapply(last_append_eq ????? EQlabels) #EQ destruct(EQ) @⊥
     1408  lapply(fresh_labs pt) >e0 * #_ * #_ * #_ *** #H #_ #_ @H -H
     1409   @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
    13161410  whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
    13171411  >(find_lookup ?????? EQfind) @I
    1318 | #last1 #pre1 #_ #EQl >split_on_last_append normalize nodelta @eq_identifier_elim
    1319   [2: #_ *] #EQ lapply EQl destruct(EQ) #EQl #_ lapply pp_labs
    1320   whd in match partial_partition; normalize nodelta * #_ #H lapply(H lbl pt)
    1321   >EQl <e0 in EQlabels; #EQlabels >EQlabels whd in ⊢ (% → ?); -H #H
    1322   >(H last1 ? ?) [%] >(memb_append_l2 ? last1 ? [last1] ?) /2 by /
    1323 ]
    1324 qed.
     1412]
     1413#lb #labels #_  @(list_elim_left … (labels) …) -labels normalize nodelta
     1414[2: #last1 #pre #_] #EQl [ >(split_on_last_append … (lb::pre) last1) ]
     1415normalize nodelta @eq_identifier_elim [2,4: #_ *] #EQ destruct(EQ) #_
     1416lapply(last_append_eq ????? EQlabels) #EQ destruct(EQ)
     1417lapply pp_labs whd in match partial_partition; normalize nodelta * #_ #H
     1418lapply(H lbl pt) >e0 whd in EQmid : (??%%); >EQl
     1419#H [ >(H last1 ? ?) | >(H lb ? ?) ] [1,4: %
     1420               |6: whd in match (memb ???); @if_elim [#_ @I]
     1421                  #H lapply(Prop_notb ? H) * -H #H @⊥ @H cases lb #x normalize
     1422                  @if_elim [#_ %] #H lapply(Prop_notb ? H) * -H #H @H >(eqb_n_n x) %
     1423               |5: >(memb_append_l2 ? lb ? [lb] ?) /2 by /
     1424               |*: >(memb_append_l2 ? last1 ? [last1] ?) /2 by /
     1425                   @Exists_memb %2 elim pre [ % % | #hd #tl #IH %2 @IH]
     1426               ]
     1427qed.
     1428
    13251429
    13261430lemma fetch_call_commute :
     
    13301434 ∀f_bl_r.
    13311435 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    1332      translate_data prog f_bl_r f_lbls f_regs →
     1436     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
    13331437∀id,fn,c_id,c_args,c_dest,nxt,pc.
    13341438fetch_statement ERTL_semantics
     
    13431447cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
    13441448#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
    1345 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs
    1346 #_ #fresh_labs #_ #_ #_ #H cases(H … EQstmt) -H #labels * #registers
    1347 ** #EQlabels #EQregisters normalize nodelta >if_merge_right [2,4: %]
    1348 whd in match translate_step;
    1349 normalize nodelta whd in ⊢ (% → ?); * #bl * whd in ⊢ (% → ?);
    1350 cases registers in EQregisters; -registers normalize nodelta
    1351 [2,3: [ #x #y] #_ *|4: #r #tl] #EQregisters
    1352 [ whd in ⊢ (% → ?); cases tl in EQregisters; -tl [2: #x #y #_ *] normalize nodelta
    1353 #EQregisters] #EQ destruct(EQ) whd in ⊢ (% → ?); *
    1354 #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in ⊢ (% → ?);
    1355 [ * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?);
     1449[2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_
     1450#_ #_ #_ #_ #_ #H cases(H … EQstmt) -H #bl whd in ⊢ (% → ?); *
     1451>if_merge_right [2,4: %] whd in match translate_step;
     1452normalize nodelta whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta
     1453[|2,3:[ #x #y #_] #_ * |4: #r #tl #_ ] #EQregs
     1454[ | cases tl in EQregs; [2: #x #y #_ *] #EQregs whd in ⊢ (% → ?);] #EQ destruct(EQ)
     1455whd in ⊢ (% → ?); * #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in ⊢ (% → ?);
     1456[2: * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?);
    13561457  * #nxt1 * #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    13571458  whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ) * #nxt1 *
     
    13721473      [1,3: #EQbl >fetch_internal_function_no_minus_one in EQfn; try assumption
    13731474            #EQ destruct(EQ)] #_ normalize nodelta
    1374             [2: >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
     1475            [2: >(get_sigma_idempotent … good … EQfn EQstmt EQ)
    13751476            |*: change with (pc_block pc) in match (pc_block ?);
    1376                 >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
     1477                >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt e0)
    13771478            ] >m_return_bind normalize nodelta >pc_of_point_of_pc %
    13781479|*: whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind
     
    13871488∀ f_lbls,f_regs.∀f_bl_r.
    13881489b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    1389      translate_data prog f_bl_r f_lbls f_regs →
     1490     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
    13901491∀pc,lb.
    13911492next_of_call_pc ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog)
     
    16031704]
    16041705qed.
     1706
     1707
Note: See TracChangeset for help on using the changeset viewer.