source: src/common/StatusSimulation.ma @ 2413

Last change on this file since 2413 was 2413, checked in by tranquil, 7 years ago
  • tal_rel corrected to include cases where tal_base_call \approx tal_step_call
  • status simulation: from local properties to propagation of structured traces
File size: 17.5 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "common/StructuredTraces.ma".
16
17record status_rel
18  (S1 : abstract_status)
19  (S2 : abstract_status)
20  : Type[1] ≝
21  { sem_rel :2> S1 → S2 → Prop
22  (* this is kept separate, as not necessarily carrier will
23     synchronise on calls. It should state the minimal properties
24     necessary for as_after_return (typically just the program counter)
25     maybe what function is called too? *)
26  ; call_rel : (Σs.∃f.as_classifier S1 s (cl_call f)) →
27               (Σs.∃f.as_classifier S2 s (cl_call f)) → Prop
28  ; sim_final :
29    ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2
30  }.
31
32(* if we later genralise, we should move this inside status_rel *)
33definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2.
34
35definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.λs1,s2.
36  ∀s1_pre,s2_pre.as_after_return S1 s1_pre s1 → call_rel … R s1_pre s2_pre →
37                 as_after_return S2 s2_pre s2.
38
39(* the equivalent of a collapsable trace_any_label where we do not forse
40   costedness of the lookahead status *)
41inductive trace_any_any_free (S : abstract_status) : S → S → Type[0] ≝
42| taaf_base : ∀s.trace_any_any_free S s s
43| taaf_step : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
44  as_classifier S s2 cl_other →
45  trace_any_any_free S s1 s3.
46
47definition taaf_non_empty ≝ λS,s1,s2.λtaaf : trace_any_any_free S s1 s2.
48match taaf with
49[ taaf_base _ ⇒ false
50| taaf_step _ _ _ _ _ _ ⇒ true
51].
52
53(* notice: labels and semantic relation between states are not in sync *)
54record status_simulation
55  (S1 : abstract_status)
56  (S2 : abstract_status)
57  : Type[1] ≝
58  { sim_status_rel :> status_rel S1 S2
59  ; sim_execute :
60    ∀st1,st1',c,st2.as_execute S1 st1 st1' →
61    sim_status_rel st1 st2 →
62    ∀prf : as_classifier S1 st1 c. (* <-- watch out, different from status_simulation *)
63    match c return λc.as_classifier S1 st1 c → ? with
64    [ cl_call _ ⇒ λprf.
65      ∃st2_pre_call.call_rel ?? sim_status_rel «st1, ex_intro … prf» st2_pre_call ∧
66      ∃st2_after_call,st2'.
67      ∃taa2 : trace_any_any … st2 st2_pre_call.
68      ∃taa2' : trace_any_any … st2_after_call st2'.
69      as_execute … st2_pre_call st2_after_call ∧
70      sim_status_rel st1' st2' ∧
71      label_rel … st1' st2_after_call
72    | cl_return ⇒ λ_.
73      ∃st2_ret,st2_after_ret,st2'.
74      ∃taa2 : trace_any_any … st2 st2_ret.
75      ∃taa2' : trace_any_any_free … st2_after_ret st2'.
76      (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
77      as_classifier … st2_ret cl_return (* is it really important? *) ∧
78      as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
79      ret_rel … sim_status_rel st1' st2_after_ret ∧
80      label_rel … st1' st2'
81    | _ ⇒ λ_.
82      (* this allows to freely exchange cl_other and cl_jump,
83         but if cl_jump imposed labels before, they will be kept afterwards *)
84      ∃st2'.
85      ∃taa2 : trace_any_any_free … st2 st2'.
86      (* we ensure no labels are collapsed. Technicality? *)
87      (if taaf_non_empty … taa2 then True else ¬as_costed … st1) ∧
88      sim_status_rel st1' st2' ∧
89      label_rel … st1' st2'
90    ] prf
91  }.
92
93let rec taa_append_taa S st1 st2 st3
94  (taa : trace_any_any S st1 st2) on taa :
95  trace_any_any S st2 st3 →
96  trace_any_any S st1 st3 ≝
97  match taa
98  with
99  [ taa_base st1' ⇒ λst3,taa2.taa2
100  | taa_step st1' st2' st3' H I J tl ⇒ λst3,taa2.
101    taa_step ???? H I J (taa_append_taa … tl taa2)
102  ] st3.
103
104lemma associative_taa_append_tal : ∀S,s1,s2,fl,s3,s4.
105  ∀taa1 : trace_any_any S s1 s2.
106  ∀taa2 : trace_any_any S s2 s3.
107  ∀tal : trace_any_label S fl s3 s4.
108  (taa_append_taa … taa1 taa2) @ tal = taa1 @ taa2 @ tal.
109#S #s1 #s2 #fl #s3 #s4 #taa1 elim taa1 -s1 -s2
110[ #s1 #taa2 #tal %
111| #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
112  normalize >IH %
113]
114qed.
115
116lemma associative_taa_append_taa : ∀S,s1,s2,s3,s4.
117  ∀taa1 : trace_any_any S s1 s2.
118  ∀taa2 : trace_any_any S s2 s3.
119  ∀taa3 : trace_any_any S s3 s4.
120  taa_append_taa … (taa_append_taa … taa1 taa2) taa3 =
121  taa_append_taa … taa1 (taa_append_taa … taa2 taa3).
122#S #s1 #s2 #s3 #s4 #taa1 elim taa1 -s1 -s2
123[ #s1 #taa2 #tal %
124| #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
125  normalize >IH %
126]
127qed.
128
129let rec taa_append_tal_rel S1 fl1 st1 st1'
130  (tal1 : trace_any_label S1 fl1 st1 st1')
131  S2 st2 st2mid fl2 st2'
132  (taa2 : trace_any_any S2 st2 st2mid)
133  (tal2 : trace_any_label S2 fl2 st2mid st2')
134  on tal1 :
135  tal_rel … tal1 tal2 →
136  tal_rel … tal1 (taa2 @ tal2) ≝ ?.
137cases tal1 -fl1 -st1 -st1'
138[ #H1 #H2 #H3 #H4 #H5 *#K1 *#K2 *#K3 *#K4 *#K5 *#K6 #EQ
139| #H1 #H2 #H3 #H4 *#K1 *#K2 *#K3 *#K4 *#K5 #EQ
140| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 *#K1 *#K2 *#K3 *#K4 *#K5 *
141  [*#K6 *#K7 *#K8 *#K9 *#K10 * #EQ #EQ'
142  |*#K6 *#K7 *#K8 *#K9 *#K10 *#K11 *#K12 ** #EQ #EQ' #coll
143  ]
144| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12
145  *#K2 *#K3 *#K4 *#K5 *
146  [*#EQ_fl *#K6 *#K7 *#K8 *#K9 *#K10 ** #EQ #coll #EQ'
147  |*#K6 *#K7 *#K8 *#K9 *#K10 *#K11 *#K12 ** #EQ #EQ' #EQ''
148  ]
149| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 whd in ⊢ (%→%); @(taa_append_tal_rel … H6)
150]
151destruct
152<associative_taa_append_tal
153  [1,2,3,4:% try @refl] %{K2} %{(taa_append_taa … taa2 K3)}
154  [1,2,3: % [2,4,6: % [2: % [2:%] |4:% |6: %1 %{K6} %{K7} %{K8} %{K9} %{K10} %{EQ'} % ]]
155  |*: %{K4} %{K5}
156    [1,3: %2 %{K6} %{K7} %{K8} %{K9} %{K10} %{K11} %{K12}
157    | %1 %{(refl …)} %{K6} %{K7} %{K8} %{K9} %{K10}
158    ] /3 by conj/
159  ]
160qed.
161
162let rec tal_end_costed S st1 st2 (tal : trace_any_label S doesnt_end_with_ret st1 st2)
163  on tal : as_costed … st2 ≝
164  match tal return λfl,st1,st2,tal.fl = doesnt_end_with_ret → as_costed ? st2 with
165  [ tal_step_call fl' _ _ st1' st2' _ _ _ _ _ _ tl ⇒ λprf.tal_end_costed ? st1' st2' (tl⌈trace_any_label ????↦?⌉)
166  | tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ λprf.tal_end_costed ? st1'st2' (tl⌈trace_any_label ????↦?⌉)
167  | tal_base_not_return _ st2' _ _ K ⇒ λ_.K
168  | tal_base_return _ _ _ _ ⇒ λprf.⊥
169  | tal_base_call _ _ st2' _ _ _ _ _ K ⇒ λ_.K
170  ] (refl …).
171[ destruct
172|*: >prf %
173]
174qed.
175
176let rec tal_collapsable_to_rel S fl st1 st2
177  (tal : trace_any_label S fl st1 st2) on tal :
178  tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
179  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) ≝
180  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
181  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J)
182  with
183  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_to_rel ???? tl
184  | tal_base_not_return _ st2' _ _ K ⇒ ?
185  | _ ⇒ Ⓧ
186  ].
187* #S2 #st12 #st22 #H #I #J % %[|%{(taa_base ??)} %[|%[|%[| %
188qed.
189
190definition taaf_append_tal : ∀S,st1,fl,st2,st3.
191  ∀taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
192  trace_any_label S fl st1 st3 ≝ λS,st1,fl,st2,st3,taaf.
193  match taaf return λst1,st2,taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
194  trace_any_label S fl st1 st3 with
195  [ taaf_base s ⇒ λ_.λtal.tal
196  | taaf_step s1 s2 s3 hd H I ⇒ λJ,tal.hd @ tal_step_default ????? H tal I J
197  ].
198
199lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2.
200  tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 →
201  tal_rel … tal1 (taaf_append_tal S2 st2_pre … taaf2 H tal2).
202#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * -H7 -H8 normalize //
203#H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24
204change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????);
205<associative_taa_append_tal /2 by taa_append_tal_rel/
206qed.
207
208(* little helpers *)
209lemma if_else_True : ∀b,P.P → if b then P else True.
210* // qed-.
211lemma if_then_True : ∀b,P.P → if b then True else P.
212* // qed-.
213
214include alias "basics/logic.ma".
215
216let rec status_simulation_produce_tlr S1 S2 (R : status_simulation S1 S2)
217  st1 st1' st2_lab st2
218  (tlr1 : trace_label_return S1 st1 st1')
219  (taa2_pre : trace_any_any S2 st2_lab st2)
220  on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
221  ∃st2_mid.∃st2'.
222  ∃tlr2 : trace_label_return S2 st2_lab st2_mid.
223  ∃taa2 : trace_any_any_free … st2_mid st2'.
224  (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
225  R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
226  tlr_rel … tlr1 tlr2 ≝
227 match tlr1 with
228 [ tlr_base st1 st1' tll1 ⇒ ?
229 | tlr_step st1 st1_mid st1' tll1 tl1 ⇒ ?
230 ]
231and status_simulation_produce_tll S1 S2 (R : status_simulation S1 S2)
232  fl st1 st1' st2_lab st2
233  (tll1 : trace_label_label S1 fl st1 st1')
234  (taa2_pre : trace_any_any S2 st2_lab st2)
235  on tll1 : R st1 st2 → label_rel … st1 st2_lab →
236    match fl with
237    [ ends_with_ret ⇒
238      ∃st2_mid.∃st2'.
239      ∃tll2 : trace_label_label S2 ends_with_ret st2_lab st2_mid.
240      ∃taa2 : trace_any_any_free … st2_mid st2'.
241      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
242      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
243      tll_rel … tll1 tll2
244    | doesnt_end_with_ret ⇒
245      ∃st2'.∃tll2 : trace_label_label S2 doesnt_end_with_ret st2_lab st2'.
246      R st1' st2' ∧ label_rel … st1' st2' ∧ tll_rel … tll1 tll2
247    ] ≝
248  match tll1 with
249  [ tll_base fl1' st1' st1'' tal1 H ⇒ ?
250  ]
251and status_simulation_produce_tal S1 S2 (R : status_simulation S1 S2)
252  fl st1 st1' st2
253  (tal1 : trace_any_label S1 fl st1 st1')
254  on tal1 : R st1 st2 →
255    match fl with
256    [ ends_with_ret ⇒
257      ∃st2_mid.∃st2'.
258      ∃tal2 : trace_any_label S2 ends_with_ret st2 st2_mid.
259      ∃taa2 : trace_any_any_free … st2_mid st2'.
260      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
261      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
262      tal_rel … tal1 tal2
263    | doesnt_end_with_ret ⇒
264      (∃st2'.∃tal2 : trace_any_label S2 doesnt_end_with_ret st2 st2'.
265       R st1' st2' ∧ label_rel … st1' st2' ∧ tal_rel … tal1 tal2) ∨
266      (* empty *)
267      (R st1' st2 ∧ label_rel … st1' st2 ∧ tal_collapsable … tal1 ∧ ¬as_costed … st1)
268    ] ≝
269  match tal1 with
270  [ tal_base_not_return st1' st1'' H G K ⇒ ?
271  | tal_base_return st1' st1'' H G ⇒ ?
272  | tal_base_call st1_pre_call st1_after_call st1' H f G K tlr1 L ⇒ ?
273  | tal_step_call fl1' st1' st1'' st1''' st1'''' H f G L tlr1 K tl1 ⇒ ?
274  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
275  ].
276#st1_R_st2
277[1,2,3: #st1_L_st2_lab ]
278[ (* tlr_base *)
279  elim (status_simulation_produce_tll … tll1 taa2_pre st1_R_st2 st1_L_st2_lab)
280  #st2_mid * #st2' * #tll2 #H
281  %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H
282| (* tlr_step *)
283  elim (status_simulation_produce_tll … tll1 taa2_pre st1_R_st2 st1_L_st2_lab)
284  #st2_mid * #tll2 ** #H1 #H2 #H3
285  elim (status_simulation_produce_tlr … tl1 (taa_base …) H1 H2)
286  #st2_mid' * #st2' * #tl2 * #taa2 * #H4 #H5
287  %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2}
288  %{H4} %{H3 H5}
289| (* tll_base *)
290  lapply (status_simulation_produce_tal ?? R ??? st2 tal1 st1_R_st2)
291  cases fl1' in tal1; normalize nodelta #tal1 *
292  [3: * #_ #ABS elim (absurd … H ABS) ]
293  [ #st2_mid ] * #st2' * #tal2 [* #taa2 ] * #H1 #H2
294  [%{st2_mid}] %{st2'} %{(tll_base … (taa_append_tal … taa2_pre tal2) ?)}
295  [1,3: whd <st1_L_st2_lab assumption
296  |*: [%{taa2} ] %{H1} %
297    [1,3: change with (opt_safe ??? = opt_safe ???)
298      @opt_safe_elim #a #EQ1
299      @opt_safe_elim #b <st1_L_st2_lab >EQ1 #EQ2  destruct %
300    |*: @taa_append_tal_rel assumption
301    ]
302  ]
303| (* tal_base_non_return *) whd
304  cases G #G'
305  elim (sim_execute … R … H st1_R_st2 G')
306  #st2' ** -st2 -st2'
307  [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *)
308    ** whd in ⊢ (%→?); #ncost #R' #L' %2 /4 by conj/
309  |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 *** #st1_R_st2' #st1_L_st2' %1
310    %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 (or_intror ?? I2) ?))}
311    [1,3: whd <st1_L_st2' assumption ]
312    % [1,3: /2 by conj/]
313    % try @refl %{st2_mid} %{taa2} %{H2} %[2,4: %[2,4: %]]
314  ]
315| (* tal_base_return *) whd
316  elim (sim_execute … R … H st1_R_st2 G)
317  #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
318  ***** #ncost #J2 #K2
319  #st1_Rret_st2' #st1_Rret_st2' #st1_L_st2'
320  %[2,4:%[2,4: %{(taa_append_tal … taa2 (tal_base_return … K2 J2))} %{taa2'}
321  % [ /4 by conj/ ]
322  %[ % | %[|%[|%[|%[| % ]]]]]]]
323| (* tal_base_call *) whd
324  elim (sim_execute … R … H st1_R_st2 G)
325  * #st2_pre_call * #f #G2 * #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
326  #st1_R_st2_mid #st1_L_st2_after_call
327  elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call)
328  #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2'
329  [ #st2' #tlr2 *****
330  | #st2_after_ret #st2_after_ret' #st2' #taa2''
331    #I2 #J2 #tlr2 **** #ncost
332  ]
333  #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S %1
334  %{st2'}
335  [ %{(taa2 @ tal_base_call ???? H2 ? G2 ? tlr2 ?)}
336    [3: % [ % assumption ]
337      % [%] %[|%[|%[|%[| %1 %[|%[|%[|%[|%[| %{S} % ]]]]]]]]]
338    ]
339  | %{(taa2 @ tal_step_call ?????? H2 ? G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 (or_intror ?? J2) ?))}
340    [3: % [ % assumption ]
341      % [%] %[|%[|%[|%[| %2 %[|%[|%[|%[|%[|%[|%[| % [ %{S} % ] /2 by taa_append_collapsable, I/
342      ]]]]]]]]]]]
343    ]
344  ]
345  [1,3: @(st1_Rret_st2' … st1_C_st2) assumption
346  |*: whd <st1_L_st2' assumption
347  ]
348| (* tal_step_call *)
349  elim (sim_execute … R … H st1_R_st2 G)
350  * #st2_pre_call * #f #G2 * #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
351  #st1_R_st2_mid #st1_L_st2_after_call
352  elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call)
353  #st2_after_ret * #st2' * #tlr2 * #taa2''
354  ****
355  #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S
356  lapply (status_simulation_produce_tal … tl1 st1_R_st2')
357  cases fl1' in tl1; #tl1 *
358  [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S'
359    %[|%[| %{(taa2 @ tal_step_call ?????? H2 ? G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
360    [4: %{taa2'''} % [ /4 by conj/ ]
361      %[|%[|%[|%[| %2 %[|%[|%[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]]
362    ]]] 
363  | *#st2'' *#tl2 ** #st1_R_st2'' #st1_L_st2'' #S' %1
364    %[| %{(taa2 @ tal_step_call ?????? H2 ? G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
365    [4: % [ /2 by conj/ ]
366      %[|%[|%[|%[| %2 %[|%[|%[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]]
367    ]]
368  | lapply S lapply tlr2 lapply st1_Rret_st2' lapply st1_L_st2' lapply st1_R_st2'
369    lapply taa_ncost cases taa2'' -st2_after_ret -st2'
370    [ #st2' * #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
371      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost %1
372      %[| %{(taa2 @ tal_base_call ???? H2 ? G2 ? tlr2 ?)}
373      [3: % [ /2 by conj/ ]
374      %[|%[|%[|%[| %1 %{(refl …)} %[|%[|%[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]]]]
375    | #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' #ncost
376      #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
377      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost' %1
378      %[| %{(taa2 @ tal_step_call ?????? H2 ? G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' (or_intror ?? J2') ?))}
379      [3: % [ /2 by conj/ ]
380        %[|%[|%[|%[| %2 %[|%[|%[|%[|%[|%[|%[| %{S} % [%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/
381        ]]]]]]]]]]]
382      ]]
383    ]
384  ]
385  [1,4,7,9: @(st1_Rret_st2' … st1_C_st2) assumption
386  |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2'
387    [1,3: #st2_after_ret * #L whd in ⊢ (?%); <L assumption
388    |*: #st2_after_ret #st2_post #st2' #tl2 #K #M #H #_ @H %
389    ]
390  |3,6: @if_else_True whd in ⊢ (?%); <st1_L_st2' assumption
391  |*: whd <st1_L_st2'' @(tal_end_costed … tl1)
392  ]
393| (* step_default *)
394  elim (sim_execute … R … H st1_R_st2 G)
395  #st2_mid *#taa2 ** #cost #st1_R_st2_mid #st1_L_st2_mid
396  lapply (status_simulation_produce_tal … tl1 st1_R_st2_mid)
397  cases fl1' in tl1; #tl1 *
398  [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G
399    %[|%[| %{(taaf_append_tal … taa2 ? tal2)}
400      [2: %{taa2'} % [/4 by conj/ ] @taaf_append_tal_rel @G ]
401    ]]
402  | *#st2' *#tal2 *#H #G %1
403    %[| %{(taaf_append_tal … taa2 ? tal2)}
404      [2: % [/2 by conj/] @taaf_append_tal_rel @G ]
405    ]
406  | lapply st1_L_st2_mid lapply st1_R_st2_mid lapply cost
407    cases taa2 -st2_mid -st2
408    [ #st2 #cost #_ #_ *#H #G %2 %{H cost} ]
409    #st2 #st2_mid' #st2_mid #hd #H2 #I2 * #st1_R_st2_mid #st1_L_st2_mid
410    *** #H #G #K #L %1
411    %[| %{(hd @ tal_base_not_return ??? H2 (or_intror ?? I2) ?)}
412    [2: % [/2 by conj/] @taa_append_tal_rel @tal_collapsable_to_rel assumption
413    |1: whd <G @(tal_end_costed … tl1)
414    ]]
415  ]
416  @if_else_True whd in ⊢ (?%); <st1_L_st2_mid assumption
417]
418qed.
Note: See TracBrowser for help on using the repository browser.