source: LTS/Traces.ma @ 3534

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

new notion of measurable: some lemmas are still broken

File size: 39.4 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
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*)
321
322inductive pre_silent_trace (S : abstract_status) :
323∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝
324| silent_empty : ∀st : S.as_classify … st ≠ cl_io → pre_silent_trace … (t_base S st)
325| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2.
326                ∀tl : raw_trace S st2 st3. as_classify … st1 ≠ cl_io → pre_silent_trace … tl →
327                pre_silent_trace … (t_ind … prf … tl).
328               
329definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
330raw_trace S st1 st2 → bool ≝
331λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
332
333definition silent_trace : ∀S:abstract_status.∀s1,s2 : S.
334raw_trace S s1 s2 → Prop ≝ λS,s1,s2,t.pre_silent_trace … t ∨
335¬ (bool_to_Prop (is_trace_non_empty … t)).
336
337lemma pre_silent_io : ∀S : abstract_status.
338∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t →
339as_classify … s2 ≠ cl_io.
340#S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
341#st1 #st2 #st3 #l #prf #tl #IH #H inversion H //
342#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
343#EQ destruct #_ @IH assumption
344qed.
345
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*)
443
444inductive pre_measurable_trace (S : abstract_status) :
445∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝
446 | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st)
447 | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel.
448                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
449                      as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl →
450                      pre_measurable_trace … (t_ind … prf … tl)
451 | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel.
452                      as_classify … st1 ≠ cl_io →
453                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
454                      is_labelled_ret_act l → pre_measurable_trace … tl →
455                      pre_measurable_trace … (t_ind … prf … tl)
456 | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel.
457                      ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3.
458                      as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 →
459                      pre_measurable_trace … tl →
460                      pre_measurable_trace … (t_ind … prf … tl)
461 | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
462                      ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3.
463                      ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4.
464                      as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io
465                      →  is_call_act l1 → ¬ is_call_post_label … st1 →
466                      pre_measurable_trace … t1 → pre_measurable_trace … t2 →
467                      as_syntactical_succ S st1 st4 →
468                      is_unlabelled_ret_act l2 →
469                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
470                     
471lemma pre_measurable_trace_inv : ∀S : abstract_status.
472∀st1,st2 : S.∀t : raw_trace … st1 st2. pre_measurable_trace … t →
473(st1 = st2 ∧ as_classify … st1 ≠ cl_io ∧ t ≃ t_base … st1) ∨
474(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
475 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_cost_act l ∧
476 pre_measurable_trace … tl) ∨
477(∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl.
478 t = t_ind … prf … tl ∧
479 as_classify … st1 ≠ cl_io ∧ is_labelled_ret_act l ∧ pre_measurable_trace … tl) ∨
480(∃st1' : S .∃l.∃prf : as_execute S l st1 st1'.∃tl.
481 t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_call_act l ∧
482 (bool_to_Prop (is_call_post_label … st1)) ∧ pre_measurable_trace … tl) ∨
483(∃st1',st1'',st1''' : S.∃l1,l2.∃prf : as_execute S l1 st1 st1'.
484 ∃t1 : raw_trace S st1' st1''.∃t2 : raw_trace S st1''' st2.
485 ∃prf' : as_execute S l2 st1'' st1'''.
486 t = t_ind … prf … (t1 @ (t_ind … prf' … t2)) ∧ as_classify … st1 ≠cl_io ∧
487 as_classify … st1'' ≠ cl_io ∧ is_call_act l1 ∧
488 bool_to_Prop (¬ is_call_post_label … st1) ∧
489 pre_measurable_trace … t1 ∧ pre_measurable_trace … t2 ∧
490 as_syntactical_succ S st1 st1''' ∧ is_unlabelled_ret_act l2).
491#S #st1 #st2 #t #H inversion H
492[ #st #Hclass #EQ1 #EQ2 destruct #EQ destruct #_ %%%%% // % //
493| #st1' #st2' #st3' #l #prf #tl #Hst1' #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
494  %%%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
495| #st1' #st2' #st3' #l #Hst1 #prf #tl #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
496  %%%2 %{st2'} %{l} %{prf} %{tl} % // % // % //
497| #st1' #st2' #st3' #l #prf #tl #Hst1 #Hl #H1st1 #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_
498  % %2 %{st2'} %{l} %{prf} %{tl} % // % // % // % //
499| #st1' #st2' #st3' #st4' #st5' #l1 #l2 #prf #t1 #t2 #prf' #Hst1' #Hst3' #Hl1
500  #H1st1'  #Ht1 #Ht2 #succ #Hl2 #_ #_ #EQ1 #EQ2 #EQ3 destruct #_ %2
501  %{st2'} %{st3'} %{st4'} %{l1} %{(ret_act (None ?))} %{prf} %{t1} %{t2}
502  %{prf'} /12 by conj/
503]
504qed.
505
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
637definition measurable :
638 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝
639λS,si,s1,s3,sn,t.
640 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
641 ∃l1,l2,prf1,prf2.
642 pre_measurable_trace … t12 ∧
643  t = ti0 @  t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n))
644 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ (is_call_act l2 → bool_to_Prop (is_call_post_label … s2))
645 ∧ silent_trace … ti0 ∧ silent_trace … t3n ∧ (is_call_act l1 → bool_to_Prop (is_call_post_label … s0)).
646
647 
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
865(*
866
867lemma measurable_suffix_is_measurable:
868∀S : abstract_status.
869∀s1,s4 : S.
870∀t : raw_trace … s1 s4.
871pre_measurable_trace … t →
8722 ≤ |get_costlabels_of_trace … t | →
873measurable_suffix … t → ∃s1,s3.
874measurable … s1 … s3 … t.
875#S #s1 #s4 #t #pre_meas_t #Hlab * #s_em * #t_pre * #s_init * #t_post * #sil_tpost
876* #l_em * #ex_em ** #EQ destruct #Hcall #Hcost_lem
877>get_cost_label_append in Hlab; >append_length >get_costlabelled_is_costlabelled //
878>(get_cost_label_silent_is_empty … sil_tpost) #CARD
879cases(measurable_prefix_of_premeasurable … t_pre)
880[3: cases(get_costlabels_of_trace ????) in CARD; [ /3/ | #c #xc #_ % #EQ destruct]
881|2: @(prefix_of_measurable_suffix_is_premeasurable … pre_meas_t) [5: %|*:] assumption
882| #s_prefix * #s_post_pre * #t_prefix * #lab * #exe1 * #t34 ** #sil_tprefix #EQ destruct #cost_lab
883  /20 width=20 by conj,ex_intro/
884]
885qed.*)
Note: See TracBrowser for help on using the repository browser.