source: src/Clight/CexecEquiv.ma @ 702

Last change on this file since 702 was 702, checked in by campbell, 9 years ago

Refine small-step executable semantics abstraction a little.
Some progress on using the new definition in CexecEquiv?, but only partial
because of over-eager normalisation by the destruct tactic.
Whole program semantics for RTLabs using it.

File size: 40.0 KB
Line 
1include "Clight/CexecComplete.ma".
2include "Clight/CexecSound.ma".
3include "utilities/extralib.ma".
4
5include "basics/jmeq.ma".
6
7(* A "single execution" - where all of the input values are made explicit. *)
8coinductive s_execution : Type[0] ≝
9| se_stop : trace → int → mem → s_execution
10| se_step : trace → state → s_execution → s_execution
11| se_wrong : s_execution
12| se_interact : ∀o:io_out. (io_in o → execution state io_out io_in) → io_in o → s_execution → s_execution.
13
14coinductive single_exec_of : execution state io_out io_in → s_execution → Prop ≝
15| seo_stop : ∀tr,r,m. single_exec_of (e_stop ??? tr r m) (se_stop tr r m)
16| seo_step : ∀tr,s,e,se.
17    single_exec_of e se →
18    single_exec_of (e_step ??? tr s e) (se_step tr s se)
19| seo_wrong : single_exec_of (e_wrong ???) se_wrong
20| seo_interact : ∀o,k,i,se.
21    single_exec_of (k i) se →
22    single_exec_of (e_interact ??? o k) (se_interact o k i se).
23
24(* starting after state s, zero or more steps of execution e reach state s'
25   after which comes e'. *)
26inductive execution_isteps : trace → state → s_execution → state → s_execution → Prop ≝
27| isteps_none : ∀s,e. execution_isteps E0 s e s e
28| isteps_one : ∀e,e',tr,tr',s,s',s0.
29    execution_isteps tr' s e s' e' →
30    execution_isteps (tr⧺tr') s0 (se_step tr s e) s' e'
31| isteps_interact : ∀e,e',o,k,i,s,s',s0,tr,tr'.
32    execution_isteps tr' s e s' e' →
33    execution_isteps (tr⧺tr') s0 (se_interact o k i (se_step tr s e)) s' e'.
34
35lemma isteps_trans: ∀tr1,tr2,s1,s2,s3,e1,e2,e3.
36  execution_isteps tr1 s1 e1 s2 e2 →
37  execution_isteps tr2 s2 e2 s3 e3 →
38  execution_isteps (tr1⧺tr2) s1 e1 s3 e3.
39#tr1 #tr2 #s1 #s2 #s3 #e1 #e2 #e3 #H1 elim H1;
40[ #s #e //;
41| #e #e' #tr #tr' #s1' #s2' #s3' #H1 #H2 #H3
42    >(Eapp_assoc …)
43    @isteps_one
44    @H2 @H3
45| #e #e' #o #k #i #s1' #s2' #s3' #tr #tr' #H1 #H2 #H3
46    >(Eapp_assoc …)
47    @isteps_interact
48    /2/
49] qed.
50
51lemma is_final_elim: ∀s.∀P:option int → Type[0].
52 (∀r. final_state s r → P (Some ? r)) →
53 ((¬∃r.final_state s r) → P (None ?)) →
54P (is_final clight_exec s).
55#s #P #F #NF whd in ⊢ (?%) cases (is_final_state s)
56[ * #r #FINAL @F @FINAL
57| #NOTFINAL @NF @NOTFINAL
58] qed.
59
60lemma exec_e_step: ∀ge,x,tr,s,e.
61  exec_inf_aux clight_exec ge x = e_step ??? tr s e →
62  exec_inf_aux clight_exec ge (exec_step ge s) = e.
63#ge #x #tr #s #e
64>(exec_inf_aux_unfold …) cases x;
65[ #o #k #EXEC whd in EXEC:(??%?); destruct
66| #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
67  @is_final_elim
68  [ #r #FINAL | #FINAL ]
69  (* Some trickery to prevent destruct normalizing clight_exec *)
70  #EXEC whd in EXEC:(??%?); [ @False_ind destruct |
71  cut (s = s') [ generalize in EXEC:(??(??????%)?) ⊢ ? #e0 #E destruct @refl ]
72  #Es <Es in EXEC #EXEC
73  generalize in EXEC:(??(??????%)?) ⊢ (??%?)
74  #e0 #E destruct @refl
75  ]
76| #EXEC whd in EXEC:(??%?); destruct
77] qed.
78
79lemma exec_e_step_inv: ∀ge,x,tr,s,e.
80  exec_inf_aux clight_exec ge x = e_step ??? tr s e →
81  x = Value ??? 〈tr,s〉.
82#ge #x #tr #s #e
83>(exec_inf_aux_unfold …) cases x;
84[ #o #k #EXEC whd in EXEC:(??%?); destruct
85| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
86  @is_final_elim
87  [ #r ] #FINAL #EXEC whd in EXEC:(??%?)
88  (* Again, prevent destruct blowing up *)
89  [ 2: generalize in EXEC:(??(??????%)?) ⊢ ? #e0 #EXEC ]
90  destruct;
91    @refl
92| #EXEC whd in EXEC:(??%?); destruct
93] qed.
94
95lemma exec_e_step_inv2: ∀ge,x,tr,s,e.
96  exec_inf_aux clight_exec ge x = e_step ??? tr s e →
97  ¬∃r.final_state s r.
98#ge #x #tr #s #e
99>(exec_inf_aux_unfold …) cases x;
100[ #o #k #EXEC whd in EXEC:(??%?); destruct
101| #y cases y; #tr' #s' whd in ⊢ (??%? → ?)
102  @is_final_elim [ #r #F #EXEC whd in EXEC:(??%?); destruct
103  | #F whd in ⊢ (??%? → ?) generalize in ⊢ (??(??????%)? → ?) #e0 #EXEC destruct  @F ]
104| #EXEC whd in EXEC:(??%?); destruct
105] qed.
106
107definition exec_from : genv → state → s_execution → Prop ≝
108λge,s,se. single_exec_of (exec_inf_aux clight_exec ge (exec_step ge s)) se.
109
110lemma se_step_eq : ∀tr,s,e,tr',s',e'.
111 se_step tr s e = se_step tr' s' e' →
112 tr = tr' ∧ s = s' ∧ e = e'.
113#tr #s #e #tr' #s' #e' #E
114(* destruct  This takes a hideous amount of time, not sure why. *)
115@(match E return λl.λ_. match l with [ se_step tr0 s0 e0 ⇒ tr = tr0 ∧ s = s0 ∧ e = e0 | _ ⇒ False ] with [ refl ⇒ ? ])
116whd % try % @refl qed.
117
118lemma exec_from_step : ∀ge,s,tr,s',e.
119exec_from ge s (se_step tr s' e) →
120exec_step ge s = Value ??? 〈tr,s'〉 ∧ exec_from ge s' e.
121#ge #s0 #tr0 #s0' #e0 #H inversion H;
122[ #tr #r #m #E1 #E2 destruct
123| #tr #s #e #se #H1 #H2 #E (*destruct (E);*)
124  lapply (se_step_eq … E) * * #E1 #E2 #E3 >E1 >E2 >E3
125    >(exec_e_step_inv … H2)
126    <(exec_e_step … H2) in H1 #H1 % //
127| #_ #E destruct
128| #o #k #i #se #H1 #H2 #E destruct
129] qed.
130
131axiom exec_from_interact : ∀ge,s,o,k,i,tr,s',e.
132exec_from ge s (se_interact o k i (se_step tr s' e)) →
133step ge s tr s' ∧
134(*exec_step ge s = Value ??? 〈tr,s'〉 ∧*) exec_from ge s' e.
135(*
136#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
137[ #tr #r #m #E1 #E2 destruct
138| #tr #s #e #se #H1 #H2 #E destruct (E)
139| #_ #E destruct
140| #o #k #i #se #H1 #H2 #E (*destruct (E);*)
141    lapply (exec_step_sound ge s0);
142    cases (exec_step ge s0) in H2 ⊢ %;
143    [ #o' #k' >(exec_inf_aux_unfold …)
144        #E' whd in E':(??%?); destruct (E');
145        #STEP
146        inversion H1;
147        [ #tr #r #m #E1 #E2 destruct
148        | #tr' #s' #e' #se' #H2 #H3 #E2 destruct (E2);
149            <(exec_e_step … H3) in H2 #H2 % //;
150            lapply (STEP i);
151            >(exec_e_step_inv … H3)
152            #S @S
153        | #_ #E destruct
154        | #o #k #i #se #H1 #H2 #E destruct
155        ]
156    | #x cases x; #tr' #s' >(exec_inf_aux_unfold …)
157        whd in ⊢ (??%? → ?); cases (is_final_state s');
158        #F #E whd in E:(??%?); destruct
159    | >(exec_inf_aux_unfold …)
160        #E' whd in E':(??%?); destruct (E');
161    ]
162] qed.*)
163
164axiom exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
165exec_from ge s (se_interact o k i (se_stop tr r m)) →
166step ge s tr (Returnstate (Vint r) Kstop m).
167(*
168#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
169[ #tr #r #m #E1 #E2 destruct
170| #tr #s #e #se #H1 #H2 #E destruct (E)
171| #_ #E destruct
172| #o #k #i #se #H1 #H2 #E destruct (E);
173    lapply (exec_step_sound ge s0);
174    >(exec_inf_aux_unfold …) in H2;
175    cases (exec_step ge s0);
176    [ #o' #k'
177        #E' whd in E':(??%?); destruct (E');
178        #STEP
179        inversion H1;
180        [ #tr #r #m #E1 #E2 lapply (STEP i); destruct;
181            >(exec_inf_aux_unfold …) in E1;
182            cases (k' i);
183            [ #o2 #k2 #E whd in E:(??%?); destruct (E)
184            | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
185                cases (is_final_state s2);
186                [ #F cases F; #r' #FINAL #E whd in E:(??%?);
187                    destruct (E);
188                    inversion FINAL;
189                    #r'' #m'' #E1 #E2 destruct (E1 E2); //;
190                | #NF #E whd in E:(??%?); destruct (E)
191                ]
192            | #E whd in E:(??%?); destruct (E)
193            ]
194       | #tr #s #e #e' #H #EXEC #E destruct (E)
195       | #EXEC #E destruct (E)
196       | #o2 #k2 #i2 #e2 #H #EXEC #E destruct (E)
197       ]
198   | #x cases x; #tr #s whd in ⊢ (??%? → ?);
199       cases (is_final_state s); #F #E whd in E:(??%?); destruct (E)
200   | #E whd in E:(??%?); destruct (E)
201   ]
202] qed.*)
203
204(* NB: the E0 in the execs are irrelevant. *)
205lemma several_steps: ∀ge,tr,e,e',s,s'.
206  execution_isteps tr s e s' e' →
207  exec_from ge s e →
208  star (mk_transrel … step) ge s tr s' ∧
209  exec_from ge s' e'.
210#ge #tr0 #e0 #e0' #s0 #s0' #H
211elim H;
212[ #s #e #EXEC % //;
213| #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #STEPS #IH #EXEC
214    elim (exec_from_step … EXEC); #EXEC3 #EXEC1
215    elim (IH EXEC1);
216    #STAR12 #EXEC2 % //;
217    lapply (exec_step_sound ge s3);
218    >EXEC3 #STEP3
219    @(star_step (mk_transrel ?? step) … STEP3 STAR12)
220    @refl
221| #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #STEPS #IH #EXEC
222    elim (exec_from_interact … EXEC);
223    #STEP3 #EXEC1
224    elim (IH EXEC1); #STAR #EXEC2
225    %
226    [ @(star_step (mk_transrel ?? step) … STEP3 STAR)
227        @refl
228    | //
229    ]
230] qed.
231
232inductive execution_terminates : trace → state → s_execution → int → mem → Prop ≝
233| terminates : ∀s,s',tr,tr',r,e,m.
234    execution_isteps tr s e s' (se_stop tr' r m) →
235    execution_terminates (tr⧺tr') s (se_step E0 s e) r m
236(* We should only be able to get to here if main is an external function, which is silly. *)
237| annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,m,o,k,i.
238    execution_isteps tr s e s' (se_interact o k i (se_stop tr' r m)) →
239    execution_terminates (tr⧺tr') s (se_step E0 s e) r m.
240
241coinductive execution_diverging : s_execution → Prop ≝
242| diverging_step : ∀s,e. execution_diverging e → execution_diverging (se_step E0 s e).
243
244(* Makes a finite number of interactions (including cost labels) before diverging. *)
245inductive execution_diverges : trace → state → s_execution → Prop ≝
246| diverges_diverging: ∀tr,s,s',e,e'.
247    execution_isteps tr s e s' e' →
248    execution_diverging e' →
249    execution_diverges tr s (se_step E0 s e).
250
251(* NB: "reacting" includes hitting a cost label. *)
252coinductive execution_reacting : traceinf → state → s_execution → Prop ≝
253| reacting: ∀tr,tr',s,s',e,e'.
254    execution_reacting tr' s' e' →
255    execution_isteps tr s e s' e' →
256    tr ≠ E0 →
257    execution_reacting (tr⧻tr') s e.
258
259inductive execution_reacts : traceinf → state → s_execution → Prop ≝
260| reacts: ∀tr,s,e.
261    execution_reacting tr s e →
262    execution_reacts tr s (se_step E0 s e).
263
264inductive execution_goes_wrong: trace → state → s_execution → state → Prop ≝
265| go_wrong: ∀tr,s,s',e.
266    execution_isteps tr s e s' se_wrong →
267    execution_goes_wrong tr s (se_step E0 s e) s'.
268
269let corec silent_sound ge s e
270  (H0:execution_diverging e)
271  (EXEC:exec_from ge s e)
272  : forever_silent (mk_transrel ?? step) … ge s ≝ ?.
273cut (∃s2.∃e2.And (And (execution_diverging e2) (step ge s E0 s2)) (exec_from ge s2 e2));
274[ cases H0 in EXEC ⊢ %; #s1 #e1 #H1 #EXEC
275    elim (exec_from_step … EXEC);
276    #EXEC0 #EXEC1
277    %{ s1} %{ e1} % //; % //;
278    lapply (exec_step_sound ge s); >EXEC0 whd in ⊢ (% → ?); #H @H
279| *; #s2 *; #e2 *; *; #H2 #STEP2 #EXEC2
280    @(forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 e2 ??))
281    //;
282] qed.
283
284axiom final_step: ∀ge,tr,r,m,s.
285  exec_from ge s (se_stop tr r m) →
286  step ge s tr (Returnstate (Vint r) Kstop m).
287  (*
288#ge #tr #r #m #s #EXEC
289whd in EXEC;
290inversion EXEC;
291[ #tr' #r' #m' #EXEC' #E destruct (E);
292    lapply (exec_step_sound ge s);
293    >(exec_inf_aux_unfold …) in EXEC';
294    cases (exec_step ge s);
295    [ #o #k #EXEC' whd in EXEC':(??%?); destruct (EXEC');
296    | #x cases x; #tr'' #s' whd in ⊢ (??%? → ?);
297        cases (is_final_state s'); #F [ 1: cases F; #r'' #FINAL ]
298        #EXEC' whd in EXEC':(??%?); destruct (EXEC');
299    | #EXEC' whd in EXEC':(??%?); destruct (EXEC');
300    ]
301    inversion FINAL; #r''' #m' #E1 #E2 #H destruct (E1 E2);
302    @H
303| #tr' #s' #e' #se' #H #EXEC' #E destruct
304| #EXEC' #E destruct
305| #o #k #i #e #H #EXEC #E destruct
306] qed.*)
307
308
309lemma e_stop_inv: ∀ge,x,tr,r,m.
310  exec_inf_aux clight_exec ge x = e_stop ??? tr r m →
311  x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉.
312#ge #x #tr #r #m
313>(exec_inf_aux_unfold …) cases x;
314[ #o #k #EXEC whd in EXEC:(??%?); destruct;
315| #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim
316  [ #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);
317      destruct (EXEC); @refl
318  | #F #EXEC whd in EXEC:(??%?); destruct (EXEC);
319  ]
320| #EXEC whd in EXEC:(??%?); destruct (EXEC);
321] qed.
322
323lemma terminates_sound: ∀ge,tr,s,r,m,e.
324  execution_terminates tr s (se_step E0 s e) r m →
325  exec_from ge s e →
326  star (mk_transrel … step) ge s tr (Returnstate (Vint r) Kstop m).
327#ge #tr0 #s0 #r #m #e0 #H inversion H;
328[ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC
329    destruct (E1 E2 E3 E4 E5);
330    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
331    @(star_right … STARs')
332    [ 2: @(final_step ge tr' r m s' … EXECs')
333    | skip
334    | @refl
335    ]
336| #s #s' #tr #tr' #r #e #m #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC
337    destruct;
338    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
339    @(star_right … STARs')
340    [ @tr'
341    | @(exec_from_interact_stop … EXECs')
342    | @refl
343    ]
344] qed.
345
346let corec reacts_sound ge tr s e
347  (REACTS:execution_reacting tr s e)
348  (EXEC:exec_from ge s e) :
349  forever_reactive (mk_transrel … step) ge s tr ≝ ?.
350cut (∃s'.∃e'.∃tr'.∃tr''.(And (And (And (execution_reacting tr'' s' e') (execution_isteps tr' s e s' e')) (tr' ≠ E0)) (tr = tr'⧻tr'')));
351[ inversion REACTS;
352    #tr0 #tr' #s0 #s' #e0 #e' #EREACTS #ESTEPS #REACTED #E1 #E2 #E3 destruct (E2 E3);
353    %{ s'} %{ e'} %{ tr0} %{ tr'} % [ % [ % //; | @REACTED ] | @refl ]
354| *; #s' *; #e' *; #tr' *; #tr''
355    *; *; *; #REACTS' #ESTEPS #REACTED #APPTR
356(*    >APPTR *)
357    @(match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ])
358    %
359    cases (several_steps … ESTEPS EXEC); #STEPS #EXEC'
360    [ 2: @STEPS
361    | skip
362    | @REACTED
363    | @reacts_sound
364      [ 2: @REACTS'
365      | skip
366      | @EXEC'
367      ]
368    ]
369qed.
370
371lemma exec_from_wrong: ∀ge,s.
372  exec_from ge s se_wrong →
373  exec_step ge s = Wrong ???.
374#ge #s #H whd in H;
375inversion H;
376[ #tr #r #m #EXEC #E destruct (E)
377| #tr #s' #e #e' #H #EXEC #E destruct (E)
378| >(exec_inf_aux_unfold …)
379    cases (exec_step ge s);
380  [ #o #k #EXEC whd in EXEC:(??%?); destruct
381  | #x cases x; #tr #s' whd in ⊢ (??%? → ?) @is_final_elim
382      [ #r ] #F #EXEC whd in EXEC:(??%?); destruct
383  | //
384  ]
385| #o #k #i #e #H #EXEC #E destruct
386] qed.
387
388lemma exec_from_step_notfinal: ∀ge,s,tr,s',e.
389  exec_from ge s (se_step tr s' e) →
390  ¬(∃r. final_state s' r).
391#ge #s #tr #s' #e #H whd in H; inversion H;
392[ #tr' #r #m #EXEC #E destruct
393| #tr' #s'' #e' #e'' #H #EXEC #E destruct (E);
394    >(exec_inf_aux_unfold …) in EXEC;
395    cases (exec_step ge s);
396    [ #o #k #EXEC whd in EXEC:(??%?); destruct
397    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim
398        [ #r ] #F #E whd in E:(??%?); [ destruct | generalize in E:(??(??????%)?) ⊢ ? #e0 #E destruct; @F ]
399    | #E whd in E:(??%?); destruct
400    ]
401| #EXEC #E destruct
402| #o #k #i #e' #H #EXEC #E destruct
403] qed.
404
405lemma exec_from_interact_step_notfinal: ∀ge,s,o,k,i,tr,s',e.
406  exec_from ge s (se_interact o k i (se_step tr s' e)) →
407  ¬(∃r. final_state s' r).
408#ge #s #o #k #i #tr #s' #e #H
409% *; #r #F cases F in H; #r' #m #H
410inversion H;
411[ #tr' #r #m #EXEC #E destruct
412| #tr' #s'' #e' #e'' #H #EXEC #E destruct (E);
413| #EXEC #E destruct
414| #o' #k' #i' #e' #H #EXEC #E destruct;
415    >(exec_inf_aux_unfold …) in EXEC;
416    cases (exec_step ge s);
417    [ #o1 #k1 #EXEC1 whd in EXEC1:(??%?); destruct (EXEC1);
418        inversion H;
419        [ #tr1 #r1 #m1 #EXECK #E destruct (E);
420        | #tr1 #s1 #e1 #e2 #H1 #EXECK #E destruct (E);
421            >(exec_inf_aux_unfold …) in EXECK;
422            cases (k1 i');
423            [ #o2 #k2 #EXECK whd in EXECK:(??%?); destruct
424            | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
425                cases (is_final_state s2); #F #EXECK
426                whd in EXECK:(??%?); destruct;
427                @(absurd ?? F)
428                %{ r'} //;
429            | #E whd in E:(??%?); destruct
430            ]
431        | #EXECK #E  whd in E:(??%?); destruct
432        | #o2 #k2 #i2 #e2 #H2 #EXECK #E destruct
433        ]
434    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?);
435        cases (is_final_state s1); #F #E whd in E:(??%?); destruct;
436    | #E whd in E:(??%?); destruct
437    ]
438] qed.
439
440lemma wrong_sound: ∀ge,tr,s,s',e.
441  execution_goes_wrong tr s (se_step E0 s e) s' →
442  exec_from ge s e →
443  (¬∃r. final_state s r) →
444  star (mk_transrel … step) ge s tr s' ∧
445  nostep (mk_transrel … step) ge s' ∧
446  (¬∃r. final_state s' r).
447#ge #tr0 #s0 #s0' #e0 #WRONG inversion WRONG;
448#tr #s #s' #e #ESTEPS #E1 #E2 #E3 #E4 #EXEC #NOTFINAL destruct (E1 E2 E3 E4);
449cases (several_steps … ESTEPS EXEC);
450#STAR #EXEC' %
451[ % [ @STAR
452       | #badtr #bads % #badSTEP
453           lapply (step_complete … badSTEP);
454           >(exec_from_wrong … EXEC')
455           //;
456       ]
457| %
458    elim ESTEPS in NOTFINAL EXEC ⊢ %;
459    [ #s1 #e1 #NF #EX #F @(absurd ? F NF)
460    | #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #ESTEPS1 #IH #NF #EXEC
461        cases (exec_from_step … EXEC); #EXEC3 #EXEC1
462        @(IH … EXEC1)
463        @(exec_from_step_notfinal … EXEC)
464    | #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #ESTEPS1 #IH #NF #EXEC
465        @IH
466        [ @(exec_from_interact_step_notfinal … EXEC)
467        | cases (exec_from_interact … EXEC); //;
468        ]
469    ]
470] qed.
471
472inductive execution_characterisation : state → s_execution → Prop ≝
473| ec_terminates: ∀s,r,m,e,tr.
474    execution_terminates tr s e r m →
475    execution_characterisation s e
476| ec_diverges: ∀s,e,tr.
477    execution_diverges tr s e →
478    execution_characterisation s e
479| ec_reacts: ∀s,e,tr.
480    execution_reacts tr s e →
481    execution_characterisation s e
482| ec_wrong: ∀e,s,s',tr.
483    execution_goes_wrong tr s e s' →
484    execution_characterisation s e.
485
486(* bit of a hack to avoid inability to reduce term in match *)
487definition interact_prop : ∀A:Type[0].(∀o:io_out. (io_in o → IO io_out io_in A) → Prop) → IO io_out io_in A → Prop ≝
488λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ].
489
490lemma err_does_not_interact: ∀A,B,P,e1,e2.
491  (∀x:B.interact_prop A P (e2 x)) →
492  interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2).
493#A #B #P #e1 #e2 #H
494cases e1; //; qed.
495
496lemma err2_does_not_interact: ∀A,B,C,P,e1,e2.
497  (∀x,y.interact_prop A P (e2 x y)) →
498  interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2).
499#A #B #C #P #e1 #e2 #H
500cases e1; [ #z cases z; ] //; qed.
501
502lemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2.
503  (∀x.interact_prop A P (e2 x)) →
504  interact_prop A P (bindIO ?? (Sig B Q) A (err_to_io_sig ??? Q e1) e2).
505#A #B #P #Q #e1 #e2 #H
506cases e1; //; qed.
507
508lemma opt_does_not_interact: ∀A,B,P,e1,e2.
509  (∀x:B.interact_prop A P (e2 x)) →
510  interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2).
511#A #B #P #e1 #e2 #H
512cases e1; //; qed.
513
514lemma exec_step_interaction:
515  ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s).
516#ge #s cases s;
517[ #f #st #kk #e #m cases st;
518  [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
519  [ 4,6,8,9: @I ]
520  whd in ⊢ (???%);
521  [ cases a; [ cases (fn_return f); //; | #e whd nodelta in ⊢ (???%);
522                    cases (type_eq_dec (fn_return f) Tvoid); #x //; @err2_does_not_interact // ]
523  | cases (find_label a (fn_body f) (call_cont kk)); [ @I | #z cases z #x #y @I ]
524  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I
525  | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
526  | @err2_does_not_interact #x1 #x2 cases x1; //;
527  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5  @err_does_not_interact #x6 cases a;
528      [ @I | #x7 @err2_does_not_interact #x8 #x9 @I ]
529  | cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
530      | @I ]
531  | cases kk; [ 1,8: cases (fn_return f); //; | 2,3,5,6,7: //;
532      | #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I ]
533  | cases kk; //;
534  | cases kk; [ 4: #z1 #z2 #z3  @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I
535      | *: // ]
536  ]
537| #f #args #kk #m cases f;
538  [ #f' whd in ⊢ (???%); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
539    #x1 #x2 whd in ⊢ (???%) @err_does_not_interact //
540  (* This is the only case that actually matters! *)
541  | #fn #argtys #rty whd in ⊢ (???%);
542      @err_does_not_interact #x1
543      whd; #i % [ 2: % [ 2: % [ % whd in ⊢ (??%?); @refl
544        | % #E whd in E:(??%%); destruct (E); ] ] ]
545  ]
546| #v #kk #m whd in ⊢ (???%); cases kk;
547    [ 8: #x1 #x2 #x3 #x4 cases x1;
548      [ whd in ⊢ (???%); cases v; // | #x5 whd in ⊢ (???%); cases x5;
549          #x6 #x7 @opt_does_not_interact // ]
550    | *: // ]
551] qed.
552
553
554(* Some classical logic (roughly like a fragment of Coq's library) *)
555lemma classical_doubleneg:
556  ∀classic:(∀P:Prop.P ∨ ¬P).
557  ∀P:Prop. ¬ (¬ P) → P.
558#classic #P *; #H
559cases (classic P);
560[ // | #H' @False_ind /2/; ]
561qed.
562
563lemma classical_not_all_not_ex:
564  ∀classic:(∀P:Prop.P ∨ ¬P).
565  ∀A:Type[0].∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x.
566#classic #A #P *; #H
567@(classical_doubleneg classic) % *; #H'
568@H #x % #H'' @H' %{x} @H''
569qed.
570
571lemma classical_not_all_ex_not:
572  ∀classic:(∀P:Prop.P ∨ ¬P).
573  ∀A:Type[0].∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x.
574#classic #A #P *; #H
575@(classical_not_all_not_ex classic A (λx.¬ P x))
576% #H' @H #x @(classical_doubleneg classic)
577@H'
578qed.
579
580lemma not_ex_all_not:
581  ∀A:Type[0].∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x.
582#A #P *; #H #x % #H'
583@H %{ x} @H'
584qed.
585
586lemma not_imply_elim:
587  ∀classic:(∀P:Prop.P ∨ ¬P).
588  ∀P,Q:Prop. ¬ (P → Q) → P.
589#classic #P #Q *; #H
590@(classical_doubleneg classic) % *; #H'
591@H #H'' @False_ind @H' @H''
592qed.
593
594lemma not_imply_elim2:
595  ∀P,Q:Prop. ¬ (P → Q) → ¬ Q.
596#P #Q *; #H % #H'
597@H #_ @H'
598qed.
599
600lemma imply_to_and:
601  ∀classic:(∀P:Prop.P ∨ ¬P).
602  ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q.
603#classic #P #Q #H %
604[ @(not_imply_elim classic P Q H)
605| @(not_imply_elim2 P Q H)
606] qed.
607
608lemma not_and_to_imply:
609  ∀classic:(∀P:Prop.P ∨ ¬P).
610  ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q.
611#classic #P #Q *; #H #H'
612% #H'' @H % //;
613qed.
614
615inductive execution_not_over : s_execution → Prop ≝
616| eno_step: ∀tr,s,e. execution_not_over (se_step tr s e)
617| eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)).
618
619lemma eno_stop: ∀tr,r,m. execution_not_over (se_stop tr r m) → False.
620#tr0 #r0 #m0 #H inversion H;
621[ #tr #s #e #E destruct
622| #o #k #tr #s #e #i #E destruct
623] qed.
624
625lemma eno_wrong: execution_not_over se_wrong → False.
626#H inversion H;
627[ #tr #s #e #E destruct
628| #o #k #tr #s #e #i #E destruct
629] qed.
630
631let corec show_divergence s e
632 (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
633                 execution_not_over e1)
634 (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0)
635 (CONTINUES:∀tr2,s2,o,k,i,e'. execution_isteps tr2 s e s2 (se_interact o k i e') → ∃tr3.∃s3.∃e3. And (e' = se_step tr3 s3 e3) (tr3 ≠ E0))
636 : execution_diverging e ≝ ?.
637lapply (NONTERMINATING E0 s e ?); //;
638cases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %;
639[ #tr #i #m #_ #_ #_ #ENO elim (eno_stop … ENO);
640| #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?);
641  [ <(E0_right tr) in ⊢ (?%????)
642      @isteps_one @isteps_none
643  | #TR @(match sym_eq ??? TR with [ refl ⇒ ? ]) (* >TR in UNREACTIVE ⊢ % *)
644      #NONTERMINATING #CONTINUES #_ %
645      @(show_divergence s')
646      [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1)
647        change in ⊢ (?%????) with (Eapp E0 tr1); @isteps_one
648        @S
649      | #tr2 #s2 #e2 #S >TR in UNREACTIVE #UNREACTIVE @(UNREACTIVE tr2 s2 e2)
650          change in ⊢ (?%????) with (Eapp E0 tr2);
651          @isteps_one @S
652      | #tr2 #s2 #o #k #i #e2 #S @(CONTINUES tr2 s2 o k i)
653          change in ⊢ (?%????) with (Eapp E0 tr2);
654          @(isteps_one … S)
655      ]
656  ]
657| #_ #_ #_ #ENO elim (eno_wrong … ENO);
658| #o #k #i #e' #UNREACTIVE #NONTERMINATING #CONTINUES #_
659    lapply (CONTINUES E0 s o k i e' (isteps_none …));
660    *; #tr' *; #s' *; #e' *; #EXEC #NOTSILENT
661    @False_ind @(absurd ?? NOTSILENT)
662    @(UNREACTIVE … s' e')
663    <(E0_right tr') in ⊢ (?%????)
664    >EXEC
665    @isteps_interact //;
666] qed.
667
668(* XXX == > jmeq notation and coercion *)
669
670lemma jmeq_to_eq : ∀A:Type[0].∀a,b:A.jmeq A a A b → a = b.
671#A #a #b #E @gral @jm_to_eq_sigma @E
672qed.
673
674coercion jmeq_to_eq : ∀A:Type[0].∀a,b:A.∀p:jmeq A a A b.a = b ≝
675  jmeq_to_eq on _p: jmeq ???? to eq ???.
676
677notation > "hvbox(a break ≃ b)"
678  non associative with precedence 45
679for @{ 'jmeq ? $a ? $b }.
680
681notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
682  non associative with precedence 45
683for @{ 'jmeq $t $a $u $b }.
684
685interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
686
687(* XXX < == *)
688
689lemma se_inv: ∀e1,e2.
690  single_exec_of e1 e2 →
691  match e1 with
692  [ e_stop tr r m ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ m = m' | _ ⇒ False ]
693  | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
694  | e_wrong ⇒ match e2 with [ se_wrong ⇒ True | _ ⇒ False ]
695  | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ]
696  ].
697#e01 #e02 #H
698cases H;
699[ #tr #r #m whd; % [ % ] //
700| #tr #s #e1' #e2' #H' whd; % [ % ] //
701| whd; //
702| #o #k #i #e #H' whd; % [ % ] //
703] qed.
704
705lemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
706  exec_from ge s (se_interact o k i (se_step tr s' e)) →
707  tr ≠ E0.
708#ge #o #k #i #tr #s #s' #e whd in ⊢ (% → ?); >(exec_inf_aux_unfold …)
709lapply (exec_step_interaction ge s);
710cases (exec_step ge s);
711[ #o' #k' ; whd in ⊢ (% → ?%? → ?); #H #K cases (se_inv … K);
712    *; #E1 #E2 #H1 destruct (E1);
713    lapply (H i); *; #tr' *; #s'' *; #K' #TR
714    >E2 in H1 #H1 whd in H1:(?%?); >K' in H1
715    >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?);
716    cases (is_final_state s'');
717    [ #F whd in ⊢ (?%? → ?); #S
718        @False_ind @(absurd ? S) cases (se_inv … S)
719    | #NF #S whd in S:(?%?); cases (se_inv … S);
720        *; #E1 #E2 #S' <E1 @TR
721    ]
722| #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?);
723    cases (is_final_state s''); #F #E whd in E:(?%?);
724    inversion E;
725    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
726    | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct
727    | 3,7: #E destruct
728    | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct
729    ]
730| #_ #E whd in E:(?%?);
731    inversion E;
732    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
733    | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct
734    | 3,7: #E1 #E2 destruct
735    | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct
736    ]
737] qed.
738
739let corec reactive_traceinf' ge s e
740  (EXEC:exec_from ge s e)
741  (REACTIVE: ∀tr,s1,e1.
742    execution_isteps tr s e s1 e1 →
743    (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)))
744  : traceinf' ≝ ?.
745lapply (REACTIVE E0 s e (isteps_none …));
746*; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H
747%{ tr ? H}
748@(reactive_traceinf' ge s' e' ?)
749[ cases (several_steps … STEPS EXEC); #_ #H' @H'
750| #tr1 #s1 #e1 #STEPS1
751    @REACTIVE
752    [ 2:
753        @(isteps_trans … STEPS STEPS1)
754    | skip
755    ]
756]
757qed.
758
759(* A slightly different version of the above, to work around a problem with the
760   next result. *)
761let corec reactive_traceinf'' ge s e
762  (EXEC:exec_from ge s e)
763  (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
764  (REACTIVE: ∀tr,s1,e1.
765    execution_isteps tr s e s1 e1 →
766    (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)))
767  : traceinf' ≝ ?.
768cases REACTIVE0; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H
769%{ tr ? H}
770@(reactive_traceinf'' ge s' e' ?)
771[ cases (several_steps … STEPS EXEC); #_ #H' @H'
772| @(REACTIVE … STEPS)
773| #tr1 #s1 #e1 #STEPS1
774    @REACTIVE
775    [ 2:
776        @(isteps_trans … STEPS STEPS1)
777    | skip
778    ]
779] qed.
780
781(* We want to prove
782
783lemma show_reactive : ∀ge,s.
784  ∀REACTIVE:∀tr,s1,e1.
785    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
786    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
787  execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)).
788 
789but the current matita won't unfold reactive_traceinf' so that we can do case
790analysis on (REACTIVE …).  Instead we take an "applied" version of REACTIVE that
791we can do case analysis on, then get it into the desired form afterwards.
792*)
793let corec show_reactive' ge s e
794  (EXEC:exec_from ge s e)
795  (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
796  (REACTIVE: ∀tr1,s1,e1.
797    execution_isteps tr1 s e s1 e1 →
798    (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)))
799  : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?.
800(*>(unroll_traceinf' (reactive_traceinf'' …)) *)
801@(match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ])
802cases REACTIVE0;
803#x cases x; #tr1 #y cases y; #s1 #e1 #z cases z; #STEPS #NOTSILENT
804whd in ⊢ (?(?%)??);
805(*>(traceinf_traceinfp_app …) *)
806@(match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ])
807@(reacting … STEPS NOTSILENT)
808@show_reactive'
809qed.
810
811lemma show_reactive : ∀ge,s,e.
812  ∀EXEC:exec_from ge s e.
813  ∀REACTIVE:∀tr,s1,e1.
814    execution_isteps tr s e s1 e1 →
815    (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)).
816  execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC ? REACTIVE)) s e.
817[ #ge #s #e #EXEC #REACTIVE
818    @show_reactive'
819| @(REACTIVE … (isteps_none …))
820] qed.
821
822lemma execution_characterisation_complete:
823  ∀classic:(∀P:Prop.P ∨ ¬P).
824  ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P).
825   ∀ge,s,e.
826   exec_from ge s e →
827   execution_characterisation s (se_step E0 s e).
828#classic #constructive_indefinite_description #ge #s #e #EXEC
829cases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
830                 execution_not_over e1));
831[ #NONTERMINATING
832    cases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧
833                     ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0));
834  [ *; #tr *; #s1 *; #e1 *; #INITIAL #UNREACTIVE
835      @(ec_diverges … s ? tr)
836      @(diverges_diverging … INITIAL)
837      @(show_divergence s1 e1)
838      [ #tr2 #s2 #e2 #S @(NONTERMINATING (Eapp tr tr2) s2 e2)
839          @(isteps_trans … INITIAL S)
840      | #tr2 #s2 #e2 #S @(UNREACTIVE … S)
841      | #tr2 #s2 #o #k #i #e2 #STEPS
842          lapply (NONTERMINATING (Eapp tr tr2) s2 (se_interact o k i e2) ?);
843          [ @(isteps_trans … INITIAL STEPS) ]
844          #NOTOVER inversion NOTOVER;
845          [ #tr' #s' #e' #E destruct (E);
846          | #o' #k' #tr' #s' #e' #i' #E destruct (E);
847              %{ tr'} %{s'} %{e'} % //;
848              cases (several_steps … INITIAL EXEC); #_ #EXEC1
849              cases (several_steps … STEPS EXEC1); #_ #EXEC2
850              @(interaction_is_not_silent … EXEC2)
851          ]
852      ]
853
854  | *; #NOTUNREACTIVE
855      cut (∀tr,s1,e1.execution_isteps tr s e s1 e1 →
856            ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0);
857      [ #tr #s1 #e1 #STEPS
858          @(classical_doubleneg classic) % #NOREACTION
859          @NOTUNREACTIVE
860          %{ tr} %{s1} %{e1} % //;
861          #tr2 #s2 #e2 #STEPS2
862          lapply (not_ex_all_not … NOREACTION); #NR1
863          lapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2
864          @(classical_doubleneg classic)
865          @NR2 normalize //
866      | #REACTIVE
867          @ec_reacts
868          [ 2: @reacts
869                   @(show_reactive ge s … EXEC)
870                   #tr #s1 #e1 #STEPS
871                   @constructive_indefinite_description
872                   @(REACTIVE … tr s1 e1 STEPS)
873          | skip
874          ]
875      ]
876  ]
877 
878| #NOTNONTERMINATING lapply (classical_not_all_ex_not classic … NOTNONTERMINATING);
879    *; #tr #NNT2 lapply (classical_not_all_ex_not classic … NNT2);
880    *; #s' #NNT3 lapply (classical_not_all_ex_not classic … NNT3);
881    *; #e #NNT4 elim (imply_to_and classic … NNT4);
882    cases e;
883    [ #tr' #r #m #STEPS #NOSTEP
884        @(ec_terminates s r m ? (Eapp tr tr')) %
885        [ @s'
886        | @STEPS
887        ]
888    | #tr' #s'' #e' #STEPS *; #NOSTEP @False_rect_Type0
889        @NOSTEP //
890    | #STEPS #NOSTEP
891        @(ec_wrong ? s s' tr) % //;
892    (* The following is stupidly complicated when most of the cases are impossible.
893       It ought to be simplified. *)
894    | #o #k #i #e' #STEPS #NOSTEP
895        cases e' in STEPS NOSTEP;
896        [ #tr' #r #m #STEPS #NOSTEP
897            @(ec_terminates s ???)
898           [ 4: @(annoying_corner_case_terminates … STEPS) ]
899        | #tr1 #s1 #e1 #STEPS *; #NOSTEP
900            @False_ind @NOSTEP //
901        | #STEPS #NOSTEP
902            lapply (exec_step_interaction ge s');
903            cases (several_steps … STEPS EXEC); #_
904            whd in ⊢ (% → ?);
905            >(exec_inf_aux_unfold …)
906            cases (exec_step ge s');
907            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
908                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2);
909                cases (H i); #tr1 *; #s1 *; #K #E >K in H2
910                >(exec_inf_aux_unfold …)
911                whd in ⊢ (?%? → ?); cases (is_final_state s1);
912                #F #S whd in S:(?%?); cases (se_inv … S);
913            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
914                cases (is_final_state s'); #F #S whd in S:(?%?);
915                cases (se_inv … S);
916            | #S cases (se_inv … S);
917            ]
918        | #o1 #k1 #i1 #e1 #STEPS #NOSTEP
919            lapply (exec_step_interaction ge s');
920            cases (several_steps … STEPS EXEC); #_
921            whd in ⊢ (% → ?);
922            >(exec_inf_aux_unfold …)
923            cases (exec_step ge s');
924            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
925                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2);
926                cases (H i); #tr1 *; #s1 *; #K #E >K in H2
927                >(exec_inf_aux_unfold …)
928                whd in ⊢ (?%? → ?); cases (is_final_state s1);
929                #F #S whd in S:(?%?); cases (se_inv … S);
930            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
931                cases (is_final_state s'); #F #S whd in S:(?%?);
932                cases (se_inv … S);
933            | #S cases (se_inv … S);
934            ]
935        ]
936    ]
937]
938qed.   
939
940inductive execution_matches_behavior: s_execution → program_behavior → Prop ≝
941| emb_terminates: ∀s,e,tr,r,m.
942    execution_terminates tr s e r m →
943    execution_matches_behavior e (Terminates tr r)
944| emb_diverges: ∀s,e,tr.
945    execution_diverges tr s e →
946    execution_matches_behavior e (Diverges tr)
947| emb_reacts: ∀s,e,tr.
948    execution_reacts tr s e →
949    execution_matches_behavior e (Reacts tr)
950| emb_wrong: ∀e,s,s',tr.
951    execution_goes_wrong tr s e s' →
952    execution_matches_behavior e (Goes_wrong tr)
953| emb_initially_wrong:
954    execution_matches_behavior se_wrong (Goes_wrong E0).
955
956lemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
957  execution_terminates tr s (se_step tr' s' e) r m → s = s'.
958#tr #tr' #s #s' #e #r #m #H inversion H;
959[ #s1 #s2 #tr1 #tr2 #r' #e' #m' #H' #E1 #E2 #E3 #E4 #E5 destruct; @refl
960| #s1 #s2 #tr1 #tr2 #r' #e' #m' #o #k #i #H' #E1 #E2 #E3 #E4 #E5 destruct; @refl
961] qed.
962
963lemma exec_state_diverges: ∀tr,tr',s,s',e.
964  execution_diverges tr s (se_step tr' s' e) → s = s'.
965#tr #tr' #s #s' #e #H inversion H;
966#tr1 #s1 #s2 #e1 #e2 #H' #E1 #E2 #E3 #E4 destruct; @refl qed.
967
968lemma exec_state_reacts: ∀tr,tr',s,s',e.
969  execution_reacts tr s (se_step tr' s' e) → s = s'.
970#tr #tr' #s #s' #e #H inversion H;
971#tr1 #s1 #e1 #H' #E1 #E2 #E3 destruct; @refl qed.
972
973lemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
974  execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'.
975#tr #tr' #s #s' #s'' #e #H inversion H;
976#tr1 #s1 #s2 #e1 #H' #E1 #E2 #E3 #E4 destruct; @refl qed.
977
978lemma behavior_of_execution: ∀s,e.
979  execution_characterisation s e →
980  ∃b:program_behavior. execution_matches_behavior e b.
981#s0 #e0 #exec
982cases exec;
983[ #s #r #m #e #tr #TERM
984    %{ (Terminates tr r)}
985    @(emb_terminates … TERM)
986| #s #e #tr #DIV
987    %{ (Diverges tr)}
988    @(emb_diverges … DIV)
989| #s #e #tr #REACTS
990    %{ (Reacts tr)}
991    @(emb_reacts … REACTS)
992| #e #s #s' #tr #WRONG
993    %{ (Goes_wrong tr)}
994    @(emb_wrong … WRONG)
995] qed.
996
997lemma initial_state_not_final: ∀ge,s.
998  initial_state ge s →
999  ¬ ∃r.final_state s r.
1000#ge #s #H cases H;
1001#b #f #ge #m #E1 #E2 #E3 #E4 % *; #r #H2
1002inversion H2;
1003#r' #m' #E5 #E6 destruct (E5);
1004qed.
1005
1006lemma initial_step: ∀ge,s,e.
1007  exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
1008  ¬(∃r.final_state s r) →
1009  ∃e'.e = e_step E0 s e'.
1010#ge #s #e >(exec_inf_aux_unfold …)
1011whd in ⊢ (??%? → ?); cases (is_final_state s);
1012[ #FINAL #EXEC #NOTFINAL
1013    @False_ind @(absurd ?? NOTFINAL)
1014    cases FINAL;
1015    #r #F %{r} @F
1016| #F1 #EXEC #F2 whd in EXEC:(??%?); % [ 2: <EXEC @refl ]
1017qed.
1018
1019theorem exec_inf_equivalence:
1020  ∀classic:(∀P:Prop.P ∨ ¬P).
1021  ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P).
1022  ∀p,e. single_exec_of (exec_inf p) e →
1023   ∃b.execution_matches_behavior e b ∧ exec_program p b.
1024#classic #constructive_indefinite_description #p #e
1025whd in ⊢ (?%? → ??(λ_.?(?%?)%));
1026lapply (make_initial_state_sound p);
1027lapply (the_initial_state p);
1028cases (make_initial_state p);
1029[ #gs cases gs; #ge #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
1030    cases INITIAL; #Ege #INITIAL''
1031    >(exec_inf_aux_unfold …)
1032    whd in ⊢ (?%? → ?);
1033    cases (is_final_state s);
1034    [ #F @False_ind
1035        @(absurd ?? (initial_state_not_final … INITIAL''))
1036        cases F; #r #F' %{r} @F'
1037    | #NOTFINAL whd in ⊢ (?%? → ?); cases e;
1038        [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #EXEC0 | #o #k #i #e #EXEC0 ]
1039        cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC'
1040    lapply (behavior_of_execution ??
1041              (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
1042        *; #b #MATCHES %{b} % //;
1043        #ge' >Ege #Ege' >(?:ge' = ge) [ 2: destruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ]
1044        inversion MATCHES;
1045        [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM
1046            #TERM
1047            lapply (exec_state_terminates … TERM); #E1
1048            >E1 in TERM #TERM
1049            @(program_terminates (mk_transrel … step) ?? ge s)
1050            [ 2: @INITIAL''
1051            | 3: @(terminates_sound … TERM EXEC')
1052            | skip
1053            | //;
1054            ]
1055        | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES #DIVERGES
1056            lapply (exec_state_diverges … DIVERGES);
1057            #E1 >E1 in DIVERGES #DIVERGES
1058            inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6
1059            <E4 in INITSTEPS ⊢ % <E5 in E6 ⊢ % #E6 #INITSTEPS
1060            cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
1061            #E7 <E7 in INITSTEPS #INITSTEPS
1062            cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV
1063            @(program_diverges (mk_transrel … step) ?? ge s … INITIAL'' INITSTAR)
1064            @(silent_sound … DIVERGING EXECDIV)
1065        | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS #REACTS
1066            lapply (exec_state_reacts … REACTS);
1067            #E1 >E1 in REACTS #REACTS
1068            inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5
1069            <E4 in REACTING ⊢ % <E5 #REACTING #E6
1070            cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
1071            #E7 <E7 in REACTING #REACTING
1072            @(program_reacts (mk_transrel … step) ?? ge s … INITIAL'')
1073            @(reacts_sound … REACTING EXEC')
1074        | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG #WRONG
1075            lapply (exec_state_wrong … WRONG);
1076            #E1 >E1 in WRONG #WRONG
1077            inversion WRONG; #tr' #s1' #s2' #e'' #GOESWRONG #E4 #E5 #E6 #E7
1078            <E4 in GOESWRONG ⊢ % <E5 <E7 #GOESWRONG
1079            cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ]
1080            #E8 <E8 in GOESWRONG #GOESWRONG
1081            elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL
1082            @(program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL'' STAR STOP)
1083            #r % #F @(absurd ?? FINAL) %{r} @F
1084        | #E destruct (E);
1085        ]
1086   ]
1087| whd in ⊢ ((∀_.? → %) → ?);
1088    #NOINIT #_ #EXEC
1089    %{ (Goes_wrong E0)} %
1090    [ whd in EXEC:(?%?);
1091        cases e in EXEC;
1092        [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #EXEC0 | #o #k #i #e #EXEC0 ]
1093        cases (se_inv … EXEC0);
1094        @emb_initially_wrong
1095    | #ge #Ege
1096        @program_goes_initially_wrong
1097        #s % #INIT cases (NOINIT s INIT); #ge' #H @H
1098    ]
1099] qed.
1100
Note: See TracBrowser for help on using the repository browser.