Changeset 2668 for src/common/SmallstepExec.ma
 Timestamp:
 Feb 15, 2013, 11:27:56 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/SmallstepExec.ma
r2618 r2668 183 183 lemma after_1_of_n_steps : ∀n,O,I,exec,g,inv,P,s. 184 184 after_n_steps (S n) O I exec g s inv P → 185 ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧ 185 ∃tr,s'. 186 is_final … exec g s = None ? ∧ 187 step … exec g s = Value … 〈tr,s'〉 ∧ 186 188 bool_to_Prop (inv s') ∧ 187 189 after_n_steps n O I exec g s' inv (λtr'',s''. P (tr⧺tr'') s''). … … 193 195 [ #o #k * 194 196  * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr) #AFTER 195 %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % / 2/ cases AFTER197 %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % /3/ cases AFTER 196 198  #m * 197 199 ] … … 201 203 lemma after_1_step : ∀O,I,exec,g,inv,P,s. 202 204 after_n_steps 1 O I exec g s inv P → 203 ∃tr,s'. step ?? exec g s = Value … 〈tr,s'〉 ∧ bool_to_Prop (inv s') ∧ P tr s'. 205 ∃tr,s'. is_final … exec g s = None ? ∧ 206 step ?? exec g s = Value … 〈tr,s'〉 ∧ 207 bool_to_Prop (inv s') ∧ P tr s'. 204 208 #O #I #exec #g #inv #P #s #AFTER 205 209 cases (after_1_of_n_steps … AFTER) 206 #tr * #s' * * #STEP #INV #FIN %{tr} %{s'} % [%] // whd in FIN; >E0_right in FIN; //210 #tr * #s' * * * #NF #STEP #INV #FIN %{tr} %{s'} % [%[%]] // whd in FIN; >E0_right in FIN; // 207 211 qed. 208 212 … … 377 381 ]. 378 382 379 383 (* For now I'm doing this without I/O, to keep things simple. In the place I 384 intend to use it (the definition of measurable subtraces, and proofs using 385 that) I should allow I/O for the prefix. *) 386 387 let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (trace × (state … fx g)) × (state … fx g)) ≝ 388 match n with 389 [ O ⇒ return 〈[ ], s〉 390  S m ⇒ 391 match is_final … fx g s with 392 [ Some r ⇒ Error … (msg TerminatedEarly) 393  None ⇒ 394 match step … fx g s with 395 [ Value trs ⇒ 396 ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs); 397 return 〈trs::tl, s'〉 398  Interact _ _ ⇒ Error … (msg UnexpectedIO) 399  Wrong m ⇒ Error … m 400 ] 401 ] 402 ]. 403 404 (* Show that it's nice. *) 405 406 lemma exec_steps_S : ∀O,I,fx,g,n,s,trace,s''. 407 exec_steps (S n) O I fx g s = OK … 〈trace,s''〉 → 408 is_final … fx g s = None ? ∧ 409 ∃tr',s',tl. 410 trace = 〈tr',s'〉::tl ∧ 411 step … fx g s = Value … 〈tr',s'〉 ∧ 412 exec_steps n O I fx g s' = OK … 〈tl,s''〉. 413 #O #I #fx #g #n #s #trace #s'' 414 whd in ⊢ (??%? → ?); 415 cases (is_final … s) 416 [ whd in ⊢ (??%? → ?); 417 cases (step … s) 418 [ #o #i #EX whd in EX:(??%?); destruct 419  * #tr' #s' whd in ⊢ (??%? → ?); #EX %{(refl ??)} 420 %{tr'} %{s'} cases (exec_steps … g s') in EX ⊢ %; 421 [ * #tl #s'' #EX whd in EX:(??%?); destruct %{tl} /3/ 422  #m #EX whd in EX:(??%?); destruct 423 ] 424  #m #EX whd in EX:(??%?); destruct 425 ] 426  #r #EX whd in EX:(??%?); destruct 427 ] qed. 428 429 lemma exec_steps_length : ∀O,I,fx,g,n,s,trace,s'. 430 exec_steps n O I fx g s = OK … 〈trace,s'〉 → 431 n = trace. 432 #O #I #fx #g #n elim n 433 [ #s #trace #s' #EX whd in EX:(??%?); destruct % 434  #m #IH #s #trace #s' #EX 435 cases (exec_steps_S … EX) #notfinal * #tr' * #s'' * #tl * * #Etl #Estep #steps 436 >(IH … steps) >Etl % 437 ] qed. 438 439 lemma exec_steps_nonterm : ∀O,I,fx,g,n,s,h,t,s'. 440 exec_steps n O I fx g s = OK … 〈h::t,s'〉 → 441 is_final … s = None ?. 442 #O #I #fx #g #n #s #h #t #s' #EX 443 lapply (exec_steps_length … EX) 444 #Elen destruct whd in EX:(??%?); 445 cases (is_final … s) in EX ⊢ %; 446 [ // 447  #r #EX whd in EX:(??%?); destruct 448 ] qed. 449 450 lemma exec_steps_nonterm' : ∀O,I,fx,g,n,s,h,t,s'. 451 exec_steps n O I fx g s = OK … 〈h@[t], s'〉 → 452 is_final … s = None ?. 453 #O #I #fx #g #n #s * [2: #h1 #h2] #t #s' @exec_steps_nonterm 454 qed. 455 456 let rec gather_trace S (l:list (trace × S)) on l : trace ≝ 457 match l with 458 [ nil ⇒ E0 459  cons h t ⇒ (\fst h)⧺(gather_trace S t) 460 ]. 461 462 lemma exec_steps_after_n_simple : ∀n,O,I,fx,g,s,trace,s'. 463 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 464 after_n_steps n O I fx g s (λ_. true) (λtr,s''. 〈tr,s''〉 = 〈gather_trace ? trace,s'〉). 465 #n elim n 466 [ #O #I #fx #g #s #trace #s' #EXEC whd in EXEC:(??%?); destruct 467 whd % 468  #m #IH #O #I #fx #g #s #trace #s' #EXEC 469 cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS 470 @(after_n_m 1 … (IH … STEPS)) 471 whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #E destruct % 472 ] qed. 473 474 lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P. 475 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 476 all … (λts. inv (\snd ts)) trace → 477 P (gather_trace ? trace) s' → 478 after_n_steps n O I fx g s inv P. 479 #n elim n 480 [ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct 481 #ALL #p whd @p 482  #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC 483 cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS 484 destruct 485 #ALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all … (λts. inv (\snd ts)) tl)) 486 [ whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/ ] * #i1 #itl 487 #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?)) 488 [ @p 489  whd >NOTFINAL whd >STEP whd >i1 whd %{(refl ??)} #tr'' #s'' #p' @p' 490 ] 491 ] qed. 492 493 lemma exec_steps_after_n_noinv : ∀n,O,I,fx,g,s,trace,s',P. 494 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 495 P (gather_trace ? trace) s' → 496 after_n_steps n O I fx g s (λ_.true) P. 497 #n #O #I #fx #g #s #trace #s' #P #EXEC #p 498 @(exec_steps_after_n … EXEC) // 499 elim trace /2/ 500 qed. 501 502 lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P. 503 after_n_steps n O I fx g s inv P → 504 ∃trace,s'. exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ P (gather_trace ? trace) s'. 505 #n elim n 506 [ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} %{(refl ??)} @AFTER 507  #m #IH #O #I #fx #g #s #inv #P #AFTER 508 cases (after_1_of_n_steps … AFTER) 509 #tr1 * #s1 * * * #NF #STEP #INV #AFTER' 510 cases (IH … AFTER') 511 #tl * #s' * #STEPS #p 512 %{(〈tr1,s1〉::tl)} %{s'} % 513 [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS %  // ] 514 ] qed. 515 516 lemma exec_steps_split : ∀n,m,O,I,fx,g,s,trace,s'. 517 exec_steps (n+m) O I fx g s = OK ? 〈trace,s'〉 → 518 ∃trace1,trace2,s1. 519 exec_steps n O I fx g s = OK ? 〈trace1,s1〉 ∧ 520 exec_steps m O I fx g s1 = OK ? 〈trace2,s'〉 ∧ 521 trace = trace1 @ trace2. 522 #n elim n 523 [ #m #O #I #fx #g #s #trace #s' #EXEC 524 %{[ ]} %{trace} %{s} /3/ 525  #n' #IH #m #O #I #fx #g #s #trace #s' #EXEC 526 cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC' 527 cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2 528 %{(〈tr',s'〉::trace1)} %{trace2} %{s1} 529 % 530 [ % 531 [ whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >EXEC1 % 532  @EXEC2 533 ] 534  destruct % 535 ] 536 ] qed. 537 538 lemma exec_steps_join : ∀n,m,O,I,fx,g,s1,trace1,s2,trace2,s3. 539 exec_steps n O I fx g s1 = OK ? 〈trace1,s2〉 → 540 exec_steps m O I fx g s2 = OK ? 〈trace2,s3〉 → 541 exec_steps (n+m) O I fx g s1 = OK ? 〈trace1@trace2,s3〉. 542 #n elim n 543 [ #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2 544 whd in EXEC1:(??%?); destruct @EXEC2 545  #n' #IH #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2 546 cases (exec_steps_S … EXEC1) #NF * #tr' * #s' * #tl' * * #E1 #STEP #EXEC' 547 whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >(IH … EXEC' EXEC2) 548 destruct % 549 ] qed. 550 551 (* Show that it corresponds to split_trace … (exec_inf …) *) 552 553 lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'. 554 exec_steps n O I fx g s = OK ? 〈trace,s'〉 → 555 match is_final … s' with 556 [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈trace, exec_inf_aux … fx g (step … s')〉 557  Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈trace, e_stop … tr' r s'〉 558 ]. 559 #O #I #fx #g #n elim n 560 [ #s #trace #s' #EX whd in EX:(??%%); destruct 561 cases (is_final … s') [ %  #r %1 % ] 562  #m #IH #s #trace #s' #EX 563 cases (exec_steps_S … EX) 564 #notfinal * #tr'' * #s'' * #tl * * #Etrace #Estep #Esteps 565 cases tl in Etrace Esteps ⊢ %; 566 [ #E destruct #Esteps 567 lapply (exec_steps_length … Esteps) #Elen normalize in Elen; destruct 568 whd in Esteps:(??%?); destruct 569 >Estep 570 >exec_inf_aux_unfold normalize nodelta 571 cases (is_final … s') 572 [ % 573  #r %2 %{tr''} % 574 ] 575  * #tr1 #s1 #tl1 #E normalize in E; destruct #Esteps 576 lapply (IH … Esteps) cases (is_final … s') 577 [ normalize nodelta #IH' >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); 578 >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' % 579  normalize nodelta #r * 580 [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct 581  * #tr'' #IH' %2 %{tr''} >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?); 582 >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' % 583 ] 584 ] 585 ] 586 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.