Changeset 3549 for LTS/Lang_meas.ma


Ignore:
Timestamp:
Apr 2, 2015, 3:44:19 PM (5 years ago)
Author:
piccolo
Message:

added paolo's trick

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Lang_meas.ma

    r3542 r3549  
    1313(**************************************************************************)
    1414
    15 include "Language.ma".
     15include "Lang_corr.ma".
    1616
    1717
     
    2121∀s1,s2,s1' : state p.∀abs_top,abs_tail.
    2222execute_l … p' (env … prog) l s1 s2 →
    23 is_costlabelled_act l →
    24 (is_call_act l → is_call_post_label (operational_semantics p p' prog) … s1) →
     23is_costlabelled_act p l →
     24(is_call_act p l → is_call_post_label p (operational_semantics p p' prog) … s1) →
    2525state_rel … m keep abs_top abs_tail s1 s1' → abs_top = nil ? ∧
    26 (is_call_act l → is_call_post_label (operational_semantics p p' t_prog) … s1').
     26(is_call_act p l → is_call_post_label p (operational_semantics p p' t_prog) … s1').
    2727#p #p' #prog @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
    2828#l #s1 #s2 #s1' #abs_top #abs_tail #H elim H -s1 -s2 -l
     
    3333  >EQcont in EQcheck; whd in ⊢ (??%? → ?); inversion(cont … s1') normalize nodelta
    3434  [ #_ #EQ destruct] * #lab' #code_cont' #stack' #_ #EQcont'
    35     change with (check_continuations ?????) in match (foldr2 ???????);
     35    change with (check_continuations ??????) in match (foldr2 ???????);
    3636    inversion(check_continuations ?????) [ #_ normalize #EQ destruct]
    3737    ** #H2 #a_top1 #a_tail1 #EQcheck >m_return_bind normalize nodelta
     
    134134  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
    135135  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #EQ destruct % // * #f * #c #EQ destruct
    136 | cases daemon
     136| #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #instrs #new_m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct
     137  #Hio1 #Hio2 * #_ whd in match state_rel; normalize nodelta inversion(check_continuations ?????) normalize nodelta
     138  [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1  inversion(code ? s1')
     139  [1,2,3,5,6,7:
     140    [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_
     141       | #lin #io #lout #instr #_ ]
     142          #_ whd in ⊢ (??%% → ?);
     143          [ |
     144          | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]]
     145          | cases(call_post_clean ?????) normalize nodelta
     146            [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta
     147               [| #y cases(?∧?) normalize nodelta
     148               ]
     149            ]
     150          | cases(call_post_clean ?????) normalize nodelta
     151             [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta
     152                [ cases (?==?) normalize nodelta ]
     153             ]]
     154          | cases(call_post_clean ?????) normalize nodelta
     155             [| #x cases(? ∧ ?) normalize nodelta ]
     156          ]
     157          whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     158  ]
     159  #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?);
     160  inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr'
     161  whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2
     162  #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] *
     163  #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta
     164  whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ #_ #EQ destruct % // * #f * #c #EQ destruct
    137165| cases daemon
    138166| cases daemon
     
    156184      cases(?==?) normalize nodelta
    157185    [2:  #EQ destruct] whd in ⊢ (??%% → ?); #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct #_#_ #EQ1 destruct % //
    158     #_ whd in match (is_call_post_label ??); >EQcode_s1' %
     186    #_ whd in match (is_call_post_label ???); >EQcode_s1' %
    159187    ]
    160188    #ABS whd in ⊢ (??%% → ?);  #EQ1 lapply(eq_to_jmeq ??? EQ1) -EQ1 #EQ1 destruct lapply(Hcall ?) [ %{f} %{(f_lab … env_it)} %]
    161     whd in ⊢ (% → ?); whd in match (is_call_post_label ??); normalize nodelta >EQcode *
     189    whd in ⊢ (% → ?); whd in match (is_call_post_label ???); normalize nodelta >EQcode *
    162190 ]
    163191| #s1 #s2 #r_t #mem #stack * [|#lbl] #i #EQcode #EQcont #EQ destruct #_ #_ #EQeval #EQ1 #EQ2 destruct * #_
     
    168196    >EQcont in EQcheck; inversion (cont ? s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
    169197    * #LAB #instrs #stack' #_ #EQcont_s1' whd in match check_continuations; normalize nodelta
    170     whd in match (foldr2 ???????); change with (check_continuations ?????) in match (foldr2 ???????);
     198    whd in match (foldr2 ???????); change with (check_continuations ??????) in match (foldr2 ???????);
    171199    cases(check_continuations ?????) normalize nodelta [#EQ destruct] ** #H2 #a_top1 #a_tail1
    172200    normalize nodelta   whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta [ #EQ destruct cases HH1]
     
    196224let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
    197225∀s1,s2,s1' : state p.∀abs_top,abs_tail.
    198 ∀l.is_costlabelled_act l →
     226∀l.is_costlabelled_act p l →
    199227∀prf :execute_l p p' (env … prog) l s1 s2.
    200228state_rel … m keep abs_top abs_tail s1 s1' →
     
    202230execute_l p p' (env … t_prog) l s1' s2' ∧
    203231state_rel  … m keep abs_top' abs_tail s2 s2' ∧
    204 map_labels_on_trace … m … (actionlabel_to_costlabel l) =
    205 actionlabel_to_costlabel l @ abs_top'.
     232map_labels_on_trace … m … (actionlabel_to_costlabel p l) =
     233actionlabel_to_costlabel p l @ abs_top'.
    206234#p #p' #prog  #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
    207235#s1 #s2 #s1' #abs_top #abs_tail #l #Hl #H lapply Hl -Hl elim H -s1 -s2 -l
     
    209237  #Hlbl #cost_lbl whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????)
    210238  normalize nodelta [ #_ *] ** #H1 #a_top #a_tail >EQcont_s1 inversion(cont … s1') [ #_ whd in ⊢ (??%% → ?); #EQ destruct]
    211   * #lbl' #i' #stack' #_ #EQcont_s1' whd in ⊢ (??%% → ?); change with (check_continuations ?????) in match (foldr2 ???????);
     239  * #lbl' #i' #stack' #_ #EQcont_s1' whd in ⊢ (??%% → ?); change with (check_continuations ??????) in match (foldr2 ???????);
    212240  inversion(check_continuations ?????) normalize nodelta [ #_ #EQ destruct] ** #H2 #a_top1 #a_tail1 #EQcheck
    213241  normalize nodelta inversion(call_post_clean ?????) normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct ***** ]
     
    247275  * #genlab #cleaned #EQcleaned inversion(?∧?) normalize nodelta #EQget whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ
    248276  #EQ destruct #EQstore_s1_s1' #EQioinfo #EQ destruct %{[]}
    249   %{(mk_state … (EMPTY …) (〈cost_act (Some ? lout),i'〉::(cont … s1')) (store … s2) true)} % [%
     277  %{(mk_state … (EMPTY …) (〈cost_act p (Some ? lout),i'〉::(cont … s1')) (store … s2) true)} % [%
    250278  [ @(io_in … EQcode_s1') // ]
    251   whd >EQcont_s2 whd in match (check_continuations ?????); change with (check_continuations ?????) in match (foldr2 ???????);
     279  whd >EQcont_s2 whd in match (check_continuations ??????); change with (check_continuations ??????) in match (foldr2 ???????);
    252280  >EQcheck normalize nodelta >EQcleaned normalize nodelta % // % // % // % [2: >EQcode_s2 %] %
    253281  [2: cases(andb_Prop_true … (bool_true … EQget)) #H #_ >(\P (bool_true … H)) % ] % // % //]
     
    265293let 〈t_prog,m,keep〉 ≝ trans_prog … prog in
    266294∀si,s1,s2,sn,si' : state p.∀abs_top,abs_tail.
    267 ∀t : raw_trace (operational_semantics … p' prog) si sn.
    268 measurable (operational_semantics … p' prog) … s1 s2 … t →
     295∀t : raw_trace p (operational_semantics … p' prog) si sn.
     296measurable p (operational_semantics p p' prog) … s1 s2 … t →
    269297state_rel … m keep abs_top abs_tail si si' →
    270 ∃abs_top',abs_tail'.∃sn'.∃t' : raw_trace (operational_semantics … p' t_prog) si' sn'.
     298∃abs_top',abs_tail'.∃sn'.∃t' : raw_trace p (operational_semantics … p' t_prog) si' sn'.
    271299state_rel  … m keep abs_top' abs_tail' sn sn' ∧
    272 is_permutation ? (map_labels_on_trace m (chop … (get_costlabels_of_trace … t))) 
     300is_permutation ? (map_labels_on_trace m (chop … (get_costlabels_of_trace … t))) 
    273301                  (chop … (get_costlabels_of_trace … t')) ∧
    274302                  ∃s1',s2'.
    275 measurable (operational_semantics … p' t_prog)  … s1' s2' … t'.
     303measurable p (operational_semantics … p' t_prog)  … s1' s2' … t'.
    276304#p #p' #prog #no_dup @pair_elim * #t_prog #m #keep #EQt_prog normalize nodelta
    277305#si #s1 #s3 #sn #si' #abs_top #abs_tail #t *  #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2
     
    300328  >append_nil cases(actionlabel_ok … Hl2) #c2 #EQc2 >EQc2 <associative_append <associative_append
    301329  <associative_append >chop_append_singleton <associative_append <associative_append >chop_append_singleton
    302   >append_nil whd in match (get_costlabels_of_trace ??? (t_ind (operational_semantics p p' t_prog) … prf1' (t_base …)));
     330  >append_nil whd in match (get_costlabels_of_trace ???? (t_ind ? (operational_semantics p p' t_prog) … prf1' (t_base …)));
    303331  >append_nil >map_labels_on_trace_append >EQmap_l1 >associative_append @is_permutation_append_left_cancellable
    304332  lapply(top_move_source_is_empty … p' prog) >EQt_prog normalize nodelta #H
Note: See TracChangeset for help on using the changeset viewer.