Changeset 3394 for LTS


Ignore:
Timestamp:
Oct 30, 2013, 10:29:47 AM (6 years ago)
Author:
piccolo
Message:

Added abstract language and procedure to add call post labelled

Location:
LTS
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3391 r3394  
    1111
    1212record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝
    13  { simulate_tau:
     13 { initial_is_initial :
     14   ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2))
     15 ; final_is_final :
     16   ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))
     17 ; simulate_tau:
    1418     ∀s1,s2,s1' : S.
    1519      as_execute … (cost_act (None ?))  s1 s1'→
     
    2630       as_execute … (cost_act (Some ? l)) s2' s2'' ∧
    2731       ∃t3: raw_trace S s2'' s2'''.
    28         Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     32        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    2933 ; simulate_call_pl:
    3034     ∀s1,s2,s1' : S.∀f,l.
     
    3842       bool_to_Prop(is_call_post_label … s2') ∧
    3943       ∃t3: raw_trace S s2'' s2'''.
    40         Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     44        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    4145 ; simulate_ret_l:
    4246     ∀s1,s2,s1' : S.∀l.
     
    4852       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
    4953       ∃t3: raw_trace S s2'' s2'''.
    50         Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     54        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    5155 ; simulate_call_n:
    5256     ∀s1,s2,s1' : S.∀f,l.
     
    6064       as_execute … (call_act f l) s2' s2'' ∧
    6165       ∃t3: raw_trace S s2'' s2'''.
    62         Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     66        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
    6367        ∧ Crel … rel s1 s2'
    6468 ; simulate_ret_n:
     
    7175       as_execute … (ret_act (None ?)) s2' s2''  ∧
    7276       ∃t3: raw_trace S s2'' s2'''.
    73         Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     77        Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3
    7478        ∧ Rrel … rel s1' s2''
     79 ; simulate_io_in :
     80   ∀s1,s2,s1' : S.∀l.
     81   as_execute … (cost_act … (Some ? l)) s1 s1' →
     82   as_classify … s1 ≠ cl_io → as_classify … s1' = cl_io →
     83   Srel … rel s1 s2 →
     84   ∃s2',s2'' : S.∃t: raw_trace … s2 s2'.
     85   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2' s2'' ∧
     86   as_classify … s2'' = cl_io ∧ Srel … rel s1' s2''
     87; simulate_io_out :
     88  ∀s1,s2,s1' : S.∀l.
     89   as_execute … (cost_act … (Some ? l)) s1 s1' →
     90   as_classify … s1 = cl_io → as_classify … s1' ≠ cl_io →
     91   Srel … rel s1 s2 →
     92   ∃s2',s2'' : S.∃t : raw_trace … s2' s2''.
     93   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2 s2' ∧
     94   as_classify … s2 = cl_io ∧ Srel … rel s1' s2''
    7595 }.
    7696
     
    102122#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
    103123[ #st #t #Hpre #_ whd in ⊢ (????%); assumption]
    104 #s1 #s2 #s3 #l #prf #tl #IH #t #Hpre #H inversion H in ⊢ ?;
     124#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?;
    105125[ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
    106126#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
     
    110130| @IH try assumption
    111131]
    112 qed.
    113 
    114 lemma silent_is_premeasurable : ∀S : abstract_status.
    115 ∀st1,st2 : S. ∀t : raw_trace S st1 st2.silent_trace … t
     132% assumption
     133qed.
     134
     135lemma pre_silent_is_premeasurable : ∀S : abstract_status.
     136∀st1,st2 : S. ∀t : raw_trace S st1 st2.pre_silent_trace … t
    116137→ pre_measurable_trace … t.
    117138#S #st1 #st2 #t elim t
     
    134155pre_measurable_trace … (t' @ t).
    135156#S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
    136 [ normalize #st #Hst #r #H1 @silent_is_premeasurable assumption
     157[ #st #Hst #r * [ #H1 @pre_silent_is_premeasurable assumption ]
     158  inversion r [2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 cases H11
     159  #ABS @⊥ @ABS % ] #s' #EQ1 #EQ2 #EQ3 destruct #_
     160  %1 assumption
    137161|2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct
    138162  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ]
     
    205229get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
    206230#S #st1 #st2 #st3 #t1 elim t1
    207 [#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 #H
    208 inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
     231[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 *
     232[2: whd in match is_trace_non_empty; normalize nodelta * #ABS @⊥ @ABS %]
     233#H inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
    209234#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
    210 #_ whd in ⊢ (??%?); >IH [%] assumption
    211 qed.
     235#_ whd in ⊢ (??%?); >IH [%] %1 assumption
     236qed. 
    212237
    213238lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.
     
    251276#S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
    252277[ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
    253   /8 by refl, silent_empty, conj, silent_is_premeasurable/
     278  /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/
    254279| #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
    255280  #pre_measurable_tl #IH #s2 #classify_s2 #REL
    256281  [ cases(simulate_tau … good … execute … REL) /2/ #s2'' * #t_s2'' * #RELst2s2''
    257     #silent_ts2'' cases(IH … RELst2s2'') /2 by silent_io/
     282    #silent_ts2'' cases(IH … RELst2s2'')
     283    [2: cases silent_ts2'' /2 by pre_silent_io/ inversion t_s2''
     284        [ #x #EQ1 #EQ2 #EQ3 destruct // ]
     285        #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct * #ABS @⊥ @ABS % ]
    258286    #s3 * #ts3 ** #pre_meas_ts3 #EQcost #RELst3s3
    259287    %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % /2 by append_premeasurable_silent/
     
    262290    [2,3: /2/]
    263291    #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2''''
    264     #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''') /2 by silent_io/
     292    #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''')  /2 by pre_silent_io/
    265293    #s3 * #t_s3 ** #pre_s3 #EQcost #RElst3s3 %{s3}
    266294    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
    267295    %
    268     [ /4 by pm_cons_cost_act, silent_io, ex_intro, append_premeasurable_silent/
     296    [ @append_premeasurable_silent // %2 /2 by ex_intro/
     297       [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2''
     298         [ #H31 #H32 #H33 #H34 #H35 destruct assumption ]
     299         #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
     300         cases H47 #ABS @⊥ @ABS % ]
     301       @append_premeasurable_silent // % //
    269302    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
    270303      [2: assumption] whd in ⊢ (???%);
     
    272305    ]
    273306  ]
     307  % assumption
    274308| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
    275309  #pre_meas_tl #IH #s2 #class_s2 #RELst1s2
     
    277311  #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2'''
    278312  #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
    279   [2: @(silent_io … sil_t2) assumption]
     313  [2: @(pre_silent_io … sil_t2) assumption]
    280314  #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL
    281315  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
     
    283317        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
    284318        whd in ⊢ (???%);
    285         >(get_cost_label_invariant_for_append_silent_trace_l … sil_t2)
     319        >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2))
    286320        @eq_f assumption ]
    287   /4 by pm_cons_lab_ret, silent_io, ex_intro, append_premeasurable_silent/
     321  @append_premeasurable_silent [2: //] %3
     322  [2,3: /3 by append_premeasurable_silent, ex_intro, or_introl/ ]
     323  cases sil_t1 [ /2 by pre_silent_io/ ] inversion t1
     324  [ #H49 #H50 #H51 #H52 #H53 destruct //]
     325  #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65
     326  #ABS @⊥ @ABS %
    288327| #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
    289328  #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
     
    292331   #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
    293332   cases(IH  … REL)
    294    [2: /2 by silent_io/ ]
     333   [2: /2 by pre_silent_io/ ]
    295334   #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL1 %{s2_fin}
    296335   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
     
    298337        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
    299338        whd in ⊢ (???%);
    300         >(get_cost_label_invariant_for_append_silent_trace_l … sil_t2)
     339        >(get_cost_label_invariant_for_append_silent_trace_l …  (or_introl … sil_t2))
    301340        @eq_f assumption ]
    302341   @append_premeasurable_silent try assumption
    303342     %4 try assumption
    304      [ /2 by silent_io/
     343     [ cases sil_t1 [/2 by pre_silent_io/ ] inversion t1 [#H67 #H68 #H69 #H70 #H71 destruct //]
     344       #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 destruct cases H83
     345       #ABS @⊥ @ABS %
    305346     | whd %{f} %{lab} %
    306      | /2 by append_premeasurable_silent/
     347     | @append_premeasurable_silent // % assumption
    307348     ]
    308349| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
     
    311352  #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1
    312353  #sil_tr2 #call_rel cases(IH1 … REL1)
    313   [2: /2 by silent_io/ ]
     354  [2: /2 by pre_silent_io/ ]
    314355  #st3' * #tr3 ** #pre_tr3 #EQcost_tr3 #REL2
    315356  cases(simulate_ret_n … good … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
    316357  #st3'' * #st4' * #st4'' *
    317   #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by silent_io/ ]
     358  #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ]
    318359  #st5' * #tr6 ** #pre_tr6 #EQcost_tr6 #REL4 %{st5'}
    319360  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
    320361  % [2: assumption] %
    321362  [ @append_premeasurable_silent try assumption %5
    322        [1,2: /2 by silent_io/
     363       [1,2: /2 by pre_silent_io/
     364             cases sil_tr1 /2 by pre_silent_io/ inversion tr1
     365             [ #H85 #H86 #H87 #H88 #H89 destruct // ]
     366             #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct
     367             cases H107 #ABS @⊥ @ABS %
    323368       | whd %{f} %{l} %
    324369       | assumption
    325        | @append_premeasurable_silent try assumption
    326          @append_silent_premeasurable assumption
     370       | @append_premeasurable_silent try assumption [2: % //]
     371         @append_silent_premeasurable // % //
    327372       | @append_premeasurable_silent try assumption
    328373       | @(RET_REL … call_rel) assumption
     
    332377    whd in ⊢ (??%%); @eq_f >append_associative
    333378    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
    334     [2: // ] >append_associative
     379    [2: % // ] >append_associative
    335380    >get_cost_label_append in ⊢ (???%);
    336381    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
    337     [2: //] normalize
     382    [2: % //] normalize
    338383    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
    339     [2: // ] >get_cost_label_append in ⊢ (??%?); @eq_f2
     384    [2: % // ] >get_cost_label_append in ⊢ (??%?); @eq_f2
    340385    assumption
    341386  ]
     387  % //
    342388]
    343389qed.
    344 
    345 sxxxxx
    346390
    347391
     
    358402  as_execute … s2 so L'. *)
    359403
    360 record LR_raw_trace (S : abstract_status) : Type[0] ≝
     404record measurable_trace (S : abstract_status) : Type[0] ≝
    361405 { L_label: ActionLabel
    362  ; R_label : ActionLabel
    363  ; LR_s1: S
    364  ; LR_s2: S
    365  ; LR_t : raw_trace S LR_s1 LR_s2
    366  ; L_init_ok : bool_to_Prop(as_initial … LR_s1) → L_label = init_act
    367  ; L_noinit_ok :
    368       bool_to_Prop (¬ as_initial … LR_s1) →
    369         ∃s0. as_execute … L_label s0 LR_s1 ∧ is_costlabelled_act L_label
    370         ∧ ¬ bool_to_Prop (is_act_io_entering S L_label)
    371  ; R_nonfin_ok :
    372     bool_to_Prop (¬ as_final … (LR_s2)) →
    373       ∃so.as_execute … R_label LR_s2 so ∧ is_costlabelled_act R_label
    374           ∧ ¬ bool_to_Prop (is_act_io_exiting S R_label)
    375  }.
     406 ; R_label : option ActionLabel
     407 ; L_pre_state : option S
     408 ; L_s1 : S
     409 ; R_s2: S
     410 ; R_post_state : option S
     411 ; trace : raw_trace S L_s1 R_s2
     412 ; pre_meas : pre_measurable_trace … trace
     413 ; L_init_ok : match L_pre_state with
     414               [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = init_act
     415               | Some s ⇒ is_costlabelled_act L_label ∧
     416                          as_execute … L_label s L_s1
     417               ]
     418 ; R_fin_ok : match R_label with
     419               [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ?
     420               | Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧
     421                          (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
     422                          ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s'
     423               ]
     424}.
     425
     426lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s.
     427#P #H1 #H2 * // @H2 % #EQ destruct qed.
     428
     429lemma case_cl_io : ∀s : status_class.decidable … (s = cl_io).
     430* [2: %%] %2 % #EQ destruct qed.
     431
     432lemma tail_of_premeasurable_is_not_io : ∀S : abstract_status.
     433∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
     434as_classify … st2 ≠ cl_io.
     435#S #st1 #st2 #t #H elim H //
     436qed.
     437
     438lemma get_cost_label_silent_is_empty : ∀S : abstract_status.
     439∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
     440#S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
     441#H inversion H
     442[#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
     443destruct #_ @IH % assumption
     444qed.
     445
     446lemma get_cost_label_invariant_for_append_silent_trace_r :∀S : abstract_status.
     447∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
     448silent_trace … t2 →
     449get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t1.
     450#S #st1 #st2 #st3 #t1 #t2 #H >get_cost_label_append
     451>(get_cost_label_silent_is_empty … H) //
     452qed.
     453
     454lemma instr_execute_commute : ∀S :abstract_status.
     455∀rel : relations S.
     456simulation_conditions … rel →
     457∀s1,s1': S.∀l.l ≠ init_act → l ≠ cost_act (None ?) →  as_execute S l s1 s1' →
     458(as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
     459∀s2.
     460Srel … rel s1 s2 →
     461∃s2' : S.∃tr : raw_trace S s2 s2'.silent_trace … tr ∧
     462∃s2'' : S.as_execute S l s2' s2'' ∧ ∃s2''' : S.
     463∃tr' : raw_trace S s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧
     464(is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
     465(as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
     466#S #rel #good #s1 #s1' #l #l_noinit #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
     467[ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
     468  cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
     469  cases(simulate_io_out … good … prf … EQs1_io Hio_s1' … REL)
     470  #s2' * #s2'' * #t *** #sil_t #prf' #class_io #REL'
     471  %{s2} %{(t_base …)} % [ %2 % * ] %{s2'} % // %{s2''} %{t} % 
     472  [2: #_ @(head_of_premeasurable_is_not_io … t) @pre_silent_is_premeasurable
     473     assumption ] % [  %//  % // ] * #f * #l #EQ destruct
     474| #Hclass_s1 cases(case_cl_io … (as_classify … s1'))
     475  [ #EQs1' cases(io_entering … EQs1' … prf) #l1 #EQ destruct(EQ)
     476    cases(simulate_io_in … good … prf … Hclass_s1 EQs1' …  REL) #s2' * #s2'' * #t
     477    *** #sil_t #exe #Hclass_s2'' #REL'  %{s2'} %{t} %{(or_introl … sil_t)} %{s2''}
     478    %{exe} %{s2''} %{(t_base …)} % [2: >EQs1' * #H @⊥ @H % ] %
     479     [ /4 by or_intror, conj, nmk/] * #f * #l #EQ destruct
     480  | #Hclass_s1' cases l in prf l_noinit l_notau;
     481    [ #f #l #prf #_ #_ inversion(is_call_post_label … s1)
     482      [ #Hpost cases(simulate_call_pl … good … prf … REL)
     483        [2: >Hpost % |3,4: assumption]
     484        #s2' * #s2'' * #s2''' * #t1 ** #exe #Hpost' * #t3 * * #REL #sil_t1 #sil_t3
     485        %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
     486        [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
     487        % [ /4 by or_introl, conj/ ] /3 by /
     488     | #Hpost cases(simulate_call_n … good … prf … REL)
     489       [2: >Hpost % |3,4: // ] #s2' * #s2'' * #s2''' * #t1 ** #Hpost' #exe * #t3
     490       *** #REL' #sil_t1 #sil_t3 #_ %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''}
     491       %{t3} % [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
     492       % [2: #_ *] % //
     493     ]
     494   | *
     495     [ #prf #_ #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
     496       * #s2''' * #t1 * #exe * #t3 *** #REL' #sil_t1 #sil_t3 #_ %{s2'}
     497       %{t1} %{(or_introl … sil_t1)} %{s2''} %{exe} %{s2'''} %{t3} %
     498       [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
     499       % [ % // % // ] * #f * #l #EQ destruct
     500     | #l #prf #_ #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
     501       #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3
     502       %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
     503       [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
     504       % [ % // % //] * #f * #l #EQ destruct
     505    ]
     506  | * [ #_ #_ * #H @⊥ @H % ] #lab #prf #_ #_
     507    cases(simulate_label … prf … REL) [2,3,4: // ] #s2' * #s2'' * #s2''' * #t1
     508    * #exe * #t3 ** #REL' #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe}
     509    %{s2'''} %{t3} %
     510    [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
     511    % [% // % //] * #f * #l #EQ destruct
     512  | #_ * #H @⊥ @H %
     513  ]
     514  % //
     515]
     516qed.
     517
     518
     519theorem simulate_LR_trace :
     520∀S : abstract_status.
     521∀t : measurable_trace S.
     522∀rel : relations S.
     523simulation_conditions … rel →
     524∀s2 : S.
     525match L_pre_state … t with
     526[ None ⇒
     527   as_classify … s2 ≠ cl_io ∧
     528   Srel … rel (L_s1 … t) s2 
     529| Some s1 ⇒ Srel … rel s1 s2 ] →
     530∃t' : measurable_trace S.
     531 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
     532 get_costlabels_of_trace … (trace … t) =
     533  get_costlabels_of_trace … (trace … t') ∧
     534match L_pre_state … t with
     535[ None ⇒ L_s1 … t' = s2
     536| Some s1 ⇒
     537         ∃ pre_state : S.
     538         L_pre_state … t' = Some ? pre_state ∧
     539         ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i
     540] ∧
     541match R_post_state … t with         
     542[ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
     543| Some s1' ⇒
     544          ∃s2' : S. Srel … rel s1' s2' ∧
     545          ∃ post_state : S.
     546          R_post_state … t' = Some ? post_state ∧
     547          ∃tr : raw_trace S post_state s2'. silent_trace … tr
     548].
     549#S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ]
     550[2: #REL_pre
     551    cut
     552     (∃pre_state: S.
     553      ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ∧
     554      ∃middle_state: S.
     555       as_execute … (L_label … t) pre_state middle_state ∧
     556      ∃final_state: S.
     557      ∃tr_i2: raw_trace S middle_state final_state. silent_trace … tr_i2 ∧
     558       as_classify … final_state ≠ cl_io ∧
     559       Srel … rel (L_s1 … t) final_state)
     560    [ lapply(L_init_ok … t) >EQpre normalize nodelta * #Hcost #exe   
     561      cases(instr_execute_commute … good … (L_label … t) … exe … REL_pre)
     562      [2,3: % #EQ >EQ in Hcost; * |4: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
     563      #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' #Hcall
     564      #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} % // % //
     565      cases sil_t3 [/2 by pre_silent_io/ ] inversion t3
     566      [ #H109 #H110 #H111 #H112 #H113 destruct @Hclass @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
     567      #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 cases H125
     568      #H @⊥ @H %]
     569    * #pre_state * #tr_i * #silent_i * #middle_state * #step_pre_middle
     570    * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
     571| #REL
     572  cut(bool_to_Prop (as_initial S s2)∧L_label S t=init_act)
     573      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //]
     574        @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
     575]
     576cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) //
     577#fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t)
     578[2,4: #post_s2] #EQpost normalize nodelta
     579[3,4: cut (match R_label S t in option return λ_:(option ActionLabel).Prop with 
     580 [None⇒bool_to_Prop (as_final S fin_s2)∧None S=None S
     581 |Some (l:ActionLabel)⇒
     582  (is_costlabelled_act l∨is_unlabelled_ret_act l)
     583  ∧(is_call_act l→is_call_post_label S fin_s2)
     584  ∧(∃s':S.None S=Some S s'∧as_execute S l fin_s2 s')])
     585  [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta
     586      [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption
     587      |*: #a ** #_ #_ * #x * >EQpost #EQ destruct
     588      ]
     589  ] #R_label_fin
     590|*: cut(∃l.(R_label … t) = Some ? l)
     591    [1,3:  lapply(R_fin_ok … t) cases(R_label… t) normalize nodelta [1,3: >EQpost * #_ #EQ destruct]
     592          #a #_ %{a} % ] * #final_label #EQfinal_label
     593     cut
     594      (∃middle_state: S.
     595       ∃tr : raw_trace S fin_s2 middle_state. silent_trace … tr ∧
     596       ∃post_state : S.
     597       as_execute … final_label middle_state post_state ∧
     598       (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧
     599       ∃final_state: S.
     600       ∃tr_f2: raw_trace S post_state final_state. silent_trace … tr_f2 ∧
     601       Srel … rel post_s2 final_state)
     602     [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin
     603         * >EQpost #EQ destruct #exe
     604          cases(instr_execute_commute … good … final_label … exe … REL')
     605          [2,3,6,7: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct]
     606          |4,8: %1 @tail_of_premeasurable_is_not_io //
     607          ]
     608          #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL'
     609          #Hcall #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} % [2,4: %{s2'''} %{t3} % //]
     610          % // #H @Hcall // @H2 // ] * #middle_state' * #tr' * #sil_tr' * #post_state' ** #exe'
     611     #Hcall * #final_state' * #tr_f2 * #sil_tr_f2 #fin_rel
     612]
     613[2: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (None ?) … pre_meas_t' …)}
     614     normalize nodelta /5 by conj/
     615|3: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (Some ? post_state') … (tr_i2 @ t' @ tr') …)}
     616    normalize nodelta [2: % // lapply(L_init_ok … t) >EQpre normalize nodelta * //
     617    |3: /3 by append_silent_premeasurable, append_premeasurable_silent/
     618    |4: % [2: %{final_state'} /5 by ex_intro, conj/ ] % /8 by ex_intro, conj/ % [ /3 by conj/]
     619        >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???%); [2: //]
     620        >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???(???%)));
     621        /2 by refl, pair_destruct_1/
     622    | lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_
     623      % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] //
     624    ]
     625| %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (None ?) … (tr_i2 @ t') …)}
     626  normalize nodelta
     627  [ assumption
     628  | % // lapply(L_init_ok … t) >EQpre normalize nodelta * //
     629  | /4 by append_premeasurable_silent/
     630  | % // % [2: %{pre_state} /3/ ] % [ /2/] >get_cost_label_append
     631    >get_cost_label_silent_is_empty in ⊢ (???%); [2: //] /2 by refl, pair_destruct_1/
     632  ]
     633| %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (Some ? post_state') … (t' @ tr') …)}
     634  normalize nodelta
     635 [ lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_
     636      % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] //
     637 | /2/
     638 | /3 by append_silent_premeasurable/
     639 | % [2: %{final_state'} /5 by ex_intro, conj/
     640 | % [2: % ] % [ /2/] >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???%));
     641   // ]
     642 ]   
     643]
     644qed.   
     645(*
     646xxxxxxxxxxxxxxxxxxxx
    376647 
    377 definition measurable ≝ λS : abstract_status.λt : LR_raw_trace S.
    378 pre_measurable_trace … (LR_t … t) ∧ well_formed_trace … (LR_t … t).
     648theorem simulate_LR_trace :
     649∀S : abstract_status.
     650∀t : measurable_trace S.
     651∀rel : relations S.
     652simulation_conditions … rel →
     653∀s2 : S.
     654match L_pre_state … t with
     655[ None ⇒ as_classify … s2 ≠ cl_io → Srel … rel (L_s1 … t) s2 → 
     656         ∃t' : measurable_trace S.L_s1 … t' = s2 ∧
     657         L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
     658         get_costlabels_of_trace … (trace … t) =
     659                      get_costlabels_of_trace … (trace … t') ∧
     660         match R_post_state … t with
     661         [ None ⇒  Srel … rel (R_s2 … t) (R_s2 … t')
     662         | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?).
     663                      ∃post_state : S.
     664                      ∃tr : raw_trace S (opt_safe … prf) post_state.
     665                      silent_trace … tr ∧ Srel … rel s2' post_state
     666         ]
     667| Some s1 ⇒ Srel … rel s1 s2 →
     668            ∃ pre_state : S.∃tr_i : raw_trace S s2 pre_state.
     669            silent_trace … tr_i ∧
     670            ∃t' : measurable_trace S.L_pre_state … t' = Some ? pre_state ∧
     671            L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
     672            get_costlabels_of_trace … (trace … t) =
     673                      get_costlabels_of_trace … (trace … t') ∧
     674            match R_post_state … t with         
     675            [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
     676            | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?).
     677                         ∃post_state : S.
     678                         ∃tr : raw_trace S (opt_safe … prf) post_state.
     679                         silent_trace … tr ∧ Srel … rel s2' post_state
     680            ]
     681].
     682#S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [ #Hclass_s2 ]
     683#REL inversion(R_post_state … t) [2,4: #post_s2 ] #EQpost normalize nodelta
     684[1,3: cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) [2,4: assumption]
     685     #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL
     686     [2: %{(mk_measurable_trace … (L_label … t) (R_label … t) (None ?) … (None ?) … pre_meas_t' …)}
     687         [ inversion(R_label … t) normalize nodelta
     688           [ #EQnone % // cases(final_is_final … good … REL) #H #_ @H lapply(R_fin_ok … t)
     689             >EQnone normalize nodelta * //
     690           | #r_lab #EQr_lab lapply(R_fin_ok … t) >EQr_lab normalize nodelta * #_ * #x *
     691             >EQpost #EQ destruct
     692           ]
     693         | normalize nodelta %
     694           [ -REL cases(initial_is_initial … good … REL) #H #_ @H ] lapply(L_init_ok … t)
     695           >EQpre normalize nodelta * //
     696         | /6 by conj/
     697         ]
     698     | lapply(R_fin_ok … t) inversion(R_label … t) [ #_ normalize nodelta * #_ >EQpost #EQ destruct]
     699       #post_lab #EQpost_lab normalize nodelta *** #Hfin #Hpost_lab1 #Hpost_lab2 *
     700       #s2_post * >EQpost #EQ destruct(EQ) #exe cases(case_cl_io … (as_classify … s2_post))
     701       [ #Hio lapply(io_entering … Hio … exe) [ /3 by pre_meas, tail_of_premeasurable_is_not_io/ ]
     702         * #c #EQ destruct(EQ) cases(simulate_io_in … good … exe … REL) //
     703         [2: /3 by pre_meas, tail_of_premeasurable_is_not_io/] #x1 * #x2 * #t1 *
     704         ** #sil_t1 #exe' #Hx2 #REL1
     705         %{(mk_measurable_trace … (L_label … t) (Some ? (cost_act (Some ? c))) (None ?) … (Some ? x2) … (t'@t1) …)}
     706         [ normalize nodelta % [2: %{x2} % //] % [2: * #x3 * #x4 #EQ destruct] % [2: % %]
     707           @notb_Prop % #ABS @(as_final_ok … ABS exe')
     708         | normalize nodelta lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: // ]
     709           -REL cases(initial_is_initial … good … REL) #H3 #_ @H3 assumption
     710         | /3 by append_silent_premeasurable/
     711         | % [2: % [ % #EQ destruct] whd in match (opt_safe ???); assumption] %
     712           [% // % // ] >get_cost_label_invariant_for_append_silent_trace_r assumption
     713         ]
     714       | (*go by cases on the instruction executed TODO *) cases daemon
     715       ]
     716    ]
     717|*: cases daemon (*TODO*)
     718]
     719qed.
     720
     721
     722
     723
     724#L_label * [| #R_label] * [2,4: #pre_s1] #L_s1 #R_s2 * [2,4,6,8: #post_s2] #t #pre_meas_t
     725normalize nodelta * [1,2,5,6: * ] #Hinitial [1,2,3,4: #Hcost #pre_exe |*: #EQ destruct(EQ) ]
     726* [2,4,6,8: ** ] #Hfinal [5,6,7,8: #EQ destruct(EQ) |*:
     727
     728
     729whd in ⊢ (% → ?);
     730
     731
    379732
    380733
     
    497850       ]
    498851    ]
     852    *)
  • LTS/Traces.ma

    r3391 r3394  
    5151coercion call_act_label_to_cost_label.
    5252
     53definition eq_nf_label : NonFunctionalLabel → NonFunctionalLabel → bool ≝
     54λx,y.match x with [ a_non_functional_label n ⇒
     55                    match y with [a_non_functional_label m ⇒ eqb n m ] ].
     56
     57lemma eq_fn_label_elim : ∀P : bool → Prop.∀l1,l2 : NonFunctionalLabel.
     58(l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eq_nf_label l1 l2).
     59#P * #l1 * #l2 #H1 #H2 normalize @eqb_elim /3/ * #H3 @H2 % #EQ destruct @H3 % qed.
     60
     61definition DEQNonFunctionalLabel ≝ mk_DeqSet NonFunctionalLabel eq_nf_label ?.
     62#x #y @eq_fn_label_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
     63assumption
     64qed.
     65
     66unification hint  0 ≔ ;
     67    X ≟ DEQNonFunctionalLabel
     68(* ---------------------------------------- *) ⊢
     69    NonFunctionalLabel ≡ carr X.
     70
     71unification hint  0 ≔ p1,p2;
     72    X ≟ DEQNonFunctionalLabel
     73(* ---------------------------------------- *) ⊢
     74    eq_nf_label p1 p2 ≡ eqb X p1 p2.
     75
     76definition eq_function_name : FunctionName → FunctionName → bool ≝
     77λf1,f2.match f1 with [ a_function_id n ⇒ match f2 with [a_function_id m ⇒ eqb n m ] ].
     78
     79lemma eq_function_name_elim : ∀P : bool → Prop.∀f1,f2.
     80(f1 = f2 → P true) → (f1 ≠ f2 → P false) → P (eq_function_name f1 f2).
     81#P * #f1 * #f2 #H1 #H2 normalize @eqb_elim /2/ * #H3 @H2 % #EQ destruct @H3 % qed.
     82
     83definition DEQFunctionName ≝ mk_DeqSet FunctionName eq_function_name ?.
     84#x #y @eq_function_name_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
     85assumption
     86qed.
     87
     88unification hint  0 ≔ ;
     89    X ≟ DEQFunctionName
     90(* ---------------------------------------- *) ⊢
     91    FunctionName ≡ carr X.
     92
     93unification hint  0 ≔ p1,p2;
     94    X ≟ DEQFunctionName
     95(* ---------------------------------------- *) ⊢
     96    eq_function_name p1 p2 ≡ eqb X p1 p2.
     97
     98definition eq_return_cost_lab : ReturnPostCostLabel → ReturnPostCostLabel → bool ≝
     99λc1,c2.match c1 with [a_return_cost_label n ⇒ match c2 with [ a_return_cost_label m ⇒ eqb n m]].
     100
     101lemma eq_return_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
     102(c1 ≠ c2 → P false) → P (eq_return_cost_lab c1 c2).
     103#P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed.
     104
     105definition DEQReturnPostCostLabel ≝ mk_DeqSet ReturnPostCostLabel eq_return_cost_lab ?.
     106#x #y @eq_return_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
     107assumption
     108qed.
     109
     110unification hint  0 ≔ ;
     111    X ≟ DEQReturnPostCostLabel
     112(* ---------------------------------------- *) ⊢
     113    ReturnPostCostLabel ≡ carr X.
     114
     115unification hint  0 ≔ p1,p2;
     116    X ≟ DEQReturnPostCostLabel
     117(* ---------------------------------------- *) ⊢
     118    eq_return_cost_lab p1 p2 ≡ eqb X p1 p2.
     119
     120definition eq_call_cost_lab : CallCostLabel → CallCostLabel → bool ≝
     121λc1,c2.match c1 with [a_call_label x ⇒ match c2 with [a_call_label y ⇒ eqb x y ]].
     122
     123lemma eq_call_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
     124(c1 ≠ c2 → P false) → P (eq_call_cost_lab c1 c2).
     125#P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed.
     126
     127definition DEQCallCostLabel ≝ mk_DeqSet CallCostLabel eq_call_cost_lab ?.
     128#x #y @eq_call_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
     129assumption
     130qed.
     131
     132unification hint  0 ≔ ;
     133    X ≟ DEQCallCostLabel
     134(* ---------------------------------------- *) ⊢
     135    CallCostLabel ≡ carr X.
     136
     137unification hint  0 ≔ p1,p2;
     138    X ≟ DEQCallCostLabel
     139(* ---------------------------------------- *) ⊢
     140    eq_call_cost_lab p1 p2 ≡ eqb X p1 p2.
     141
     142definition eq_costlabel : CostLabel → CostLabel → bool ≝
     143λc1.match c1 with
     144  [ a_call x1 ⇒ λc2.match c2 with [a_call y1 ⇒ x1 == y1 | _ ⇒ false ]
     145  | a_return_post x1 ⇒
     146      λc2.match c2 with [ a_return_post y1 ⇒ x1 == y1 | _ ⇒ false ]
     147  | a_non_functional_label x1 ⇒
     148     λc2.match c2 with [a_non_functional_label y1 ⇒ x1 == y1 | _ ⇒ false ]
     149  ].
     150
     151lemma eq_costlabel_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
     152(c1 ≠ c2 → P false) → P (eq_costlabel c1 c2).
     153#P * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??);
     154try (@H2 % #EQ destruct)
     155[ change with (eq_call_cost_lab ??) in ⊢ (?%); @eq_call_cost_lab_elim
     156  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
     157| change with (eq_return_cost_lab ??) in ⊢ (?%);
     158   @eq_return_cost_lab_elim
     159   [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
     160| change with (eq_nf_label ??) in ⊢ (?%); @eq_fn_label_elim
     161  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
     162]
     163qed.
     164
     165
     166definition DEQCostLabel ≝ mk_DeqSet CostLabel eq_costlabel ?.
     167#x #y @eq_costlabel_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
     168assumption
     169qed.
     170
     171unification hint  0 ≔ ;
     172    X ≟ DEQCostLabel
     173(* ---------------------------------------- *) ⊢
     174    CostLabel ≡ carr X.
     175
     176unification hint  0 ≔ p1,p2;
     177    X ≟ DEQCostLabel
     178(* ---------------------------------------- *) ⊢
     179    eq_costlabel p1 p2 ≡ eqb X p1 p2.
     180
     181   
     182
     183
    53184inductive ActionLabel : Type[0] ≝
    54185 | call_act : FunctionName → (CallCostLabel + NonFunctionalLabel) → ActionLabel
     
    76207 ; as_initial : as_status → bool
    77208 ; as_final : as_status → bool
    78  ; is_io_entering : NonFunctionalLabel → bool
    79  ; is_io_exiting : NonFunctionalLabel → bool
    80209 ; jump_emits : ∀s1,s2,l.
    81210      as_classify … s1 = cl_jump →
    82211      as_execute l s1 s2 → is_non_silent_cost_act l
     212 ; io_entering : ∀s1,s2,l.as_classify … s2 = cl_io →
     213      as_execute l s1 s2 → is_non_silent_cost_act l
     214 ; io_exiting : ∀s1,s2,l.as_classify … s1 = cl_io →
     215     as_execute l s1 s2 → is_non_silent_cost_act l
    83216 }.
    84  
     217 (*
    85218definition is_act_io_entering : abstract_status → ActionLabel → bool ≝
    86219λS,l.match l with
     
    104237| init_act ⇒ false
    105238].
    106 
     239*)
    107240
    108241inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
     
    182315λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
    183316
    184 inductive silent_trace (S : abstract_status) :
     317inductive pre_silent_trace (S : abstract_status) :
    185318∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    186 | silent_empty : ∀st : S.as_classify … st ≠ cl_io → silent_trace … (t_base S st)
     319| silent_empty : ∀st : S.as_classify … st ≠ cl_io → pre_silent_trace … (t_base S st)
    187320| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
    188                 ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → silent_trace … tl →
    189                 silent_trace … (t_ind … prf … tl).
    190 
    191 lemma silent_io : ∀S : abstract_status.
    192 ∀s1,s2 : S. ∀t : raw_trace … s1 s2. silent_trace … t →
     321                ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → pre_silent_trace … tl →
     322                pre_silent_trace … (t_ind … prf … tl).
     323               
     324definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
     325raw_trace S st1 st2 → bool ≝
     326λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
     327
     328definition silent_trace : ∀S:abstract_status.∀s1,s2 : S.
     329raw_trace S s1 s2 → Prop ≝ λS,s1,s2,t.pre_silent_trace … t ∨
     330¬ (bool_to_Prop (is_trace_non_empty … t)).
     331
     332lemma pre_silent_io : ∀S : abstract_status.
     333∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t →
    193334as_classify … s2 ≠ cl_io.
    194335#S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
     
    198339qed.
    199340
    200 definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
    201 raw_trace S st1 st2 → bool ≝
    202 λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
    203341(*
    204342definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
Note: See TracChangeset for help on using the changeset viewer.