Changeset 3524 for LTS/Final.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/Final.ma

    r3523 r3524  
    1414
    1515include "Simulation.ma".
    16 include "Vm.ma".
    17 
    18 inductive no_io_trace (S : abstract_status) : ∀st1,st2 : S.raw_trace … st1 st2 → Prop ≝
    19   t_base_io :∀st : S.as_classify … st ≠ cl_io →  no_io_trace S … (t_base … st)
    20 | t_ind_io : ∀st1,st2,st3 : S.∀l,prf.∀tl : raw_trace … st2 st3.as_classify … st1 ≠ cl_io →
    21                    no_io_trace … tl → no_io_trace … (t_ind … st1 … l prf tl).
    22 
    23 lemma no_io_append : ∀S : abstract_status.
    24 ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
    25 ∀t2 : raw_trace … st2 st3.
    26 no_io_trace … t1 → no_io_trace … t2 →
    27 no_io_trace … (t1 @ t2).
    28 #S #st1 #st2 #st3 #t1 lapply st3 elim t1
    29 [ #st #st3 #t2 #_ //]
    30 #s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
    31 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 destruct ]
    32 #st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #_ destruct
    33 #H3 %2 // @IH //
    34 qed.
    35 
    36 lemma pre_measurable_no_io : ∀S : abstract_status.
    37 ∀st1,st2 : S. ∀t : raw_trace … st1 st2.
    38 pre_measurable_trace … t →
    39 no_io_trace … t.
    40 #S #st1 #st2 #t #H elim H /2/ -st1-st2
    41 #st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf' #H1 #H2 #H3 #H4 #pre1 #pre2 #H5
    42 #H6 #IH1 #IH2 %2 // @no_io_append // %2 //
    43 qed.
    44 
    45 lemma head_of_no_io_is_no_io : ∀S : abstract_status.
    46 ∀st1,st2 : S. ∀t : raw_trace … st1 st2.
    47 no_io_trace … t → as_classify … st1 ≠ cl_io.
    48 #S #st1 #st2 #t #H elim H //
    49 qed.
    50 
    51 
    52 lemma no_io_append_l1 : ∀S : abstract_status.
    53 ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
    54 ∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) →
    55 no_io_trace … t1.
    56 #S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H % /2/]
    57 #s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
    58 [ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
    59 #st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct
    60 %2 // @IH //
    61 qed.
    62 
    63 lemma no_io_append_l2 : ∀S : abstract_status.
    64 ∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
    65 ∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) →
    66 no_io_trace … t2.
    67 #S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H assumption ]
    68 #s #s' #s'' #l #prf #tl #IH #st3 #t2 #H @IH inversion H in ⊢ ?;
    69 [ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
    70 #st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct //
    71 qed.
    72 
    73 lemma is_costlabelled_act_elim :
    74 ∀P : ActionLabel → Prop.
    75 (∀l. is_costlabelled_act l → P l) →
    76 (∀l. ¬is_costlabelled_act l → P l) →
    77 ∀l.P l.
    78 #P #H1 #H2 * /2/
    79 [ * /2/ @H2 % *] * /2/ @H2 %*
    80 qed.
    81 
    82 (*
    83 lemma append_silent_premeasurable_l : ∀S : abstract_status.
    84 ∀st1,st2,st3,st4 : S.∀t1 : raw_trace … st1 st2.∀l,prf.
    85 ∀t2 : raw_trace … st3 st4.
    86 pre_measurable_trace … (t1 @ (t_ind … l prf t2)) →
    87 as_classify … st2 ≠ cl_io.
    88 #S #st1 #st2 #st3 #st4 #t1 lapply st4 lapply st3 -st3 -st4 elim t1
    89 [ #st #st3 #st4 #l #prf #t2 #H @(head_of_premeasurable_is_not_io … H)
    90 | #st' #st'' #st''' #l1 #prf #tl #IH
    91 *)
    92 
    93 definition measurable_prefix ≝ 
    94 λS : abstract_status.
    95 λs1,s4 :S.
    96 λt : raw_trace … s1 s4.
    97 ∃s2,s3 : S.∃t12 : raw_trace … s1 s2.
    98 ∃l.∃prf : as_execute … l s2 s3.
    99 ∃t34 : raw_trace … s3 s4.
    100 silent_trace … t12 ∧ t = t12 @ (t_ind … prf t34) ∧ is_costlabelled_act l.
    101 
    102 lemma measurable_prefix_of_premeasurable :
    103 ∀S : abstract_status.
    104 ∀s1,s4 : S.
    105 ∀t : raw_trace … s1 s4.
    106 pre_measurable_trace … t →
    107 get_costlabels_of_trace … t ≠ nil ? →
    108 measurable_prefix … t.
    109 #S #s1 #s4 #t elim t
    110 [ #st #_ * #H @⊥ @H %]
    111 #st1 #st2 #st3 #l @(is_costlabelled_act_elim … l) -l
    112 [ #l #Hl #prf #t' #IH #_ #_ %{st1} %{st2} %{(t_base …)} %{l} %{prf} %{t'}
    113   % // % // %2 normalize % *]
    114 #l #Hl #prf #t' #IH #H inversion H
    115 [ #st #H1 #H2 #H3 #H4 #H5 destruct
    116 | #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
    117   cases l2 in Hl Hl2 prf2;
    118   [ #f #c #_ * #z #EQ destruct
    119   | * [|#lbl] #_ * #z #EQ destruct
    120   | * [|#lbl * #H cases(H I)]
    121   ]
    122 | #x1 #x2 #x3 #l2 #Hclass #prf2 #tl #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
    123   cases l2 in Hl Hl2 prf2;
    124   [ #f #c #_ * #z #EQ destruct
    125   | #lbl1 #H1 * #z #EQ destruct cases H1 -H1 #H1 @⊥ @H1 %
    126   | #lbl #_ * #z #EQ destruct
    127   ]
    128 | #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #Hpost #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
    129   cases l2 in Hl Hl2 prf2;
    130   [ #f #c * #H @⊥ @H %
    131   | #lbl1 #_ * #z * #z1 #EQ destruct
    132   | #lbl #_ * #z * #z1 #EQ destruct
    133   ]
    134 | #x1 #x2 #x3 #x4 #x5 #l2 #l3 #prf2 #tl1 #tl2 #prf3 #Hclass1 #Hclass2 #Hl2 #Hx1 #pre1 #pre2 #succ #Hl3
    135   #_ #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
    136   cases l2 in Hl Hl2 prf2;
    137   [ #f #c * #H @⊥ @H %
    138   | #lbl1 #_ * #z * #z1 #EQ destruct
    139   | #lbl #_ * #z * #z1 #EQ destruct
    140   ]
    141 ]
    142 #_ #_ #prf #H1 cases(IH pre_tl ?)
    143 [2: % #EQ whd in H1 : (?(??%?)); >EQ in H1; * #H @H % ]
    144 #s2 * #s3 * #t12 * #l1 * #prf1 * #t34 ** #H2 #H3 #H4 %{s2} %{s3} %{(t_ind … prf t12)}
    145 %{l1} %{prf1} %{t34} % // %
    146 [ % %2 // cases H2 // inversion t12 [2: #z1 #z2 #z3 #lbl #prf5 #tl1 #_ #EQ1 #EQ2 #E3 destruct * #H @⊥ @H // ]
    147   #st #EQ1 #EQ2 #EQ3 destruct #_ % /2 by head_of_premeasurable_is_not_io/
    148 | >H3 //
    149 ]
    150 qed.
    151 
    152 (*
    153 definition measurable_suffix ≝
    154  λS : abstract_status.λs1,s1' : S.λt : raw_trace … s1 s1'.
    155 ∃s1_em1 : S.
    156 ∃t_pre_em : raw_trace … s1 s1_em1.
    157 ∃s1_postem1 : S.
    158      ∃t_post_em : raw_trace … s1_postem s1'.
    159      silent_trace S ?? t_post_em ∧
    160      ∃l_em : ActionLabel.
    161      ∃ex_em : as_execute … l_em s1_em s1_postem.
    162      t = t_pre_em @ (t_ind … ex_em t_post_em) ∧
    163      (is_call_act l_em → bool_to_Prop(is_call_post_label … s1_em)).
    164 *)     
    165 
    166 lemma append_nil_is_nil : ∀S : abstract_status.
    167 ∀s1,s2 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s1.
    168 t1 @ t2 = t_base … s1 → s1 = s2 ∧ t1 ≃ t_base … s1 ∧ t2 ≃ t_base … s1.
    169 #S #s1 #s2 #t1 elim t1 -t1 -s1 -s2
    170 [ #st #t2 normalize #EQ destruct /3 by refl_jmeq, conj/]
    171 #s1 #s2 #s3 #l #prf #t2 #IH #t2 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    172 qed.
    173 
    174 lemma append_silent : ∀S : abstract_status.
    175 ∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.
    176 ∀t2 : raw_trace … s2 s3.silent_trace … t1 →
    177 silent_trace … t2 →
    178 silent_trace … (t1 @ t2).
    179 #S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
    180 [ #st #t2 #_ * /2 by or_introl, or_intror/ ]
    181 #st1 #st2 #st3 #l #prf #tl #IH #t2 *
    182 [2: * #H cases(H I) ] #H inversion H in ⊢ ?;
    183 [ #st #H1 #H2 #H3 #H4 #H5 #H6 destruct ]
    184 #st1' #st2' #st3' #prf' #tl' #Hst1' #Htl' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
    185 #Ht2 % %2 // cases(IH … Ht2) /2/
    186 inversion(tl' @ t2)
    187 [2: #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 * #H cases (H I) ]
    188 #st #EQ1 #EQ2 destruct #H cases(append_nil_is_nil … H) * #EQ1 #EQ2 #EQ3 destruct //
    189 qed.
    190 
    191 
    192 definition measurable_suffix ≝
    193  λS : abstract_status.λs1,s1' : S.λt : raw_trace … s1 s1'.
    194 ∃s1_em : S.
    195 ∃t_pre_em : raw_trace … s1 s1_em.
    196 ∃s1_postem : S.
    197      ∃t_post_em : raw_trace … s1_postem s1'.
    198      silent_trace S ?? t_post_em ∧
    199      ∃l_em : ActionLabel.
    200      ∃ex_em : as_execute … l_em s1_em s1_postem.
    201      t = t_pre_em @ (t_ind … ex_em t_post_em) ∧
    202      (is_call_act l_em → bool_to_Prop(is_call_post_label … s1_em)) ∧
    203      is_costlabelled_act l_em.
    204      
    205 
    206 lemma measurable_suffix_tind : ∀S : abstract_status.
    207 ∀s1,s2,s3 : S.∀l : ActionLabel.∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
    208 measurable_suffix … (t_ind … prf t) → (is_costlabelled_act l \wedge silent_trace … t) ∨ measurable_suffix … t.
    209 #S #s1 #s2 #s3 #l #prf #t lapply prf -prf lapply s1 -s1 cases t -t -s2 -s3
    210 [ #st #st1 #prf * #s_em * #t_pre * #s_post * #t_post * #sil_post * #l_em * #ex_em **
    211  inversion t_pre in ⊢ ?;
    212  [#st' #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    213   #_ /4 by or_introl, conj/
    214  | #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct normalize in H34;
    215    lapply(eq_to_jmeq ??? H34) -H34 #H34 destruct inversion H29 in ⊢ ?;
    216    [ #H38 #H39 #H40 #H41 destruct
    217    | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 destruct normalize in e1; destruct
    218    ]
    219  normalize in e0; destruct
    220 ]
    221 ]
    222 #s1 #s2 #s3 #l1 #prf1 #tl #s4 #prf * #s_em * #t_post lapply prf -prf cases t_post -t_post
    223 [ #s5 #prf * #s_post * #t_post * #sil_tpost * #l_em * #prf2 ** #EQ normalize in EQ;
    224   lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct /4/
    225 | #s5 #s6 #s7 #lbl #prf2 #tl1 #prf3 * #s_post * #t_post * #sil_tpost * #l_em * #ex_em **
    226   #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost %2
    227   >e0 whd %{s7} %{tl1} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/
    228 ]
    229 qed.
    230 
    231 lemma measurable_suffix_append : ∀S : abstract_status.
    232 ∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
    233 measurable_suffix … t2 → measurable_suffix … (t1 @ t2).
    234 #S #s1 #s2 #s3 #t1 #t2 * #s_em * #pre_t * #s_post * #t_post
    235 * #sil_tpost * #l_em * #prf ** #EQ destruct #Hcall #Hcost
    236 %{s_em} %{(t1@pre_t)} %{s_post} %{t_post} /7 by ex_intro, conj/
    237 qed.
    238 
    239 lemma silent_append_l2 : ∀S : abstract_status.
    240 ∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
    241 silent_trace … (t1 @ t2) → silent_trace … t2.
    242 #S #s1 #s2 #s3 #t1 elim t1 // -s1 -s2
    243 #st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)]
    244 #H @IH % inversion H in ⊢ ?;
    245 [ #H42 #H43 #H44 #H45 normalize #H46 #H47 destruct
    246 | #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 normalize in H59; destruct assumption
    247 ]
    248 qed.
    249 
    250 lemma silent_append_l1 : ∀S : abstract_status.
    251 ∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
    252 silent_trace … (t1 @ t2) → silent_trace … t1.
    253 #S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
    254 [ #st #t2 #_ %2 % *]
    255 #st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)] #H
    256 % inversion H in ⊢ ?; [ #H62 #H63 #H64 #H65 #H66 #H67 normalize in H66; destruct]
    257 #z1 #z2 #z3 #prf' #tl' #Hclass #Htl' #_ #EQ1 #EQ2 #EQ3 normalize in EQ3; #EQ4 destruct
    258 %2 // cases(IH t2 …) /2/ inversion tl
    259 [2: #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 destruct cases H79 #H cases(H I) ]
    260 #st #EQ1 #EQ2 #EQ3 destruct #_ % normalize in Htl'; inversion Htl'
    261 [ #H81 #H82 #H83 #H84 #H85 #H86 destruct //
    262 | #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 destruct //
    263 ]
    264 qed.
    265 
    266 lemma measurable_suffix_append_l1 : ∀S : abstract_status.
    267 ∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
    268 measurable_suffix … (t1 @ t2) → silent_trace … t2 → measurable_suffix … t1.
    269 #S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
    270 [#st #t2 * #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em * #exe ** #EQ normalize in EQ; destruct
    271  #Hcall #Hcost #H lapply(silent_append_l2 … H) -H * [2: * #H cases(H I)] #H inversion H
    272  [ #H113 #H114 #H115 #H116 #H117 #H118 destruct ]
    273  #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 destruct cases Hcost
    274 ]
    275 #st1 #st2 #st3 #l #prf #tl #IH #t2 * #s_em * #t_pre inversion t_pre in ⊢ ?;
    276 [ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em
    277   * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    278   #Hcall #Hcost #sil_t2 %{st} %{(t_base …)} %{s_post} %{tl} % [ /2 by silent_append_l1/]
    279   %{l_em} %{ex_em} /4 by refl, conj/
    280 | #s #s' #s'' #l' #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em
    281   ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost #H
    282   change with ((t_ind ?????? (t_base …)) @ tl) in ⊢ (????%); @measurable_suffix_append @(IH t2) //
    283   %{s''} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} % // % assumption
    284 ]
    285 qed.
    286 
    287 lemma measurable_suffix_append_case : ∀S : abstract_status.
    288 ∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
    289 measurable_suffix … (t1 @ t2) → (measurable_suffix … t1 ∧ silent_trace … t2) ∨ measurable_suffix … t2.
    290 #S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
    291 [ #st #t2 #H %2 assumption]
    292 #st1 #st2 #st3 #l #prf #tl #IH #t2 whd in match (append_on_trace ??????); #Hsuff
    293 cases(measurable_suffix_tind … Hsuff)
    294 [ * #_ #H %% [2: /2 by silent_append_l2/]  change with ((t_ind ?????? tl) @ t2) in Hsuff : (????%);
    295  @(measurable_suffix_append_l1 … Hsuff) /2/
    296 | #H cases(IH … H)
    297   [ * #H1 #H2 %% // change with ((t_ind ?????? (t_base …)) @ tl) in ⊢ (????%); @measurable_suffix_append //
    298   | /2/
    299   ]
    300 ]
    301 qed.
    302 
    303 
    304 
    305 theorem simulates_pre_mesurable:
    306  ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
    307  ∀s1,s1' : S1. ∀t1: raw_trace S1 s1 s1'.
    308   simulation_conditions … rel →
    309   pre_measurable_trace … t1 →
    310   ∀s2 : S2.
    311  as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
    312   ∃s2'. ∃t2: raw_trace … s2 s2'.
    313     pre_measurable_trace … t2 ∧
    314     get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
    315     Srel … rel s1' s2' ∧
    316     (measurable_suffix … t1 → measurable_suffix … t2) ∧
    317     (silent_trace … t1 → silent_trace … t2).
    318 #S1 #S2 #rel #s1 #s1' #t1 #sim #H elim H -t1 -s1 -s1'
    319 [ #st #Hst #s2 #Hs2 #Rsts2 %{s2} %{(t_base …)} %
    320  [ % [ % // % // % //] * #s_em ** [ #sx | #x1 #x2 #x3 #l1 #prf1 #tl1] * #t_pre * #s_post * #t_post * #sil_tpost
    321   * #prf1 ** normalize #EQ  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    322  | #_ %2 % *
    323  ]
    324 | #st1 #st2 #st3 #l #prf #tl #Hclass **
    325   [ #EQ destruct #pre_tl #IH #s2 #Hclass2 #R_st1_s2
    326     cases(simulate_tau … sim … prf … R_st1_s2) [2,3: /2 by head_of_premeasurable_is_not_io/]
    327     #s2' * #t2_init * #R_st2_s2' #silent_t2_init cases(IH … R_st2_s2')
    328     [2: cases silent_t2_init /2 by pre_silent_io/ cases t2_init in Hclass2; // 
    329         #H12 #H13 #H14 #H15 #H16 #H17 #H18 * #H19 cases(H19 I) ]
    330     #s2_fin * #t2_fin **** #pre_t2_fin #EQcost #R_st3_s2_fin #Hm #Hs %{s2_fin} %{(t2_init @ t2_fin)}
    331     cut(? : Prop)
    332       [3: #Hpre %
    333          [ %
    334              [ %
    335                  [ %{Hpre} >get_cost_label_invariant_for_append_silent_trace_l // assumption
    336                  | assumption
    337                  ]
    338              |  #meas_suff cases(Hm ?)
    339                 [ #s_pre' * #t_pre' * #s_post' * #t_post' * #sil_tpost' * #l_em * #ex_em ** #EQ
    340                   destruct #Hcall #lem_cost %{s_pre'} %{(t2_init @ t_pre')} %{s_post'} %{t_post'}
    341                   %{sil_tpost'} %{l_em} %{ex_em} /4 by conj/
    342                 | cases meas_suff -meas_suff #s_em * #t_pre inversion t_pre in ⊢ ?;
    343                   [ #st #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em * #ex_em
    344                     ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ *
    345                   | #st1' #st2' #st3' #lbl #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost
    346                     * #l_em * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #cost_lem
    347                     %{st3'} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/
    348                   ]
    349                 ]
    350              ]
    351         | * [2: * #H cases(H I)] #H inversion H [ #H9 #H10 #H11 #H12 #H13 #H14 destruct]
    352           #x1 #x2 #x3 #prf3 #tl'' #Hclass' #pre_siltl'' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
    353           /4 by append_silent,or_introl/
    354         ]
    355      |
    356      ]
    357     @append_premeasurable_silent //
    358   | #lbl #EQ destruct #pre_tl #IH #s2 #Hs2 #REL
    359     cases(simulate_label … sim … prf … REL)
    360     [2,3: /2/]
    361     #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2''''
    362     #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''')  /2 by pre_silent_io/
    363     #s3 * #t_s3 **** #pre_s3 #EQcost #RElst3s3 #Hm #Hs %{s3}
    364     %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] %
    365     [2: * [ #H inversion H
    366             [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
    367             | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
    368             ]
    369           | * #H cases(H I)
    370           ]
    371      ]
    372     %
    373     [ % [2: assumption] %
    374       [ @append_premeasurable_silent // %2 /2 by ex_intro/
    375        [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2''
    376          [ #H31 #H32 #H33 #H34 #H35 destruct assumption ]
    377          #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
    378          cases H47 #ABS @⊥ @ABS % ]
    379        @append_premeasurable_silent // % //
    380     | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
    381       [2: assumption] whd in ⊢ (???%);
    382       >get_cost_label_invariant_for_append_silent_trace_l //
    383     ] % assumption
    384     | #Hsuff cases(measurable_suffix_tind … Hsuff)
    385       [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s2''} %{t_s2''} %{s2'''} %{(t_s2'''' @ t_s3)}
    386       % [ /3 by or_introl, append_silent/ ] %{(cost_act (Some ? lbl))} %{(exe_s2''')} % // % // * #f * #c #EQ destruct
    387       | #H @measurable_suffix_append change with ((t_ind ?????? t_s2'''')@t_s3) in ⊢ (????%);
    388         @measurable_suffix_append /2/
    389       ]
    390   ]
    391   ]
    392 | #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
    393   #pre_meas_tl #IH #s1 #class_s2 #RELst1s2
    394   cases(simulate_ret_l … sim … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
    395   #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2'''
    396   #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
    397   [2: @(pre_silent_io … sil_t2) assumption]
    398   #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL #Hm #Hs
    399   %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} %
    400   [2: * [ #H inversion H
    401             [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
    402             | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
    403             ]
    404           | * #H cases(H I)
    405           ]
    406   ]
    407   %
    408     [ % [2: assumption]
    409       % [2: whd in ⊢ (??%?);
    410         >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
    411         whd in ⊢ (???%);
    412         >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2))
    413         @eq_f assumption ]
    414   @append_premeasurable_silent [2: //] %3
    415   [2,3: /3 by append_premeasurable_silent, ex_intro, or_introl/ ]
    416   cases sil_t1 [ /2 by pre_silent_io/ ] inversion t1
    417   [ #H49 #H50 #H51 #H52 #H53 destruct //]
    418   #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65
    419   #ABS @⊥ @ABS %
    420  |  #Hsuff cases(measurable_suffix_tind … Hsuff)
    421       [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{st1} %{t1} %{st2} %{(t2 @ t_fin)}
    422       % [ /3 by or_introl, append_silent/ ] %{(ret_act (Some ? ret_lab))} %{(exe_s2'')} % // % // * #f * #c #EQ destruct
    423       | #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);
    424         @measurable_suffix_append /2/
    425       ]
    426   ]
    427 | #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
    428   #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
    429    cases(simulate_call_pl … sim … post … exe_s1_s2 … REL_s1_s2')
    430    [2,3: /2 by head_of_premeasurable_is_not_io/ ]
    431    #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
    432    cases(IH  … REL)
    433    [2: /2 by pre_silent_io/ ]
    434    #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL1 #Hm #Hs %{s2_fin}
    435    %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} %
    436    [2: * [ #H inversion H
    437             [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
    438             | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
    439             ]
    440           | * #H cases(H I)
    441           ]
    442   ]
    443   %
    444    [ % [2: assumption] %
    445    [2: whd in ⊢ (??%?);
    446         >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
    447         whd in ⊢ (???%);
    448         >(get_cost_label_invariant_for_append_silent_trace_l …  (or_introl … sil_t2))
    449         @eq_f assumption ]
    450    @append_premeasurable_silent try assumption
    451      %4 try assumption
    452      [ cases sil_t1 [/2 by pre_silent_io/ ] inversion t1 [#H67 #H68 #H69 #H70 #H71 destruct //]
    453        #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 destruct cases H83
    454        #ABS @⊥ @ABS %
    455      | whd %{f} %{lab} %
    456      | @append_premeasurable_silent // % assumption
    457      ]
    458    | #Hsuff cases(measurable_suffix_tind … Hsuff)
    459       [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s'} %{t1} %{s2''} %{(t2 @ t_fin)}
    460       % [ /3 by or_introl, append_silent/ ] %{(call_act f lab)} %{(exe_s2'')} % // % //
    461       | #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);
    462         @measurable_suffix_append /2/
    463       ]
    464   ]
    465 |  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
    466   #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
    467   #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … sim … exe_12 … Hst1 … REL) [2,3: /2/ ]
    468   #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1
    469   #sil_tr2 #call_rel cases(IH1 … REL1)
    470   [2: /2 by pre_silent_io/ ]
    471   #st3' * #tr3 **** #pre_tr3 #EQcost_tr3 #REL2 #Hm1 #Hs1
    472   cases(simulate_ret_n … sim … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
    473   #st3'' * #st4' * #st4'' *
    474   #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ]
    475   #st5' * #tr6 **** #pre_tr6 #EQcost_tr6 #REL4 #Hm2 #Hs2 %{st5'}
    476   %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
    477   %
    478   [2: * [ #H inversion H
    479             [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
    480             | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
    481             ]
    482           | * #H cases(H I)
    483           ]
    484   ]
    485   %
    486   [ % [2: assumption] %
    487   [ @append_premeasurable_silent try assumption %5
    488        [1,2: /2 by pre_silent_io/
    489              cases sil_tr1 /2 by pre_silent_io/ inversion tr1
    490              [ #H85 #H86 #H87 #H88 #H89 destruct // ]
    491              #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct
    492              cases H107 #ABS @⊥ @ABS %
    493        | whd %{f} %{l} %
    494        | assumption
    495        | @append_premeasurable_silent try assumption [2: % //]
    496          @append_silent_premeasurable // % //
    497        | @append_premeasurable_silent try assumption
    498        | @(RET_REL … call_rel) assumption
    499        | %
    500        ]
    501   | >get_cost_label_invariant_for_append_silent_trace_l [2: // ]
    502     whd in ⊢ (??%%); @eq_f >append_associative
    503     >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
    504     [2: % // ] >append_associative
    505     >get_cost_label_append in ⊢ (???%);
    506     >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
    507     [2: % //] normalize
    508     >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
    509     [2: % // ] >get_cost_label_append in ⊢ (??%?); @eq_f2
    510     assumption
    511   ]
    512   % //
    513  | #Hsuff cases(measurable_suffix_tind … Hsuff)
    514    [ * #_ #ABS @⊥ cases Hsuff #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em
    515      * #ex_em ** inversion t_pre in ⊢ ?;
    516      [2: #z1 #z2 #z3 #lb #exec #tail #_ #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ
    517          #EQ destruct >e0 in ABS; #ABS lapply(silent_append_l2 … ABS) -ABS * [2: * #H cases(H I)] -IH1 -IH2
    518          -Hsuff -e0 -EQ #H inversion H
    519          [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 destruct]
    520          #y1 #y2 #y3 #exec #tail1 #Hclass1 #sil_tail #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct #_ *
    521      ]
    522      #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    523      #ABS1 >ABS1 in Hst1; [2: /3 by ex_intro/] *
    524    | #Hsuff @measurable_suffix_append change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append
    525      change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append @Hm2
    526      cases(measurable_suffix_append_case … Hsuff)
    527      [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
    528        [ #H137 #H138 #H139 #H140 #H141 #H142 @⊥
    529          -H142 lapply H141 -H141 lapply H138 -H138 lapply H140 -H140 <H139 #EQ lapply t2 -t2 >EQ -EQ
    530          #st2 #_ #EQ destruct(EQ)
    531        | #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 @⊥ -Hsuff destruct
    532        ]
    533      | -Hsuff * #s_em * #t_pre inversion t_pre in ⊢ ?;
    534        [ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em ** #EQ normalize in EQ;
    535          lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ *
    536        | #a1 #a2#a3 #lbl #exe #tl1 #_ #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em
    537          * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost
    538          %{a3} %{tl1} %{s1_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /5 by conj/
    539        ]
    540      ]
    541    ]
    542  ]
    543 ]
    544 qed.
    545          
    546        
    547 lemma get_costlabels_of_trace_empty : ∀S : abstract_status.∀s1,s2 : S.∀t : raw_trace … s1 s2.
    548 get_costlabels_of_trace … t = nil ? → pre_measurable_trace … t → silent_trace … t.
    549 #S #s1 #s2 #t elim t [ #st #_ #_ %2 % * ] #st1 #st2 #st3 #l #prf #t' #IH #EQ #H -s1 -s2 inversion H
    550 [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
    551 | #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
    552 | #s1 #s2 #s3 #l1 #Hclass #prf1 #tl * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
    553 | #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #f * #c #EQ destruct #Hs1 #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
    554 | #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hclass1 #Hclass3 * #f * #c #EQ destruct #Hs1
    555   #pre1 #pre2 #Hs1s4 whd in match is_unlabelled_ret_act; normalize nodelta #EQ destruct #_ #_ #EQ1 #EQ2 #EQ3 #EQ4
    556   destruct
    557 ]
    558 whd in EQ : (??%?); destruct cases lbl in prf1 EQ; -lbl normalize [2: #lbl #H #EQ destruct]
    559 #prf #H % %2 // cases(IH …) // cases tl in pre_meas_tl;
    560 [2: #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 cases(absurd ?? H87) %]
    561 #st #H1 #_ % /2 by head_of_premeasurable_is_not_io/
    562 qed.
    563 
    564 lemma measurable_is_measurable_suffix : ∀S : abstract_status.
    565 ∀si,s1,s3,sn : S. ∀t : raw_trace … si sn.measurable …s1 s3 … t → measurable_suffix … t.
    566 #S #si #s1 #s3 #sn #t * #_ * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 *****
    567 #EQ destruct /11 width=20 by conj,ex_intro/
    568 qed.
    569 
    570 lemma get_costlabelled_is_costlabelled :
    571 ∀S : abstract_status.∀s1,s2,s3 : S. ∀l.
    572 ∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
    573 is_costlabelled_act l →
    574 |get_costlabels_of_trace … (t_ind … prf t)| = 1 + |get_costlabels_of_trace … t|.
    575 #S #s1 #s2 #s3 * normalize
    576   [ /2 by monotonic_pred/
    577   | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
    578   | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
    579   ]
    580 qed.
    581 
    582 lemma silent_suffix_cancellable : ∀S : abstract_status.
    583 ∀s1,s2,s2',s3,s3',s4 : S.∀l,l'.
    584 ∀t1 : raw_trace … s1 s2. ∀prf : as_execute … l s2 s3.
    585 ∀t2 : raw_trace … s3 s4.
    586 ∀t1' :raw_trace … s1 s2'.∀prf' : as_execute … l' s2' s3'.
    587 ∀t2' : raw_trace … s3' s4.
    588 is_costlabelled_act l → is_costlabelled_act l' →
    589 silent_trace … t2 → silent_trace … t2' →
    590 t1 @ (t_ind … prf t2) = t1' @ (t_ind … prf' t2') →
    591 s2 = s2' ∧ l = l' ∧ t1 ≃ t1'.
    592 #S #s1 #s2 #s2' #s3 #s3' #s4 #l #l' #t1 #prf #t2 #t1' #prf' #t2' #Hl #Hl' #sil_t2 #sil_t2'
    593 lapply prf -prf lapply prf' -prf' lapply t1' -t1' elim t1
    594 [ normalize #st * normalize
    595   [ #st' #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct /3/
    596   | #st1 #st2 #st3 #lbl #prf1 #tl #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    597     @⊥ lapply(silent_append_l2 … sil_t2) * [2: * #H cases(H I)] #H inversion H
    598     [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
    599     | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl'
    600     ]
    601   ]
    602 ]
    603 #st1 #st2 #st3 #lbl #prf1 #tl #IH #t1' inversion t1' in ⊢ ?;
    604 [ #st #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
    605   @⊥ lapply(silent_append_l2 … sil_t2') * [2: * #H cases(H I)] #H inversion H
    606     [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
    607     | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl
    608     ]
    609 | #st1' #st2' #st3' #lbl' #prf1' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize
    610   #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct -EQ cases(IH … e0) * #EQ1 #EQ2 #EQ3 destruct /3/
    611 ]
    612 qed.
    613 
    614 
    615 lemma prefix_of_measurable_suffix_is_premeasurable : ∀S : abstract_status.
    616 ∀s1,s2,s3,s4 :S.∀l.∀prf : as_execute … l s2 s3.
    617 ∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s3 s4.∀t : raw_trace … s1 s4.
    618 pre_measurable_trace … t → t = (t1 @ (t_ind … prf t2)) → is_costlabelled_act l →
    619 silent_trace … t2 → (is_call_act l → bool_to_Prop(is_call_post_label … s2)) →
    620 pre_measurable_trace … t1.
    621 #S #s1 #s2 #s3 #s4 #l #prf #t1 #t2 #t #H lapply t1 -t1 lapply t2 -t2 lapply prf -prf lapply s2 -s2
    622 lapply s3 -s3 elim H -t -s1 -s4
    623 [ #st #_ #s1 #s2 #prf #r #p inversion p in ⊢ ?;
    624   [ #H1 #H2 #H3 #H4 destruct #H5 #H6 #H7 normalize in H5; lapply(eq_to_jmeq ??? H5) -H5 #H5 destruct
    625   | #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 destruct
    626     normalize in H19; lapply(eq_to_jmeq ??? H19) -H19 #H19 destruct
    627   ]
    628 | #st1 #st2 #st3 #lbl #prf #tl #Hclass **
    629   [ #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?;
    630     [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
    631       destruct *
    632     | #s3 #s4 #s5 #lab #exe #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?);
    633       #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/
    634     ]
    635   | #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?;
    636     [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
    637       destruct #_ #_ #_ % //
    638     | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
    639       lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/
    640    ]
    641  ]
    642 | #st1 #st2 #st3 #lbl #Hclass #prf #tl * #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1
    643   #t1 #t2 inversion t2 in ⊢ ?;
    644   [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
    645     destruct #_ #_ #_ % //
    646   | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
    647       lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %3 /2/ @(IH … (refl …)) /2/
    648   ]
    649 | #st1 #st2 #st3 #lbl #prf #tl #Hclass * #f * #c #EQ destruct #call_post #pre_tl #IH #s1 #s2 #prf1
    650   #t1 #t2 inversion t2 in ⊢ ?;
    651   [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
    652     destruct #_ #_ #_ % //
    653   | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
    654       lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %4 /3/ @(IH … (refl …)) /2/
    655   ]
    656 | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hst1 #Hst3 * #f * #c #EQ destruct
    657   #Hcall #pre_t1 #pre_t2 #succ whd in ⊢ (% → ?); #EQ destruct #IH1 #IH2 #s1 #s2 #prf3
    658   #t3 #t4 inversion t4 in ⊢ ?;
    659   [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
    660     destruct #_ #_ #_ % //
    661   | #s3 #s4 #s5 #lbl #prf4 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
    662     lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t3 #H1
    663     cut(measurable_suffix … (t1@(t_ind … prf2 t2)))
    664     [ whd %{s5} %{tail} %{s1} %{t3} %{sil_t3} %{l} %{prf3} /4 by jmeq_to_eq, conj/]
    665     #Hmeas cases(measurable_suffix_append_case … Hmeas)
    666     [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
    667       [ #H4 #H5 #H6 #H7 #H8 #H9 destruct
    668       | #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
    669       ]
    670     | -Hmeas #Hmeas cases(measurable_suffix_tind … Hmeas)
    671       [ **] -Hmeas -IH1 -EQ * #s_em * #t_pre * #s_post * #t_post * #sil_tpost
    672       * #l_em * #ex_em ** #EQ destruct #H1 #H2
    673       change with (t_ind … (t_base …) @ ?) in match (t_ind ???????) in e0;
    674       <append_associative in e0; <append_associative #e0
    675       cases(silent_suffix_cancellable … e0) // -e0 * #EQ1 #EQ2 #EQ3 destruct
    676       >append_associative %5 /2/ [ %{f} %{c} //] normalize
    677       @(IH2 … (refl …)) /2/
    678      ]
    679    ]
    680  ]
    681 qed.
    682  
    683 
    684 lemma measurable_suffix_is_measurable:
    685 ∀S : abstract_status.
    686 ∀s1,s4 : S.
    687 ∀t : raw_trace … s1 s4.
    688 pre_measurable_trace … t →
    689 2 ≤ |get_costlabels_of_trace … t | →
    690 measurable_suffix … t → ∃s1,s3.
    691 measurable … s1 … s3 … t.
    692 #S #s1 #s4 #t #pre_meas_t #Hlab * #s_em * #t_pre * #s_init * #t_post * #sil_tpost
    693 * #l_em * #ex_em ** #EQ destruct #Hcall #Hcost_lem
    694 >get_cost_label_append in Hlab; >append_length >get_costlabelled_is_costlabelled //
    695 >(get_cost_label_silent_is_empty … sil_tpost) #CARD
    696 cases(measurable_prefix_of_premeasurable … t_pre)
    697 [3: cases(get_costlabels_of_trace ????) in CARD; [ /3/ | #c #xc #_ % #EQ destruct]
    698 |2: @(prefix_of_measurable_suffix_is_premeasurable … pre_meas_t) [5: %|*:] assumption
    699 | #s_prefix * #s_post_pre * #t_prefix * #lab * #exe1 * #t34 ** #sil_tprefix #EQ destruct #cost_lab
    700   /20 width=20 by conj,ex_intro/
    701 ]
    702 qed.
    703 
    704 
    705 
    706 theorem simulates_measurable:
    707  ∀S1,S2: abstract_status.
    708  
    709  ∀rel: relations S1 S2. simulation_conditions … rel →
    710  
    711  ∀si,sn: S1. ∀t: raw_trace … si sn.
    712  
    713  ∀s1,s2. measurable … s1 s2 … t →
    714  
    715  ∀si': S2. as_classify … si' ≠ cl_io →
    716  
    717  Srel … rel si si' →
    718  
    719  ∃sn'. ∃t': raw_trace … si' sn'.
    720 
    721  Srel … rel sn sn' ∧
    722 
    723  get_costlabels_of_trace … t = get_costlabels_of_trace … t' ∧
    724  
    725  ∃s1',s2'. measurable … s1' s2' … t'.
    726 #S1 #S2 #rel #sim_rel #si #sn #t #s1 #s2 #Hmeas #s1' #Hclass #Rsi_si'
    727 cases(simulates_pre_mesurable … rel … t … Rsi_si') //
    728 [2: cases Hmeas //] #sn' * #t2 **** #pre_meas_t2 #EQcost #R_sn_sn'
    729 #Hmeas1 #_ %{sn'} %{t2} % [% //] @(measurable_suffix_is_measurable … t2) /4 by measurable_is_measurable_suffix/
    730 <EQcost cases Hmeas #_ * #s1 * #s2 * #t_pre * #t_mid * #t_last * #l1 * #l2 * #prf1 * #prf2 ***** #EQ destruct
    731 #H1 #H2 #_ #_ #_ >get_cost_label_append >length_append >get_costlabelled_is_costlabelled //
    732  >get_cost_label_append >length_append >get_costlabelled_is_costlabelled // /2 by le_plus_a/
    733 qed.
    734    
    735 
    736 
     16include "Vm.ma".   
    73717
    73818theorem cerco:
     
    80888   sull'assembler
    809893. Integrare la prima passata di Language nel risultato finale
    810 4. Chiudere il demone
    811905. Cambi al control flow: Paolo's trick (label = coppia label-pezzo di stato)
    812916. Rappresentabilita' di I, [[ ]] e stati astratti =⇒ instrumentazione
Note: See TracChangeset for help on using the changeset viewer.