Changeset 3389
 Timestamp:
 Oct 10, 2013, 1:07:28 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Simulation.ma
r3388 r3389 60 60 ∃s2',s2'',s2'''. 61 61 ∃t1: raw_trace S s2 s2'. 62 as_execute … (call_act f l) s2' s2'' ∧ 62 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 ∧ 63 65 ∃t3: raw_trace S s2'' s2'''. 64 66 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 … … 67 69 ∀s1,s2,s1' : S. 68 70 as_execute … (ret_act (None ?)) s1 s1' → 69 Srel … rel s1 s2 → 71 Srel … rel s1 s2 → as_classify … s2 ≠ cl_io ∧ 70 72 ∃s2',s2'',s2'''. 71 73 ∃t1: raw_trace S s2 s2'. 72 as_execute … (ret_act (None ?)) s2' s2'' ∧ 74 as_execute … (ret_act (None ?)) s2' s2'' ∧ as_classify … s2' ≠ cl_jump ∧ 75 as_classify … s2'' ≠ cl_io ∧ 73 76 ∃t3: raw_trace S s2'' s2'''. 74 77 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3 75 ∧ Rrel … rel s 2s2''78 ∧ Rrel … rel s1' s2'' 76 79 }. 77 80 … … 113 116 qed. 114 117 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 120 → pre_measurable_trace … t. 121 #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' 126 #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption  whd %{(None ?)} % ] 127 @IH [ >Hst2' % #EQ destruct  assumption] 128 qed. 129 130 lemma append_tind_commute : ∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l. 131 ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3. 132 ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2. 133 #S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed. 134 135 lemma append_silent_premeasurable : ∀S : abstract_status. 136 ∀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 → 138 pre_measurable_trace … (t' @ t). 139 #S #st1' #st1 #st2 #t #t' #Ht' lapply t t elim Ht' 140 [ normalize #st #Hst #r #H1 #H2 @pre_silent_is_premeasurable assumption 141 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 ] 143 try ( %{x} %) try @IH try assumption % ] 144 #s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1' 145 #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 151 try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption 152 qed. 153 154 155 115 156 definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2. 116 157 raw_trace S st1 st2 → bool ≝ … … 133 174 qed. 134 175 176 lemma well_formed_append : ∀S : abstract_status. 177 ∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. 178 well_formed_trace … (t1 @ t2) → well_formed_trace … t1 ∧ well_formed_trace … t2. 179 #S #st1 #st2 #st3 #t1 #t2 #H % 180 [ lapply H H lapply t2 t2 elim t1 [ //] #st1' #st2' #st3' #l #exe #tl #IH #r 181 #H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 normalize in EQ3; destruct ] 182 #st1'' #st2'' #st3'' #l' #prf' #tl' #wf_tl' [#Hst1''  * #x #EQ destruct] #_ 183 #EQ1 #EQ2 normalize in ⊢ (% → ?); #EQ3 destruct #_ 184 [ %2 [ @IH assumption ] assumption  %3 [ @IH assumption ] %{x} % ] 185 ] 186 lapply H lapply t2 t2 elim t1 [ #st #r normalize //] 187 #s1 #s2 #s3 #l #prf #tl #IH #r #H inversion H in ⊢ ?; 188 [ #st #EQ1 #EQ2 normalize #EQ3 destruct ] 189 #s1' #s2' #s3' #l' #prf' #tl' #wf_tl' #Hs1' #_ normalize #EQ1 #EQ2 #EQ3 destruct 190 #_ @IH assumption 191 qed. 192 193 194 lemma append_well_formed : ∀S : abstract_status. 195 ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. 196 well_formed_trace … t1 → well_formed_trace … t2 → well_formed_trace … (t1 @ t2). 197 #S #st1 #st2 #st3 #t1 #t2 #H lapply t2 t2 elim H 198 [ #st #r #H1 @H1 ] 199 #s1 #s2 #s3 #l #prf #tl #wf_tl #Hs1 #IH #r #wf_r normalize [ %2  %3] 200 try @IH assumption 201 qed. 202 203 lemma silent_is_well_formed : ∀S : abstract_status. 204 ∀st1,st2 : S.∀t : raw_trace … st1 st2.silent_trace … t → well_formed_trace … t. 205 #S #st1 #st2 #t elim t [ #st #_ %] 206 #s1 #s2 #s3 #l #prf #tl #IH * #H inversion H [ #st #EQ1 #EQ2 #EQ3 destruct] 207 #s1' #s2' #s3' #prf' #tl' #Hs2' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #_ #H1 %2 208 [ @IH % [2: #_ ] assumption  >(H1 I) % #EQ destruct] 209 qed. 210 211 135 212 lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status. 136 213 ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. … … 144 221 qed. 145 222 223 lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S. 224 ∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3. 225 get_costlabels_of_trace … (t1 @ t2) = 226 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2). 227 #S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' * 228 [#f * #l  * [ * #l]  * [ #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH 229 qed. 230 146 231 (* 147 232 lemma raw_trace_ind_r : ∀S : abstract_status. … … 318 403 ] 319 404 ] 320  cases daemon (*TODO*) 405  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 * 406 #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct 407 #IH1 #IH2 #wf_all #st1' #Hst1' #REL 408 cases(simulate_call_n … good … exe_12 … Hst1 … REL) 409 #st1'' * #st1''' * #st2' * #tr1 **** #nps_st1'' #exe_12' #Hst1'' #Hst1''' * #tr2 *** #REL1 #sil_tr1 410 #sil_tr2 #call_rel cases(IH1 … REL1) 411 [2: inversion wf_all [ #st #EQ1 #EQ2 #EQ3 destruct] 412 #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1  * #y1 #EQ destruct(EQ) ] #_ 413 #EQ1 #EQ2 #EQ3 destruct #_ @(proj1 … (well_formed_append … wf_tl)) 414 3: @(silent_io … (proj1 … sil_tr2)) assumption 415 ] 416 #st3' * #tr3 *** #pre_tr3 #wf_tr3 #EQcost_tr3 #REL2 417 cases(simulate_ret_n … good … exe_34 … REL2) #Hst3' * #st3'' * #st4' * #st4'' * 418 #tr4 *** #exe_34' #Hst3'' #Hst4' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) 419 [2: inversion wf_all in ⊢ ?; [#st #EQ1 #EQ2 destruct whd in ⊢ (????% → ?); #EQ destruct] 420 #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1  * #y1 #EQ destruct(EQ)] #_ 421 #EQ1 #EQ2 #EQ3 destruct #_ cases(well_formed_append … wf_tl) wf_tl wf_all 422 #_ #H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct] 423 #z1 #z2 #z3 #w #prf' #tl' #wf_tl' [ #Hz1  * #w1 #EQ destruct(EQ)] #_ 424 #EQ1 #EQ2 #EQ3 destruct #_ assumption 425 3: @(silent_io … (proj1 … sil_tr5)) assumption 426 ] 427 #st5' * #tr6 *** #pre_tr6 #wf_tr6 #EQcost_tr6 #REL4 %{st5'} 428 %{(tr1 @ (t_ind … exe_12' … ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))} 429 % [2: assumption] % 430 [ % 431 [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_tr1) ] 432 %5 433 [ @(silent_io … (proj1 … sil_tr1)) assumption 434  @(silent_io … (proj1 … sil_tr4)) assumption 435  whd %{f} %{l} % 436  assumption 437  @append_premeasurable_silent try assumption [2: @(proj1 … sil_tr2)] 438 @append_silent_premeasurable try assumption @(proj1 … sil_tr4) 439  @append_premeasurable_silent try assumption @(proj1 … sil_tr5) 440  @(RET_REL … call_rel) assumption 441  % 442 ] 443  @append_well_formed_silent [2: @(proj1 … sil_tr1) 3: @(proj2 … sil_tr1) ] 444 %2 [2: assumption] >append_associative @append_well_formed_silent 445 [2: @(proj1 … sil_tr2) 3: @(proj2 … sil_tr2) ] @append_well_formed 446 [ @append_well_formed try assumption @silent_is_well_formed assumption ] 447 %2 [2: assumption] @append_well_formed try assumption @silent_is_well_formed 448 assumption 449 ] 450  >get_cost_label_invariant_for_append_silent_trace_l [2: @(proj1 … sil_tr1) ] 451 whd in ⊢ (??%%); @eq_f >append_associative 452 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 453 [2: @(proj1 … sil_tr2) ] >append_associative 454 >get_cost_label_append in ⊢ (???%); 455 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 456 [2: @(proj1 … sil_tr4) ] normalize 457 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 458 [2: @(proj1 … sil_tr5) ] >get_cost_label_append in ⊢ (??%?); @eq_f2 459 assumption 460 ] 321 461 ] 322 qed. 323 324 325 326 #st3 #l #class_st1 #exe #tl * #x #EQ destruct(EQ) #pre_tl #IH 327 #well_formed #s2 #class_s2 #REL cases(simulate_ret_l … good … exe … REL) 328 #s2'' * #s2''' * #s2'''' * #t1 * #exe' * #t2 ** #Rs2s2'''' #t1_sil #t2_sil 329 xxxxxxxxx 330 331 332 #st4 #st5 #l1 #l2 * #x #EQ whd in ⊢ (% → ?); 333 @append_premeasurable_silent 334 335 xxxxxxxxxxxxxx 336 ] 337 *: cases daemon (*TODO*) 338 ] 339 qed.*) 462 qed. 463 464 xxxxx 465 340 466 341 467 (* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio … … 402 528 ∀t : LR_raw_trace S. 403 529 ∀rel : relations S. 530 simulation_conditions … rel → 404 531 measurable S t → 405 ∀s1' .Srel … rel (LR_s1 … t) s1' →532 ∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' → 406 533 ∃ t' : LR_raw_trace S. 407 534 measurable S t' ∧ … … 417 544 ∧ 418 545 get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t'). 419 cases daemon (*TODO*) 546 #S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL 547 cases(simulates_pre_mesurable … (LR_t … t) … REL) 548 [2: @good 3: @pre_t 4: @wf_t 5: @Hs1' ] 549 #s2 * #t2 *** #pre_t2 #wf_t2 #EQcost #REL1 550 inversion(as_initial … (LR_s1 … t)) #Has_initial 551 inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry 552 inversion(as_final … (LR_s2 … t)) #Has_final 553 inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit 554 normalize nodelta 555 [ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2: 556 557 558 420 559 qed. 421 560
Note: See TracChangeset
for help on using the changeset viewer.