Changeset 3524 for LTS


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

rearrangments of lemmas, final statement in place

Location:
LTS
Files:
5 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
  • LTS/Simulation.ma

    r3523 r3524  
    11include "Traces.ma".
     2include "basics/jmeq.ma".
     3
     4discriminator option.
    25
    36record relations (S1,S2 : abstract_status) : Type[0] ≝
     
    9497 }.
    9598
    96 lemma append_premeasurable_silent : ∀S : abstract_status.
    97 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
    98 pre_measurable_trace … t → silent_trace … t' → 
    99 pre_measurable_trace … (t' @ t).
    100 #S #st1' #st1 #st2 #t #t' lapply t -t elim t'
    101 [ #st #t #Hpre #_ whd in ⊢ (????%); assumption]
    102 #s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?;
    103 [ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
    104 #s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
    105 destruct #_ whd in ⊢ (????%); %2
    106 [ assumption
    107 | %{(None ?)} %
    108 | @IH try assumption
    109 ]
    110 % assumption
    111 qed.
    112 
    113 lemma pre_silent_is_premeasurable : ∀S : abstract_status.
    114 ∀st1,st2 : S. ∀t : raw_trace S st1 st2.pre_silent_trace … t
    115 → pre_measurable_trace … t.
    116 #S #st1 #st2 #t elim t
    117 [ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
    118 #st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
    119 -t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H in ⊢ ?;
    120 [ #st #H2 #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
    121 #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
    122 @IH assumption
    123 qed.
    124 
    125 lemma append_tind_commute : ∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
    126     ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
    127     ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2.
    128 #S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.   
    129 
    130 lemma append_silent_premeasurable : ∀S : abstract_status.
    131 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
    132 pre_measurable_trace … t' → silent_trace … t →
    133 pre_measurable_trace … (t' @ t).
    134 #S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
    135 [ #st #Hst #r * [ #H1 @pre_silent_is_premeasurable assumption ]
    136   inversion r [2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 cases H11
    137   #ABS @⊥ @ABS % ] #s' #EQ1 #EQ2 #EQ3 destruct #_
    138   %1 assumption
    139 |2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct
    140   [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ]
    141   try ( %{x} %) try @IH try assumption % ]
    142 #s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
    143 #EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
    144 #r #pre_r normalize
    145 >append_tind_commute >append_tind_commute >append_associative
    146 <append_tind_commute in ⊢ (????(??????%)); %5
    147 try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
    148 qed.
    149 
    150 (*
    151 lemma append_well_formed_silent : ∀S : abstract_status.
    152 ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
    153 well_formed_trace … t → pre_silent_trace … t' →
    154 (is_trace_non_empty … t' → as_classify … st) →
    155 well_formed_trace … (t' @ t).
    156 #S #st1' #st1 #st2 #t #t' lapply t -t elim t'
    157 [ #st #t #H #_ #_ assumption ]
    158 #s1' #s2' #s3' #l #prf #tl #IH #t #well_formed_t #H
    159 inversion H in ⊢ ?;
    160 [ #st #EQ1 #EQ2 #EQ3 destruct]
    161 #st1'' #st2' #st3' #prf' #tl' #Hclass #silent_tl #_
    162 #EQ1 destruct #EQ #EQ1 destruct #_ #Hclass1 %2
    163 [2: >(Hclass1 I) % #EQ destruct]
    164 @IH try assumption #_ assumption
    165 qed.*)
    166 
    167 (*
    168 lemma well_formed_append : ∀S : abstract_status.
    169 ∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
    170 well_formed_trace … (t1 @ t2) → well_formed_trace … t1 ∧ well_formed_trace … t2.
    171 #S #st1 #st2 #st3 #t1 #t2 #H %
    172 [ lapply H -H lapply t2 -t2 elim t1 [ //] #st1' #st2' #st3' #l #exe #tl #IH #r
    173 #H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 normalize in EQ3; destruct ]
    174 #st1'' #st2'' #st3'' #l' #prf' #tl' #wf_tl' [#Hst1'' | * #x #EQ destruct] #_
    175 #EQ1 #EQ2 normalize in ⊢ (% → ?); #EQ3 destruct #_
    176 [ %2 [ @IH assumption ] assumption | %3 [ @IH assumption ] %{x} % ]
    177 ]
    178 lapply H lapply t2 -t2 elim t1 [ #st #r normalize //]
    179 #s1 #s2 #s3 #l #prf #tl #IH #r #H inversion H in ⊢ ?;
    180 [ #st #EQ1 #EQ2 normalize #EQ3 destruct ]
    181 #s1' #s2' #s3' #l' #prf' #tl' #wf_tl' #Hs1' #_ normalize #EQ1 #EQ2 #EQ3 destruct
    182 #_ @IH assumption
    183 qed.
    184 
    185 
    186 lemma append_well_formed : ∀S : abstract_status.
    187 ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
    188 well_formed_trace … t1 → well_formed_trace … t2 → well_formed_trace … (t1 @ t2).
    189 #S #st1 #st2 #st3 #t1 #t2 #H lapply t2 -t2 elim H
    190 [ #st #r #H1 @H1 ]
    191 #s1 #s2 #s3 #l #prf #tl #wf_tl #Hs1 #IH #r #wf_r normalize [ %2 | %3]
    192 try @IH assumption
    193 qed.
    194 (*
    195 lemma silent_is_well_formed : ∀S : abstract_status.
    196 ∀st1,st2 : S.∀t : raw_trace … st1 st2.silent_trace … t → well_formed_trace … t.
    197 #S #st1 #st2 #t elim t [ #st #_ %]
    198 #s1 #s2 #s3 #l #prf #tl #IH * #H inversion H [ #st #EQ1 #EQ2 #EQ3 destruct]
    199 #s1' #s2' #s3' #prf' #tl' #Hs2' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #_ #H1 %2
    200 [ @IH % [2: #_ ] assumption | >(H1 I) % #EQ destruct]
    201 qed.
    202 *)
    203 *)
    204 lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
    205 ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
    206 silent_trace … t1 →
    207 get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
    208 #S #st1 #st2 #st3 #t1 elim t1
    209 [#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 *
    210 [2: whd in match is_trace_non_empty; normalize nodelta * #ABS @⊥ @ABS %]
    211 #H inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
    212 #st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
    213 #_ whd in ⊢ (??%?); >IH [%] %1 assumption
    214 qed.
    215 
    216 (*
    217 lemma raw_trace_ind_r : ∀S : abstract_status.
    218 ∀P : (∀st1,st2.raw_trace S st1 st2 → Prop).
    219 (∀st : S.P … (t_base … st)) →
    220 (∀st1,st2,st3,l.
    221  ∀prf : as_execute S l st2 st3.
    222  ∀tl : raw_trace S st1 st2. P … tl → P … (tl @ (t_ind … prf … (t_base … st3)))) →
    223 ∀st1,st2 : S.∀t : raw_trace S st1 st2.P … t.
    224 #S #P #base #ind #st1 #st2 #t elim t [ assumption]
    225 #st1 #st2 #st3 #l #prf #raw #IH
    226 *)
    227 
    228 lemma head_of_premeasurable_is_not_io : ∀S : abstract_status.
    229 ∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
    230 as_classify … st1 ≠ cl_io.
    231 #S #st1 #st2 #t #H inversion H //
    232 qed.
    233 
    234 (*
     99
    235100theorem simulates_pre_mesurable:
    236101 ∀S1,S2 : abstract_status.∀rel : relations S1 S2.
     
    243108    pre_measurable_trace … t2 ∧
    244109    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
    245     Srel … rel s1' s2'.
    246 #S1 #S2 #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
    247 [ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
    248   /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/
    249 | #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
    250   #pre_measurable_tl #IH #s2 #classify_s2 #REL
    251   [ cases(simulate_tau … good … execute … REL) /2/ #s2'' * #t_s2'' * #RELst2s2''
    252     #silent_ts2'' cases(IH … RELst2s2'')
    253     [2: cases silent_ts2'' /2 by pre_silent_io/ inversion t_s2''
    254         [ #x #EQ1 #EQ2 #EQ3 destruct // ]
    255         #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct * #ABS @⊥ @ABS % ]
    256     #s3 * #ts3 ** #pre_meas_ts3 #EQcost #RELst3s3
    257     %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % /2 by append_premeasurable_silent/
    258     whd in ⊢ (??%?); /2/
    259   | cases(simulate_label … good … execute … REL)
     110    Srel … rel s1' s2' ∧
     111    (measurable_suffix … t1 → measurable_suffix … t2) ∧
     112    (silent_trace … t1 → silent_trace … t2).
     113#S1 #S2 #rel #s1 #s1' #t1 #sim #H elim H -t1 -s1 -s1'
     114[ #st #Hst #s2 #Hs2 #Rsts2 %{s2} %{(t_base …)} %
     115 [ % [ % // % // % //] * #s_em ** [ #sx | #x1 #x2 #x3 #l1 #prf1 #tl1] * #t_pre * #s_post * #t_post * #sil_tpost
     116  * #prf1 ** normalize #EQ  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     117 | #_ %2 % *
     118 ]
     119| #st1 #st2 #st3 #l #prf #tl #Hclass **
     120  [ #EQ destruct #pre_tl #IH #s2 #Hclass2 #R_st1_s2
     121    cases(simulate_tau … sim … prf … R_st1_s2) [2,3: /2 by head_of_premeasurable_is_not_io/]
     122    #s2' * #t2_init * #R_st2_s2' #silent_t2_init cases(IH … R_st2_s2')
     123    [2: cases silent_t2_init /2 by pre_silent_io/ cases t2_init in Hclass2; // 
     124        #H12 #H13 #H14 #H15 #H16 #H17 #H18 * #H19 cases(H19 I) ]
     125    #s2_fin * #t2_fin **** #pre_t2_fin #EQcost #R_st3_s2_fin #Hm #Hs %{s2_fin} %{(t2_init @ t2_fin)}
     126    cut(? : Prop)
     127      [3: #Hpre %
     128         [ %
     129             [ %
     130                 [ %{Hpre} >get_cost_label_invariant_for_append_silent_trace_l // assumption
     131                 | assumption
     132                 ]
     133             |  #meas_suff cases(Hm ?)
     134                [ #s_pre' * #t_pre' * #s_post' * #t_post' * #sil_tpost' * #l_em * #ex_em ** #EQ
     135                  destruct #Hcall #lem_cost %{s_pre'} %{(t2_init @ t_pre')} %{s_post'} %{t_post'}
     136                  %{sil_tpost'} %{l_em} %{ex_em} /4 by conj/
     137                | cases meas_suff -meas_suff #s_em * #t_pre inversion t_pre in ⊢ ?;
     138                  [ #st #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em * #ex_em
     139                    ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ *
     140                  | #st1' #st2' #st3' #lbl #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost
     141                    * #l_em * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #cost_lem
     142                    %{st3'} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/
     143                  ]
     144                ]
     145             ]
     146        | * [2: * #H cases(H I)] #H inversion H [ #H9 #H10 #H11 #H12 #H13 #H14 destruct]
     147          #x1 #x2 #x3 #prf3 #tl'' #Hclass' #pre_siltl'' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     148          /4 by append_silent,or_introl/
     149        ]
     150     |
     151     ]
     152    @append_premeasurable_silent //
     153  | #lbl #EQ destruct #pre_tl #IH #s2 #Hs2 #REL
     154    cases(simulate_label … sim … prf … REL)
    260155    [2,3: /2/]
    261156    #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2''''
    262157    #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''')  /2 by pre_silent_io/
    263     #s3 * #t_s3 ** #pre_s3 #EQcost #RElst3s3 %{s3}
    264     %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
    265     %
    266     [ @append_premeasurable_silent // %2 /2 by ex_intro/
     158    #s3 * #t_s3 **** #pre_s3 #EQcost #RElst3s3 #Hm #Hs %{s3}
     159    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] %
     160    [2: * [ #H inversion H
     161            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
     162            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
     163            ]
     164          | * #H cases(H I)
     165          ]
     166     ]
     167    %
     168    [ % [2: assumption] %
     169      [ @append_premeasurable_silent // %2 /2 by ex_intro/
    267170       [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2''
    268171         [ #H31 #H32 #H33 #H34 #H35 destruct assumption ]
     
    273176      [2: assumption] whd in ⊢ (???%);
    274177      >get_cost_label_invariant_for_append_silent_trace_l //
    275     ]
    276   ]
    277   % assumption
     178    ] % assumption
     179    | #Hsuff cases(measurable_suffix_tind … Hsuff)
     180      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s2''} %{t_s2''} %{s2'''} %{(t_s2'''' @ t_s3)}
     181      % [ /3 by or_introl, append_silent/ ] %{(cost_act (Some ? lbl))} %{(exe_s2''')} % // % // * #f * #c #EQ destruct
     182      | #H @measurable_suffix_append change with ((t_ind ?????? t_s2'''')@t_s3) in ⊢ (????%);
     183        @measurable_suffix_append /2/
     184      ]
     185  ]
     186  ]
    278187| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
    279   #pre_meas_tl #IH #s2 #class_s2 #RELst1s2
    280   cases(simulate_ret_l … good … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
     188  #pre_meas_tl #IH #s1 #class_s2 #RELst1s2
     189  cases(simulate_ret_l … sim … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
    281190  #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2'''
    282191  #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
    283192  [2: @(pre_silent_io … sil_t2) assumption]
    284   #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL
    285   %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
    286   % [2: whd in ⊢ (??%?);
     193  #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL #Hm #Hs
     194  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} %
     195  [2: * [ #H inversion H
     196            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
     197            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
     198            ]
     199          | * #H cases(H I)
     200          ]
     201  ]
     202  %
     203    [ % [2: assumption]
     204      % [2: whd in ⊢ (??%?);
    287205        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
    288206        whd in ⊢ (???%);
     
    295213  #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65
    296214  #ABS @⊥ @ABS %
     215 |  #Hsuff cases(measurable_suffix_tind … Hsuff)
     216      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{st1} %{t1} %{st2} %{(t2 @ t_fin)}
     217      % [ /3 by or_introl, append_silent/ ] %{(ret_act (Some ? ret_lab))} %{(exe_s2'')} % // % // * #f * #c #EQ destruct
     218      | #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);
     219        @measurable_suffix_append /2/
     220      ]
     221  ]
    297222| #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
    298223  #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
    299    cases(simulate_call_pl … good … post … exe_s1_s2 … REL_s1_s2')
     224   cases(simulate_call_pl … sim … post … exe_s1_s2 … REL_s1_s2')
    300225   [2,3: /2 by head_of_premeasurable_is_not_io/ ]
    301226   #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
    302227   cases(IH  … REL)
    303228   [2: /2 by pre_silent_io/ ]
    304    #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL1 %{s2_fin}
    305    %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
     229   #s2_fin * #t_fin **** #pre_t_fin #EQcost #REL1 #Hm #Hs %{s2_fin}
     230   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} %
     231   [2: * [ #H inversion H
     232            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
     233            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
     234            ]
     235          | * #H cases(H I)
     236          ]
     237  ]
     238  %
     239   [ % [2: assumption] %
    306240   [2: whd in ⊢ (??%?);
    307241        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
     
    317251     | @append_premeasurable_silent // % assumption
    318252     ]
    319 | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
     253   | #Hsuff cases(measurable_suffix_tind … Hsuff)
     254      [ * #_ #sil_tl lapply(Hs sil_tl) #sil_ts3 %{s'} %{t1} %{s2''} %{(t2 @ t_fin)}
     255      % [ /3 by or_introl, append_silent/ ] %{(call_act f lab)} %{(exe_s2'')} % // % //
     256      | #H @measurable_suffix_append change with ((t_ind ?????? t2)@t_fin) in ⊢ (????%);
     257        @measurable_suffix_append /2/
     258      ]
     259  ]
     260|  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
    320261  #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
    321   #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … good … exe_12 … Hst1 … REL) [2,3: /2/ ]
     262  #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … sim … exe_12 … Hst1 … REL) [2,3: /2/ ]
    322263  #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1
    323264  #sil_tr2 #call_rel cases(IH1 … REL1)
    324265  [2: /2 by pre_silent_io/ ]
    325   #st3' * #tr3 ** #pre_tr3 #EQcost_tr3 #REL2
    326   cases(simulate_ret_n … good … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
     266  #st3' * #tr3 **** #pre_tr3 #EQcost_tr3 #REL2 #Hm1 #Hs1
     267  cases(simulate_ret_n … sim … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
    327268  #st3'' * #st4' * #st4'' *
    328269  #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ]
    329   #st5' * #tr6 ** #pre_tr6 #EQcost_tr6 #REL4 %{st5'}
     270  #st5' * #tr6 **** #pre_tr6 #EQcost_tr6 #REL4 #Hm2 #Hs2 %{st5'}
    330271  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
    331   % [2: assumption] %
     272  %
     273  [2: * [ #H inversion H
     274            [ #H22 #H23 #H24 #H25 #H26 #H27 destruct
     275            | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 destruct
     276            ]
     277          | * #H cases(H I)
     278          ]
     279  ]
     280  %
     281  [ % [2: assumption] %
    332282  [ @append_premeasurable_silent try assumption %5
    333283       [1,2: /2 by pre_silent_io/
     
    356306  ]
    357307  % //
     308 | #Hsuff cases(measurable_suffix_tind … Hsuff)
     309   [ * #_ #ABS @⊥ cases Hsuff #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em
     310     * #ex_em ** inversion t_pre in ⊢ ?;
     311     [2: #z1 #z2 #z3 #lb #exec #tail #_ #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ
     312         #EQ destruct >e0 in ABS; #ABS lapply(silent_append_l2 … ABS) -ABS * [2: * #H cases(H I)] -IH1 -IH2
     313         -Hsuff -e0 -EQ #H inversion H
     314         [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 destruct]
     315         #y1 #y2 #y3 #exec #tail1 #Hclass1 #sil_tail #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct #_ *
     316     ]
     317     #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
     318     #ABS1 >ABS1 in Hst1; [2: /3 by ex_intro/] *
     319   | #Hsuff @measurable_suffix_append change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append
     320     change with (t_ind ??????? @ ?) in ⊢ (????%); @measurable_suffix_append @Hm2
     321     cases(measurable_suffix_append_case … Hsuff)
     322     [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
     323       [ #H137 #H138 #H139 #H140 #H141 #H142 @⊥
     324         -H142 lapply H141 -H141 lapply H138 -H138 lapply H140 -H140 <H139 #EQ lapply t2 -t2 >EQ -EQ
     325         #st2 #_ #EQ destruct(EQ)
     326       | #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 #H152 #H153 #H154 #H155 @⊥ -Hsuff destruct
     327       ]
     328     | -Hsuff * #s_em * #t_pre inversion t_pre in ⊢ ?;
     329       [ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em ** #EQ normalize in EQ;
     330         lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #_ *
     331       | #a1 #a2#a3 #lbl #exe #tl1 #_ #EQ1 #EQ2 #EQ3 destruct * #s1_post * #t_post * #sil_tpost * #l_em
     332         * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost
     333         %{a3} %{tl1} %{s1_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /5 by conj/
     334       ]
     335     ]
     336   ]
     337 ]
    358338]
    359339qed.
    360340
    361 (* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
    362    sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
    363    cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
    364 
    365 (*
    366 lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s.
    367 #P #H1 #H2 * // @H2 % #EQ destruct qed.
    368 
    369 lemma case_cl_io : ∀s : status_class.decidable … (s = cl_io).
    370 * [2: %%] %2 % #EQ destruct qed.
    371 
    372 lemma tail_of_premeasurable_is_not_io : ∀S : abstract_status.
    373 ∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
    374 as_classify … st2 ≠ cl_io.
    375 #S #st1 #st2 #t #H elim H //
     341theorem simulates_measurable:
     342 ∀S1,S2: abstract_status.
     343 
     344 ∀rel: relations S1 S2. simulation_conditions … rel →
     345 
     346 ∀si,sn: S1. ∀t: raw_trace … si sn.
     347 
     348 ∀s1,s2. measurable … s1 s2 … t →
     349 
     350 ∀si': S2. as_classify … si' ≠ cl_io →
     351 
     352 Srel … rel si si' →
     353 
     354 ∃sn'. ∃t': raw_trace … si' sn'.
     355
     356 Srel … rel sn sn' ∧
     357
     358 get_costlabels_of_trace … t = get_costlabels_of_trace … t' ∧
     359 
     360 ∃s1',s2'. measurable … s1' s2' … t'.
     361#S1 #S2 #rel #sim_rel #si #sn #t #s1 #s2 #Hmeas #s1' #Hclass #Rsi_si'
     362cases(simulates_pre_mesurable … rel … t … Rsi_si') //
     363[2: cases Hmeas //] #sn' * #t2 **** #pre_meas_t2 #EQcost #R_sn_sn'
     364#Hmeas1 #_ %{sn'} %{t2} % [% //] @(measurable_suffix_is_measurable … t2) /4 by measurable_is_measurable_suffix/
     365<EQcost cases Hmeas #_ * #s1 * #s2 * #t_pre * #t_mid * #t_last * #l1 * #l2 * #prf1 * #prf2 ***** #EQ destruct
     366#H1 #H2 #_ #_ #_ >get_cost_label_append >length_append >get_costlabelled_is_costlabelled //
     367 >get_cost_label_append >length_append >get_costlabelled_is_costlabelled // /2 by le_plus_a/
    376368qed.
    377 
    378 lemma get_cost_label_invariant_for_append_silent_trace_r :∀S : abstract_status.
    379 ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
    380 silent_trace … t2 →
    381 get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t1.
    382 #S #st1 #st2 #st3 #t1 #t2 #H >get_cost_label_append
    383 >(get_cost_label_silent_is_empty … H) //
    384 qed.
    385 
    386 lemma instr_execute_commute : ∀S1,S2 :abstract_status.
    387 ∀rel : relations S1 S2.
    388 simulation_conditions … rel →
    389 ∀s1,s1': S1.∀l.l ≠ cost_act (None ?) →  as_execute … l s1 s1' →
    390 (as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
    391 ∀s2.
    392 Srel … rel s1 s2 →
    393 ∃s2' : S2.∃tr : raw_trace … s2 s2'.silent_trace … tr ∧
    394 ∃s2'' : S2.as_execute … l s2' s2'' ∧ ∃s2''' : S2.
    395 ∃tr' : raw_trace … s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧
    396 (is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
    397 (as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
    398 #S1 #S2 #rel #good #s1 #s1' #l #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
    399 [ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
    400   cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
    401   cases(simulate_io_out … good … prf … EQs1_io Hio_s1' … REL)
    402   #s2' * #s2'' * #t *** #sil_t #prf' #class_io #REL'
    403   %{s2} %{(t_base …)} % [ %2 % * ] %{s2'} % // %{s2''} %{t} % 
    404   [2: #_ @(head_of_premeasurable_is_not_io … t) @pre_silent_is_premeasurable
    405      assumption ] % [  %//  % // ] * #f * #l #EQ destruct
    406 | #Hclass_s1 cases(case_cl_io … (as_classify … s1'))
    407   [ #EQs1' cases(io_entering … EQs1' … prf) #l1 #EQ destruct(EQ)
    408     cases(simulate_io_in … good … prf … Hclass_s1 EQs1' …  REL) #s2' * #s2'' * #t
    409     *** #sil_t #exe #Hclass_s2'' #REL'  %{s2'} %{t} %{(or_introl … sil_t)} %{s2''}
    410     %{exe} %{s2''} %{(t_base …)} % [2: >EQs1' * #H @⊥ @H % ] %
    411      [ /4 by or_intror, conj, nmk/] * #f * #l #EQ destruct
    412   | #Hclass_s1' cases l in prf l_notau;
    413     [ #f #l #prf #_ inversion(is_call_post_label … s1)
    414       [ #Hpost cases(simulate_call_pl … good … prf … REL)
    415         [2: >Hpost % |3,4: assumption]
    416         #s2' * #s2'' * #s2''' * #t1 ** #exe #Hpost' * #t3 * * #REL #sil_t1 #sil_t3
    417         %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
    418         [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    419         % [ /4 by or_introl, conj/ ] /3 by /
    420      | #Hpost cases(simulate_call_n … good … prf … REL)
    421        [2: >Hpost % |3,4: // ] #s2' * #s2'' * #s2''' * #t1 ** #Hpost' #exe * #t3
    422        *** #REL' #sil_t1 #sil_t3 #_ %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''}
    423        %{t3} % [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    424        % [2: #_ *] % //
    425      ]
    426    | *
    427      [ #prf #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
    428        * #s2''' * #t1 * #exe * #t3 *** #REL' #sil_t1 #sil_t3 #_ %{s2'}
    429        %{t1} %{(or_introl … sil_t1)} %{s2''} %{exe} %{s2'''} %{t3} %
    430        [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    431        % [ % // % // ] * #f * #l #EQ destruct
    432      | #l #prf #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
    433        #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3
    434        %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
    435        [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    436        % [ % // % //] * #f * #l #EQ destruct
    437     ]
    438   | * [ #_ * #H @⊥ @H % ] #lab #prf #_
    439     cases(simulate_label … prf … REL) [2,3,4: // ] #s2' * #s2'' * #s2''' * #t1
    440     * #exe * #t3 ** #REL' #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe}
    441     %{s2'''} %{t3} %
    442     [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
    443     % [% // % //] * #f * #l #EQ destruct
    444   ]
    445   % //
    446 ]
    447 qed.
    448 *)*)
  • 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.
  • LTS/Vm.ma

    r3523 r3524  
    8080
    8181record sem_params (p : assembler_params) : Type[1] ≝
    82 { m : monoid
    83 ; asm_store_type : Type[0]
     82{ asm_store_type : Type[0]
    8483; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type
    8584; eval_asm_cond : jump_condition p → asm_store_type → option bool
    8685; eval_asm_io : io_instr p → asm_store_type → option asm_store_type
    87 ; cost_of_io : io_instr p → asm_store_type → m
    88 ; cost_of : AssemblerInstr p → asm_store_type →  m
    8986}.
    9087
     
    9491; asm_store : asm_store_type … p'
    9592; asm_is_io : bool
    96 ; cost : m … p'
    9793}.
    9894
     
    116112           asm_is_io … st1 = asm_is_io … st2 →
    117113           S (pc … st1) = pc … st2 →
    118            op … (cost … st1) (cost_of p p' (Seq p i l) (asm_store … st1)) = cost … st2 →
    119114           vmstep … (cost_act l) st1 st2
    120115| vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ.
     
    125120           asm_is_io … st1 = asm_is_io … st2 →
    126121           new_pc = pc … st2 →
    127            op … (cost … st1) (cost_of p p' (Ijmp … new_pc) (asm_store … st1)) = cost … st2 →
    128122           vmstep … (cost_act (None ?)) st1 st2
    129123| vm_cjump_true :
     
    136130           asm_is_io … st1 = asm_is_io … st2 →
    137131           pc … st2 = new_pc →
    138            op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 →
    139132           vmstep … (cost_act (Some ? ltrue)) st1 st2
    140133| vm_cjump_false :
     
    147140           asm_is_io … st1 = asm_is_io … st2 →
    148141           S (pc … st1) = pc … st2 →
    149            op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 →
    150142           vmstep … (cost_act (Some ? lfalse)) st1 st2
    151143| vm_io_in : 
     
    157149           true = asm_is_io … st2 →
    158150           pc … st1 = pc … st2 →
    159            cost … st1 = cost … st2 →
    160151           vmstep … (cost_act (Some ? lin)) st1 st2
    161152| vm_io_out :
     
    167158           false = asm_is_io … st2 →
    168159           S (pc … st1) = pc … st2 →
    169            op … (cost … st1) (cost_of_io p p' io (asm_store … st1)) = cost … st2 →
    170160           vmstep … (cost_act (Some ? lout)) st1 st2
    171161| vm_call :
     
    177167           asm_is_io … st1 = asm_is_io … st2 →
    178168           entry_of_function … prog f = pc … st2 →
    179            op … (cost … st1) (cost_of p p' (Icall p f) (asm_store … st1)) = cost … st2 →
    180169           label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f) = return lbl →
    181170           vmstep … (call_act f lbl) st1 st2
     
    189178           newpc = pc … st2 →
    190179           label_of_pc ? (return_label_fun … prog) newpc = return lbl →
    191            op … (cost … st1) (cost_of p p' (Iret p) (asm_store … st1)) = cost … st2 →
    192180           vmstep … (ret_act (Some ? lbl)) st1 st2.
    193181
     
    203191     ! new_store ← eval_asm_seq p p' x (asm_store … st);
    204192     return 〈cost_act opt_l,
    205              mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false
    206                 (op … (cost … st) (cost_of p p' (Seq p x opt_l) (asm_store … st)))〉
     193             mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false〉
    207194| Ijmp newpc ⇒
    208195   if asm_is_io … st then
     
    210197   else
    211198     return 〈cost_act (None ?),
    212              mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
    213                 (op … (cost … st) (cost_of p p' (Ijmp … newpc) (asm_store … st)))〉
     199             mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false〉
    214200| CJump cond newpc ltrue lfalse ⇒
    215201   if asm_is_io … st then
     
    219205     if b then
    220206       return 〈cost_act (Some ? ltrue),
    221                mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false
    222                 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉
     207               mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false〉
    223208     else
    224209       return 〈cost_act (Some ? lfalse),
    225                mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false
    226                 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉
     210               mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false〉
    227211| Iio lin io lout ⇒
    228212              if asm_is_io … st then
     
    230214                 return 〈cost_act (Some ? lout),
    231215                         mk_vm_state ?? (S (pc … st)) (asm_stack … st)
    232                          new_store false
    233                          (op … (cost … st)
    234                                (cost_of_io p p' io (asm_store … st)))〉   
     216                         new_store false〉   
    235217              else
    236218                return 〈cost_act (Some ? lin),
    237219                        mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st)
    238                                     true (cost … st)
     220                                    true
    239221| Icall f ⇒
    240222    if asm_is_io … st then
     
    245227              mk_vm_state ?? (entry_of_function … prog f)
    246228                             ((S (pc … st)) :: (asm_stack … st))
    247                              (asm_store … st) false
    248                              (op … (cost … st) (cost_of p p' (Icall p f) (asm_store … st)))〉
     229                             (asm_store … st) false〉
    249230| Iret ⇒ if asm_is_io … st then
    250231            None ?
     
    253234            ! lbl ← label_of_pc ? (return_label_fun … prog) newpc;
    254235            return 〈ret_act (Some ? lbl),
    255                     mk_vm_state ?? newpc tl (asm_store … st) false   
    256                      (op … (cost … st) (cost_of p p' (Iret p) (asm_store … st)))〉
     236                    mk_vm_state ?? newpc tl (asm_store … st) false〉
    257237].
    258238
     
    291271lemma vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 →
    292272eval_vmstate p p' prog st1 = return 〈l,st2〉.
    293 #p #p' #prog * #pc1 #stack1 #store1 #io1 #cost1
    294 * #pc2 #stack2 #store2 #io2 #cost2 #l #H inversion H
    295 [ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc #EQcost
     273#p #p' #prog * #pc1 #stack1 #store1 #io1
     274* #pc2 #stack2 #store2 #io2 #l #H inversion H
     275[ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc
    296276  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta   
    297277  >EQfetch >m_return_bind normalize nodelta >EQio normalize nodelta >EQstore
    298   >m_return_bind <EQio1 >EQio <EQpc >EQstack >EQcost %
    299 | #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc #EQcost
     278  >m_return_bind <EQio1 >EQio <EQpc >EQstack %
     279| #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc
    300280  #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta
    301281  >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta <EQio2 >EQio1
    302   >EQstore >EQstack <EQcost >EQstore %
     282  >EQstore >EQstack >EQstore %
    303283|3,4: #s1 #s2 #cond #newoc #ltrue #lfalse #EQev_cond #EQfetch #EQio1 #EQstore
    304   #EQstack #EQio2 #EQnewoc #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct
     284  #EQstack #EQio2 #EQnewoc #EQ1 #EQ2 #EQ3 #EQ4 destruct
    305285  whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind
    306286  normalize nodelta >EQio1 normalize nodelta >EQev_cond >m_return_bind
    307   normalize nodelta <EQio1 >EQio2 >EQstore >EQstack <EQcost >EQstore [%] >EQnewoc %
     287  normalize nodelta <EQio1 >EQio2 >EQstore >EQstack >EQstore [%] >EQnewoc %
    308288|5,6: #s1 #s2 #lin #io #lout #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQpc
    309    #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
     289   #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
    310290   normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
    311    normalize nodelta >EQstack <EQpc >EQcost [ >EQstore <EQio2 %]
     291   normalize nodelta >EQstack <EQpc [ >EQstore <EQio2 %]
    312292   >EQstore >m_return_bind <EQpc <EQio2 %
    313293| #s1 #s2 #f #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQentry
    314   #EQcost #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
     294  #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
    315295  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1
    316   normalize nodelta >EQlab_pc >m_return_bind >EQentry >EQcost <EQio2 >EQio1
     296  normalize nodelta >EQlab_pc >m_return_bind >EQentry <EQio2 >EQio1
    317297  <EQstack >EQstore %
    318298| #s1 #s2 #newpc #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc
    319   #EQlab_pc #EQcosts #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
     299  #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate;
    320300  normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta
    321301  >EQstack whd in match option_pop; normalize nodelta >m_return_bind
    322   >EQlab_pc >m_return_bind >EQcosts >EQstore  <EQio2 >EQio1 %
     302  >EQlab_pc >m_return_bind >EQstore  <EQio2 >EQio1 %
    323303]
    324304qed.
     
    448428definition asm_concrete_trans_sys ≝
    449429λp,p',prog.mk_concrete_transition_sys …
    450              (asm_operational_semantics p p' prog) (m … p')
    451              (λs.match s with [STATE st ⇒ cost … st | _ ⇒ e …] ).
    452 
     430             (asm_operational_semantics p p' prog).
     431             
     432         
    453433definition emits_labels ≝
    454434λp.λinstr : AssemblerInstr p.match instr with
     
    465445
    466446record asm_galois_connection (p: assembler_params) (p': sem_params p) (prog: AssemblerProgram p) : Type[2] ≝
    467 { aabs_d : abstract_transition_sys (m … p')
     447{ aabs_d : abstract_transition_sys
    468448; agalois_rel:> galois_rel (asm_concrete_trans_sys p p' prog) aabs_d
    469449}.
  • LTS/costs.ma

    r3500 r3524  
    3232record concrete_transition_sys : Type[2] ≝
    3333{ trans_sys :> abstract_status
    34 ; cost_mon : monoid
    35 ; cost_of : trans_sys → cost_mon
    3634}.
    3735
    38 record abstract_transition_sys (concrete_costs : Type[0]) : Type[1] ≝
     36record abstract_transition_sys : Type[1] ≝
    3937{ abs_state_t :> Type[0]
    4038; abs_instr : monoid
    4139; act_abs : monoid_action abs_instr abs_state_t
    42 ; abs_cost : abs_state_t → concrete_costs
    4340}.
    4441
    4542notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }.
    46 interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x).
     43interpretation "act_abs" 'sem f x = (act ?? (act_abs ?) f x).
    4744
    4845record galois_rel (C : concrete_transition_sys)
    49                    (A : abstract_transition_sys (cost_mon C)) : Type[0] ≝
     46                   (A : abstract_transition_sys) : Type[0] ≝
    5047{ rel_galois :2> C → A → Prop
    51 ; rel_galois_cost : ∀s,a.rel_galois … s a → abs_cost … a = cost_of … s
    5248}.
    5349
    5450record galois_connection : Type[2] ≝
    5551{ concr : concrete_transition_sys
    56 ; abs_d : abstract_transition_sys (cost_mon concr)
     52; abs_d : abstract_transition_sys
    5753; galois_rel:> galois_rel concr abs_d
    5854}.
Note: See TracChangeset for help on using the changeset viewer.