Changeset 3524 for LTS/Simulation.ma
 Timestamp:
 Mar 11, 2015, 4:26:40 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Simulation.ma
r3523 r3524 1 1 include "Traces.ma". 2 include "basics/jmeq.ma". 3 4 discriminator option. 2 5 3 6 record relations (S1,S2 : abstract_status) : Type[0] ≝ … … 94 97 }. 95 98 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 235 100 theorem simulates_pre_mesurable: 236 101 ∀S1,S2 : abstract_status.∀rel : relations S1 S2. … … 243 108 pre_measurable_trace … t2 ∧ 244 109 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) 260 155 [2,3: /2/] 261 156 #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2'''' 262 157 #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/ 267 170 [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2'' 268 171 [ #H31 #H32 #H33 #H34 #H35 destruct assumption ] … … 273 176 [2: assumption] whd in ⊢ (???%); 274 177 >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 ] 278 187  #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ) 279 #pre_meas_tl #IH #s 2#class_s2 #RELst1s2280 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/ ] 281 190 #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2''' 282 191 #sil_t1 #sil_t2 cases(IH … rel_s2_s2''') 283 192 [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 ⊢ (??%?); 287 205 >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1) 288 206 whd in ⊢ (???%); … … 295 213 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65 296 214 #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 ] 297 222  #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct 298 223 #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') 300 225 [2,3: /2 by head_of_premeasurable_is_not_io/ ] 301 226 #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2 302 227 cases(IH … REL) 303 228 [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] % 306 240 [2: whd in ⊢ (??%?); 307 241 >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1) … … 317 251  @append_premeasurable_silent // % assumption 318 252 ] 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 * 320 261 #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/ ] 322 263 #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1 323 264 #sil_tr2 #call_rel cases(IH1 … REL1) 324 265 [2: /2 by pre_silent_io/ ] 325 #st3' * #tr3 ** #pre_tr3 #EQcost_tr3 #REL2326 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/ ] 327 268 #st3'' * #st4' * #st4'' * 328 269 #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'} 330 271 %{(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] % 332 282 [ @append_premeasurable_silent try assumption %5 333 283 [1,2: /2 by pre_silent_io/ … … 356 306 ] 357 307 % // 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 ] 358 338 ] 359 339 qed. 360 340 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 // 341 theorem 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' 362 cases(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/ 376 368 qed. 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_append383 >(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_premeasurable405 assumption ] % [ %// % // ] * #f * #l #EQ destruct406  #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'' * #t409 *** #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 destruct412  #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_t3417 %{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 * #t3422 *** #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 destruct432  #l #prf #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]433 #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3434 %{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 destruct437 ]438  * [ #_ * #H @⊥ @H % ] #lab #prf #_439 cases(simulate_label … prf … REL) [2,3,4: // ] #s2' * #s2'' * #s2''' * #t1440 * #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 destruct444 ]445 % //446 ]447 qed.448 *)*)
Note: See TracChangeset
for help on using the changeset viewer.