source: src/common/SmallstepExec.ma @ 2669

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

Tweak exec_steps output; show that simulations extend to measurable
subtrace prefixes.

File size: 21.0 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   
387   If the execution has the form
388   
389     s1 -tr1→ s2 -tr2→ … sn -trn→ s'
390   
391   then the function returns
392   
393     〈[〈s1,tr1〉; 〈s2,tr2〉; …; 〈sn,trn〉], s'〉
394   *)
395
396let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (state … fx g × trace) × (state … fx g)) ≝
397match n with
398[ O ⇒ return 〈[ ], s〉
399| S m ⇒
400  match is_final … fx g s with
401  [ Some r ⇒ Error … (msg TerminatedEarly)
402  | None ⇒
403    match step … fx g s with
404    [ Value trs ⇒
405        ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs);
406        return 〈〈s, \fst trs〉::tl, s'〉
407    | Interact _ _ ⇒ Error … (msg UnexpectedIO)
408    | Wrong m ⇒ Error … m
409    ]
410  ]
411].
412
413(* Show that it's nice. *)
414
415lemma exec_steps_S : ∀O,I,fx,g,n,s,trace,s''.
416  exec_steps (S n) O I fx g s = OK … 〈trace,s''〉 →
417  is_final … fx g s = None ? ∧
418  ∃tr',s',tl.
419    trace = 〈s,tr'〉::tl ∧
420    step … fx g s = Value … 〈tr',s'〉 ∧
421    exec_steps n O I fx g s' = OK … 〈tl,s''〉.
422#O #I #fx #g #n #s #trace #s''
423whd in ⊢ (??%? → ?);
424cases (is_final … s)
425[ whd in ⊢ (??%? → ?);
426  cases (step … s)
427  [ #o #i #EX whd in EX:(??%?); destruct
428  | * #tr' #s' whd in ⊢ (??%? → ?); #EX %{(refl ??)}
429    %{tr'} %{s'} cases (exec_steps … g s') in EX ⊢ %;
430    [ * #tl #s'' #EX whd in EX:(??%?); destruct %{tl} /3/
431    | #m #EX whd in EX:(??%?); destruct
432    ]
433  | #m #EX whd in EX:(??%?); destruct
434  ]
435| #r #EX whd in EX:(??%?); destruct
436] qed.
437
438lemma exec_steps_length : ∀O,I,fx,g,n,s,trace,s'.
439  exec_steps n O I fx g s = OK … 〈trace,s'〉 →
440  n = |trace|.
441#O #I #fx #g #n elim n
442[ #s #trace #s' #EX whd in EX:(??%?); destruct %
443| #m #IH #s #trace #s' #EX
444  cases (exec_steps_S … EX) #notfinal * #tr' * #s'' * #tl * * #Etl #Estep #steps
445  >(IH … steps) >Etl %
446] qed.
447
448lemma exec_steps_nonterm : ∀O,I,fx,g,n,s,h,t,s'.
449  exec_steps n O I fx g s = OK … 〈h::t,s'〉 →
450  is_final … s = None ?.
451#O #I #fx #g #n #s #h #t #s' #EX
452lapply (exec_steps_length … EX)
453#Elen destruct whd in EX:(??%?);
454cases (is_final … s) in EX ⊢ %;
455[ //
456| #r #EX whd in EX:(??%?); destruct
457] qed.
458
459lemma exec_steps_nonterm' : ∀O,I,fx,g,n,s,h,t,s'.
460  exec_steps n O I fx g s = OK … 〈h@[t], s'〉 →
461  is_final … s = None ?.
462#O #I #fx #g #n #s * [2: #h1 #h2] #t #s' @exec_steps_nonterm
463qed.
464
465let rec gather_trace S (l:list (S × trace)) on l : trace ≝
466match l with
467[ nil ⇒ E0
468| cons h t ⇒ (\snd h)⧺(gather_trace S t)
469].
470
471lemma exec_steps_after_n_simple : ∀n,O,I,fx,g,s,trace,s'.
472  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
473  after_n_steps n O I fx g s (λ_. true) (λtr,s''. 〈tr,s''〉 = 〈gather_trace ? trace,s'〉).
474#n elim n
475[ #O #I #fx #g #s #trace #s' #EXEC whd in EXEC:(??%?); destruct
476  whd %
477| #m #IH #O #I #fx #g #s #trace #s' #EXEC
478  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
479  @(after_n_m 1 … (IH … STEPS))
480  whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #E destruct %
481] qed.
482
483lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P.
484  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
485  all ? (λstr. inv (\fst str)) (tail … trace) →
486  inv s' →
487  P (gather_trace ? trace) s' →
488  after_n_steps n O I fx g s inv P.
489#n elim n
490[ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct
491  #ALL #FI #p whd @p
492| #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC
493  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
494  destruct
495  #ALL #FALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all ? (λst. inv (\fst st)) (tail … tl)))
496  [ cases m in STEPS;
497    [ whd in ⊢ (??%? → ?); #E destruct /2/
498    | #m' #STEPS cases (exec_steps_S … STEPS) #_ * #tr'' * #s'' * #tl'' * * #E #_ #_ destruct
499      whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/
500    ]
501  ] * #i1 #itl
502  #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ??))
503  [ @p
504  | @FALL
505  | whd >NOTFINAL whd >STEP whd >i1 whd %{(refl ??)} #tr'' #s'' #p' @p'
506  ]
507] qed.
508
509lemma exec_steps_after_n_noinv : ∀n,O,I,fx,g,s,trace,s',P.
510  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
511  P (gather_trace ? trace) s' →
512  after_n_steps n O I fx g s (λ_.true) P.
513#n #O #I #fx #g #s #trace #s' #P #EXEC #p
514@(exec_steps_after_n … EXEC) //
515cases trace // #x #trace'
516elim trace' /2/
517qed.
518
519lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P.
520  after_n_steps n O I fx g s inv P →
521  ∃trace,s'. exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧ P (gather_trace ? trace) s'.
522#n elim n
523[ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} %{(refl ??)} @AFTER
524| #m #IH #O #I #fx #g #s #inv #P #AFTER
525  cases (after_1_of_n_steps … AFTER)
526  #tr1 * #s1 * * * #NF #STEP #INV #AFTER'
527  cases (IH … AFTER')
528  #tl * #s' * #STEPS #p
529  %{(〈s,tr1〉::tl)} %{s'} %
530  [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS % | // ]
531] qed.
532
533lemma exec_steps_split : ∀n,m,O,I,fx,g,s,trace,s'.
534  exec_steps (n+m) O I fx g s = OK ? 〈trace,s'〉 →
535  ∃trace1,trace2,s1.
536    exec_steps n O I fx g s = OK ? 〈trace1,s1〉 ∧
537    exec_steps m O I fx g s1 = OK ? 〈trace2,s'〉 ∧   
538    trace = trace1 @ trace2.
539#n elim n
540[ #m #O #I #fx #g #s #trace #s' #EXEC
541  %{[ ]} %{trace} %{s} /3/
542| #n' #IH #m #O #I #fx #g #s #trace #s' #EXEC
543  cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC'
544  cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2
545  %{(〈s,tr'〉::trace1)} %{trace2} %{s1}
546  %
547  [ %
548    [ whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >EXEC1 %
549    | @EXEC2
550    ]
551  | destruct %
552  ]
553] qed.
554
555lemma exec_steps_join : ∀n,m,O,I,fx,g,s1,trace1,s2,trace2,s3.
556  exec_steps n O I fx g s1 = OK ? 〈trace1,s2〉 →
557  exec_steps m O I fx g s2 = OK ? 〈trace2,s3〉 →
558  exec_steps (n+m) O I fx g s1 = OK ? 〈trace1@trace2,s3〉.
559#n elim n
560[ #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2
561  whd in EXEC1:(??%?); destruct @EXEC2
562| #n' #IH #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2
563  cases (exec_steps_S … EXEC1) #NF * #tr' * #s' * #tl' * * #E1 #STEP #EXEC'
564  whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >(IH … EXEC' EXEC2)
565  destruct %
566] qed.
567
568lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'.
569  exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 →
570  s = s1.
571#n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC
572lapply (exec_steps_length … EXEC) #E normalize in E; destruct
573cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct
574%
575qed.
576
577(* Show that it corresponds to split_trace … (exec_inf …).
578   We need to adjust the form of trace. *)
579
580let rec switch_trace_aux S tr (l:list (S × trace)) (s':S) on l : list (trace × S) ≝
581match l with
582[ nil ⇒ [〈tr,s'〉]
583| cons h t ⇒ 〈tr,\fst h〉::(switch_trace_aux S (\snd h) t s')
584].
585
586definition switch_trace ≝
587λS,l,s'. match l with
588[ nil ⇒ nil ?
589| cons h t ⇒ switch_trace_aux S (\snd h) t s'
590].
591
592lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'.
593  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
594  match is_final … s' with
595  [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', exec_inf_aux … fx g (step … s')〉
596  | Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', e_stop … tr' r s'〉
597  ].
598#O #I #fx #g #n elim n
599[ #s #trace #s' #EX whd in EX:(??%%); destruct
600  cases (is_final … s') [ % | #r %1 % ]
601| #m #IH #s #trace #s' #EX
602  cases (exec_steps_S … EX)
603  #notfinal * #tr'' * #s'' * #tl * * #Etrace #Estep #Esteps
604  cases tl in Etrace Esteps ⊢ %;
605  [ #E destruct #Esteps
606    lapply (exec_steps_length … Esteps) #Elen normalize in Elen; destruct
607    whd in Esteps:(??%?); destruct
608    >Estep
609    >exec_inf_aux_unfold normalize nodelta
610    cases (is_final … s')
611    [ whd %
612    | #r %2 %{tr''} %
613    ]
614  | * #s1 #tr1 #tl1 #E normalize in E; destruct #Esteps
615    lapply (IH … Esteps) cases (is_final … s')
616    [ normalize nodelta #IH' >Estep <(exec_steps_first … Esteps)
617      >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
618      >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' normalize nodelta %
619    | normalize nodelta #r *
620      [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct
621      | * #tr'' #IH' %2 %{tr''} >Estep <(exec_steps_first … Esteps)
622        >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
623        >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' %
624      ]
625    ]
626  ]
627] qed.
Note: See TracBrowser for help on using the repository browser.