source: src/common/StatusSimulation.ma @ 2500

Last change on this file since 2500 was 2477, checked in by tranquil, 7 years ago

status_simulation reformulated
definition of joint_classify split up in subdefinitions

File size: 35.2 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
17(* We work with two relations on states in parallel, as well as two derived ones.
18   sem_rel is the classic semantic relation between states, keeping track of
19   memory and how program counters are mapped between languages.
20   call_rel keeps track of what pcs corresponding calls have and just that:
21   this is different than corresponance between program counters in sem_rel when
22   CALL f ↦ instr* CALL f instr* *)
23
24record status_rel
25  (S1 : abstract_status)
26  (S2 : abstract_status)
27  : Type[1] ≝
28  { sem_rel :2> S1 → S2 → Prop
29  (* this is kept separate, as not necessarily carrier will
30     synchronise on calls. It should state the minimal properties
31     necessary for as_after_return (typically just the program counter)
32     maybe what function is called too? *)
33  ; call_rel : (Σs.as_classifier S1 s cl_call) →
34               (Σs.as_classifier S2 s cl_call) → Prop
35  ; sim_final :
36    ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2
37  }.
38
39(* The two derived relations are
40   label_rel which tells that the two states are colabelled
41   ret_rel which tells that two return states are in relation: the idea is that
42   it happens when "going back" through as_after_return on one side we get
43   a pair of call_rel related states, then we enjoy as_after_return also on the
44   other. Roughly call_rel will store just enough information so that we can
45   advance locally on a return step and build structured traces any way *)
46
47(* if we later generalise, we should move this inside status_rel *)
48definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2.
49
50definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.
51  λs1_ret,s2_ret.
52  ∀s1_pre,s2_pre.as_after_return S1 s1_pre s1_ret →
53                 call_rel ?? R s1_pre s2_pre →
54                 as_after_return S2 s2_pre s2_ret.
55
56(* the equivalent of a collapsable trace_any_label where we do not force
57   costedness of the lookahead status *)
58inductive trace_any_any_free (S : abstract_status) : S → S → Type[0] ≝
59| taaf_base : ∀s.trace_any_any_free S s s
60| taaf_step : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
61  as_classifier S s2 cl_other →
62  trace_any_any_free S s1 s3.
63
64definition taaf_non_empty ≝ λS,s1,s2.λtaaf : trace_any_any_free S s1 s2.
65match taaf with
66[ taaf_base _ ⇒ false
67| taaf_step _ _ _ _ _ _ ⇒ true
68].
69
70(* the base property we ask for simulation to work depends on the status_class
71   S will mark semantic relation, C call relation, L label relation, R return relation *)
72
73definition status_simulation ≝
74  λS1 : abstract_status.
75  λS2 : abstract_status.
76  λsim_status_rel : status_rel S1 S2.
77    ∀st1,st1',st2.as_execute S1 st1 st1' →
78    sim_status_rel st1 st2 →
79    match as_classify … st1 with
80    [ cl_call ⇒ ∀prf.
81      (*
82           st1' ------------S----------\
83            ↑ \                         \
84           st1 \--L--\                   \
85            | \       \                   \
86            S  \-C-\  st2_after_call →taa→ st2'
87            |       \     ↑
88           st2 →taa→ st2_pre_call
89      *)
90      ∃st2_pre_call.
91      as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
92      call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
93      ∃st2_after_call,st2'.
94      ∃taa2 : trace_any_any … st2 st2_pre_call.
95      ∃taa2' : trace_any_any … st2_after_call st2'.
96      as_execute … st2_pre_call st2_after_call ∧
97      sim_status_rel st1' st2' ∧
98      label_rel … st1' st2_after_call
99    | cl_return ⇒
100      (*
101           st1
102          / ↓
103         | st1'----------S,L------------\
104         S   \                           \
105          \   \-----R-------\            |     
106           \                 |           |
107           st2 →taa→ st2_ret |           |
108                        ↓   /            |
109                   st2_after_ret →taaf→ st2'
110
111         we also ask that st2_after_ret be not labelled if the taaf tail is
112         not empty
113      *)
114      ∃st2_ret,st2_after_ret,st2'.
115      ∃taa2 : trace_any_any … st2 st2_ret.
116      ∃taa2' : trace_any_any_free … st2_after_ret st2'.
117      (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
118      as_classifier … st2_ret cl_return ∧
119      as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
120      ret_rel … sim_status_rel st1' st2_after_ret ∧
121      label_rel … st1' st2'
122    | cl_other ⇒
123        (*         
124        st1 → st1'
125          |      \
126          S      S,L
127          |        \
128         st2 →taaf→ st2'
129         
130         the taaf can be empty (e.g. tunneling) but we ask it must not be the
131         case when both st1 and st1' are labelled (we would be able to collapse
132         labels otherwise)
133       *)
134      ∃st2'.
135      ∃taa2 : trace_any_any_free … st2 st2'.
136      (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
137      sim_status_rel st1' st2' ∧
138      label_rel … st1' st2'
139    | cl_jump ⇒
140      (*
141          st1 → st1'           st1 → st1'--------\
142          |    /               |                  \
143          S  S,L       or      S                  S,L
144          |  /                 |                    \
145          st2                 st2 →collapsable tal→ st2'
146      *)
147      (¬as_costed … st1 (* st1' will necessarily be costed *) ∧
148       sim_status_rel st1' st2 ∧ label_rel … st1' st2) ∨
149      (∃st2'.∃tal : trace_any_label … doesnt_end_with_ret st2 st2'.
150        tal_collapsable … tal ∧
151        sim_status_rel st1' st2' ∧ label_rel … st1' st2')
152    ].
153
154
155(* some useful lemmas *)
156
157let rec taa_append_taa S st1 st2 st3
158  (taa : trace_any_any S st1 st2) on taa :
159  trace_any_any S st2 st3 →
160  trace_any_any S st1 st3 ≝
161  match taa
162  with
163  [ taa_base st1' ⇒ λst3,taa2.taa2
164  | taa_step st1' st2' st3' H I J tl ⇒ λst3,taa2.
165    taa_step ???? H I J (taa_append_taa … tl taa2)
166  ] st3.
167
168lemma associative_taa_append_tal : ∀S,s1,s2,fl,s3,s4.
169  ∀taa1 : trace_any_any S s1 s2.
170  ∀taa2 : trace_any_any S s2 s3.
171  ∀tal : trace_any_label S fl s3 s4.
172  (taa_append_taa … taa1 taa2) @ tal = taa1 @ taa2 @ tal.
173#S #s1 #s2 #fl #s3 #s4 #taa1 elim taa1 -s1 -s2
174[ #s1 #taa2 #tal %
175| #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
176  normalize >IH %
177]
178qed.
179
180lemma associative_taa_append_taa : ∀S,s1,s2,s3,s4.
181  ∀taa1 : trace_any_any S s1 s2.
182  ∀taa2 : trace_any_any S s2 s3.
183  ∀taa3 : trace_any_any S s3 s4.
184  taa_append_taa … (taa_append_taa … taa1 taa2) taa3 =
185  taa_append_taa … taa1 (taa_append_taa … taa2 taa3).
186#S #s1 #s2 #s3 #s4 #taa1 elim taa1 -s1 -s2
187[ #s1 #taa2 #tal %
188| #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
189  normalize >IH %
190]
191qed.
192
193let rec taa_append_tal_rel S1 fl1 st1 st1'
194  (tal1 : trace_any_label S1 fl1 st1 st1')
195  S2 st2 st2mid fl2 st2'
196  (taa2 : trace_any_any S2 st2 st2mid)
197  (tal2 : trace_any_label S2 fl2 st2mid st2')
198  on tal1 :
199  tal_rel … tal1 tal2 →
200  tal_rel … tal1 (taa2 @ tal2) ≝
201match tal1 return λfl1,st1,st1',tal1.? with
202  [ tal_base_not_return st1 st1' _ _ _ ⇒ ?
203  | tal_base_return st1 st1' _ _ ⇒ ?
204  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ?
205  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ?
206  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ?
207  ].
208[ * #EQfl *#st2mid *#taa2' *#H2 *#G2 *#K2 #EQ
209| * #EQfl *#st2mid *#taa2' *#H2 *#G2 #EQ
210| * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
211  [ *#K2 *#tlr2 *#L2 * #EQ #EQ'
212  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll
213  ]
214| * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *
215  [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ'
216  | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #EQ''
217  ]
218| whd in ⊢ (%→%); @(taa_append_tal_rel … tl1)
219]
220destruct
221<associative_taa_append_tal
222  [1,2,3,4:%{(refl …)}] %{st2mid}
223  [1,2:|*: %{G2} %{EQcall} ]
224  %{(taa_append_taa … taa2 taa2')}
225  [1,2: %{H2} %{G2} [%{K2}] %
226  |*: %{st2mid'} %{H2}
227    [1,3: %1 [|%{(refl …)}] |*: %2 %{st2mid''} ]
228    %{K2} %{tlr2} %{L2} [3,4: %{tl2} ] /3 by conj/
229  ]
230qed.
231
232let rec tal_end_costed S st1 st2 (tal : trace_any_label S doesnt_end_with_ret st1 st2)
233  on tal : as_costed … st2 ≝
234  match tal return λfl,st1,st2,tal.fl = doesnt_end_with_ret → as_costed ? st2 with
235  [ tal_step_call fl' _ _ st1' st2' _ _ _ _ _ tl ⇒ λprf.tal_end_costed ? st1' st2' (tl⌈trace_any_label ????↦?⌉)
236  | tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ λprf.tal_end_costed ? st1'st2' (tl⌈trace_any_label ????↦?⌉)
237  | tal_base_not_return _ st2' _ _ K ⇒ λ_.K
238  | tal_base_return _ _ _ _ ⇒ λprf.⊥
239  | tal_base_call _ _ st2' _ _ _ _ K ⇒ λ_.K
240  ] (refl …).
241[ destruct
242|*: >prf %
243]
244qed.
245
246lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2.
247  if taa_non_empty … taa then ¬as_costed … s2 else True.
248#S #s1 #s2 #taa elim taa -s1 -s2 normalize nodelta
249[ #s1 %
250| #s1 #s2 #s3 #H #G #K #tl lapply K lapply H cases tl -s2 -s3
251  [ #s2 #H #K #_ assumption
252  | #s2 #s3 #s4 #H' #G' #K' #tl' #H #K #I @I
253  ]
254]
255qed.
256
257let rec tal_collapsable_to_rel S fl st1 st2
258  (tal : trace_any_label S fl st1 st2) on tal :
259  tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
260  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) ≝
261  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J.
262  tal_rel … tal (tal_base_not_return S2 st12 st22 H I J)
263  with
264  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_to_rel ???? tl
265  | tal_base_not_return _ st2' _ _ K ⇒ ?
266  | _ ⇒ Ⓧ
267  ].
268* #S2 #st12 #st22 #H #I #J % %[|%{(taa_base ??)} %[|%[|%[| %
269qed.
270
271let rec tal_collapsable_eq_flag S fl st1 st2
272  (tal : trace_any_label S fl st1 st2) on tal :
273  tal_collapsable ???? tal → fl = doesnt_end_with_ret ≝
274  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → fl = ?
275  with
276  [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_eq_flag ???? tl
277  | tal_base_not_return _ st2' _ _ K ⇒ λ_.refl …
278  | _ ⇒ Ⓧ
279  ].
280
281let rec tal_collapsable_split S fl st1 st2
282  (tal : trace_any_label S fl st1 st2) on tal :
283  tal_collapsable ???? tal → ∃st2_mid.∃taa : trace_any_any S st1 st2_mid.∃H,I,J.
284  tal ≃ taa @ tal_base_not_return … st2 H I J ≝
285  match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∃st2_mid,taa,H,I,J.
286  tal ≃ taa @ tal_base_not_return … st2_mid ? H I J
287  with
288  [ tal_step_default fl' st1' st2' st3' H tl I J ⇒ ?
289  | tal_base_not_return st1' st2' H I J ⇒ ?
290  | _ ⇒ Ⓧ
291  ].
292[ * %{st1'} %{(taa_base …)} %{H} %{I} %{J} %
293| #coll
294  elim (tal_collapsable_split … tl coll) #st2_mid * #taa * #H' * #I' *#J'
295  #EQ %{st2_mid} %{(taa_step … taa)} try assumption
296  %{H'} %{I'} %{J'} lapply EQ lapply tl >(tal_collapsable_eq_flag … coll) -tl #tl
297  #EQ >EQ %
298]
299qed.
300
301lemma tal_collapsable_to_rel_symm : ∀S,fl,st1,st2,tal.
302tal_collapsable S fl st1 st2 tal → ∀S2,st12,st22,H,I,J.
303  tal_rel … (tal_base_not_return S2 st12 st22 H I J) tal.
304#S #fl #st1 #st2 #tal #coll #S2 #st12 #st22 #H #I #J
305elim (tal_collapsable_split … coll) lapply tal
306 >(tal_collapsable_eq_flag … coll) -tal #tal
307#st2_mid * #taa *#H' *#I' *#J' #EQ >EQ % [%]
308%[|%[|%[|%[|%[| % ]]]]]
309qed.
310
311definition taaf_append_tal : ∀S,st1,fl,st2,st3.
312  ∀taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
313  trace_any_label S fl st1 st3 ≝ λS,st1,fl,st2,st3,taaf.
314  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 →
315  trace_any_label S fl st1 st3 with
316  [ taaf_base s ⇒ λ_.λtal.tal
317  | taaf_step s1 s2 s3 hd H I ⇒ λJ,tal.hd @ tal_step_default ????? H tal I J
318  ].
319
320lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2.
321  tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 →
322  tal_rel … tal1 (taaf_append_tal S2 st2_pre … taaf2 H tal2).
323#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * -H7 -H8 normalize //
324#H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24
325change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????);
326<associative_taa_append_tal /2 by taa_append_tal_rel/
327qed.
328
329(* little helpers *)
330lemma if_else_True : ∀b,P.P → if b then P else True.
331* // qed-.
332lemma if_then_True : ∀b,P.P → if b then True else P.
333* // qed-.
334
335include alias "basics/logic.ma".
336
337let rec status_simulation_produce_tlr S1 S2 R
338(* we start from this situation
339     st1 →→→→tlr→→→→ st1'
340      | \
341      L  \---S--\
342      |          \
343   st2_lab →taa→ st2   (the taa preamble is in general either empty or given
344                        by the preceding call)
345   
346   and we produce
347     st1 →→→→tlr→→→→ st1'
348             \\      /  \
349             //     R    \-L,S-\
350             \\     |           \
351   st2_lab →tlr→ st2_mid →taaf→ st2'
352*)
353  st1 st1' st2_lab st2
354  (tlr1 : trace_label_return S1 st1 st1')
355  (taa2_pre : trace_any_any S2 st2_lab st2)
356  (sim_execute : status_simulation S1 S2 R)
357  on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
358  ∃st2_mid.∃st2'.
359  ∃tlr2 : trace_label_return S2 st2_lab st2_mid.
360  ∃taa2 : trace_any_any_free … st2_mid st2'.
361  (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
362  R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
363  tlr_rel … tlr1 tlr2 ≝
364 match tlr1 with
365 [ tlr_base st1 st1' tll1 ⇒ ?
366 | tlr_step st1 st1_mid st1' tll1 tl1 ⇒ ?
367 ]
368and status_simulation_produce_tll S1 S2 R
369(* we start from this situation
370     st1 →→→→tll→→→ st1'
371      | \
372      L  \---S--\
373      |          \
374   st2_lab →taa→ st2
375   
376   and if the tll is a returning one we produce a diagram like the one for tlr,
377   otherwise a simpler:
378     st1 →→→→tll→→→→ st1'
379             \\       |
380             //      L,S
381             \\       |
382   st2_lab →→→tll→→→ st2'
383*)
384  fl st1 st1' st2_lab st2
385  (tll1 : trace_label_label S1 fl st1 st1')
386  (taa2_pre : trace_any_any S2 st2_lab st2)
387  (sim_execute : status_simulation S1 S2 R)
388   on tll1 : R st1 st2 → label_rel … st1 st2_lab →
389    match fl with
390    [ ends_with_ret ⇒
391      ∃st2_mid.∃st2'.
392      ∃tll2 : trace_label_label S2 ends_with_ret st2_lab st2_mid.
393      ∃taa2 : trace_any_any_free … st2_mid st2'.
394      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
395      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
396      tll_rel … tll1 tll2
397    | doesnt_end_with_ret ⇒
398      ∃st2'.∃tll2 : trace_label_label S2 doesnt_end_with_ret st2_lab st2'.
399      R st1' st2' ∧ label_rel … st1' st2' ∧ tll_rel … tll1 tll2
400    ] ≝
401  match tll1 with
402  [ tll_base fl1' st1' st1'' tal1 H ⇒ ?
403  ]
404and status_simulation_produce_tal S1 S2 R
405(* we start from this situation
406     st1 →→tal→→ st1'
407      |
408      S
409      |
410     st2
411   
412   and if the tal is a returning one we produce a diagram like the one for tlr,
413   otherwise we allow for two possibilities:
414   either
415
416     st1 →→tal→→ st1'
417            \\    |
418            //   L,S
419            \\    |
420     st2 →→tal→→ st2'
421
422   or we do not advance from st2:
423
424     st1 →→tal→→ st1'  collapsable, and st1 uncosted
425                /
426         /-L,S-/
427        /
428     st2
429*)
430  fl st1 st1' st2
431  (tal1 : trace_any_label S1 fl st1 st1')
432  (sim_execute : status_simulation S1 S2 R)
433   on tal1 : R st1 st2 →
434    match fl with
435    [ ends_with_ret ⇒
436      ∃st2_mid.∃st2'.
437      ∃tal2 : trace_any_label S2 ends_with_ret st2 st2_mid.
438      ∃taa2 : trace_any_any_free … st2_mid st2'.
439      (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
440      R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
441      tal_rel … tal1 tal2
442    | doesnt_end_with_ret ⇒
443      (∃st2'.∃tal2 : trace_any_label S2 doesnt_end_with_ret st2 st2'.
444       R st1' st2' ∧ label_rel … st1' st2' ∧ tal_rel … tal1 tal2) ∨
445      (* empty *)
446      (R st1' st2 ∧ label_rel … st1' st2 ∧ tal_collapsable … tal1 ∧ ¬as_costed … st1)
447    ] ≝
448  match tal1 with
449  [ tal_base_not_return st1' st1'' H G K ⇒ ?
450  | tal_base_return st1' st1'' H G ⇒ ?
451  | tal_base_call st1_pre_call st1_after_call st1' H G K tlr1 L ⇒ ?
452  | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ?
453  | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ?
454  ].
455#st1_R_st2
456[1,2,3: #st1_L_st2_lab ]
457[ (* tlr_base *)
458  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
459  #st2_mid * #st2' * #tll2 #H
460  %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H
461| (* tlr_step *)
462  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
463  #st2_mid * #tll2 ** #H1 #H2 #H3
464  elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute H1 H2)
465  #st2_mid' * #st2' * #tl2 * #taa2 * #H4 #H5
466  %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2}
467  %{H4} %{H3 H5}
468| (* tll_base *)
469  lapply (status_simulation_produce_tal … st2 tal1 sim_execute st1_R_st2)
470  cases fl1' in tal1; normalize nodelta #tal1 *
471  [3: * #_ #ABS elim (absurd … H ABS) ]
472  [ #st2_mid ] * #st2' * #tal2 [* #taa2 ] * #H1 #H2
473  [%{st2_mid}] %{st2'} %{(tll_base … (taa_append_tal … taa2_pre tal2) ?)}
474  [1,3: whd <st1_L_st2_lab assumption
475  |*: [%{taa2} ] %{H1} %
476    [1,3: change with (opt_safe ??? = opt_safe ???)
477      @opt_safe_elim #a #EQ1
478      @opt_safe_elim #b <st1_L_st2_lab >EQ1 #EQ2  destruct %
479    |*: @taa_append_tal_rel assumption
480    ]
481  ]
482| (* tal_base_non_return *) whd
483  cases G -G #G
484  lapply (sim_execute … H st1_R_st2)
485  (* without try it fails... why? *)
486  try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
487  [ (* jump to none *)
488    ** #K' #st1_R_st2' #st1_L_st2' %2 /4 by conj/
489  | (* jump to some *)
490    * #st2' * #tal2 ** #tal2_coll #st1_R_st2' #st1_L_st2'
491    %1
492    %{st2'} %{tal2} % [ /3 by conj/ ]
493    @tal_collapsable_to_rel_symm assumption
494  | (* other *)
495    #st2' ** -st2 -st2'
496    [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *)
497      ** whd in ⊢ (%→?); *
498      [1,3: #ncost #R' #L' %2 /4 by conj/
499      |*: * #ABS elim (ABS K)
500      ]
501    |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 *** #st1_R_st2' #st1_L_st2' %1
502      %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 (or_intror ?? I2) ?))}
503      [1,3: whd <st1_L_st2' assumption ]
504      % [1,3: /2 by conj/]
505      % try @refl %{st2_mid} %{taa2} %{H2} %[2,4: %[2,4: %]]
506    ]
507  ]
508| (* tal_base_return *) whd
509  lapply (sim_execute … H st1_R_st2)
510  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
511  #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
512  ***** #ncost #J2 #K2
513  #st1_Rret_st2' #st1_Rret_st2' #st1_L_st2'
514  %[2,4:%[2,4: %{(taa_append_tal … taa2 (tal_base_return … K2 J2))} %{taa2'}
515  % [ /4 by conj/ ]
516  %[ % | %[|%[|%[|%[| % ]]]]]]]
517| (* tal_base_call *) whd
518  lapply (sim_execute … H st1_R_st2)
519  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
520  #H elim (H G) -H
521  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
522  #st1_R_st2_mid #st1_L_st2_after_call
523  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
524  #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2'
525  [ #st2' #tlr2 *****
526  | #st2_after_ret #st2_after_ret' #st2' #taa2''
527    #I2 #J2 #tlr2 **** #ncost
528  ]
529  #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S %1
530  %{st2'}
531  [ %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
532    [3: % [ % assumption ]
533      % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]]
534    ]
535  | %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 (or_intror ?? J2) ?))}
536    [3: % [ % assumption ]
537      % [%] %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| % [ %{S} % ] /2 by taa_append_collapsable, I/
538      ]]]]]]]]]]
539    ]
540  ]
541  [1,3: @(st1_Rret_st2' … st1_C_st2) assumption
542  |*: whd <st1_L_st2' assumption
543  ]
544| (* tal_step_call *)
545  lapply (sim_execute … H st1_R_st2)
546  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?);
547  #H elim (H G) -H
548  * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
549  #st1_R_st2_mid #st1_L_st2_after_call
550  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
551  #st2_after_ret * #st2' * #tlr2 * #taa2''
552  ****
553  #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S
554  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2')
555  cases fl1' in tl1; #tl1 *
556  [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S'
557    %[|%[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
558    [4: %{taa2'''} % [ /4 by conj/ ]
559      %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
560    ]]] 
561  | *#st2'' *#tl2 ** #st1_R_st2'' #st1_L_st2'' #S' %1
562    %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))}
563    [4: % [ /2 by conj/ ]
564      %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]]
565    ]]
566  | lapply S lapply tlr2 lapply st1_Rret_st2' lapply st1_L_st2' lapply st1_R_st2'
567    lapply taa_ncost cases taa2'' -st2_after_ret -st2'
568    [ #st2' * #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
569      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost %1
570      %[| %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)}
571      [3: % [ /2 by conj/ ]
572      %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]]]
573    | #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' #ncost
574      #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S
575      *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost' %1
576      %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' (or_intror ?? J2') ?))}
577      [3: % [ /2 by conj/ ]
578        %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/
579        ]]]]]]]]]]
580      ]]
581    ]
582  ]
583  [1,4,7,9: @(st1_Rret_st2' … st1_C_st2) assumption
584  |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2'
585    [1,3: #st2_after_ret * #L whd in ⊢ (?%); <L assumption
586    |*: #st2_after_ret #st2_post #st2' #tl2 #K #M #H #_ @H %
587    ]
588  |3,6: @if_else_True whd in ⊢ (?%); <st1_L_st2' assumption
589  |*: whd <st1_L_st2'' @(tal_end_costed … tl1)
590  ]
591| (* step_default *)
592  lapply (sim_execute … H st1_R_st2)
593  >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
594  #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
595  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
596  cases fl1' in tl1; #tl1 *
597  [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G
598    %[|%[| %{(taaf_append_tal … taa2 ? tal2)}
599      [2: %{taa2'} % [/4 by conj/ ] @taaf_append_tal_rel @G ]
600    ]]
601  | *#st2' *#tal2 *#H #G %1
602    %[| %{(taaf_append_tal … taa2 ? tal2)}
603      [2: % [/2 by conj/] @taaf_append_tal_rel @G ]
604    ]
605  | (* can't happen *)
606    *** #_ #L' elim (absurd ?? K)
607    whd >st1_L_st2_mid <L' @(tal_end_costed … tl1)
608  ]
609  @if_else_True whd in ⊢ (?%); <st1_L_st2_mid assumption
610]
611qed.
612
613(* finite flat traces, with recursive structure right to left. The list of
614   identifiers represents the call stack *)
615
616inductive flat_trace (S : abstract_status) (start : S) : S → list ident → Type[0] ≝
617| ft_start : flat_trace S start start [ ]
618| ft_advance_flat :
619  ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
620  (as_classifier ? st1 cl_jump ∨ as_classifier ? st1 cl_other) →
621  flat_trace S start st2 stack
622| ft_advance_call :
623  ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 →
624  ∀prf : as_classifier ? st1 cl_call.
625  flat_trace S start st2 (as_call_ident ? «st1, prf» :: stack)
626| ft_advance_ret :
627  ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 →
628  as_classifier ? st1 cl_return →
629  flat_trace S start st2 stack.
630
631let rec ft_extend_taa S st1 st2 stack st3 (ft : flat_trace S st1 st2 stack)
632  (taa : trace_any_any S st2 st3)
633on taa : flat_trace S st1 st3 stack ≝
634match taa return λst2,st3,taa.flat_trace ?? st2 ? → flat_trace ?? st3 ? with
635[ taa_base s ⇒ λacc.acc
636| taa_step st1 st2 st3 H G _ tl ⇒
637  λacc.ft_extend_taa ????? (ft_advance_flat ????? acc H (or_intror … G)) tl
638] ft.
639
640lemma ft_extend_extend_taa : ∀S,st1,st2,stack,st3,st4,ft,taa1,taa2.
641  ft_extend_taa S st1 st3 stack st4 (ft_extend_taa ?? st2 ?? ft taa1) taa2 =
642  ft_extend_taa … ft (taa_append_taa … taa1 taa2).
643#S #st1 #st2 #stack #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize
644/2/
645qed.
646
647definition ft_extend_taaf ≝ λS,st1,st2,stack,st3.λft : flat_trace S st1 st2 stack.
648  λtaaf : trace_any_any_free S st2 st3.
649  match taaf return λst2,st3,taaf.flat_trace ?? st2 ? → flat_trace ?? st3 ? with
650  [ taaf_base s ⇒ λft.ft
651  | taaf_step s1 s2 s3 pre H G ⇒
652    λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_intror … G)
653  ] ft.
654
655definition option_to_list : ∀A.option A → list A ≝ λA,x.
656  match x with
657  [ Some x ⇒ [x]
658  | None ⇒ [ ]
659  ].
660
661(* the observables of a flat trace (for the moment, only labels, calls and returns) *)
662
663inductive intensional_event : Type[0] ≝
664| IEVcost : costlabel → intensional_event
665| IEVcall : ident → intensional_event
666| IEVret : ident → intensional_event.
667
668let rec ft_observables_aux acc S st st' stack
669  (ft : flat_trace S st st' stack) on ft : list intensional_event ≝
670match ft with
671[ ft_start ⇒ acc
672| ft_advance_flat st1_mid st1' stack pre1 _ _ ⇒
673  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
674  ft_observables_aux (add @ acc) … pre1
675| ft_advance_call st1_mid st1' stack pre1 _ prf ⇒
676  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
677  let add ≝ add @ [IEVcall (as_call_ident ? «st1_mid, prf»)] in
678  ft_observables_aux (add @ acc) … pre1
679| ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒
680  let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in
681  let add ≝ add @ [IEVret f] in
682  ft_observables_aux (add @ acc) … pre1
683].
684
685definition ft_observables ≝ ft_observables_aux [ ].
686
687lemma ft_observables_aux_def : ∀acc,S,st1,st2,stack,ft.
688  ft_observables_aux acc S st1 st2 stack ft = ft_observables … ft @ acc.
689#acc #S #st1 #st2 #stack #ft lapply acc -acc elim ft -st2 -stack
690[ // ]
691#st2 #st3 #stack [3: #f ] #pre #H #G #IH #acc
692whd in ⊢ (??%(??%?));
693>IH >IH >append_nil //
694qed.
695
696lemma ft_extend_taa_obs : ∀S,st1,st2,stack,st3,ft,taa.
697  ft_observables … (ft_extend_taa S st1 st2 stack st3 ft taa) =
698    ft_observables … ft @
699    if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
700#S #st1 #st2 #stack #st3 #ft #taa lapply ft elim taa -st2 -st3
701[ #st2 #ft >append_nil % ]
702#st2 #st3 #st4 #H #K #G #taa #IH #ft
703normalize in ⊢ (??(?????%)?); >IH
704-IH lapply G lapply H cases taa -st3 -st4 normalize nodelta
705[ #st3 #H #G
706| #st3 #st4 #st5 #ex #H' #G' #taa #H #G
707  whd in match (as_label ? st3); >(not_costed_no_label … G)
708] >append_nil whd in ⊢ (??%?); >ft_observables_aux_def >append_nil %
709qed.
710
711lemma ft_extend_taa_advance_call_obs : ∀S,st1,st2,stack,st3,st4.
712  ∀ft : flat_trace S st1 st2 stack.
713  ∀taa : trace_any_any S st2 st3.
714  ∀H : as_execute S st3 st4.∀G.
715  ft_observables … (ft_advance_call … (ft_extend_taa … ft taa) H G) =
716  ft_observables … ft @
717  option_to_list … (!l←as_label … st2;return IEVcost l) @
718  [IEVcall (as_call_ident … «st3, G»)].
719#S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
720whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
721>ft_extend_taa_obs
722lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
723[ #st2 * #ft #H #G >append_nil %
724| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G
725  whd in match (as_label ? st3); >(not_costed_no_label … K)
726  normalize nodelta //
727]
728qed.
729
730lemma ft_extend_taa_advance_ret_obs : ∀S,st1,st2,stack,f,st3,st4.
731  ∀ft : flat_trace S st1 st2 (f :: stack).
732  ∀taa : trace_any_any S st2 st3.
733  ∀H : as_execute S st3 st4.∀G.
734  ft_observables … (ft_advance_ret … (ft_extend_taa … ft taa) H G) =
735    ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVret f].
736#S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G
737whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
738>ft_extend_taa_obs
739lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
740[ #st2 * #ft #H >append_nil %
741| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
742  whd in match (as_label ? st3); >(not_costed_no_label … K)
743  normalize nodelta //
744]
745qed.
746
747lemma ft_extend_taa_advance_flat_obs : ∀S,st1,st2,stack,st3,st4.
748  ∀ft : flat_trace S st1 st2 stack.
749  ∀taa : trace_any_any S st2 st3.
750  ∀H : as_execute S st3 st4.∀G.
751  ft_observables … (ft_advance_flat … (ft_extend_taa … ft taa) H G) =
752    ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l).
753#S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G
754whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
755>ft_extend_taa_obs
756lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3
757[ #st2 * #ft #H >append_nil %
758| #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H
759  whd in match (as_label ? st3); >(not_costed_no_label … K)
760  normalize nodelta >append_nil //
761]
762qed.
763
764lemma ft_extend_taaf_obs : ∀S,st1,st2,stack,st3,ft,taaf.
765  ft_observables … (ft_extend_taaf S st1 st2 stack st3 ft taaf) =
766    ft_observables … ft @
767    if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ].
768#S #st1 #st2 #stack #st3 #ft #taa lapply ft cases taa -st2 -st3
769[ #st2 #ft >append_nil % ]
770#st2 #st3 #st4 #taa #H normalize nodelta #G #ft
771@ft_extend_taa_advance_flat_obs
772qed.
773
774(* little helper to avoid splitting equal cases *)
775lemma if_eq : ∀b,A.∀x : A.if b then x else x = x. * // qed-.
776
777theorem status_simulation_produce_ft :
778(* from
779
780  st1 →→→ft→→→ st1'
781   |
782  R,L
783   |
784  st2
785
786  we produce
787 
788  st1 →→→ft→→→ st1'-------\
789         //      \         \
790         \\       L         S
791         //       |          \
792  st2 →→→ft→→→ st2_lab →taa→ st2'
793 
794  so that from any tlr or tll following st1' we can produce the corresponding
795  structured trace from st2_lab using the previous result
796*)
797  ∀S1,S2.
798  ∀R.
799  ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack.
800  status_simulation S1 S2 R → label_rel … st1 st2 → R st1 st2 →
801  ∃st2_lab,st2'.
802  ∃ft2 : flat_trace S2 st2 st2_lab stack.
803  ∃taa : trace_any_any S2 st2_lab st2'.
804  label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2.
805#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack
806[ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
807|*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl
808  (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S
809  [ (* jump *)
810    lapply (sim_execute … ex G')
811    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
812    [ ** #ncost #G'' #H''
813      %{st2_mid} %{st2_mid}
814      %[@(ft_extend_taa … taa)
815        assumption]
816      %{(taa_base …)} % [ %{H'' G''} ]
817      whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
818      >ft_extend_taa_obs <L'
819      whd in match (as_label ? st1_mid);
820      >(not_costed_no_label … ncost) >if_eq >S %
821    | * #st2' * #tal ** #coll
822      elim (tal_collapsable_split … coll) #st2_mid' * #taa2
823      * #K2 * #J2 *#H2 #EQ  #G'' #H''
824      %{st2'} %{st2'}
825      %[@(ft_advance_flat … K2 J2)
826        @(ft_extend_taa … (taa_append_taa … taa taa2))
827        assumption]
828      %{(taa_base …)} % [ %{H'' G''} ]
829      >ft_extend_taa_advance_flat_obs
830      whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
831      <S <L' %
832    ]
833  | (* other *)
834    lapply (sim_execute … ex G')
835    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
836    #st2' *#taaf ** #ncost #G'' #H''
837    %{st2'} %{st2'}
838    %[1,3:
839      @(ft_extend_taaf … taaf)
840      @(ft_extend_taa … taa)
841      assumption]
842    %{(taa_base …)}
843    % [1,3: %{H'' G''} ]
844    whd in ⊢ (??%?); >ft_observables_aux_def >append_nil
845    lapply ncost lapply taa lapply H'' cases taaf -st2_mid -st2'
846    [1,3: #st2' #H'' #taa * #ncost
847      >ft_extend_taa_obs <L'
848      [1,3: whd in match (as_label ? st1_mid);
849        >(not_costed_no_label … ncost) >if_eq >S %
850      |*: lapply L' lapply H'' lapply S lapply ft2 cases taa -st2_lab -st2'
851        [1,3: #st2' #ft2 #S #H'' #L' >append_nil
852          whd in match (as_label ??); >not_costed_no_label
853          [1,3: >append_nil @S ]
854          whd in ⊢ (?%); >L' <H'' assumption
855        |*: normalize nodelta #st2_mid #st2_mid' #st2' #_ #_ #_ #taa #ft2 #S #_ #_
856          >S %
857        ]
858      ]
859    |*: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' #_ #taa *
860      whd in ⊢ (???(?????%));
861      >ft_extend_extend_taa >ft_extend_taa_advance_flat_obs
862      >S >L' %
863    ]
864  |3: (* ret *)
865    lapply (sim_execute … ex G')
866    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); *
867    #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
868    ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'}
869    %[@(ft_extend_taaf … taa2')
870      @(ft_advance_ret … f … ex' cl')
871      @(ft_extend_taa … (taa_append_taa … taa taa2))
872      assumption]
873    %{(taa_base …)}
874    % [ %{H'' G''} ]
875    >ft_extend_taaf_obs
876    >ft_extend_taa_advance_ret_obs
877    whd in ⊢ (??%?);
878    >ft_observables_aux_def >append_nil
879    lapply ncost cases taa2' -st2_after_ret -st2'
880    [ #st2' * >append_nil
881    | #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' #ncost
882      whd in match (as_label ? st2_after_ret); >(not_costed_no_label … ncost)
883      >if_eq >append_nil
884    ]
885    >S >L' %
886  |4: (* call *)
887    lapply (sim_execute … ex G')
888    >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]→?); #H elim (H cl) -H
889    * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2'
890    * #taa2 * #taa2' ** #ex' #G'' #H''
891    %{st2_after_call} %{st2'}
892    lapply (refl_jmeq … (ft_advance_call … ft1 ex cl))
893    generalize in match (ft_advance_call … ft1 ex cl) in ⊢ (????%→%);
894    <EQcall in ⊢ (%→???%%→%);
895    #ft1' #EQft1'
896    %[@(ft_advance_call … ex' cl')
897      @(ft_extend_taa … (taa_append_taa … taa taa2))
898      assumption]
899    %{taa2'}
900    % [ %{H'' G''} ]
901    >ft_extend_taa_advance_call_obs
902    lapply EQft1' lapply ft1' -ft1'
903    >EQcall in ⊢ (%→???%%→%);
904    #ft1' #EQft1' destruct (EQft1')
905    whd in ⊢ (??%?);
906    >ft_observables_aux_def >append_nil
907    >S >L' %
908  ]
909]
910qed.
Note: See TracBrowser for help on using the repository browser.