Ignore:
Timestamp:
Jul 13, 2015, 5:38:01 PM (4 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/variable_stack_pass.ma

    r3579 r3581  
    427427#EQ destruct @expr_bound_good_expr /2 by le_maxl/
    428428qed.
    429 
    430 check frame_assign_var
    431429
    432430lemma var_to_shift_frame_assign_var_ok : ∀st,v,val,new_st.
     
    512510      @(var_instr_bond_seq_ok … Hstore2)
    513511    ]
    514     @append_silent [ % @create_silent_trace_from_eval_combinators_ok [7: % |*:] ]
    515     xxxx
    516    
    517  
    518   %{((create_silent_trace_from_eval_combinators …) @ (t_ind … (t_base …)))}
    519  
    520 
    521  whd in ⊢ (??%? → ?); #H cases(bind_inversion ????? H)
    522    
    523        
    524 qed.
     512    @append_silent [ % @create_silent_trace_from_eval_combinators_ok [7: % |*:] ]
     513      % %2 [ % #EQ normalize in EQ; destruct ] % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
     514    [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     515            #lin *] normalize nodelta #EQ destruct
     516  | %{(t_ind … (cost_act … (None ?)) … (t_base …))}
     517    [ whd applyS seq_sil try assumption try % [ <Hio1 @Hio2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct]
     518      change with (frame_assign_var ???) in ⊢ (??%?); <EQstore_12 assumption
     519    | % [ % [2: <EQcont @(var_instr_bond_seq_ok … (var_instr_bond_frame_assign_var_ok … Hstore2 … EQmem)) ]
     520          % [2: @(var_to_shift_frame_assign_var_ok … EQmem) assumption]
     521          % // % // % // % // ]
     522      % %2 [ % whd in ⊢ (??%?→ ?); >EQcode_s2 normalize nodelta #EQ destruct] %
     523      % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
     524    [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     525            #lin *] normalize nodelta #EQ destruct
     526   ]
     527 ]
     528| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 destruct
     529| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
     530| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
     531| #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 destruct
     532| #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
     533| #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 #H138 destruct
     534| #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 destruct
     535]
     536qed.
     537
     538lemma var_stack_simulate_label :
     539∀prog : Program frame_state_params frame_state_params frame_state_params.
     540∀bound : ℕ.
     541∀s1.∀s2.∀l.∀s1'.
     542execute_l … (frame_sem_state_params bound) (env … prog) (cost_act … (Some ? l)) s1 s1' →
     543lang_classify … s1 ≠ cl_io → lang_classify … s1' ≠ cl_io →
     544frame_variable_sem_rel s1 s2 →
     545∃s2',s2'',s2'''.
     546∃t1: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2 s2'.
     547execute_l … (stack_sem_state_params bound) (env … (trans_var_prog prog)) (cost_act … (Some ? l)) s2' s2'' ∧
     548∃t3: raw_trace … (operational_semantics … (stack_sem_state_params bound) (trans_var_prog prog)) s2'' s2'''.
     549frame_variable_sem_rel  s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3.
     550#prog #bound #s1 #s2 #lbl #s1' #H inversion H
     551[ #st1 #st1' * #lab #instr #tail #EQcode_st1 #EQcont_st1 #EQ1 #EQ2 destruct #EQstore #Hio1 #Hio2 #no_ret
     552  #EQ1 #EQ2 #EQ3 #EQ4 destruct #Hclass1 #Hclass2 ****** #EQstore_12 >EQcode_st1 whd in ⊢ (???% → ?);
     553  #EQcode_s2 >EQcont_st1 whd in ⊢ (???% → ?); #EQcont_s2 #Hio3 #_ #Hstore1 #Hstore2 %{s2}
     554  %{(mk_state … (trans_var_instr (code … st1')) (foldr … (λx,tail.〈\fst x,trans_var_instr (\snd x)〉::tail) [ ] (cont … st1'))
     555      (store … st1') false)}
     556  %{(mk_state … (trans_var_instr (code … st1')) (foldr … (λx,tail.〈\fst x,trans_var_instr (\snd x)〉::tail) [ ] (cont … st1'))
     557      (store … st1') false)} %{(t_base …)} 
     558 %
     559 [ whd applyS empty try assumption try % [ #_ whd %{lbl} % | <EQstore_12 % ] ]
     560 %{(t_base …)} %
     561 [ % [ % [ % [ /5 by refl, conj/ | <EQstore // ] | <EQstore @(var_instr_bond_for_empty … Hstore2) ] ]
     562 %2 % * ] % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
     563 [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     564           #lin *] normalize nodelta #EQ destruct
     565| #st1 #st1' * [ * #v #e | #v ] #instr #mem #opt_l #EQcode_st1
     566  [ change with (m_bind ?????) in ⊢ (??%? → ?);
     567    #H1 cases(bind_inversion ????? H1) #curr_env * (*inversion(store … st1) *
     568    [| #hd #tl] #fp #EQstore_st1 whd in ⊢ (??%% → ?); #EQ destruct*) #EQcurr_env  #H
     569    cases(bind_inversion ????? H) -H #sem_e * #EQsem_e
     570  | change with (frame_assign_var ???) in ⊢ (??%? → ?);
     571  ]
     572  #EQmem #EQ destruct #EQcont #EQ destruct #EQio_st1 #EQio_st1' #EQ1 #EQ2 #EQ3 #EQ4 destruct #Hclass1 #Hclass2 ******
     573  #EQstore_12 >EQcode_st1
     574  [change with (list_combinators_to_instructions ??) in ⊢ (???% → ?); | whd in ⊢ (???% → ?); ]
     575  #EQcode_s2 #EQcont_s2 #Hio1 #Hio2 #Hstore1 #Hstore2
     576  [ cases(eval_exp_ok … EQcurr_env … EQsem_e)
     577    [2,3: cases(bind_inversion ????? EQcurr_env) #c_env inversion(store … st1) *
     578        [2,4: #hd #tl] #fp #EQstore_st1 * whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct
     579        [ >EQstore_st1 in Hstore1; * // |  >EQstore_st1 in Hstore2; #H @(good_expr_for_var_instr_ok … H) % ] ]
     580    #new_st * >EQstore_12 #EQnew_st #EQpop
     581    %{(mk_state … ? (cont … s2) new_st false)}
     582    [2: %{(mk_state … (trans_var_instr (code … st1')) (cont … s2) (store … st1') false)}
     583        %{(mk_state … (trans_var_instr (code … st1')) (cont … s2) (store … st1') false)}
     584        %{(create_silent_trace_from_eval_combinators (trans_var_prog prog) bound s2
     585          (mk_state … ? (cont … s2) new_st false)
     586          (trans_expr e) EQnew_st …)} try assumption try %
     587         [1,2: <Hio1 @Hio2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     588         | whd @seq_sil [4,6,7,8,9,10: % |1,2,3:] whd in ⊢ (??%?); >EQpop normalize nodelta <EQstore_12 @EQmem
     589         ]
     590         %{(t_base …)} %
     591         [ % [ % [ % [ % // % // % // % //] @(var_to_shift_frame_assign_var_ok … EQmem) assumption ]
     592               @(var_instr_bond_frame_assign_var_ok … EQmem) <EQcont
     593               @(var_instr_bond_seq_ok … Hstore2)
     594             ] % @create_silent_trace_from_eval_combinators_ok [7: % |*:] ]
     595         % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
     596    [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     597            #lin *] normalize nodelta #EQ destruct
     598   |]
     599 | %{s2} %{(mk_state … (trans_var_instr (code … st1')) (cont … s2) (store … st1') false)}
     600   %{(mk_state … (trans_var_instr (code … st1')) (cont … s2) (store … st1') false)} %{(t_base …)}
     601   %
     602   [ whd @seq_sil try assumption [3,4,5,7: % |6: <Hio1 @Hio2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     603      |2: change with (frame_assign_var ???) in ⊢ (??%?); <EQstore_12 assumption |] ]
     604   %{(t_base …)} % [ %
     605    [ % [2: <EQcont @(var_instr_bond_seq_ok … (var_instr_bond_frame_assign_var_ok … Hstore2 … EQmem)) ]
     606          % [2: @(var_to_shift_frame_assign_var_ok … EQmem) assumption]
     607          % // % // % // % // ]
     608    %2 % *]
     609    % % whd in ⊢ (??%? → ?); cases(trans_var_instr ?)
     610    [| #rt | #seq #opt_l #i | #cond #ltrue #i_true #lfalse #i_false #i | #cond #ltrue #i_true #lfalse #i | #f #act #opt_l #i |
     611            #lin *] normalize nodelta #EQ destruct
     612   ]
     613|*: cases daemon (*todo*)
     614]
     615qed.
     616 
     617
    525618
    526619definition simulation_imp_frame :
Note: See TracChangeset for help on using the changeset viewer.