Changeset 3391 for LTS


Ignore:
Timestamp:
Oct 10, 2013, 5:28:33 PM (6 years ago)
Author:
piccolo
Message:

Definition of well formed trace is in the operational semantics

Location:
LTS
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3390 r3391  
    1414     ∀s1,s2,s1' : S.
    1515      as_execute … (cost_act (None ?))  s1 s1'→
    16       Srel … rel s1 s2 →
     16      Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    1717      ∃s2'. ∃t: raw_trace S s2 s2'.
    1818        Srel … rel s1' s2' ∧ silent_trace … t
     
    2020     ∀s1,s2,l,s1'.
    2121      as_execute S (cost_act (Some ? l)) s1 s1' →
    22       as_classify … s1' ≠ cl_io →
     22      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    2323      Srel … rel s1 s2 →
    2424      ∃s2',s2'',s2'''.
    2525       ∃t1: raw_trace S s2 s2'.
    26        as_execute … (cost_act (Some ? l)) s2' s2'' ∧ as_classify … s2'' ≠ cl_io ∧
     26       as_execute … (cost_act (Some ? l)) s2' s2'' ∧
    2727       ∃t3: raw_trace S s2'' s2'''.
    2828        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     
    3131      is_call_post_label … s1 →
    3232      as_execute … (call_act f l) s1 s1' →
    33       as_classify … s1' ≠ cl_io →
     33      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    3434      Srel … rel s1 s2 →
    3535      ∃s2',s2'',s2'''.
    3636       ∃t1: raw_trace S s2 s2'.
    37        as_classify … s2' ≠ cl_jump ∧
    3837       as_execute … (call_act f l) s2' s2'' ∧
    3938       bool_to_Prop(is_call_post_label … s2') ∧
    40        as_classify … s2'' ≠ cl_io ∧
    4139       ∃t3: raw_trace S s2'' s2'''.
    4240        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     
    4442     ∀s1,s2,s1' : S.∀l.
    4543      as_execute S (ret_act (Some ? l)) s1 s1' →
    46       as_classify … s1' ≠ cl_io →
     44      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    4745      Srel  … rel s1 s2 →
    4846      ∃s2',s2'',s2'''.
    4947       ∃t1: raw_trace S s2 s2'.
    50        as_classify … s2' ≠ cl_jump ∧
    5148       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
    52        as_classify … s2'' ≠ cl_io ∧
    5349       ∃t3: raw_trace S s2'' s2'''.
    5450        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     
    5753      as_execute … (call_act f l) s1 s1' →
    5854      ¬ is_call_post_label … s1 →
     55      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
    5956      Srel … rel s1 s2 →
    6057      ∃s2',s2'',s2'''.
    6158       ∃t1: raw_trace S s2 s2'.
    6259       bool_to_Prop (¬ is_call_post_label … s2') ∧
    63        as_execute … (call_act f l) s2' s2'' ∧ as_classify … s2' ≠ cl_jump ∧
    64        as_classify … s2'' ≠ cl_io ∧
     60       as_execute … (call_act f l) s2' s2'' ∧
    6561       ∃t3: raw_trace S s2'' s2'''.
    6662        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     
    6965     ∀s1,s2,s1' : S.
    7066      as_execute … (ret_act (None ?)) s1 s1' →
    71       Srel … rel s1 s2 → as_classify … s2 ≠ cl_io ∧
     67      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
     68      Srel … rel s1 s2 →
    7269      ∃s2',s2'',s2'''.
    7370       ∃t1: raw_trace S s2 s2'.
    74        as_execute … (ret_act (None ?)) s2' s2''  ∧ as_classify … s2' ≠ cl_jump ∧
    75        as_classify … s2'' ≠ cl_io ∧
     71       as_execute … (ret_act (None ?)) s2' s2''  ∧
    7672       ∃t3: raw_trace S s2'' s2'''.
    7773        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
     
    10298lemma append_premeasurable_silent : ∀S : abstract_status.
    10399∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
    104 pre_measurable_trace … t → pre_silent_trace … t' → as_classify … st1' ≠ cl_io →
     100pre_measurable_trace … t → silent_trace … t' →
    105101pre_measurable_trace … (t' @ t).
    106102#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
    107 [ #st #t #Hpre #_ #_ whd in ⊢ (????%); assumption]
     103[ #st #t #Hpre #_ whd in ⊢ (????%); assumption]
    108104#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre #H inversion H in ⊢ ?;
    109 [ #s #EQ1 #EQ2 destruct #EQ destruct]
     105[ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
    110106#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
    111 destruct #_ #Hs1' whd in ⊢ (????%); %2
     107destruct #_ whd in ⊢ (????%); %2
    112108[ assumption
    113109| %{(None ?)} %
     
    116112qed.
    117113
    118 lemma pre_silent_is_premeasurable : ∀S : abstract_status.
    119 ∀st1,st2 : S. ∀t : raw_trace S st1 st2.as_classify … st1 ≠cl_io → pre_silent_trace … t
     114lemma silent_is_premeasurable : ∀S : abstract_status.
     115∀st1,st2 : S. ∀t : raw_trace S st1 st2.silent_trace … t
    120116→ pre_measurable_trace … t.
    121117#S #st1 #st2 #t elim t
    122 [ #st #Hst #H inversion H in ⊢ ?; [ #st' #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
    123   #st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
    124 -t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #Hst1 #H inversion H in ⊢ ?;
    125 [ #st #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
     118[ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
     119#st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
     120-t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H in ⊢ ?;
     121[ #st #H2 #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
    126122#_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
    127123@IH assumption
     
    135131lemma append_silent_premeasurable : ∀S : abstract_status.
    136132∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
    137 pre_measurable_trace … t' → pre_silent_trace … t → as_classify … st1 ≠ cl_io →
     133pre_measurable_trace … t' → silent_trace … t →
    138134pre_measurable_trace … (t' @ t).
    139135#S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
    140 [ normalize #st #Hst #r #H1 #H2 @pre_silent_is_premeasurable assumption
     136[ normalize #st #Hst #r #H1 @silent_is_premeasurable assumption
    141137|2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct
    142   [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r #Hs3 [ %2 | %3 | %4 ]
     138  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ]
    143139  try ( %{x} %) try @IH try assumption % ]
    144140#s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
    145141#EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
    146 #r #pre_r #Hs5 normalize
    147 cut(∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
    148     ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
    149     ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2)
    150 [ @append_tind_commute ] #H >H >H >append_associative <H in ⊢ (????(??????%)); %5
     142#r #pre_r normalize
     143>append_tind_commute >append_tind_commute >append_associative
     144<append_tind_commute in ⊢ (????(??????%)); %5
    151145try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
    152146qed.
    153 
    154 
    155 
    156 definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
    157 raw_trace S st1 st2 → bool ≝
    158 λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
    159147
    160148(*
     
    175163qed.*)
    176164
     165(*
    177166lemma well_formed_append : ∀S : abstract_status.
    178167∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
     
    210199qed.
    211200*)
    212 
     201*)
    213202lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
    214203∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
    215 pre_silent_trace … t1 →
     204silent_trace … t1 →
    216205get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
    217206#S #st1 #st2 #st3 #t1 elim t1
    218207[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 #H
    219 inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
     208inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
    220209#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
    221210#_ whd in ⊢ (??%?); >IH [%] assumption
     
    242231*)
    243232
     233lemma head_of_premeasurable_is_not_io : ∀S : abstract_status.
     234∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
     235as_classify … st1 ≠ cl_io.
     236#S #st1 #st2 #t #H inversion H //
     237qed.
     238
    244239
    245240theorem simulates_pre_mesurable:
     
    248243  simulation_conditions S rel →
    249244  pre_measurable_trace … t1 →
    250   well_formed_trace … t1 → ∀s2 : S.
    251   as_classify … s2 ≠ cl_io → Srel … rel s1 s2 →
     245  ∀s2 : S.
     246 as_classify … s2 ≠ cl_io →  Srel … rel s1 s2 →
    252247  ∃s2'. ∃t2: raw_trace … s2 s2'.
    253248    pre_measurable_trace … t2 ∧
    254     well_formed_trace … t2 ∧
    255249    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
    256250    Srel … rel s1' s2'.
    257251#S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
    258 [ #st #H1 #well_formed #s2 #H2 #REL %{s2} %{(t_base …)}
    259   /8 by refl, pm_empty, wf_empty, conj/
     252[ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
     253  /8 by refl, silent_empty, conj, silent_is_premeasurable/
    260254| #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
    261   #pre_measurable_tl #IH #well_formed #s2 #classify_s2 #REL
    262   [ cases(simulate_tau … good … execute … REL) #s2'' * #t_s2'' * #RELst2s2''
    263     ** #silent_ts2'' #Hclass_s2 #wf_ts2'' cases(IH … RELst2s2'')
    264     [2: cases(well_formed_trace_inv … well_formed)
    265          [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
    266              #EQ destruct(EQ) assumption
    267          | *
    268             [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct
    269                 assumption
    270             | * #EQ1 #EQ2 destruct
    271             ]
    272          ]
    273     |3: @(silent_io … silent_ts2'')  assumption   
    274     ]
    275     #s3 * #ts3 *** #pre_meas_ts3 #well_formed_ts3 #EQcost #RELst3s3
    276     %{s3} %{(t_s2'' @ ts3)} % [2: assumption] %
    277     [ %
    278       [ @append_premeasurable_silent assumption
    279       | @append_well_formed assumption
    280       ]
    281     | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
    282       [% | assumption]
    283     ]
     255  #pre_measurable_tl #IH #s2 #classify_s2 #REL
     256  [ cases(simulate_tau … good … execute … REL) /2/ #s2'' * #t_s2'' * #RELst2s2''
     257    #silent_ts2'' cases(IH … RELst2s2'') /2 by silent_io/
     258    #s3 * #ts3 ** #pre_meas_ts3 #EQcost #RELst3s3
     259    %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % /2 by append_premeasurable_silent/
     260    whd in ⊢ (??%?); /2/
    284261  | cases(simulate_label … good … execute … REL)
    285     [2: cases pre_measurable_tl
    286         [ #st #H @H
    287         | #st1 #st2 #st3 #l #prf #tl #H #_ #_ @H
    288         | #st1 #st2 #st3 #l #H #_ #tl #_ #_ @H
    289         | #st1 #st2 #st3 #l #_ #tl #H #_ #_ #_ @H
    290         | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #_ #t1 #t2 #_ #H #_ #_ #_ #_ #_ #_ #_ @H
    291         ]
    292     ]
    293     #s2'' * #s2''' * #s2'''' * #t_s2'' ** #exe_s2''' #CLASS' * #t_s2'''' ** #RELst2_s2''''
    294     ** #sil_ts2'' #Hclass_s2 #wf_ts2'' ** #sil_t_s2'''' #Hclass_s2''' #wf_ts2'''' cases(IH … RELst2_s2'''')
    295     [2: cases(well_formed_trace_inv … well_formed)
    296          [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
    297              #EQ destruct(EQ) assumption
    298          | *
    299             [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct
    300                 assumption
    301             | * #EQ1 #EQ2 destruct
    302             ]
    303          ]
    304     |3: @(silent_io … sil_t_s2'''') assumption
    305     ]
    306     #s3 * #t_s3 *** #pre_s3 #well_s3 #EQcost #RElst3s3 %{s3}
     262    [2,3: /2/]
     263    #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/
     265    #s3 * #t_s3 ** #pre_s3 #EQcost #RElst3s3 %{s3}
    307266    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
    308267    %
    309     [ %
    310       [ @append_premeasurable_silent try assumption %2
    311         [ @(silent_io … t_s2'') assumption
    312         | %{(Some ? c)} %
    313         ]
    314         @append_premeasurable_silent assumption
    315       | @append_well_formed try assumption inversion(as_classify … s2'')
    316         #Hclass
    317         [ %3 [2: %{c} %]
    318         |*: %2 [2,4: >Hclass % #EQ destruct]
    319         ]
    320         @append_well_formed assumption
    321       ]
     268    [ /4 by pm_cons_cost_act, silent_io, ex_intro, append_premeasurable_silent/
    322269    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
    323       [2: assumption] whd in ⊢ (???%);
    324       >get_cost_label_invariant_for_append_silent_trace_l
    325       [ % | assumption]
     270      [2: assumption] whd in ⊢ (???%);
     271      >get_cost_label_invariant_for_append_silent_trace_l //
    326272    ]
    327273  ]
    328274| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
    329   #pre_meas_tl #IH #H inversion H
    330   [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ]
    331   #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl'
    332   [ #class_no_jump | whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ]
    333   #_ #EQ1 #EQ2 #EQ3 destruct #_ -H #s2 #class_s2 #RELst1s2
    334   cases(simulate_ret_l … good … exe_st1_st2 … RELst1s2)
    335   [2: inversion pre_meas_tl
    336       try #x1 try #x2 try #x3 try #x4 try #x5 try #x6
    337       try #x11 try #x12 try #x13 try #x14 try #x15 try #x16
    338       try #x17 try #x18 try #x19 try #x20 try #x21 try #x22
    339       try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33
    340       destruct assumption ]
    341   #s2' * #s2'' * #s2''' * #t1 *** #j_s2' #exe_s2'' #class_s2'' * #t2 ** #rel_s2_s2'''
    342   #sil_t1 #sil_t2
    343   cases(IH … wf_tl' … rel_s2_s2''')
    344   [2: @(silent_io … (proj1 … (proj1 … sil_t2))) assumption]
    345   #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL
     275  #pre_meas_tl #IH #s2 #class_s2 #RELst1s2
     276  cases(simulate_ret_l … good … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
     277  #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2'''
     278  #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
     279  [2: @(silent_io … sil_t2) assumption]
     280  #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL
    346281  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
    347282  % [2: whd in ⊢ (??%?);
    348         >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t1)))
     283        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
    349284        whd in ⊢ (???%);
    350         >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t2)))
     285        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t2)
    351286        @eq_f assumption ]
    352   %
    353   [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_t1))]
    354     %3
    355     [ @(silent_io … (proj1 … (proj1 … sil_t1))) assumption
    356     | whd %{ret_lab} %
    357     | @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_t2))
    358     ]
    359   | @append_well_formed
    360     [ @(proj2 … sil_t1)]
    361     %2 try assumption @append_well_formed try assumption @(proj2 … sil_t2)
    362   ]
    363 | #s2 #s2' #s2'' #l #exe_s2_s2' #tl #class_s2 whd in ⊢ (% → ?); * #f * #lab #EQ destruct
    364   #post #pre_tl #IH #H inversion H [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ]
    365   #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl'
    366   [#class_no_jump | whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ]
    367    #_ #EQ1 #EQ2 #EQ3 destruct #_ -H #s2 #io_s2 #REL_st1_s2
    368    cases(simulate_call_pl … good … post … exe_st1_st2 … REL_st1_s2)
    369    [2: inversion pre_tl
    370       try #x1 try #x2 try #x3 try #x4 try #x5 try #x6
    371       try #x11 try #x12 try #x13 try #x14 try #x15 try #x16
    372       try #x17 try #x18 try #x19 try #x20 try #x21 try #x22
    373       try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33
    374       destruct assumption ]
    375    #s2' * #s2'' * #s2''' * #t1 **** #j_s2' #exe_s2'' #post' #io_s2'' * #t2 ** #REL #sil_t1 #sil_t2
    376    cases(IH … wf_tl' … REL)
    377    [2: @(silent_io … (proj1 … (proj1 … sil_t2))) assumption ]
    378    #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL1 %{s2_fin}
     287  /4 by pm_cons_lab_ret, silent_io, ex_intro, append_premeasurable_silent/
     288| #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
     289  #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
     290   cases(simulate_call_pl … good … post … exe_s1_s2 … REL_s1_s2')
     291   [2,3: /2 by head_of_premeasurable_is_not_io/ ]
     292   #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
     293   cases(IH  … REL)
     294   [2: /2 by silent_io/ ]
     295   #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL1 %{s2_fin}
    379296   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
    380297   [2: whd in ⊢ (??%?);
    381         >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t1)))
     298        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
    382299        whd in ⊢ (???%);
    383         >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … (proj1 … sil_t2)))
     300        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t2)
    384301        @eq_f assumption ]
    385    %
    386    [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_t1))]
     302   @append_premeasurable_silent try assumption
    387303     %4 try assumption
    388      [ @(silent_io … (proj1 … (proj1 … sil_t1))) assumption
     304     [ /2 by silent_io/
    389305     | whd %{f} %{lab} %
    390      | @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_t2))
     306     | /2 by append_premeasurable_silent/
    391307     ]
    392    | @append_well_formed [ @(proj2 … sil_t1) ]
    393      %2 try assumption @append_well_formed try assumption @(proj2 … sil_t2)
    394    ]
    395308| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
    396309  #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
    397   #IH1 #IH2 #wf_all #st1' #Hst1' #REL
    398   cases(simulate_call_n … good … exe_12 … Hst1 … REL)
    399   #st1'' * #st1''' * #st2' * #tr1 **** #nps_st1'' #exe_12' #Hst1'' #Hst1''' * #tr2 *** #REL1 #sil_tr1
     310  #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … good … exe_12 … Hst1 … REL) [2,3: /2/ ]
     311  #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1
    400312  #sil_tr2 #call_rel cases(IH1 … REL1)
    401   [2: inversion wf_all [ #st #EQ1 #EQ2 #EQ3 destruct]
    402       #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1 | * #y1 #EQ destruct(EQ) ] #_
    403       #EQ1 #EQ2 #EQ3 destruct #_ @(proj1 … (well_formed_append … wf_tl))
    404   |3: @(silent_io … (proj1 … (proj1 … sil_tr2))) assumption
    405   ]
    406   #st3' * #tr3 *** #pre_tr3 #wf_tr3 #EQcost_tr3 #REL2
    407   cases(simulate_ret_n … good … exe_34 … REL2) #Hst3' * #st3'' * #st4' * #st4'' *
    408   #tr4 *** #exe_34' #Hst3'' #Hst4' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3)
    409   [2: inversion wf_all in ⊢ ?; [#st #EQ1 #EQ2 destruct whd in ⊢ (????% → ?); #EQ destruct]
    410       #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1 | * #y1 #EQ destruct(EQ)] #_
    411       #EQ1 #EQ2 #EQ3 destruct #_ cases(well_formed_append … wf_tl) -wf_tl -wf_all
    412       #_ #H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
    413       #z1 #z2 #z3 #w #prf' #tl' #wf_tl' [ #Hz1 | * #w1 #EQ destruct(EQ)] #_
    414       #EQ1 #EQ2 #EQ3 destruct #_ assumption
    415   |3: @(silent_io … (proj1 … (proj1 … sil_tr5))) assumption
    416   ]
    417   #st5' * #tr6 *** #pre_tr6 #wf_tr6 #EQcost_tr6 #REL4 %{st5'}
     313  [2: /2 by silent_io/ ]
     314  #st3' * #tr3 ** #pre_tr3 #EQcost_tr3 #REL2
     315  cases(simulate_ret_n … good … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
     316  #st3'' * #st4' * #st4'' *
     317  #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by silent_io/ ]
     318  #st5' * #tr6 ** #pre_tr6 #EQcost_tr6 #REL4 %{st5'}
    418319  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
    419320  % [2: assumption] %
    420   [ %
    421      [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_tr1)) ]
    422        %5
    423        [ @(silent_io … (proj1 … (proj1 … sil_tr1))) assumption
    424        | @(silent_io … (proj1 … (proj1 … sil_tr4))) assumption
     321  [ @append_premeasurable_silent try assumption %5
     322       [1,2: /2 by silent_io/
    425323       | whd %{f} %{l} %
    426324       | assumption
    427        | @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_tr2))]
    428          @append_silent_premeasurable try assumption @(proj1 … (proj1 … sil_tr4))
    429        | @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_tr5))
     325       | @append_premeasurable_silent try assumption
     326         @append_silent_premeasurable assumption
     327       | @append_premeasurable_silent try assumption
    430328       | @(RET_REL … call_rel) assumption
    431329       | %
    432330       ]
    433      | @append_well_formed [ @(proj2 … sil_tr1) ]
    434        %2 [2: assumption] >append_associative @append_well_formed
    435        [ @(proj2 … sil_tr2) ]  @append_well_formed
    436        [ @append_well_formed try assumption @silent_is_well_formed assumption ]
    437        %2 [2: assumption] @append_well_formed try assumption @silent_is_well_formed
    438        assumption
    439      ]
    440   | >get_cost_label_invariant_for_append_silent_trace_l [2: @(proj1 … (proj1 … sil_tr1)) ]
     331  | >get_cost_label_invariant_for_append_silent_trace_l [2: // ]
    441332    whd in ⊢ (??%%); @eq_f >append_associative
    442333    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
    443     [2: @(proj1 … (proj1 … sil_tr2)) ] >append_associative
     334    [2: // ] >append_associative
    444335    >get_cost_label_append in ⊢ (???%);
    445336    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
    446     [2: @(proj1 … (proj1 … sil_tr4)) ] normalize
     337    [2: //] normalize
    447338    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
    448     [2: @(proj1 … (proj1 … sil_tr5)) ] >get_cost_label_append in ⊢ (??%?); @eq_f2
     339    [2: // ] >get_cost_label_append in ⊢ (??%?); @eq_f2
    449340    assumption
    450341  ]
  • LTS/Traces.ma

    r3390 r3391  
    6565 | cl_other : status_class.
    6666
     67definition is_non_silent_cost_act : ActionLabel → Prop ≝
     68λact. ∃l. act = cost_act (Some ? l).
     69
    6770record abstract_status : Type[2] ≝
    6871 { as_status :> Type[0]
     
    7578 ; is_io_entering : NonFunctionalLabel → bool
    7679 ; is_io_exiting : NonFunctionalLabel → bool
     80 ; jump_emits : ∀s1,s2,l.
     81      as_classify … s1 = cl_jump →
     82      as_execute l s1 s2 → is_non_silent_cost_act l
    7783 }.
    7884 
     
    118124λact.act = ret_act (None ?).
    119125
    120 definition is_non_silent_cost_act : ActionLabel → Prop ≝
    121 λact. ∃l. act = cost_act (Some ? l).
    122 
    123126definition is_costlabelled_act : ActionLabel → Prop ≝
    124127λact.match act with [ call_act _ _ ⇒ True
     
    127130                    | init_act ⇒ False
    128131                    ].
    129 
    130 inductive well_formed_trace (S : abstract_status) :
    131    ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    132   | wf_empty : ∀st: S.well_formed_trace … (t_base S st)
    133   | wf_cons_no_jump :  ∀st1,st2,st3 : S.∀l : ActionLabel.
    134                        ∀prf: as_execute S l st1 st2.∀ tl: raw_trace S st2 st3.
    135                        well_formed_trace … tl → as_classify … st1 ≠ cl_jump →
    136                        well_formed_trace … (t_ind … prf … tl)
    137   | wf_cons_jump : ∀st1,st2,st3 : S.∀ l : ActionLabel.
    138                   ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    139                   well_formed_trace … tl → is_non_silent_cost_act l →
    140                   well_formed_trace … (t_ind … prf … tl).
    141 (*  | wf_cons_io : ∀st1,st2,st3 : S.∀l : ActionLabel.
    142                  ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
    143                  well_formed_trace … tl → as_classify … st1 = cl_io →
    144                  is_non_silent_cost_act l → well_formed_trace … (t_ind … prf … tl).*)
    145 
     132(*
    146133lemma well_formed_trace_inv :
    147134∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2.
     
    167154qed.
    168155
     156*)
    169157
    170158let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
     
    194182λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
    195183
    196 inductive pre_silent_trace (S : abstract_status) :
     184inductive silent_trace (S : abstract_status) :
    197185∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
    198 | silent_empty : ∀st : S.pre_silent_trace … (t_base S st)
     186| silent_empty : ∀st : S.as_classify … st ≠ cl_io → silent_trace … (t_base S st)
    199187| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
    200                 ∀tl : raw_trace S st2 st3. as_classify … st2 ≠ cl_io → pre_silent_trace … tl →
    201                 pre_silent_trace … (t_ind … prf … tl).
     188                ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → silent_trace … tl →
     189                silent_trace … (t_ind … prf … tl).
    202190
    203191lemma silent_io : ∀S : abstract_status.
    204 ∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t → as_classify … s1 ≠ cl_io
     192∀s1,s2 : S. ∀t : raw_trace … s1 s2. silent_trace … t
    205193as_classify … s2 ≠ cl_io.
    206 #S #s1 #s2 #t elim t [ #st #_ #Hclass @Hclass]
    207 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H
    208 [ #st' #EQ1 #EQ2 destruct #EQ destruct]
     194#S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
     195#st1 #st2 #st3 #l #prf #tl #IH #H inversion H //
    209196#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
    210 #EQ destruct #_ #Hclass' @IH [ assumption ] assumption
     197#EQ destruct #_ @IH assumption
    211198qed.
    212199
     
    214201raw_trace S st1 st2 → bool ≝
    215202λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
    216 
     203(*
    217204definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
    218205raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧
    219 (is_trace_non_empty … t → as_classify … st1 ≠ cl_io) ∧
    220206well_formed_trace … t.
    221207
     
    223209∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t.
    224210#S #st1 #st2 #t * //
    225 qed.
     211qed. *)
    226212(* elim t -t
    227213[ #st #_ %]
Note: See TracChangeset for help on using the changeset viewer.