Changeset 2413
 Timestamp:
 Oct 23, 2012, 11:15:28 AM (9 years ago)
 Location:
 src/common
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/StructuredTraces.ma
r2398 r2413 468 468 interpretation "trace any any label append" 'append taa tal = (taa_append_tal ????? taa tal). 469 469 470 let rec tal_collapsable S fl s1 s2 (tal : trace_any_label S fl s1 s2) on tal : Prop ≝ 471 match tal with 472 [ tal_base_not_return _ _ _ _ _ ⇒ True 473  tal_step_default fl1 _ st1' st1'' _ tl1 _ _ ⇒ tal_collapsable … tl1 474  _ ⇒ False 475 ]. 476 470 477 let rec tlr_rel S1 st1 st1' S2 st2 st2' 471 478 (tlr1 : trace_label_return S1 st1 st1') … … 512 519  tal_base_call st1 st1' st1'' _ _ _ _ tlr1 _ ⇒ 513 520 fl2 = doesnt_end_with_ret ∧ 514 ∃st2mid,taa,st2mid',H,f,G,K,tlr2,L. 515 tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa 516 (tal_base_call ? st2mid st2mid' st2' H f G K tlr2 L) ∧ 517 tlr_rel … tlr1 tlr2 521 ∃st2mid.∃taa : trace_any_any ? st2 st2mid.∃st2mid',H. 522 (* we must allow a tal_base_call to be similar to a call followed 523 by a collapsable trace (trace_any_any followed by a base_not_return; 524 we cannot use trace_any_any as it disallows labels in the end as soon 525 as it is nonempty) *) 526 (∃f,G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L. 527 tal2 ≃ taa @ (tal_base_call … H f G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨ 528 ∃st2mid'',f,G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L. 529 ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'. 530 tal2 ≃ taa @ (tal_step_call … H f G K tlr2 L tl2) ∧ 531 tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2 518 532  tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ _ tlr1 _ tl1 ⇒ 519 ∃st2mid,taa,st2_fun,st2_after_fun,H,f,G,K,tlr2,L,tl2. 520 tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa 521 (tal_step_call ?? st2mid st2_fun st2_after_fun st2' H f G K tlr2 L tl2) ∧ 522 tlr_rel … tlr1 tlr2 ∧ tal_rel … tl1 tl2 533 ∃st2mid.∃taa : trace_any_any ? st2 st2mid.∃st2mid',H. 534 (fl2 = doesnt_end_with_ret ∧ ∃f,G,K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L. 535 tal2 ≃ taa @ tal_base_call … H f G K tlr2 L ∧ 536 tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨ 537 ∃st2mid'',f,G,K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L. 538 ∃tl2 : trace_any_label ? fl2 st2mid'' st2'. 539 tal2 ≃ taa @ (tal_step_call … H f G K tlr2 L tl2) ∧ 540 tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2 523 541  tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ 524 542 tal_rel … tl1 tal2 (* < this makes it many to many *) … … 528 546 interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2). 529 547 interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ?????? t1 t2). 548 549 let rec tal_collapsable_eq_fl S1 fl1 s1 s1' 550 (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 : 551 tal_collapsable … tal1 → fl1 = doesnt_end_with_ret ≝ ?. 552 cases tal1 fl1 s1 s1' // 553 [ #s1 #s1' #H #I * 554  #s1 #s1' #s1'' #s1''' #s1'''' #H #f #I #J #tlr #K #tl * 555  #fl1 #s1 #s1' #s1'' #H #tl #I #J @(tal_collapsable_eq_fl … tl) 556 ] 557 qed. 558 559 let rec tal_rel_eq_fl S1 fl1 s1 s1' S2 fl2 s2 s2' 560 (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 : 561 ∀tal2 : trace_any_label S2 fl2 s2 s2'.tal_rel … tal1 tal2 → fl1 = fl2 ≝ 562 match tal1 return λfl1,s1,s1',tal1.? with 563 [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ? 564  tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ? 565  tal_base_call st1 st1' st1'' _ _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ? 566  tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ? 567  tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ? 568 ]. 569 fl1 s1 s1' 570 [1,2,3: tal_rel_eq_fl #tal2 * // 571  #tal2 * #s2_mid * #taa2 * #s2' *#H2 * 572 [ * #EQ1 *#f *#G2 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) // 573  * #s2_mid' *#f *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #_ #step #_ 574 @(tal_rel_eq_fl … step) 575 ] 576  #tal2 whd in ⊢ (%→?); #step @(tal_rel_eq_fl … step) 577 ] 578 qed. 530 579 531 580 let rec taa_rel_inv S1 fl1 st1 st1mid st1' S2 fl2 st2 st2' … … 542 591 qed. 543 592 544 let rec tlr_rel_transitive S1 st1 st1' S2 st2 st2' S3 st3 st3' 545 (tlr1 : trace_label_return S1 st1 st1') 546 (tlr2 : trace_label_return S2 st2 st2') 547 (tlr3 : trace_label_return S3 st3 st3') on tlr1 : 548 tlr_rel … tlr1 tlr2 → tlr_rel … tlr2 tlr3 → tlr_rel … tlr1 tlr3 ≝ 549 match tlr1 with 550 [ tlr_base st1' st1'' tll1 ⇒ ? 551  tlr_step st1' st1'' st1''' tll1 tl1 ⇒ ? 552 ] 553 and tll_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3' 554 (tll1 : trace_label_label S1 fl1 st1 st1') 555 (tll2 : trace_label_label S2 fl2 st2 st2') 556 (tll3 : trace_label_label S3 fl3 st3 st3') on tll1 : 557 tll1 ≈ tll2 → tll2 ≈ tll3 → tll1 ≈ tll3 ≝ 558 match tll1 with 559 [ tll_base fl1' st1' st1'' tal1 H ⇒ ? 560 ] 561 and tal_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3' 562 (tal1 : trace_any_label S1 fl1 st1 st1') 563 (tal2 : trace_any_label S2 fl2 st2 st2') 564 (tal3 : trace_any_label S3 fl3 st3 st3') on tal1 : 565 tal1 ≈ tal2 → tal2 ≈ tal3 → tal1 ≈ tal3 ≝ 566 match tal1 with 567 [ tal_base_not_return st1' st1'' H G K ⇒ ? 568  tal_base_return st1' st1'' H G ⇒ ? 569  tal_base_call st1' st1'' st1''' H f G K tlr1 L ⇒ ? 570  tal_step_call fl1' st1' st1'' st1''' st1'''' H f G L tlr1 K tl1 ⇒ ? 571  tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ? 572 ]. 573 [1,2: cases tlr2 #st2' #st2'' [1,3: #tllhd2 2,4: #st2''' #tllhd2 #tlrtl2] 574 [2,3: *] normalize in ⊢ (%→?); [ #Rhd12  * #Rhd12 #Rtl12 ] 575 cases tlr3 #st3' #st3'' [1,3: #tllhd3 2,4: #st3''' #tllhd3 #tlrtl3] 576 [2,3: *] normalize in ⊢ (%→?); [ #Rhd23  * #Rhd23 #Rtl23 ] whd 577 [ @(tll_rel_transitive … Rhd12 Rhd23)  578 %{(tll_rel_transitive … Rhd12 Rhd23)} 579 @(tlr_rel_transitive … Rtl12 Rtl23) 580 ] 581 3: 582 cases tll2 #fl2' #st2' #st2'' #tal2 #H2 * #G2 #R12 583 cases tll3 #fl3' #st3' #st3'' #tal3 #H3 * #G3 #R23 584 %{(tal_rel_transitive … R12 R23)} // 585 *: 586 [1,2,3: * #EQ] 587 [5: whd in ⊢ (%→?→%); @tal_rel_transitive] 588 *#st2mid *#taa2 589 [ *#H2 *#G2 *#K2 #R12 590  *#H2 *#G2 #R12 591  *#st2' *#H2 *#f2 *#G2 *#K2 *#tlr2 *#L2 *#R12 #R12' 592  *#st2' *#st2'' *#H2 *#f2 *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #R12 #R12' #R12'' 593 ] destruct #R23 lapply (taa_rel_inv … R23) [1,2: // 3: *#EQ destruct] 594 *#st3mid *#taa3 595 [ *#st3' *#H3 *#f3 *#G3 *#K3 *#tlr3 *#L3 *#R23 #R23' 596 %{(refl …)} %{st3mid} %{taa3} %{st3'} %{H3} %{f3} %{G3} %{K3} %{tlr3} %{L3} 597 %{R23} @(tlr_rel_transitive … R12' R23') 598  *#st3' *#st3'' *#H3 *#f3 *#G3 *#K3 *#tlr3 *#L3 *#tl3 ** #R23 #R23' #R23'' 599 %{st3mid} %{taa3} %{st3'} %{st3''} %{H3} %{f3} %{G3} %{K3} %{tlr3} %{L3} %{tl3} 600 %{(tal_rel_transitive … R12'' R23'')} 601 %{R23} @(tlr_rel_transitive … R12' R23') 602 ] 593 lemma taa_append_collapsable : ∀S,s1,fl,s2,s3. 594 ∀taa,tal.tal_collapsable S fl s2 s3 tal → tal_collapsable S fl s1 s3 (taa@tal). 595 #S #s1 #fl #s2 #s3 #taa elim taa s1 s2 /2/ 596 qed. 597 598 let rec tal_rel_collapsable S1 fl1 s1 s1' S2 fl2 s2 s2' 599 (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 : 600 ∀tal2 : trace_any_label S2 fl2 s2 s2'.tal_collapsable … tal1 → tal_rel … tal1 tal2 → 601 tal_collapsable … tal2 ≝ 602 match tal1 return λfl1,s1,s1',tal1.? with 603 [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ? 604  tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ? 605  tal_base_call st1 st1' st1'' _ _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ? 606  tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ? 607  tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ? 608 ]. 609 fl1 s1 s1' 610 [1,2,3: tal_rel_collapsable #tal2 * * 611 #EQ * #s2 * #taa2 *#H *#G *#K #EQ' destruct @taa_append_collapsable % 612  #tal2 * 613  #tal2 #tal2 whd in ⊢ (%→?); #step @(tal_rel_collapsable … step) assumption 603 614 ] 604 615 qed. … … 677 688 ] 678 689 qed. 690 691 let rec tal_collapsable_flatten S fl st1 st2 tal 692 on tal : 693 tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ] ≝ 694 match tal 695 return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ] 696 with 697 [ tal_base_not_return the_status _ _ _ _ ⇒ λ_.refl ?? 698  tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ 699 tal_collapsable_flatten ???? tail_trace 700  _ ⇒ Ⓧ 701 ]. 679 702 680 703 let rec tll_rel_to_traces_same_flatten … … 737 760 [ *#H' *#G' *#K' #EQ 738 761  *#H' *#G' #EQ 739  *#st_mid' *#H' *#f' *#G' *#K' *#tlr2 *#L' * #EQ #H_tlr 740  *#st_fun *#st_after *#H' *#f' *#G' *#K' *#tlr2 *#L' *#tl2 ** #EQ #H_tlr #H_tal 762  *#st_mid' *#H' * [*#st2_mid''] *#f' *#G' *#K' *#tlr2 *#L' 763 [*#tl2 *] * #EQ #H_tlr [ #H_tl] 764  *#st_fun *#H' * 765 [*#fl_EQ destruct(fl_EQ) * #st2_mid ] *#f' *#G' *#K' *#tlr2 *#L' 766 [ *#tl2] ** #EQ #H_tl #H_tlr 741 767 ] >EQ >taa_append_tal_same_flatten 742 768  whd in ⊢ (%→??(????%)?); … … 744 770 ] 745 771 [1,2: % 746  @(tlr_rel_to_traces_same_flatten … H_tlr) 747  <map_append 772 3: @(tlr_rel_to_traces_same_flatten … H_tlr) 773 4,5: <map_append 774 >(tal_collapsable_flatten … H_tl) >append_nil 775 >(tlr_rel_to_traces_same_flatten … H_tlr) % 776 6: <map_append 748 777 >(tlr_rel_to_traces_same_flatten … H_tlr) 749 >(tal_rel_to_traces_same_flatten … H_t al)778 >(tal_rel_to_traces_same_flatten … H_tl) 750 779 @map_append 751 780 ]
Note: See TracChangeset
for help on using the changeset viewer.