source: src/Clight/CexecEquiv.ma @ 1352

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

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

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