source: C-semantics/CexecEquiv.ma @ 399

Last change on this file since 399 was 399, checked in by campbell, 10 years ago

Rearrange executable semantics a little.

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