Changeset 2186 for src/common


Ignore:
Timestamp:
Jul 16, 2012, 4:59:09 PM (7 years ago)
Author:
tranquil
Message:

updated joint semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r2129 r2186  
    334334qed.
    335335
    336 (* an uncalling, unreturning and *unjumping*,
    337   as well as unlabelled (but possibly for the first and last statuses)
    338   possibly empty trace segment *)
    339 inductive trace_any_any (S:abstract_status) : S → S → Type[0] ≝
    340   | taa_base :
     336(*
     337(* an trace of unlabeled and cl_other states, possibly empty *)
     338inductive trace_no_label_any (S:abstract_status) : S → S → Type[0] ≝
     339  | tna_base :
    341340      ∀start_status: S.
    342         trace_any_any S start_status start_status
    343   | taa_step :
     341      ¬as_costed … start_status →
     342      trace_no_label_any S start_status start_status
     343  | tna_step :
    344344      ∀status_pre: S.
    345345      ∀status_init: S.
    346346      ∀status_end: S.
    347347        as_execute S status_pre status_init →
    348         trace_any_any S status_init status_end →
    349348        as_classifier S status_pre cl_other →
    350         ¬as_costed … status_init →
    351           trace_any_any S status_pre status_end.
    352 
    353 let rec taa_status_list S st1 st2 (taa : trace_any_any S st1 st2) on taa : list S ≝
     349        ¬as_costed … status_pre →
     350        trace_no_label_any S status_init status_end →
     351          trace_no_label_any S status_pre status_end.
     352
     353let rec tna_append_tna S st1 st2 st3 (taa1 : trace_no_label_any S st1 st2)
     354  on taa1 :
     355    trace_no_label_any S st2 st3 →
     356    trace_no_label_any S st1 st3 ≝
     357  match taa1 with
     358  [ tna_base st1' H ⇒ λtaa2.taa2
     359  | tna_step st1' st2' st3' H G K tl ⇒
     360    λtaa2.tna_step ???? H G K (tna_append_tna … tl taa2)
     361  ].
     362
     363definition tna_non_empty ≝ λS,st1,st2.λtna : trace_no_label_any S st1 st2.
     364  match tna with
     365  [ tna_base _ _ ⇒ false
     366  | tna_step _ _ _ _ _ _ _ ⇒ true
     367  ].
     368
     369coercion tna_to_bool : ∀S,st1,st2.∀tna:trace_no_label_any S st1 st2.bool ≝
     370 tna_non_empty on _tna : trace_no_label_any ??? to bool.
     371
     372lemma tna_unlabelled : ∀S,st1,st2.trace_no_label_any S st1 st2 → ¬as_costed … st1.
     373#S #st1 #st2 * [#st #H @H | #st #st' #st'' #_ #_ #H #_ @H] qed.
     374
     375let rec tna_append_tal S st1 fl st2 st3 (tna : trace_no_label_any S st1 st2)
     376  on tna :
     377  trace_any_label S fl st2 st3 →
     378  if tna then Not (as_costed … st2) else True →
     379  trace_any_label S fl st1 st3 ≝
     380  match tna return λst1,st2.λx : trace_no_label_any S st1 st2.
     381    ∀fl,st3.
     382    trace_any_label S fl st2 st3 →
     383    if x then Not (as_costed … st2) else True →
     384    trace_any_label S fl st1 st3
     385  with
     386  [ tna_base st1' H ⇒ λfl,st3,taa2,prf.taa2
     387  | tna_step st1' st2' st3' H G K tl ⇒ λfl,st3,taa2,prf.
     388    tal_step_default ????? H (tna_append_tal ????? tl taa2 ?) G (tna_unlabelled … tl)
     389  ] fl st3.
     390  cases (tna_non_empty … tl) [@prf|%]
     391  qed.
     392*)
     393
     394inductive trace_any_any (S : abstract_status) : S → S → Type[0] ≝
     395  | taa_base : ∀st.trace_any_any S st st
     396  | taa_step : ∀st1,st2,st3.
     397    as_execute S st1 st2 →
     398    as_classifier S st1 cl_other →
     399    ¬as_costed S st2 →
     400    trace_any_any S st2 st3 →
     401    trace_any_any S st1 st3.
     402
     403definition taa_non_empty ≝ λS,st1,st2.λtaa : trace_any_any S st1 st2.
    354404  match taa with
    355   [ taa_base st1' ⇒ [st1']
    356   | taa_step st1' st2' st3' _ tl _ _ ⇒ st1' :: taa_status_list … tl
     405  [ taa_base _ ⇒ false
     406  | taa_step _ _ _ _ _ _ _ ⇒ true
    357407  ].
    358408
    359 let rec taa_append_taa S st1 st2 st3 (taa1 : trace_any_any S st1 st2)
    360   on taa1 : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝
    361   match taa1
    362   return λst1,st2.λx : trace_any_any S st1 st2.
    363     trace_any_any S st2 st3 → trace_any_any S st1 st3
    364   with
    365   [ taa_base _ ⇒ λtaa2.taa2
    366   | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
    367       taa_step … H (taa_append_taa … tl taa2) G K
    368   ].
    369 
    370 let rec taa_append_tal S st1 fl st2 st3 (taa : trace_any_any S st1 st2)
    371   on taa :
     409coercion taa_to_bool : ∀S,st1,st2.∀taa:trace_any_any S st1 st2.bool ≝
     410 taa_non_empty on _taa : trace_any_any ??? to bool.
     411
     412let rec taa_append_tal S st1 fl st2 st3
     413  (taa : trace_any_any S st1 st2) on taa :
    372414  trace_any_label S fl st2 st3 →
    373415  trace_any_label S fl st1 st3 ≝
    374   match taa
    375   return λst1,st2.λx : trace_any_any S st1 st2.
    376     trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3
     416  match taa return λst1,st2.λx : trace_any_any S st1 st2.
     417    ∀fl,st3.
     418    trace_any_label S fl st2 st3 →
     419    trace_any_label S fl st1 st3
    377420  with
    378   [ taa_base _ ⇒ λtaa2.taa2
    379   | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
    380       tal_step_default … H (taa_append_tal … tl taa2) G K
    381   ].
     421  [ taa_base st1' ⇒ λfl,st3,tal2.tal2
     422  | taa_step st1' st2' st3' H G K tl ⇒ λfl,st3,tal2.
     423    tal_step_default ????? H (taa_append_tal ????? tl tal2) G K
     424  ] fl st3.
     425
     426interpretation "trace any any label append" 'append taa tal = (taa_append_tal ????? taa tal).
    382427
    383428let rec tlr_rel S1 st1 st1' S2 st2 st2'
     
    416461    fl2 = doesnt_end_with_ret ∧
    417462    ∃st2mid,taa,H,G,K.
    418     tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
     463    tal2 ≃ taa_append_tal ? st2 ??? taa
    419464      (tal_base_not_return ? st2mid st2' H G K)
    420465  | tal_base_return st1 st1' _ _ ⇒
     
    437482    tal_rel … tl1 tal2 (* <- this makes it many to many *)
    438483  ].
    439  
     484
    440485interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2).
    441486interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2).
    442 interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ???????? t1 t2).
    443 
     487interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ?????? t1 t2).
     488
     489let rec taa_rel_inv S1 fl1 st1 st1mid st1' S2 fl2 st2 st2'
     490  (taa1 : trace_any_any S1 st1 st1mid) on taa1 :
     491  ∀tal1 : trace_any_label S1 fl1 st1mid st1'.
     492  ∀tal2 : trace_any_label S2 fl2 st2 st2'.
     493  tal_rel … (taa1 @ tal1) tal2 →
     494  tal_rel … tal1 tal2 ≝ ?.
     495cases taa1 -taa1
     496[ -taa_rel_inv //
     497| #st #st' #st'' #H #G #K #tl #tal1 #tal2 whd in ⊢ (%→?);
     498  @(taa_rel_inv … tl)
     499]
     500qed.
     501
     502let rec tlr_rel_transitive S1 st1 st1' S2 st2 st2' S3 st3 st3'
     503  (tlr1 : trace_label_return S1 st1 st1')
     504  (tlr2 : trace_label_return S2 st2 st2')
     505  (tlr3 : trace_label_return S3 st3 st3') on tlr1 :
     506  tlr_rel … tlr1 tlr2 → tlr_rel … tlr2 tlr3 → tlr_rel … tlr1 tlr3 ≝
     507match tlr1 with
     508  [ tlr_base st1' st1'' tll1 ⇒ ?
     509  | tlr_step st1' st1'' st1''' tll1 tl1 ⇒ ?
     510  ]
     511and tll_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3'
     512  (tll1 : trace_label_label S1 fl1 st1 st1')
     513  (tll2 : trace_label_label S2 fl2 st2 st2')
     514  (tll3 : trace_label_label S3 fl3 st3 st3') on tll1 :
     515  tll1 ≈ tll2 → tll2 ≈ tll3 → tll1 ≈ tll3 ≝
     516  match tll1 with
     517  [ tll_base fl1' st1' st1'' tal1 H ⇒ ?
     518  ]
     519and tal_rel_transitive S1 fl1 st1 st1' S2 fl2 st2 st2' S3 fl3 st3 st3'
     520  (tal1 : trace_any_label S1 fl1 st1 st1')
     521  (tal2 : trace_any_label S2 fl2 st2 st2')
     522  (tal3 : trace_any_label S3 fl3 st3 st3') on tal1 :
     523  tal1 ≈ tal2 → tal2 ≈ tal3 → tal1 ≈ tal3 ≝
     524  match tal1 with
     525  [ tal_base_not_return st1' st1'' H G K ⇒ ?
     526  | tal_base_return st1' st1'' H G ⇒ ?
     527  | tal_base_call st1' st1'' st1''' H G K tlr1 L ⇒ ?
     528  | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
     529  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
     530  ].
     531[1,2: cases tlr2 #st2' #st2'' [1,3: #tllhd2 |2,4: #st2''' #tllhd2 #tlrtl2]
     532  [2,3: *] normalize in ⊢ (%→?); [ #Rhd12 | * #Rhd12 #Rtl12 ]
     533  cases tlr3 #st3' #st3'' [1,3: #tllhd3 |2,4: #st3''' #tllhd3 #tlrtl3]
     534  [2,3: *] normalize in ⊢ (%→?); [ #Rhd23 | * #Rhd23 #Rtl23 ] whd
     535  [ @(tll_rel_transitive … Rhd12 Rhd23) |
     536    %{(tll_rel_transitive … Rhd12 Rhd23)}
     537    @(tlr_rel_transitive … Rtl12 Rtl23)
     538  ]
     539|3:
     540  cases tll2 #fl2' #st2' #st2'' #tal2 #H2 * #G2 #R12
     541  cases tll3 #fl3' #st3' #st3'' #tal3 #H3 * #G3 #R23
     542  %{(tal_rel_transitive … R12 R23)} //
     543|*:
     544  [1,2,3: * #EQ]
     545  [5: whd in ⊢ (%→?→%); @tal_rel_transitive]
     546  *#st2mid *#taa2
     547  [ *#H2 *#G2 *#K2 #R12
     548  | *#H2 *#G2 #R12
     549  | *#st2' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#R12 #R12'
     550  | *#st2' *#st2'' *#H2 *#G2 *#K2 *#tlr2 *#L2 *#tl2 ** #R12 #R12' #R12''
     551  ] destruct #R23 lapply (taa_rel_inv … R23) [1,2: // |3: *#EQ destruct]
     552  *#st3mid *#taa3
     553  [ *#st3' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#R23 #R23'
     554    %{(refl …)} %{st3mid} %{taa3} %{st3'} %{H3} %{G3} %{K3} %{tlr3} %{L3}
     555    %{R23} @(tlr_rel_transitive … R12' R23')
     556  | *#st3' *#st3'' *#H3 *#G3 *#K3 *#tlr3 *#L3 *#tl3 ** #R23 #R23' #R23''
     557    %{st3mid} %{taa3} %{st3'} %{st3''} %{H3} %{G3} %{K3} %{tlr3} %{L3} %{tl3}
     558    %{(tal_rel_transitive … R12'' R23'')}
     559    %{R23} @(tlr_rel_transitive … R12' R23')
     560  ]
     561]
     562qed.
    444563
    445564let rec flatten_trace_label_label
     
    507626  S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa :
    508627  ∀tal : trace_any_label S fl st2 st3.
    509     flatten_trace_any_label … (taa_append_tal … taa tal) =
     628    flatten_trace_any_label … (taa @ tal) =
    510629      flatten_trace_any_label … tal ≝ ?.
    511630cases taa -st1 -st2
    512 [ #st1 #tal %
    513 | #st_pre #st_init #st2 #H #taa #G #K #tal
    514   whd in match (taa_append_tal ???????);
     631[ //
     632| #st_pre #st_init #st2 #H #G #K #taa' #tal
     633  whd in match (? @ ?);
    515634  whd in ⊢ (??%?); //
    516635]
    517 qed. 
    518 
     636qed.
    519637
    520638let rec tll_rel_to_traces_same_flatten
     
    606724  λS : abstract_status. (Σl.∃pc.as_label_of_pc S pc = Some ? l) → ℕ.
    607725
    608 definition lift_cost_map_id :
    609   ∀S_in, S_out: abstract_status.
    610    (∀l. (∃pc.as_label_of_pc S_out pc = Some … l) +
    611        ¬(∃pc.as_label_of_pc S_out pc = Some … l)) →
    612   (as_cost_map S_out) → as_cost_map S_in ≝ λS_in,S_out,dec,m,l_sig.
    613    match dec l_sig with
    614    [ inl prf ⇒ m «l_sig, prf»
    615    | inr _ ⇒ 0 (* labels not present in out code get 0 *)
     726definition lift_sigma_map_id :
     727  ∀A,B : Type[0].∀P_in,P_out : A → Prop.B →
     728    (∀a.P_out a + ¬ P_out a) →
     729  ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig.
     730   match dec a_sig with
     731   [ inl prf ⇒ m «a_sig, prf»
     732   | inr _ ⇒ dflt (* labels not present in out code get 0 *)
    616733   ].
    617734
    618 lemma lift_cost_map_id_eq :
    619   ∀S_in, S_out, dec, m, l_in, l_out.
    620   pi1 ?? l_in = pi1 ?? l_out → lift_cost_map_id S_in S_out dec m l_in = m l_out.
    621 #S_in #S_out #dec #m #l_in * #l_out #prf #EQ
    622 whd in match lift_cost_map_id; normalize nodelta
    623 cases (dec l_in) normalize nodelta >EQ
    624 [2: #H @⊥] /2 by refl, absurd/
     735lemma lift_sigma_map_id_eq :
     736  ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out.
     737  pi1 ?? a_in = pi1 ?? a_out →
     738  lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out.
     739#A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ
     740whd in match lift_sigma_map_id; normalize nodelta
     741cases (dec a_in) normalize nodelta >EQ cases a_out
     742#a #H #G [ % | @⊥ /2 by absurd/ ]
    625743qed.
    626744
     
    631749  with precedence 20
    632750for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
     751
     752definition lift_cost_map_id :
     753  ∀S_in,S_out : abstract_status.? →
     754  as_cost_map S_out → as_cost_map S_in
     755  ≝
     756 λS_in,S_out : abstract_status.
     757  lift_sigma_map_id costlabel ℕ
     758    (λl.∃pc.as_label_of_pc S_in pc = Some ? l)
     759    (λl.∃pc.as_label_of_pc S_out pc = Some ? l)
     760    0.
    633761
    634762lemma lift_cost_map_same_cost :
     
    645773  #EQ destruct
    646774  whd in ⊢(??%%);
    647   >(lift_cost_map_id_eq … e0)
     775  whd in match lift_cost_map_id; normalize nodelta
     776  >(lift_sigma_map_id_eq ????????? e0)
    648777  >e0 in e1; normalize in ⊢(%→?); #EQ
    649778  >(IH … EQ) %
Note: See TracChangeset for help on using the changeset viewer.