source: src/Clight/CexecEquiv.ma @ 748

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

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