source: LTS/Traces.ma @ 3549

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

added paolo's trick

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