source: src/Clight/CexecEquiv.ma @ 950

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

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