Changeset 2413


Ignore:
Timestamp:
Oct 23, 2012, 11:15:28 AM (7 years ago)
Author:
tranquil
Message:
  • tal_rel corrected to include cases where tal_base_call \approx tal_step_call
  • status simulation: from local properties to propagation of structured traces
Location:
src/common
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r2398 r2413  
    468468interpretation "trace any any label append" 'append taa tal = (taa_append_tal ????? taa tal).
    469469
     470let rec tal_collapsable S fl s1 s2 (tal : trace_any_label S fl s1 s2) on tal : Prop ≝
     471match tal with
     472[ tal_base_not_return _ _ _ _ _ ⇒ True
     473| tal_step_default fl1 _ st1' st1'' _ tl1 _ _ ⇒ tal_collapsable … tl1
     474| _ ⇒ False
     475].
     476
    470477let rec tlr_rel S1 st1 st1' S2 st2 st2'
    471478  (tlr1 : trace_label_return S1 st1 st1')
     
    512519  | tal_base_call st1 st1' st1'' _ _ _ _ tlr1 _ ⇒
    513520    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 non-empty) *)
     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
    518532  | 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
    523541  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
    524542    tal_rel … tl1 tal2 (* <- this makes it many to many *)
     
    528546interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2).
    529547interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ?????? t1 t2).
     548
     549let 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 ≝ ?.
     552cases 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]
     557qed.
     558
     559let 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]
     578qed.
    530579
    531580let rec taa_rel_inv S1 fl1 st1 st1mid st1' S2 fl2 st2 st2'
     
    542591qed.
    543592
    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   ]
     593lemma 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/
     596qed.
     597
     598let 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
    603614]
    604615qed.
     
    677688]
    678689qed.
     690
     691let 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 = [ ] ≝
     694match tal
     695return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ]
     696with
     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].
    679702
    680703let rec tll_rel_to_traces_same_flatten
     
    737760    [ *#H' *#G' *#K' #EQ
    738761    | *#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
    741767    ] >EQ >taa_append_tal_same_flatten
    742768  | whd in ⊢ (%→??(????%)?);
     
    744770  ]
    745771  [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
    748777    >(tlr_rel_to_traces_same_flatten … H_tlr)
    749     >(tal_rel_to_traces_same_flatten … H_tal)
     778    >(tal_rel_to_traces_same_flatten … H_tl)
    750779    @map_append
    751780  ]
Note: See TracChangeset for help on using the changeset viewer.