source: Deliverables/D3.1/C-semantics/CexecEquiv.ma @ 492

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

Port Clight semantics to the new-new matita syntax.

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