source: src/common/StructuredTraces.ma @ 2702

Last change on this file since 2702 was 2553, checked in by tranquil, 8 years ago

as_classify changed to a partial function
added a status for tailcalls

File size: 37.8 KB
Line 
1include "basics/types.ma".
2include "basics/bool.ma".
3include "basics/jmeq.ma".
4include "common/CostLabel.ma".
5include "utilities/option.ma".
6include "basics/lists/listb.ma".
7include "ASM/Util.ma".
8
9inductive status_class: Type[0] ≝
10  | cl_return: status_class
11  | cl_jump: status_class
12  | cl_call: status_class
13  | cl_tailcall: status_class
14  | cl_other: status_class.
15
16record abstract_status : Type[1] ≝
17  { as_status :> Type[0]
18  ; as_execute : as_status → as_status → Prop
19  ; as_pc : DeqSet
20  ; as_pc_of : as_status → as_pc
21  ; as_classify : as_status → option status_class
22  ; as_label_of_pc : as_pc → option costlabel
23  ; as_after_return : (Σs:as_status. as_classify s = Some ? cl_call) → as_status → Prop
24  ; as_final: as_status → Prop
25  ; as_call_ident : (Σs:as_status.as_classify s = Some ? cl_call) → ident
26  ; as_tailcall_ident : (Σs:as_status.as_classify s = Some ? cl_tailcall) → ident
27  }.
28
29definition as_classifier ≝ λS,s,cl.as_classify S s = Some ? cl.
30definition as_call ≝ λS,s,f.as_call_ident S s = f.
31
32definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc ? (as_pc_of ? s).
33
34(* temporary alias for backward compatibility *)
35(* definition final_abstract_status ≝ abstract_status. *)
36
37definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
38  λa_s,st.as_label ? st ≠ None ?.
39
40definition as_label_safe : ∀a_s : abstract_status.
41  (Σs : a_s.as_costed ? s) → costlabel ≝
42  λa_s,st_sig.opt_safe … (pi2 … st_sig).
43
44lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) + (¬as_costed S s).
45#S #s whd in match (as_costed S s);
46cases (as_label S s) [ %2 % * /2/ | #c %1 % #E destruct ]
47qed.
48
49lemma not_costed_no_label : ∀S,st.
50  ¬as_costed S st →
51  as_label S st = None ?.
52#S #st * normalize cases (as_label_of_pc S ?)
53[ // | #l #H cases (H ?) % #E destruct ]
54qed.
55
56(* cost map generalities *)
57
58definition as_cost_labelled_at ≝
59  λS : abstract_status. λl.λpc.as_label_of_pc S pc = Some ? l.
60
61definition as_cost_labelled ≝
62  λS : abstract_status. λl.∃pc.as_cost_labelled_at S l pc.
63
64definition as_cost_label ≝
65  λS : abstract_status. Σl.as_cost_labelled S l.
66
67definition as_cost_labels ≝
68  λS : abstract_status. list (as_cost_label S).
69
70definition as_cost_get_label ≝
71  λS : abstract_status. λl_sig: as_cost_label S. pi1 … l_sig.
72
73definition as_cost_get_labels ≝
74  λS : abstract_status. map … (as_cost_get_label S).
75
76definition as_cost_map ≝
77  λS : abstract_status. (as_cost_label S) → ℕ.
78 
79definition lift_sigma_map_id :
80  ∀A,B : Type[0].∀P_in,P_out : A → Prop.B →
81    (∀a.P_out a + ¬ P_out a) →
82  ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig.
83   match dec a_sig with
84   [ inl prf ⇒ m «a_sig, prf»
85   | inr _ ⇒ dflt (* labels not present in out code get 0 *)
86   ].
87
88lemma lift_sigma_map_id_eq :
89  ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out.
90  pi1 ?? a_in = pi1 ?? a_out →
91  lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out.
92#A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ
93whd in match lift_sigma_map_id; normalize nodelta
94cases (dec a_in) normalize nodelta >EQ cases a_out
95#a #H #G [ % | @⊥ /2 by absurd/ ]
96qed.
97
98notation > "Σ_{ ident i ∈ l } f"
99  with precedence 20
100  for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}.
101notation < "Σ_{ ident i ∈ l } f"
102  with precedence 20
103for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}.
104
105definition lift_cost_map_id :
106  ∀S_in,S_out : abstract_status.? →
107  as_cost_map S_out → as_cost_map S_in
108  ≝
109 λS_in,S_out : abstract_status.
110  lift_sigma_map_id costlabel ℕ
111    (*λl.∃pc.as_label_of_pc S_in pc = Some ? l*) (as_cost_labelled S_in)
112    (*λl.∃pc.as_label_of_pc S_out pc = Some ? l*) (as_cost_labelled S_out)
113    0.
114
115lemma lift_cost_map_same_cost :
116  ∀S_in, S_out, dec, m_out, trace_in, trace_out.
117  map … (pi1 ??) trace_in = map … (pi1 ??) trace_out →
118  (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) =
119  (Σ_{ l_sig ∈ trace_out } (m_out l_sig)).
120#S_in #S_out #dec #m_out #trace_in elim trace_in
121[2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out]
122normalize in ⊢ (%→?);
123[2,3: #ABS destruct(ABS)
124|4: #_ %
125|1:
126  #EQ destruct
127  whd in ⊢(??%%);
128  whd in match lift_cost_map_id; normalize nodelta
129  >(lift_sigma_map_id_eq ????????? e0)
130  >e0 in e1; normalize in ⊢(%→?); #EQ
131  >(IH … EQ) %
132]
133qed.
134
135
136(* structured traces: down to business *)
137
138inductive trace_ends_with_ret: Type[0] ≝
139  | ends_with_ret: trace_ends_with_ret
140  | doesnt_end_with_ret: trace_ends_with_ret.
141
142inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
143  | tlr_base:
144      ∀status_before: S.
145      ∀status_after: S.
146        trace_label_label S ends_with_ret status_before status_after →
147        trace_label_return S status_before status_after
148  | tlr_step:
149      ∀status_initial: S.
150      ∀status_labelled: S.
151      ∀status_final: S.
152        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
153        trace_label_return S status_labelled status_final →
154          trace_label_return S status_initial status_final
155with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
156  | tll_base:
157      ∀ends_flag: trace_ends_with_ret.
158      ∀start_status: S.
159      ∀end_status: S.
160        trace_any_label S ends_flag start_status end_status →
161        as_costed S start_status →
162          trace_label_label S ends_flag start_status end_status
163with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
164  (* Single steps within a function which reach a label.
165     Note that this is the only case applicable for a jump. *)
166  | tal_base_not_return:
167      ∀start_status: S.
168      ∀final_status: S.
169        as_execute S start_status final_status →
170        (as_classifier S start_status cl_jump ∨
171         as_classifier S start_status cl_other) →
172        as_costed S final_status →
173          trace_any_label S doesnt_end_with_ret start_status final_status
174  | tal_base_return:
175      ∀start_status: S.
176      ∀final_status: S.
177        as_execute S start_status final_status →
178        as_classifier S start_status cl_return →
179          trace_any_label S ends_with_ret start_status final_status
180  (* A call followed by a label on return. *)
181  | tal_base_call:
182      ∀status_pre_fun_call: S.
183      ∀status_start_fun_call: S.
184      ∀status_final: S.
185        as_execute S status_pre_fun_call status_start_fun_call →
186        ∀H:as_classifier S status_pre_fun_call cl_call.
187          as_after_return S «status_pre_fun_call, H» status_final →
188          trace_label_return S status_start_fun_call status_final →
189          as_costed S status_final →
190            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
191  (* A tailcall, which ends the trace like a return. *)
192  | tal_base_tailcall:
193      ∀status_pre_fun_call: S.
194      ∀status_start_fun_call: S.
195      ∀status_final: S.
196        as_execute S status_pre_fun_call status_start_fun_call →
197        as_classifier S status_pre_fun_call cl_tailcall →
198          trace_label_return S status_start_fun_call status_final →
199            trace_any_label S ends_with_ret status_pre_fun_call status_final
200  (* A call followed by a non-empty trace. *)
201  | tal_step_call:
202      ∀end_flag: trace_ends_with_ret.
203      ∀status_pre_fun_call: S.
204      ∀status_start_fun_call: S.
205      ∀status_after_fun_call: S.
206      ∀status_final: S.
207        as_execute S status_pre_fun_call status_start_fun_call →
208        ∀H:as_classifier S status_pre_fun_call cl_call.
209          as_after_return S «status_pre_fun_call, H» status_after_fun_call →
210          trace_label_return S status_start_fun_call status_after_fun_call →
211          ¬ as_costed S status_after_fun_call →
212          trace_any_label S end_flag status_after_fun_call status_final →
213            trace_any_label S end_flag status_pre_fun_call status_final
214  | tal_step_default:
215      ∀end_flag: trace_ends_with_ret.
216      ∀status_pre: S.
217      ∀status_init: S.
218      ∀status_end: S.
219        as_execute S status_pre status_init →
220        trace_any_label S end_flag status_init status_end →
221        as_classifier S status_pre cl_other →
222        ¬ (as_costed S status_init) →
223          trace_any_label S end_flag status_pre status_end.
224
225let rec tal_pc_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2)
226  on tal : list (as_pc S) ≝
227 match tal with
228 [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl
229 | tal_step_default fl' pre st1' st2' _ tl _ _ ⇒  as_pc_of … pre :: tal_pc_list … tl
230 | tal_base_not_return pre _ _ _ _ ⇒ [as_pc_of … pre]
231 | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre]
232 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
233 | tal_base_tailcall pre _ _ _ _ _ ⇒ [as_pc_of … pre]
234 ].
235
236definition as_trace_any_label_length':
237    ∀S: abstract_status.
238    ∀trace_ends_flag: trace_ends_with_ret.
239    ∀start_status: S.
240    ∀final_status: S.
241    ∀the_trace: trace_any_label S trace_ends_flag start_status final_status.
242      nat ≝
243  λS: abstract_status.
244  λtrace_ends_flag: trace_ends_with_ret.
245  λstart_status: S.
246  λfinal_status: S.
247  λthe_trace: trace_any_label S trace_ends_flag start_status final_status.
248    |tal_pc_list … the_trace|.
249
250let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
251  match tlr with
252  [ tlr_base st1 st2 tll ⇒ tll_unrepeating … tll
253  | tlr_step st1 st2 st3 tll tl ⇒ tll_unrepeating … tll ∧ tlr_unrepeating … tl
254  ]
255and tll_unrepeating S fl st1 st2 (tll : trace_label_label S fl st1 st2) on tll : Prop ≝
256  match tll with
257  [ tll_base fl st1 st2 tal _ ⇒ tal_unrepeating … tal
258  ]
259and tal_unrepeating S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : Prop ≝
260  match tal with
261  [ tal_step_call fl st1 st2 st3 st4 _ _ _ tlr _ tl ⇒
262    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
263    tal_unrepeating … tl ∧
264    tlr_unrepeating … tlr
265  | tal_step_default fl st1 st2 st3 _ tl _ _ ⇒
266    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
267    tal_unrepeating … tl
268  | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
269  | tal_base_tailcall pre _ _ _ _ trace ⇒ tlr_unrepeating … trace
270  | _ ⇒ True
271  ].
272
273definition tll_hd_label : ∀S : abstract_status.∀fl,st1,st2.
274  trace_label_label S fl st1 st2 → costlabel ≝
275  λS,fl,st1,st2,tr.match tr with
276  [ tll_base _ st1' _ _ prf ⇒ as_label_safe … «st1', prf» ].
277
278definition tlr_hd_label : ∀S : abstract_status.∀st1,st2.
279  trace_label_return S st1 st2 → costlabel ≝
280  λS,st1,st2,tr.match tr with
281  [ tlr_base st1' st2' tll ⇒ tll_hd_label … tll
282  | tlr_step st1' st2' _ tll _ ⇒ tll_hd_label … tll
283  ].
284
285let rec tal_unrepeating_uniqueb S fl st1 st2 tal on tal :
286  tal_unrepeating S fl st1 st2 tal → bool_to_Prop (uniqueb … (tal_pc_list … tal)) ≝ ?.
287cases tal //
288#fl' #st1' [#st_fun] #st2' #st3' #H
289[ #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
290#A #B [#_] >A normalize nodelta @tal_unrepeating_uniqueb assumption
291qed.
292
293lemma tal_pc_list_start : ∀S,fl,s1,s2. ∀tal: trace_any_label S fl s1 s2.
294  ∃tl. tal_pc_list … tal = (as_pc_of S s1)::tl.
295#S #fl0 #s10 #s20 *
296[ #s1 #s2 #EX #CL #CS
297| #s1 #s2 #EX #CL
298| #s1 #s2 #s3 #EX #CL #AF #tlr #CS
299| #s1 #s2 #s3 #EX #CL #tlr
300| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal
301| #fl #s1 #s2 #s3 #EX #tal #CL #CS
302] whd in ⊢ (??(λ_.??%?)); % [2,4,6,8,10,12: % | *: skip ]
303qed.
304
305let rec tal_tail_not_costed S fl st1 st2 tal
306  (H:Not (as_costed S st1)) on tal :
307  All ? (λpc. as_label_of_pc S pc = None ?) (tal_pc_list S fl st1 st2 tal) ≝ ?.
308cases tal in H ⊢ %;
309[ #start #final #EX #CL #CS #CS' % // @(not_costed_no_label ?? CS')
310| #start #final #EX #CL #CS % // @(not_costed_no_label ?? CS)
311| #pre #start #final #EX #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS')
312| #pre #start #final #EX #CL #tlr #CS' % // @(not_costed_no_label ?? CS')
313| #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal' #CS'
314  cases (tal_pc_list_start … tal')
315  #hd #E >E
316  % [ @(not_costed_no_label ?? CS') | @tal_tail_not_costed assumption ]
317| #fl' #pre #init #end #EX #tal' #CL #CS #CS'
318  cases (tal_pc_list_start … tal')
319  #hd #E >E
320  % [ @(not_costed_no_label ?? CS') | @tal_tail_not_costed assumption ]
321] qed.
322
323
324inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
325  | tac_base:
326      ∀status: S.
327        as_classifier S status cl_call ∨ as_classifier S status cl_tailcall →
328          trace_any_call S status status
329  | tac_step_call:
330      ∀status_pre_fun_call: S.
331      ∀status_after_fun_call: S.
332      ∀status_final: S.
333      ∀status_start_fun_call: S.
334        as_execute S status_pre_fun_call status_start_fun_call →
335        ∀H:as_classifier S status_pre_fun_call cl_call.
336          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
337          trace_label_return S status_start_fun_call status_after_fun_call →
338          ¬ as_costed S status_after_fun_call →
339          trace_any_call S status_after_fun_call status_final →
340            trace_any_call S status_pre_fun_call status_final
341  | tac_step_default:
342      ∀status_pre: S.
343      ∀status_end: S.
344      ∀status_init: S.
345        as_execute S status_pre status_init →
346        trace_any_call S status_init status_end →
347        as_classifier S status_pre cl_other →
348        ¬ (as_costed S status_init) →
349          trace_any_call S status_pre status_end.
350
351             
352inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝
353  | tlc_base:
354      ∀start_status: S.
355      ∀end_status: S.
356        trace_any_call S start_status end_status →
357        as_costed S start_status →
358        trace_label_call S start_status end_status
359.
360
361definition tlc_hd_label : ∀S : abstract_status.∀st1,st2.
362  trace_label_call S st1 st2 → costlabel ≝
363  λS,st1,st2,tr.match tr with
364  [ tlc_base st1' _ _ prf ⇒ as_label_safe … «st1', prf»
365  ].
366   
367coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
368  | tld_step:
369      ∀status_initial: S.
370      ∀status_labelled: S.
371          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
372          trace_label_diverges S status_labelled →
373            trace_label_diverges S status_initial
374  | tld_base:
375      ∀status_initial: S.
376      ∀status_pre_fun_call: S.
377      ∀status_start_fun_call: S.
378        trace_label_call S status_initial status_pre_fun_call →
379        as_execute S status_pre_fun_call status_start_fun_call →
380        ∀H:as_classifier S status_pre_fun_call cl_call.
381          trace_label_diverges S status_start_fun_call →
382            trace_label_diverges S status_initial.
383
384definition tld_hd_label : ∀S : abstract_status.∀st.
385  trace_label_diverges S st → costlabel ≝
386  λS,st,tr.match tr with
387  [ tld_step st' st'' tll _ ⇒ tll_hd_label … tll
388  | tld_base st' st'' _ tlc _ _ _ ⇒ tlc_hd_label … tlc
389  ].       
390
391(* Version in Prop for showing existence. *)
392coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
393  | tld_step':
394      ∀status_initial: S.
395      ∀status_labelled: S.
396          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
397          trace_label_diverges_exists S status_labelled →
398            trace_label_diverges_exists S status_initial
399  | tld_base':
400      ∀status_initial: S.
401      ∀status_pre_fun_call: S.
402      ∀status_start_fun_call: S.
403        trace_label_call S status_initial status_pre_fun_call →
404        as_execute S status_pre_fun_call status_start_fun_call →
405        ∀H:as_classifier S status_pre_fun_call cl_call.
406          trace_label_diverges_exists S status_start_fun_call →
407            trace_label_diverges_exists S status_initial.
408
409inductive trace_whole_program (S: abstract_status) : S → Type[0] ≝
410  | twp_terminating:
411      ∀status_initial: S.
412      ∀status_start_fun: S.
413      ∀status_final: S.
414        as_classifier S status_initial cl_call →
415        as_execute S status_initial status_start_fun →
416        trace_label_return S status_start_fun status_final →
417        as_final S status_final →
418        trace_whole_program S status_initial
419  | twp_diverges:
420      ∀status_initial: S.
421      ∀status_start_fun: S.
422        as_classifier S status_initial cl_call →
423        as_execute S status_initial status_start_fun →
424        trace_label_diverges S status_start_fun →
425        trace_whole_program S status_initial.
426
427(* Again, an identical version in Prop for existence proofs. *)
428inductive trace_whole_program_exists (S: abstract_status) : S → Prop ≝
429  | twp_terminating:
430      ∀status_initial: S.
431      ∀status_start_fun: S.
432      ∀status_final: S.
433        as_classifier S status_initial cl_call →
434        as_execute S status_initial status_start_fun →
435        trace_label_return S status_start_fun status_final →
436        as_final S status_final →
437        trace_whole_program_exists S status_initial
438  | twp_diverges:
439      ∀status_initial: S.
440      ∀status_start_fun: S.
441        as_classifier S status_initial cl_call →
442        as_execute S status_initial status_start_fun →
443        trace_label_diverges_exists S status_start_fun →
444        trace_whole_program_exists S status_initial.
445
446
447let rec trace_any_label_label S s s' f
448  (tr:trace_any_label S f s s') on tr : match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] ≝
449match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with
450[ tal_base_not_return start final _ _ C ⇒ C
451| tal_base_return _ _  _ _ ⇒ I
452| tal_base_call _ _ _ _ _ _ _ C ⇒ C
453| tal_base_tailcall _ _ _ _ _ _ ⇒ I
454| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
455| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
456].
457
458definition tal_tl_label : ∀S : abstract_status.∀st1,st2.
459  trace_any_label S doesnt_end_with_ret st1 st2 → costlabel ≝
460  λS,st1,st2,tr.as_label_safe … «st2, trace_any_label_label … tr».
461
462lemma trace_label_label_label : ∀S,s,s',f.
463  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
464#S #s #s' #f #tr
465cases tr
466#f #start #end #tr' #C @(trace_any_label_label … tr')
467qed.
468
469definition tll_tl_label : ∀S : abstract_status.∀st1,st2.
470  trace_label_label S doesnt_end_with_ret st1 st2 → costlabel ≝
471  λS,st1,st2,tr.as_label_safe … «st2, trace_label_label_label … tr».
472
473lemma trace_any_call_call : ∀S,s,s'.
474  trace_any_call S s s' → as_classifier S s' cl_call ∨ as_classifier S s' cl_tailcall.
475#S #s #s' #T elim T [1,3: //]
476#H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 //
477qed.
478
479(*
480(* an trace of unlabeled and cl_other states, possibly empty *)
481inductive trace_no_label_any (S:abstract_status) : S → S → Type[0] ≝
482  | tna_base :
483      ∀start_status: S.
484      ¬as_costed … start_status →
485      trace_no_label_any S start_status start_status
486  | tna_step :
487      ∀status_pre: S.
488      ∀status_init: S.
489      ∀status_end: S.
490        as_execute S status_pre status_init →
491        as_classifier S status_pre cl_other →
492        ¬as_costed … status_pre →
493        trace_no_label_any S status_init status_end →
494          trace_no_label_any S status_pre status_end.
495
496let rec tna_append_tna S st1 st2 st3 (taa1 : trace_no_label_any S st1 st2)
497  on taa1 :
498    trace_no_label_any S st2 st3 →
499    trace_no_label_any S st1 st3 ≝
500  match taa1 with
501  [ tna_base st1' H ⇒ λtaa2.taa2
502  | tna_step st1' st2' st3' H G K tl ⇒
503    λtaa2.tna_step ???? H G K (tna_append_tna … tl taa2)
504  ].
505
506definition tna_non_empty ≝ λS,st1,st2.λtna : trace_no_label_any S st1 st2.
507  match tna with
508  [ tna_base _ _ ⇒ false
509  | tna_step _ _ _ _ _ _ _ ⇒ true
510  ].
511
512coercion tna_to_bool : ∀S,st1,st2.∀tna:trace_no_label_any S st1 st2.bool ≝
513 tna_non_empty on _tna : trace_no_label_any ??? to bool.
514
515lemma tna_unlabelled : ∀S,st1,st2.trace_no_label_any S st1 st2 → ¬as_costed … st1.
516#S #st1 #st2 * [#st #H @H | #st #st' #st'' #_ #_ #H #_ @H] qed.
517
518let rec tna_append_tal S st1 fl st2 st3 (tna : trace_no_label_any S st1 st2)
519  on tna :
520  trace_any_label S fl st2 st3 →
521  if tna then Not (as_costed … st2) else True →
522  trace_any_label S fl st1 st3 ≝
523  match tna return λst1,st2.λx : trace_no_label_any S st1 st2.
524    ∀fl,st3.
525    trace_any_label S fl st2 st3 →
526    if x then Not (as_costed … st2) else True →
527    trace_any_label S fl st1 st3
528  with
529  [ tna_base st1' H ⇒ λfl,st3,taa2,prf.taa2
530  | tna_step st1' st2' st3' H G K tl ⇒ λfl,st3,taa2,prf.
531    tal_step_default ????? H (tna_append_tal ????? tl taa2 ?) G (tna_unlabelled … tl)
532  ] fl st3.
533  cases (tna_non_empty … tl) [@prf|%]
534  qed.
535*)
536
537inductive trace_any_any (S : abstract_status) : S → S → Type[0] ≝
538  | taa_base : ∀st.trace_any_any S st st
539  | taa_step : ∀st1,st2,st3.
540    as_execute S st1 st2 →
541    as_classifier S st1 cl_other →
542    ¬as_costed S st2 →
543    trace_any_any S st2 st3 →
544    trace_any_any S st1 st3.
545
546definition taa_non_empty ≝ λS,st1,st2.λtaa : trace_any_any S st1 st2.
547  match taa with
548  [ taa_base _ ⇒ false
549  | taa_step _ _ _ _ _ _ _ ⇒ true
550  ].
551
552coercion taa_to_bool : ∀S,st1,st2.∀taa:trace_any_any S st1 st2.bool ≝
553 taa_non_empty on _taa : trace_any_any ??? to bool.
554
555let rec taa_append_tal S st1 fl st2 st3
556  (taa : trace_any_any S st1 st2) on taa :
557  trace_any_label S fl st2 st3 →
558  trace_any_label S fl st1 st3 ≝
559  match taa return λst1,st2.λx : trace_any_any S st1 st2.
560    ∀fl,st3.
561    trace_any_label S fl st2 st3 →
562    trace_any_label S fl st1 st3
563  with
564  [ taa_base st1' ⇒ λfl,st3,tal2.tal2
565  | taa_step st1' st2' st3' H G K tl ⇒ λfl,st3,tal2.
566    tal_step_default ????? H (taa_append_tal ????? tl tal2) G K
567  ] fl st3.
568
569interpretation "trace any any label append" 'append taa tal = (taa_append_tal ????? taa tal).
570
571let rec tal_collapsable S fl s1 s2 (tal : trace_any_label S fl s1 s2) on tal : Prop ≝
572match tal with
573[ tal_base_not_return _ _ _ _ _ ⇒ True
574| tal_step_default fl1 _ st1' st1'' _ tl1 _ _ ⇒ tal_collapsable … tl1
575| _ ⇒ False
576].
577
578let rec tlr_rel S1 st1 st1' S2 st2 st2'
579  (tlr1 : trace_label_return S1 st1 st1')
580  (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
581match tlr1 with
582  [ tlr_base st1 st1' tll1 ⇒
583    match tlr2 with
584    [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
585    | _ ⇒ False
586    ]
587  | tlr_step st1 st1' st1'' tll1 tl1 ⇒
588    match tlr2 with
589    [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
590      tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
591    | _ ⇒ False
592    ]
593  ]
594and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
595 (tll1 : trace_label_label S1 fl1 st1 st1')
596 (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
597  match tll1 with
598  [ tll_base fl1 st1 st1' tal1 H ⇒
599    match tll2 with
600    [ tll_base fl2 st2 st2 tal2 G ⇒
601      as_label_safe … («?, H») = as_label_safe … («?, G») ∧
602      tal_rel … tal1 tal2
603    ]
604  ]
605and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
606 (tal1 : trace_any_label S1 fl1 st1 st1')
607 (tal2 : trace_any_label S2 fl2 st2 st2')
608   on tal1 : Prop ≝
609  match tal1 with
610  [ tal_base_not_return st1 st1' _ _ _ ⇒
611    fl2 = doesnt_end_with_ret ∧
612    ∃st2mid,taa,H,G,K.
613    tal2 ≃ taa_append_tal ? st2 ??? taa
614      (tal_base_not_return ? st2mid st2' H G K)
615  | tal_base_return st1 st1' _ _ ⇒
616    fl2 = ends_with_ret ∧
617    ∃st2mid,taa,H,G.
618    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
619      (tal_base_return ? st2mid st2' H G)
620  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒
621    fl2 = doesnt_end_with_ret ∧
622    ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
623    ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
624    (* we must allow a tal_base_call to be similar to a call followed
625      by a collapsable trace (trace_any_any followed by a base_not_return;
626      we cannot use trace_any_any as it disallows labels in the end as soon
627      as it is non-empty) *)
628    (∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
629      tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨
630    ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
631    ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'.
632      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
633      tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
634  | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒
635    fl2 = ends_with_ret ∧
636    ∃st2mid,G.as_tailcall_ident S2 («st2mid, G») = as_tailcall_ident ? «st1, prf» ∧
637    ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
638    ∃tlr2 : trace_label_return ? st2mid' st2'.
639      tal2 ≃ taa @ (tal_base_tailcall … H G tlr2) ∧ tlr_rel … tlr1 tlr2
640  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒
641    ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
642    ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
643    (fl2 = doesnt_end_with_ret ∧ ∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
644      tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧
645      tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨
646    ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
647    ∃tl2 : trace_any_label ? fl2 st2mid'' st2'.
648      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
649      tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2
650  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
651    tal_rel … tl1 tal2 (* <- this makes it many to many *)
652  ].
653
654interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2).
655interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2).
656interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ?????? t1 t2).
657
658let rec tal_collapsable_eq_fl S1 fl1 s1 s1'
659  (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 :
660  tal_collapsable … tal1 → fl1 = doesnt_end_with_ret ≝
661match tal1 return λfl1,s1,s1',tal1.
662  tal_collapsable S1 fl1 s1 s1' tal1 → fl1 = doesnt_end_with_ret with
663[ tal_base_not_return _ _ _ _ _ ⇒ λ_.refl …
664| tal_step_default fl1 _ st1' st1'' _ tl1 _ _ ⇒ tal_collapsable_eq_fl … tl1
665| _ ⇒ Ⓧ
666].
667
668let rec tal_rel_eq_fl S1 fl1 s1 s1' S2 fl2 s2 s2'
669  (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 :
670  ∀tal2 : trace_any_label S2 fl2 s2 s2'.tal_rel … tal1 tal2 → fl1 = fl2 ≝
671  match tal1 return λfl1,s1,s1',tal1.? with
672  [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ?
673  | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ?
674  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
675  | tal_base_tailcall st1 st1' st1'' _ _ tlr1 ⇒ let BASE_TC ≝ 0 in ?
676  | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
677  | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ?
678  ].
679-fl1 -s1 -s1'
680[1,2,3,4: -tal_rel_eq_fl #tal2 * //
681| #tal2 * #s2_mid * #G2 * #call * #taa2 * #s2' *#H2 *
682  [ * #EQ1 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) //
683  | * #s2_mid' *#K2 *#tlr2 *#L2 *#tl2 ** #_ #step #_
684     @(tal_rel_eq_fl … step)
685  ]
686| #tal2 whd in ⊢ (%→?); #step @(tal_rel_eq_fl … step)
687]
688qed.
689
690let rec taa_rel_inv S1 fl1 st1 st1mid st1' S2 fl2 st2 st2'
691  (taa1 : trace_any_any S1 st1 st1mid) on taa1 :
692  ∀tal1 : trace_any_label S1 fl1 st1mid st1'.
693  ∀tal2 : trace_any_label S2 fl2 st2 st2'.
694  tal_rel … (taa1 @ tal1) tal2 →
695  tal_rel … tal1 tal2 ≝ ?.
696cases taa1 -taa1
697[ -taa_rel_inv //
698| #st #st' #st'' #H #G #K #tl #tal1 #tal2 whd in ⊢ (%→?);
699  @(taa_rel_inv … tl)
700]
701qed.
702
703lemma taa_append_collapsable : ∀S,s1,fl,s2,s3.
704  ∀taa,tal.tal_collapsable S fl s2 s3 tal → tal_collapsable S fl s1 s3 (taa@tal).
705  #S #s1 #fl #s2 #s3 #taa elim taa -s1 -s2 /2/
706qed.
707
708let rec tal_rel_collapsable S1 fl1 s1 s1' S2 fl2 s2 s2'
709  (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 :
710  ∀tal2 : trace_any_label S2 fl2 s2 s2'.tal_collapsable … tal1 → tal_rel … tal1 tal2 →
711  tal_collapsable … tal2 ≝
712  match tal1 return λfl1,s1,s1',tal1.? with
713  [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ?
714  | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ?
715  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
716  | tal_base_tailcall st1 st1' st1'' _ _ tlr1 ⇒ let BASE_TC ≝ 0 in ?
717  | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
718  | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ?
719  ].
720-fl1 -s1 -s1'
721[1,2,3,4: -tal_rel_collapsable #tal2 * *
722  #EQ * #s2 * #taa2 *#H *#G *#K #EQ' destruct @taa_append_collapsable %
723| #tal2 *
724| #tal2 #tal2 whd in ⊢ (%→?); #step @(tal_rel_collapsable … step) assumption
725]
726qed.
727
728let rec flatten_trace_label_label
729  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
730    (start_status: S) (final_status: S)
731      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
732        on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
733  match the_trace with
734  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
735      let label ≝
736        match as_label … initial return λx: option costlabel. x ≠ None ? → ? with
737        [ None ⇒ λabs. ⊥
738        | Some l ⇒ λ_. l
739        ] labelled_proof
740      in
741        (mk_Sig … label ?)::flatten_trace_any_label S ends_flag initial final given_trace
742  ]
743and flatten_trace_any_label
744  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
745    (start_status: S) (final_status: S)
746      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
747        on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
748  match the_trace with
749  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
750  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
751      flatten_trace_label_return … call_trace
752  | tal_base_tailcall pre_fun_call start_fun_call final _ _ call_trace ⇒
753      flatten_trace_label_return … call_trace
754  | tal_base_return the_status _ _ _ ⇒ [ ]
755  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
756    _ _ _ call_trace _ final_trace ⇒
757    let call_cost_trace ≝ flatten_trace_label_return … call_trace in
758    let final_cost_trace ≝ flatten_trace_any_label … end_flag … final_trace in
759        call_cost_trace @ final_cost_trace
760  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
761      flatten_trace_any_label … tail_trace
762  ]
763and flatten_trace_label_return
764  (S: abstract_status)
765    (start_status: S) (final_status: S)
766      (the_trace: trace_label_return S start_status final_status)
767        on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝
768  match the_trace with
769  [ tlr_base before after trace_to_lift ⇒
770      flatten_trace_label_label … trace_to_lift
771  | tlr_step initial labelled final labelled_trace ret_trace ⇒
772    let labelled_cost ≝ flatten_trace_label_label … doesnt_end_with_ret … labelled_trace in
773    let return_cost ≝ flatten_trace_label_return … ret_trace in
774        labelled_cost @ return_cost
775  ].
776  [2:
777    cases abs -abs #abs @abs %
778  |1:
779    %{(as_pc_of … initial)} whd in match label;
780    change with (as_label ?? = ?)
781    generalize in match labelled_proof; whd in ⊢ (% → ?);
782    cases (as_label S initial)
783    [1:
784      #absurd @⊥ cases absurd -absurd #absurd @absurd %
785    |2:
786      #costlabel normalize nodelta #_ %
787    ]
788  ]
789qed.
790
791(* JHM: base case now passes the termination checker *)
792let rec taa_append_tal_same_flatten
793  S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa :
794  ∀tal : trace_any_label S fl st2 st3.
795    flatten_trace_any_label … (taa @ tal) =
796      flatten_trace_any_label … tal ≝ ?.
797cases taa -st1 -st2
798[ #st #tal normalize in ⊢ (??%?); //
799| #st_pre #st_init #st2 #H #G #K #taa' #tal
800  whd in match (? @ ?);
801  whd in ⊢ (??%?); //
802]
803qed.
804
805let rec tal_collapsable_flatten S fl st1 st2 tal
806  on tal :
807  tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ] ≝
808match tal
809return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ]
810with
811[ tal_base_not_return the_status _ _ _ _ ⇒ λ_.refl ??
812| tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
813    tal_collapsable_flatten ???? tail_trace
814| _ ⇒ Ⓧ
815].
816
817let rec tll_rel_to_traces_same_flatten
818  (S: abstract_status) (S': abstract_status)
819    (trace_ends_flag_l: trace_ends_with_ret) (trace_ends_flag_r: trace_ends_with_ret)
820    (start_status_l: S) (final_status_l: S) (start_status_r: S') (final_status_r: S')
821      (the_trace_l: trace_label_label S trace_ends_flag_l start_status_l final_status_l)
822        (the_trace_r: trace_label_label S' trace_ends_flag_r start_status_r final_status_r)
823          on the_trace_l:
824            tll_rel … the_trace_l the_trace_r →
825              map … (pi1 …) (flatten_trace_label_label … the_trace_l) =
826                map … (pi1 …) (flatten_trace_label_label … the_trace_r) ≝
827  match the_trace_l with
828  [ tll_base fl1 st1 st1' tal1 H ⇒
829    match the_trace_r with
830    [ tll_base fl2 st2 st2 tal2 G ⇒ ?
831    ]
832  ]
833and tal_rel_to_traces_same_flatten
834  (S: abstract_status) (S': abstract_status) (trace_ends_flag_l: trace_ends_with_ret)
835    (trace_ends_flag_r: trace_ends_with_ret)
836      (start_status_l: S) (final_status_l: S) (start_status_r: S') (final_status_r: S')
837        (the_trace_l: trace_any_label S trace_ends_flag_l start_status_l final_status_l)
838          (the_trace_r: trace_any_label S' trace_ends_flag_r start_status_r final_status_r)
839          on the_trace_l:
840            tal_rel … the_trace_l the_trace_r →
841              map … (pi1 …) (flatten_trace_any_label … the_trace_l) =
842                map … (pi1 …) (flatten_trace_any_label … the_trace_r) ≝
843  match the_trace_l with
844  [ tal_base_not_return st1 st1' H G K ⇒ ?
845  | tal_base_return st1 st1' H G ⇒ ?
846  | tal_base_call st1 st1' st1'' H G K tlr1 L ⇒ ?
847  | tal_base_tailcall st1 st1' st1'' H G tlr1 ⇒ ?
848  | tal_step_call fl1 st1 st1' st1'' st1''' H G K tlr1 L tl1 ⇒ ?
849  | tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ?
850  ]
851and tlr_rel_to_traces_same_flatten
852  (S: abstract_status) (S': abstract_status) (start_status_l: S) (final_status_l: S)
853    (start_status_r: S') (final_status_r: S')
854      (the_trace_l: trace_label_return S start_status_l final_status_l)
855        (the_trace_r: trace_label_return S' start_status_r final_status_r)
856        on the_trace_l:
857          tlr_rel … the_trace_l the_trace_r →
858            map … (pi1 …) (flatten_trace_label_return … the_trace_l) =
859              map … (pi1 …) (flatten_trace_label_return … the_trace_r) ≝
860  match the_trace_l with
861  [ tlr_base before after tll_l ⇒ ?
862  | tlr_step initial labelled final tll_l tlr_l ⇒ ?
863  ]. 
864[ * whd in match as_label_safe; normalize nodelta
865  @opt_safe_elim #l1 #EQ1
866  @opt_safe_elim #l2 #EQ2
867  #EQ destruct(EQ) #H_tal
868  change with (? :: ? = ? :: ?) lapply H -H lapply G -G
869  whd in match as_costed; normalize nodelta
870  >EQ1 >EQ2 normalize nodelta #_ #_
871  >(tal_rel_to_traces_same_flatten … H_tal) @refl
872|2,3,4,5,6,7:
873  [1,2,3,4: * #EQ destruct(EQ)]
874  [1,2,3,4,5: * #st_mid [1,2:|*: * #G' * #call ] * #taa
875    [ *#H' *#G' *#K' #EQ
876    | *#H' *#G' #EQ
877    | *#st_mid' *#H' * [|*#st2_mid''] *#K' *#tlr2 *#L'
878      [|*#tl2 *] * #EQ #H_tlr [| #H_tl]
879    | *#st_mid' *#H' *#tlr2 * #EQ #H_tlr
880    | *#st_fun *#H' *
881      [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#K' *#tlr2 *#L'
882      [| *#tl2] ** #EQ #H_tl #H_tlr
883    ] >EQ >taa_append_tal_same_flatten
884  | whd in ⊢ (%→??(????%)?);
885    @tal_rel_to_traces_same_flatten
886  ]
887  [1,2: %
888  |3,5: @(tlr_rel_to_traces_same_flatten … H_tlr)
889  |4,6: <map_append
890    >(tal_collapsable_flatten … H_tl) >append_nil
891    >(tlr_rel_to_traces_same_flatten … H_tlr) %
892  |7: <map_append
893    >(tlr_rel_to_traces_same_flatten … H_tlr)
894    >(tal_rel_to_traces_same_flatten … H_tl)
895    @map_append
896  ]
897|*: cases the_trace_r
898  [1,3: #st_before_r #st_after_r #tll_r
899    [ @tll_rel_to_traces_same_flatten | * ]
900  |*: #st_init_r #st_labld_r #st_fin_r #tll_r #tlr_r *
901    #H_tll #H_tlr
902    <map_append
903    >(tll_rel_to_traces_same_flatten … H_tll)
904    >(tlr_rel_to_traces_same_flatten … H_tlr)
905    @map_append
906  ]
907]
908qed.
909
910(* cost maps specifics: summing over flattened traces *)
911
912lemma lift_cost_map_same_cost_tal :
913  ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out.
914  ∀the_trace_in : trace_any_label S_in f_in start_in end_in.
915  ∀the_trace_out : trace_any_label S_out f_out start_out end_out.
916  tal_rel … the_trace_in the_trace_out →
917  (Σ_{l ∈ flatten_trace_any_label … the_trace_in}
918    (lift_cost_map_id … dec m_out l)) =
919  (Σ_{l ∈ flatten_trace_any_label … the_trace_out} (m_out l)).
920#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
921#tal_in #tal_out #H_tal
922@(lift_cost_map_same_cost … (tal_rel_to_traces_same_flatten … H_tal))
923qed.
924
925lemma lift_cost_map_same_cost_tll :
926  ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out.
927  ∀the_trace_in : trace_label_label S_in f_in start_in end_in.
928  ∀the_trace_out : trace_label_label S_out f_out start_out end_out.
929  tll_rel … the_trace_in the_trace_out →
930  (Σ_{l ∈ flatten_trace_label_label … the_trace_in}
931    (lift_cost_map_id … dec m_out l)) =
932  (Σ_{l ∈ flatten_trace_label_label … the_trace_out} (m_out l)).
933#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
934#tll_in #tll_out #H_tll
935@(lift_cost_map_same_cost … (tll_rel_to_traces_same_flatten … H_tll))
936qed.
937
938lemma lift_cost_map_same_cost_tlr :
939  ∀S_in, S_out, dec, m_out, start_in, start_out, end_in, end_out.
940  ∀the_trace_in : trace_label_return S_in start_in end_in.
941  ∀the_trace_out : trace_label_return S_out start_out end_out.
942  tlr_rel … the_trace_in the_trace_out →
943  (Σ_{l ∈ flatten_trace_label_return … the_trace_in}
944    (lift_cost_map_id … dec m_out l)) =
945  (Σ_{l ∈ flatten_trace_label_return … the_trace_out} (m_out l)).
946#S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out
947#tlr_in #tlr_out #H_tlr
948@(lift_cost_map_same_cost … (tlr_rel_to_traces_same_flatten … H_tlr))
949qed.
Note: See TracBrowser for help on using the repository browser.