source: LTS/Traces.ma @ 3540

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

final statement of cerco with the first pass integrated in place

File size: 39.5 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 "arithmetics/nat.ma".
16include "basics/types.ma".
17include "basics/deqsets.ma".
18include "../src/ASM/Util.ma".
19
20(*LABELS*)
21
22inductive FunctionName : Type[0] ≝
23 | a_function_id : ℕ → FunctionName.
24 
25inductive CallCostLabel : Type[0] ≝
26 | a_call_label : ℕ → CallCostLabel.
27 
28inductive ReturnPostCostLabel : Type[0] ≝
29 | a_return_cost_label : ℕ → ReturnPostCostLabel.
30 
31inductive NonFunctionalLabel : Type[0] ≝
32 | a_non_functional_label : ℕ → NonFunctionalLabel.
33 
34inductive CostLabel : Type[0] ≝
35 | a_call : CallCostLabel → CostLabel
36 | a_return_post : ReturnPostCostLabel → CostLabel
37 | a_non_functional_label : NonFunctionalLabel → CostLabel.
38
39coercion a_call.
40coercion a_return_post.
41coercion a_non_functional_label.
42
43definition eq_nf_label : NonFunctionalLabel → NonFunctionalLabel → bool ≝
44λx,y.match x with [ a_non_functional_label n ⇒
45                    match y with [a_non_functional_label m ⇒ eqb n m ] ].
46
47lemma eq_fn_label_elim : ∀P : bool → Prop.∀l1,l2 : NonFunctionalLabel.
48(l1 = l2 → P true) → (l1 ≠ l2 → P false) → P (eq_nf_label l1 l2).
49#P * #l1 * #l2 #H1 #H2 normalize @eqb_elim /3/ * #H3 @H2 % #EQ destruct @H3 % qed.
50
51definition DEQNonFunctionalLabel ≝ mk_DeqSet NonFunctionalLabel eq_nf_label ?.
52#x #y @eq_fn_label_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
53assumption
54qed.
55
56unification hint  0 ≔ ;
57    X ≟ DEQNonFunctionalLabel
58(* ---------------------------------------- *) ⊢
59    NonFunctionalLabel ≡ carr X.
60
61unification hint  0 ≔ p1,p2;
62    X ≟ DEQNonFunctionalLabel
63(* ---------------------------------------- *) ⊢
64    eq_nf_label p1 p2 ≡ eqb X p1 p2.
65
66definition eq_function_name : FunctionName → FunctionName → bool ≝
67λf1,f2.match f1 with [ a_function_id n ⇒ match f2 with [a_function_id m ⇒ eqb n m ] ].
68
69lemma eq_function_name_elim : ∀P : bool → Prop.∀f1,f2.
70(f1 = f2 → P true) → (f1 ≠ f2 → P false) → P (eq_function_name f1 f2).
71#P * #f1 * #f2 #H1 #H2 normalize @eqb_elim /2/ * #H3 @H2 % #EQ destruct @H3 % qed.
72
73definition DEQFunctionName ≝ mk_DeqSet FunctionName eq_function_name ?.
74#x #y @eq_function_name_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
75assumption
76qed.
77
78unification hint  0 ≔ ;
79    X ≟ DEQFunctionName
80(* ---------------------------------------- *) ⊢
81    FunctionName ≡ carr X.
82
83unification hint  0 ≔ p1,p2;
84    X ≟ DEQFunctionName
85(* ---------------------------------------- *) ⊢
86    eq_function_name p1 p2 ≡ eqb X p1 p2.
87
88definition eq_return_cost_lab : ReturnPostCostLabel → ReturnPostCostLabel → bool ≝
89λc1,c2.match c1 with [a_return_cost_label n ⇒ match c2 with [ a_return_cost_label m ⇒ eqb n m]].
90
91lemma eq_return_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
92(c1 ≠ c2 → P false) → P (eq_return_cost_lab c1 c2).
93#P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed.
94
95definition DEQReturnPostCostLabel ≝ mk_DeqSet ReturnPostCostLabel eq_return_cost_lab ?.
96#x #y @eq_return_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
97assumption
98qed.
99
100unification hint  0 ≔ ;
101    X ≟ DEQReturnPostCostLabel
102(* ---------------------------------------- *) ⊢
103    ReturnPostCostLabel ≡ carr X.
104
105unification hint  0 ≔ p1,p2;
106    X ≟ DEQReturnPostCostLabel
107(* ---------------------------------------- *) ⊢
108    eq_return_cost_lab p1 p2 ≡ eqb X p1 p2.
109
110definition eq_call_cost_lab : CallCostLabel → CallCostLabel → bool ≝
111λc1,c2.match c1 with [a_call_label x ⇒ match c2 with [a_call_label y ⇒ eqb x y ]].
112
113lemma eq_call_cost_lab_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
114(c1 ≠ c2 → P false) → P (eq_call_cost_lab c1 c2).
115#P * #c1 * #c2 #H1 #H2 normalize @eqb_elim /2/ * #H @H2 % #EQ destruct @H % qed.
116
117definition DEQCallCostLabel ≝ mk_DeqSet CallCostLabel eq_call_cost_lab ?.
118#x #y @eq_call_cost_lab_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
119assumption
120qed.
121
122unification hint  0 ≔ ;
123    X ≟ DEQCallCostLabel
124(* ---------------------------------------- *) ⊢
125    CallCostLabel ≡ carr X.
126
127unification hint  0 ≔ p1,p2;
128    X ≟ DEQCallCostLabel
129(* ---------------------------------------- *) ⊢
130    eq_call_cost_lab p1 p2 ≡ eqb X p1 p2.
131
132definition eq_costlabel : CostLabel → CostLabel → bool ≝
133λc1.match c1 with
134  [ a_call x1 ⇒ λc2.match c2 with [a_call y1 ⇒ x1 == y1 | _ ⇒ false ]
135  | a_return_post x1 ⇒
136      λc2.match c2 with [ a_return_post y1 ⇒ x1 == y1 | _ ⇒ false ]
137  | a_non_functional_label x1 ⇒
138     λc2.match c2 with [a_non_functional_label y1 ⇒ x1 == y1 | _ ⇒ false ]
139  ].
140
141lemma eq_costlabel_elim : ∀P : bool → Prop.∀c1,c2.(c1 = c2 → P true) →
142(c1 ≠ c2 → P false) → P (eq_costlabel c1 c2).
143#P * #c1 * #c2 #H1 #H2 whd in match (eq_costlabel ??);
144try (@H2 % #EQ destruct)
145[ change with (eq_call_cost_lab ??) in ⊢ (?%); @eq_call_cost_lab_elim
146  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
147| change with (eq_return_cost_lab ??) in ⊢ (?%);
148   @eq_return_cost_lab_elim
149   [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
150| change with (eq_nf_label ??) in ⊢ (?%); @eq_fn_label_elim
151  [ #EQ destruct @H1 % | * #H @H2 % #EQ destruct @H % ]
152]
153qed.
154
155
156definition DEQCostLabel ≝ mk_DeqSet CostLabel eq_costlabel ?.
157#x #y @eq_costlabel_elim [ #EQ destruct /2/] * #H % [ #EQ destruct] #H1 @⊥ @H
158assumption
159qed.
160
161unification hint  0 ≔ ;
162    X ≟ DEQCostLabel
163(* ---------------------------------------- *) ⊢
164    CostLabel ≡ carr X.
165
166unification hint  0 ≔ p1,p2;
167    X ≟ DEQCostLabel
168(* ---------------------------------------- *) ⊢
169    eq_costlabel p1 p2 ≡ eqb X p1 p2.
170
171inductive ActionLabel : Type[0] ≝
172 | call_act : FunctionName → CallCostLabel → ActionLabel
173 | ret_act : option(ReturnPostCostLabel) → ActionLabel
174 | cost_act : option NonFunctionalLabel → ActionLabel.
175 
176definition is_cost_label : ActionLabel → Prop ≝
177λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
178
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
212inductive status_class : Type[0] ≝
213 | cl_jump : status_class
214 | cl_io : status_class
215 | cl_other : status_class.
216 
217record abstract_status : Type[2] ≝
218 { as_status :> Type[0]
219 ; as_execute : ActionLabel → relation as_status
220 ; as_syntactical_succ : relation as_status
221 ; as_classify : as_status → status_class
222 ; is_call_post_label : as_status → bool
223 ; as_initial : as_status → bool
224 ; as_final : as_status → bool
225 ; jump_emits : ∀s1,s2,l.
226      as_classify … s1 = cl_jump →
227      as_execute l s1 s2 → is_non_silent_cost_act l
228 ; io_entering : ∀s1,s2,l.as_classify … s2 = cl_io →
229      as_execute l s1 s2 → is_non_silent_cost_act l
230 ; io_exiting : ∀s1,s2,l.as_classify … s1 = cl_io →
231     as_execute l s1 s2 → is_non_silent_cost_act l
232 }.
233
234(* RAW TRACES *)
235
236inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝
237  | t_base : ∀st : S.raw_trace S st st
238  | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel.
239             as_execute S l st1 st2 → raw_trace S st2 st3 →
240             raw_trace S st1 st3.
241
242let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S)
243(t1 : raw_trace S st1 st2) on t1 : raw_trace S st2 st3 → raw_trace S st1 st3 ≝
244match t1
245return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3
246with
247[ t_base st ⇒ λt2.t2
248| t_ind st1' st2' st3' l prf tl ⇒ λt2.t_ind … prf … (append_on_trace … tl t2)
249].
250
251interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2).
252
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
261lemma append_associative : ∀S,st1,st2,st3,st4.
262∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
263∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3).
264#S #st1 #st2 #st3 #st4 #t1 elim t1 -t1
265[ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH %
266qed.
267
268definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 →
269raw_trace … st1 st3 → Prop≝
270λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3.
271
272definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 →
273raw_trace … st1 st3 → Prop≝
274λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
275
276definition actionlabel_to_costlabel ≝
277λl : ActionLabel.match l with
278    [ call_act f c ⇒ [ c ]
279    | ret_act x ⇒ match x with
280                  [ Some c ⇒ [ a_return_post c ]
281                  | None ⇒ []
282                  ]
283    | cost_act x ⇒ match x with
284                  [ Some c ⇒ [ a_non_functional_label c ]
285                  | None ⇒ []
286                  ]
287   ].
288
289let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
290(t : raw_trace S st1 st2) on t : list CostLabel ≝
291match t with
292[ t_base st ⇒ [ ]
293| t_ind st1' st2' st3' l prf t' ⇒
294    let tl ≝ get_costlabels_of_trace … t' in
295    actionlabel_to_costlabel l  @ tl
296].
297
298lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.
299∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
300get_costlabels_of_trace … (t1 @ t2) =
301 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
302#S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
303[#f * #l | * [| * #l] | *  [| #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH
304qed.
305
306lemma append_tind_commute : ∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
307    ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
308    ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2.
309#S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.
310
311lemma get_costlabelled_is_costlabelled :
312∀S : abstract_status.∀s1,s2,s3 : S. ∀l.
313∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
314is_costlabelled_act l →
315|get_costlabels_of_trace … (t_ind … prf t)| = 1 + |get_costlabels_of_trace … t|.
316#S #s1 #s2 #s3 * normalize
317  [ /2 by monotonic_pred/
318  | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
319  | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
320  ]
321qed.
322
323(*SILENT TRACES*)
324
325inductive pre_silent_trace (S : abstract_status) :
326∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
327| silent_empty : ∀st : S.as_classify … st ≠ cl_io → pre_silent_trace … (t_base S st)
328| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
329                ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → pre_silent_trace … tl →
330                pre_silent_trace … (t_ind … prf … tl).
331               
332definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
333raw_trace S st1 st2 → bool ≝
334λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
335
336definition silent_trace : ∀S:abstract_status.∀s1,s2 : S.
337raw_trace S s1 s2 → Prop ≝ λS,s1,s2,t.pre_silent_trace … t ∨
338¬ (bool_to_Prop (is_trace_non_empty … t)).
339
340lemma pre_silent_io : ∀S : abstract_status.
341∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t →
342as_classify … s2 ≠ cl_io.
343#S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
344#st1 #st2 #st3 #l #prf #tl #IH #H inversion H //
345#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
346#EQ destruct #_ @IH assumption
347qed.
348
349lemma append_silent : ∀S : abstract_status.
350∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.
351∀t2 : raw_trace … s2 s3.silent_trace … t1 →
352silent_trace … t2 →
353silent_trace … (t1 @ t2).
354#S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
355[ #st #t2 #_ * /2 by or_introl, or_intror/ ]
356#st1 #st2 #st3 #l #prf #tl #IH #t2 *
357[2: * #H cases(H I) ] #H inversion H in ⊢ ?;
358[ #st #H1 #H2 #H3 #H4 #H5 #H6 destruct ]
359#st1' #st2' #st3' #prf' #tl' #Hst1' #Htl' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
360#Ht2 % %2 // cases(IH … Ht2) /2/
361inversion(tl' @ t2)
362[2: #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 * #H cases (H I) ]
363#st #EQ1 #EQ2 destruct #H cases(append_nil_is_nil … H) * #EQ1 #EQ2 #EQ3 destruct //
364qed.
365
366lemma silent_append_l2 : ∀S : abstract_status.
367∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
368silent_trace … (t1 @ t2) → silent_trace … t2.
369#S #s1 #s2 #s3 #t1 elim t1 // -s1 -s2
370#st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)]
371#H @IH % inversion H in ⊢ ?;
372[ #H42 #H43 #H44 #H45 normalize #H46 #H47 destruct
373| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 normalize in H59; destruct assumption
374]
375qed.
376
377lemma silent_append_l1 : ∀S : abstract_status.
378∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
379silent_trace … (t1 @ t2) → silent_trace … t1.
380#S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
381[ #st #t2 #_ %2 % *]
382#st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)] #H
383% inversion H in ⊢ ?; [ #H62 #H63 #H64 #H65 #H66 #H67 normalize in H66; destruct]
384#z1 #z2 #z3 #prf' #tl' #Hclass #Htl' #_ #EQ1 #EQ2 #EQ3 normalize in EQ3; #EQ4 destruct
385%2 // cases(IH t2 …) /2/ inversion tl
386[2: #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 destruct cases H79 #H cases(H I) ]
387#st #EQ1 #EQ2 #EQ3 destruct #_ % normalize in Htl'; inversion Htl'
388[ #H81 #H82 #H83 #H84 #H85 #H86 destruct //
389| #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 destruct //
390]
391qed.
392
393lemma get_cost_label_silent_is_empty : ∀S : abstract_status.
394∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
395#S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
396#H inversion H
397[#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
398destruct #_ @IH % assumption
399qed.
400
401lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
402∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
403silent_trace … t1 →
404get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
405#S #st1 #st2 #st3 #t1 elim t1
406[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 *
407[2: whd in match is_trace_non_empty; normalize nodelta * #ABS @⊥ @ABS %]
408#H inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
409#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
410#_ whd in ⊢ (??%?); >IH [%] %1 assumption
411qed.
412
413lemma silent_suffix_cancellable : ∀S : abstract_status.
414∀s1,s2,s2',s3,s3',s4 : S.∀l,l'.
415∀t1 : raw_trace … s1 s2. ∀prf : as_execute … l s2 s3.
416∀t2 : raw_trace … s3 s4.
417∀t1' :raw_trace … s1 s2'.∀prf' : as_execute … l' s2' s3'.
418∀t2' : raw_trace … s3' s4.
419is_costlabelled_act l → is_costlabelled_act l' →
420silent_trace … t2 → silent_trace … t2' →
421t1 @ (t_ind … prf t2) = t1' @ (t_ind … prf' t2') →
422s2 = s2' ∧ l = l' ∧ t1 ≃ t1'.
423#S #s1 #s2 #s2' #s3 #s3' #s4 #l #l' #t1 #prf #t2 #t1' #prf' #t2' #Hl #Hl' #sil_t2 #sil_t2'
424lapply prf -prf lapply prf' -prf' lapply t1' -t1' elim t1
425[ normalize #st * normalize
426  [ #st' #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct /3/
427  | #st1 #st2 #st3 #lbl #prf1 #tl #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
428    @⊥ lapply(silent_append_l2 … sil_t2) * [2: * #H cases(H I)] #H inversion H
429    [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
430    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl'
431    ]
432  ]
433]
434#st1 #st2 #st3 #lbl #prf1 #tl #IH #t1' inversion t1' in ⊢ ?;
435[ #st #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
436  @⊥ lapply(silent_append_l2 … sil_t2') * [2: * #H cases(H I)] #H inversion H
437    [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
438    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl
439    ]
440| #st1' #st2' #st3' #lbl' #prf1' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize
441  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct -EQ cases(IH … e0) * #EQ1 #EQ2 #EQ3 destruct /3/
442]
443qed.
444
445(*PRE-MEASURABLE TRACES*)
446
447inductive pre_measurable_trace (S : abstract_status) :
448∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝
449 | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st)
450 | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
451                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
452                      as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl →
453                      pre_measurable_trace … (t_ind … prf … tl)
454 | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel.
455                      as_classify … st1 ≠ cl_io →
456                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
457                      is_labelled_ret_act l → pre_measurable_trace … tl →
458                      pre_measurable_trace … (t_ind … prf … tl)
459 | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel.
460                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
461                      as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 →
462                      pre_measurable_trace … tl →
463                      pre_measurable_trace … (t_ind … prf … tl)
464 | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
465                      ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
466                      ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
467                      as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io
468                      →  is_call_act l1 → ¬ is_call_post_label … st1 →
469                      pre_measurable_trace … t1 → pre_measurable_trace … t2 →
470                      as_syntactical_succ S st1 st4 →
471                      is_unlabelled_ret_act l2 →
472                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
473                     
474lemma pre_measurable_trace_inv : ∀S : abstract_status.
475∀st1,st2 : S.∀t : raw_trace … st1 st2. pre_measurable_trace … t →
476(st1 = st2 ∧ as_classify … st1 ≠ cl_io ∧ t ≃ t_base … st1) ∨
477(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
478 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_cost_act l ∧
479 pre_measurable_trace … tl) ∨
480(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
481 t = t_ind … prf … tl ∧
482 as_classify … st1 ≠ cl_io ∧ is_labelled_ret_act l ∧ pre_measurable_trace … tl) ∨
483(∃st1' : S .∃l.∃prf : as_execute S l st1 st1'.∃tl.
484 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_call_act l ∧
485 (bool_to_Prop (is_call_post_label … st1)) ∧ pre_measurable_trace … tl) ∨
486(∃st1',st1'',st1''' : S.∃l1,l2.∃prf : as_execute S l1 st1 st1'.
487 ∃t1 : raw_trace S st1' st1''.∃t2 : raw_trace S st1''' st2.
488 ∃prf' : as_execute S l2 st1'' st1'''.
489 t = t_ind … prf … (t1 @ (t_ind … prf' … t2)) ∧ as_classify … st1 ≠cl_io ∧
490 as_classify … st1'' ≠ cl_io ∧ is_call_act l1 ∧
491 bool_to_Prop (¬ is_call_post_label … st1) ∧
492 pre_measurable_trace … t1 ∧ pre_measurable_trace … t2 ∧
493 as_syntactical_succ S st1 st1''' ∧ is_unlabelled_ret_act l2).
494#S #st1 #st2 #t #H inversion H
495[ #st #Hclass #EQ1 #EQ2 destruct #EQ destruct #_ %%%%% // % //
496| #st1' #st2' #st3' #l #prf #tl #Hst1' #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
497  %%%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
498| #st1' #st2' #st3' #l #Hst1 #prf #tl #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
499  %%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
500| #st1' #st2' #st3' #l #prf #tl #Hst1 #Hl #H1st1 #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
501  % %2 %{st2'} %{l} %{prf} %{tl} % // % // % // % //
502| #st1' #st2' #st3' #st4' #st5' #l1 #l2 #prf #t1 #t2 #prf' #Hst1' #Hst3' #Hl1
503  #H1st1'  #Ht1 #Ht2 #succ #Hl2 #_ #_ #EQ1 #EQ2 #EQ3 destruct #_ %2
504  %{st2'} %{st3'} %{st4'} %{l1} %{(ret_act (None ?))} %{prf} %{t1} %{t2}
505  %{prf'} /12 by conj/
506]
507qed.
508
509lemma append_premeasurable_silent : ∀S : abstract_status.
510∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
511pre_measurable_trace … t → silent_trace … t' → 
512pre_measurable_trace … (t' @ t).
513#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
514[ #st #t #Hpre #_ whd in ⊢ (????%); assumption]
515#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?;
516[ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
517#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
518destruct #_ whd in ⊢ (????%); %2
519[ assumption
520| %{(None ?)} %
521| @IH try assumption
522]
523% assumption
524qed.
525
526lemma pre_silent_is_premeasurable : ∀S : abstract_status.
527∀st1,st2 : S. ∀t : raw_trace S st1 st2.pre_silent_trace … t
528→ pre_measurable_trace … t.
529#S #st1 #st2 #t elim t
530[ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
531#st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
532-t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H in ⊢ ?;
533[ #st #H2 #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
534#_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
535@IH assumption
536qed.
537
538lemma append_silent_premeasurable : ∀S : abstract_status.
539∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
540pre_measurable_trace … t' → silent_trace … t →
541pre_measurable_trace … (t' @ t).
542#S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
543[ #st #Hst #r * [ #H1 @pre_silent_is_premeasurable assumption ]
544  inversion r [2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 cases H11
545  #ABS @⊥ @ABS % ] #s' #EQ1 #EQ2 #EQ3 destruct #_
546  %1 assumption
547|2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct
548  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ]
549  try ( %{x} %) try @IH try assumption % ]
550#s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
551#EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
552#r #pre_r normalize
553>append_tind_commute >append_tind_commute >append_associative
554<append_tind_commute in ⊢ (????(??????%)); %5
555try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
556qed.
557
558lemma head_of_premeasurable_is_not_io : ∀S : abstract_status.
559∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
560as_classify … st1 ≠ cl_io.
561#S #st1 #st2 #t #H inversion H //
562qed.
563
564lemma get_costlabels_of_trace_empty : ∀S : abstract_status.∀s1,s2 : S.∀t : raw_trace … s1 s2.
565get_costlabels_of_trace … t = nil ? → pre_measurable_trace … t → silent_trace … t.
566#S #s1 #s2 #t elim t [ #st #_ #_ %2 % * ] #st1 #st2 #st3 #l #prf #t' #IH #EQ #H -s1 -s2 inversion H
567[ #H1 #H2 #H3 #H4 #H5 #H6 destruct
568| #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
569| #s1 #s2 #s3 #l1 #Hclass #prf1 #tl * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
570| #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #f * #c #EQ destruct #Hs1 #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
571| #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hclass1 #Hclass3 * #f * #c #EQ destruct #Hs1
572  #pre1 #pre2 #Hs1s4 whd in match is_unlabelled_ret_act; normalize nodelta #EQ destruct #_ #_ #EQ1 #EQ2 #EQ3 #EQ4
573  destruct
574]
575whd in EQ : (??%?); destruct cases lbl in prf1 EQ; -lbl normalize [2: #lbl #H #EQ destruct]
576#prf #H % %2 // cases(IH …) // cases tl in pre_meas_tl;
577[2: #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 cases(absurd ?? H87) %]
578#st #H1 #_ % /2 by head_of_premeasurable_is_not_io/
579qed.
580
581(*NO-IO TRACES*)
582
583inductive no_io_trace (S : abstract_status) : ∀st1,st2 : S.raw_trace … st1 st2 → Prop ≝
584  t_base_io :∀st : S.as_classify … st ≠ cl_io →  no_io_trace S … (t_base … st)
585| t_ind_io : ∀st1,st2,st3 : S.∀l,prf.∀tl : raw_trace … st2 st3.as_classify … st1 ≠ cl_io →
586                   no_io_trace … tl → no_io_trace … (t_ind … st1 … l prf tl).
587
588lemma no_io_append : ∀S : abstract_status.
589∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
590∀t2 : raw_trace … st2 st3.
591no_io_trace … t1 → no_io_trace … t2 →
592no_io_trace … (t1 @ t2).
593#S #st1 #st2 #st3 #t1 lapply st3 elim t1
594[ #st #st3 #t2 #_ //]
595#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
596[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 destruct ]
597#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #_ destruct
598#H3 %2 // @IH //
599qed.
600
601lemma pre_measurable_no_io : ∀S : abstract_status.
602∀st1,st2 : S. ∀t : raw_trace … st1 st2.
603pre_measurable_trace … t →
604no_io_trace … t.
605#S #st1 #st2 #t #H elim H /2/ -st1-st2
606#st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf' #H1 #H2 #H3 #H4 #pre1 #pre2 #H5
607#H6 #IH1 #IH2 %2 // @no_io_append // %2 //
608qed.
609
610lemma head_of_no_io_is_no_io : ∀S : abstract_status.
611∀st1,st2 : S. ∀t : raw_trace … st1 st2.
612no_io_trace … t → as_classify … st1 ≠ cl_io.
613#S #st1 #st2 #t #H elim H //
614qed.
615
616
617lemma no_io_append_l1 : ∀S : abstract_status.
618∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
619∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) →
620no_io_trace … t1.
621#S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H % /2/]
622#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
623[ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
624#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct
625%2 // @IH //
626qed.
627
628lemma no_io_append_l2 : ∀S : abstract_status.
629∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
630∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) →
631no_io_trace … t2.
632#S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H assumption ]
633#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H @IH inversion H in ⊢ ?;
634[ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
635#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct //
636qed.
637
638(*MEASURABLE TRACES*)
639
640definition measurable :
641 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn →  Prop ≝
642λS,si,s1,s3,sn,t.
643 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
644 ∃l1,l2,prf1,prf2.
645 pre_measurable_trace … t12 ∧
646  t = ti0 @  t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n))
647 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ (is_call_act l2 → bool_to_Prop (is_call_post_label … s2))
648 ∧ silent_trace … ti0 ∧ silent_trace … t3n ∧ (is_call_act l1 → bool_to_Prop (is_call_post_label … s0)).
649
650 
651definition measurable_prefix ≝ 
652λS : abstract_status.
653λs1,s4 :S.
654λt : raw_trace … s1 s4.
655∃s2,s3 : S.∃t12 : raw_trace … s1 s2.
656∃l.∃prf : as_execute … l s2 s3.
657∃t34 : raw_trace … s3 s4.
658silent_trace … t12 ∧ t = t12 @ (t_ind … prf t34) ∧ is_costlabelled_act l.
659
660lemma measurable_prefix_of_premeasurable :
661∀S : abstract_status.
662∀s1,s4 : S.
663∀t : raw_trace … s1 s4.
664pre_measurable_trace … t →
665get_costlabels_of_trace … t ≠ nil ? →
666measurable_prefix … t.
667#S #s1 #s4 #t elim t
668[ #st #_ * #H @⊥ @H %]
669#st1 #st2 #st3 #l @(is_costlabelled_act_elim … l) -l
670[ #l #Hl #prf #t' #IH #_ #_ %{st1} %{st2} %{(t_base …)} %{l} %{prf} %{t'}
671  % // % // %2 normalize % *]
672#l #Hl #prf #t' #IH #H inversion H
673[ #st #H1 #H2 #H3 #H4 #H5 destruct
674| #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
675  cases l2 in Hl Hl2 prf2;
676  [ #f #c #_ * #z #EQ destruct
677  | * [|#lbl] #_ * #z #EQ destruct
678  | * [|#lbl * #H cases(H I)]
679  ]
680| #x1 #x2 #x3 #l2 #Hclass #prf2 #tl #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
681  cases l2 in Hl Hl2 prf2;
682  [ #f #c #_ * #z #EQ destruct
683  | #lbl1 #H1 * #z #EQ destruct cases H1 -H1 #H1 @⊥ @H1 %
684  | #lbl #_ * #z #EQ destruct
685  ]
686| #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #Hpost #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
687  cases l2 in Hl Hl2 prf2;
688  [ #f #c * #H @⊥ @H %
689  | #lbl1 #_ * #z * #z1 #EQ destruct
690  | #lbl #_ * #z * #z1 #EQ destruct
691  ]
692| #x1 #x2 #x3 #x4 #x5 #l2 #l3 #prf2 #tl1 #tl2 #prf3 #Hclass1 #Hclass2 #Hl2 #Hx1 #pre1 #pre2 #succ #Hl3
693  #_ #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
694  cases l2 in Hl Hl2 prf2;
695  [ #f #c * #H @⊥ @H %
696  | #lbl1 #_ * #z * #z1 #EQ destruct
697  | #lbl #_ * #z * #z1 #EQ destruct
698  ]
699]
700#_ #_ #prf #H1 cases(IH pre_tl ?)
701[2: % #EQ whd in H1 : (?(??%?)); >EQ in H1; * #H @H % ]
702#s2 * #s3 * #t12 * #l1 * #prf1 * #t34 ** #H2 #H3 #H4 %{s2} %{s3} %{(t_ind … prf t12)}
703%{l1} %{prf1} %{t34} % // %
704[ % %2 // cases H2 // inversion t12 [2: #z1 #z2 #z3 #lbl #prf5 #tl1 #_ #EQ1 #EQ2 #E3 destruct * #H @⊥ @H // ]
705  #st #EQ1 #EQ2 #EQ3 destruct #_ % /2 by head_of_premeasurable_is_not_io/
706| >H3 //
707]
708qed.
709
710definition measurable_suffix ≝
711 λS : abstract_status.λs1,s1' : S.λt : raw_trace … s1 s1'.
712∃s1_em : S.
713∃t_pre_em : raw_trace … s1 s1_em.
714∃s1_postem : S.
715     ∃t_post_em : raw_trace … s1_postem s1'.
716     silent_trace S ?? t_post_em ∧
717     ∃l_em : ActionLabel.
718     ∃ex_em : as_execute … l_em s1_em s1_postem.
719     t = t_pre_em @ (t_ind … ex_em t_post_em) ∧
720     (is_call_act l_em → bool_to_Prop(is_call_post_label … s1_em)) ∧
721     is_costlabelled_act l_em.
722     
723
724lemma measurable_suffix_tind : ∀S : abstract_status.
725∀s1,s2,s3 : S.∀l : ActionLabel.∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
726measurable_suffix … (t_ind … prf t) → (is_costlabelled_act l \wedge silent_trace … t) ∨ measurable_suffix … t.
727#S #s1 #s2 #s3 #l #prf #t lapply prf -prf lapply s1 -s1 cases t -t -s2 -s3
728[ #st #st1 #prf * #s_em * #t_pre * #s_post * #t_post * #sil_post * #l_em * #ex_em **
729 inversion t_pre in ⊢ ?;
730 [#st' #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
731  #_ /4 by or_introl, conj/
732 | #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct normalize in H34;
733   lapply(eq_to_jmeq ??? H34) -H34 #H34 destruct inversion H29 in ⊢ ?;
734   [ #H38 #H39 #H40 #H41 destruct
735   | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 destruct normalize in e1; destruct
736   ]
737 normalize in e0; destruct
738]
739]
740#s1 #s2 #s3 #l1 #prf1 #tl #s4 #prf * #s_em * #t_post lapply prf -prf cases t_post -t_post
741[ #s5 #prf * #s_post * #t_post * #sil_tpost * #l_em * #prf2 ** #EQ normalize in EQ;
742  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct /4/
743| #s5 #s6 #s7 #lbl #prf2 #tl1 #prf3 * #s_post * #t_post * #sil_tpost * #l_em * #ex_em **
744  #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost %2
745  >e0 whd %{s7} %{tl1} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/
746]
747qed.
748
749lemma measurable_suffix_append : ∀S : abstract_status.
750∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
751measurable_suffix … t2 → measurable_suffix … (t1 @ t2).
752#S #s1 #s2 #s3 #t1 #t2 * #s_em * #pre_t * #s_post * #t_post
753* #sil_tpost * #l_em * #prf ** #EQ destruct #Hcall #Hcost
754%{s_em} %{(t1@pre_t)} %{s_post} %{t_post} /7 by ex_intro, conj/
755qed.
756
757lemma measurable_suffix_append_l1 : ∀S : abstract_status.
758∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
759measurable_suffix … (t1 @ t2) → silent_trace … t2 → measurable_suffix … t1.
760#S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
761[#st #t2 * #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em * #exe ** #EQ normalize in EQ; destruct
762 #Hcall #Hcost #H lapply(silent_append_l2 … H) -H * [2: * #H cases(H I)] #H inversion H
763 [ #H113 #H114 #H115 #H116 #H117 #H118 destruct ]
764 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 destruct cases Hcost
765]
766#st1 #st2 #st3 #l #prf #tl #IH #t2 * #s_em * #t_pre inversion t_pre in ⊢ ?;
767[ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em
768  * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
769  #Hcall #Hcost #sil_t2 %{st} %{(t_base …)} %{s_post} %{tl} % [ /2 by silent_append_l1/]
770  %{l_em} %{ex_em} /4 by refl, conj/
771| #s #s' #s'' #l' #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em
772  ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost #H
773  change with ((t_ind ?????? (t_base …)) @ tl) in ⊢ (????%); @measurable_suffix_append @(IH t2) //
774  %{s''} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} % // % assumption
775]
776qed.
777
778lemma measurable_suffix_append_case : ∀S : abstract_status.
779∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
780measurable_suffix … (t1 @ t2) → (measurable_suffix … t1 ∧ silent_trace … t2) ∨ measurable_suffix … t2.
781#S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
782[ #st #t2 #H %2 assumption]
783#st1 #st2 #st3 #l #prf #tl #IH #t2 whd in match (append_on_trace ??????); #Hsuff
784cases(measurable_suffix_tind … Hsuff)
785[ * #_ #H %% [2: /2 by silent_append_l2/]  change with ((t_ind ?????? tl) @ t2) in Hsuff : (????%);
786 @(measurable_suffix_append_l1 … Hsuff) /2/
787| #H cases(IH … H)
788  [ * #H1 #H2 %% // change with ((t_ind ?????? (t_base …)) @ tl) in ⊢ (????%); @measurable_suffix_append //
789  | /2/
790  ]
791]
792qed.
793
794lemma measurable_is_measurable_suffix : ∀S : abstract_status.
795∀si,s1,s3,sn : S. ∀t : raw_trace … si sn.measurable …s1 s3 … t → measurable_suffix … t.
796#S #si #s1 #s3 #sn #t * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 ******* #_
797#EQ destruct /11 width=20 by conj,ex_intro/
798qed.
799
800lemma prefix_of_measurable_suffix_is_premeasurable : ∀S : abstract_status.
801∀s1,s2,s3,s4 :S.∀l.∀prf : as_execute … l s2 s3.
802∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s3 s4.∀t : raw_trace … s1 s4.
803pre_measurable_trace … t → t = (t1 @ (t_ind … prf t2)) → is_costlabelled_act l →
804silent_trace … t2 → (is_call_act l → bool_to_Prop(is_call_post_label … s2)) →
805pre_measurable_trace … t1.
806#S #s1 #s2 #s3 #s4 #l #prf #t1 #t2 #t #H lapply t1 -t1 lapply t2 -t2 lapply prf -prf lapply s2 -s2
807lapply s3 -s3 elim H -t -s1 -s4
808[ #st #_ #s1 #s2 #prf #r #p inversion p in ⊢ ?;
809  [ #H1 #H2 #H3 #H4 destruct #H5 #H6 #H7 normalize in H5; lapply(eq_to_jmeq ??? H5) -H5 #H5 destruct
810  | #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 destruct
811    normalize in H19; lapply(eq_to_jmeq ??? H19) -H19 #H19 destruct
812  ]
813| #st1 #st2 #st3 #lbl #prf #tl #Hclass **
814  [ #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?;
815    [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
816      destruct *
817    | #s3 #s4 #s5 #lab #exe #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?);
818      #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/
819    ]
820  | #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?;
821    [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
822      destruct #_ #_ #_ % //
823    | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
824      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/
825   ]
826 ]
827| #st1 #st2 #st3 #lbl #Hclass #prf #tl * #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1
828  #t1 #t2 inversion t2 in ⊢ ?;
829  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
830    destruct #_ #_ #_ % //
831  | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
832      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %3 /2/ @(IH … (refl …)) /2/
833  ]
834| #st1 #st2 #st3 #lbl #prf #tl #Hclass * #f * #c #EQ destruct #call_post #pre_tl #IH #s1 #s2 #prf1
835  #t1 #t2 inversion t2 in ⊢ ?;
836  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
837    destruct #_ #_ #_ % //
838  | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
839      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %4 /3/ @(IH … (refl …)) /2/
840  ]
841| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hst1 #Hst3 * #f * #c #EQ destruct
842  #Hcall #pre_t1 #pre_t2 #succ whd in ⊢ (% → ?); #EQ destruct #IH1 #IH2 #s1 #s2 #prf3
843  #t3 #t4 inversion t4 in ⊢ ?;
844  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
845    destruct #_ #_ #_ % //
846  | #s3 #s4 #s5 #lbl #prf4 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
847    lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t3 #H1
848    cut(measurable_suffix … (t1@(t_ind … prf2 t2)))
849    [ whd %{s5} %{tail} %{s1} %{t3} %{sil_t3} %{l} %{prf3} /4 by jmeq_to_eq, conj/]
850    #Hmeas cases(measurable_suffix_append_case … Hmeas)
851    [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
852      [ #H4 #H5 #H6 #H7 #H8 #H9 destruct
853      | #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
854      ]
855    | -Hmeas #Hmeas cases(measurable_suffix_tind … Hmeas)
856      [ **] -Hmeas -IH1 -EQ * #s_em * #t_pre * #s_post * #t_post * #sil_tpost
857      * #l_em * #ex_em ** #EQ destruct #H1 #H2
858      change with (t_ind … (t_base …) @ ?) in match (t_ind ???????) in e0;
859      <append_associative in e0; <append_associative #e0
860      cases(silent_suffix_cancellable … e0) // -e0 * #EQ1 #EQ2 #EQ3 destruct
861      >append_associative %5 /2/ [ %{f} %{c} //] normalize
862      @(IH2 … (refl …)) /2/
863     ]
864   ]
865 ]
866qed.
867
868(*
869
870lemma measurable_suffix_is_measurable:
871∀S : abstract_status.
872∀s1,s4 : S.
873∀t : raw_trace … s1 s4.
874pre_measurable_trace … t →
8752 ≤ |get_costlabels_of_trace … t | →
876measurable_suffix … t → ∃s1,s3.
877measurable … s1 … s3 … t.
878#S #s1 #s4 #t #pre_meas_t #Hlab * #s_em * #t_pre * #s_init * #t_post * #sil_tpost
879* #l_em * #ex_em ** #EQ destruct #Hcall #Hcost_lem
880>get_cost_label_append in Hlab; >append_length >get_costlabelled_is_costlabelled //
881>(get_cost_label_silent_is_empty … sil_tpost) #CARD
882cases(measurable_prefix_of_premeasurable … t_pre)
883[3: cases(get_costlabels_of_trace ????) in CARD; [ /3/ | #c #xc #_ % #EQ destruct]
884|2: @(prefix_of_measurable_suffix_is_premeasurable … pre_meas_t) [5: %|*:] assumption
885| #s_prefix * #s_post_pre * #t_prefix * #lab * #exe1 * #t34 ** #sil_tprefix #EQ destruct #cost_lab
886  /20 width=20 by conj,ex_intro/
887]
888qed.*)
Note: See TracBrowser for help on using the repository browser.