source: C-semantics/CexecIOcomplete.ma @ 387

Last change on this file since 387 was 387, checked in by campbell, 9 years ago

Sort out equality checking of types.

File size: 44.3 KB
Line 
1include "CexecIO.ma".
2include "Plogic/connectives.ma".
3
4ndefinition yields : ∀A,P. res (Σx:A. P x) → A → Prop ≝
5λA,P,e,v. match e with [ OK v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | _ ⇒ False].
6
7(* This tells us that some execution of e results in v.
8   (There may be many possible executions due to I/O, but we're trying to prove
9   that one particular one exists corresponding to a derivation in the inductive
10   semantics.) *)
11nlet rec yieldsIO (A:Type) (P:A → Prop) (e:IO io_out io_in (Σx:A. P x)) (v:A) on e : Prop ≝
12match e with
13[ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ]
14| Interact _ k ⇒ ∃r.yieldsIO A P (k r) v
15| _ ⇒ False].
16
17nlemma is_pointer_compat_true: ∀m,b,sp.
18  pointer_compat (block_space m b) sp →
19  is_pointer_compat (block_space m b) sp = true.
20#m b sp H; nwhd in ⊢ (??%?);
21nelim (pointer_compat_dec (block_space m b) sp);
22##[ //
23##| #H'; napply False_ind; napply (absurd … H H');
24##] nqed.
25
26nlemma ms_eq_dec_true: ∀s. ms_eq_dec s s = inl ???.
27##[ #s; ncases s; napply refl;
28##| ##skip
29##] nqed.
30
31notation < "vbox( e break ↓ break e')" with precedence 99 for @{'yields ${e} ${e'}}.
32interpretation "yields" 'yields e e' = (yields ?? e e').
33interpretation "yields IO" 'yields e e' = (yieldsIO ?? e e').
34
35ntheorem is_det: ∀p,s,s'.
36initial_state p s → initial_state p s' → s = s'.
37#p s s' H1 H2;
38ninversion H1; #b1 f1 e11 e12 e13;
39ninversion H2; #b2 f2 e21 e22 e23;
40nrewrite > e11 in e21;
41#e1; nrewrite > (?:b1 = b2) in e12;
42##[ nrewrite > e22; #e2; nrewrite > (?:f2 = f1);
43  ##[ //;
44  ##| ndestruct (e2) skip (e22 e23); //;
45  ##]
46##| ndestruct (e1) skip (e11); //
47##] nqed.
48
49nlet rec yieldsIObare (A:Type) (a:IO io_out io_in A) (v':A) on a : Prop ≝
50match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIObare A (k r) v' | _ ⇒ False ].
51
52nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
53yieldsIObare A a v' →
54yieldsIO A P (io_inject io_out io_in A (λx.P x) (Some ? a) p) v'.
55#A P a; nelim a;
56##[ #a k IH v' p H; nwhd in H ⊢ %; nelim H; #r H'; @ r; napply IH; napply H';
57##| #v v' p H; napply H;
58##| #a b; *;
59##] nqed.
60
61ndefinition yieldsbare ≝ λA.λa:res A.λv':A.
62match a with [ OK v ⇒ v' = v | _ ⇒ False ].
63
64nlemma yieldsbare_eq: ∀A,a,v'. yieldsbare A a v' → a = OK ? v'.
65#A a v'; ncases a; //; nwhd in ⊢ (% → ?); *;
66nqed.
67
68nlemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
69yieldsbare A a v' →
70yields A P (err_inject A (λx.P x) (Some ? a) p) v'.
71#A P a; ncases a;
72##[ #v v' p H; napply H;
73##| #a b; *;
74##] nqed.
75
76
77ntheorem the_initial_state:
78  ∀p,s. initial_state p s → yieldsbare ? (make_initial_state p) s.
79#p s; ncases p; #fns main globs H;
80ninversion H;
81#b f e1 e2 e3;
82nwhd in ⊢ (??%?);
83nrewrite > e1;
84nwhd in ⊢ (??%?);
85nrewrite > e2;
86nwhd; napply refl;
87nqed.
88
89nlemma cast_complete: ∀m,v,ty,ty',v'.
90  cast m v ty ty' v' → yieldsbare ? (exec_cast m v ty ty') v'.
91#m v ty ty' v' H;
92nelim H;
93##[ #m i sz1 sz2 sg1 sg2; napply refl;
94##| #m f sz szi sg; napply refl;
95##| #m i sz sz' sg; napply refl;
96##| #m f sz sz'; napply refl;
97##| #m sp sp' ty ty' b ofs H1 H2 H3;
98    nelim H1; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #tys1 ty1; nletin sp1 ≝ Code ##]
99    nwhd in ⊢ (??%?);
100    ##[ ##1,2: nrewrite > (ms_eq_dec_true …); nwhd in ⊢ (??%?); ##]
101    nelim H2 in H3 ⊢ %; ##[ ##1,4,7: #sp2 ty2 ##| ##2,5,8: #sp2 ty2 n2 ##| ##3,6,9: #tys2 ty2; nletin sp2 ≝ Code ##]
102    #H3; nwhd in ⊢ (??%?);
103    nrewrite > (is_pointer_compat_true …); //;
104##| #m sz si ty'' H; ncases H; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #args rty ##] napply refl;
105##| #m t t' H H'; ncases H; ncases H'; //;
106##] nqed.
107
108nlemma yields_eq: ∀A,P,e,v. yields A P e v → ∃p. e = OK ? (sig_intro … v p).
109#A P e v; ncases e;
110##[ #vp; ncases vp; #v' p H; nwhd in H; nrewrite > H; @ p; napply refl;
111##| *;
112##] nqed.
113
114(* Use to narrow down the choice of expression to just the lvalues. *)
115nlemma lvalue_expr: ∀ge,env,m,e,ty,sp,l,ofs,tr. ∀P:expr_descr → Prop.
116  eval_lvalue ge env m (Expr e ty) sp l ofs tr →
117  (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) →
118  P e.
119#ge env m e ty sp l ofs tr P H; napply (eval_lvalue_inv_ind … H);
120##[ #id l ty e1 e2 e3 e4 e5 e6; ndestruct; //
121##| #id sp l ty e1 e2 e3 e4 e5 e6 e7; ndestruct; //
122##| #e ty sp l ofs tr H e1 e2 e3 e4 e5; ndestruct; //
123##| #e id ty sp l ofs id' fs d tr H e1 e2;(* bogus? *) #_; #e3 e4 e5 e6 e7; ndestruct; //
124##| #e id ty sp l ofs id' fs tr H e1;(* bogus? *) #_; #e2 e3 e4 e5 e6; ndestruct; //
125##] nqed.
126
127nlemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yieldsbare ? (exec_bool_of_val v ty) b.
128#v ty r H; nelim H; #v t H'; nelim H';
129  ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
130  ##| #p b i i0 s; @ true; @; //
131  ##| #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
132  ##| #p b i p0 t0; @ true; @; //
133  ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
134  ##| #i s; @ false; @; //;
135  ##| #p t; @ false; @; //;
136  ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
137  ##]
138nqed.
139
140nlemma bool_of_true: ∀v,ty. is_true v ty → yieldsbare ? (exec_bool_of_val v ty) true.
141#v ty H; nelim H;
142  ##[ #i is s ne; nwhd; nrewrite > (eq_false … ne); //;
143  ##| #p b i i0 s; //
144  ##| #i p t ne; nwhd; nrewrite > (eq_false … ne); //;
145  ##| #p b i p0 t0; //
146  ##| #f s ne; nwhd; nrewrite > (Feq_zero_false … ne); //;
147  ##]
148nqed.
149
150nlemma bool_of_false: ∀v,ty. is_false v ty → yieldsbare ? (exec_bool_of_val v ty) false.
151#v ty H; nelim H;
152  ##[ #i s; //;
153  ##| #p t; //;
154  ##| #s; nwhd; nrewrite > (Feq_zero_true …); //;
155  ##]
156nqed.
157
158nremark eq_to_jmeq: ∀A. ∀a,b:A. a = b → a ≃ b.
159#A a b H; nrewrite > H; //; nqed.
160
161nlemma dep_option_rewrite: ∀A,B:Type. ∀e:option A. ∀r:B. ∀P:B → Prop. ∀Q:e ≃ None A → res (Σx:B. P x). ∀R:∀v. e ≃ Some A v → res (Σx:B. P x). ∀h: e = None A.
162 yields ?? (Q (eq_to_jmeq ??? h)) r →
163 yields ?? ((match e return λe'.e ≃ e' → ? with [ None ⇒ λp.Q p | Some v ⇒ λp.R v p ]) (refl_jmeq (option A) e)) r.
164#A B e; ncases e;
165##[ #r P Q R h; nwhd in ⊢ (? → ???%?);
166napply (streicherKjmeq ?? (λe. yields ?? (Q e) r → yields ?? (Q (refl_jmeq (option A) (None A))) r));
167//;
168##| #v r P Q R h; ndestruct (h);
169##] nqed.
170
171nlemma expr_lvalue_complete: ∀ge,env,m.
172(∀e,v,tr. eval_expr ge env m e v tr → yieldsbare ? (exec_expr ge env m e) (〈v,tr〉)) ∧
173(∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yieldsbare ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)).
174#ge env m;
175napply (combined_expr_lvalue_ind ge env m
176  (λe,v,tr,H. yieldsbare ? (exec_expr ge env m e) (〈v,tr〉))
177  (λe,sp,l,off,tr,H. yieldsbare ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)));
178##[ #i ty; napply refl;
179##| #f ty; napply refl;
180##| #e ty sp l off v tr H1 H2; napply (lvalue_expr … H1);
181    ##[ #id ##| #e' ##| #e' id ##] #H3;
182    nwhd in ⊢ (??%?);
183    nrewrite > (yieldsbare_eq ??? H3);
184    nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
185##| #e ty sp l off tr H1 H2; nwhd in ⊢ (??%?);
186    nrewrite > (yieldsbare_eq ??? H2);
187    napply refl;
188##| #ty' ty; napply refl;
189##| #op e ty v1 v tr H1 H2 H3; nwhd in ⊢ (??%?);
190    nrewrite > (yieldsbare_eq ??? H3);
191    nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
192##| #op e1 e2 ty v1 v2 v tr1 tr2 H1 H2 e3 H4 H5; nwhd in ⊢ (??%?);
193    nrewrite > (yieldsbare_eq ??? H4); nwhd in ⊢ (??%?);
194    nrewrite > (yieldsbare_eq ??? H5); nwhd in ⊢ (??%?);
195    nrewrite > e3; napply refl;
196##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?);
197    nrewrite > (yieldsbare_eq ??? H4); nwhd in ⊢ (??%?);
198    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
199    nrewrite > (yieldsbare_eq ??? H5);
200    napply refl;
201##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?);
202    nrewrite > (yieldsbare_eq ??? H4); nwhd in ⊢ (??%?);
203    nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
204    nrewrite > (yieldsbare_eq ??? H5);
205    napply refl;
206##| #e1 e2 ty v1 tr H1 H2 H3; nwhd in ⊢ (??%?);
207    nrewrite > (yieldsbare_eq ??? H3); nwhd in ⊢ (??%?);
208    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
209    napply refl;   
210##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; nwhd in ⊢ (??%?);
211    nrewrite > (yieldsbare_eq ??? H5); nwhd in ⊢ (??%?);
212    nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
213    nrewrite > (yieldsbare_eq ??? H6); nwhd in ⊢ (??%?);
214    nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb;
215    nrewrite > (yieldsbare_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb;
216    napply refl;   
217##| #e1 e2 ty v1 tr H1 H2 H3; nwhd in ⊢ (??%?);
218    nrewrite > (yieldsbare_eq ??? H3); nwhd in ⊢ (??%?);
219    nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
220    napply refl;   
221##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; nwhd in ⊢ (??%?);
222    nrewrite > (yieldsbare_eq ??? H5); nwhd in ⊢ (??%?);
223    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
224    nrewrite > (yieldsbare_eq ??? H6); nwhd in ⊢ (??%?);
225    nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb;
226    nrewrite > (yieldsbare_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb;
227    napply refl;
228##| #e ty ty' v1 v tr H1 H2 H3; nwhd in ⊢ (??%?);
229    nrewrite > (yieldsbare_eq ??? H3); nwhd in ⊢ (??%?);
230    nrewrite > (yieldsbare_eq ??? (cast_complete … H2));
231    napply refl;
232##| #e ty v l tr H1 H2; nwhd in ⊢ (??%?);
233    nrewrite > (yieldsbare_eq ??? H2); nwhd in ⊢ (??%?);
234    napply refl;
235   
236  (* lvalues *)
237##| #id l ty e1; nwhd in ⊢ (??%?); nrewrite > e1; napply refl;
238##| #id sp l ty e1 e2; nwhd in ⊢ (??%?); nrewrite > e1;
239    nrewrite > e2; napply refl;
240##| #e ty sp l ofs tr H1 H2; nwhd in ⊢ (??%?);
241    nrewrite > (yieldsbare_eq ??? H2);
242    napply refl;
243##| #e i ty sp l ofs id fList delta tr H1 H2 H3 H4; ncases e in H2 H4 ⊢ %;
244    #e' ty' H2; nwhd in H2:(??%?); nrewrite > H2; #H4; nwhd in ⊢ (??%?);
245    nrewrite > (yieldsbare_eq ??? H4); nwhd in ⊢ (??%?);
246    nrewrite > H3; napply refl;
247##| #e i ty sp l ofs id fList tr; ncases e; #e' ty' H1 H2;
248    nwhd in H2:(??%?); nrewrite > H2; #H3; nwhd in ⊢ (??%?);
249    nrewrite > (yieldsbare_eq ??? H3); napply refl;
250##] nqed.
251
252ntheorem expr_complete:  ∀ge,env,m.
253 ∀e,v,tr. eval_expr ge env m e v tr → yieldsbare ? (exec_expr ge env m e) (〈v,tr〉).
254#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
255
256ntheorem exprlist_complete: ∀ge,env,m,es,vs,tr.
257  eval_exprlist ge env m es vs tr → yieldsbare ? (exec_exprlist ge env m es) (〈vs,tr〉).
258#ge env m es vs tr H; nelim H;
259##[ napply refl;
260##| #e et v vt tr trt H1 H2 H3; nwhd in ⊢ (??%?);
261    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
262    nrewrite > (yieldsbare_eq ??? H3);
263    napply refl;
264##] nqed.
265
266ntheorem lvalue_complete: ∀ge,env,m.
267 ∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yieldsbare ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉).
268#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
269
270nlet rec P_typelist (P:type → Prop) (l:typelist) on l : Prop ≝
271match l with
272[ Tnil ⇒ True
273| Tcons h t ⇒ P h ∧ P_typelist P t
274].
275
276nlet rec type_ind2l
277  (P:type → Prop) (Q:typelist → Prop)
278  (vo:P Tvoid)
279  (it:∀i,s. P (Tint i s))
280  (fl:∀f. P (Tfloat f))
281  (pt:∀s,t. P t → P (Tpointer s t))
282  (ar:∀s,t,n. P t → P (Tarray s t n))
283  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
284  (st:∀i,fl. P (Tstruct i fl))
285  (un:∀i,fl. P (Tunion i fl))
286  (cp:∀i. P (Tcomp_ptr i))
287  (nl:Q Tnil)
288  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
289 (t:type) on t : P t ≝
290  match t return λt'.P t' with
291  [ Tvoid ⇒ vo
292  | Tint i s ⇒ it i s
293  | Tfloat s ⇒ fl s
294  | Tpointer s t' ⇒ pt s t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
295  | Tarray s t' n ⇒ ar s t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
296  | Tfunction tl t' ⇒ fn tl t' (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl) (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
297  | Tstruct i fs ⇒ st i fs
298  | Tunion i fs ⇒ un i fs
299  | Tcomp_ptr i ⇒ cp i
300  ]
301and typelist_ind2l
302  (P:type → Prop) (Q:typelist → Prop)
303  (vo:P Tvoid)
304  (it:∀i,s. P (Tint i s))
305  (fl:∀f. P (Tfloat f))
306  (pt:∀s,t. P t → P (Tpointer s t))
307  (ar:∀s,t,n. P t → P (Tarray s t n))
308  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
309  (st:∀i,fl. P (Tstruct i fl))
310  (un:∀i,fl. P (Tunion i fl))
311  (cp:∀i. P (Tcomp_ptr i))
312  (nl:Q Tnil)
313  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
314  (ts:typelist) on ts : Q ts ≝
315  match ts return λts'.Q ts' with
316  [ Tnil ⇒ nl
317  | Tcons t tl ⇒ cs t tl (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t)
318                     (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl)
319  ].
320
321nlemma assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
322#t; nwhd in ⊢ (??(λ_.??%?)); ncases (type_eq_dec t t); #E;
323##[ @ E; //
324##| napply False_ind; napply (absurd ?? E); //
325##] nqed.
326
327nlemma is_not_void_true: ∀f. ¬fn_return f = Tvoid → ∃p. is_not_void (fn_return f) = OK ? p.
328#f; ncases f; #ty; #_; #_; #_; ncases ty;
329##[ #H; napply False_ind; /2/;
330##| #sz sg e; @ ?; //; ##| #sz e; @ ?; // ##| #sp ty e; @ ?; // ##| #sp ty n e; @ ?; // ##|
331    #tys ty e; @ ?; // ##| #id fs e; @ ?; // ##| #id fs e; @ ?; // ##| #id e; @ ?; // ##]
332nqed.
333
334nlemma alloc_vars_complete: ∀env,m,l,env',m'.
335  alloc_variables env m l env' m' →
336  ∃p.exec_alloc_variables env m l = sig_intro ?? (Some ? 〈env', m'〉) p.
337#env m l env' m' H; nelim H;
338##[ #env'' m''; @ ?; nwhd; //;
339##| #env1 m1 id ty l1 m2 loc m3 env2 H1 H2 H3;
340    nwhd in H1:(??%?) ⊢ (??(λ_.??%?));
341    ndestruct (H1);
342    nelim H3; #p3 e3; nrewrite > e3; nwhd in ⊢ (??(λ_.??%?)); @ ?; //;
343##] nqed.
344
345nlemma bind_params_complete: ∀e,m,params,vs,m2.
346  bind_parameters e m params vs m2 →
347  yields ?? (exec_bind_parameters e m params vs) m2.
348#e m params vs m2 H; nelim H;
349##[ //;
350##| #env1 m1 id ty l v tl loc m2 m3 H1 H2 H3 H4;
351    napply remove_res_sig;
352    nrewrite > H1; nwhd in ⊢ (??%?);
353    nrewrite > H2; nwhd in ⊢ (??%?);
354    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4;
355    napply refl;
356##] nqed.
357
358nlemma eventval_match_complete': ∀ev,ty,v.
359  eventval_match ev ty v → yields ?? (check_eventval' v ty) ev.
360#ev ty v H; nelim H; //; nqed.
361
362nlemma eventval_list_match_complete: ∀vs,tys,evs.
363  eventval_list_match evs tys vs → yields ?? (check_eventval_list vs tys) evs.
364#vs tys evs H; nelim H;
365##[ //
366##| #e etl ty tytl v vtl H1 H2 H3; napply remove_res_sig;
367    nelim (yields_eq ???? (eventval_match_complete' … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
368    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
369    napply refl;
370##] nqed.   
371
372
373ntheorem step_complete: ∀ge,s,tr,s'.
374  step ge s tr s' → yieldsIObare ? (exec_step ge s) 〈tr,s'〉.
375#ge s tr s' H; nelim H;
376##[ #f e e1 k e2 m sp loc ofs v m' tr1 tr2 H1 H2 H3; nwhd in ⊢ (??%?);
377    nrewrite > (yieldsbare_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
378    nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
379    nrewrite > H3; napply refl;
380##| #f e eargs k ef m vf vargs f' tr1 tr2 H1 H2 H3 H4; nwhd in ⊢ (??%?);
381    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
382    nrewrite > (yieldsbare_eq ??? (exprlist_complete … H2)); nwhd in ⊢ (??%?);
383    nrewrite > H3; nwhd in ⊢ (??%?);
384    nrewrite > H4; nelim (assert_type_eq_true (typeof e)); #pty ety; nrewrite > ety;
385    napply refl;
386##| #f el ef eargs k env m sp loc ofs vf vargs f' tr1 tr2 tr3 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?);
387    nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
388    nrewrite > (yieldsbare_eq ??? (exprlist_complete … H3)); nwhd in ⊢ (??%?);
389    nrewrite > H4; nwhd in ⊢ (??%?);
390    nrewrite > H5; nelim (assert_type_eq_true (typeof ef)); #pty ety; nrewrite > ety;
391    nwhd in ⊢ (??%?);
392    nrewrite > (yieldsbare_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
393    napply refl;
394##| #f s1 s2 k env m; napply refl
395##| ##5,6,7: #f s k env m; napply refl
396##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
397    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
398    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
399    napply refl
400##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
401    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
402    nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
403    napply refl
404##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?);
405    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
406    nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
407    napply refl
408##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?);
409    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
410    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
411    napply refl
412##| #f s1 e s2 k env m H; ncases H; #es1; nrewrite > es1; napply refl;
413##| ##13,14: #f e s k env m; napply refl
414##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?);
415    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
416    nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
417    napply refl
418##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?);
419    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
420    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
421    napply refl
422##| #f e s k env m; napply refl;
423##| #f s1 e s2 s3 k env m nskip; nwhd in ⊢ (??%?); ncases (is_Sskip s1);
424    ##[ #H; napply False_ind; /2/;
425    ##| #H; nwhd in ⊢ (??%?); napply refl ##]
426##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
427    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
428    nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
429    napply refl;
430##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
431    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
432    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
433    napply refl;
434##| #f s1 e s2 s3 k env m; *; #es1; nrewrite > es1; napply refl;
435##| ##22,23: #f e s1 s2 k env m; napply refl;
436##| #f k env m H; nwhd in ⊢ (??%?); nrewrite > H; napply refl;
437##| #f e k env m v tr H1 H2; nwhd in ⊢ (??%?);
438    nelim (is_not_void_true f H1); #pf ef; nrewrite > ef; nwhd in ⊢ (??%?);
439    nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
440    napply refl;
441##| #f k env m; ncases k;
442    ##[ #H1 H2; nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
443    ##| #s' k'; nwhd in ⊢ (% → ?); *;
444    ##| ##3,4: #e' s' k'; nwhd in ⊢ (% → ?); *;
445    ##| ##5,6: #e' s1' s2' k'; nwhd in ⊢ (% → ?); *;
446    ##| #k'; nwhd in ⊢ (% → ?); *;
447    ##| #r f' env' k' H1 H2; nwhd in ⊢ (??%?); nrewrite > H2; napply refl
448    ##]
449##| #f e s k env m i tr H1; nwhd in ⊢ (??%?);
450    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
451    napply refl
452##| #f s k env m; *; #es; nrewrite > es; napply refl;
453##| #f k env m; napply refl
454##| #f l s k env m; napply refl
455##| #f l k env m s k' H1; nwhd in ⊢ (??%?); nrewrite > H1; napply refl;
456##| #f args k m1 env m2 m3 H1 H2; nwhd in ⊢ (??%?);
457    nelim (alloc_vars_complete … H1); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
458    nelim (yields_eq ???? (bind_params_complete … H2)); #p2 e2; nrewrite > e2;
459    napply refl;
460##| #id tys rty args k m rv tr H; nwhd in ⊢ (??%?);
461    ninversion H; #f' args' rv' eargs erv H1 H2 e1 e2 e3 e4; nrewrite < e1 in H1 H2;
462    #H1 H2;
463    nelim (yields_eq ???? (eventval_list_match_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
464    nwhd; ninversion H2; #x e5 e6 e7; @ x; nwhd in ⊢ (??%?);
465    napply refl
466##| #v f env k m; nwhd in ⊢ (??%?); napply daemon (* FIXME: inductive semantics allows any value ?! *)
467##| #v f env k m1 m2 sp loc ofs ty H; nwhd in ⊢ (??%?);
468    nrewrite > H; napply refl
469##| #f l s k env m; napply refl
470##] nqed.
471 
472nlemma wrong_sound: ∀ge,tr,s,s',e.
473  execution_goes_wrong tr s (e_step E0 s e) s' →
474  exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e →
475  star (mk_transrel … step) ge s tr s' ∧
476  nostep (mk_transrel … step) ge s' ∧
477  (¬∃r. final_state s' r).
478#ge tr0 s0 s0' e0 WRONG; ncases WRONG;
479#tr s s' e ESTEPS EXEC;
480ncases (several_steps … ESTEPS EXEC);
481#STAR EXEC'; @;
482##[ @; ##[ napply STAR;
483       ##| #badtr bads; @; #badSTEP;
484           nlapply (step_complete … badSTEP);
485           nlapply (exec_e_step … EXEC');
486           ncases (exec_step ge s');
487           ##[ #o k; nrewrite > (execution_cases (exec_inf_aux …)); #E; nwhd in E:(??%?);
488               ndestruct
489           ##| #x; ncases x; #trx stx; nrewrite > (exec_inf_aux_unfold …);
490               nwhd in ⊢ (??%? → ?); ncases (is_final_state stx);
491               #FINAL E; nwhd in E:(??%?); ndestruct
492           ##| #E H; nwhd in H; napply H
493           ##]
494       ##]
495##| @; #FINAL;
496    nrewrite > (exec_inf_aux_unfold …) in EXEC';
497    nwhd in ⊢ (??%? → ?);
498    ncases (is_final_state s'); #FINAL';
499    ##[ nwhd in ⊢ (??%? → ?); #E; ndestruct;
500    ##| napply False_ind; napply (absurd … FINAL FINAL');
501    ##]
502##] nqed.
503
504ninductive execution_characterisation : state → execution → Prop ≝
505| ec_terminates: ∀s,r,m,e,tr.
506    execution_terminates tr s e r m →
507    execution_characterisation s e
508| ec_diverges: ∀s,e,tr.
509    execution_diverges tr s e →
510    execution_characterisation s e
511| ec_reacts: ∀s,e,tr.
512    execution_reacts tr s e →
513    execution_characterisation s e
514| ec_wrong: ∀e,s,s',tr.
515    execution_goes_wrong tr s e s' →
516    execution_characterisation s e.
517
518(* bit of a hack to avoid inability to reduce term in match *)
519ndefinition interact_prop : ∀A:Type.(∀o:io_out. (io_in o → IO io_out io_in A) → Prop) → IO io_out io_in A → Prop ≝
520λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ].
521
522nlemma err_does_not_interact: ∀A,B,P,e1,e2.
523  (∀x:B.interact_prop A P (e2 x)) →
524  interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2).
525#A B P e1 e2 H;
526ncases e1; //; nqed.
527
528nlemma err2_does_not_interact: ∀A,B,C,P,e1,e2.
529  (∀x,y.interact_prop A P (e2 x y)) →
530  interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2).
531#A B C P e1 e2 H;
532ncases e1; ##[ #z; ncases z; ##] //; nqed.
533
534nlemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2.
535  (∀x.interact_prop A P (e2 x)) →
536  interact_prop A P (bindIO ?? (sigma B Q) A (err_to_io_sig ??? Q e1) e2).
537#A B P Q e1 e2 H;
538ncases e1; //; nqed.
539
540nlemma opt_does_not_interact: ∀A,B,P,e1,e2.
541  (∀x:B.interact_prop A P (e2 x)) →
542  interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2).
543#A B P e1 e2 H;
544ncases e1; //; nqed.
545
546nlemma exec_step_interaction:
547  ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s).
548#ge s; ncases s;
549##[ #f st kk e m; ncases st;
550  ##[ ##11,14: #a ##| ##2,4,6,7,12,13,15: #a b ##| ##3,5: #a b c ##| ##8: #a b c d ##]
551  ##[ ##4,6,8,9: napply I ##]
552  nwhd in ⊢ (???%);
553  ##[ ncases a; ##[ ncases (fn_return f); //; ##| #e; nwhd nodelta in ⊢ (???%);
554                    napply err_sig_does_not_interact; #x; napply err2_does_not_interact; // ##]
555  ##| ncases (find_label a (fn_body f) (call_cont kk)); ##[ napply I ##| #z; ncases z; #x y; napply I ##]
556  ##| napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5; napply I
557  ##| ##4,7: napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I
558  ##| napply err2_does_not_interact; #x1 x2; ncases x1; //;
559  ##| napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5;  napply err_does_not_interact; #x6; ncases a;
560      ##[ napply I; ##| #x7; napply err2_does_not_interact; #x8 x9; napply I ##]
561  ##| ncases (is_Sskip a); #H; ##[ napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I
562      ##| napply I ##]
563  ##| ncases kk; ##[ ##1,8: ncases (fn_return f); //; ##| ##2,3,5,6,7: //;
564      ##| #z1 z2 z3; napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I ##]
565  ##| ncases kk; //;
566  ##| ncases kk; ##[ ##4: #z1 z2 z3;  napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I
567      ##| ##*: // ##]
568  ##]
569##| #f args kk m; ncases f;
570  ##[ #f'; nwhd in ⊢ (???%); ncases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'));
571      #x; ncases x; ##[ *; ##| #z; ncases z; #x1 x2 H;
572                        napply err_sig_does_not_interact; //; ##]
573  (* This is the only case that actually matters! *)
574  ##| #fn argtys rty; nwhd in ⊢ (???%);
575      napply  err_sig_does_not_interact; #x1;
576      nwhd; #i; @; ##[ ##2: @; ##[ ##2: @; ##[ @; nwhd in ⊢ (??%?); napply refl;
577        ##| @; #E; nwhd in E:(??%%); ndestruct (E); ##] ##] ##]
578  ##]
579##| #v kk m; nwhd in ⊢ (???%); ncases kk;
580    ##[ ##8: #x1 x2 x3 x4; ncases x1;
581      ##[ nwhd in ⊢ (???%); ncases v; // ##| #x5; nwhd in ⊢ (???%); ncases x5;
582          #x6 x7; napply opt_does_not_interact; // ##]
583    ##| ##*: // ##]
584##] nqed.
585
586
587(* Some classical logic (roughly like a fragment of Coq's library) *)
588nlemma classical_doubleneg:
589  ∀classic:(∀P:Prop.P ∨ ¬P).
590  ∀P:Prop. ¬ (¬ P) → P.
591#classic P; *; #H;
592ncases (classic P);
593##[ // ##| #H'; napply False_ind; /2/; ##]
594nqed.
595
596nlemma classical_not_all_not_ex:
597  ∀classic:(∀P:Prop.P ∨ ¬P).
598  ∀A:Type.∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x.
599#classic A P; *; #H;
600napply (classical_doubleneg classic); @; *; #H';
601napply H; #x; @; #H''; napply H'; @x; napply H'';
602nqed.
603
604nlemma classical_not_all_ex_not:
605  ∀classic:(∀P:Prop.P ∨ ¬P).
606  ∀A:Type.∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x.
607#classic A P; *; #H;
608napply (classical_not_all_not_ex classic A (λx.¬ P x));
609@; #H'; napply H; #x; napply (classical_doubleneg classic);
610napply H';
611nqed.
612
613nlemma not_ex_all_not:
614  ∀A:Type.∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x.
615#A P; *; #H x; @; #H';
616napply H; @ x; napply H';
617nqed.
618
619nlemma not_imply_elim:
620  ∀classic:(∀P:Prop.P ∨ ¬P).
621  ∀P,Q:Prop. ¬ (P → Q) → P.
622#classic P Q; *; #H;
623napply (classical_doubleneg classic); @; *; #H';
624napply H; #H''; napply False_ind; napply H'; napply H'';
625nqed.
626
627nlemma not_imply_elim2:
628  ∀P,Q:Prop. ¬ (P → Q) → ¬ Q.
629#P Q; *; #H; @; #H';
630napply H; #_; napply H';
631nqed.
632
633nlemma imply_to_and:
634  ∀classic:(∀P:Prop.P ∨ ¬P).
635  ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q.
636#classic P Q H; @;
637##[ napply (not_imply_elim classic P Q H);
638##| napply (not_imply_elim2 P Q H);
639##] nqed.
640
641nlemma not_and_to_imply:
642  ∀classic:(∀P:Prop.P ∨ ¬P).
643  ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q.
644#classic P Q; *; #H H';
645@; #H''; napply H; @; //;
646nqed.
647
648ninductive execution_not_over : execution → Prop ≝
649| eno_step: ∀tr,s,e. execution_not_over (e_step tr s e)
650| eno_interact: ∀o,k,tr,s,e,i.
651    k i = e_step tr s e →
652    execution_not_over (e_interact o k).
653
654nlemma eno_stop: ∀tr,r,m. execution_not_over (e_stop tr r m) → False.
655#tr0 r0 m0 H; ninversion H;
656##[ #tr s e E; ndestruct
657##| #o k tr s e i K E; ndestruct
658##] nqed.
659
660nlemma eno_wrong: execution_not_over e_wrong → False.
661#H; ninversion H;
662##[ #tr s e E; ndestruct
663##| #o k tr s e i K E; ndestruct
664##] nqed.
665
666nlet corec show_divergence s e
667 (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
668                 execution_not_over e1)
669 (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0)
670 (CONTINUES:∀tr2,s2,o,k. execution_isteps tr2 s e s2 (e_interact o k) → ∃i.∃tr3.∃s3.∃e3. k i = e_step tr3 s3 e3 ∧ tr3 ≠ E0)
671 : execution_diverging e ≝ ?.
672nlapply (NONTERMINATING E0 s e ?); //;
673ncases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %;
674##[ #tr i m; #_; #_; #_; #ENO; nelim (eno_stop … ENO);
675##| #tr s' e' UNREACTIVE; nlapply (UNREACTIVE tr s' e' ?);
676  ##[ nrewrite < (E0_right tr) in ⊢ (?%????);
677      napply isteps_one; napply isteps_none;
678  ##| #TR; napply (match sym_eq ??? TR with [ refl ⇒ ? ]); (* nrewrite > TR in UNREACTIVE ⊢ %;*)
679      #NONTERMINATING CONTINUES; #_; @;
680      napply (show_divergence s');
681      ##[ #tr1 s1 e1 S; napply (NONTERMINATING tr1 s1 e1);
682        nchange in ⊢ (?%????) with (Eapp E0 tr1); napply isteps_one;
683        napply S;
684      ##| #tr2 s2 e2 S; nrewrite > TR in UNREACTIVE; #UNREACTIVE; napply (UNREACTIVE tr2 s2 e2);
685          nchange in ⊢ (?%????) with (Eapp E0 tr2);
686          napply isteps_one; napply S;
687      ##| #tr2 s2 o k S; napply (CONTINUES tr2 s2 o k);
688          nchange in ⊢ (?%????) with (Eapp E0 tr2);
689          napply isteps_one; napply S;
690      ##]
691  ##]
692##| #_; #_; #_; #ENO; nelim (eno_wrong … ENO);
693##| #o k UNREACTIVE NONTERMINATING CONTINUES; #_;
694    nlapply (CONTINUES E0 s o k ?);
695    ##[ napply isteps_none;
696    ##| *; #i; *; #tr'; *; #s'; *; #e'; *; #EXEC NOTSILENT;
697        napply False_ind; napply (absurd ?? NOTSILENT);
698        napply (UNREACTIVE … s' e');
699        nrewrite < (E0_right tr') in ⊢ (?%????);
700        napply (isteps_interact … EXEC); //;
701    ##]
702##] nqed.
703
704nlemma exec_over_isteps: ∀ge,tr,s,s',e,e'.
705  execution_isteps tr s e s' e' →
706  e = (exec_inf_aux ge (exec_step ge s)) →
707  exec_inf_aux ge (exec_step ge s') = e'.
708#ge tr0 s0 s0' e0 e0';
709#ISTEPS; nelim ISTEPS;
710##[ #s e E; nrewrite > E; napply refl;
711##| #e1 e2 tr1 tr2 s1 s2 s3 ISTEPS' IH E;
712    napply IH; napply sym_eq; napply exec_e_step;
713    ##[ ##3: napply sym_eq; napply E ##]
714##| #e1 e2 o k i s1 s2 s3 tr1 tr2 ISTEPS' EXECK IH E;
715    napply IH;
716    ncases (exec_step ge s3) in E;
717    ##[ #o' k'; nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
718        #E'; nwhd in E':(???%); ndestruct (E');
719        napply sym_eq; napply exec_e_step;
720        ##[ ##3: napply EXECK; ##]
721    ##| #z; ncases z; #tr' s';
722        nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
723        nwhd in ⊢ (???% → ?); ncases (is_final_state s');
724        #F E'; nwhd in E':(???%); ndestruct (E');
725    ##| nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
726        #E'; nwhd in E':(???%); ndestruct (E');
727    ##]
728##] nqed.
729
730nlemma exec_over_isteps': ∀ge,tr,s,s',e'.
731  execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s' e' →
732  exec_inf_aux ge (exec_step ge s') = e'.
733#ge tr s s' e'; nletin e ≝ (exec_inf_aux ge (exec_step ge s)); #H;
734napply (exec_over_isteps … H (refl ??));
735nqed.
736
737nlemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
738  exec_inf_aux ge (exec_step ge s) = e_interact o k →
739  k i = e_step tr s' e →
740  tr ≠ E0.
741#ge o k i tr s s' e; nrewrite > (exec_inf_aux_unfold …);
742nlapply (exec_step_interaction ge s);
743ncases (exec_step ge s);
744##[ #o' k' ; nwhd in ⊢ (% → ??%? → ?); #H E K; ndestruct (E);
745    nlapply (H i); *; #tr'; *; #s''; *; #K' TR;
746    nrewrite > K' in K; nrewrite > (exec_inf_aux_unfold …);
747    nwhd in ⊢ (??%? → ?);
748    ncases (is_final_state s'');
749    ##[ #F; nwhd in ⊢ (??%? → ?); #E; ndestruct (E);
750    ##| #F; nwhd in ⊢ (??%? → ?); #E; ndestruct (E);
751        napply TR
752    ##]
753##| #x; ncases x; #tr' s'' H; nwhd in ⊢ (??%? → ?);
754    ncases (is_final_state s''); #F E; nwhd in E:(??%?); ndestruct (E);
755##| #_; #E; nwhd in E:(??%?); ndestruct (E);
756##] nqed.
757
758nlet corec reactive_traceinf' ge s
759  (REACTIVE: ∀tr,s1,e1.
760    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
761    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
762  : traceinf' ≝ ?.
763nlapply (REACTIVE E0 s (exec_inf_aux ge (exec_step ge s)) ?);
764##[ napply isteps_none
765##| *; #x; ncases x; #tr; #y; ncases y; #s' e; *; #STEPS H;
766    @ tr ? H;
767    napply (reactive_traceinf' ge s');
768    #tr1 s1 e1 STEPS1;
769    napply REACTIVE;
770    ##[ ##2: nrewrite > (exec_over_isteps' … STEPS) in STEPS1; #STEPS1;
771        napply (isteps_trans … STEPS STEPS1);
772    ##| ##skip
773    ##]
774##]
775nqed.
776
777nlet corec 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)) ≝ ?.
782napply daemon; (*
783nrewrite > (unroll_traceinf' (reactive_traceinf' …));
784(* FIXME: want to unfold and do case analysis on REACTIVE …, but can't until bug is fixed. *)
785ncases (reactive_traceinf' ge s REACTIVE);
786#tr tr' NE; nwhd in ⊢ (?(?%)??); nrewrite > (traceinf_traceinfp_app …);
787napply (reacting … NE);
788*)
789nqed.
790
791nlemma execution_characterisation_complete:
792  ∀classic:(∀P:Prop.P ∨ ¬P).
793  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
794   ∀ge,s. ¬ (∃r. final_state s r) →
795   execution_characterisation s (exec_inf_aux ge (Value ??? 〈E0,s〉)).
796#classic constructive_indefinite_description ge s; *; #NOTFINAL;
797nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%);
798ncases (is_final_state s); ##[ #x; ncases x; #r FINAL; napply False_rect_Type0; napply NOTFINAL; @r; napply FINAL ##]
799#NOTFINAL'; nwhd in ⊢ (??%);
800ncases (classic (∀tr1,s1,e1. execution_isteps tr1 s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
801                 execution_not_over e1));
802##[ #NONTERMINATING;
803    ncases (classic (∃tr,s1,e1. execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 ∧
804                     ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0));
805  ##[ *; #tr; *; #s1; *; #e1; *; #INITIAL UNREACTIVE;
806      napply (ec_diverges … s ? tr);
807      napply (diverges_diverging … INITIAL);
808      napply (show_divergence s1);
809      ##[ #tr2 s2 e2 S; napply (NONTERMINATING (Eapp tr tr2) s2 e2);
810          napply (isteps_trans … INITIAL S);
811      ##| #tr2 s2 e2 S; napply (UNREACTIVE … S);
812      ##| #tr2 s2 o; ncases o; #o_id o_args o_typ; ncases o_typ; #k S;
813          nlapply (exec_over_isteps … INITIAL (refl ??)); #EXEC1;
814          nlapply (exec_over_isteps … S (sym_eq … EXEC1));
815          nlapply (NONTERMINATING (Eapp tr tr2) s2 (e_interact (mk_io_out o_id o_args ?) k) ?);
816          ##[ ##1,3: napply (isteps_trans … INITIAL S); ##]
817          #NOTOVER; ninversion NOTOVER;
818          ##[ ##1,3: #tr' s' e' E; ndestruct (E);
819          ##| ##*: #o' k' tr' s' e' i' KR E; ndestruct (E);
820              #EXEC;
821              @ i'; @ tr'; @s'; @e'; @;//; napply (interaction_is_not_silent … EXEC KR);
822          ##]
823      ##]
824
825  ##| *; #NOTUNREACTIVE;
826      ncut (∀tr,s1,e1.execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
827            ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0);
828      ##[ #tr s1 e1 STEPS;
829          napply (classical_doubleneg classic); @; #NOREACTION;
830          napply NOTUNREACTIVE;
831          @ tr; @s1; @e1; @; //;
832          #tr2 s2 e2 STEPS2;
833          nlapply (not_ex_all_not … NOREACTION); #NR1;
834          nlapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2;
835          napply (classical_doubleneg classic);
836          napply NR2; //;
837      ##| #REACTIVE;
838          napply ec_reacts;
839          ##[ ##2: napply reacts;
840                   napply (show_reactive ge s …);
841                   #tr s1 e1 STEPS;
842                   napply constructive_indefinite_description;
843                   napply (REACTIVE … tr s1 e1 STEPS);
844          ##| ##skip
845          ##]
846      ##]
847  ##]
848 
849##| #NOTNONTERMINATING; nlapply (classical_not_all_ex_not classic … NOTNONTERMINATING);
850    *; #tr NNT2; nlapply (classical_not_all_ex_not classic … NNT2);
851    *; #s' NNT3; nlapply (classical_not_all_ex_not classic … NNT3);
852    *; #e NNT4; nelim (imply_to_and classic … NNT4);
853    ncases e;
854    ##[ #tr' r m; #STEPS NOSTEP;
855        napply (ec_terminates s r m ? (Eapp tr tr')); @;
856        ##[ napply s'
857        ##| napply STEPS
858        ##]
859    ##| #tr' s'' e' STEPS; *; #NOSTEP; napply False_rect_Type0;
860        napply NOSTEP; //
861    ##| #STEPS NOSTEP;
862        napply (ec_wrong ? s s' tr); @; //;
863    (* The following is stupidly complicated when most of the cases are impossible.
864       It ought to be simplified. *)
865    ##| #o; ncases o; #o_id o_args o_rty; ncases o_rty; #k STEPS NOSTEP;
866        ##[ nletin i ≝ (repr 0) ##| nletin i ≝ Fzero ##]
867        nlapply (refl ? (k i));
868        ncases (k i) in ⊢ (???% → ?);
869        ##[ ##1,5: #tr' r m K;
870                   napply (ec_terminates s ???);
871                   ##[ ##4,8: napply (annoying_corner_case_terminates … STEPS K);
872                   ##| ##*: ##skip
873                   ##]
874        ##| ##2,6: #tr' s'' e' K; napply False_rect_Type0;
875            napply (absurd ?? NOSTEP);
876            napply (eno_interact … K);
877        ##| ##3,7: #K;
878            nlapply (exec_step_interaction ge s');
879            nlapply (exec_over_isteps … STEPS (refl ??));
880            nrewrite > (exec_inf_aux_unfold …); ncases (exec_step ge s');
881            ##[ ##1,4: #o k E H; nwhd in E:(??%?) H;
882                ndestruct (E);
883                nlapply (H i); *; #tr'; *; #s'; *; #K'; nrewrite > K' in K;
884                nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
885                ncases (is_final_state s'); #F E; nwhd in E:(??%?);
886                ndestruct (E);
887            ##| ##2,5: #z; ncases z; #tr s; nwhd in ⊢ (??%? → ?);
888                ncases (is_final_state s); #F E; nwhd in E:(??%?);
889                ndestruct (E);
890            ##| ##3,6: #E; nwhd in E:(??%?); ndestruct (E);
891            ##]
892        ##| ##4,8: #o0 k0 K;
893            nlapply (exec_step_interaction ge s');
894            nlapply (exec_over_isteps … STEPS (refl ??));
895            nrewrite > (exec_inf_aux_unfold …); ncases (exec_step ge s');
896            ##[ ##1,4: #o k E H; nwhd in E:(??%?) H;
897                ndestruct (E);
898                nlapply (H i); *; #tr'; *; #s'; *; #K'; nrewrite > K' in K;
899                nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
900                ncases (is_final_state s'); #F E; nwhd in E:(??%?);
901                ndestruct (E);
902            ##| ##2,5: #z; ncases z; #tr s; nwhd in ⊢ (??%? → ?);
903                ncases (is_final_state s); #F E; nwhd in E:(??%?);
904                ndestruct (E);
905            ##| ##3,6: #E; nwhd in E:(??%?); ndestruct (E);
906            ##]
907        ##]
908    ##]
909##]
910nqed.   
911
912ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
913| emb_terminates: ∀s,e,tr,r,m.
914    execution_terminates tr s e r m →
915    execution_matches_behavior e (Terminates tr r)
916| emb_diverges: ∀s,e,tr.
917    execution_diverges tr s e →
918    execution_matches_behavior e (Diverges tr)
919| emb_reacts: ∀s,e,tr.
920    execution_reacts tr s e →
921    execution_matches_behavior e (Reacts tr)
922| emb_wrong: ∀e,s,s',tr.
923    execution_goes_wrong tr s e s' →
924    execution_matches_behavior e (Goes_wrong tr)
925| emb_initially_wrong:
926    execution_matches_behavior e_wrong (Goes_wrong E0).
927
928nlemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
929  execution_terminates tr s (e_step tr' s' e) r m → s = s'.
930#tr tr' s s' e r m H; ninversion H;
931##[ #s1 s2 tr1 tr2 r' e' m' H' E1 E2 E3 E4 E5; ndestruct; napply refl
932##| #s1 s2 tr1 tr2 r' e' m' o k i H' E1 E2 E3 E4 E5 E6; ndestruct; napply refl
933##] nqed.
934
935nlemma exec_state_diverges: ∀tr,tr',s,s',e.
936  execution_diverges tr s (e_step tr' s' e) → s = s'.
937#tr tr' s s' e H; ninversion H;
938#tr1 s1 s2 e1 e2 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
939
940nlemma exec_state_reacts: ∀tr,tr',s,s',e.
941  execution_reacts tr s (e_step tr' s' e) → s = s'.
942#tr tr' s s' e H; ninversion H;
943#tr1 s1 e1 H' E1 E2 E3; ndestruct; napply refl; nqed.
944
945nlemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
946  execution_goes_wrong tr s (e_step tr' s' e) s'' → s = s'.
947#tr tr' s s' s'' e H; ninversion H;
948#tr1 s1 s2 e1 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
949
950nlemma behavior_of_execution: ∀s,e.
951  execution_characterisation s e →
952  ∃b:program_behavior. execution_matches_behavior e b.
953#s0 e0 exec;
954ncases exec;
955##[ #s r m e tr TERM;
956    @ (Terminates tr r);
957    napply (emb_terminates … TERM);
958##| #s e tr DIV;
959    @ (Diverges tr);
960    napply (emb_diverges … DIV);
961##| #s e tr REACTS;
962    @ (Reacts tr);
963    napply (emb_reacts … REACTS);
964##| #e s s' tr WRONG;
965    @ (Goes_wrong tr);
966    napply (emb_wrong … WRONG);
967##] nqed.
968
969nlemma initial_state_not_final: ∀ge,s.
970  initial_state ge s →
971  ¬ ∃r.final_state s r.
972#ge s H; ncases H;
973#b f E1 E2; @; *; #r H2;
974ninversion H2;
975#r' m E3 E4; ndestruct (E3);
976nqed.
977
978nlemma initial_step: ∀ge,s,e.
979  exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
980  ¬(∃r.final_state s r) →
981  ∃e'.e = e_step E0 s e'.
982#ge s e; nrewrite > (exec_inf_aux_unfold …);
983nwhd in ⊢ (??%? → ?); ncases (is_final_state s);
984##[ #FINAL EXEC NOTFINAL;
985    napply False_ind; napply (absurd ?? NOTFINAL);
986    ncases FINAL;
987    #r F; @r; napply F;
988##| #F1 EXEC F2; nwhd in EXEC:(??%?); @; ##[ ##2: nrewrite < EXEC; napply refl ##]
989nqed.
990
991ntheorem exec_inf_sound:
992  ∀classic:(∀P:Prop.P ∨ ¬P).
993  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
994  ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b.
995#classic constructive_indefinite_description p;
996nwhd in ⊢ (??(λ_.?(?%?)%)); nletin ge ≝ (globalenv Genv fundef type p);
997nlapply (make_initial_state_sound p);
998nlapply (the_initial_state p);
999ncases (make_initial_state p);
1000##[ #s INITIAL' INITIAL; nwhd in INITIAL ⊢ (??(λ_.?(?(??%)?)?));
1001    nlapply (behavior_of_execution ??
1002              (execution_characterisation_complete classic constructive_indefinite_description ge s ?));
1003    ##[ napply (initial_state_not_final … INITIAL);
1004    ##| *; #b MATCHES; @b; @; //;
1005        ninversion MATCHES;
1006        ##[ #s0 e tr r m TERM EXEC BEHAVES;
1007            nlapply (initial_step … EXEC ?);
1008            ##[ napply initial_state_not_final; //; ##]
1009            *; #e' E2; nrewrite > E2 in EXEC TERM; #EXEC TERM;
1010            nlapply (exec_state_terminates … TERM); #E1;
1011            nrewrite > E1 in TERM; #TERM;
1012            napply (program_terminates (mk_transrel … step) ?? ge s);
1013            ##[ ##2: napply INITIAL
1014            ##| ##3: napply (terminates_sound … TERM EXEC);
1015            ##| ##skip
1016            ##| //;
1017            ##]
1018        ##| #s0 e tr DIVERGES EXEC E2;
1019            nlapply (initial_step … EXEC ?);
1020            ##[ napply initial_state_not_final; //; ##]
1021            *; #e' E3; nrewrite > E3 in DIVERGES EXEC ⊢ %;
1022            #DIVERGES EXEC; nlapply (exec_state_diverges … DIVERGES);
1023            #E1; nrewrite > E1 in DIVERGES; #DIVERGES;
1024            ninversion DIVERGES; #tr' s1 s2 e1 e2 INITSTEPS DIVERGING E4 E5 E6;
1025            nrewrite < E4 in INITSTEPS ⊢ %; nrewrite < E5 in E6 ⊢ %; #E6 INITSTEPS;
1026            ncut (e' = e1); ##[ ndestruct (E6) skip (MATCHES EXEC); // ##]
1027            #E7; nrewrite < E7 in INITSTEPS; #INITSTEPS;
1028            ncases (several_steps … INITSTEPS EXEC); #INITSTAR EXECDIV;
1029            napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL INITSTAR);
1030            napply (silent_sound … DIVERGING EXECDIV);
1031        ##| #s0 e tr REACTS EXEC E2;
1032            nlapply (initial_step … EXEC ?);
1033            ##[ napply initial_state_not_final; //; ##]
1034            *; #e' E3; nrewrite > E3 in EXEC REACTS ⊢ %;
1035            #EXEC REACTS;
1036            nlapply (exec_state_reacts … REACTS);
1037            #E1; nrewrite > E1 in REACTS; #REACTS;
1038            ninversion REACTS; #tr' s' e'' REACTING E4 E5;
1039            nrewrite < E4 in REACTING ⊢ %; nrewrite < E5; #REACTING E6;
1040            ncut (e' = e''); ##[ ndestruct (E6) skip (MATCHES EXEC); // ##]
1041            #E7; nrewrite < E7 in REACTING; #REACTING;
1042            napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL);
1043            napply (reacts_sound … REACTING EXEC);
1044        ##| #e s1 s2 tr WRONG EXEC E2;
1045            nlapply (initial_step … EXEC ?);
1046            ##[ napply initial_state_not_final; //; ##]
1047            *; #e' E3; nrewrite > E3 in EXEC WRONG ⊢ %;
1048            #EXEC WRONG;
1049            nlapply (exec_state_wrong … WRONG);
1050            #E1; nrewrite > E1 in WRONG; #WRONG;
1051            ninversion WRONG; #tr' s1' s2' e'' GOESWRONG E4 E5 E6 E7;
1052            nrewrite < E4 in GOESWRONG ⊢ %; nrewrite < E5; nrewrite < E7; #GOESWRONG;
1053            ncut (e' = e''); ##[ ndestruct (E6) skip (MATCHES EXEC); // ##]
1054            #E8; nrewrite < E8 in GOESWRONG; #GOESWRONG;
1055            nelim (wrong_sound … WRONG EXEC); *; #STAR STOP FINAL;
1056            napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL STAR STOP);
1057            #r; @; #F; napply (absurd ?? FINAL); @r; napply F;
1058        ##| nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
1059            ncases (is_final_state s); #F EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
1060        ##]
1061   ##]
1062##| nwhd in ⊢ ((∀_.? → %) → ?);
1063    #NOINIT WHATEVER;
1064    @ (Goes_wrong E0); @;
1065    ##[ nwhd in ⊢ (?(??%)?);
1066        nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (?%?);
1067        napply emb_initially_wrong;
1068    ##| napply program_goes_initially_wrong;
1069        #s; @; napply NOINIT;
1070    ##]
1071##] nqed.
1072
Note: See TracBrowser for help on using the repository browser.