source: src/Clight/CexecEquiv.ma @ 1350

Last change on this file since 1350 was 1350, checked in by sacerdot, 9 years ago

Porting to latest destruct tactic.

Note: the tactics has a few remaining bugs to be ironed out.
Look for "Wilmer: XXX" comments in the .ma files to see where
these are avoided ATM using axioms.

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