Changeset 3524 for LTS/Traces.ma


Ignore:
Timestamp:
Mar 11, 2015, 4:26:40 PM (5 years ago)
Author:
piccolo
Message:

rearrangments of lemmas, final statement in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3523 r3524  
    1717include "basics/deqsets.ma".
    1818include "../src/ASM/Util.ma".
     19
     20(*LABELS*)
    1921
    2022inductive FunctionName : Type[0] ≝
     
    3941coercion a_non_functional_label.
    4042
    41 (*
    42 definition ret_act_label_to_cost_label :
    43 (ReturnPostCostLabel + NonFunctionalLabel) → CostLabel ≝
    44 λx.match x with [inl a ⇒ a_return_post a | inr b ⇒ a_non_functional_label b].
    45 
    46 coercion ret_act_label_to_cost_label.
    47 
    48 definition call_act_label_to_cost_label :
    49 (CallCostLabel + NonFunctionalLabel) → CostLabel ≝
    50 λx.match x with [inl a ⇒ a_call a | inr b ⇒ a_non_functional_label b].
    51 
    52 coercion call_act_label_to_cost_label.
    53 *)
    54 
    5543definition eq_nf_label : NonFunctionalLabel → NonFunctionalLabel → bool ≝
    5644λx,y.match x with [ a_non_functional_label n ⇒
     
    181169    eq_costlabel p1 p2 ≡ eqb X p1 p2.
    182170
    183    
    184 
    185 
    186171inductive ActionLabel : Type[0] ≝
    187172 | call_act : FunctionName → CallCostLabel → ActionLabel
     
    192177λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
    193178
     179definition is_non_silent_cost_act : ActionLabel → Prop ≝
     180λact. ∃l. act = cost_act (Some ? l).
     181
     182definition is_cost_act : ActionLabel → Prop ≝
     183λact.∃l.act = cost_act l.
     184
     185definition is_call_act : ActionLabel → Prop ≝
     186λact.∃f,l.act = call_act f l.
     187
     188definition is_labelled_ret_act : ActionLabel → Prop ≝
     189λact.∃l.act = ret_act (Some ? l).
     190
     191definition is_unlabelled_ret_act : ActionLabel → Prop ≝
     192λact.act = ret_act (None ?).
     193
     194definition is_costlabelled_act : ActionLabel → Prop ≝
     195λact.match act with [ call_act _ _ ⇒ True
     196                    | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
     197                    | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
     198                    ].
     199                   
     200lemma is_costlabelled_act_elim :
     201∀P : ActionLabel → Prop.
     202(∀l. is_costlabelled_act l → P l) →
     203(∀l. ¬is_costlabelled_act l → P l) →
     204∀l.P l.
     205#P #H1 #H2 * /2/
     206[ * /2/ @H2 % *] * /2/ @H2 %*
     207qed.
     208
     209
     210(*ABSTRACT STATUS*)
     211
    194212inductive status_class : Type[0] ≝
    195213 | cl_jump : status_class
    196214 | cl_io : status_class
    197215 | cl_other : status_class.
    198 
    199 definition is_non_silent_cost_act : ActionLabel → Prop ≝
    200 λact. ∃l. act = cost_act (Some ? l).
    201 
     216 
    202217record abstract_status : Type[2] ≝
    203218 { as_status :> Type[0]
     
    216231     as_execute l s1 s2 → is_non_silent_cost_act l
    217232 }.
    218  (*
    219 definition is_act_io_entering : abstract_status → ActionLabel → bool ≝
    220 λS,l.match l with
    221 [ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_entering S c' ]
    222 | ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false
    223                                                    | inr c' ⇒ is_io_entering S c']
    224                            | None ⇒ false
    225                            ]
    226 | cost_act x ⇒ match x with [ Some c ⇒ is_io_entering S c | None ⇒ false ]
    227 | init_act ⇒ false
    228 ].
    229 
    230 definition is_act_io_exiting : abstract_status → ActionLabel → bool ≝
    231 λS,l.match l with
    232 [ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_exiting S c' ]
    233 | ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false
    234                                                    | inr c' ⇒ is_io_exiting S c']
    235                            | None ⇒ false
    236                            ]
    237 | cost_act x ⇒ match x with [ Some c ⇒ is_io_exiting S c | None ⇒ false ]
    238 | init_act ⇒ false
    239 ].
    240 *)
     233
     234(* RAW TRACES *)
    241235
    242236inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
     
    245239             as_execute S l st1 st2 → raw_trace S st2 st3 →
    246240             raw_trace S st1 st3.
    247 
    248 definition is_cost_act : ActionLabel → Prop ≝
    249 λact.∃l.act = cost_act l.
    250 
    251 definition is_call_act : ActionLabel → Prop ≝
    252 λact.∃f,l.act = call_act f l.
    253 
    254 definition is_labelled_ret_act : ActionLabel → Prop ≝
    255 λact.∃l.act = ret_act (Some ? l).
    256 
    257 definition is_unlabelled_ret_act : ActionLabel → Prop ≝
    258 λact.act = ret_act (None ?).
    259 
    260 definition is_costlabelled_act : ActionLabel → Prop ≝
    261 λact.match act with [ call_act _ _ ⇒ True
    262                     | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
    263                     | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
    264                     ].
    265 (*
    266 lemma well_formed_trace_inv :
    267 ∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2.
    268 well_formed_trace … t →
    269 (st1 = st2 ∧ t ≃ t_base S st1) ∨
    270 (∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2.
    271 well_formed_trace … tl ∧ as_classify … st1 ≠ cl_jump ∧
    272 t ≃ t_ind … prf … tl) ∨
    273 (∃st1'.∃l.∃ prf : as_execute S l st1 st1'.∃ tl : raw_trace S st1' st2.
    274  well_formed_trace … tl ∧ is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl). (* ∨
    275 (∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2.
    276  well_formed_trace … tl ∧ as_classify … st1 = cl_io ∧
    277  is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl).*)
    278 #S #st1 #st2 #t #H inversion H
    279 [ #st #EQ1 #EQ2 destruct(EQ1 EQ2) #EQ destruct(EQ) #_ /5 by refl_jmeq, or_introl, conj/
    280 | #st1' #st2' #st3' #l #prf' #tl' #Htl #Hclass #_ #EQ2 #EQ3 #EQ4 destruct #_
    281   %  %2 %{st2'} %{l} %{prf'} %{tl'} /4 by conj/
    282 | #st1' #st2' #st3' #l #prf #tl #Htl #Hl #_ #EQ2 #EQ3 #EQ4 destruct #_ %2 %{st2'}
    283   %{l} %{prf} %{tl} % // % //
    284 (*| #st1' #st2' #st3' #l #prf #tl #Htl #Hclass #is_non_silent #_ #EQ1 #EQ2 #EQ3
    285   destruct #_ %2 %{st2'} %{l} %{prf} %{tl} /5 by conj/ *)
    286 ]
    287 qed.
    288 
    289 *)
    290241
    291242let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
     
    300251interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2).
    301252
     253lemma append_nil_is_nil : ∀S : abstract_status.
     254∀s1,s2 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s1.
     255t1 @ t2 = t_base … s1 → s1 = s2 ∧ t1 ≃ t_base … s1 ∧ t2 ≃ t_base … s1.
     256#S #s1 #s2 #t1 elim t1 -t1 -s1 -s2
     257[ #st #t2 normalize #EQ destruct /3 by refl_jmeq, conj/]
     258#s1 #s2 #s3 #l #prf #t2 #IH #t2 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     259qed.
     260
    302261lemma append_associative : ∀S,st1,st2,st3,st4.
    303262∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
     
    314273raw_trace … st1 st3 → Prop≝
    315274λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
     275
     276let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
     277(t : raw_trace S st1 st2) on t : list CostLabel ≝
     278match t with
     279[ t_base st ⇒ [ ]
     280| t_ind st1' st2' st3' l prf t' ⇒
     281    let tl ≝ get_costlabels_of_trace … t' in
     282    match l with
     283    [ call_act f c ⇒ [ c ]
     284    | ret_act x ⇒ match x with
     285                  [ Some c ⇒ [ a_return_post c ]
     286                  | None ⇒ []
     287                  ]
     288    | cost_act x ⇒ match x with
     289                  [ Some c ⇒ [ a_non_functional_label c ]
     290                  | None ⇒ []
     291                  ]
     292   ] @ tl
     293].
     294
     295lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.
     296∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
     297get_costlabels_of_trace … (t1 @ t2) =
     298 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
     299#S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
     300[#f * #l | * [| * #l] | *  [| #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH
     301qed.
     302
     303lemma append_tind_commute : ∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
     304    ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
     305    ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2.
     306#S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.
     307
     308lemma get_costlabelled_is_costlabelled :
     309∀S : abstract_status.∀s1,s2,s3 : S. ∀l.
     310∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
     311is_costlabelled_act l →
     312|get_costlabels_of_trace … (t_ind … prf t)| = 1 + |get_costlabels_of_trace … t|.
     313#S #s1 #s2 #s3 * normalize
     314  [ /2 by monotonic_pred/
     315  | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
     316  | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
     317  ]
     318qed.
     319
     320(*SILENT TRACES*)
    316321
    317322inductive pre_silent_trace (S : abstract_status) :
     
    339344qed.
    340345
    341 (*
    342 definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
    343 raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧
    344 well_formed_trace … t.
    345 
    346 lemma silent_is_well_formed : ∀S : abstract_status.∀st1,st2 : S.
    347 ∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t.
    348 #S #st1 #st2 #t * //
    349 qed. *)
    350 (* elim t -t
    351 [ #st #_ %]
    352 #st1' #st2' #st3' #l #prf #tl #IH * #H #cl %2
    353 [2: >cl % #EQ destruct]
    354 @IH inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
    355 #st1'' #st2'' #st3'' #prf' #tl' #H1 #Htl' #_ #EQ1 #EQ2 #EQ3 destruct #_
    356 % [ assumption | #_ assumption]
    357 qed.*)
     346lemma append_silent : ∀S : abstract_status.
     347∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.
     348∀t2 : raw_trace … s2 s3.silent_trace … t1 →
     349silent_trace … t2 →
     350silent_trace … (t1 @ t2).
     351#S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
     352[ #st #t2 #_ * /2 by or_introl, or_intror/ ]
     353#st1 #st2 #st3 #l #prf #tl #IH #t2 *
     354[2: * #H cases(H I) ] #H inversion H in ⊢ ?;
     355[ #st #H1 #H2 #H3 #H4 #H5 #H6 destruct ]
     356#st1' #st2' #st3' #prf' #tl' #Hst1' #Htl' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     357#Ht2 % %2 // cases(IH … Ht2) /2/
     358inversion(tl' @ t2)
     359[2: #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 * #H cases (H I) ]
     360#st #EQ1 #EQ2 destruct #H cases(append_nil_is_nil … H) * #EQ1 #EQ2 #EQ3 destruct //
     361qed.
     362
     363lemma silent_append_l2 : ∀S : abstract_status.
     364∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
     365silent_trace … (t1 @ t2) → silent_trace … t2.
     366#S #s1 #s2 #s3 #t1 elim t1 // -s1 -s2
     367#st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)]
     368#H @IH % inversion H in ⊢ ?;
     369[ #H42 #H43 #H44 #H45 normalize #H46 #H47 destruct
     370| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 normalize in H59; destruct assumption
     371]
     372qed.
     373
     374lemma silent_append_l1 : ∀S : abstract_status.
     375∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
     376silent_trace … (t1 @ t2) → silent_trace … t1.
     377#S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
     378[ #st #t2 #_ %2 % *]
     379#st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)] #H
     380% inversion H in ⊢ ?; [ #H62 #H63 #H64 #H65 #H66 #H67 normalize in H66; destruct]
     381#z1 #z2 #z3 #prf' #tl' #Hclass #Htl' #_ #EQ1 #EQ2 #EQ3 normalize in EQ3; #EQ4 destruct
     382%2 // cases(IH t2 …) /2/ inversion tl
     383[2: #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 destruct cases H79 #H cases(H I) ]
     384#st #EQ1 #EQ2 #EQ3 destruct #_ % normalize in Htl'; inversion Htl'
     385[ #H81 #H82 #H83 #H84 #H85 #H86 destruct //
     386| #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 destruct //
     387]
     388qed.
     389
     390lemma get_cost_label_silent_is_empty : ∀S : abstract_status.
     391∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
     392#S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
     393#H inversion H
     394[#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
     395destruct #_ @IH % assumption
     396qed.
     397
     398lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
     399∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
     400silent_trace … t1 →
     401get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
     402#S #st1 #st2 #st3 #t1 elim t1
     403[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 *
     404[2: whd in match is_trace_non_empty; normalize nodelta * #ABS @⊥ @ABS %]
     405#H inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
     406#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
     407#_ whd in ⊢ (??%?); >IH [%] %1 assumption
     408qed.
     409
     410lemma silent_suffix_cancellable : ∀S : abstract_status.
     411∀s1,s2,s2',s3,s3',s4 : S.∀l,l'.
     412∀t1 : raw_trace … s1 s2. ∀prf : as_execute … l s2 s3.
     413∀t2 : raw_trace … s3 s4.
     414∀t1' :raw_trace … s1 s2'.∀prf' : as_execute … l' s2' s3'.
     415∀t2' : raw_trace … s3' s4.
     416is_costlabelled_act l → is_costlabelled_act l' →
     417silent_trace … t2 → silent_trace … t2' →
     418t1 @ (t_ind … prf t2) = t1' @ (t_ind … prf' t2') →
     419s2 = s2' ∧ l = l' ∧ t1 ≃ t1'.
     420#S #s1 #s2 #s2' #s3 #s3' #s4 #l #l' #t1 #prf #t2 #t1' #prf' #t2' #Hl #Hl' #sil_t2 #sil_t2'
     421lapply prf -prf lapply prf' -prf' lapply t1' -t1' elim t1
     422[ normalize #st * normalize
     423  [ #st' #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct /3/
     424  | #st1 #st2 #st3 #lbl #prf1 #tl #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     425    @⊥ lapply(silent_append_l2 … sil_t2) * [2: * #H cases(H I)] #H inversion H
     426    [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
     427    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl'
     428    ]
     429  ]
     430]
     431#st1 #st2 #st3 #lbl #prf1 #tl #IH #t1' inversion t1' in ⊢ ?;
     432[ #st #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     433  @⊥ lapply(silent_append_l2 … sil_t2') * [2: * #H cases(H I)] #H inversion H
     434    [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
     435    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl
     436    ]
     437| #st1' #st2' #st3' #lbl' #prf1' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize
     438  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct -EQ cases(IH … e0) * #EQ1 #EQ2 #EQ3 destruct /3/
     439]
     440qed.
     441
     442(*PRE-MEASURABLE TRACES*)
    358443
    359444inductive pre_measurable_trace (S : abstract_status) :
     
    419504qed.
    420505
     506lemma append_premeasurable_silent : ∀S : abstract_status.
     507∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
     508pre_measurable_trace … t → silent_trace … t' → 
     509pre_measurable_trace … (t' @ t).
     510#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
     511[ #st #t #Hpre #_ whd in ⊢ (????%); assumption]
     512#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?;
     513[ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
     514#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
     515destruct #_ whd in ⊢ (????%); %2
     516[ assumption
     517| %{(None ?)} %
     518| @IH try assumption
     519]
     520% assumption
     521qed.
     522
     523lemma pre_silent_is_premeasurable : ∀S : abstract_status.
     524∀st1,st2 : S. ∀t : raw_trace S st1 st2.pre_silent_trace … t
     525→ pre_measurable_trace … t.
     526#S #st1 #st2 #t elim t
     527[ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
     528#st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
     529-t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H in ⊢ ?;
     530[ #st #H2 #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
     531#_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
     532@IH assumption
     533qed.
     534
     535lemma append_silent_premeasurable : ∀S : abstract_status.
     536∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
     537pre_measurable_trace … t' → silent_trace … t →
     538pre_measurable_trace … (t' @ t).
     539#S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
     540[ #st #Hst #r * [ #H1 @pre_silent_is_premeasurable assumption ]
     541  inversion r [2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 cases H11
     542  #ABS @⊥ @ABS % ] #s' #EQ1 #EQ2 #EQ3 destruct #_
     543  %1 assumption
     544|2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct
     545  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ]
     546  try ( %{x} %) try @IH try assumption % ]
     547#s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
     548#EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
     549#r #pre_r normalize
     550>append_tind_commute >append_tind_commute >append_associative
     551<append_tind_commute in ⊢ (????(??????%)); %5
     552try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
     553qed.
     554
     555lemma head_of_premeasurable_is_not_io : ∀S : abstract_status.
     556∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
     557as_classify … st1 ≠ cl_io.
     558#S #st1 #st2 #t #H inversion H //
     559qed.
     560
     561lemma get_costlabels_of_trace_empty : ∀S : abstract_status.∀s1,s2 : S.∀t : raw_trace … s1 s2.
     562get_costlabels_of_trace … t = nil ? → pre_measurable_trace … t → silent_trace … t.
     563#S #s1 #s2 #t elim t [ #st #_ #_ %2 % * ] #st1 #st2 #st3 #l #prf #t' #IH #EQ #H -s1 -s2 inversion H
     564[ #H1 #H2 #H3 #H4 #H5 #H6 destruct
     565| #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     566| #s1 #s2 #s3 #l1 #Hclass #prf1 #tl * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     567| #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #f * #c #EQ destruct #Hs1 #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     568| #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hclass1 #Hclass3 * #f * #c #EQ destruct #Hs1
     569  #pre1 #pre2 #Hs1s4 whd in match is_unlabelled_ret_act; normalize nodelta #EQ destruct #_ #_ #EQ1 #EQ2 #EQ3 #EQ4
     570  destruct
     571]
     572whd in EQ : (??%?); destruct cases lbl in prf1 EQ; -lbl normalize [2: #lbl #H #EQ destruct]
     573#prf #H % %2 // cases(IH …) // cases tl in pre_meas_tl;
     574[2: #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 cases(absurd ?? H87) %]
     575#st #H1 #_ % /2 by head_of_premeasurable_is_not_io/
     576qed.
     577
     578(*NO-IO TRACES*)
     579
     580inductive no_io_trace (S : abstract_status) : ∀st1,st2 : S.raw_trace … st1 st2 → Prop ≝
     581  t_base_io :∀st : S.as_classify … st ≠ cl_io →  no_io_trace S … (t_base … st)
     582| t_ind_io : ∀st1,st2,st3 : S.∀l,prf.∀tl : raw_trace … st2 st3.as_classify … st1 ≠ cl_io →
     583                   no_io_trace … tl → no_io_trace … (t_ind … st1 … l prf tl).
     584
     585lemma no_io_append : ∀S : abstract_status.
     586∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
     587∀t2 : raw_trace … st2 st3.
     588no_io_trace … t1 → no_io_trace … t2 →
     589no_io_trace … (t1 @ t2).
     590#S #st1 #st2 #st3 #t1 lapply st3 elim t1
     591[ #st #st3 #t2 #_ //]
     592#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
     593[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 destruct ]
     594#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #_ destruct
     595#H3 %2 // @IH //
     596qed.
     597
     598lemma pre_measurable_no_io : ∀S : abstract_status.
     599∀st1,st2 : S. ∀t : raw_trace … st1 st2.
     600pre_measurable_trace … t →
     601no_io_trace … t.
     602#S #st1 #st2 #t #H elim H /2/ -st1-st2
     603#st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf' #H1 #H2 #H3 #H4 #pre1 #pre2 #H5
     604#H6 #IH1 #IH2 %2 // @no_io_append // %2 //
     605qed.
     606
     607lemma head_of_no_io_is_no_io : ∀S : abstract_status.
     608∀st1,st2 : S. ∀t : raw_trace … st1 st2.
     609no_io_trace … t → as_classify … st1 ≠ cl_io.
     610#S #st1 #st2 #t #H elim H //
     611qed.
     612
     613
     614lemma no_io_append_l1 : ∀S : abstract_status.
     615∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
     616∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) →
     617no_io_trace … t1.
     618#S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H % /2/]
     619#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
     620[ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
     621#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct
     622%2 // @IH //
     623qed.
     624
     625lemma no_io_append_l2 : ∀S : abstract_status.
     626∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
     627∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) →
     628no_io_trace … t2.
     629#S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H assumption ]
     630#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H @IH inversion H in ⊢ ?;
     631[ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
     632#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct //
     633qed.
     634
     635(*MEASURABLE TRACES*)
     636
    421637definition measurable :
    422638 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝
     
    429645 ∧ silent_trace … ti0 ∧ silent_trace … t3n.
    430646
    431 let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
    432 (t : raw_trace S st1 st2) on t : list CostLabel ≝
    433 match t with
    434 [ t_base st ⇒ [ ]
    435 | t_ind st1' st2' st3' l prf t' ⇒
    436     let tl ≝ get_costlabels_of_trace … t' in
    437     match l with
    438     [ call_act f c ⇒ [ c ]
    439     | ret_act x ⇒ match x with
    440                   [ Some c ⇒ [ a_return_post c ]
    441                   | None ⇒ []
    442                   ]
    443     | cost_act x ⇒ match x with
    444                   [ Some c ⇒ [ a_non_functional_label c ]
    445                   | None ⇒ []
    446                   ]
    447    ] @ tl
    448 ].
    449 
    450 lemma get_cost_label_silent_is_empty : ∀S : abstract_status.
    451 ∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
    452 #S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
    453 #H inversion H
    454 [#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
    455 destruct #_ @IH % assumption
    456 qed.
    457 
    458 lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.
    459 ∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
    460 get_costlabels_of_trace … (t1 @ t2) =
    461  append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
    462 #S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
    463 [#f * #l | * [| * #l] | *  [| #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH
    464 qed.
    465647 
     648definition measurable_prefix ≝ 
     649λS : abstract_status.
     650λs1,s4 :S.
     651λt : raw_trace … s1 s4.
     652∃s2,s3 : S.∃t12 : raw_trace … s1 s2.
     653∃l.∃prf : as_execute … l s2 s3.
     654∃t34 : raw_trace … s3 s4.
     655silent_trace … t12 ∧ t = t12 @ (t_ind … prf t34) ∧ is_costlabelled_act l.
     656
     657lemma measurable_prefix_of_premeasurable :
     658∀S : abstract_status.
     659∀s1,s4 : S.
     660∀t : raw_trace … s1 s4.
     661pre_measurable_trace … t →
     662get_costlabels_of_trace … t ≠ nil ? →
     663measurable_prefix … t.
     664#S #s1 #s4 #t elim t
     665[ #st #_ * #H @⊥ @H %]
     666#st1 #st2 #st3 #l @(is_costlabelled_act_elim … l) -l
     667[ #l #Hl #prf #t' #IH #_ #_ %{st1} %{st2} %{(t_base …)} %{l} %{prf} %{t'}
     668  % // % // %2 normalize % *]
     669#l #Hl #prf #t' #IH #H inversion H
     670[ #st #H1 #H2 #H3 #H4 #H5 destruct
     671| #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     672  cases l2 in Hl Hl2 prf2;
     673  [ #f #c #_ * #z #EQ destruct
     674  | * [|#lbl] #_ * #z #EQ destruct
     675  | * [|#lbl * #H cases(H I)]
     676  ]
     677| #x1 #x2 #x3 #l2 #Hclass #prf2 #tl #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     678  cases l2 in Hl Hl2 prf2;
     679  [ #f #c #_ * #z #EQ destruct
     680  | #lbl1 #H1 * #z #EQ destruct cases H1 -H1 #H1 @⊥ @H1 %
     681  | #lbl #_ * #z #EQ destruct
     682  ]
     683| #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #Hpost #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     684  cases l2 in Hl Hl2 prf2;
     685  [ #f #c * #H @⊥ @H %
     686  | #lbl1 #_ * #z * #z1 #EQ destruct
     687  | #lbl #_ * #z * #z1 #EQ destruct
     688  ]
     689| #x1 #x2 #x3 #x4 #x5 #l2 #l3 #prf2 #tl1 #tl2 #prf3 #Hclass1 #Hclass2 #Hl2 #Hx1 #pre1 #pre2 #succ #Hl3
     690  #_ #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     691  cases l2 in Hl Hl2 prf2;
     692  [ #f #c * #H @⊥ @H %
     693  | #lbl1 #_ * #z * #z1 #EQ destruct
     694  | #lbl #_ * #z * #z1 #EQ destruct
     695  ]
     696]
     697#_ #_ #prf #H1 cases(IH pre_tl ?)
     698[2: % #EQ whd in H1 : (?(??%?)); >EQ in H1; * #H @H % ]
     699#s2 * #s3 * #t12 * #l1 * #prf1 * #t34 ** #H2 #H3 #H4 %{s2} %{s3} %{(t_ind … prf t12)}
     700%{l1} %{prf1} %{t34} % // %
     701[ % %2 // cases H2 // inversion t12 [2: #z1 #z2 #z3 #lbl #prf5 #tl1 #_ #EQ1 #EQ2 #E3 destruct * #H @⊥ @H // ]
     702  #st #EQ1 #EQ2 #EQ3 destruct #_ % /2 by head_of_premeasurable_is_not_io/
     703| >H3 //
     704]
     705qed.
     706
     707definition measurable_suffix ≝
     708 λS : abstract_status.λs1,s1' : S.λt : raw_trace … s1 s1'.
     709∃s1_em : S.
     710∃t_pre_em : raw_trace … s1 s1_em.
     711∃s1_postem : S.
     712     ∃t_post_em : raw_trace … s1_postem s1'.
     713     silent_trace S ?? t_post_em ∧
     714     ∃l_em : ActionLabel.
     715     ∃ex_em : as_execute … l_em s1_em s1_postem.
     716     t = t_pre_em @ (t_ind … ex_em t_post_em) ∧
     717     (is_call_act l_em → bool_to_Prop(is_call_post_label … s1_em)) ∧
     718     is_costlabelled_act l_em.
     719     
     720
     721lemma measurable_suffix_tind : ∀S : abstract_status.
     722∀s1,s2,s3 : S.∀l : ActionLabel.∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
     723measurable_suffix … (t_ind … prf t) → (is_costlabelled_act l \wedge silent_trace … t) ∨ measurable_suffix … t.
     724#S #s1 #s2 #s3 #l #prf #t lapply prf -prf lapply s1 -s1 cases t -t -s2 -s3
     725[ #st #st1 #prf * #s_em * #t_pre * #s_post * #t_post * #sil_post * #l_em * #ex_em **
     726 inversion t_pre in ⊢ ?;
     727 [#st' #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     728  #_ /4 by or_introl, conj/
     729 | #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct normalize in H34;
     730   lapply(eq_to_jmeq ??? H34) -H34 #H34 destruct inversion H29 in ⊢ ?;
     731   [ #H38 #H39 #H40 #H41 destruct
     732   | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 destruct normalize in e1; destruct
     733   ]
     734 normalize in e0; destruct
     735]
     736]
     737#s1 #s2 #s3 #l1 #prf1 #tl #s4 #prf * #s_em * #t_post lapply prf -prf cases t_post -t_post
     738[ #s5 #prf * #s_post * #t_post * #sil_tpost * #l_em * #prf2 ** #EQ normalize in EQ;
     739  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct /4/
     740| #s5 #s6 #s7 #lbl #prf2 #tl1 #prf3 * #s_post * #t_post * #sil_tpost * #l_em * #ex_em **
     741  #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost %2
     742  >e0 whd %{s7} %{tl1} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/
     743]
     744qed.
     745
     746lemma measurable_suffix_append : ∀S : abstract_status.
     747∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
     748measurable_suffix … t2 → measurable_suffix … (t1 @ t2).
     749#S #s1 #s2 #s3 #t1 #t2 * #s_em * #pre_t * #s_post * #t_post
     750* #sil_tpost * #l_em * #prf ** #EQ destruct #Hcall #Hcost
     751%{s_em} %{(t1@pre_t)} %{s_post} %{t_post} /7 by ex_intro, conj/
     752qed.
     753
     754lemma measurable_suffix_append_l1 : ∀S : abstract_status.
     755∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
     756measurable_suffix … (t1 @ t2) → silent_trace … t2 → measurable_suffix … t1.
     757#S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
     758[#st #t2 * #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em * #exe ** #EQ normalize in EQ; destruct
     759 #Hcall #Hcost #H lapply(silent_append_l2 … H) -H * [2: * #H cases(H I)] #H inversion H
     760 [ #H113 #H114 #H115 #H116 #H117 #H118 destruct ]
     761 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 destruct cases Hcost
     762]
     763#st1 #st2 #st3 #l #prf #tl #IH #t2 * #s_em * #t_pre inversion t_pre in ⊢ ?;
     764[ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em
     765  * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     766  #Hcall #Hcost #sil_t2 %{st} %{(t_base …)} %{s_post} %{tl} % [ /2 by silent_append_l1/]
     767  %{l_em} %{ex_em} /4 by refl, conj/
     768| #s #s' #s'' #l' #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em
     769  ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost #H
     770  change with ((t_ind ?????? (t_base …)) @ tl) in ⊢ (????%); @measurable_suffix_append @(IH t2) //
     771  %{s''} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} % // % assumption
     772]
     773qed.
     774
     775lemma measurable_suffix_append_case : ∀S : abstract_status.
     776∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
     777measurable_suffix … (t1 @ t2) → (measurable_suffix … t1 ∧ silent_trace … t2) ∨ measurable_suffix … t2.
     778#S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
     779[ #st #t2 #H %2 assumption]
     780#st1 #st2 #st3 #l #prf #tl #IH #t2 whd in match (append_on_trace ??????); #Hsuff
     781cases(measurable_suffix_tind … Hsuff)
     782[ * #_ #H %% [2: /2 by silent_append_l2/]  change with ((t_ind ?????? tl) @ t2) in Hsuff : (????%);
     783 @(measurable_suffix_append_l1 … Hsuff) /2/
     784| #H cases(IH … H)
     785  [ * #H1 #H2 %% // change with ((t_ind ?????? (t_base …)) @ tl) in ⊢ (????%); @measurable_suffix_append //
     786  | /2/
     787  ]
     788]
     789qed.
     790
     791lemma measurable_is_measurable_suffix : ∀S : abstract_status.
     792∀si,s1,s3,sn : S. ∀t : raw_trace … si sn.measurable …s1 s3 … t → measurable_suffix … t.
     793#S #si #s1 #s3 #sn #t * #_ * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 *****
     794#EQ destruct /11 width=20 by conj,ex_intro/
     795qed.
     796
     797lemma prefix_of_measurable_suffix_is_premeasurable : ∀S : abstract_status.
     798∀s1,s2,s3,s4 :S.∀l.∀prf : as_execute … l s2 s3.
     799∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s3 s4.∀t : raw_trace … s1 s4.
     800pre_measurable_trace … t → t = (t1 @ (t_ind … prf t2)) → is_costlabelled_act l →
     801silent_trace … t2 → (is_call_act l → bool_to_Prop(is_call_post_label … s2)) →
     802pre_measurable_trace … t1.
     803#S #s1 #s2 #s3 #s4 #l #prf #t1 #t2 #t #H lapply t1 -t1 lapply t2 -t2 lapply prf -prf lapply s2 -s2
     804lapply s3 -s3 elim H -t -s1 -s4
     805[ #st #_ #s1 #s2 #prf #r #p inversion p in ⊢ ?;
     806  [ #H1 #H2 #H3 #H4 destruct #H5 #H6 #H7 normalize in H5; lapply(eq_to_jmeq ??? H5) -H5 #H5 destruct
     807  | #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 destruct
     808    normalize in H19; lapply(eq_to_jmeq ??? H19) -H19 #H19 destruct
     809  ]
     810| #st1 #st2 #st3 #lbl #prf #tl #Hclass **
     811  [ #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?;
     812    [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     813      destruct *
     814    | #s3 #s4 #s5 #lab #exe #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?);
     815      #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/
     816    ]
     817  | #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?;
     818    [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     819      destruct #_ #_ #_ % //
     820    | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
     821      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/
     822   ]
     823 ]
     824| #st1 #st2 #st3 #lbl #Hclass #prf #tl * #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1
     825  #t1 #t2 inversion t2 in ⊢ ?;
     826  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     827    destruct #_ #_ #_ % //
     828  | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
     829      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %3 /2/ @(IH … (refl …)) /2/
     830  ]
     831| #st1 #st2 #st3 #lbl #prf #tl #Hclass * #f * #c #EQ destruct #call_post #pre_tl #IH #s1 #s2 #prf1
     832  #t1 #t2 inversion t2 in ⊢ ?;
     833  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     834    destruct #_ #_ #_ % //
     835  | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
     836      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %4 /3/ @(IH … (refl …)) /2/
     837  ]
     838| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hst1 #Hst3 * #f * #c #EQ destruct
     839  #Hcall #pre_t1 #pre_t2 #succ whd in ⊢ (% → ?); #EQ destruct #IH1 #IH2 #s1 #s2 #prf3
     840  #t3 #t4 inversion t4 in ⊢ ?;
     841  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     842    destruct #_ #_ #_ % //
     843  | #s3 #s4 #s5 #lbl #prf4 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
     844    lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t3 #H1
     845    cut(measurable_suffix … (t1@(t_ind … prf2 t2)))
     846    [ whd %{s5} %{tail} %{s1} %{t3} %{sil_t3} %{l} %{prf3} /4 by jmeq_to_eq, conj/]
     847    #Hmeas cases(measurable_suffix_append_case … Hmeas)
     848    [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
     849      [ #H4 #H5 #H6 #H7 #H8 #H9 destruct
     850      | #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
     851      ]
     852    | -Hmeas #Hmeas cases(measurable_suffix_tind … Hmeas)
     853      [ **] -Hmeas -IH1 -EQ * #s_em * #t_pre * #s_post * #t_post * #sil_tpost
     854      * #l_em * #ex_em ** #EQ destruct #H1 #H2
     855      change with (t_ind … (t_base …) @ ?) in match (t_ind ???????) in e0;
     856      <append_associative in e0; <append_associative #e0
     857      cases(silent_suffix_cancellable … e0) // -e0 * #EQ1 #EQ2 #EQ3 destruct
     858      >append_associative %5 /2/ [ %{f} %{c} //] normalize
     859      @(IH2 … (refl …)) /2/
     860     ]
     861   ]
     862 ]
     863qed.
     864
     865lemma measurable_suffix_is_measurable:
     866∀S : abstract_status.
     867∀s1,s4 : S.
     868∀t : raw_trace … s1 s4.
     869pre_measurable_trace … t →
     8702 ≤ |get_costlabels_of_trace … t | →
     871measurable_suffix … t → ∃s1,s3.
     872measurable … s1 … s3 … t.
     873#S #s1 #s4 #t #pre_meas_t #Hlab * #s_em * #t_pre * #s_init * #t_post * #sil_tpost
     874* #l_em * #ex_em ** #EQ destruct #Hcall #Hcost_lem
     875>get_cost_label_append in Hlab; >append_length >get_costlabelled_is_costlabelled //
     876>(get_cost_label_silent_is_empty … sil_tpost) #CARD
     877cases(measurable_prefix_of_premeasurable … t_pre)
     878[3: cases(get_costlabels_of_trace ????) in CARD; [ /3/ | #c #xc #_ % #EQ destruct]
     879|2: @(prefix_of_measurable_suffix_is_premeasurable … pre_meas_t) [5: %|*:] assumption
     880| #s_prefix * #s_post_pre * #t_prefix * #lab * #exe1 * #t34 ** #sil_tprefix #EQ destruct #cost_lab
     881  /20 width=20 by conj,ex_intro/
     882]
     883qed.
Note: See TracChangeset for help on using the changeset viewer.