source: src/common/SmallstepExec.ma @ 2668

Last change on this file since 2668 was 2668, checked in by campbell, 7 years ago

Intermediate measurable proof check-in before I change its traces again.

File size: 19.8 KB
Line 
1include "utilities/extralib.ma".
2include "common/IOMonad.ma".
3include "common/Integers.ma".
4include "common/Events.ma".
5
6record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
7{ global : Type[1]
8; state  : global → Type[0]
9; is_final : ∀g. state g → option int
10; step : ∀g. state g → IO outty inty (trace×(state g))
11}.
12
13let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:trans_system outty inty)
14               (g:global ?? exec) (s:state ?? exec g)
15 : IO outty inty (trace × (state ?? exec g)) ≝
16match n with
17[ O ⇒ Value ??? 〈E0, s〉
18| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
19         ! 〈tn,sn〉 ← repeat n' ?? exec g s1;
20         Value ??? 〈t1⧺tn,sn〉
21].
22
23(* We take care here to check that we're not at the final state.  It is not
24   necessarily the case that a success step guarantees this (e.g., because
25   there may be no way to stop a processor, so an infinite loop is used
26   instead). *)
27inductive plus (O) (I) (TS:trans_system O I) (ge:global … TS) : state … TS ge → trace → state … TS ge → Prop ≝
28| plus_one : ∀s1,tr,s2.
29    is_final … TS ge s1 = None ? →
30    step … TS ge s1 = OK … 〈tr,s2〉 →
31    plus … ge s1 tr s2
32| plus_succ : ∀s1,tr,s2,tr',s3.
33    is_final … TS ge s1 = None ? →
34    step … TS ge s1 = OK … 〈tr,s2〉 →
35    plus … ge s2 tr' s3 →
36    plus … ge s1 (tr⧺tr') s3.
37
38lemma plus_not_final : ∀O,I,FE. ∀gl,s,tr,s'.
39  plus O I FE gl s tr s' →
40  is_final … FE gl s = None ?.
41#O #I #FE #gl #s0 #tr0 #s0' * //
42qed.
43
44let rec trace_map (A,B:Type[0]) (f:A → res (trace × B))
45                  (l:list A) on l : res (trace × (list B)) ≝
46match l with
47[ nil ⇒ OK ? 〈E0, [ ]〉
48| cons h t ⇒
49    do 〈tr,h'〉 ← f h;
50    do 〈tr',t'〉 ← trace_map … f t;
51    OK ? 〈tr ⧺ tr',h'::t'〉
52].
53
54(* A third version of making several steps (!)
55
56   The idea here is to have a computational definition of reducing serveral
57   steps then showing some property about the resulting trace and state.  By
58   careful use of let rec we can ensure that reduction stops in a sensible
59   way whenever the number of steps or the step currently being executed is
60   not (reducible to) a value.
61   
62   An invariant is also asserted on every state other than the initial one.
63
64   For example, we state a property to prove by something like
65
66     ∃n. after_n_steps n … clight_exec ge s inv (λtr,s'. <some property>)
67
68   then start reducing by giving the number of steps and reducing the
69   definition
70
71     %{3} whd
72
73   and then whenever the reduction gets stuck, the currently reducing step is
74   the third subterm, which we can reduce and unblock with (for example)
75   rewriting
76
77     whd in ⊢ (??%?); >EXe'
78
79   and at the end reduce with whd to get the property as the goal.
80
81   There are a few inversion-like results to get back the information contained in
82   the proof below, and other that provides all the steps in an inductive form
83   in Executions.ma.
84
85  *)
86
87record await_value_stuff : Type[2] ≝ {
88 avs_O : Type[0];
89 avs_I : avs_O → Type[0];
90 avs_exec : trans_system avs_O avs_I;
91 avs_g : global ?? avs_exec;
92 avs_inv : state ?? avs_exec avs_g → bool
93}.
94
95let rec await_value (avs:await_value_stuff)
96 (v:IO (avs_O avs) (avs_I avs) (trace × (state ?? (avs_exec avs) (avs_g avs))))
97 (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) on v : Prop ≝
98match v with
99[ Value ts ⇒ P (\fst ts) (\snd ts)
100| _ ⇒ False
101].
102
103let rec assert (b:bool) (P:Prop) on b ≝
104if b then P else False.
105
106let rec after_aux (avs:await_value_stuff)
107  (n:nat) (s:state ?? (avs_exec avs) (avs_g avs)) (tr:trace)
108  (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop)
109on n : Prop ≝
110match n with
111[ O ⇒ P tr s
112| S n' ⇒
113  match is_final … s with
114  [ None ⇒
115    await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s.
116      assert (avs_inv avs s) (after_aux avs n' s (tr ⧺ tr') P))
117  | _ ⇒ False
118  ]
119].
120
121definition after_n_steps : nat →
122 ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec.
123 state ?? exec g →
124 (state ?? exec g → bool) →
125 (trace → state ?? exec g → Prop) → Prop ≝
126λn,O,I,exec,g,s,inv,P. after_aux (mk_await_value_stuff O I exec g inv) n s E0 P.
127
128lemma after_aux_covariant : ∀avs,P,Q,tr'.
129  (∀tr,s. P (tr'⧺tr) s → Q tr s) →
130  ∀n,s,tr.
131  after_aux avs n s (tr'⧺tr) P →
132  after_aux avs n s tr Q.
133#avs #P #Q #tr' #H #n elim n
134[ normalize /2/
135| #n' #IH #s #tr
136  whd in ⊢ (% → %); cases (is_final … s) [ 2: #x * ]
137  whd in ⊢ (% → %);
138  cases (step … s) [1,3: normalize /2/ ]
139  * #tr'' #s''
140  whd in ⊢ (% → %);
141  cases (avs_inv avs s'') [ 2: * ]
142  whd in ⊢ (% → %);
143  >Eapp_assoc @IH
144] qed.
145
146lemma after_n_covariant : ∀n,O,I,exec,g,P,inv,Q.
147  (∀tr,s. P tr s → Q tr s) →
148  ∀s.
149  after_n_steps n O I exec g s inv P →
150  after_n_steps n O I exec g s inv Q.
151normalize /3/
152qed.
153
154(* for joining a couple of these together *)
155
156lemma after_n_m : ∀n,m,O,I,exec,g,inv,P,Q,s,s'.
157  after_n_steps m O I exec g s' inv Q →
158  after_n_steps n O I exec g s inv (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) →
159  after_n_steps (n+m) O I exec g s inv P.
160#n #m #O #I #exec #g #inv #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n
161[ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2
162  whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %;
163  generalize in match s; -s
164  elim m
165  [ #s #tr' whd in ⊢ (% → %); @H2
166  | #m' #IH #s #tr' whd in ⊢ (% → %);
167    cases (is_final … s) [2: #r * ]
168    whd in ⊢ (% → %);
169    cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %);
170    cases (inv s'') [2: * ]
171    >Eapp_assoc @IH ]
172| #n' #IH #tr #s #s' #H whd in ⊢ (% → %);
173  cases (is_final … s) [2: #r * ]
174  whd in ⊢ (% → %);
175  cases (step O I exec g s) [1,3: normalize // ]
176  * #tr1 #s1 whd in ⊢ (% → %);
177  cases (inv s1) [2:*]
178  @IH @H
179] qed.
180
181(* Inversion lemmas. *)
182
183lemma after_1_of_n_steps : ∀n,O,I,exec,g,inv,P,s.
184  after_n_steps (S n) O I exec g s inv P →
185  ∃tr,s'.
186  is_final … exec g s = None ? ∧
187  step … exec g s = Value … 〈tr,s'〉 ∧
188  bool_to_Prop (inv s') ∧
189  after_n_steps n O I exec g s' inv (λtr'',s''. P (tr⧺tr'') s'').
190#n #O #I #exec #g #inv #P #s
191whd in ⊢ (% → ?);
192cases (is_final … s)
193[ whd in ⊢ (% → ?);
194  cases (step … s)
195  [ #o #k *
196  | * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr) #AFTER
197    %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % /3/ cases AFTER
198  | #m *
199  ]
200| #r *
201] qed.
202
203lemma after_1_step : ∀O,I,exec,g,inv,P,s.
204  after_n_steps 1 O I exec g s inv P →
205  ∃tr,s'. is_final … exec g s = None ? ∧
206    step ?? exec g s = Value … 〈tr,s'〉 ∧
207    bool_to_Prop (inv s') ∧ P tr s'.
208#O #I #exec #g #inv #P #s #AFTER
209cases (after_1_of_n_steps … AFTER)
210#tr * #s' * * * #NF #STEP #INV #FIN %{tr} %{s'} % [%[%]] // whd in FIN; >E0_right in FIN; //
211qed.
212
213(* A typical way to use the following:
214
215   With a hypothesis
216     EX : after_n_steps n ... (State ...) ...
217   reduce it [whd in EX;] to
218     EX : await_value ...
219   then perform inversion
220   [cases (await_value_bind_inv … EX) -EX * #x * #E1 #EX]
221      x : T
222     E1 : f = return x
223     EX : await_value ...
224 *)
225
226lemma await_value_bind_inv : ∀avs,T,f,g,P.
227  await_value avs (m_bind … f g) P →
228  ∃x:T. (f = return x) ∧ await_value avs (g x) P.
229#avs #T *
230[ #o #k #g #P *
231| #x #g #P #AWAIT %{x} % //
232| #m #g #P *
233] qed.
234
235(* A (possibly non-terminating) execution.   *)
236coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
237| e_stop : trace → int → state → execution state output input
238| e_step : trace → state → execution state output input → execution state output input
239| e_wrong : errmsg → execution state output input
240| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
241
242(* This definition is slightly awkward because of the need to provide resumptions.
243   It records the last trace/state passed in, then recursively processes the next
244   state. *)
245
246let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
247                       (exec:trans_system output input) (g:global ?? exec)
248                       (s:IO output input (trace×(state ?? exec g)))
249                       : execution ??? ≝
250match s with
251[ Wrong m ⇒ e_wrong ??? m
252| Value v ⇒ let 〈t,s'〉 ≝ v in
253    match is_final ?? exec g s' with
254    [ Some r ⇒ e_stop ??? t r s'
255    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
256| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
257].
258
259lemma execution_cases: ∀o,i,s.∀e:execution s o i.
260 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
261 | e_step tr s e ⇒ e_step ??? tr s e
262 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
263#o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E %
264 | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto
265  here, used reflexivity instead *)
266
267axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
268match s with
269[ Wrong m ⇒ e_wrong ??? m
270| Value v ⇒ let 〈t,s'〉 ≝ v in
271    match is_final ?? exec g s' with
272    [ Some r ⇒ e_stop ??? t r s'
273    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
274| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
275].
276(*
277#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
278[ #o #k
279| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
280| ]
281whd in ⊢ (??%%); //;
282qed.
283*)
284
285lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
286  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
287  step … ge s = Value … 〈tr, s'〉 ∧
288  is_final … s' = Some ? r.
289#O #I #TS #ge #s #s' #tr #r
290>exec_inf_aux_unfold
291cases (step … ge s)
292[ 1,3: normalize #H1 #H2 try #H3 destruct
293| * #tr' #s''
294  whd in ⊢ (??%? → ?);
295  lapply (refl ? (is_final … s''))
296  cases (is_final … s'') in ⊢ (???% → %);
297  [ #_ whd in ⊢ (??%? → ?); #E destruct
298  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
299  ]
300] qed.
301
302lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
303  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
304  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
305#O #I #TS #ge #s #s' #tr #e
306>exec_inf_aux_unfold
307cases (step … s)
308[ 1,3: normalize #H1 #H2 try #H3 destruct
309| * #tr' #s''
310  whd in ⊢ (??%? → ?);
311  cases (is_final … s'')
312  [ #E normalize in E; destruct /2/
313  | #r #E normalize in E; destruct
314  ]
315] qed.
316
317lemma extract_interact : ∀O,I,TS,ge,s,o,k.
318  exec_inf_aux O I TS ge (step … ge s) = e_interact … o k →
319  ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)).
320#O #I #TS #ge #s #o #k >exec_inf_aux_unfold
321cases (step … s)
322[ #o' #k' normalize #E destruct %{k'} /2/
323| * #x #y normalize cases (is_final ?????) normalize
324  #X try #Y destruct
325| normalize #m #E destruct
326] qed.
327
328lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
329  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
330  is_final … s' = None ?.
331#O #I #TS #ge #s #s' #tr #e
332>exec_inf_aux_unfold
333cases (step … s)
334[ 1,3: normalize #H1 #H2 try #H3 destruct
335| * #tr' #s''
336  whd in ⊢ (??%? → ?);
337  lapply (refl ? (is_final … s''))
338  cases (is_final … s'') in ⊢ (???% → %);
339  [ #F whd in ⊢ (??%? → ?); #E destruct @F
340  | #r' #_ #E whd in E:(??%?);  destruct
341  ]
342] qed.
343
344
345
346record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
347{ program : Type[0]
348; es1 :> trans_system outty inty
349; make_global : program → global ?? es1
350; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
351}.
352
353definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
354λo,i,fx,p.
355  match make_initial_state ?? fx p with
356  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
357  | Error m ⇒ e_wrong ??? m
358  ].
359
360
361
362
363definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).
364
365let rec split_trace O I (state:Type[0]) (x:execution state O I) (n:nat) on n : option (execution_prefix state × (execution state O I)) ≝
366match n with
367[ O ⇒ Some ? 〈[ ], x〉
368| S n' ⇒
369  match x with
370  [ e_step tr s x' ⇒
371    ! 〈pre,x''〉 ← split_trace ?? state x' n';
372    Some ? 〈〈tr,s〉::pre,x''〉
373    (* Necessary for a measurable trace at the end of the program *)
374  | e_stop tr r s ⇒
375    match n' with
376    [ O ⇒ Some ? 〈[〈tr,s〉], x〉
377    | _ ⇒ None ?
378    ]
379  | _ ⇒ None ?
380  ]
381].
382
383(* For now I'm doing this without I/O, to keep things simple.  In the place I
384   intend to use it (the definition of measurable subtraces, and proofs using
385   that) I should allow I/O for the prefix. *)
386
387let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (trace × (state … fx g)) × (state … fx g)) ≝
388match n with
389[ O ⇒ return 〈[ ], s〉
390| S m ⇒
391  match is_final … fx g s with
392  [ Some r ⇒ Error … (msg TerminatedEarly)
393  | None ⇒
394    match step … fx g s with
395    [ Value trs ⇒
396        ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs);
397        return 〈trs::tl, s'〉
398    | Interact _ _ ⇒ Error … (msg UnexpectedIO)
399    | Wrong m ⇒ Error … m
400    ]
401  ]
402].
403
404(* Show that it's nice. *)
405
406lemma exec_steps_S : ∀O,I,fx,g,n,s,trace,s''.
407  exec_steps (S n) O I fx g s = OK … 〈trace,s''〉 →
408  is_final … fx g s = None ? ∧
409  ∃tr',s',tl.
410    trace = 〈tr',s'〉::tl ∧
411    step … fx g s = Value … 〈tr',s'〉 ∧
412    exec_steps n O I fx g s' = OK … 〈tl,s''〉.
413#O #I #fx #g #n #s #trace #s''
414whd in ⊢ (??%? → ?);
415cases (is_final … s)
416[ whd in ⊢ (??%? → ?);
417  cases (step … s)
418  [ #o #i #EX whd in EX:(??%?); destruct
419  | * #tr' #s' whd in ⊢ (??%? → ?); #EX %{(refl ??)}
420    %{tr'} %{s'} cases (exec_steps … g s') in EX ⊢ %;
421    [ * #tl #s'' #EX whd in EX:(??%?); destruct %{tl} /3/
422    | #m #EX whd in EX:(??%?); destruct
423    ]
424  | #m #EX whd in EX:(??%?); destruct
425  ]
426| #r #EX whd in EX:(??%?); destruct
427] qed.
428
429lemma exec_steps_length : ∀O,I,fx,g,n,s,trace,s'.
430  exec_steps n O I fx g s = OK … 〈trace,s'〉 →
431  n = |trace|.
432#O #I #fx #g #n elim n
433[ #s #trace #s' #EX whd in EX:(??%?); destruct %
434| #m #IH #s #trace #s' #EX
435  cases (exec_steps_S … EX) #notfinal * #tr' * #s'' * #tl * * #Etl #Estep #steps
436  >(IH … steps) >Etl %
437] qed.
438
439lemma exec_steps_nonterm : ∀O,I,fx,g,n,s,h,t,s'.
440  exec_steps n O I fx g s = OK … 〈h::t,s'〉 →
441  is_final … s = None ?.
442#O #I #fx #g #n #s #h #t #s' #EX
443lapply (exec_steps_length … EX)
444#Elen destruct whd in EX:(??%?);
445cases (is_final … s) in EX ⊢ %;
446[ //
447| #r #EX whd in EX:(??%?); destruct
448] qed.
449
450lemma exec_steps_nonterm' : ∀O,I,fx,g,n,s,h,t,s'.
451  exec_steps n O I fx g s = OK … 〈h@[t], s'〉 →
452  is_final … s = None ?.
453#O #I #fx #g #n #s * [2: #h1 #h2] #t #s' @exec_steps_nonterm
454qed.
455
456let rec gather_trace S (l:list (trace × S)) on l : trace ≝
457match l with
458[ nil ⇒ E0
459| cons h t ⇒ (\fst h)⧺(gather_trace S t)
460].
461
462lemma exec_steps_after_n_simple : ∀n,O,I,fx,g,s,trace,s'.
463  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
464  after_n_steps n O I fx g s (λ_. true) (λtr,s''. 〈tr,s''〉 = 〈gather_trace ? trace,s'〉).
465#n elim n
466[ #O #I #fx #g #s #trace #s' #EXEC whd in EXEC:(??%?); destruct
467  whd %
468| #m #IH #O #I #fx #g #s #trace #s' #EXEC
469  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
470  @(after_n_m 1 … (IH … STEPS))
471  whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #E destruct %
472] qed.
473
474lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P.
475  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
476  all … (λts. inv (\snd ts)) trace →
477  P (gather_trace ? trace) s' →
478  after_n_steps n O I fx g s inv P.
479#n elim n
480[ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct
481  #ALL #p whd @p
482| #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC
483  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
484  destruct
485  #ALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all … (λts. inv (\snd ts)) tl))
486  [ whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/ ] * #i1 #itl
487  #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?))
488  [ @p
489  | whd >NOTFINAL whd >STEP whd >i1 whd %{(refl ??)} #tr'' #s'' #p' @p'
490  ]
491] qed.
492
493lemma exec_steps_after_n_noinv : ∀n,O,I,fx,g,s,trace,s',P.
494  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
495  P (gather_trace ? trace) s' →
496  after_n_steps n O I fx g s (λ_.true) P.
497#n #O #I #fx #g #s #trace #s' #P #EXEC #p
498@(exec_steps_after_n … EXEC) //
499elim trace /2/
500qed.
501
502lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P.
503  after_n_steps n O I fx g s inv P →
504  ∃trace,s'. exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ P (gather_trace ? trace) s'.
505#n elim n
506[ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} %{(refl ??)} @AFTER
507| #m #IH #O #I #fx #g #s #inv #P #AFTER
508  cases (after_1_of_n_steps … AFTER)
509  #tr1 * #s1 * * * #NF #STEP #INV #AFTER'
510  cases (IH … AFTER')
511  #tl * #s' * #STEPS #p
512  %{(〈tr1,s1〉::tl)} %{s'} %
513  [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS % | // ]
514] qed.
515
516lemma exec_steps_split : ∀n,m,O,I,fx,g,s,trace,s'.
517  exec_steps (n+m) O I fx g s = OK ? 〈trace,s'〉 →
518  ∃trace1,trace2,s1.
519    exec_steps n O I fx g s = OK ? 〈trace1,s1〉 ∧
520    exec_steps m O I fx g s1 = OK ? 〈trace2,s'〉 ∧   
521    trace = trace1 @ trace2.
522#n elim n
523[ #m #O #I #fx #g #s #trace #s' #EXEC
524  %{[ ]} %{trace} %{s} /3/
525| #n' #IH #m #O #I #fx #g #s #trace #s' #EXEC
526  cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC'
527  cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2
528  %{(〈tr',s'〉::trace1)} %{trace2} %{s1}
529  %
530  [ %
531    [ whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >EXEC1 %
532    | @EXEC2
533    ]
534  | destruct %
535  ]
536] qed.
537
538lemma exec_steps_join : ∀n,m,O,I,fx,g,s1,trace1,s2,trace2,s3.
539  exec_steps n O I fx g s1 = OK ? 〈trace1,s2〉 →
540  exec_steps m O I fx g s2 = OK ? 〈trace2,s3〉 →
541  exec_steps (n+m) O I fx g s1 = OK ? 〈trace1@trace2,s3〉.
542#n elim n
543[ #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2
544  whd in EXEC1:(??%?); destruct @EXEC2
545| #n' #IH #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2
546  cases (exec_steps_S … EXEC1) #NF * #tr' * #s' * #tl' * * #E1 #STEP #EXEC'
547  whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >(IH … EXEC' EXEC2)
548  destruct %
549] qed.
550
551(* Show that it corresponds to split_trace … (exec_inf …) *)
552
553lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'.
554  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
555  match is_final … s' with
556  [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈trace, exec_inf_aux … fx g (step … s')〉
557  | Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈trace, e_stop … tr' r s'〉
558  ].
559#O #I #fx #g #n elim n
560[ #s #trace #s' #EX whd in EX:(??%%); destruct
561  cases (is_final … s') [ % | #r %1 % ]
562| #m #IH #s #trace #s' #EX
563  cases (exec_steps_S … EX)
564  #notfinal * #tr'' * #s'' * #tl * * #Etrace #Estep #Esteps
565  cases tl in Etrace Esteps ⊢ %;
566  [ #E destruct #Esteps
567    lapply (exec_steps_length … Esteps) #Elen normalize in Elen; destruct
568    whd in Esteps:(??%?); destruct
569    >Estep
570    >exec_inf_aux_unfold normalize nodelta
571    cases (is_final … s')
572    [ %
573    | #r %2 %{tr''} %
574    ]
575  | * #tr1 #s1 #tl1 #E normalize in E; destruct #Esteps
576    lapply (IH … Esteps) cases (is_final … s')
577    [ normalize nodelta #IH' >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
578      >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' %
579    | normalize nodelta #r *
580      [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct
581      | * #tr'' #IH' %2 %{tr''} >Estep >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
582        >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' %
583      ]
584    ]
585  ]
586] qed.
Note: See TracBrowser for help on using the repository browser.