source: src/Clight/CexecEquiv.ma @ 1603

Last change on this file since 1603 was 1566, checked in by campbell, 8 years ago

Pacify changes to destruct tactic.

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