Changeset 3391
- Timestamp:
- Oct 10, 2013, 5:28:33 PM (7 years ago)
- Location:
- LTS
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Simulation.ma
r3390 r3391 14 14 ∀s1,s2,s1' : S. 15 15 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 → 17 17 ∃s2'. ∃t: raw_trace S s2 s2'. 18 18 Srel … rel s1' s2' ∧ silent_trace … t … … 20 20 ∀s1,s2,l,s1'. 21 21 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 → 23 23 Srel … rel s1 s2 → 24 24 ∃s2',s2'',s2'''. 25 25 ∃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'' ∧ 27 27 ∃t3: raw_trace S s2'' s2'''. 28 28 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 … … 31 31 is_call_post_label … s1 → 32 32 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 → 34 34 Srel … rel s1 s2 → 35 35 ∃s2',s2'',s2'''. 36 36 ∃t1: raw_trace S s2 s2'. 37 as_classify … s2' ≠ cl_jump ∧38 37 as_execute … (call_act f l) s2' s2'' ∧ 39 38 bool_to_Prop(is_call_post_label … s2') ∧ 40 as_classify … s2'' ≠ cl_io ∧41 39 ∃t3: raw_trace S s2'' s2'''. 42 40 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 … … 44 42 ∀s1,s2,s1' : S.∀l. 45 43 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 → 47 45 Srel … rel s1 s2 → 48 46 ∃s2',s2'',s2'''. 49 47 ∃t1: raw_trace S s2 s2'. 50 as_classify … s2' ≠ cl_jump ∧51 48 as_execute … (ret_act (Some ? l)) s2' s2'' ∧ 52 as_classify … s2'' ≠ cl_io ∧53 49 ∃t3: raw_trace S s2'' s2'''. 54 50 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 … … 57 53 as_execute … (call_act f l) s1 s1' → 58 54 ¬ is_call_post_label … s1 → 55 as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → 59 56 Srel … rel s1 s2 → 60 57 ∃s2',s2'',s2'''. 61 58 ∃t1: raw_trace S s2 s2'. 62 59 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'' ∧ 65 61 ∃t3: raw_trace S s2'' s2'''. 66 62 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 … … 69 65 ∀s1,s2,s1' : S. 70 66 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 → 72 69 ∃s2',s2'',s2'''. 73 70 ∃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'' ∧ 76 72 ∃t3: raw_trace S s2'' s2'''. 77 73 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 … … 102 98 lemma append_premeasurable_silent : ∀S : abstract_status. 103 99 ∀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 →100 pre_measurable_trace … t → silent_trace … t' → 105 101 pre_measurable_trace … (t' @ t). 106 102 #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] 108 104 #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] 110 106 #s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3 111 destruct #_ #Hs1'whd in ⊢ (????%); %2107 destruct #_ whd in ⊢ (????%); %2 112 108 [ assumption 113 109 | %{(None ?)} % … … 116 112 qed. 117 113 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 … t114 lemma silent_is_premeasurable : ∀S : abstract_status. 115 ∀st1,st2 : S. ∀t : raw_trace S st1 st2.silent_trace … t 120 116 → pre_measurable_trace … t. 121 117 #S #st1 #st2 #t elim t 122 [ #st #H st #H inversion H in ⊢ ?; [ #st'#EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]123 124 -t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H st1 #Hinversion 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' 126 122 #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ] 127 123 @IH assumption … … 135 131 lemma append_silent_premeasurable : ∀S : abstract_status. 136 132 ∀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 →133 pre_measurable_trace … t' → silent_trace … t → 138 134 pre_measurable_trace … (t' @ t). 139 135 #S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht' 140 [ normalize #st #Hst #r #H1 #H2 @pre_silent_is_premeasurable assumption136 [ normalize #st #Hst #r #H1 @silent_is_premeasurable assumption 141 137 |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 ] 143 139 try ( %{x} %) try @IH try assumption % ] 144 140 #s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1' 145 141 #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 151 145 try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption 152 146 qed. 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 ].159 147 160 148 (* … … 175 163 qed.*) 176 164 165 (* 177 166 lemma well_formed_append : ∀S : abstract_status. 178 167 ∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. … … 210 199 qed. 211 200 *) 212 201 *) 213 202 lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status. 214 203 ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. 215 pre_silent_trace … t1 →204 silent_trace … t1 → 216 205 get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2. 217 206 #S #st1 #st2 #st3 #t1 elim t1 218 207 [#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 #H 219 inversion H in ⊢ ?; [ #st # EQ1 #EQ2 #EQ3 destruct]208 inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct] 220 209 #st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct 221 210 #_ whd in ⊢ (??%?); >IH [%] assumption … … 242 231 *) 243 232 233 lemma head_of_premeasurable_is_not_io : ∀S : abstract_status. 234 ∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t → 235 as_classify … st1 ≠ cl_io. 236 #S #st1 #st2 #t #H inversion H // 237 qed. 238 244 239 245 240 theorem simulates_pre_mesurable: … … 248 243 simulation_conditions S rel → 249 244 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 → 252 247 ∃s2'. ∃t2: raw_trace … s2 s2'. 253 248 pre_measurable_trace … t2 ∧ 254 well_formed_trace … t2 ∧255 249 get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧ 256 250 Srel … rel s1' s2'. 257 251 #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/ 260 254 | #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/ 284 261 | 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} 307 266 %{(t_s2'' @ (t_ind … exe_s2''' …))} [ @(t_s2'''' @ t_s3) ] % [2: assumption] 308 267 % 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/ 322 269 | 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 // 326 272 ] 327 273 ] 328 274 | #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 346 281 %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] 347 282 % [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) 349 284 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) 351 286 @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} 379 296 %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] % 380 297 [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) 382 299 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) 384 301 @eq_f assumption ] 385 % 386 [ @append_premeasurable_silent try assumption [2: @(proj1 … (proj1 … sil_t1))] 302 @append_premeasurable_silent try assumption 387 303 %4 try assumption 388 [ @(silent_io … (proj1 … (proj1 … sil_t1))) assumption304 [ /2 by silent_io/ 389 305 | whd %{f} %{lab} % 390 | @append_premeasurable_silent try assumption @(proj1 … (proj1 … sil_t2))306 | /2 by append_premeasurable_silent/ 391 307 ] 392 | @append_well_formed [ @(proj2 … sil_t1) ]393 %2 try assumption @append_well_formed try assumption @(proj2 … sil_t2)394 ]395 308 | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 * 396 309 #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 400 312 #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'} 418 319 %{(tr1 @ (t_ind … exe_12' … ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))} 419 320 % [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/ 425 323 | whd %{f} %{l} % 426 324 | 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 430 328 | @(RET_REL … call_rel) assumption 431 329 | % 432 330 ] 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: // ] 441 332 whd in ⊢ (??%%); @eq_f >append_associative 442 333 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 443 [2: @(proj1 … (proj1 … sil_tr2))] >append_associative334 [2: // ] >append_associative 444 335 >get_cost_label_append in ⊢ (???%); 445 336 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 446 [2: @(proj1 … (proj1 … sil_tr4))] normalize337 [2: //] normalize 447 338 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 448 [2: @(proj1 … (proj1 … sil_tr5))] >get_cost_label_append in ⊢ (??%?); @eq_f2339 [2: // ] >get_cost_label_append in ⊢ (??%?); @eq_f2 449 340 assumption 450 341 ] -
LTS/Traces.ma
r3390 r3391 65 65 | cl_other : status_class. 66 66 67 definition is_non_silent_cost_act : ActionLabel → Prop ≝ 68 λact. ∃l. act = cost_act (Some ? l). 69 67 70 record abstract_status : Type[2] ≝ 68 71 { as_status :> Type[0] … … 75 78 ; is_io_entering : NonFunctionalLabel → bool 76 79 ; 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 77 83 }. 78 84 … … 118 124 λact.act = ret_act (None ?). 119 125 120 definition is_non_silent_cost_act : ActionLabel → Prop ≝121 λact. ∃l. act = cost_act (Some ? l).122 123 126 definition is_costlabelled_act : ActionLabel → Prop ≝ 124 127 λact.match act with [ call_act _ _ ⇒ True … … 127 130 | init_act ⇒ False 128 131 ]. 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 (* 146 133 lemma well_formed_trace_inv : 147 134 ∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2. … … 167 154 qed. 168 155 156 *) 169 157 170 158 let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S) … … 194 182 λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1. 195 183 196 inductive pre_silent_trace (S : abstract_status) :184 inductive silent_trace (S : abstract_status) : 197 185 ∀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) 199 187 | silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2. 200 ∀tl : raw_trace S st2 st3. as_classify … st 2 ≠ 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). 202 190 203 191 lemma 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 → 205 193 as_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 // 209 196 #st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct 210 #EQ destruct #_ #Hclass' @IH [ assumption ]assumption197 #EQ destruct #_ @IH assumption 211 198 qed. 212 199 … … 214 201 raw_trace S st1 st2 → bool ≝ 215 202 λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ]. 216 203 (* 217 204 definition silent_trace : ∀S : abstract_status.∀st1,st2 : S. 218 205 raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧ 219 (is_trace_non_empty … t → as_classify … st1 ≠ cl_io) ∧220 206 well_formed_trace … t. 221 207 … … 223 209 ∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t. 224 210 #S #st1 #st2 #t * // 225 qed. 211 qed. *) 226 212 (* elim t -t 227 213 [ #st #_ %]
Note: See TracChangeset
for help on using the changeset viewer.