source: LTS/Final.ma @ 3523

Last change on this file since 3523 was 3523, checked in by piccolo, 5 years ago

closed all daemon with the final statement

File size: 37.2 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "Simulation.ma".
16include "Vm.ma".
17
18inductive 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
23lemma no_io_append : ∀S : abstract_status.
24∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
25∀t2 : raw_trace … st2 st3.
26no_io_trace … t1 → no_io_trace … t2 →
27no_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 //
34qed.
35
36lemma pre_measurable_no_io : ∀S : abstract_status.
37∀st1,st2 : S. ∀t : raw_trace … st1 st2.
38pre_measurable_trace … t →
39no_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 //
43qed.
44
45lemma head_of_no_io_is_no_io : ∀S : abstract_status.
46∀st1,st2 : S. ∀t : raw_trace … st1 st2.
47no_io_trace … t → as_classify … st1 ≠ cl_io.
48#S #st1 #st2 #t #H elim H //
49qed.
50
51
52lemma 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) →
55no_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 //
61qed.
62
63lemma 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) →
66no_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 //
71qed.
72
73lemma 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 %*
80qed.
81
82(*
83lemma 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.
86pre_measurable_trace … (t1 @ (t_ind … l prf t2)) →
87as_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
93definition 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.
100silent_trace … t12 ∧ t = t12 @ (t_ind … prf t34) ∧ is_costlabelled_act l.
101
102lemma measurable_prefix_of_premeasurable :
103∀S : abstract_status.
104∀s1,s4 : S.
105∀t : raw_trace … s1 s4.
106pre_measurable_trace … t →
107get_costlabels_of_trace … t ≠ nil ? →
108measurable_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]
150qed.
151
152(*
153definition 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
166lemma append_nil_is_nil : ∀S : abstract_status.
167∀s1,s2 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s1.
168t1 @ 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
172qed.
173
174lemma append_silent : ∀S : abstract_status.
175∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.
176∀t2 : raw_trace … s2 s3.silent_trace … t1 →
177silent_trace … t2 →
178silent_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/
186inversion(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 //
189qed.
190
191
192definition 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
206lemma measurable_suffix_tind : ∀S : abstract_status.
207∀s1,s2,s3 : S.∀l : ActionLabel.∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
208measurable_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]
229qed.
230
231lemma measurable_suffix_append : ∀S : abstract_status.
232∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
233measurable_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/
237qed.
238
239lemma silent_append_l2 : ∀S : abstract_status.
240∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
241silent_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]
248qed.
249
250lemma silent_append_l1 : ∀S : abstract_status.
251∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
252silent_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]
264qed.
265
266lemma measurable_suffix_append_l1 : ∀S : abstract_status.
267∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
268measurable_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]
285qed.
286
287lemma measurable_suffix_append_case : ∀S : abstract_status.
288∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
289measurable_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
293cases(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]
301qed.
302
303
304
305theorem 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]
544qed.
545         
546       
547lemma get_costlabels_of_trace_empty : ∀S : abstract_status.∀s1,s2 : S.∀t : raw_trace … s1 s2.
548get_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]
558whd 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/
562qed.
563
564lemma 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/
568qed.
569
570lemma 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.
573is_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  ]
580qed.
581
582lemma 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.
588is_costlabelled_act l → is_costlabelled_act l' →
589silent_trace … t2 → silent_trace … t2' →
590t1 @ (t_ind … prf t2) = t1' @ (t_ind … prf' t2') →
591s2 = 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'
593lapply 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]
612qed.
613
614
615lemma 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.
618pre_measurable_trace … t → t = (t1 @ (t_ind … prf t2)) → is_costlabelled_act l →
619silent_trace … t2 → (is_call_act l → bool_to_Prop(is_call_post_label … s2)) →
620pre_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
622lapply 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 ]
681qed.
682 
683
684lemma measurable_suffix_is_measurable:
685∀S : abstract_status.
686∀s1,s4 : S.
687∀t : raw_trace … s1 s4.
688pre_measurable_trace … t →
6892 ≤ |get_costlabels_of_trace … t | →
690measurable_suffix … t → ∃s1,s3.
691measurable … 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
696cases(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]
702qed.
703
704
705
706theorem 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'
727cases(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/
733qed.
734   
735
736
737
738theorem cerco:
739 (* Given the operational semantics of a source program *)
740 ∀S1: abstract_status.
741
742 (* Given the compiled assembly program *)
743 ∀p,p',prog.
744 
745 (* Let S2 be the operational semantics of the compiled code  *)
746 let S2 ≝ asm_operational_semantics p p' prog in
747 
748 (* If the simulation conditions between the source and compiled
749    code holds (i.e. if the compiler is correct) *)
750 ∀rel: relations S1 S2. simulation_conditions … rel →
751
752 (* Given an abstract interpretation framework for the compiled code *)
753 ∀R: asm_abstract_interpretation p p' prog.
754 
755 (* If the static analysis does not fail *)
756 ∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1.
757
758 (* For every source trace whose measurable fragment starts in s1 and ends in s2 or,
759   equivalently, whose state after the initial labelled transition is s1
760   and whose state after the final labelled transition is s2  *)
761 ∀si,s1,s2,sn. ∀t: raw_trace S1 … si sn.
762 measurable … s1 s2 … t →
763
764 (* For each target non I/O state si' in relation with the source state si *)
765 ∀si': S2. as_classify … si' ≠ cl_io → Srel ?? rel si si' →
766
767 (* There exists a corresponding target trace starting from si' *)
768 ∃sn'. ∃t': raw_trace … si' sn'.
769  Srel … rel sn sn' ∧
770  ∃EQ:get_costlabels_of_trace … t = get_costlabels_of_trace … t'.
771 
772 (* that has a measurable fragment starting in s1' and ending in s2' *)
773 ∃s1',s2'. measurable … s1' s2' … t' ∧
774
775 (* Let labels be the costlabels observed in the trace (last one excluded) *)
776 let labels ≝ chop … (get_costlabels_of_trace …  t) in
777
778(* Let abs_actions be the list of statically computed abstract actions
779   associated to each label in labels. *)
780 ∀abs_actions.
781  abs_actions =
782   dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
783
784 (* Given an abstract state in relation with the first state of the measurable
785    fragment *)
786 ∀a1.R s1' a1 →
787
788 (* The final state of the measurable fragment is in relation with the one
789   obtained by applying every semantics in abs_trace. *)
790 R s2' (〚abs_actions〛 a1).
791[2: @hide_prf normalize nodelta in prf; >EQ in prf; #prf
792    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
793    #lbl' #pc * #Hmem #EQ destruct
794    >(proj1 … (static_analisys_ok … EQmap … Hmem))
795    @(proj2 … (static_analisys_ok … EQmap … Hmem))]
796#S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ???) #rel #sim_conds
797#R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi'
798cases (simulates_measurable … sim_conds … Hmeas … Hclass Rsisi')
799#sn' * #t' ** #Rsnsn' #EQcostlabs * #s1' * #s2' #Hmeas'
800%{sn'} %{t'} %{Rsnsn'} %{EQcostlabs} %{s1'} %{s2'} %{Hmeas'} #acts #EQacts
801@(static_dynamic … EQmap … Hmeas') >rewrite_in_dependent_map
802[2: <EQcostlabs in ⊢ (??%?); % | // ]
803qed. 
804
805(* TODO:
8061. Monoide di costo: eliminare.
8072. Discorso I/O, fallimento della block-cost, ipotesi di premisurabilita'
808   sull'assembler
8093. Integrare la prima passata di Language nel risultato finale
8104. Chiudere il demone
8115. Cambi al control flow: Paolo's trick (label = coppia label-pezzo di stato)
8126. Rappresentabilita' di I, [[ ]] e stati astratti =⇒ instrumentazione
813*)
Note: See TracBrowser for help on using the repository browser.