Changeset 2896 for src/RTLabs/MeasurableToStructured.ma
 Timestamp:
 Mar 16, 2013, 9:08:20 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/MeasurableToStructured.ma
r2895 r2896 45 45 ] (next_state ge s). 46 46 // 47 qed. 48 49 lemma drop_exec_ext : ∀ge,s,tr,s'. 50 eval_ext_statement ge s = return 〈tr,s'〉 → 51 eval_statement ge s = return 〈tr,Ras_state … s'〉. 52 #ge #s #tr #s' 53 whd in ⊢ (??%? → ?); 54 letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *) 55 cut (∀s',t,EV. Ras_state … (f s' t EV) = s') 56 [ // ] 57 generalize in match f; f 58 cases (eval_statement ge s) 59 [ #o #k #n #N #E whd in E:(??%%); destruct 60  * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT // 61  #m #n #N #E whd in E:(??%%); destruct 62 ] qed. 63 64 lemma as_eval_ext_statement : ∀ge,s,tr,s'. 65 eval_ext_statement ge s = Value … 〈tr,s'〉 → 66 as_execute (RTLabs_status ge) s s'. 67 #ge #s #tr #s' #EX 68 whd %{tr} %{(drop_exec_ext … EX)} 69 whd in EX:(??%?); 70 letin ns ≝ (next_state ge s) in EX; #EX 71 change with (ns s' tr ?) in match (next_state ge s s' tr ?); 72 generalize in match (drop_exec_ext ?????); 73 #EX' 74 generalize in match ns in EX ⊢ %; ns >EX' #ns whd in ⊢ (??%? → %); 75 #E destruct @e1 47 76 qed. 48 77 … … 216 245 qed. 217 246 218 lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'. 247 lemma intensional_state_change_State : ∀ge,cs,f,fs,m. 248 intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs (State f fs m) = 〈cs,[ ]〉. 249 #ge #cs #f #fs #m 250 whd in ⊢ (??%?); 251 generalize in match (cs_callee ??); 252 whd in match (cs_classify ??); cases (next_instruction f) // 253 qed. 254 255 (* TODO move*) 256 lemma All2_tail : ∀A,B,P,a,b. 257 All2 A B P a b → 258 All2 A B P (tail A a) (tail B b). 259 #A #B #P * [2: #ah #at] * [2,4: #bh #bt] 260 * // 261 qed. 262 263 lemma final_pre_S : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'. 264 eval_statement ge s = Value ??? 〈tr,s'〉 → 265 match s' with [Finalstate _ ⇒ Ras_fn_stack … s = [ ]  _ ⇒ True]. 266 #ge #s #tr #s' #EV 267 cases (extend_RTLabs_eval_statement … EV) #S * #M #EV' 268 inversion (eval_preserves_ext … (as_eval_ext_statement … EV')) 269 [ 6: #ge' #r #dst #m #M1 #M2 #E1 #E2 #E3 #E4 destruct whd % 270  *: #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 try #x15 try #x16 try #x17 try #x18 destruct // 271 ] qed. 272 273 lemma extend_RTLabs_step : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s',cs. 274 eval_statement ge s = Value … 〈tr,s'〉 → 275 All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) (Ras_fn_stack … s) cs → 276 ∃S',M'. 277 eval_ext_statement ge s = Value … 〈tr,mk_RTLabs_ext_state … s' S' M'〉 ∧ 278 All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S' (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs s')). 279 #ge #s #tr #s' #cs #EV #STACK 280 whd in match (eval_ext_statement ??); 281 letin ns ≝ (next_state ge s) 282 cut (∀s',t,EV. Ras_state … (ns s' t EV) = s' ∧ 283 match s' with 284 [ State _ _ _ ⇒ Ras_fn_stack … (ns s' t EV) = Ras_fn_stack … s 285  Callstate fid _ _ _ _ _ ⇒ ∃b. symbol_for_block … ge b = Some ? fid ∧ Ras_fn_stack … (ns s' t EV) = b::(Ras_fn_stack … s) 286  Returnstate _ _ _ _ ⇒ Ras_fn_stack … (ns s' t EV) = tail … (Ras_fn_stack … s) 287  Finalstate _ ⇒ Ras_fn_stack … (ns s' t EV) = Ras_fn_stack … s 288 ]) 289 [ #s'' #t #EV' % [ %  290 cases s'' in EV' ⊢ %; // 291 [ #fid #fn #args #ret #fs #m #EV'' 292 %{(func_block_of_exec … EV'')} % 293 [ cases (func_block_of_exec … EV'') #b * #FS #FFP 294 @(symbol_for_block_fn … FS FFP) 295  % 296 ] 297  #r #EV whd lapply (final_pre_S … EV) whd in ⊢ (% → ?); #E >E % 298 ] 299 ] 300 ] 301 generalize in match ns; ns 302 >EV #next #NEXT cases (NEXT … (refl ??)) 303 lapply (refl ? (next s' tr (refl ??))) 304 cases (next s' tr ?) in ⊢ (???% → ?); 305 #s'' #S'' #M'' 306 #Enext1 >Enext1 #Enext2 destruct #Snext %{S''} %{M''} 307 % 308 [ whd in ⊢ (??%%); >Enext1 % 309  cases s' in Snext ⊢ %; 310 [ #f #fs #m whd in ⊢ (% → ?); #E destruct 311 >intensional_state_change_State @STACK 312  #fid #fn #args #ret #fs #m whd in ⊢ (% → ?); * #b * #SYM #ES destruct 313 whd in match (intensional_state_change ???); 314 whd in match (cs_callee ???); 315 % [ @SYM  @STACK ] 316  #rv #rr #fs #m whd in ⊢ (% → ?); #ES destruct 317 whd in match (intensional_state_change ???); 318 >(?:\fst ? = tail ? cs) 319 [2: cases cs // ] 320 @All2_tail 321 @STACK 322  #r whd in ⊢ (% → ?); #E destruct 323 whd in match (intensional_state_change ???); 324 @STACK 325 ] 326 ] qed. 327 328 329 lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs,cs',itrace. 219 330 exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 → 220 ∃trace',S,M. exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉. 331 intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs trace = 〈cs',itrace〉 → 332 All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) (Ras_fn_stack … s) (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs (Ras_state … s))) → 333 ∃trace',S,M. 334 exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧ 335 All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')). 221 336 #ge #n0 elim n0 222 [ #s #trace #s' #E whd in E:(??%%); destruct %{[ ]} cases s #s' #S #M 223 %{S} %{M} % 224  #n #IH #s #trace #s' #EX 337 [ * #s #S #M #trace #s' #cs #cs' #itrace #E whd in E:(??%%); destruct 338 #E whd in E:(??%%); destruct 339 #CS %{[ ]} 340 %{S} %{M} % [ %  @CS ] 341  #n #IH * #s #S #M #trace #s' #cs #cs' #itrace #EX 225 342 cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX' 226 lapply (refl ? (eval_ext_statement ge s)) 227 whd in ⊢ (???% → ?); 228 change with (eval_statement ge s) in STEP:(??%?); 229 letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *) 230 cut (∀s',t,EV. Ras_state … (f s' t EV) = s') 231 [ // ] 232 generalize in match f; f 233 >STEP #next #NEXT whd in ⊢ (???% → ?); letin s1' ≝ (next s1 tr ?) #STEP' 234 <(NEXT … (refl ??)) in EX'; #EX' 235 cases (IH s1' … EX') 236 #tl' * #S'' * #M'' #STEPS'' 237 %{(〈s,tr〉::tl')} %{S''} %{M''} 238 whd in ⊢ (??%?); 239 change with (RTLabs_is_final s) in match (is_final ?????); 240 change with (RTLabs_is_final s) in match (is_final ?????) in NF; 241 >NF whd in ⊢ (??%?); 242 change with (eval_ext_statement ??) in match (step ?????); 243 >STEP' whd in ⊢ (??%?); 244 >STEPS'' % 245 ] qed. 343 >E whd in ⊢ (??%? → ?); @pair_elim #cs1 #itrace1 #ITOT1 344 whd in ⊢ (??%? → ?); @pair_elim #cs2 #itrace2 #ITOT2 #E' destruct 345 #STACK 346 cases (extend_RTLabs_step ge (mk_RTLabs_ext_state ge s S M) ??? STEP STACK) 347 #S' * #M' * #STEP' #STACK' 348 cases (IH (mk_RTLabs_ext_state ge s1 S' M') … EX' ITOT2 STACK') 349 #tl' * #S'' * #M'' * #EX'' #STACK'' 350 %{(〈mk_RTLabs_ext_state … s S M,tr〉::tl')} %{S''} %{M''} 351 % 352 [ whd in ⊢ (??%?); 353 change with (RTLabs_is_final s) in match (is_final ?????); 354 change with (RTLabs_is_final s) in match (is_final ?????) in NF; 355 >NF whd in ⊢ (??%?); 356 change with (eval_ext_statement ??) in match (step ?????); 357 >STEP' whd in ⊢ (??%?); 358 >EX'' % 359  @STACK'' 360 ] 361 ] qed. 362 363 lemma extend_initial_RTLabs_exec_steps : ∀p. let ge ≝ make_global p in ∀n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs',itrace. 364 exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 → 365 intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) [ ] trace = 〈cs',itrace〉 → 366 make_ext_initial_state p = OK ? s → 367 ∃trace',S,M. 368 exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧ 369 All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')). 370 #p #n #s #trace #s' #cs' #itrace #EXEC #ITOT #INIT 371 @(extend_RTLabs_exec_steps … EXEC ITOT) 372 cases (bind_inversion ????? INIT) INIT #m * #E1 #INIT 373 cases (bind_as_inversion ????? INIT) INIT #b * #Eb #INIT 374 cases (bind_as_inversion ????? INIT) INIT #f * #Ef #INIT 375 whd in INIT:(??%%); lapply (Ras_fn_match … s) destruct 376 * * #FS #FFP #_ 377 % [ >(symbol_for_block_fn … FS FFP) %  % ] 378 qed. 246 379 247 380 lemma label_to_return_state_labelled : ∀C,n,s,trace,s'. … … 304 437 lemma as_exec_eq_step : ∀ge,s1,s2,tr,s2'. 305 438 as_execute (RTLabs_status ge) s1 s2 → 306 step io_out io_in RTLabs_ext_fullexec ge s1 = Value ??? 〈tr,s2'〉 → 307 s2 = s2'. 308 #ge #s1 #s2 #tr #s2' * #tr * #EX 309 whd in ⊢ (? → ??%? → ?); 310 letin f ≝ (next_state ge s1) change with (f (Ras_state … s2) tr EX) in ⊢ (??%? → ?); 311 generalize in ⊢ (??(%???)? → ??(?%)? → ?); >EX in ⊢ (% → % → ??(match % with [_⇒?_⇒?_⇒?]?)? → ?); 312 #next #NEXT whd in ⊢ (??%? → ?); #E destruct >NEXT % 439 step io_out io_in RTLabs_fullexec ge (Ras_state … s1) = Value ??? 〈tr,s2'〉 → 440 Ras_state … s2 = s2'. 441 #ge #s1 #s2 #tr #s2' * #tr * #EX #NX 442 change with (eval_statement ge (Ras_state … s1)) in ⊢ (??%? → ?); >EX #E destruct 443 % 313 444 qed. 314 445 … … 316 447 317 448 let rec eq_end_tlr ge s trace' s' tlr s'' on tlr : 318 exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_ ext_fullexec ge s= OK ? 〈trace',s''〉 →319 s'= s'' ≝ ?449 exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 → 450 (Ras_state … s') = s'' ≝ ? 320 451 and eq_end_tll ge s trace' s' ends tll s'' on tll : 321 exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_ ext_fullexec ge s= OK ? 〈trace',s''〉 →322 s'= s'' ≝ ?452 exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 → 453 (Ras_state … s') = s'' ≝ ? 323 454 and eq_end_tal ge s trace' s' ends tal s'' on tal : 324 exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_ ext_fullexec ge s= OK ? 〈trace',s''〉 →325 s'= s'' ≝ ?.455 exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 → 456 (Ras_state … s') = s'' ≝ ?. 326 457 [ cases tlr 327 458 [ #s1 #s2 #tll @eq_end_tll … … 413 544 ] qed. 414 545 415 lemma drop_exec_ext : ∀ge,s,tr,s'.416 eval_ext_statement ge s = return 〈tr,s'〉 →417 eval_statement ge s = return 〈tr,Ras_state … s'〉.418 #ge #s #tr #s'419 whd in ⊢ (??%? → ?);420 letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *)421 cut (∀s',t,EV. Ras_state … (f s' t EV) = s')422 [ // ]423 generalize in match f; f424 cases (eval_statement ge s)425 [ #o #k #n #N #E whd in E:(??%%); destruct426  * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT //427  #m #n #N #E whd in E:(??%%); destruct428 ] qed.429 430 546 lemma RTLabs_as_label : ∀ge,s. 431 547 RTLabs_cost_label (Ras_state … s) = as_label (RTLabs_status ge) s. … … 448 564 449 565 lemma step_cost_event : ∀ge,s,tr,s',obs. 450 step … RTLabs_ ext_fullexec ge s= Value ??? 〈tr,s'〉 →566 step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 → 451 567 maybe_label ge s obs = intensional_events_of_events tr@obs. 452 568 #ge #s #tr #s' #obs #ST 453 cases (only_plain_step_events_is_one_cost … (drop_exec_ext … ST))569 cases (only_plain_step_events_is_one_cost … ST) 454 570 [ * #cl * #E1 #CS whd in ⊢ (??%?); 455 571 <RTLabs_as_label >CS destruct % … … 470 586 471 587 lemma call_ret_event : ∀ge,s,tr,s',obs. 472 step … RTLabs_ ext_fullexec ge s= Value ??? 〈tr,s'〉 →588 step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 → 473 589 (as_classify (RTLabs_status ge) s = cl_call ∨ as_classify (RTLabs_status ge) s = cl_return) → 474 590 maybe_label ge s obs = obs ∧ tr = [ ]. … … 482 598 [ 1,3: // ] #CS % 483 599 [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ] 484 lapply (drop_exec_ext … ST)600 lapply ST 485 601 whd in ⊢ (??%? → ?); 486 602 [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?); … … 493 609 [ 1,3: // ] #CS % 494 610 [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ] 495 lapply (drop_exec_ext … ST)611 lapply ST 496 612 whd in ⊢ (??%? → ?); 497 613 [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct % … … 502 618 503 619 lemma as_call_cs_callee : ∀ge,s,CL,CL'. 504 as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_ ext_pcsys ge) sCL'.620 as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_pcsys ge) (Ras_state … s) CL'. 505 621 #ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E 506 622 destruct % … … 514 630 intensional_trace_of_trace C (cs_callee C s CL :: cs) rem = 〈cs',trace'〉. 515 631 #C #cs #s #rem #cs' #trace #CL 516 whd in ⊢ (??%? → ?); 632 whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???); 517 633 @generalize_callee cases (cs_classify C s) in CL ⊢ %; * 518 634 #name whd in ⊢ (??%? → ?); cases (intensional_trace_of_trace C (name I::cs) rem) … … 522 638 lemma itot_step : ∀ge,cs,s,tr,s',rem,cs',obs. 523 639 as_classifier (RTLabs_status ge) s cl_other → 524 step … RTLabs_ ext_pcsys ge s= Value ??? 〈tr,s'〉 →525 intensional_trace_of_trace (pcs_to_cs … RTLabs_ ext_pcsys ge) cs (〈s,tr〉::rem) = 〈cs',obs〉 →640 step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 → 641 intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs (〈Ras_state … s,tr〉::rem) = 〈cs',obs〉 → 526 642 ∃obs'. 527 643 obs = (intensional_events_of_events tr) @ obs' ∧ 528 intensional_trace_of_trace (pcs_to_cs … RTLabs_ ext_pcsys ge) cs rem = 〈cs',obs'〉.644 intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs rem = 〈cs',obs'〉. 529 645 #ge #cs #s #tr #s' #rem #cs #obs #CL #EX 530 whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (% → ?); 531 whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_ext_pcsys ge) ?) in CL:(??%?); 646 whd in ⊢ (??%? → ?); 647 whd in match (intensional_state_change (pcs_to_cs RTLabs_pcsys ge) ??); 648 generalize in match (cs_callee ??) in ⊢ (% → ?); 649 whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_pcsys ge) ?) in CL:(??%?); 532 650 >CL #name whd in ⊢ (??%? → ?); 533 651 cases (intensional_trace_of_trace ???) #cs'' #trace'' #E whd in E:(??%?); destruct … … 539 657 events from the structured trace *) 540 658 let rec eq_obs_tlr ge s trace' s' tlr fn cs cs' obs on tlr : 541 exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_ ext_fullexec ge s = OK ? 〈trace',s'〉 →542 intensional_trace_of_trace (pcs_to_cs RTLabs_ ext_pcsys ge) (fn::cs) trace' = 〈cs',obs〉 →659 exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',Ras_state … s'〉 → 660 intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace' = 〈cs',obs〉 → 543 661 pi1 … (observables_trace_label_return (RTLabs_status ge) s s' tlr fn) = obs ∧ cs = cs' ≝ ? 544 662 and eq_obs_tll ge s trace1 s' ends tll fn cs cs' obs on tll : 545 exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_ ext_fullexec ge s = OK ? 〈trace1,s'〉 →546 intensional_trace_of_trace (pcs_to_cs RTLabs_ ext_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →663 exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 → 664 intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 → 547 665 pi1 … (observables_trace_label_label (RTLabs_status ge) ends s s' tll fn) = obs ∧ cs_change ends fn cs cs' ≝ ? 548 666 and eq_obs_tal ge s trace1 s' ends tal fn cs cs' obs on tal : 549 exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_ ext_fullexec ge s = OK ? 〈trace1,s'〉 →550 intensional_trace_of_trace (pcs_to_cs RTLabs_ ext_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 →667 exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 → 668 intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 → 551 669 maybe_label ge s (pi1 … (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn)) = obs ∧ cs_change ends fn cs cs' ≝ ?. 552 670 [ cases tlr … … 566 684 cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX 567 685 whd in EX:(??%?); destruct 568 whd in CL; change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ?) in CL:(??%?); 569 whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (??%? → ?); 686 whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ?) in CL:(??%?); 687 whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???); 688 generalize in match (cs_callee ??) in ⊢ (??%? → ?); 570 689 whd in ⊢ (? → ? → ?(??(???%)?)?); 571 690 >CL #call whd in ⊢ (??%? → ?); #E destruct … … 574 693 cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX 575 694 whd in EX:(??%?); destruct 576 whd in CL; change with (cs_classify (pcs_to_cs RTLabs_ext_pcsys ge) ?) in CL:(??%?); 577 whd in ⊢ (??%? → ?); generalize in match (cs_callee ??) in ⊢ (??%? → ?); 695 whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ?) in CL:(??%?); 696 whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???); 697 generalize in match (cs_callee ??) in ⊢ (??%? → ?); 578 698 whd in ⊢ (? → ? → ?(??(???%)?)?); >CL #call whd in ⊢ (??%? → ?); #E destruct 579 699 cases (call_ret_event … ST') … … 586 706 whd in EX:(??%?); destruct cases (call_ret_event … ST') 587 707 [ #E1 #E2 >E1 >E2  skip  %1 @CL ] #ITOT 588 cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_ ext_pcsys ge) ? = ?) in CL; >CL % ]708 cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ? = ?) in CL; >CL % ] 589 709 #obs' * #E3 #ITOT' 590 710 <(as_exec_eq_step … ST ST') in EX; #EX … … 599 719 cases (call_ret_event … ST') 600 720 [ #E2 #E3 >E2 >E3  skip  %1 @CL ] #ITOT 601 cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_ ext_pcsys ge) ? = ?) in CL; >CL % ]721 cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ? = ?) in CL; >CL % ] 602 722 #obs' * #E4 #ITOT' 603 723 <(as_exec_eq_step … ST ST') in EX; #EX … … 649 769 ] qed. 650 770 771 lemma cost_state_intensional_state_change : ∀ge,s,cs. 772 RTLabs_cost s → 773 \fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs s) = cs. 774 #ge * 775 [ #f #fs #m #cs // 776  #fid #fn #args #ret #fs #m #cs * 777  #rv #rr #fs #m #cs * 778  #r #cs * 779 ] qed. 780 781 651 782 652 783 (* I'm not entirely certain that existentially quantifying fn is the right thing … … 676 807 whd in ⊢ (??%? → ?); >EXEC1 677 808 whd in ⊢ (??%? → ?); >EXEC2 678 whd in ⊢ (??%? → ?); @breakup_pair #E whd in E:(??%%); destruct 809 whd in ⊢ (??%? → ?); 810 @pair_elim #cs1 #prefix1 #ITOT1 811 lapply (refl ? (intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ?) cs1 interesting')) 812 cases (intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ?) cs1 interesting') in ⊢ (???% → %); 813 #cs2 #interesting'' #ITOT2 814 #E whd in E:(??%%); destruct 679 815 cases (initial_states_OK' … INIT) #S * #M #INIT' 680 cases (extend_ RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1)681 #prefix'' * #S1 * #M1 816 cases (extend_initial_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1 ITOT1 INIT') 817 #prefix'' * #S1 * #M1 * 682 818 lapply (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) #CS1 683 819 lapply (cost_state_is_in_function ge s1 S1 M1 CS1) * #fnb * #S1' * #fn * #ES1 #FN destruct 684 letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1' 820 letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1' #CALLSTACK1 821 cut (∃cs1'. cs1 = fn::cs1') 822 [ >(cost_state_intensional_state_change … CS1) in CALLSTACK1; 823 cases cs1 [ * ] #fn' #cs1' * >FN #Efn destruct #_ %{cs1'} % 824 ] * #cs1' #Ecs destruct 685 825 cases (will_return_equiv … EXEC2 RETURNS) #RETURNS' #RETURNS_END 686 826 lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????) … … 712 852 <plus_n_O @(λx.x) ] 713 853 #LEN' <LEN' in EXEC2; #EXEC2 714 cases (extend_RTLabs_exec_steps ?? s1' … EXEC2) #interesting'''715 lapply (eq_obs_tlr ????????? EXEC2)854 lapply (eq_obs_tlr ????????? EXEC2 ITOT2) 855 * // 716 856 ] 717 857 ]]
Note: See TracChangeset
for help on using the changeset viewer.