source: LTS/Traces.ma @ 3580

Last change on this file since 3580 was 3576, checked in by piccolo, 4 years ago
File size: 46.0 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
280lemma eq_ActionLabel_elim : ∀P : bool → Prop.∀p,c1,c2.(c1 = c2 → P true) → (c1 ≠ c2 → P false) → P (eq_ActionLabel p c1 c2).
281#P #p * [#f #lab | * [| #lab] | * [| #lab] ] *
282[1,4,7,10,13: #f' #lab' |2,5,8,14: * [2,4,6,8: #lab'] |*: * [2,4,6,8,10,12: #lab'] ] #H1 #H2
283whd in match eq_ActionLabel; normalize nodelta
284try(@H2 % #EQ destruct)
285[ @eq_function_name_elim [ @eq_call_cost_lab_elim [| #H #_ lapply H -H ] ]  | @eq_return_cost_lab_elim | | @eq_fn_label_elim ]
286normalize nodelta
287[1,4,6,7,9: try(#EQ destruct) try(#EQ destruct) @H1 %
288|*: * #H @H2 % #EQ destruct cases H %
289]
290qed.
291
292definition DeqActionLabel ≝ λp.mk_DeqSet (ActionLabel p) (eq_ActionLabel p) ?.
293@hide_prf #x #y @eq_ActionLabel_elim [ #EQ destruct % // | * #H % #EQ destruct cases H %]
294qed.
295
296unification hint  0 ≔ p ;
297    X ≟ (DeqActionLabel p)
298(* ---------------------------------------- *) ⊢
299    (ActionLabel p) ≡ carr X.
300
301unification hint  0 ≔ p,p1,p2;
302    X ≟ (DeqActionLabel p)
303(* ---------------------------------------- *) ⊢
304    eq_ActionLabel p p1 p2 ≡ eqb X p1 p2.
305
306definition is_cost_label : ∀p.ActionLabel p → Prop ≝
307λp,act.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
308
309definition is_non_silent_cost_act : ∀p.ActionLabel p → Prop ≝
310λp,act. ∃l. act = cost_act … (Some ? l).
311
312definition is_cost_act : ∀p.ActionLabel p → Prop ≝
313λp,act.∃l.act = cost_act … l.
314
315definition is_call_act : ∀p.ActionLabel p → Prop ≝
316λp,act.∃f,l.act = call_act … f l.
317
318definition is_labelled_ret_act : ∀p.(ActionLabel p) → Prop ≝
319λp,act.∃l.act = ret_act … (Some ? l).
320
321definition is_unlabelled_ret_act : ∀p.ActionLabel p → Prop ≝
322λp,act.act = ret_act … (None ?).
323
324definition is_costlabelled_act : ∀p.ActionLabel p → Prop ≝
325λp,act.match act with [ call_act _ _ ⇒ True
326                    | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
327                    | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ]
328                    ].
329                   
330definition is_ret_call_act : ∀p.ActionLabel p → Prop ≝
331λp,a.match a with [ret_act _ ⇒ True | call_act _ _ ⇒ True | _ ⇒ False ].
332
333definition is_silent_cost_act_b : ∀p.ActionLabel p → bool ≝
334λp,act. match act with
335 [ cost_act x ⇒ match x with [None ⇒ true | _ ⇒ false ] | _ ⇒ false].
336                   
337lemma is_costlabelled_act_elim : ∀p.
338∀P : ActionLabel p → Prop.
339(∀l. is_costlabelled_act p l → P l) →
340(∀l. ¬is_costlabelled_act p l → P l) →
341∀l.P l. #p
342#P #H1 #H2 * /2/
343[ * /2/ @H2 % *] * /2/ @H2 %*
344qed.
345
346lemma eq_a_call_label : ∀p.
347∀c1,c2.c1 == c2 → a_call p c1 == a_call p c2.
348#p #c1 #c2 #EQ cases(eqb_true ? c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ
349#EQ destruct >(\b (refl …)) @I
350qed.
351
352lemma eq_a_non_functional_label : ∀p.
353∀c1,c2.c1 == c2 → a_non_functional_label p c1 == a_non_functional_label p c2.
354#p #c1 #c2 #EQ cases(eqb_true (DEQNonFunctionalLabel ?) c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ
355#EQ destruct >(\b (refl …)) @I
356qed.
357
358(* TOOLS FOR FRESHING LABELS *)
359
360definition fresh_nf_label : ∀p : label_params.p → NonFunctionalLabel p × p ≝
361λp,x.〈a_non_functional_label … (succ_label … p x),(succ_label … p x)〉.
362
363definition fresh_cc_labe : ∀p : label_params.p → CallCostLabel p × p ≝
364λp,x.〈a_call_label … (succ_label … p x),(succ_label … p x)〉.
365
366definition fresh_rc_label : ∀p : label_params.p → ReturnPostCostLabel p × p ≝
367λp,x.〈a_return_cost_label … (succ_label … p x),(succ_label … p x)〉.
368
369
370(*ABSTRACT STATUS*)
371
372inductive status_class : Type[0] ≝
373 | cl_jump : status_class
374 | cl_io : status_class
375 | cl_other : status_class.
376 
377record abstract_status (p : label_params) : Type[2] ≝
378 { as_status :> Type[0]
379 ; as_execute : (ActionLabel p) → relation as_status
380 ; as_syntactical_succ : relation as_status
381 ; as_classify : as_status → status_class
382 ; is_call_post_label : as_status → bool
383 ; as_initial : as_status → bool
384 ; as_final : as_status → bool
385 ; jump_emits : ∀s1,s2,l.
386      as_classify … s1 = cl_jump →
387      as_execute l s1 s2 → is_non_silent_cost_act … l
388 ; io_entering : ∀s1,s2,l.as_classify … s2 = cl_io →
389      as_execute l s1 s2 → is_non_silent_cost_act … l
390 ; io_exiting : ∀s1,s2,l.as_classify … s1 = cl_io →
391     as_execute l s1 s2 → is_non_silent_cost_act … l
392 }.
393
394(* RAW TRACES *)
395
396inductive raw_trace (p : label_params) (S : abstract_status p) : S → S → Type[0] ≝
397  | t_base : ∀st : S.raw_trace … S st st
398  | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel p.
399             as_execute … S l st1 st2 → raw_trace … S st2 st3 →
400             raw_trace … S st1 st3.
401             
402
403let rec append_on_trace (p : label_params) (S : abstract_status p) (st1 : S) (st2 : S) (st3 : S)
404(t1 : raw_trace … S st1 st2) on t1 : raw_trace …  S st2 st3 → raw_trace … S st1 st3 ≝
405match t1
406return λst1,st2,tr.raw_trace … S st2 st3 → raw_trace … S st1 st3
407with
408[ t_base st ⇒ λt2.t2
409| t_ind st1' st2' st3' l prf tl ⇒ λt2.t_ind … prf … (append_on_trace … tl t2)
410].
411
412interpretation "trace_append" 'append t1 t2 = (append_on_trace ????? t1 t2).
413
414let rec len (p : label_params) (s : abstract_status p) (st1 : s) (st2 : s) (t : raw_trace p s st1 st2)
415on t : ℕ ≝
416match t with
417[ t_base s ⇒ O
418| t_ind s1 s2 s3 l prf lt ⇒ S (len … lt)
419].
420
421lemma len_append : ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.
422∀t1 : raw_trace … st1 st2.∀t2 : raw_trace … st2 st3.
423len  ???? (t1 @ t2)  = (len  ????  t1) + (len  ???? t2).
424#p #S #st1 #st2 #st3 #t1 elim t1 normalize //
425qed.
426
427lemma append_nil_is_nil : ∀p. ∀S : abstract_status p.
428∀s1,s2 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s1.
429t1 @ t2 = t_base … s1 → s1 = s2 ∧ t1 ≃ t_base … s1 ∧ t2 ≃ t_base … s1.
430#p #S #s1 #s2 #t1 elim t1 -t1 -s1 -s2
431[ #st #t2 normalize #EQ destruct /3 by refl_jmeq, conj/]
432#s1 #s2 #s3 #l #prf #t2 #IH #t2 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
433qed.
434
435lemma append_associative : ∀p.∀S,st1,st2,st3,st4.
436∀t1 : raw_trace p S st1 st2.∀t2 : raw_trace … S st2 st3.
437∀t3 : raw_trace … S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3).
438#p #S #st1 #st2 #st3 #st4 #t1 elim t1 -t1
439[ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH %
440qed.
441
442definition trace_prefix: ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.raw_trace … st1 st2 →
443raw_trace … st1 st3 → Prop≝
444λp,S,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3.
445
446definition trace_suffix : ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.raw_trace … st2 st3 →
447raw_trace … st1 st3 → Prop≝
448λp,S,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
449
450definition actionlabel_to_costlabel ≝ λp.
451λl : ActionLabel p.match l with
452    [ call_act f c ⇒ [ c ]
453    | ret_act x ⇒ match x with
454                  [ Some c ⇒ [ a_return_post … c ]
455                  | None ⇒ []
456                  ]
457    | cost_act x ⇒ match x with
458                  [ Some c ⇒ [ a_non_functional_label  … c ]
459                  | None ⇒ []
460                  ]
461   ].
462
463let rec get_costlabels_of_trace (p : label_params) (S : abstract_status p) (st1 : S) (st2 : S)
464(t : raw_trace p S st1 st2) on t : list (CostLabel p) ≝
465match t with
466[ t_base st ⇒ [ ]
467| t_ind st1' st2' st3' l prf t' ⇒
468    let tl ≝ get_costlabels_of_trace … t' in
469    actionlabel_to_costlabel … l  @ tl
470].
471
472lemma get_cost_label_append : ∀p.∀S : abstract_status p.∀st1,st2,st3 : S.
473∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
474get_costlabels_of_trace … (t1 @ t2) =
475 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
476#p #S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
477[#f * #l | * [| * #l] | *  [| #l] ] #prf #tl #IH #t2 normalize try @eq_f @IH
478qed.
479
480lemma append_tind_commute : ∀p.∀S : abstract_status p.∀st1,st2,st3,st4 : S.∀l.
481    ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace p S st2 st3.
482    ∀t2 : raw_trace p S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2.
483#p #S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.
484
485lemma get_costlabelled_is_costlabelled :
486∀p.∀S : abstract_status p.∀s1,s2,s3 : S. ∀l.
487∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
488is_costlabelled_act p l →
489|get_costlabels_of_trace … (t_ind … prf t)| = 1 + |get_costlabels_of_trace … t|.
490#p #S #s1 #s2 #s3 * normalize
491  [ /2 by monotonic_pred/
492  | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
493  | * normalize /2 by lt_to_le, monotonic_pred/ #_ #t *
494  ]
495qed.
496
497(*SILENT TRACES*)
498
499inductive pre_silent_trace (p : label_params) (S : abstract_status p) :
500∀st1,st2 : S.raw_trace p S st1 st2 → Prop ≝
501| silent_empty : ∀st : S.as_classify … st ≠ cl_io → pre_silent_trace … (t_base p S st)
502| silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute p S (cost_act  … (None ?)) st1 st2.
503                ∀tl : raw_trace p S st2 st3. as_classify … st1 ≠ cl_io → pre_silent_trace … tl →
504                pre_silent_trace … (t_ind … prf … tl).
505               
506definition is_trace_non_empty : ∀p.∀S : abstract_status p.∀st1,st2.
507raw_trace p S st1 st2 → bool ≝
508λp,S,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
509
510definition silent_trace : ∀p.∀S:abstract_status p.∀s1,s2 : S.
511raw_trace p S s1 s2 → Prop ≝ λp,S,s1,s2,t.pre_silent_trace … t ∨
512¬ (bool_to_Prop (is_trace_non_empty … t)).
513
514lemma pre_silent_io : ∀p.∀S : abstract_status p.
515∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t →
516as_classify … s2 ≠ cl_io.
517#p #S #s1 #s2 #t elim t [ #st #H inversion H // #st1 #st2 #st3 #prf #tl #H1 #sil_tl #_ #EQ1 #EQ2 #EQ3 destruct]
518#st1 #st2 #st3 #l #prf #tl #IH #H inversion H //
519#st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct
520#EQ destruct #_ @IH assumption
521qed.
522
523lemma append_silent : ∀p.∀S : abstract_status p.
524∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.
525∀t2 : raw_trace … s2 s3.silent_trace … t1 →
526silent_trace … t2 →
527silent_trace … (t1 @ t2).
528#p #S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
529[ #st #t2 #_ * /2 by or_introl, or_intror/ ]
530#st1 #st2 #st3 #l #prf #tl #IH #t2 *
531[2: * #H cases(H I) ] #H inversion H in ⊢ ?;
532[ #st #H1 #H2 #H3 #H4 #H5 #H6 destruct ]
533#st1' #st2' #st3' #prf' #tl' #Hst1' #Htl' #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
534#Ht2 % %2 // cases(IH … Ht2) /2/
535inversion(tl' @ t2)
536[2: #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 * #H cases (H I) ]
537#st #EQ1 #EQ2 destruct #H cases(append_nil_is_nil … H) * #EQ1 #EQ2 #EQ3 destruct //
538qed.
539
540lemma silent_append_l2 : ∀p.∀S : abstract_status p.
541∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
542silent_trace … (t1 @ t2) → silent_trace … t2.
543#p #S #s1 #s2 #s3 #t1 elim t1 // -s1 -s2
544#st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)]
545#H @IH % inversion H in ⊢ ?;
546[ #H42 #H43 #H44 #H45 normalize #H46 #H47 destruct
547| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 normalize in H59; destruct assumption
548]
549qed.
550
551lemma silent_append_l1 : ∀p.∀S : abstract_status p.
552∀s1,s2,s3 :S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
553silent_trace … (t1 @ t2) → silent_trace … t1.
554#p #S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
555[ #st #t2 #_ %2 % *]
556#st1 #st2 #st3 #l #prf #tl #IH #t2 * [2: * #H cases(H I)] #H
557% inversion H in ⊢ ?; [ #H62 #H63 #H64 #H65 #H66 #H67 normalize in H66; destruct]
558#z1 #z2 #z3 #prf' #tl' #Hclass #Htl' #_ #EQ1 #EQ2 #EQ3 normalize in EQ3; #EQ4 destruct
559%2 // cases(IH t2 …) /2/ inversion tl
560[2: #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 destruct cases H79 #H cases(H I) ]
561#st #EQ1 #EQ2 #EQ3 destruct #_ % normalize in Htl'; inversion Htl'
562[ #H81 #H82 #H83 #H84 #H85 #H86 destruct //
563| #H88 #H89 #H90 #H91 #H92 #H93 #H94 #H95 #H96 #H97 #H98 #H99 destruct //
564]
565qed.
566
567lemma get_cost_label_silent_is_empty : ∀p.∀S : abstract_status p.
568∀st1,st2.∀t : raw_trace p S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
569#p #S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
570#H inversion H
571[#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
572destruct #_ @IH % assumption
573qed.
574
575lemma get_cost_label_invariant_for_append_silent_trace_l :∀p.∀S : abstract_status p.
576∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2 : raw_trace … st2 st3.
577silent_trace … t1 →
578get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
579#p #S #st1 #st2 #st3 #t1 elim t1
580[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 *
581[2: whd in match is_trace_non_empty; normalize nodelta * #ABS @⊥ @ABS %]
582#H inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
583#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
584#_ whd in ⊢ (??%?); >IH [%] %1 assumption
585qed.
586
587lemma silent_suffix_cancellable : ∀p.∀S : abstract_status p.
588∀s1,s2,s2',s3,s3',s4 : S.∀l,l'.
589∀t1 : raw_trace … s1 s2. ∀prf : as_execute … l s2 s3.
590∀t2 : raw_trace … s3 s4.
591∀t1' :raw_trace … s1 s2'.∀prf' : as_execute … l' s2' s3'.
592∀t2' : raw_trace … s3' s4.
593is_costlabelled_act … l → is_costlabelled_act … l' →
594silent_trace … t2 → silent_trace … t2' →
595t1 @ (t_ind … prf t2) = t1' @ (t_ind … prf' t2') →
596s2 = s2' ∧ l = l' ∧ t1 ≃ t1'.
597#p #S #s1 #s2 #s2' #s3 #s3' #s4 #l #l' #t1 #prf #t2 #t1' #prf' #t2' #Hl #Hl' #sil_t2 #sil_t2'
598lapply prf -prf lapply prf' -prf' lapply t1' -t1' elim t1
599[ normalize #st * normalize
600  [ #st' #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct /3/
601  | #st1 #st2 #st3 #lbl #prf1 #tl #prf' #prf #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
602    @⊥ lapply(silent_append_l2 … sil_t2) * [2: * #H cases(H I)] #H inversion H
603    [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
604    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl'
605    ]
606  ]
607]
608#st1 #st2 #st3 #lbl #prf1 #tl #IH #t1' inversion t1' in ⊢ ?;
609[ #st #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
610  @⊥ lapply(silent_append_l2 … sil_t2') * [2: * #H cases(H I)] #H inversion H
611    [ #H1 #H2 #H3 #H4 #H5 #H6 destruct
612    | #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 destruct cases Hl
613    ]
614| #st1' #st2' #st3' #lbl' #prf1' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #prf' #prf normalize
615  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct -EQ cases(IH … e0) * #EQ1 #EQ2 #EQ3 destruct /3/
616]
617qed.
618
619(*PRE-MEASURABLE TRACES*)
620
621inductive pre_measurable_trace (p : label_params) (S : abstract_status p) :
622∀st1,st2 : S.raw_trace … st1 st2 → Prop ≝
623 | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base … st)
624 | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel p.
625                      ∀prf : as_execute … l st1 st2.∀tl : raw_trace … st2 st3.
626                      as_classify … st1 ≠ cl_io → is_cost_act … l → pre_measurable_trace … tl →
627                      pre_measurable_trace … (t_ind … prf … tl)
628 | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel p.
629                      as_classify … st1 ≠ cl_io →
630                      ∀prf : as_execute … l st1 st2.∀tl : raw_trace … st2 st3.
631                      is_labelled_ret_act … l → pre_measurable_trace … tl →
632                      pre_measurable_trace … (t_ind … prf … tl)
633 | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel p.
634                      ∀prf : as_execute … l st1 st2.∀tl : raw_trace … st2 st3.
635                      as_classify … st1 ≠ cl_io → is_call_act … l → is_call_post_label … st1 →
636                      pre_measurable_trace … tl →
637                      pre_measurable_trace … (t_ind … prf … tl)
638 | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2.
639                      ∀prf : as_execute … l1 st1 st2.∀t1 : raw_trace … st2 st3.
640                      ∀t2 : raw_trace … st4 st5.∀prf' : as_execute … l2 st3 st4.
641                      as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io
642                      →  is_call_act … l1 → ¬ is_call_post_label … st1 →
643                      pre_measurable_trace … t1 → pre_measurable_trace … t2 →
644                      as_syntactical_succ … st1 st4 →
645                      is_unlabelled_ret_act … l2 →
646                      pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))).
647
648lemma append_premeasurable : ∀p.∀S : abstract_status p.
649∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.∀t2: raw_trace … st2 st3.
650pre_measurable_trace … t1 → pre_measurable_trace … t2 →
651pre_measurable_trace … (t1 @ t2).
652#p #S #st1 #st2 #st3 #t1 #t2 #Hpre lapply t2 -t2 elim Hpre -Hpre //
653[ #s1 #s2 #s3 #l #prf #tl #Hclass #Hcost #pre_tl #IH #t2 #pr3_t2
654  %2 // @IH //
655| #s1 #s2 #s3 #l #Hclass #prf #tl #ret_l #pre_tl #IH #t2 #pre_t2 %3 // @IH //
656| #s1 #s2 #s3 #l #prf #tl #Hclass #call #callp #pre_tl #IH #t2 #pre_t2 %4 // @IH //
657| #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #tl1 #tl2 #prf2 #Hclass1 #Hclass3 #call_l1
658  #nopost #pre_tl1 #pre_tl2 #succ #unlab #IH1 #IH2 #t2 #pre_t2
659  normalize >append_associative in ⊢ (?????(????????%)); %5 // @IH2 //
660]
661qed.
662
663lemma append_premeasurable_silent : ∀p.∀S : abstract_status p.
664∀st1',st1,st2 : S.∀t : raw_trace … st1 st2.∀t' : raw_trace … st1' st1.
665pre_measurable_trace … t → silent_trace … t' → 
666pre_measurable_trace … (t' @ t).
667#p #S #st1' #st1 #st2 #t #t' lapply t -t elim t'
668[ #st #t #Hpre #_ whd in ⊢ (?????%); assumption]
669#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?;
670[ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
671#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
672destruct #_ whd in ⊢ (?????%); %2
673[ assumption
674| %{(None ?)} %
675| @IH try assumption
676]
677% assumption
678qed.
679
680lemma pre_silent_is_premeasurable : ∀p.∀S : abstract_status p.
681∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_silent_trace … t
682→ pre_measurable_trace … t.
683#p #S #st1 #st2 #t elim t
684[ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
685#st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
686-t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H in ⊢ ?;
687[ #st #H2 #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
688#_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
689@IH assumption
690qed.
691
692lemma append_silent_premeasurable : ∀p.∀S : abstract_status p.
693∀st1',st1,st2 : S.∀t : raw_trace … st1 st2.∀t' : raw_trace … st1' st1.
694pre_measurable_trace … t' → silent_trace … t →
695pre_measurable_trace … (t' @ t).
696#p #S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
697[ #st #Hst #r * [ #H1 @pre_silent_is_premeasurable assumption ]
698  inversion r [2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 cases H11
699  #ABS @⊥ @ABS % ] #s' #EQ1 #EQ2 #EQ3 destruct #_
700  %1 assumption
701|2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct
702  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ]
703  try ( %{x} %) try @IH try assumption % ]
704#s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
705#EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
706#r #pre_r normalize
707>append_tind_commute >append_tind_commute >append_associative
708<append_tind_commute in ⊢ (?????(???????%)); %5
709try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
710qed.
711
712lemma head_of_premeasurable_is_not_io : ∀p.∀S : abstract_status p.
713∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
714as_classify … st1 ≠ cl_io. #p
715#S #st1 #st2 #t #H inversion H //
716qed.
717
718lemma get_costlabels_of_trace_empty : ∀p.∀S : abstract_status p.∀s1,s2 : S.∀t : raw_trace … s1 s2.
719get_costlabels_of_trace … t = nil ? → pre_measurable_trace … t → silent_trace … t.
720#p #S #s1 #s2 #t elim t [ #st #_ #_ %2 % * ] #st1 #st2 #st3 #l #prf #t' #IH #EQ #H -s1 -s2 inversion H
721[ #H1 #H2 #H3 #H4 #H5 #H6 destruct
722| #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
723| #s1 #s2 #s3 #l1 #Hclass #prf1 #tl * #lbl #EQ destruct #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
724| #s1 #s2 #s3 #l1 #prf1 #tl #Hclass * #f * #c #EQ destruct #Hs1 #pre_meas_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
725| #s1 #s2 #s3 #s4 #s5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hclass1 #Hclass3 * #f * #c #EQ destruct #Hs1
726  #pre1 #pre2 #Hs1s4 whd in match is_unlabelled_ret_act; normalize nodelta #EQ destruct #_ #_ #EQ1 #EQ2 #EQ3 #EQ4
727  destruct
728]
729whd in EQ : (??%?); destruct cases lbl in prf1 EQ; -lbl normalize [2: #lbl #H #EQ destruct]
730#prf #H % %2 // cases(IH …) // cases tl in pre_meas_tl;
731[2: #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 cases(absurd ?? H87) %]
732#st #H1 #_ % /2 by head_of_premeasurable_is_not_io/
733qed.
734
735(*NO-IO TRACES*)
736
737inductive no_io_trace (p : label_params) (S : abstract_status p) : ∀st1,st2 : S.raw_trace … st1 st2 → Prop ≝
738  t_base_io :∀st : S.as_classify … st ≠ cl_io →  no_io_trace … S … (t_base … st)
739| t_ind_io : ∀st1,st2,st3 : S.∀l,prf.∀tl : raw_trace … st2 st3.as_classify … st1 ≠ cl_io →
740                   no_io_trace … tl → no_io_trace … (t_ind … st1 … l prf tl).
741
742lemma no_io_append : ∀p.∀S : abstract_status p.
743∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
744∀t2 : raw_trace … st2 st3.
745no_io_trace … t1 → no_io_trace … t2 →
746no_io_trace … (t1 @ t2).
747#p #S #st1 #st2 #st3 #t1 lapply st3 elim t1
748[ #st #st3 #t2 #_ //]
749#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
750[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 destruct ]
751#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #_ destruct
752#H3 %2 // @IH //
753qed.
754
755lemma pre_measurable_no_io : ∀p.∀S : abstract_status p.
756∀st1,st2 : S. ∀t : raw_trace … st1 st2.
757pre_measurable_trace … t →
758no_io_trace … t.
759#p #S #st1 #st2 #t #H elim H /2/ -st1-st2
760#st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf' #H1 #H2 #H3 #H4 #pre1 #pre2 #H5
761#H6 #IH1 #IH2 %2 // @no_io_append // %2 //
762qed.
763
764lemma head_of_no_io_is_no_io : ∀p.∀S : abstract_status p.
765∀st1,st2 : S. ∀t : raw_trace … st1 st2.
766no_io_trace … t → as_classify … st1 ≠ cl_io.
767#p #S #st1 #st2 #t #H elim H //
768qed.
769
770
771lemma no_io_append_l1 : ∀p.∀S : abstract_status p.
772∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
773∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) →
774no_io_trace … t1.
775#p #S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H % /2/]
776#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H inversion H in ⊢ ?;
777[ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
778#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct
779%2 // @IH //
780qed.
781
782lemma no_io_append_l2 : ∀p.∀S : abstract_status p.
783∀st1,st2,st3 : S.∀t1 : raw_trace … st1 st2.
784∀t2 : raw_trace … st2 st3.no_io_trace … (t1 @ t2) →
785no_io_trace … t2.
786#p #S #st1 #st2 #st3 #t1 lapply st3 elim t1 [ #st #st3 #t2 normalize #H assumption ]
787#s #s' #s'' #l #prf #tl #IH #st3 #t2 #H @IH inversion H in ⊢ ?;
788[ #H9 #H10 #H11 #H12 #H13 #H14 destruct normalize in H13; destruct ]
789#st #st' #st'' #l' #prf' #tl' #H1 #H2 #_ #EQ1 #EQ2 #EQ3 #EQ4 normalize in EQ3 EQ4; destruct //
790qed.
791
792(*MEASURABLE TRACES*)
793
794definition measurable : ∀p.
795 ∀S: abstract_status p. ∀si,s1,s3,sn : S. raw_trace … si sn →  Prop ≝
796λp,S,si,s1,s3,sn,t.
797 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn.
798 ∃l1,l2,prf1,prf2.
799 pre_measurable_trace p … t12 ∧
800  t = ti0 @  t_ind … s0 s1 sn l1 prf1 … (t12 @ (t_ind … s2 s3 sn l2 prf2 … t3n))
801 ∧ is_costlabelled_act … l1 ∧ is_costlabelled_act … l2 ∧ (is_call_act … l2 → bool_to_Prop (is_call_post_label … s2))
802 ∧ silent_trace … ti0 ∧ silent_trace … t3n ∧ (is_call_act … l1 → bool_to_Prop (is_call_post_label … s0)).
803
804 
805definition measurable_prefix ≝  λp.
806λS : abstract_status p.
807λs1,s4 :S.
808λt : raw_trace … s1 s4.
809∃s2,s3 : S.∃t12 : raw_trace … s1 s2.
810∃l.∃prf : as_execute … l s2 s3.
811∃t34 : raw_trace … s3 s4.
812silent_trace … t12 ∧ t = t12 @ (t_ind … prf t34) ∧ is_costlabelled_act … l.
813
814lemma measurable_prefix_of_premeasurable :
815∀p.
816∀S : abstract_status p.
817∀s1,s4 : S.
818∀t : raw_trace … s1 s4.
819pre_measurable_trace … t →
820get_costlabels_of_trace … t ≠ nil ? →
821measurable_prefix … t.
822#p #S #s1 #s4 #t elim t
823[ #st #_ * #H @⊥ @H %]
824#st1 #st2 #st3 #l @(is_costlabelled_act_elim … l) -l
825[ #l #Hl #prf #t' #IH #_ #_ %{st1} %{st2} %{(t_base …)} %{l} %{prf} %{t'}
826  % // % // %2 normalize % *]
827#l #Hl #prf #t' #IH #H inversion H
828[ #st #H1 #H2 #H3 #H4 #H5 destruct
829| #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
830  cases l2 in Hl Hl2 prf2;
831  [ #f #c #_ * #z #EQ destruct
832  | * [|#lbl] #_ * #z #EQ destruct
833  | * [|#lbl * #H cases(H I)]
834  ]
835| #x1 #x2 #x3 #l2 #Hclass #prf2 #tl #Hl2 #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
836  cases l2 in Hl Hl2 prf2;
837  [ #f #c #_ * #z #EQ destruct
838  | #lbl1 #H1 * #z #EQ destruct cases H1 -H1 #H1 @⊥ @H1 %
839  | #lbl #_ * #z #EQ destruct
840  ]
841| #x1 #x2 #x3 #l2 #prf2 #tl #Hclass #Hl2 #Hpost #pre_tl #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
842  cases l2 in Hl Hl2 prf2;
843  [ #f #c * #H @⊥ @H %
844  | #lbl1 #_ * #z * #z1 #EQ destruct
845  | #lbl #_ * #z * #z1 #EQ destruct
846  ]
847| #x1 #x2 #x3 #x4 #x5 #l2 #l3 #prf2 #tl1 #tl2 #prf3 #Hclass1 #Hclass2 #Hl2 #Hx1 #pre1 #pre2 #succ #Hl3
848  #_ #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
849  cases l2 in Hl Hl2 prf2;
850  [ #f #c * #H @⊥ @H %
851  | #lbl1 #_ * #z * #z1 #EQ destruct
852  | #lbl #_ * #z * #z1 #EQ destruct
853  ]
854]
855#_ #_ #prf #H1 cases(IH pre_tl ?)
856[2: % #EQ whd in H1 : (?(??%?)); >EQ in H1; * #H @H % ]
857#s2 * #s3 * #t12 * #l1 * #prf1 * #t34 ** #H2 #H3 #H4 %{s2} %{s3} %{(t_ind … prf t12)}
858%{l1} %{prf1} %{t34} % // %
859[ % %2 // cases H2 // inversion t12 [2: #z1 #z2 #z3 #lbl #prf5 #tl1 #_ #EQ1 #EQ2 #E3 destruct * #H @⊥ @H // ]
860  #st #EQ1 #EQ2 #EQ3 destruct #_ % /2 by head_of_premeasurable_is_not_io/
861| >H3 //
862]
863qed.
864
865definition measurable_suffix ≝
866λp. λS : abstract_status p.λs1,s1' : S.λt : raw_trace … s1 s1'.
867∃s1_em : S.
868∃t_pre_em : raw_trace … s1 s1_em.
869∃s1_postem : S.
870     ∃t_post_em : raw_trace … s1_postem s1'.
871     silent_trace … S ?? t_post_em ∧
872     ∃l_em : ActionLabel p.
873     ∃ex_em : as_execute … l_em s1_em s1_postem.
874     t = t_pre_em @ (t_ind … ex_em t_post_em) ∧
875     (is_call_act … l_em → bool_to_Prop(is_call_post_label … s1_em)) ∧
876     is_costlabelled_act … l_em.
877     
878
879lemma measurable_suffix_tind : ∀p.∀S : abstract_status p.
880∀s1,s2,s3 : S.∀l : ActionLabel p.∀prf : as_execute … l s1 s2.∀t : raw_trace … s2 s3.
881measurable_suffix … (t_ind … prf t) → (is_costlabelled_act … l ∧ silent_trace … t) ∨ measurable_suffix … t.
882#p #S #s1 #s2 #s3 #l #prf #t lapply prf -prf lapply s1 -s1 cases t -t -s2 -s3
883[ #st #st1 #prf * #s_em * #t_pre * #s_post * #t_post * #sil_post * #l_em * #ex_em **
884 inversion t_pre in ⊢ ?;
885 [#st' #EQ1 #EQ2 #EQ3 destruct #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
886  #_ /4 by or_introl, conj/
887 | #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct normalize in H34;
888   lapply(eq_to_jmeq ??? H34) -H34 #H34 destruct inversion H29 in ⊢ ?;
889   [ #H38 #H39 #H40 #H41 destruct
890   | #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 destruct normalize in e1; destruct
891   ]
892 normalize in e0; destruct
893]
894]
895#s1 #s2 #s3 #l1 #prf1 #tl #s4 #prf * #s_em * #t_post lapply prf -prf cases t_post -t_post
896[ #s5 #prf * #s_post * #t_post * #sil_tpost * #l_em * #prf2 ** #EQ normalize in EQ;
897  lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct /4/
898| #s5 #s6 #s7 #lbl #prf2 #tl1 #prf3 * #s_post * #t_post * #sil_tpost * #l_em * #ex_em **
899  #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost %2
900  >e0 whd %{s7} %{tl1} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} /4 by conj/
901]
902qed.
903
904lemma measurable_suffix_append : ∀p.∀S : abstract_status p.
905∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
906measurable_suffix … t2 → measurable_suffix … (t1 @ t2).
907#p #S #s1 #s2 #s3 #t1 #t2 * #s_em * #pre_t * #s_post * #t_post
908* #sil_tpost * #l_em * #prf ** #EQ destruct #Hcall #Hcost
909%{s_em} %{(t1@pre_t)} %{s_post} %{t_post} /7 by ex_intro, conj/
910qed.
911
912lemma measurable_suffix_append_l1 : ∀p.∀S : abstract_status p.
913∀s1,s2,s3 : S.∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
914measurable_suffix … (t1 @ t2) → silent_trace … t2 → measurable_suffix … t1.
915#p #S #s1 #s2 #s3 #t1 elim t1 -t1 -s1 -s2
916[#st #t2 * #s_em * #t_pre * #s_post * #t_post * #sil_tpost * #l_em * #exe ** #EQ normalize in EQ; destruct
917 #Hcall #Hcost #H lapply(silent_append_l2 … H) -H * [2: * #H cases(H I)] #H inversion H
918 [ #H113 #H114 #H115 #H116 #H117 #H118 destruct ]
919 #H120 #H121 #H122 #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 destruct cases Hcost
920]
921#st1 #st2 #st3 #l #prf #tl #IH #t2 * #s_em * #t_pre inversion t_pre in ⊢ ?;
922[ #st #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em
923  * #ex_em ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
924  #Hcall #Hcost #sil_t2 %{st} %{(t_base …)} %{s_post} %{tl} % [ /2 by silent_append_l1/]
925  %{l_em} %{ex_em} /4 by refl, conj/
926| #s #s' #s'' #l' #prf' #tl' #_ #EQ1 #EQ2 #EQ3 destruct * #s_post * #t_post * #sil_tpost * #l_em * #ex_em
927  ** #EQ normalize in EQ; lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hcall #Hcost #H
928  change with ((t_ind ??????? (t_base …)) @ tl) in ⊢ (?????%); @measurable_suffix_append @(IH t2) //
929  %{s''} %{tl'} %{s_post} %{t_post} %{sil_tpost} %{l_em} %{ex_em} % // % assumption
930]
931qed.
932
933lemma measurable_suffix_append_case : ∀p.∀S : abstract_status p.
934∀s1,s2,s3 : S. ∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s2 s3.
935measurable_suffix … (t1 @ t2) → (measurable_suffix … t1 ∧ silent_trace … t2) ∨ measurable_suffix … t2.
936#p #S #s1 #s2 #s3 #t1 elim t1 -s1 -s2
937[ #st #t2 #H %2 assumption]
938#st1 #st2 #st3 #l #prf #tl #IH #t2 whd in match (append_on_trace ??????); #Hsuff
939cases(measurable_suffix_tind … Hsuff)
940[ * #_ #H %% [2: /2 by silent_append_l2/]  change with ((t_ind ??????? tl) @ t2) in Hsuff : (?????%);
941 @(measurable_suffix_append_l1 … Hsuff) /2/
942| #H cases(IH … H)
943  [ * #H1 #H2 %% // change with ((t_ind ??????? (t_base …)) @ tl) in ⊢ (?????%); @measurable_suffix_append //
944  | /2/
945  ]
946]
947qed.
948
949lemma measurable_is_measurable_suffix : ∀p.∀S : abstract_status p.
950∀si,s1,s3,sn : S. ∀t : raw_trace … si sn.measurable …s1 s3 … t → measurable_suffix … t.
951#p #S #si #s1 #s3 #sn #t * #s0 * #s2 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 ******* #_
952#EQ destruct /11 width=20 by conj,ex_intro/
953qed.
954
955lemma prefix_of_measurable_suffix_is_premeasurable : ∀p.∀S : abstract_status p.
956∀s1,s2,s3,s4 :S.∀l.∀prf : as_execute … l s2 s3.
957∀t1 : raw_trace … s1 s2.∀t2 : raw_trace … s3 s4.∀t : raw_trace … s1 s4.
958pre_measurable_trace … t → t = (t1 @ (t_ind … prf t2)) → is_costlabelled_act … l →
959silent_trace … t2 → (is_call_act … l → bool_to_Prop(is_call_post_label … s2)) →
960pre_measurable_trace … t1.
961#p #S #s1 #s2 #s3 #s4 #l #prf #t1 #t2 #t #H lapply t1 -t1 lapply t2 -t2 lapply prf -prf lapply s2 -s2
962lapply s3 -s3 elim H -t -s1 -s4
963[ #st #_ #s1 #s2 #prf #r #p inversion p in ⊢ ?;
964  [ #H1 #H2 #H3 #H4 destruct #H5 #H6 #H7 normalize in H5; lapply(eq_to_jmeq ??? H5) -H5 #H5 destruct
965  | #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 destruct
966    normalize in H19; lapply(eq_to_jmeq ??? H19) -H19 #H19 destruct
967  ]
968| #st1 #st2 #st3 #lbl #prf #tl #Hclass **
969  [ #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?;
970    [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
971      destruct *
972    | #s3 #s4 #s5 #lab #exe #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?);
973      #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/
974    ]
975  | #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1 #t1 #t2 inversion t2 in ⊢ ?;
976    [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
977      destruct #_ #_ #_ % //
978    | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
979      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %2 /2/ @(IH … (refl …)) /2/
980   ]
981 ]
982| #st1 #st2 #st3 #lbl #Hclass #prf #tl * #lab #EQ destruct #pre_tl #IH #s1 #s2 #prf1
983  #t1 #t2 inversion t2 in ⊢ ?;
984  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
985    destruct #_ #_ #_ % //
986  | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
987      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %3 /2/ @(IH … (refl …)) /2/
988  ]
989| #st1 #st2 #st3 #lbl #prf #tl #Hclass * #f * #c #EQ destruct #call_post #pre_tl #IH #s1 #s2 #prf1
990  #t1 #t2 inversion t2 in ⊢ ?;
991  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
992    destruct #_ #_ #_ % //
993  | #s3 #s4 #s5 #lbl #prf2 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
994      lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t1 #H1 %4 /3/ @(IH … (refl …)) /2/
995  ]
996| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #prf1 #t1 #t2 #prf2 #Hst1 #Hst3 * #f * #c #EQ destruct
997  #Hcall #pre_t1 #pre_t2 #succ whd in ⊢ (% → ?); #EQ destruct #IH1 #IH2 #s1 #s2 #prf3
998  #t3 #t4 inversion t4 in ⊢ ?;
999  [ #st #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
1000    destruct #_ #_ #_ % //
1001  | #s3 #s4 #s5 #lbl #prf4 #tail #_ #EQ1 #EQ2 #EQ3 destruct normalize in ⊢ (% → ?); #EQ
1002    lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct #Hl #sil_t3 #H1
1003    cut(measurable_suffix … (t1@(t_ind … prf2 t2)))
1004    [ whd %{s5} %{tail} %{s1} %{t3} %{sil_t3} %{l} %{prf3} /4 by jmeq_to_eq, conj/]
1005    #Hmeas cases(measurable_suffix_append_case … Hmeas)
1006    [ * #_ * [2: * #H cases(H I)] #H inversion H in ⊢ ?;
1007      [ #H4 #H5 #H6 #H7 #H8 #H9 destruct
1008      | #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct
1009      ]
1010    | -Hmeas #Hmeas cases(measurable_suffix_tind … Hmeas)
1011      [ **] -Hmeas -IH1 -EQ * #s_em * #t_pre * #s_post * #t_post * #sil_tpost
1012      * #l_em * #ex_em ** #EQ destruct #H1 #H2
1013      change with (t_ind … (t_base …) @ ?) in match (t_ind ????????) in e0;
1014      <append_associative in e0; <append_associative #e0
1015      cases(silent_suffix_cancellable … e0) // -e0 * #EQ1 #EQ2 #EQ3 destruct
1016      >append_associative %5 /2/ [ %{f} %{c} //] normalize
1017      @(IH2 … (refl …)) /2/
1018     ]
1019   ]
1020 ]
1021qed.
1022
1023(*
1024
1025lemma measurable_suffix_is_measurable:
1026∀S : abstract_status.
1027∀s1,s4 : S.
1028∀t : raw_trace … s1 s4.
1029pre_measurable_trace … t →
10302 ≤ |get_costlabels_of_trace … t | →
1031measurable_suffix … t → ∃s1,s3.
1032measurable … s1 … s3 … t.
1033#S #s1 #s4 #t #pre_meas_t #Hlab * #s_em * #t_pre * #s_init * #t_post * #sil_tpost
1034* #l_em * #ex_em ** #EQ destruct #Hcall #Hcost_lem
1035>get_cost_label_append in Hlab; >append_length >get_costlabelled_is_costlabelled //
1036>(get_cost_label_silent_is_empty … sil_tpost) #CARD
1037cases(measurable_prefix_of_premeasurable … t_pre)
1038[3: cases(get_costlabels_of_trace ????) in CARD; [ /3/ | #c #xc #_ % #EQ destruct]
1039|2: @(prefix_of_measurable_suffix_is_premeasurable … pre_meas_t) [5: %|*:] assumption
1040| #s_prefix * #s_post_pre * #t_prefix * #lab * #exe1 * #t34 ** #sil_tprefix #EQ destruct #cost_lab
1041  /20 width=20 by conj,ex_intro/
1042]
1043qed.*)
Note: See TracBrowser for help on using the repository browser.