Ignore:
Timestamp:
Mar 1, 2013, 11:06:29 AM (7 years ago)
Author:
tranquil
Message:
  • changed primitives of abstract status (with stuf that is probably already there in all of its implementations): this temporarily breaks current as creations
  • generalised stacksize file and consequently moved it to common
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r2553 r2755  
    1 include "basics/types.ma".
     1 include "basics/types.ma".
    22include "basics/bool.ma".
    33include "basics/jmeq.ma".
     
    66include "basics/lists/listb.ma".
    77include "ASM/Util.ma".
     8include "common/IO.ma".
     9include "utilities/hide.ma".
    810
    911inductive status_class: Type[0] ≝
     
    1618record abstract_status : Type[1] ≝
    1719  { as_status :> Type[0]
    18   ; as_execute : as_status → as_status → Prop
     20  ; as_eval : as_status → IO io_out io_in as_status
    1921  ; as_pc : DeqSet
    2022  ; as_pc_of : as_status → as_pc
     
    2224  ; as_label_of_pc : as_pc → option costlabel
    2325  ; as_after_return : (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop
    24   ; as_final: as_status → Prop
     26  ; as_result: as_status → option int
    2527  ; as_call_ident : (Σs:as_status.as_classify s = Some ? cl_call) → ident
    2628  ; as_tailcall_ident : (Σs:as_status.as_classify s = Some ? cl_tailcall) → ident
     
    2931definition as_classifier ≝ λS,s,cl.as_classify S s = Some ? cl.
    3032definition as_call ≝ λS,s,f.as_call_ident S s = f.
     33definition as_final ≝ λS,s.as_result S s ≠ None ?.
     34definition as_execute ≝ λS,s1,s2.as_eval S s1 = Value … s2.
    3135
    3236definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc ? (as_pc_of ? s).
     
    3741definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
    3842  λa_s,st.as_label ? st ≠ None ?.
    39 
    40 definition as_label_safe : ∀a_s : abstract_status.
    41   (Σs : a_s.as_costed ? s) → costlabel ≝
    42   λa_s,st_sig.opt_safe … (pi2 … st_sig).
    4343
    4444lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) + (¬as_costed S s).
     
    6363
    6464definition as_cost_label ≝
    65   λS : abstract_status. Σl.as_cost_labelled S l.
     65  λS : abstract_status. Σl.as_cost_labelled S l.
     66
     67unification hint 0 ≔ S ⊢ as_cost_label S ≡ Sig costlabel (λl.as_cost_labelled S l).
    6668
    6769definition as_cost_labels ≝
     
    7678definition as_cost_map ≝
    7779  λS : abstract_status. (as_cost_label S) → ℕ.
     80 
     81definition as_label_safe : ∀a_s : abstract_status.
     82  (Σs : a_s.as_costed ? s) → as_cost_label a_s ≝
     83  λa_s,st_sig.«opt_safe ?? (pi2 … st_sig), ?».
     84@hide_prf
     85@opt_safe_elim #c #EQ %{EQ} qed.
    7886 
    7987definition lift_sigma_map_id :
     
    599607    match tll2 with
    600608    [ tll_base fl2 st2 st2 tal2 G ⇒
    601       as_label_safe … («?, H») = as_label_safe … («?, G») ∧
     609      pi1 … (as_label_safe … («?, H»)) = pi1 … (as_label_safe … («?, G»)) ∧
    602610      tal_rel … tal1 tal2
    603611    ]
     
    726734qed.
    727735
    728 let rec flatten_trace_label_label
     736inductive intensional_event : Type[0] ≝
     737| IEVcost : costlabel → intensional_event
     738| IEVcall : ident → intensional_event
     739| IEVtailcall : ident → ident → intensional_event
     740| IEVret : ident → intensional_event.
     741
     742(* NB: we don't restrict call idents, because it would need some more tinkering
     743   with abstract_status *)
     744definition as_emittable : abstract_status → intensional_event → Prop ≝
     745λS,ev.
     746match ev with
     747[ IEVcost c ⇒ as_cost_labelled S c
     748| _ ⇒ True
     749].
     750 
     751definition as_trace ≝
     752λS : abstract_status.
     753Σl : list intensional_event.All … (as_emittable S) l.
     754
     755unification hint 0 ≔ S ⊢ as_trace S ≡ Sig (list intensional_event) (λl.All … (as_emittable S) l).
     756
     757definition cons_safe : ∀A,P.(Σx.P x) → (Σl.All A P l) → Σl.All A P l ≝
     758λA,P,x,l.«x::l, conj … (pi2 … x) (pi2 … l)».
     759
     760definition append_safe : ∀A,P.(Σl.All A P l) → (Σl.All A P l) → Σl.All A P l ≝
     761λA,P,l1,l2.«l1@l2,
     762  cic:/matita/cerco/utilities/lists/All_append.def(2) … (pi2 … l1) (pi2 … l2)».
     763
     764definition nil_safe : ∀A,P.(Σl.All A P l) ≝ λA,P.«[ ], I».
     765
     766interpretation "safe consing" 'vcons hd tl = (cons_safe ?? hd tl).
     767interpretation "safe appending" 'vappend l1 l2 = (append_safe ?? l1 l2).
     768interpretation "safe nil" 'vnil = (nil_safe ??).
     769
     770definition emittable_cost : ∀S.as_cost_label S → Σev.as_emittable S ev ≝
     771λS,l.«IEVcost l, pi2 … l».
     772
     773let rec observables_trace_label_label
    729774  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
    730775    (start_status: S) (final_status: S)
    731776      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
    732         on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
     777      (curr : ident)
     778        on the_trace: as_trace S ≝
    733779  match the_trace with
    734780  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    735       let label ≝
    736         match as_label … initial return λx: option costlabel. x ≠ None ? → ? with
    737         [ None ⇒ λabs. ⊥
    738         | Some l ⇒ λ_. l
    739         ] labelled_proof
    740       in
    741         (mk_Sig … label ?)::flatten_trace_any_label S ends_flag initial final given_trace
    742   ]
    743 and flatten_trace_any_label
     781      let label ≝ as_label_safe … «?, labelled_proof» in
     782      emittable_cost … label ::: observables_trace_any_label S ends_flag initial final given_trace curr
     783  ]
     784and observables_trace_any_label
    744785  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
    745786    (start_status: S) (final_status: S)
    746787      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
    747         on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
     788      (curr : ident)
     789        on the_trace: as_trace S ≝
    748790  match the_trace with
    749   [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
    750   | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
    751       flatten_trace_label_return … call_trace
    752   | tal_base_tailcall pre_fun_call start_fun_call final _ _ call_trace ⇒
    753       flatten_trace_label_return … call_trace
    754   | tal_base_return the_status _ _ _ ⇒ [ ]
     791  [ tal_base_not_return the_status _ _ _ _ ⇒ [[ ]]
     792  | tal_base_call pre_fun_call start_fun_call final _ cl _ call_trace _ ⇒
     793      let id ≝ as_call_ident ? «?, cl» in
     794      IEVcall id ::: observables_trace_label_return ??? call_trace id
     795  | tal_base_tailcall pre_fun_call start_fun_call final _ cl call_trace ⇒
     796      let id ≝ as_tailcall_ident ? «?, cl» in
     797      IEVtailcall curr id ::: observables_trace_label_return … call_trace id
     798  | tal_base_return the_status _ _ _ ⇒ [[ IEVret curr]]
    755799  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    756     _ _ _ call_trace _ final_trace ⇒
    757     let call_cost_trace ≝ flatten_trace_label_return … call_trace in
    758     let final_cost_trace ≝ flatten_trace_any_label … end_flag … final_trace in
    759         call_cost_trace @ final_cost_trace
     800    _ cl _ call_trace _ final_trace ⇒
     801    let id ≝ as_call_ident ? «?, cl» in
     802    let call_cost_trace ≝ observables_trace_label_return … call_trace id in
     803    let final_cost_trace ≝ observables_trace_any_label … end_flag … final_trace curr in
     804    IEVcall id ::: call_cost_trace @@ final_cost_trace
    760805  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    761       flatten_trace_any_label … tail_trace
    762   ]
    763 and flatten_trace_label_return
     806    observables_trace_any_label … tail_trace curr
     807  ]
     808and observables_trace_label_return
    764809  (S: abstract_status)
    765810    (start_status: S) (final_status: S)
    766811      (the_trace: trace_label_return S start_status final_status)
    767         on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
     812      (curr : ident)
     813        on the_trace: as_trace S ≝
    768814  match the_trace with
    769815  [ tlr_base before after trace_to_lift ⇒
    770       flatten_trace_label_label … trace_to_lift
     816      observables_trace_label_label … trace_to_lift curr
    771817  | tlr_step initial labelled final labelled_trace ret_trace ⇒
    772     let labelled_cost ≝ flatten_trace_label_label … doesnt_end_with_ret … labelled_trace in
    773     let return_cost ≝ flatten_trace_label_return … ret_trace in
    774         labelled_cost @ return_cost
    775   ].
    776   [2:
    777     cases abs -abs #abs @abs %
    778   |1:
    779     %{(as_pc_of … initial)} whd in match label;
    780     change with (as_label ?? = ?)
    781     generalize in match labelled_proof; whd in ⊢ (% → ?);
    782     cases (as_label S initial)
    783     [1:
    784       #absurd @⊥ cases absurd -absurd #absurd @absurd %
    785     |2:
    786       #costlabel normalize nodelta #_ %
    787     ]
    788   ]
    789 qed.
     818    let labelled_cost ≝ observables_trace_label_label … doesnt_end_with_ret … labelled_trace curr in
     819    let return_cost ≝ observables_trace_label_return … ret_trace curr in
     820        labelled_cost @@ return_cost
     821  ]. % qed.
     822 
     823let rec filter_map X Y (f : X → option Y) (l : list X) on l : list Y ≝
     824match l with
     825[ nil ⇒ [ ]
     826| cons hd tl ⇒
     827  match f hd with
     828  [ Some y ⇒ [ y ]
     829  | None ⇒ [ ]
     830  ] @ filter_map … f tl
     831].
     832
     833lemma map_to_filter_map : ∀X,Y,f,l.map X Y f l = filter_map X Y (λx.Some ? (f x)) l.
     834#X #Y #f #l elim l normalize // qed.
     835
     836lemma filter_map_compose : ∀X,Y,Z,f,g,l.
     837filter_map Y Z f (filter_map X Y g l) =
     838  filter_map X Z (λx.! y ← g x ; f y) l.
     839#X #Y #Z #f #g #l elim l [%]
     840#hd #tl #IH
     841whd in ⊢ (??(????%)%);
     842 cases (g ?) normalize nodelta
     843 [2: #y >m_return_bind whd in ⊢ (??%?); @eq_f2 [ % ]]
     844@IH
     845qed.
     846
     847lemma filter_map_ext_eq : ∀X,Y,f,g,l.
     848  (∀x.f x = g x) → filter_map X Y f l = filter_map X Y g l.
     849#X #Y #f #g #l #H elim l normalize [%] #hd #tl #IH >H @eq_f @IH qed.
     850
     851let rec list_distribute_sig_aux X P (l : list X) on l : All X P l → list (Σx.P x) ≝
     852match l return λl.All X P l → list (Σx.P x) with
     853[ nil ⇒ λ_.[ ]
     854| cons hd tl ⇒ λprf.«hd, proj1 … prf» :: list_distribute_sig_aux X P tl (proj2 … prf)
     855].
     856
     857definition list_distribute_sig : ∀A,P.(Σl.All A P l) → list (Σx.P x) ≝
     858λA,P,l.list_distribute_sig_aux … l (pi2 … l).
     859
     860let rec list_factor_sig X P (l : list (Σx.P x)) on l : Σl.All X P l ≝
     861match l with
     862[ nil ⇒ [[ ]]
     863| cons hd tl ⇒ hd ::: list_factor_sig … tl
     864].
     865
     866definition costlabels_of_observables : ∀S.as_trace S → list (as_cost_label S) ≝
     867λS,l.filter_map (Σev.as_emittable S ev) ?
     868  (λev.match ev return λev.as_emittable S ev → option ? with
     869    [ IEVcost c ⇒ λprf.Some ? «c, prf»
     870    | _ ⇒ λ_.None ?
     871    ] (pi2 … ev)) (list_distribute_sig … l).
    790872
    791873(* JHM: base case now passes the termination checker *)
    792 let rec taa_append_tal_same_flatten
     874let rec taa_append_tal_same_observables
    793875  S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa :
    794   ∀tal : trace_any_label S fl st2 st3.
    795     flatten_trace_any_label … (taa @ tal) =
    796       flatten_trace_any_label … tal ≝ ?.
     876  ∀tal : trace_any_label S fl st2 st3.∀curr.
     877    observables_trace_any_label ???? (taa @ tal) curr =
     878      observables_trace_any_label ???? tal curr ≝ ?.
    797879cases taa -st1 -st2
    798 [ #st #tal normalize in ⊢ (??%?); //
    799 | #st_pre #st_init #st2 #H #G #K #taa' #tal
     880[ #st #tal #curr normalize in ⊢ (??%?); //
     881| #st_pre #st_init #st2 #H #G #K #taa' #tal #curr
    800882  whd in match (? @ ?);
    801883  whd in ⊢ (??%?); //
     
    803885qed.
    804886
    805 let rec tal_collapsable_flatten S fl st1 st2 tal
     887let rec tal_collapsable_observables S fl st1 st2 tal
    806888  on tal :
    807   tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ] ≝
     889  ∀curr.
     890  tal_collapsable S fl st1 st2 tal → observables_trace_any_label … tal curr = [ ] ≝
     891λcurr.
    808892match tal
    809 return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ]
     893return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → observables_trace_any_label … tal curr = [ ]
    810894with
    811895[ tal_base_not_return the_status _ _ _ _ ⇒ λ_.refl ??
    812896| tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    813     tal_collapsable_flatten ???? tail_trace
     897  tal_collapsable_observables ???? tail_trace curr
    814898| _ ⇒ Ⓧ
    815899].
    816900
    817 let rec tll_rel_to_traces_same_flatten
     901let rec tll_rel_to_traces_same_observables
    818902  (S: abstract_status) (S': abstract_status)
    819903    (trace_ends_flag_l: trace_ends_with_ret) (trace_ends_flag_r: trace_ends_with_ret)
     
    821905      (the_trace_l: trace_label_label S trace_ends_flag_l start_status_l final_status_l)
    822906        (the_trace_r: trace_label_label S' trace_ends_flag_r start_status_r final_status_r)
     907        (curr : ident)
    823908          on the_trace_l:
    824909            tll_rel … the_trace_l the_trace_r →
    825               map … (pi1 …) (flatten_trace_label_label … the_trace_l) =
    826                 map … (pi1 …) (flatten_trace_label_label … the_trace_r) ≝
     910              pi1 … (observables_trace_label_label … the_trace_l curr) =
     911                pi1 … (observables_trace_label_label … the_trace_r curr) ≝
    827912  match the_trace_l with
    828913  [ tll_base fl1 st1 st1' tal1 H ⇒
     
    831916    ]
    832917  ]
    833 and tal_rel_to_traces_same_flatten
     918and tal_rel_to_traces_same_observables
    834919  (S: abstract_status) (S': abstract_status) (trace_ends_flag_l: trace_ends_with_ret)
    835920    (trace_ends_flag_r: trace_ends_with_ret)
     
    837922        (the_trace_l: trace_any_label S trace_ends_flag_l start_status_l final_status_l)
    838923          (the_trace_r: trace_any_label S' trace_ends_flag_r start_status_r final_status_r)
     924          (curr : ident)
    839925          on the_trace_l:
    840926            tal_rel … the_trace_l the_trace_r →
    841               map … (pi1 …) (flatten_trace_any_label … the_trace_l) =
    842                 map … (pi1 …) (flatten_trace_any_label … the_trace_r) ≝
     927              pi1 … (observables_trace_any_label … the_trace_l curr) =
     928                pi1 … (observables_trace_any_label … the_trace_r curr) ≝
    843929  match the_trace_l with
    844930  [ tal_base_not_return st1 st1' H G K ⇒ ?
     
    849935  | tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ?
    850936  ]
    851 and tlr_rel_to_traces_same_flatten
     937and tlr_rel_to_traces_same_observables
    852938  (S: abstract_status) (S': abstract_status) (start_status_l: S) (final_status_l: S)
    853939    (start_status_r: S') (final_status_r: S')
    854940      (the_trace_l: trace_label_return S start_status_l final_status_l)
    855941        (the_trace_r: trace_label_return S' start_status_r final_status_r)
     942        (curr : ident)
    856943        on the_trace_l:
    857944          tlr_rel … the_trace_l the_trace_r →
    858             map … (pi1 …) (flatten_trace_label_return … the_trace_l) =
    859               map … (pi1 …) (flatten_trace_label_return … the_trace_r) ≝
     945            pi1 … (observables_trace_label_return … the_trace_l curr) =
     946              pi1 … (observables_trace_label_return … the_trace_r curr) ≝
    860947  match the_trace_l with
    861948  [ tlr_base before after tll_l ⇒ ?
    862949  | tlr_step initial labelled final tll_l tlr_l ⇒ ?
    863950  ]. 
    864 [ * whd in match as_label_safe; normalize nodelta
    865   @opt_safe_elim #l1 #EQ1
    866   @opt_safe_elim #l2 #EQ2
    867   #EQ destruct(EQ) #H_tal
    868   change with (? :: ? = ? :: ?) lapply H -H lapply G -G
    869   whd in match as_costed; normalize nodelta
    870   >EQ1 >EQ2 normalize nodelta #_ #_
    871   >(tal_rel_to_traces_same_flatten … H_tal) @refl
     951[ * #EQ #H_tal
     952  whd in ⊢ (??%%); @eq_f2 [2: @(tal_rel_to_traces_same_observables … H_tal)]
     953  cases (as_label_safe ??) in EQ; #c1 #H1
     954  cases (as_label_safe ??) #c2 #H2 #EQ destruct %
    872955|2,3,4,5,6,7:
    873956  [1,2,3,4: * #EQ destruct(EQ)]
     
    881964      [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#K' *#tlr2 *#L'
    882965      [| *#tl2] ** #EQ #H_tl #H_tlr
    883     ] >EQ >taa_append_tal_same_flatten
    884   | whd in ⊢ (%→??(????%)?);
    885     @tal_rel_to_traces_same_flatten
    886   ]
     966    ] >EQ >taa_append_tal_same_observables
     967  | whd in ⊢ (%→??(???%)?); @tal_rel_to_traces_same_observables
     968  ]
     969  whd in ⊢ (??%%);
    887970  [1,2: %
    888   |3,5: @(tlr_rel_to_traces_same_flatten … H_tlr)
    889   |4,6: <map_append
    890     >(tal_collapsable_flatten … H_tl) >append_nil
    891     >(tlr_rel_to_traces_same_flatten … H_tlr) %
    892   |7: <map_append
    893     >(tlr_rel_to_traces_same_flatten … H_tlr)
    894     >(tal_rel_to_traces_same_flatten … H_tl)
    895     @map_append
     971  |3,5: >call >(tlr_rel_to_traces_same_observables … H_tlr) %
     972  |4,6: >call >(tal_collapsable_observables … H_tl) >append_nil
     973    >(tlr_rel_to_traces_same_observables … H_tlr) %
     974  |7: >call
     975    >(tlr_rel_to_traces_same_observables … H_tlr)
     976    >(tal_rel_to_traces_same_observables … H_tl)
     977    %
    896978  ]
    897979|*: cases the_trace_r
    898980  [1,3: #st_before_r #st_after_r #tll_r
    899     [ @tll_rel_to_traces_same_flatten | * ]
     981    [ @tll_rel_to_traces_same_observables | * ]
    900982  |*: #st_init_r #st_labld_r #st_fin_r #tll_r #tlr_r *
    901983    #H_tll #H_tlr
    902     <map_append
    903     >(tll_rel_to_traces_same_flatten … H_tll)
    904     >(tlr_rel_to_traces_same_flatten … H_tlr)
    905     @map_append
     984    whd in ⊢ (??%%);
     985    >(tll_rel_to_traces_same_observables … H_tll)
     986    >(tlr_rel_to_traces_same_observables … H_tlr)
     987    %
    906988  ]
    907989]
     
    910992(* cost maps specifics: summing over flattened traces *)
    911993
    912 lemma lift_cost_map_same_cost_tal :
     994(* lemma lift_cost_map_same_cost_tal :
    913995  ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out.
    914996  ∀the_trace_in : trace_any_label S_in f_in start_in end_in.
     
    9351017@(lift_cost_map_same_cost … (tll_rel_to_traces_same_flatten … H_tll))
    9361018qed.
     1019*)
     1020
     1021lemma map_pi1_distribute_sig : ∀A,P,l.
     1022  map ?? (pi1 ??) (list_distribute_sig A P l) = pi1 ?? l.
     1023#A #P * #l elim l -l normalize // qed.
     1024
     1025definition flatten_trace_label_return ≝
     1026  λS,st1,st2.λtlr : trace_label_return S st1 st2.
     1027  (* as cost events do not depend on current function identifier, we
     1028     can use a dummy one *)
     1029  let dummy ≝ an_identifier ? one in
     1030  costlabels_of_observables … (observables_trace_label_return … tlr dummy).
     1031
     1032definition flatten_trace_label_label ≝
     1033  λS,flag,st1,st2.λtll : trace_label_label S flag st1 st2.
     1034  (* as cost events do not depend on current function identifier, we
     1035     can use a dummy one *)
     1036  let dummy ≝ an_identifier ? one in
     1037  costlabels_of_observables … (observables_trace_label_label … tll dummy).
    9371038
    9381039lemma lift_cost_map_same_cost_tlr :
     
    9461047#S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out
    9471048#tlr_in #tlr_out #H_tlr
    948 @(lift_cost_map_same_cost … (tlr_rel_to_traces_same_flatten … H_tlr))
    949 qed.
     1049@lift_cost_map_same_cost
     1050whd in match flatten_trace_label_return; normalize nodelta
     1051>map_to_filter_map >map_to_filter_map >filter_map_compose
     1052>filter_map_compose
     1053cut (∀S.∀x: (Σev.as_emittable S ev).
     1054  ! y ←
     1055    match pi1 ?? x return λx.as_emittable S x → option (Σc.as_cost_labelled S c) with
     1056    [ IEVcost c ⇒ λprf.Some ? «c, prf» | _ ⇒ λ_.None ? ] (pi2 ?? x) ;
     1057  Some ? (pi1 ?? y) =
     1058  ! ev ← Some ? (pi1 ?? x) ;
     1059  match ev with [ IEVcost c ⇒ Some ? c | _ ⇒ None ?])
     1060[ #S ** [ #c #em | #i * | #i #j * | #i * ] %]
     1061#EQext >(filter_map_ext_eq … (EQext S_in)) >(filter_map_ext_eq … (EQext S_out))
     1062<filter_map_compose <filter_map_compose @eq_f
     1063<map_to_filter_map <map_to_filter_map
     1064>map_pi1_distribute_sig >map_pi1_distribute_sig
     1065@(tlr_rel_to_traces_same_observables … H_tlr) %
     1066qed.
     1067
     1068lemma lift_cost_map_same_cost_tll :
     1069  ∀S_in, S_out, dec, m_out, fl_in, fl_out, start_in, start_out, end_in, end_out.
     1070  ∀the_trace_in : trace_label_label S_in fl_in start_in end_in.
     1071  ∀the_trace_out : trace_label_label S_out fl_out start_out end_out.
     1072  tll_rel … the_trace_in the_trace_out →
     1073  (Σ_{l ∈ flatten_trace_label_label … the_trace_in}
     1074    (lift_cost_map_id … dec m_out l)) =
     1075  (Σ_{l ∈ flatten_trace_label_label … the_trace_out} (m_out l)).
     1076#S_in #S_out #dec #m_out #fl_in #fl_out #start_in #start_out #end_in #end_out
     1077#tlr_in #tlr_out #H_tlr
     1078@lift_cost_map_same_cost
     1079whd in match flatten_trace_label_label; normalize nodelta
     1080>map_to_filter_map >map_to_filter_map >filter_map_compose
     1081>filter_map_compose
     1082cut (∀S.∀x: (Σev.as_emittable S ev).
     1083  ! y ←
     1084    match pi1 ?? x return λx.as_emittable S x → option (Σc.as_cost_labelled S c) with
     1085    [ IEVcost c ⇒ λprf.Some ? «c, prf» | _ ⇒ λ_.None ? ] (pi2 ?? x) ;
     1086  Some ? (pi1 ?? y) =
     1087  ! ev ← Some ? (pi1 ?? x) ;
     1088  match ev with [ IEVcost c ⇒ Some ? c | _ ⇒ None ?])
     1089[ #S ** [ #c #em | #i * | #i #j * | #i * ] %]
     1090#EQext >(filter_map_ext_eq … (EQext S_in)) >(filter_map_ext_eq … (EQext S_out))
     1091<filter_map_compose <filter_map_compose @eq_f
     1092<map_to_filter_map <map_to_filter_map
     1093>map_pi1_distribute_sig >map_pi1_distribute_sig
     1094@(tll_rel_to_traces_same_observables … H_tlr) %
     1095qed.
Note: See TracChangeset for help on using the changeset viewer.