source: C-semantics/CexecIOcomplete.ma @ 393

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

A few more details in D3.1.

File size: 47.1 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 alloc_vars_complete: ∀env,m,l,env',m'.
328  alloc_variables env m l env' m' →
329  ∃p.exec_alloc_variables env m l = sig_intro ?? (Some ? 〈env', m'〉) p.
330#env m l env' m' H; nelim H;
331##[ #env'' m''; @ ?; nwhd; //;
332##| #env1 m1 id ty l1 m2 loc m3 env2 H1 H2 H3;
333    nwhd in H1:(??%?) ⊢ (??(λ_.??%?));
334    ndestruct (H1);
335    nelim H3; #p3 e3; nrewrite > e3; nwhd in ⊢ (??(λ_.??%?)); @ ?; //;
336##] nqed.
337
338nlemma bind_params_complete: ∀e,m,params,vs,m2.
339  bind_parameters e m params vs m2 →
340  yields ?? (exec_bind_parameters e m params vs) m2.
341#e m params vs m2 H; nelim H;
342##[ //;
343##| #env1 m1 id ty l v tl loc m2 m3 H1 H2 H3 H4;
344    napply remove_res_sig;
345    nrewrite > H1; nwhd in ⊢ (??%?);
346    nrewrite > H2; nwhd in ⊢ (??%?);
347    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4;
348    napply refl;
349##] nqed.
350
351nlemma eventval_match_complete': ∀ev,ty,v.
352  eventval_match ev ty v → yields ?? (check_eventval' v ty) ev.
353#ev ty v H; nelim H; //; nqed.
354
355nlemma eventval_list_match_complete: ∀vs,tys,evs.
356  eventval_list_match evs tys vs → yields ?? (check_eventval_list vs tys) evs.
357#vs tys evs H; nelim H;
358##[ //
359##| #e etl ty tytl v vtl H1 H2 H3; napply remove_res_sig;
360    nelim (yields_eq ???? (eventval_match_complete' … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
361    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
362    napply refl;
363##] nqed.
364
365nlemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inl ?? p')) → Q f.
366#P f p Q H; ncases f;
367##[ napply H
368##| #np; napply False_ind; napply (absurd ? p np);
369##] nqed.
370
371nlemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inr ?? p')) → Q f.
372#P f p Q H; ncases f;
373##[ #np; napply False_ind; napply (absurd ? np p);
374##| napply H
375##] nqed.
376
377ntheorem step_complete: ∀ge,s,tr,s'.
378  step ge s tr s' → yieldsIObare ? (exec_step ge s) 〈tr,s'〉.
379#ge s tr s' H; nelim H;
380##[ #f e e1 k e2 m sp loc ofs v m' tr1 tr2 H1 H2 H3; nwhd in ⊢ (??%?);
381    nrewrite > (yieldsbare_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
382    nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
383    nrewrite > H3; napply refl;
384##| #f e eargs k ef m vf vargs f' tr1 tr2 H1 H2 H3 H4; nwhd in ⊢ (??%?);
385    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
386    nrewrite > (yieldsbare_eq ??? (exprlist_complete … H2)); nwhd in ⊢ (??%?);
387    nrewrite > H3; nwhd in ⊢ (??%?);
388    nrewrite > H4; nelim (assert_type_eq_true (typeof e)); #pty ety; nrewrite > ety;
389    napply refl;
390##| #f el ef eargs k env m sp loc ofs vf vargs f' tr1 tr2 tr3 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?);
391    nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
392    nrewrite > (yieldsbare_eq ??? (exprlist_complete … H3)); nwhd in ⊢ (??%?);
393    nrewrite > H4; nwhd in ⊢ (??%?);
394    nrewrite > H5; nelim (assert_type_eq_true (typeof ef)); #pty ety; nrewrite > ety;
395    nwhd in ⊢ (??%?);
396    nrewrite > (yieldsbare_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
397    napply refl;
398##| #f s1 s2 k env m; napply refl
399##| ##5,6,7: #f s k env m; 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_true ?? H2));
403    napply refl
404##| #f e s1 s2 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_false ?? H2));
411    napply refl
412##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?);
413    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
414    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
415    napply refl
416##| #f s1 e s2 k env m H; ncases H; #es1; nrewrite > es1; napply refl;
417##| ##13,14: #f e s k env m; 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_false ?? H2));
421    napply refl
422##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?);
423    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
424    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
425    napply refl
426##| #f e s k env m; napply refl;
427##| #f s1 e s2 s3 k env m nskip; nwhd in ⊢ (??%?); ncases (is_Sskip s1);
428    ##[ #H; napply False_ind; /2/;
429    ##| #H; nwhd in ⊢ (??%?); 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_false ?? H2));
433    napply refl;
434##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
435    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
436    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
437    napply refl;
438##| #f s1 e s2 s3 k env m; *; #es1; nrewrite > es1; napply refl;
439##| ##22,23: #f e s1 s2 k env m; napply refl;
440##| #f k env m H; nwhd in ⊢ (??%?); nrewrite > H; napply refl;
441##| #f e k env m v tr H1 H2; nwhd in ⊢ (??%?);
442    napply (dec_false ? (type_eq_dec (fn_return f) Tvoid) H1); #pf';
443    nwhd in ⊢ (??%?);
444    nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
445    napply refl;
446##| #f k env m; ncases k;
447    ##[ #H1 H2; nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
448    ##| #s' k'; nwhd in ⊢ (% → ?); *;
449    ##| ##3,4: #e' s' k'; nwhd in ⊢ (% → ?); *;
450    ##| ##5,6: #e' s1' s2' k'; nwhd in ⊢ (% → ?); *;
451    ##| #k'; nwhd in ⊢ (% → ?); *;
452    ##| #r f' env' k' H1 H2; nwhd in ⊢ (??%?); nrewrite > H2; napply refl
453    ##]
454##| #f e s k env m i tr H1; nwhd in ⊢ (??%?);
455    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
456    napply refl
457##| #f s k env m; *; #es; nrewrite > es; napply refl;
458##| #f k env m; napply refl
459##| #f l s k env m; napply refl
460##| #f l k env m s k' H1; nwhd in ⊢ (??%?); nrewrite > H1; napply refl;
461##| #f args k m1 env m2 m3 H1 H2; nwhd in ⊢ (??%?);
462    nelim (alloc_vars_complete … H1); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
463    nelim (yields_eq ???? (bind_params_complete … H2)); #p2 e2; nrewrite > e2;
464    napply refl;
465##| #id tys rty args k m rv tr H; nwhd in ⊢ (??%?);
466    ninversion H; #f' args' rv' eargs erv H1 H2 e1 e2 e3 e4; nrewrite < e1 in H1 H2;
467    #H1 H2;
468    nelim (yields_eq ???? (eventval_list_match_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
469    nwhd; ninversion H2; #x e5 e6 e7; @ x; nwhd in ⊢ (??%?);
470    napply refl
471##| #v f env k m; napply refl
472##| #v f env k m1 m2 sp loc ofs ty H; nwhd in ⊢ (??%?);
473    nrewrite > H; napply refl
474##| #f l s k env m; napply refl
475##] nqed.
476 
477nlemma wrong_sound: ∀ge,tr,s,s',e.
478  execution_goes_wrong tr s (e_step E0 s e) s' →
479  exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e →
480  star (mk_transrel … step) ge s tr s' ∧
481  nostep (mk_transrel … step) ge s' ∧
482  (¬∃r. final_state s' r).
483#ge tr0 s0 s0' e0 WRONG; ncases WRONG;
484#tr s s' e ESTEPS EXEC;
485ncases (several_steps … ESTEPS EXEC);
486#STAR EXEC'; @;
487##[ @; ##[ napply STAR;
488       ##| #badtr bads; @; #badSTEP;
489           nlapply (step_complete … badSTEP);
490           nlapply (exec_e_step … EXEC');
491           ncases (exec_step ge s');
492           ##[ #o k; nrewrite > (execution_cases (exec_inf_aux …)); #E; nwhd in E:(??%?);
493               ndestruct
494           ##| #x; ncases x; #trx stx; nrewrite > (exec_inf_aux_unfold …);
495               nwhd in ⊢ (??%? → ?); ncases (is_final_state stx);
496               #FINAL E; nwhd in E:(??%?); ndestruct
497           ##| #E H; nwhd in H; napply H
498           ##]
499       ##]
500##| @; #FINAL;
501    nrewrite > (exec_inf_aux_unfold …) in EXEC';
502    nwhd in ⊢ (??%? → ?);
503    ncases (is_final_state s'); #FINAL';
504    ##[ nwhd in ⊢ (??%? → ?); #E; ndestruct;
505    ##| napply False_ind; napply (absurd … FINAL FINAL');
506    ##]
507##] nqed.
508
509ninductive execution_characterisation : state → execution → Prop ≝
510| ec_terminates: ∀s,r,m,e,tr.
511    execution_terminates tr s e r m →
512    execution_characterisation s e
513| ec_diverges: ∀s,e,tr.
514    execution_diverges tr s e →
515    execution_characterisation s e
516| ec_reacts: ∀s,e,tr.
517    execution_reacts tr s e →
518    execution_characterisation s e
519| ec_wrong: ∀e,s,s',tr.
520    execution_goes_wrong tr s e s' →
521    execution_characterisation s e.
522
523(* bit of a hack to avoid inability to reduce term in match *)
524ndefinition interact_prop : ∀A:Type.(∀o:io_out. (io_in o → IO io_out io_in A) → Prop) → IO io_out io_in A → Prop ≝
525λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ].
526
527nlemma err_does_not_interact: ∀A,B,P,e1,e2.
528  (∀x:B.interact_prop A P (e2 x)) →
529  interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2).
530#A B P e1 e2 H;
531ncases e1; //; nqed.
532
533nlemma err2_does_not_interact: ∀A,B,C,P,e1,e2.
534  (∀x,y.interact_prop A P (e2 x y)) →
535  interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2).
536#A B C P e1 e2 H;
537ncases e1; ##[ #z; ncases z; ##] //; nqed.
538
539nlemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2.
540  (∀x.interact_prop A P (e2 x)) →
541  interact_prop A P (bindIO ?? (sigma B Q) A (err_to_io_sig ??? Q e1) e2).
542#A B P Q e1 e2 H;
543ncases e1; //; nqed.
544
545nlemma opt_does_not_interact: ∀A,B,P,e1,e2.
546  (∀x:B.interact_prop A P (e2 x)) →
547  interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2).
548#A B P e1 e2 H;
549ncases e1; //; nqed.
550
551nlemma exec_step_interaction:
552  ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s).
553#ge s; ncases s;
554##[ #f st kk e m; ncases st;
555  ##[ ##11,14: #a ##| ##2,4,6,7,12,13,15: #a b ##| ##3,5: #a b c ##| ##8: #a b c d ##]
556  ##[ ##4,6,8,9: napply I ##]
557  nwhd in ⊢ (???%);
558  ##[ ncases a; ##[ ncases (fn_return f); //; ##| #e; nwhd nodelta in ⊢ (???%);
559                    ncases (type_eq_dec (fn_return f) Tvoid); #x; //; napply err2_does_not_interact; // ##]
560  ##| ncases (find_label a (fn_body f) (call_cont kk)); ##[ napply I ##| #z; ncases z; #x y; napply I ##]
561  ##| napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5; napply I
562  ##| ##4,7: napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I
563  ##| napply err2_does_not_interact; #x1 x2; ncases x1; //;
564  ##| 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;
565      ##[ napply I; ##| #x7; napply err2_does_not_interact; #x8 x9; napply I ##]
566  ##| ncases (is_Sskip a); #H; ##[ napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I
567      ##| napply I ##]
568  ##| ncases kk; ##[ ##1,8: ncases (fn_return f); //; ##| ##2,3,5,6,7: //;
569      ##| #z1 z2 z3; napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I ##]
570  ##| ncases kk; //;
571  ##| ncases kk; ##[ ##4: #z1 z2 z3;  napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I
572      ##| ##*: // ##]
573  ##]
574##| #f args kk m; ncases f;
575  ##[ #f'; nwhd in ⊢ (???%); ncases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'));
576      #x; ncases x; ##[ *; ##| #z; ncases z; #x1 x2 H;
577                        napply err_sig_does_not_interact; //; ##]
578  (* This is the only case that actually matters! *)
579  ##| #fn argtys rty; nwhd in ⊢ (???%);
580      napply  err_sig_does_not_interact; #x1;
581      nwhd; #i; @; ##[ ##2: @; ##[ ##2: @; ##[ @; nwhd in ⊢ (??%?); napply refl;
582        ##| @; #E; nwhd in E:(??%%); ndestruct (E); ##] ##] ##]
583  ##]
584##| #v kk m; nwhd in ⊢ (???%); ncases kk;
585    ##[ ##8: #x1 x2 x3 x4; ncases x1;
586      ##[ nwhd in ⊢ (???%); ncases v; // ##| #x5; nwhd in ⊢ (???%); ncases x5;
587          #x6 x7; napply opt_does_not_interact; // ##]
588    ##| ##*: // ##]
589##] nqed.
590
591
592(* Some classical logic (roughly like a fragment of Coq's library) *)
593nlemma classical_doubleneg:
594  ∀classic:(∀P:Prop.P ∨ ¬P).
595  ∀P:Prop. ¬ (¬ P) → P.
596#classic P; *; #H;
597ncases (classic P);
598##[ // ##| #H'; napply False_ind; /2/; ##]
599nqed.
600
601nlemma classical_not_all_not_ex:
602  ∀classic:(∀P:Prop.P ∨ ¬P).
603  ∀A:Type.∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x.
604#classic A P; *; #H;
605napply (classical_doubleneg classic); @; *; #H';
606napply H; #x; @; #H''; napply H'; @x; napply H'';
607nqed.
608
609nlemma classical_not_all_ex_not:
610  ∀classic:(∀P:Prop.P ∨ ¬P).
611  ∀A:Type.∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x.
612#classic A P; *; #H;
613napply (classical_not_all_not_ex classic A (λx.¬ P x));
614@; #H'; napply H; #x; napply (classical_doubleneg classic);
615napply H';
616nqed.
617
618nlemma not_ex_all_not:
619  ∀A:Type.∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x.
620#A P; *; #H x; @; #H';
621napply H; @ x; napply H';
622nqed.
623
624nlemma not_imply_elim:
625  ∀classic:(∀P:Prop.P ∨ ¬P).
626  ∀P,Q:Prop. ¬ (P → Q) → P.
627#classic P Q; *; #H;
628napply (classical_doubleneg classic); @; *; #H';
629napply H; #H''; napply False_ind; napply H'; napply H'';
630nqed.
631
632nlemma not_imply_elim2:
633  ∀P,Q:Prop. ¬ (P → Q) → ¬ Q.
634#P Q; *; #H; @; #H';
635napply H; #_; napply H';
636nqed.
637
638nlemma imply_to_and:
639  ∀classic:(∀P:Prop.P ∨ ¬P).
640  ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q.
641#classic P Q H; @;
642##[ napply (not_imply_elim classic P Q H);
643##| napply (not_imply_elim2 P Q H);
644##] nqed.
645
646nlemma not_and_to_imply:
647  ∀classic:(∀P:Prop.P ∨ ¬P).
648  ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q.
649#classic P Q; *; #H H';
650@; #H''; napply H; @; //;
651nqed.
652
653ninductive execution_not_over : execution → Prop ≝
654| eno_step: ∀tr,s,e. execution_not_over (e_step tr s e)
655| eno_interact: ∀o,k,tr,s,e,i.
656    k i = e_step tr s e →
657    execution_not_over (e_interact o k).
658
659nlemma eno_stop: ∀tr,r,m. execution_not_over (e_stop tr r m) → False.
660#tr0 r0 m0 H; ninversion H;
661##[ #tr s e E; ndestruct
662##| #o k tr s e i K E; ndestruct
663##] nqed.
664
665nlemma eno_wrong: execution_not_over e_wrong → False.
666#H; ninversion H;
667##[ #tr s e E; ndestruct
668##| #o k tr s e i K E; ndestruct
669##] nqed.
670
671nlet corec show_divergence s e
672 (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
673                 execution_not_over e1)
674 (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0)
675 (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)
676 : execution_diverging e ≝ ?.
677nlapply (NONTERMINATING E0 s e ?); //;
678ncases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %;
679##[ #tr i m; #_; #_; #_; #ENO; nelim (eno_stop … ENO);
680##| #tr s' e' UNREACTIVE; nlapply (UNREACTIVE tr s' e' ?);
681  ##[ nrewrite < (E0_right tr) in ⊢ (?%????);
682      napply isteps_one; napply isteps_none;
683  ##| #TR; napply (match sym_eq ??? TR with [ refl ⇒ ? ]); (* nrewrite > TR in UNREACTIVE ⊢ %;*)
684      #NONTERMINATING CONTINUES; #_; @;
685      napply (show_divergence s');
686      ##[ #tr1 s1 e1 S; napply (NONTERMINATING tr1 s1 e1);
687        nchange in ⊢ (?%????) with (Eapp E0 tr1); napply isteps_one;
688        napply S;
689      ##| #tr2 s2 e2 S; nrewrite > TR in UNREACTIVE; #UNREACTIVE; napply (UNREACTIVE tr2 s2 e2);
690          nchange in ⊢ (?%????) with (Eapp E0 tr2);
691          napply isteps_one; napply S;
692      ##| #tr2 s2 o k S; napply (CONTINUES tr2 s2 o k);
693          nchange in ⊢ (?%????) with (Eapp E0 tr2);
694          napply isteps_one; napply S;
695      ##]
696  ##]
697##| #_; #_; #_; #ENO; nelim (eno_wrong … ENO);
698##| #o k UNREACTIVE NONTERMINATING CONTINUES; #_;
699    nlapply (CONTINUES E0 s o k ?);
700    ##[ napply isteps_none;
701    ##| *; #i; *; #tr'; *; #s'; *; #e'; *; #EXEC NOTSILENT;
702        napply False_ind; napply (absurd ?? NOTSILENT);
703        napply (UNREACTIVE … s' e');
704        nrewrite < (E0_right tr') in ⊢ (?%????);
705        napply (isteps_interact … EXEC); //;
706    ##]
707##] nqed.
708
709nlemma exec_over_isteps: ∀ge,tr,s,s',e,e'.
710  execution_isteps tr s e s' e' →
711  e = (exec_inf_aux ge (exec_step ge s)) →
712  exec_inf_aux ge (exec_step ge s') = e'.
713#ge tr0 s0 s0' e0 e0';
714#ISTEPS; nelim ISTEPS;
715##[ #s e E; nrewrite > E; napply refl;
716##| #e1 e2 tr1 tr2 s1 s2 s3 ISTEPS' IH E;
717    napply IH; napply sym_eq; napply exec_e_step;
718    ##[ ##3: napply sym_eq; napply E ##]
719##| #e1 e2 o k i s1 s2 s3 tr1 tr2 ISTEPS' EXECK IH E;
720    napply IH;
721    ncases (exec_step ge s3) in E;
722    ##[ #o' k'; nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
723        #E'; nwhd in E':(???%); ndestruct (E');
724        napply sym_eq; napply exec_e_step;
725        ##[ ##3: napply EXECK; ##]
726    ##| #z; ncases z; #tr' s';
727        nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
728        nwhd in ⊢ (???% → ?); ncases (is_final_state s');
729        #F E'; nwhd in E':(???%); ndestruct (E');
730    ##| nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
731        #E'; nwhd in E':(???%); ndestruct (E');
732    ##]
733##] nqed.
734
735nlemma exec_over_isteps': ∀ge,tr,s,s',e'.
736  execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s' e' →
737  exec_inf_aux ge (exec_step ge s') = e'.
738#ge tr s s' e'; nletin e ≝ (exec_inf_aux ge (exec_step ge s)); #H;
739napply (exec_over_isteps … H (refl ??));
740nqed.
741
742nlemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
743  exec_inf_aux ge (exec_step ge s) = e_interact o k →
744  k i = e_step tr s' e →
745  tr ≠ E0.
746#ge o k i tr s s' e; nrewrite > (exec_inf_aux_unfold …);
747nlapply (exec_step_interaction ge s);
748ncases (exec_step ge s);
749##[ #o' k' ; nwhd in ⊢ (% → ??%? → ?); #H E K; ndestruct (E);
750    nlapply (H i); *; #tr'; *; #s''; *; #K' TR;
751    nrewrite > K' in K; nrewrite > (exec_inf_aux_unfold …);
752    nwhd in ⊢ (??%? → ?);
753    ncases (is_final_state s'');
754    ##[ #F; nwhd in ⊢ (??%? → ?); #E; ndestruct (E);
755    ##| #F; nwhd in ⊢ (??%? → ?); #E; ndestruct (E);
756        napply TR
757    ##]
758##| #x; ncases x; #tr' s'' H; nwhd in ⊢ (??%? → ?);
759    ncases (is_final_state s''); #F E; nwhd in E:(??%?); ndestruct (E);
760##| #_; #E; nwhd in E:(??%?); ndestruct (E);
761##] nqed.
762
763nlet corec reactive_traceinf' ge s
764  (REACTIVE: ∀tr,s1,e1.
765    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
766    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
767  : traceinf' ≝ ?.
768nlapply (REACTIVE E0 s (exec_inf_aux ge (exec_step ge s)) ?);
769##[ napply isteps_none
770##| *; #x; ncases x; #tr; #y; ncases y; #s' e; *; #STEPS H;
771    @ tr ? H;
772    napply (reactive_traceinf' ge s');
773    #tr1 s1 e1 STEPS1;
774    napply REACTIVE;
775    ##[ ##2: nrewrite > (exec_over_isteps' … STEPS) in STEPS1; #STEPS1;
776        napply (isteps_trans … STEPS STEPS1);
777    ##| ##skip
778    ##]
779##]
780nqed.
781
782(* A slightly different version of the above, to work around a problem with the
783   next result. *)
784nlet corec reactive_traceinf'' ge s
785  (REACTIVE0: Σx.execution_isteps (\fst x) s (exec_inf_aux ge (exec_step ge s)) (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
786  (REACTIVE: ∀tr,s1,e1.
787    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
788    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
789  : traceinf' ≝ ?.
790ncases REACTIVE0; #x; ncases x; #tr; #y; ncases y; #s' e; *; #STEPS H;
791    @ tr ? H;
792    napply (reactive_traceinf'' ge s');
793    ##[ napply REACTIVE; ##[ ##2: nlapply (exec_over_isteps' … STEPS);
794                                  #E; nrewrite > E in STEPS;
795                                  #STEPS; napply STEPS; ##]
796    ##|
797    #tr1 s1 e1 STEPS1;
798    napply REACTIVE;
799    ##[ ##2: nrewrite > (exec_over_isteps' … STEPS) in STEPS1; #STEPS1;
800        napply (isteps_trans … STEPS STEPS1);
801    ##| ##skip
802    ##]
803##]
804nqed.
805
806(* We want to prove
807
808nlemma show_reactive : ∀ge,s.
809  ∀REACTIVE:∀tr,s1,e1.
810    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
811    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
812  execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)).
813 
814but the current matita won't unfold reactive_traceinf' so that we can do case
815analysis on (REACTIVE …).  Instead we take an "applied" version of REACTIVE that
816we can do case analysis on, then get it into the desired form afterwards.
817*)
818nlet corec show_reactive' ge s
819  (REACTIVE0: Σx.execution_isteps (\fst x) s (exec_inf_aux ge (exec_step ge s)) (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
820  (REACTIVE: ∀tr1,s1,e1.
821    execution_isteps tr1 s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
822    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
823  : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s REACTIVE0 REACTIVE)) s (exec_inf_aux ge (exec_step ge s)) ≝ ?.
824(*nrewrite > (unroll_traceinf' (reactive_traceinf'' …));*)
825napply (match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ]);
826ncases REACTIVE0;
827#x; ncases x; #tr1; #y; ncases y; #s1 e1; #z; ncases z; #STEPS NOTSILENT;
828nwhd in ⊢ (?(?%)??);
829(*nrewrite > (traceinf_traceinfp_app …);*)
830napply (match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ]);
831napply (reacting … STEPS NOTSILENT);
832(*nrewrite < (exec_over_isteps' … STEPS) in ⊢ (???%);*)
833napply (match (exec_over_isteps' … STEPS) return λe'.λ_.
834?(?(reactive_traceinf'' ??
835(REACTIVE ??? (eq_ind_r execution e1 (λx.λ_.execution_isteps ???? e1 → ?) (λS.S) ? (exec_over_isteps' ???? e1 STEPS) STEPS))
836(λtr2,s2,e2,S1.REACTIVE ? s2 e2 (eq_ind_r execution e1 (λx.λ_:x=e1.execution_isteps tr2 s1 x s2 e2 → ?) (λS.isteps_trans ?????? e1 ? STEPS S) ? (exec_over_isteps' ???? e1 STEPS) S1))
837))? e'
838 with [ refl ⇒ ? ]);
839napply show_reactive';
840nqed.
841
842nlemma show_reactive : ∀ge,s.
843  ∀REACTIVE:∀tr,s1,e1.
844    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
845    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
846  execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s ? REACTIVE)) s (exec_inf_aux ge (exec_step ge s)).
847##[
848#ge s REACTIVE;
849napply show_reactive';
850##| napply (REACTIVE … (isteps_none …));
851##] nqed.
852
853nlemma execution_characterisation_complete:
854  ∀classic:(∀P:Prop.P ∨ ¬P).
855  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
856   ∀ge,s. ¬ (∃r. final_state s r) →
857   execution_characterisation s (exec_inf_aux ge (Value ??? 〈E0,s〉)).
858#classic constructive_indefinite_description ge s; *; #NOTFINAL;
859nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%);
860ncases (is_final_state s); ##[ #x; ncases x; #r FINAL; napply False_rect_Type0; napply NOTFINAL; @r; napply FINAL ##]
861#NOTFINAL'; nwhd in ⊢ (??%);
862ncases (classic (∀tr1,s1,e1. execution_isteps tr1 s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
863                 execution_not_over e1));
864##[ #NONTERMINATING;
865    ncases (classic (∃tr,s1,e1. execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 ∧
866                     ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0));
867  ##[ *; #tr; *; #s1; *; #e1; *; #INITIAL UNREACTIVE;
868      napply (ec_diverges … s ? tr);
869      napply (diverges_diverging … INITIAL);
870      napply (show_divergence s1);
871      ##[ #tr2 s2 e2 S; napply (NONTERMINATING (Eapp tr tr2) s2 e2);
872          napply (isteps_trans … INITIAL S);
873      ##| #tr2 s2 e2 S; napply (UNREACTIVE … S);
874      ##| #tr2 s2 o; ncases o; #o_id o_args o_typ; ncases o_typ; #k S;
875          nlapply (exec_over_isteps … INITIAL (refl ??)); #EXEC1;
876          nlapply (exec_over_isteps … S (sym_eq … EXEC1));
877          nlapply (NONTERMINATING (Eapp tr tr2) s2 (e_interact (mk_io_out o_id o_args ?) k) ?);
878          ##[ ##1,3: napply (isteps_trans … INITIAL S); ##]
879          #NOTOVER; ninversion NOTOVER;
880          ##[ ##1,3: #tr' s' e' E; ndestruct (E);
881          ##| ##*: #o' k' tr' s' e' i' KR E; ndestruct (E);
882              #EXEC;
883              @ i'; @ tr'; @s'; @e'; @;//; napply (interaction_is_not_silent … EXEC KR);
884          ##]
885      ##]
886
887  ##| *; #NOTUNREACTIVE;
888      ncut (∀tr,s1,e1.execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
889            ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0);
890      ##[ #tr s1 e1 STEPS;
891          napply (classical_doubleneg classic); @; #NOREACTION;
892          napply NOTUNREACTIVE;
893          @ tr; @s1; @e1; @; //;
894          #tr2 s2 e2 STEPS2;
895          nlapply (not_ex_all_not … NOREACTION); #NR1;
896          nlapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2;
897          napply (classical_doubleneg classic);
898          napply NR2; //;
899      ##| #REACTIVE;
900          napply ec_reacts;
901          ##[ ##2: napply reacts;
902                   napply (show_reactive ge s …);
903                   #tr s1 e1 STEPS;
904                   napply constructive_indefinite_description;
905                   napply (REACTIVE … tr s1 e1 STEPS);
906          ##| ##skip
907          ##]
908      ##]
909  ##]
910 
911##| #NOTNONTERMINATING; nlapply (classical_not_all_ex_not classic … NOTNONTERMINATING);
912    *; #tr NNT2; nlapply (classical_not_all_ex_not classic … NNT2);
913    *; #s' NNT3; nlapply (classical_not_all_ex_not classic … NNT3);
914    *; #e NNT4; nelim (imply_to_and classic … NNT4);
915    ncases e;
916    ##[ #tr' r m; #STEPS NOSTEP;
917        napply (ec_terminates s r m ? (Eapp tr tr')); @;
918        ##[ napply s'
919        ##| napply STEPS
920        ##]
921    ##| #tr' s'' e' STEPS; *; #NOSTEP; napply False_rect_Type0;
922        napply NOSTEP; //
923    ##| #STEPS NOSTEP;
924        napply (ec_wrong ? s s' tr); @; //;
925    (* The following is stupidly complicated when most of the cases are impossible.
926       It ought to be simplified. *)
927    ##| #o; ncases o; #o_id o_args o_rty; ncases o_rty; #k STEPS NOSTEP;
928        ##[ nletin i ≝ (repr 0) ##| nletin i ≝ Fzero ##]
929        nlapply (refl ? (k i));
930        ncases (k i) in ⊢ (???% → ?);
931        ##[ ##1,5: #tr' r m K;
932                   napply (ec_terminates s ???);
933                   ##[ ##4,8: napply (annoying_corner_case_terminates … STEPS K);
934                   ##| ##*: ##skip
935                   ##]
936        ##| ##2,6: #tr' s'' e' K; napply False_rect_Type0;
937            napply (absurd ?? NOSTEP);
938            napply (eno_interact … K);
939        ##| ##3,7: #K;
940            nlapply (exec_step_interaction ge s');
941            nlapply (exec_over_isteps … STEPS (refl ??));
942            nrewrite > (exec_inf_aux_unfold …); ncases (exec_step ge s');
943            ##[ ##1,4: #o k E H; nwhd in E:(??%?) H;
944                ndestruct (E);
945                nlapply (H i); *; #tr'; *; #s'; *; #K'; nrewrite > K' in K;
946                nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
947                ncases (is_final_state s'); #F E; nwhd in E:(??%?);
948                ndestruct (E);
949            ##| ##2,5: #z; ncases z; #tr s; nwhd in ⊢ (??%? → ?);
950                ncases (is_final_state s); #F E; nwhd in E:(??%?);
951                ndestruct (E);
952            ##| ##3,6: #E; nwhd in E:(??%?); ndestruct (E);
953            ##]
954        ##| ##4,8: #o0 k0 K;
955            nlapply (exec_step_interaction ge s');
956            nlapply (exec_over_isteps … STEPS (refl ??));
957            nrewrite > (exec_inf_aux_unfold …); ncases (exec_step ge s');
958            ##[ ##1,4: #o k E H; nwhd in E:(??%?) H;
959                ndestruct (E);
960                nlapply (H i); *; #tr'; *; #s'; *; #K'; nrewrite > K' in K;
961                nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
962                ncases (is_final_state s'); #F E; nwhd in E:(??%?);
963                ndestruct (E);
964            ##| ##2,5: #z; ncases z; #tr s; nwhd in ⊢ (??%? → ?);
965                ncases (is_final_state s); #F E; nwhd in E:(??%?);
966                ndestruct (E);
967            ##| ##3,6: #E; nwhd in E:(??%?); ndestruct (E);
968            ##]
969        ##]
970    ##]
971##]
972nqed.   
973
974ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
975| emb_terminates: ∀s,e,tr,r,m.
976    execution_terminates tr s e r m →
977    execution_matches_behavior e (Terminates tr r)
978| emb_diverges: ∀s,e,tr.
979    execution_diverges tr s e →
980    execution_matches_behavior e (Diverges tr)
981| emb_reacts: ∀s,e,tr.
982    execution_reacts tr s e →
983    execution_matches_behavior e (Reacts tr)
984| emb_wrong: ∀e,s,s',tr.
985    execution_goes_wrong tr s e s' →
986    execution_matches_behavior e (Goes_wrong tr)
987| emb_initially_wrong:
988    execution_matches_behavior e_wrong (Goes_wrong E0).
989
990nlemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
991  execution_terminates tr s (e_step tr' s' e) r m → s = s'.
992#tr tr' s s' e r m H; ninversion H;
993##[ #s1 s2 tr1 tr2 r' e' m' H' E1 E2 E3 E4 E5; ndestruct; napply refl
994##| #s1 s2 tr1 tr2 r' e' m' o k i H' E1 E2 E3 E4 E5 E6; ndestruct; napply refl
995##] nqed.
996
997nlemma exec_state_diverges: ∀tr,tr',s,s',e.
998  execution_diverges tr s (e_step tr' s' e) → s = s'.
999#tr tr' s s' e H; ninversion H;
1000#tr1 s1 s2 e1 e2 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
1001
1002nlemma exec_state_reacts: ∀tr,tr',s,s',e.
1003  execution_reacts tr s (e_step tr' s' e) → s = s'.
1004#tr tr' s s' e H; ninversion H;
1005#tr1 s1 e1 H' E1 E2 E3; ndestruct; napply refl; nqed.
1006
1007nlemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
1008  execution_goes_wrong tr s (e_step tr' s' e) s'' → s = s'.
1009#tr tr' s s' s'' e H; ninversion H;
1010#tr1 s1 s2 e1 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
1011
1012nlemma behavior_of_execution: ∀s,e.
1013  execution_characterisation s e →
1014  ∃b:program_behavior. execution_matches_behavior e b.
1015#s0 e0 exec;
1016ncases exec;
1017##[ #s r m e tr TERM;
1018    @ (Terminates tr r);
1019    napply (emb_terminates … TERM);
1020##| #s e tr DIV;
1021    @ (Diverges tr);
1022    napply (emb_diverges … DIV);
1023##| #s e tr REACTS;
1024    @ (Reacts tr);
1025    napply (emb_reacts … REACTS);
1026##| #e s s' tr WRONG;
1027    @ (Goes_wrong tr);
1028    napply (emb_wrong … WRONG);
1029##] nqed.
1030
1031nlemma initial_state_not_final: ∀ge,s.
1032  initial_state ge s →
1033  ¬ ∃r.final_state s r.
1034#ge s H; ncases H;
1035#b f E1 E2; @; *; #r H2;
1036ninversion H2;
1037#r' m E3 E4; ndestruct (E3);
1038nqed.
1039
1040nlemma initial_step: ∀ge,s,e.
1041  exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
1042  ¬(∃r.final_state s r) →
1043  ∃e'.e = e_step E0 s e'.
1044#ge s e; nrewrite > (exec_inf_aux_unfold …);
1045nwhd in ⊢ (??%? → ?); ncases (is_final_state s);
1046##[ #FINAL EXEC NOTFINAL;
1047    napply False_ind; napply (absurd ?? NOTFINAL);
1048    ncases FINAL;
1049    #r F; @r; napply F;
1050##| #F1 EXEC F2; nwhd in EXEC:(??%?); @; ##[ ##2: nrewrite < EXEC; napply refl ##]
1051nqed.
1052
1053ntheorem exec_inf_equivalence:
1054  ∀classic:(∀P:Prop.P ∨ ¬P).
1055  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
1056  ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b.
1057#classic constructive_indefinite_description p;
1058nwhd in ⊢ (??(λ_.?(?%?)%)); nletin ge ≝ (globalenv Genv fundef type p);
1059nlapply (make_initial_state_sound p);
1060nlapply (the_initial_state p);
1061ncases (make_initial_state p);
1062##[ #s INITIAL' INITIAL; nwhd in INITIAL ⊢ (??(λ_.?(?(??%)?)?));
1063    nlapply (behavior_of_execution ??
1064              (execution_characterisation_complete classic constructive_indefinite_description ge s ?));
1065    ##[ napply (initial_state_not_final … INITIAL);
1066    ##| *; #b MATCHES; @b; @; //;
1067        ninversion MATCHES;
1068        ##[ #s0 e tr r m TERM EXEC BEHAVES;
1069            nlapply (initial_step … EXEC ?);
1070            ##[ napply initial_state_not_final; //; ##]
1071            *; #e' E2; nrewrite > E2 in EXEC TERM; #EXEC TERM;
1072            nlapply (exec_state_terminates … TERM); #E1;
1073            nrewrite > E1 in TERM; #TERM;
1074            napply (program_terminates (mk_transrel … step) ?? ge s);
1075            ##[ ##2: napply INITIAL
1076            ##| ##3: napply (terminates_sound … TERM EXEC);
1077            ##| ##skip
1078            ##| //;
1079            ##]
1080        ##| #s0 e tr DIVERGES EXEC E2;
1081            nlapply (initial_step … EXEC ?);
1082            ##[ napply initial_state_not_final; //; ##]
1083            *; #e' E3; nrewrite > E3 in DIVERGES EXEC ⊢ %;
1084            #DIVERGES EXEC; nlapply (exec_state_diverges … DIVERGES);
1085            #E1; nrewrite > E1 in DIVERGES; #DIVERGES;
1086            ninversion DIVERGES; #tr' s1 s2 e1 e2 INITSTEPS DIVERGING E4 E5 E6;
1087            nrewrite < E4 in INITSTEPS ⊢ %; nrewrite < E5 in E6 ⊢ %; #E6 INITSTEPS;
1088            ncut (e' = e1); ##[ ndestruct (E6) skip (MATCHES EXEC); // ##]
1089            #E7; nrewrite < E7 in INITSTEPS; #INITSTEPS;
1090            ncases (several_steps … INITSTEPS EXEC); #INITSTAR EXECDIV;
1091            napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL INITSTAR);
1092            napply (silent_sound … DIVERGING EXECDIV);
1093        ##| #s0 e tr REACTS EXEC E2;
1094            nlapply (initial_step … EXEC ?);
1095            ##[ napply initial_state_not_final; //; ##]
1096            *; #e' E3; nrewrite > E3 in EXEC REACTS ⊢ %;
1097            #EXEC REACTS;
1098            nlapply (exec_state_reacts … REACTS);
1099            #E1; nrewrite > E1 in REACTS; #REACTS;
1100            ninversion REACTS; #tr' s' e'' REACTING E4 E5;
1101            nrewrite < E4 in REACTING ⊢ %; nrewrite < E5; #REACTING E6;
1102            ncut (e' = e''); ##[ ndestruct (E6) skip (MATCHES EXEC); // ##]
1103            #E7; nrewrite < E7 in REACTING; #REACTING;
1104            napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL);
1105            napply (reacts_sound … REACTING EXEC);
1106        ##| #e s1 s2 tr WRONG EXEC E2;
1107            nlapply (initial_step … EXEC ?);
1108            ##[ napply initial_state_not_final; //; ##]
1109            *; #e' E3; nrewrite > E3 in EXEC WRONG ⊢ %;
1110            #EXEC WRONG;
1111            nlapply (exec_state_wrong … WRONG);
1112            #E1; nrewrite > E1 in WRONG; #WRONG;
1113            ninversion WRONG; #tr' s1' s2' e'' GOESWRONG E4 E5 E6 E7;
1114            nrewrite < E4 in GOESWRONG ⊢ %; nrewrite < E5; nrewrite < E7; #GOESWRONG;
1115            ncut (e' = e''); ##[ ndestruct (E6) skip (MATCHES EXEC); // ##]
1116            #E8; nrewrite < E8 in GOESWRONG; #GOESWRONG;
1117            nelim (wrong_sound … WRONG EXEC); *; #STAR STOP FINAL;
1118            napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL STAR STOP);
1119            #r; @; #F; napply (absurd ?? FINAL); @r; napply F;
1120        ##| nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
1121            ncases (is_final_state s); #F EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
1122        ##]
1123   ##]
1124##| nwhd in ⊢ ((∀_.? → %) → ?);
1125    #NOINIT WHATEVER;
1126    @ (Goes_wrong E0); @;
1127    ##[ nwhd in ⊢ (?(??%)?);
1128        nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (?%?);
1129        napply emb_initially_wrong;
1130    ##| napply program_goes_initially_wrong;
1131        #s; @; napply NOINIT;
1132    ##]
1133##] nqed.
1134
Note: See TracBrowser for help on using the repository browser.