Changeset 3524 for LTS/Simulation.ma


Ignore:
Timestamp:
Mar 11, 2015, 4:26:40 PM (5 years ago)
Author:
piccolo
Message:

rearrangments of lemmas, final statement in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3523 r3524  
    11include "Traces.ma".
     2include "basics/jmeq.ma".
     3
     4discriminator option.
    25
    36record relations (S1,S2 : abstract_status) : Type[0] ≝
     
    9497 }.
    9598
    96 lemma append_premeasurable_silent : ∀S : abstract_status.
    97 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
    98 pre_measurable_trace … t → silent_trace … t' → 
    99 pre_measurable_trace … (t' @ t).
    100 #S #st1' #st1 #st2 #t #t' lapply t -t elim t'
    101 [ #st #t #Hpre #_ whd in ⊢ (????%); assumption]
    102 #s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?;
    103 [ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
    104 #s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
    105 destruct #_ whd in ⊢ (????%); %2
    106 [ assumption
    107 | %{(None ?)} %
    108 | @IH try assumption
    109 ]
    110 % assumption
    111 qed.
    112 
    113 lemma pre_silent_is_premeasurable : ∀S : abstract_status.
    114 ∀st1,st2 : S. ∀t : raw_trace S st1 st2.pre_silent_trace … t
    115 → pre_measurable_trace … t.
    116 #S #st1 #st2 #t elim t
    117 [ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
    118 #st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
    119 -t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H in ⊢ ?;
    120 [ #st #H2 #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
    121 #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
    122 @IH assumption
    123 qed.
    124 
    125 lemma append_tind_commute : ∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
    126     ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
    127     ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2.
    128 #S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.   
    129 
    130 lemma append_silent_premeasurable : ∀S : abstract_status.
    131 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
    132 pre_measurable_trace … t' → silent_trace … t →
    133 pre_measurable_trace … (t' @ t).
    134 #S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
    135 [ #st #Hst #r * [ #H1 @pre_silent_is_premeasurable assumption ]
    136   inversion r [2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 cases H11
    137   #ABS @⊥ @ABS % ] #s' #EQ1 #EQ2 #EQ3 destruct #_
    138   %1 assumption
    139 |2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct
    140   [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ]
    141   try ( %{x} %) try @IH try assumption % ]
    142 #s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
    143 #EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
    144 #r #pre_r normalize
    145 >append_tind_commute >append_tind_commute >append_associative
    146 <append_tind_commute in ⊢ (????(??????%)); %5
    147 try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
    148 qed.
    149 
    150 (*
    151 lemma append_well_formed_silent : ∀S : abstract_status.
    152 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
    153 well_formed_trace … t → pre_silent_trace … t' →
    154 (is_trace_non_empty … t' → as_classify … st) →
    155 well_formed_trace … (t' @ t).
    156 #S #st1' #st1 #st2 #t #t' lapply t -t elim t'
    157 [ #st #t #H #_ #_ assumption ]
    158 #s1' #s2' #s3' #l #prf #tl #IH #t #well_formed_t #H
    159 inversion H in ⊢ ?;
    160 [ #st #EQ1 #EQ2 #EQ3 destruct]
    161 #st1'' #st2' #st3' #prf' #tl' #Hclass #silent_tl #_
    162 #EQ1 destruct #EQ #EQ1 destruct #_ #Hclass1 %2
    163 [2: >(Hclass1 I) % #EQ destruct]
    164 @IH try assumption #_ assumption
    165 qed.*)
    166 
    167 (*
    168 lemma well_formed_append : ∀S : abstract_status.
    169 ∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
    170 well_formed_trace … (t1 @ t2) → well_formed_trace … t1 ∧ well_formed_trace … t2.
    171 #S #st1 #st2 #st3 #t1 #t2 #H %
    172 [ lapply H -H lapply t2 -t2 elim t1 [ //] #st1' #st2' #st3' #l #exe #tl #IH #r
    173 #H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 normalize in EQ3; destruct ]
    174 #st1'' #st2'' #st3'' #l' #prf' #tl' #wf_tl' [#Hst1'' | * #x #EQ destruct] #_
    175 #EQ1 #EQ2 normalize in ⊢ (% → ?); #EQ3 destruct #_
    176 [ %2 [ @IH assumption ] assumption | %3 [ @IH assumption ] %{x} % ]
    177 ]
    178 lapply H lapply t2 -t2 elim t1 [ #st #r normalize //]
    179 #s1 #s2 #s3 #l #prf #tl #IH #r #H inversion H in ⊢ ?;
    180 [ #st #EQ1 #EQ2 normalize #EQ3 destruct ]
    181 #s1' #s2' #s3' #l' #prf' #tl' #wf_tl' #Hs1' #_ normalize #EQ1 #EQ2 #EQ3 destruct
    182 #_ @IH assumption
    183 qed.
    184 
    185 
    186 lemma append_well_formed : ∀S : abstract_status.
    187 ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
    188 well_formed_trace … t1 → well_formed_trace … t2 → well_formed_trace … (t1 @ t2).
    189 #S #st1 #st2 #st3 #t1 #t2 #H lapply t2 -t2 elim H
    190 [ #st #r #H1 @H1 ]
    191 #s1 #s2 #s3 #l #prf #tl #wf_tl #Hs1 #IH #r #wf_r normalize [ %2 | %3]
    192 try @IH assumption
    193 qed.
    194 (*
    195 lemma silent_is_well_formed : ∀S : abstract_status.
    196 ∀st1,st2 : S.∀t : raw_trace … st1 st2.silent_trace … t → well_formed_trace … t.
    197 #S #st1 #st2 #t elim t [ #st #_ %]
    198 #s1 #s2 #s3 #l #prf #tl #IH * #H inversion H [ #st #EQ1 #EQ2 #EQ3 destruct]
    199 #s1' #s2' #s3' #prf' #tl' #Hs2' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #_ #H1 %2
    200 [ @IH % [2: #_ ] assumption | >(H1 I) % #EQ destruct]
    201 qed.
    202 *)
    203 *)
    204 lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
    205 ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
    206 silent_trace … t1 →
    207 get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
    208 #S #st1 #st2 #st3 #t1 elim t1
    209 [#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 *
    210 [2: whd in match is_trace_non_empty; normalize nodelta * #ABS @⊥ @ABS %]
    211 #H inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
    212 #st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
    213 #_ whd in ⊢ (??%?); >IH [%] %1 assumption
    214 qed.
    215 
    216 (*
    217 lemma raw_trace_ind_r : ∀S : abstract_status.
    218 ∀P : (∀st1,st2.raw_trace S st1 st2 → Prop).
    219 (∀st : S.P … (t_base … st)) →
    220 (∀st1,st2,st3,l.
    221  ∀prf : as_execute S l st2 st3.
    222  ∀tl : raw_trace S st1 st2. P … tl → P … (tl @ (t_ind … prf … (t_base … st3)))) →
    223 ∀st1,st2 : S.∀t : raw_trace S st1 st2.P … t.
    224 #S #P #base #ind #st1 #st2 #t elim t [ assumption]
    225 #st1 #st2 #st3 #l #prf #raw #IH
    226 *)
    227 
    228 lemma head_of_premeasurable_is_not_io : ∀S : abstract_status.
    229 ∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
    230 as_classify … st1 ≠ cl_io.
    231 #S #st1 #st2 #t #H inversion H //
    232 qed.
    233 
    234 (*
     99
    235100theorem simulates_pre_mesurable:
    236101 ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
     
    243108    pre_measurable_trace … t2 ∧
    244109    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
    245     Srel … rel s1' s2'.
    246 #S1 #S2 #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
    247 [ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
    248   /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/
    249 | #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
    250   #pre_measurable_tl #IH #s2 #classify_s2 #REL
    251   [ cases(simulate_tau … good … execute … REL) /2/ #s2'' * #t_s2'' * #RELst2s2''
    252     #silent_ts2'' cases(IH … RELst2s2'')
    253     [2: cases silent_ts2'' /2 by pre_silent_io/ inversion t_s2''
    254         [ #x #EQ1 #EQ2 #EQ3 destruct // ]
    255         #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct * #ABS @⊥ @ABS % ]
    256     #s3 * #ts3 ** #pre_meas_ts3 #EQcost #RELst3s3
    257     %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % /2 by append_premeasurable_silent/
    258     whd in ⊢ (??%?); /2/
    259   | cases(simulate_label … good … execute … REL)
     110    Srel … rel s1' s2' ∧
     111    (measurable_suffix … t1 → measurable_suffix … t2) ∧
     112    (silent_trace … t1 → silent_trace … t2).
     113#S1 #S2 #rel #s1 #s1' #t1 #sim #H elim H -t1 -s1 -s1'
     114[ #st #Hst #s2 #Hs2 #Rsts2 %{s2} %{(t_base …)} %
     115 [ % [ % // % // % //] * #s_em ** [ #sx | #x1 #x2 #x3 #l1 #prf1 #tl1] * #t_pre * #s_post * #t_post * #sil_tpost
     116  * #prf1 ** normalize #EQ  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     117 | #_ %2 % *
     118 ]
     119| #st1 #st2 #st3 #l #prf #tl #Hclass **
     120  [ #EQ destruct #pre_tl #IH #s2 #Hclass2 #R_st1_s2
     121    cases(simulate_tau … sim … prf … R_st1_s2) [2,3: /2 by head_of_premeasurable_is_not_io/]
     122    #s2' * #t2_init * #R_st2_s2' #silent_t2_init cases(IH … R_st2_s2')
     123    [2: cases silent_t2_init /2 by pre_silent_io/ cases t2_init in Hclass2; // 
     124        #H12 #H13 #H14 #H15 #H16 #H17 #H18 * #H19 cases(H19 I) ]
     125    #s2_fin * #t2_fin **** #pre_t2_fin #EQcost #R_st3_s2_fin #Hm #Hs %{s2_fin} %{(t2_init @ t2_fin)}
     126    cut(? : Prop)
     127      [3: #Hpre %
     128         [ %
     129             [ %
     130                 [ %{Hpre} >get_cost_label_invariant_for_append_silent_trace_l // assumption
     131                 | assumption
     132                 ]
     133             |  #meas_suff cases(Hm ?)
     134                [ #s_pre' * #t_pre' * #s_post' * #t_post' * #sil_tpost' * #l_em * #ex_em ** #EQ
     135                  destruct #Hcall #lem_cost %{s_pre'} %{(t2_init @ t_pre')} %{s_post'} %{t_post'}
     136                  %{sil_tpost'} %{l_em} %{ex_em} /4 by conj/
     137                | cases meas_suff -meas_suff #s_em * #t_pre inversion t_pre in ⊢ ?;
     138                  [ #st #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em * #ex_em
     139                    ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ *
     140                  | #st1' #st2' #st3' #lbl #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost
     141                    * #l_em * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #cost_lem
     142                    %{st3'} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/
     143                  ]
     144                ]
     145             ]
     146        | * [2: * #H cases(H I)] #H inversion H [ #H9 #H10 #H11 #H12 #H13 #H14 destruct]
     147          #x1 #x2 #x3 #prf3 #tl'' #Hclass' #pre_siltl'' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     148          /4 by append_silent,or_introl/
     149        ]
     150     |
     151     ]
     152    @append_premeasurable_silent //
     153  | #lbl #EQ destruct #pre_tl #IH #s2 #Hs2 #REL
     154    cases(simulate_label … sim … prf … REL)
    260155    [2,3: /2/]
    261156    #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2''''
    262157    #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''')  /2 by pre_silent_io/
    263     #s3 * #t_s3 ** #pre_s3 #EQcost #RElst3s3 %{s3}
    264     %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
    265     %
    266     [ @append_premeasurable_silent // %2 /2 by ex_intro/
     158    #s3 * #t_s3 **** #pre_s3 #EQcost #RElst3s3 #Hm #Hs %{s3}
     159    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] %
     160    [2: * [ #H inversion H
     161            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
     162            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
     163            ]
     164          | * #H cases(H I)
     165          ]
     166     ]
     167    %
     168    [ % [2: assumption] %
     169      [ @append_premeasurable_silent // %2 /2 by ex_intro/
    267170       [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2''
    268171         [ #H31 #H32 #H33 #H34 #H35 destruct assumption ]
     
    273176      [2: assumption] whd in ⊢ (???%);
    274177      >get_cost_label_invariant_for_append_silent_trace_l //
    275     ]
    276   ]
    277   % assumption
     178    ] % assumption
     179    | #Hsuff cases(measurable_suffix_tind … Hsuff)
     180      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s2''} %{t_s2''} %{s2'''} %{(t_s2'''' @ t_s3)}
     181      % [ /3 by or_introl, append_silent/ ] %{(cost_act (Some ? lbl))} %{(exe_s2''')} % // % // * #f * #c #EQ destruct
     182      | #H @measurable_suffix_append change with ((t_ind ?????? t_s2'''')@t_s3) in ⊢ (????%);
     183        @measurable_suffix_append /2/
     184      ]
     185  ]
     186  ]
    278187| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
    279   #pre_meas_tl #IH #s2 #class_s2 #RELst1s2
    280   cases(simulate_ret_l … good … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
     188  #pre_meas_tl #IH #s1 #class_s2 #RELst1s2
     189  cases(simulate_ret_l … sim … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
    281190  #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2'''
    282191  #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
    283192  [2: @(pre_silent_io … sil_t2) assumption]
    284   #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL
    285   %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
    286   % [2: whd in ⊢ (??%?);
     193  #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL #Hm #Hs
     194  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} %
     195  [2: * [ #H inversion H
     196            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
     197            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
     198            ]
     199          | * #H cases(H I)
     200          ]
     201  ]
     202  %
     203    [ % [2: assumption]
     204      % [2: whd in ⊢ (??%?);
    287205        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
    288206        whd in ⊢ (???%);
     
    295213  #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65
    296214  #ABS @⊥ @ABS %
     215 |  #Hsuff cases(measurable_suffix_tind … Hsuff)
     216      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{st1} %{t1} %{st2} %{(t2 @ t_fin)}
     217      % [ /3 by or_introl, append_silent/ ] %{(ret_act (Some ? ret_lab))} %{(exe_s2'')} % // % // * #f * #c #EQ destruct
     218      | #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);
     219        @measurable_suffix_append /2/
     220      ]
     221  ]
    297222| #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
    298223  #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
    299    cases(simulate_call_pl … good … post … exe_s1_s2 … REL_s1_s2')
     224   cases(simulate_call_pl … sim … post … exe_s1_s2 … REL_s1_s2')
    300225   [2,3: /2 by head_of_premeasurable_is_not_io/ ]
    301226   #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
    302227   cases(IH  … REL)
    303228   [2: /2 by pre_silent_io/ ]
    304    #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL1 %{s2_fin}
    305    %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
     229   #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL1 #Hm #Hs %{s2_fin}
     230   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} %
     231   [2: * [ #H inversion H
     232            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
     233            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
     234            ]
     235          | * #H cases(H I)
     236          ]
     237  ]
     238  %
     239   [ % [2: assumption] %
    306240   [2: whd in ⊢ (??%?);
    307241        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
     
    317251     | @append_premeasurable_silent // % assumption
    318252     ]
    319 | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
     253   | #Hsuff cases(measurable_suffix_tind … Hsuff)
     254      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s'} %{t1} %{s2''} %{(t2 @ t_fin)}
     255      % [ /3 by or_introl, append_silent/ ] %{(call_act f lab)} %{(exe_s2'')} % // % //
     256      | #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);
     257        @measurable_suffix_append /2/
     258      ]
     259  ]
     260|  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
    320261  #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
    321   #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … good … exe_12 … Hst1 … REL) [2,3: /2/ ]
     262  #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … sim … exe_12 … Hst1 … REL) [2,3: /2/ ]
    322263  #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1
    323264  #sil_tr2 #call_rel cases(IH1 … REL1)
    324265  [2: /2 by pre_silent_io/ ]
    325   #st3' * #tr3 ** #pre_tr3 #EQcost_tr3 #REL2
    326   cases(simulate_ret_n … good … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
     266  #st3' * #tr3 **** #pre_tr3 #EQcost_tr3 #REL2 #Hm1 #Hs1
     267  cases(simulate_ret_n … sim … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
    327268  #st3'' * #st4' * #st4'' *
    328269  #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ]
    329   #st5' * #tr6 ** #pre_tr6 #EQcost_tr6 #REL4 %{st5'}
     270  #st5' * #tr6 **** #pre_tr6 #EQcost_tr6 #REL4 #Hm2 #Hs2 %{st5'}
    330271  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
    331   % [2: assumption] %
     272  %
     273  [2: * [ #H inversion H
     274            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
     275            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
     276            ]
     277          | * #H cases(H I)
     278          ]
     279  ]
     280  %
     281  [ % [2: assumption] %
    332282  [ @append_premeasurable_silent try assumption %5
    333283       [1,2: /2 by pre_silent_io/
     
    356306  ]
    357307  % //
     308 | #Hsuff cases(measurable_suffix_tind … Hsuff)
     309   [ * #_ #ABS @⊥ cases Hsuff #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em
     310     * #ex_em ** inversion t_pre in ⊢ ?;
     311     [2: #z1 #z2 #z3 #lb #exec #tail #_ #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ
     312         #EQ destruct >e0 in ABS; #ABS lapply(silent_append_l2 … ABS) -ABS * [2: * #H cases(H I)] -IH1 -IH2
     313         -Hsuff -e0 -EQ #H inversion H
     314         [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 destruct]
     315         #y1 #y2 #y3 #exec #tail1 #Hclass1 #sil_tail #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct #_ *
     316     ]
     317     #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     318     #ABS1 >ABS1 in Hst1; [2: /3 by ex_intro/] *
     319   | #Hsuff @measurable_suffix_append change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append
     320     change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append @Hm2
     321     cases(measurable_suffix_append_case … Hsuff)
     322     [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
     323       [ #H137 #H138 #H139 #H140 #H141 #H142 @⊥
     324         -H142 lapply H141 -H141 lapply H138 -H138 lapply H140 -H140 <H139 #EQ lapply t2 -t2 >EQ -EQ
     325         #st2 #_ #EQ destruct(EQ)
     326       | #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 @⊥ -Hsuff destruct
     327       ]
     328     | -Hsuff * #s_em * #t_pre inversion t_pre in ⊢ ?;
     329       [ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em ** #EQ normalize in EQ;
     330         lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ *
     331       | #a1 #a2#a3 #lbl #exe #tl1 #_ #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em
     332         * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost
     333         %{a3} %{tl1} %{s1_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /5 by conj/
     334       ]
     335     ]
     336   ]
     337 ]
    358338]
    359339qed.
    360340
    361 (* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
    362    sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
    363    cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
    364 
    365 (*
    366 lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s.
    367 #P #H1 #H2 * // @H2 % #EQ destruct qed.
    368 
    369 lemma case_cl_io : ∀s : status_class.decidable … (s = cl_io).
    370 * [2: %%] %2 % #EQ destruct qed.
    371 
    372 lemma tail_of_premeasurable_is_not_io : ∀S : abstract_status.
    373 ∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
    374 as_classify … st2 ≠ cl_io.
    375 #S #st1 #st2 #t #H elim H //
     341theorem simulates_measurable:
     342 ∀S1,S2: abstract_status.
     343 
     344 ∀rel: relations S1 S2. simulation_conditions … rel →
     345 
     346 ∀si,sn: S1. ∀t: raw_trace … si sn.
     347 
     348 ∀s1,s2. measurable … s1 s2 … t →
     349 
     350 ∀si': S2. as_classify … si' ≠ cl_io →
     351 
     352 Srel … rel si si' →
     353 
     354 ∃sn'. ∃t': raw_trace … si' sn'.
     355
     356 Srel … rel sn sn' ∧
     357
     358 get_costlabels_of_trace … t = get_costlabels_of_trace … t' ∧
     359 
     360 ∃s1',s2'. measurable … s1' s2' … t'.
     361#S1 #S2 #rel #sim_rel #si #sn #t #s1 #s2 #Hmeas #s1' #Hclass #Rsi_si'
     362cases(simulates_pre_mesurable … rel … t … Rsi_si') //
     363[2: cases Hmeas //] #sn' * #t2 **** #pre_meas_t2 #EQcost #R_sn_sn'
     364#Hmeas1 #_ %{sn'} %{t2} % [% //] @(measurable_suffix_is_measurable … t2) /4 by measurable_is_measurable_suffix/
     365<EQcost cases Hmeas #_ * #s1 * #s2 * #t_pre * #t_mid * #t_last * #l1 * #l2 * #prf1 * #prf2 ***** #EQ destruct
     366#H1 #H2 #_ #_ #_ >get_cost_label_append >length_append >get_costlabelled_is_costlabelled //
     367 >get_cost_label_append >length_append >get_costlabelled_is_costlabelled // /2 by le_plus_a/
    376368qed.
    377 
    378 lemma get_cost_label_invariant_for_append_silent_trace_r :∀S : abstract_status.
    379 ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
    380 silent_trace … t2 →
    381 get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t1.
    382 #S #st1 #st2 #st3 #t1 #t2 #H >get_cost_label_append
    383 >(get_cost_label_silent_is_empty … H) //
    384 qed.
    385 
    386 lemma instr_execute_commute : ∀S1,S2 :abstract_status.
    387 ∀rel : relations S1 S2.
    388 simulation_conditions … rel →
    389 ∀s1,s1': S1.∀l.l ≠ cost_act (None ?) →  as_execute … l s1 s1' →
    390 (as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
    391 ∀s2.
    392 Srel … rel s1 s2 →
    393 ∃s2' : S2.∃tr : raw_trace … s2 s2'.silent_trace … tr ∧
    394 ∃s2'' : S2.as_execute … l s2' s2'' ∧ ∃s2''' : S2.
    395 ∃tr' : raw_trace … s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧
    396 (is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
    397 (as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
    398 #S1 #S2 #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
    399 [ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
    400   cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
    401   cases(simulate_io_out … good … prf … EQs1_io Hio_s1' … REL)
    402   #s2' * #s2'' * #t *** #sil_t #prf' #class_io #REL'
    403   %{s2} %{(t_base …)} % [ %2 % * ] %{s2'} % // %{s2''} %{t} % 
    404   [2: #_ @(head_of_premeasurable_is_not_io … t) @pre_silent_is_premeasurable
    405      assumption ] % [  %//  % // ] * #f * #l #EQ destruct
    406 | #Hclass_s1 cases(case_cl_io … (as_classify … s1'))
    407   [ #EQs1' cases(io_entering … EQs1' … prf) #l1 #EQ destruct(EQ)
    408     cases(simulate_io_in … good … prf … Hclass_s1 EQs1' …  REL) #s2' * #s2'' * #t
    409     *** #sil_t #exe #Hclass_s2'' #REL'  %{s2'} %{t} %{(or_introl … sil_t)} %{s2''}
    410     %{exe} %{s2''} %{(t_base …)} % [2: >EQs1' * #H @⊥ @H % ] %
    411      [ /4 by or_intror, conj, nmk/] * #f * #l #EQ destruct
    412   | #Hclass_s1' cases l in prf l_notau;
    413     [ #f #l #prf #_ inversion(is_call_post_label … s1)
    414       [ #Hpost cases(simulate_call_pl … good … prf … REL)
    415         [2: >Hpost % |3,4: assumption]
    416         #s2' * #s2'' * #s2''' * #t1 ** #exe #Hpost' * #t3 * * #REL #sil_t1 #sil_t3
    417         %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
    418         [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    419         % [ /4 by or_introl, conj/ ] /3 by /
    420      | #Hpost cases(simulate_call_n … good … prf … REL)
    421        [2: >Hpost % |3,4: // ] #s2' * #s2'' * #s2''' * #t1 ** #Hpost' #exe * #t3
    422        *** #REL' #sil_t1 #sil_t3 #_ %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''}
    423        %{t3} % [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    424        % [2: #_ *] % //
    425      ]
    426    | *
    427      [ #prf #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
    428        * #s2''' * #t1 * #exe * #t3 *** #REL' #sil_t1 #sil_t3 #_ %{s2'}
    429        %{t1} %{(or_introl … sil_t1)} %{s2''} %{exe} %{s2'''} %{t3} %
    430        [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    431        % [ % // % // ] * #f * #l #EQ destruct
    432      | #l #prf #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
    433        #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3
    434        %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
    435        [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    436        % [ % // % //] * #f * #l #EQ destruct
    437     ]
    438   | * [ #_ * #H @⊥ @H % ] #lab #prf #_
    439     cases(simulate_label … prf … REL) [2,3,4: // ] #s2' * #s2'' * #s2''' * #t1
    440     * #exe * #t3 ** #REL' #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe}
    441     %{s2'''} %{t3} %
    442     [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    443     % [% // % //] * #f * #l #EQ destruct
    444   ]
    445   % //
    446 ]
    447 qed.
    448 *)*)
Note: See TracChangeset for help on using the changeset viewer.