Changeset 3551
- Timestamp:
- Apr 9, 2015, 4:44:52 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Lang_meas.ma
r3550 r3551 351 351 ∀prf :execute_l p p' (env … prog) l s1 s2. 352 352 state_rel … m keep abs_top abs_tail s1 s1' → 353 (is_call_act … l → bool_to_Prop (is_call_post_label … (operational_semantics … p' prog) … s1)) → 353 354 ∃abs_top'.∃s2'. 354 355 execute_l p p' (env … t_prog) l s1' s2' ∧ … … 395 396 ] 396 397 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct] #EQcode_s1' whd in ⊢ (??%% → ?); #EQ destruct 397 %{gen_labels} %{(mk_state … i' stack' (store … s1') false)} %398 #_ %{gen_labels} %{(mk_state … i' stack' (store … s1') false)} % 398 399 [% [ @(empty … EQcode_s1' EQcont_s1') // #_ %{lbl'} %] 399 400 whd >EQcheck in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); normalize nodelta % // % // % // % // >EQclean %] … … 429 430 inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #genlab #cleaned #EQcleaned 430 431 cases opt_l' in EQcode_s1'; normalize nodelta [|#lbl'] #EQcode_s1' [| inversion(?==?) normalize nodelta #EQget] 431 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQst #EQioinfo #EQ destruct 432 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQst #EQioinfo #EQ destruct #_ 432 433 %{genlab} %{(mk_state … i' (cont … s1') (store … s2) false)} % [ % 433 434 [ @(seq_sil … EQcode_s1') // ] 434 435 whd <EQcont >EQcheck normalize nodelta % // % // % // % // >EQcleaned %] 435 436 whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >(\P EQget) >append_nil % 436 | cases daemon 437 | cases daemon 438 | cases daemon 439 | cases daemon 437 | #s1 #s2 #cond #ltrue #i_true #lfalse #i_false #instr #mem #EQcode_s1 #EQcond #EQcont_s2 #EQ1 #EQ2 destruct 438 #Hio1 #Hio2 #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) [ #_ *] 439 ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1') 440 [1,2,3,5,6,7: 441 [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ 442 | #lin #io #lout #instr #_ ] 443 #_ whd in ⊢ (??%% → ?); 444 [ | 445 | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 446 | cases(call_post_clean ?????) normalize nodelta 447 [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 448 [| #y cases(?∧?) normalize nodelta 449 ] 450 ] 451 | cases(call_post_clean ?????) normalize nodelta 452 [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta 453 [ cases (?==?) normalize nodelta ] 454 ]] 455 | cases(call_post_clean ?????) normalize nodelta 456 [| #x cases(? ∧ ?) normalize nodelta ] 457 ] 458 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 459 ] 460 #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?); 461 inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr' 462 whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2 463 #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * 464 #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta 465 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQstore #EQio #EQ destruct #_ 466 %{a_top3} %{(mk_state … i_true' (〈cost_act … (None ?),instrs'〉::(cont … s1')) (store … s2) false)} % 467 [2: whd in ⊢ (??%%); >(\P EQget1) >append_nil % ] % 468 [ @(cond_true … EQcode_s1') // ] >EQcont_s2 whd in match (check_continuations ??????); 469 change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta 470 >EQinstr' normalize nodelta % // % // % // % [ % // % //] >EQi_true' % 471 | #s1 #s2 #cond #ltrue #i_true #lfalse #i_false #instr #mem #EQcode_s1 #EQcond #EQcont_s2 #EQ1 #EQ2 destruct 472 #Hio1 #Hio2 #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) [ #_ *] 473 ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1') 474 [1,2,3,5,6,7: 475 [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #itrue #lfalse #ifalse #_ #_| #f #pars #opt_l #instr #_ 476 | #lin #io #lout #instr #_ ] 477 #_ whd in ⊢ (??%% → ?); 478 [ | 479 | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 480 | cases(call_post_clean ?????) normalize nodelta 481 [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 482 [| #y cases(?∧?) normalize nodelta 483 ] 484 ] 485 | cases(call_post_clean ?????) normalize nodelta 486 [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta 487 [ cases (?==?) normalize nodelta ] 488 ]] 489 | cases(call_post_clean ?????) normalize nodelta 490 [| #x cases(? ∧ ?) normalize nodelta ] 491 ] 492 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 493 ] 494 #exp' #ltrue' #i_true' #lfalse' #i_false' #instrs' #_ #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?); 495 inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * #a_top1 #istr1 #EQinstr' 496 whd in ⊢ (??%%→ ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] * #a_top2 #istr2 497 #EQi_false' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [#_ #EQ destruct] * 498 #a_top3 #istr3 #EQi_true' inversion(?==?) #EQget1 inversion(?==?) #EQget2 normalize nodelta 499 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQstore #EQio #EQ destruct #_ 500 %{a_top2} %{(mk_state … i_false' (〈cost_act … (None ?),instrs'〉::(cont … s1')) (store … s2) false)} % 501 [2: whd in ⊢ (??%%); >(\P EQget2) >append_nil % ] % 502 [ @(cond_false … EQcode_s1') // ] >EQcont_s2 whd in match (check_continuations ??????); 503 change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta 504 >EQinstr' normalize nodelta % // % // % // % [ % // % //] >EQi_false' % 505 | #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2 506 #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta 507 [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1') 508 [1,2,3,4,6,7: 509 [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_ 510 | #lin #io #lout #instr #_ ] 511 #_ whd in ⊢ (??%% → ?); 512 [ | 513 | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 514 | cases(call_post_clean ?????); normalize nodelta 515 [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 516 [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 517 [| #z cases(?∧?) normalize nodelta 518 ] 519 ] 520 ] 521 | cases(call_post_clean ?????) normalize nodelta 522 [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta 523 [ cases (?==?) normalize nodelta ] 524 ]] 525 | cases(call_post_clean ?????) normalize nodelta 526 [| #x cases(? ∧ ?) normalize nodelta ] 527 ] 528 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 529 ] 530 #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?); 531 inversion(call_post_clean …) normalize nodelta [ #_ #EQ destruct] * #a_top1 #i_false'' 532 #EQi_false' inversion(call_post_clean …) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true'' 533 #EQi_true' >m_return_bind inversion(?==?) normalize nodelta #EQget1 [2: #EQ destruct] 534 inversion(?==?) normalize nodelta #EQget2 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 535 #EQstore #EQio #EQ destruct #_ %{a_top2} 536 %{(mk_state … i_true' (〈cost_act … (None ?),LOOP … exp ltrue i_true' lfalse i_false'〉::(cont … s1')) (store … s2) false)} 537 % [2: whd in ⊢ (??%%); >(\P EQget1) >append_nil % ] % 538 [ @(loop_true … EQcode_s1') // ] >EQcont_s2 whd in match (check_continuations ??????); 539 change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta 540 whd in match (call_post_clean ??????); >EQi_false' normalize nodelta >EQi_true' 541 >m_return_bind >(\P EQget1) >(\P EQget2) >(\b (refl …)) >(\b (refl …)) normalize nodelta 542 % // % // % // % [ % // % //] >EQi_true' % 543 | #s1 #s2 #exp #ltrue #i_true #lfalse #i_false #m #EQcode_s1 #EQeval #EQcont_s2 #EQ1 #EQ2 destruct #Hio1 #Hio2 544 #_ whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta 545 [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1') 546 [1,2,3,4,6,7: 547 [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| #f #pars #opt_l #instr #_ 548 | #lin #io #lout #instr #_ ] 549 #_ whd in ⊢ (??%% → ?); 550 [ | 551 | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 552 | cases(call_post_clean ?????); normalize nodelta 553 [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 554 [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 555 [| #z cases(?∧?) normalize nodelta 556 ] 557 ] 558 ] 559 | cases(call_post_clean ?????) normalize nodelta 560 [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta 561 [ cases (?==?) normalize nodelta ] 562 ]] 563 | cases(call_post_clean ?????) normalize nodelta 564 [| #x cases(? ∧ ?) normalize nodelta ] 565 ] 566 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 567 ] 568 #exp' #ltrue' #i_true' #lfalse' #i_false' #_ #_ #EQcode_s1' whd in ⊢ (??%% → ?); 569 inversion(call_post_clean …) normalize nodelta [ #_ #EQ destruct] * #a_top1 #i_false'' 570 #EQi_false' inversion(call_post_clean …) [ #_ whd in ⊢ (??%% → ?); #EQ destruct] * #a_top2 #i_true'' 571 #EQi_true' >m_return_bind inversion(?==?) normalize nodelta #EQget1 [2: #EQ destruct] 572 inversion(?==?) normalize nodelta #EQget2 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 573 #EQstore #EQio #EQ destruct #_ %{a_top1} 574 %{(mk_state … i_false' (cont … s1') (store … s2) false)} 575 % [2: whd in ⊢ (??%%); >(\P EQget2) >append_nil % ] % 576 [ @(loop_false … EQcode_s1') // ] >EQcont_s2 >EQcheck normalize nodelta 577 % // % // % // % // >EQi_false' % 440 578 | #s1 #s2 #lin #io #lout #i #store #EQcode_s1 #EQeval #EQcode_s2 #EQcont_s2. #EQ destruct #EQio_s2 * 441 579 whd in match state_rel in ⊢ (% → ?); normalize nodelta inversion(check_continuations ?????) normalize nodelta [#_ *] … … 466 604 #lin' #io' #lout' #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean ?????) normalize nodelta [ #_ #EQ destruct] 467 605 * #genlab #cleaned #EQcleaned inversion(?∧?) normalize nodelta #EQget whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ 468 #EQ destruct #EQstore_s1_s1' #EQioinfo #EQ destruct %{[]}606 #EQ destruct #EQstore_s1_s1' #EQioinfo #EQ destruct #_ %{[]} 469 607 %{(mk_state … (EMPTY …) (〈cost_act p (Some ? lout),i'〉::(cont … s1')) (store … s2) true)} % [% 470 608 [ @(io_in … EQcode_s1') // ] … … 475 613 whd in match actionlabel_to_costlabel; normalize nodelta whd in ⊢ (??%%); >append_nil >append_nil inversion(? == ?) in EQget'; 476 614 [2: #_ *] #EQget' #_ >(\P EQget') % 477 |*: cases daemon 478 ] 615 | #s1 #s2 #f #act_p #r_lb #i #mem #env_it #EQcode_s1 #EQlook #EQeval #EQ destruct #EQcode_s2 #EQcont_s2 616 #Hio1 #Hio2 * whd in match state_rel; normalize nodelta inversion(check_continuations …) normalize nodelta 617 [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta **** #HH1 >EQcode_s1 inversion(code … s1') 618 [1,2,3,4,5,7: 619 [ | #ret | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 620 #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #lin #io #lout #instr #_ ] 621 #_ whd in ⊢ (??%% → ?); 622 [ | 623 | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 624 | cases(call_post_clean ?????); normalize nodelta 625 [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 626 [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 627 [| #z cases(?∧?) normalize nodelta 628 ] 629 ] 630 ] 631 | cases(call_post_clean ?????) normalize nodelta 632 [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 633 [| #y cases(?∧?) normalize nodelta 634 ] 635 ] 636 | cases(call_post_clean ?????) normalize nodelta 637 [| #x cases(? ∧ ?) normalize nodelta ] 638 ] 639 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 640 ] 641 #f' #act_p' #r_lb #i' #_ #EQcode_s1' whd in ⊢ (??%% → ?); inversion(call_post_clean …) normalize nodelta 642 [ #_ #EQ destruct] * #a_top1 #i'' #EQi' inversion(r_lb) normalize nodelta [ #_ #EQ destruct] #lbl #EQ 643 destruct inversion(? ∈ ?) normalize nodelta #EQmem [ inversion(?==?) normalize nodelta #EQget] 644 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #EQstore #EQio #EQ destruct 645 lapply(trans_env_ok … no_dup) >EQt_prog normalize nodelta #H cases(H … EQlook) -H #env_it' * #n 646 ** #Hfresh #EQlook' ***** #EQt_code #EQget1 #EQsig #EQlab #same_fresh #same_keep whd in match (is_call_post_label ???); 647 >EQcode_s1 normalize nodelta [ #_ | * %{f} %{(f_lab … env_it)} %] 648 %{(gen_labels … (call_post_trans … (f_body … env_it) n []))} 649 %{(mk_state … (f_body … env_it') (〈ret_act … (Some … lbl),i'〉 :: (cont … s1')) (store … s2) false)} 650 % [2,4: whd in ⊢ (??%%); >append_nil >EQlab >EQget1 % ] % [1,3: >EQlab @(call … EQcode_s1') //] 651 >EQcont_s2 whd in match (check_continuations ??????); 652 change with (check_continuations ??????) in match (foldr2 ???????); >EQcheck normalize nodelta 653 >EQi' normalize nodelta whd in match ret_costed_abs; normalize nodelta >EQmem normalize nodelta 654 % // % // % // % [ % [ % // % //] >(\P EQget) % ] <EQt_code @inverse_call_post_trans // 655 [ >EQcode_s2 @no_duplicates_domain_of_fun // 656 | >EQcode_s2 #H20 #H21 >same_fresh // 657 | >EQcode_s2 #H23 #H24 >same_keep // 658 ] 659 | #s1 #s2 #r_t #mem #stack * [|#lbl] #i #EQcode_s1 #EQcont_s1 #EQ destruct #Hio1 #Hio2 #EQeval #EQ1 #EQ2 destruct * 660 whd in match state_rel; normalize nodelta >EQcont_s1 inversion(cont … s1') [| * #lab #i' #stack' #_ ] #EQcont_s1' 661 whd in match (check_continuations ??????); [*] change with (check_continuations ??????) in match (foldr2 ???????); 662 inversion(check_continuations ??????) normalize nodelta [ #_ *] ** #H1 #a_top #a_tail #EQcheck normalize nodelta 663 inversion(call_post_clean …) normalize nodelta [ #_ *****] * #a_top1 #i'' #EQi' inversion lab normalize nodelta 664 [ #f #lb ****** |3: * [| #x] #EQ destruct normalize nodelta ****** [|*] #EQ destruct] * [|#lb] #EQ destruct 665 normalize nodelta [****** #EQ destruct] whd in match ret_costed_abs; normalize nodelta inversion(? ∈ ?) #EQmem 666 normalize nodelta ****** [*] #EQ destruct #HH1 #EQ destruct #EQget >EQcode_s1 inversion(code … s1') 667 [1,3,4,5,6,7: 668 [ | #seq #opt_l #instr #_ | #cond #ltrue #i_true #lfalse #i_false #instr #_ #_ #_| 669 #cond #ltrue #itrue #lfalse #ifalse #_ #_ | #f #pars #opt_l #instr #_ | #lin #io #lout #instr #_ ] 670 #_ whd in ⊢ (??%% → ?); 671 [ 672 | cases(call_post_clean ?????); normalize nodelta [2: #x cases opt_l normalize nodelta [| #label cases(?==?) normalize nodelta]] 673 | cases(call_post_clean ?????); normalize nodelta 674 [2: #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 675 [|#y whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 676 [| #z cases(?∧?) normalize nodelta 677 ] 678 ] 679 ] 680 | cases(call_post_clean ?????) normalize nodelta 681 [| #x whd in ⊢ (??%? → ?); cases(call_post_clean ?????) normalize nodelta 682 [| #y cases(?∧?) normalize nodelta 683 ] 684 ] 685 | cases(call_post_clean ?????) normalize nodelta 686 [| #x cases opt_l normalize nodelta [| #lbls cases(memb ???) normalize nodelta 687 [ cases (?==?) normalize nodelta ] 688 ]] 689 | cases(call_post_clean ?????) normalize nodelta 690 [| #x cases(? ∧ ?) normalize nodelta ] 691 ] 692 whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 693 ] #r_t' #EQcode_s1' whd in ⊢ (??%% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct 694 #EQstore #EQio #EQ destruct #_ 695 %{a_top1} %{(mk_state … i' stack' (store … s2) false)} % [2: whd in ⊢ (??%%); >EQget >append_nil %] 696 % [ @(ret_instr … EQcode_s1' … EQcont_s1') // ] >EQcheck normalize nodelta % // % // % // % // >EQi' % 697 ] 479 698 qed. 480 699 … … 501 720 #abs_top1 * #s0' * #t_i0' * #Rs0_s0' #sil_ti0' 502 721 lapply(labelled_action_is_correct … p' prog no_dup) >EQt_prog normalize nodelta #Hmove 503 cases(Hmove … prf1 … Rs0_s0') // 722 cases(Hmove … prf1 … Rs0_s0') // [2: @Hcall_init] 504 723 #abs_top2 * #s1' ** #prf1' #Rs1_s1' #EQmap_l1 505 724 lapply(correctness_lemma … p' prog no_dup) >EQt_prog normalize nodelta #H 506 725 cases(H … pre_t12 … Rs1_s1') -H 507 726 #abs_top3 * #s2' * #t12' ***** #Rs2_s2' #Hperm #_ #_ #pre_t12' #_ 508 cases(Hmove … prf2 … Rs2_s2') -Hmove // 727 cases(Hmove … prf2 … Rs2_s2') -Hmove // [2: @Hcall_fin] 509 728 #abs_top4 * #s3' ** #prf2' #Rs3_s3' #EQmap_l2 510 729 cases(Hsilent … sil_t3n … Rs3_s3')
Note: See TracChangeset
for help on using the changeset viewer.