source: C-semantics/CexecIOcomplete.ma @ 398

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

This time actually prove the result I intended.

File size: 49.2 KB
Line 
1include "CexecIOequiv.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 exec_from_wrong: ∀ge,s.
478  exec_from ge s se_wrong →
479  exec_step ge s = Wrong ???.
480#ge s H; nwhd in H;
481ninversion H;
482##[ #tr r m EXEC E; ndestruct (E)
483##| #tr s' e e' H EXEC E; ndestruct (E)
484##| nrewrite > (exec_inf_aux_unfold …);
485    ncases (exec_step ge s);
486  ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
487  ##| #x; ncases x; #tr s'; nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
488      #F EXEC; nwhd in EXEC:(??%?); ndestruct
489  ##| //
490  ##]
491##| #o k i e H EXEC E; ndestruct
492##] nqed.
493
494nlemma exec_from_step_notfinal: ∀ge,s,tr,s',e.
495  exec_from ge s (se_step tr s' e) →
496  ¬(∃r. final_state s' r).
497#ge s tr s' e H; nwhd in H; ninversion H;
498##[ #tr' r m EXEC E; ndestruct
499##| #tr' s'' e' e'' H EXEC E; ndestruct (E);
500    nrewrite > (exec_inf_aux_unfold …) in EXEC;
501    ncases (exec_step ge s);
502    ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
503    ##| #x; ncases x; #tr1 s1; nwhd in ⊢ (??%? → ?); ncases (is_final_state s1);
504        #F E; nwhd in E:(??%?); ndestruct; napply F;
505    ##| #E; nwhd in E:(??%?); ndestruct
506    ##]
507##| #EXEC E; ndestruct
508##| #o k i e' H EXEC E; ndestruct
509##] nqed.
510
511nlemma exec_from_interact_step_notfinal: ∀ge,s,o,k,i,tr,s',e.
512  exec_from ge s (se_interact o k i (se_step tr s' e)) →
513  ¬(∃r. final_state s' r).
514#ge s o k i tr s' e H;
515@; *; #r F; ncases F in H; #r' m H;
516ninversion H;
517##[ #tr' r m EXEC E; ndestruct
518##| #tr' s'' e' e'' H EXEC E; ndestruct (E);
519##| #EXEC E; ndestruct
520##| #o' k' i' e' H EXEC E; ndestruct;
521    nrewrite > (exec_inf_aux_unfold …) in EXEC;
522    ncases (exec_step ge s);
523    ##[ #o1 k1 EXEC1; nwhd in EXEC1:(??%?); ndestruct (EXEC1);
524        ninversion H;
525        ##[ #tr1 r1 m1 EXECK E; ndestruct (E);
526        ##| #tr1 s1 e1 e2 H1 EXECK E; ndestruct (E);
527            nrewrite > (exec_inf_aux_unfold …) in EXECK;
528            ncases (k1 i');
529            ##[ #o2 k2 EXECK; nwhd in EXECK:(??%?); ndestruct
530            ##| #x; ncases x; #tr2 s2; nwhd in ⊢ (??%? → ?);
531                ncases (is_final_state s2); #F EXECK;
532                nwhd in EXECK:(??%?); ndestruct;
533                napply (absurd ?? F);
534                @ r'; //;
535            ##| #E; nwhd in E:(??%?); ndestruct
536            ##]
537        ##| #EXECK E;  nwhd in E:(??%?); ndestruct
538        ##| #o2 k2 i2 e2 H2 EXECK E; ndestruct
539        ##]
540    ##| #x; ncases x; #tr1 s1; nwhd in ⊢ (??%? → ?);
541        ncases (is_final_state s1); #F E; nwhd in E:(??%?); ndestruct;
542    ##| #E; nwhd in E:(??%?); ndestruct
543    ##]
544##] nqed.
545
546nlemma wrong_sound: ∀ge,tr,s,s',e.
547  execution_goes_wrong tr s (se_step E0 s e) s' →
548  exec_from ge s e →
549  (¬∃r. final_state s r) →
550  star (mk_transrel … step) ge s tr s' ∧
551  nostep (mk_transrel … step) ge s' ∧
552  (¬∃r. final_state s' r).
553#ge tr0 s0 s0' e0 WRONG; ninversion WRONG;
554#tr s s' e ESTEPS E1 E2 E3 E4 EXEC NOTFINAL; ndestruct (E1 E2 E3 E4);
555ncases (several_steps … ESTEPS EXEC);
556#STAR EXEC'; @;
557##[ @; ##[ napply STAR;
558       ##| #badtr bads; @; #badSTEP;
559           nlapply (step_complete … badSTEP);
560           nrewrite > (exec_from_wrong … EXEC');
561           //;
562       ##]
563##| @;
564    nelim ESTEPS in NOTFINAL EXEC ⊢ %;
565    ##[ #s1 e1 NF EX F; napply (absurd ? F NF);
566    ##| #e1 e2 tr1 tr2 s1 s2 s3 ESTEPS1 IH NF EXEC;
567        ncases (exec_from_step … EXEC); #EXEC3 EXEC1;
568        napply (IH … EXEC1);
569        napply (exec_from_step_notfinal … EXEC);
570    ##| #e1 e2 o k i s1 s2 s3 tr1 tr2 ESTEPS1 IH NF EXEC;
571        napply IH;
572        ##[ napply (exec_from_interact_step_notfinal … EXEC);
573        ##| ncases (exec_from_interact … EXEC); //;
574        ##]
575    ##]
576##] nqed.
577
578ninductive execution_characterisation : state → s_execution → Prop ≝
579| ec_terminates: ∀s,r,m,e,tr.
580    execution_terminates tr s e r m →
581    execution_characterisation s e
582| ec_diverges: ∀s,e,tr.
583    execution_diverges tr s e →
584    execution_characterisation s e
585| ec_reacts: ∀s,e,tr.
586    execution_reacts tr s e →
587    execution_characterisation s e
588| ec_wrong: ∀e,s,s',tr.
589    execution_goes_wrong tr s e s' →
590    execution_characterisation s e.
591
592(* bit of a hack to avoid inability to reduce term in match *)
593ndefinition interact_prop : ∀A:Type.(∀o:io_out. (io_in o → IO io_out io_in A) → Prop) → IO io_out io_in A → Prop ≝
594λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ].
595
596nlemma err_does_not_interact: ∀A,B,P,e1,e2.
597  (∀x:B.interact_prop A P (e2 x)) →
598  interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2).
599#A B P e1 e2 H;
600ncases e1; //; nqed.
601
602nlemma err2_does_not_interact: ∀A,B,C,P,e1,e2.
603  (∀x,y.interact_prop A P (e2 x y)) →
604  interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2).
605#A B C P e1 e2 H;
606ncases e1; ##[ #z; ncases z; ##] //; nqed.
607
608nlemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2.
609  (∀x.interact_prop A P (e2 x)) →
610  interact_prop A P (bindIO ?? (sigma B Q) A (err_to_io_sig ??? Q e1) e2).
611#A B P Q e1 e2 H;
612ncases e1; //; nqed.
613
614nlemma opt_does_not_interact: ∀A,B,P,e1,e2.
615  (∀x:B.interact_prop A P (e2 x)) →
616  interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2).
617#A B P e1 e2 H;
618ncases e1; //; nqed.
619
620nlemma exec_step_interaction:
621  ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s).
622#ge s; ncases s;
623##[ #f st kk e m; ncases st;
624  ##[ ##11,14: #a ##| ##2,4,6,7,12,13,15: #a b ##| ##3,5: #a b c ##| ##8: #a b c d ##]
625  ##[ ##4,6,8,9: napply I ##]
626  nwhd in ⊢ (???%);
627  ##[ ncases a; ##[ ncases (fn_return f); //; ##| #e; nwhd nodelta in ⊢ (???%);
628                    ncases (type_eq_dec (fn_return f) Tvoid); #x; //; napply err2_does_not_interact; // ##]
629  ##| ncases (find_label a (fn_body f) (call_cont kk)); ##[ napply I ##| #z; ncases z; #x y; napply I ##]
630  ##| napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5; napply I
631  ##| ##4,7: napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I
632  ##| napply err2_does_not_interact; #x1 x2; ncases x1; //;
633  ##| 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;
634      ##[ napply I; ##| #x7; napply err2_does_not_interact; #x8 x9; napply I ##]
635  ##| ncases (is_Sskip a); #H; ##[ napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I
636      ##| napply I ##]
637  ##| ncases kk; ##[ ##1,8: ncases (fn_return f); //; ##| ##2,3,5,6,7: //;
638      ##| #z1 z2 z3; napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I ##]
639  ##| ncases kk; //;
640  ##| ncases kk; ##[ ##4: #z1 z2 z3;  napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I
641      ##| ##*: // ##]
642  ##]
643##| #f args kk m; ncases f;
644  ##[ #f'; nwhd in ⊢ (???%); ncases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'));
645      #x; ncases x; ##[ *; ##| #z; ncases z; #x1 x2 H;
646                        napply err_sig_does_not_interact; //; ##]
647  (* This is the only case that actually matters! *)
648  ##| #fn argtys rty; nwhd in ⊢ (???%);
649      napply  err_sig_does_not_interact; #x1;
650      nwhd; #i; @; ##[ ##2: @; ##[ ##2: @; ##[ @; nwhd in ⊢ (??%?); napply refl;
651        ##| @; #E; nwhd in E:(??%%); ndestruct (E); ##] ##] ##]
652  ##]
653##| #v kk m; nwhd in ⊢ (???%); ncases kk;
654    ##[ ##8: #x1 x2 x3 x4; ncases x1;
655      ##[ nwhd in ⊢ (???%); ncases v; // ##| #x5; nwhd in ⊢ (???%); ncases x5;
656          #x6 x7; napply opt_does_not_interact; // ##]
657    ##| ##*: // ##]
658##] nqed.
659
660
661(* Some classical logic (roughly like a fragment of Coq's library) *)
662nlemma classical_doubleneg:
663  ∀classic:(∀P:Prop.P ∨ ¬P).
664  ∀P:Prop. ¬ (¬ P) → P.
665#classic P; *; #H;
666ncases (classic P);
667##[ // ##| #H'; napply False_ind; /2/; ##]
668nqed.
669
670nlemma classical_not_all_not_ex:
671  ∀classic:(∀P:Prop.P ∨ ¬P).
672  ∀A:Type.∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x.
673#classic A P; *; #H;
674napply (classical_doubleneg classic); @; *; #H';
675napply H; #x; @; #H''; napply H'; @x; napply H'';
676nqed.
677
678nlemma classical_not_all_ex_not:
679  ∀classic:(∀P:Prop.P ∨ ¬P).
680  ∀A:Type.∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x.
681#classic A P; *; #H;
682napply (classical_not_all_not_ex classic A (λx.¬ P x));
683@; #H'; napply H; #x; napply (classical_doubleneg classic);
684napply H';
685nqed.
686
687nlemma not_ex_all_not:
688  ∀A:Type.∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x.
689#A P; *; #H x; @; #H';
690napply H; @ x; napply H';
691nqed.
692
693nlemma not_imply_elim:
694  ∀classic:(∀P:Prop.P ∨ ¬P).
695  ∀P,Q:Prop. ¬ (P → Q) → P.
696#classic P Q; *; #H;
697napply (classical_doubleneg classic); @; *; #H';
698napply H; #H''; napply False_ind; napply H'; napply H'';
699nqed.
700
701nlemma not_imply_elim2:
702  ∀P,Q:Prop. ¬ (P → Q) → ¬ Q.
703#P Q; *; #H; @; #H';
704napply H; #_; napply H';
705nqed.
706
707nlemma imply_to_and:
708  ∀classic:(∀P:Prop.P ∨ ¬P).
709  ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q.
710#classic P Q H; @;
711##[ napply (not_imply_elim classic P Q H);
712##| napply (not_imply_elim2 P Q H);
713##] nqed.
714
715nlemma not_and_to_imply:
716  ∀classic:(∀P:Prop.P ∨ ¬P).
717  ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q.
718#classic P Q; *; #H H';
719@; #H''; napply H; @; //;
720nqed.
721
722ninductive execution_not_over : s_execution → Prop ≝
723| eno_step: ∀tr,s,e. execution_not_over (se_step tr s e)
724| eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)).
725
726nlemma eno_stop: ∀tr,r,m. execution_not_over (se_stop tr r m) → False.
727#tr0 r0 m0 H; ninversion H;
728##[ #tr s e E; ndestruct
729##| #o k tr s e i E; ndestruct
730##] nqed.
731
732nlemma eno_wrong: execution_not_over se_wrong → False.
733#H; ninversion H;
734##[ #tr s e E; ndestruct
735##| #o k tr s e i E; ndestruct
736##] nqed.
737
738nlet corec show_divergence s e
739 (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
740                 execution_not_over e1)
741 (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0)
742 (CONTINUES:∀tr2,s2,o,k,i,e'. execution_isteps tr2 s e s2 (se_interact o k i e') → ∃tr3.∃s3.∃e3. e' = se_step tr3 s3 e3 ∧ tr3 ≠ E0)
743 : execution_diverging e ≝ ?.
744nlapply (NONTERMINATING E0 s e ?); //;
745ncases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %;
746##[ #tr i m; #_; #_; #_; #ENO; nelim (eno_stop … ENO);
747##| #tr s' e' UNREACTIVE; nlapply (UNREACTIVE tr s' e' ?);
748  ##[ nrewrite < (E0_right tr) in ⊢ (?%????);
749      napply isteps_one; napply isteps_none;
750  ##| #TR; napply (match sym_eq ??? TR with [ refl ⇒ ? ]); (* nrewrite > TR in UNREACTIVE ⊢ %;*)
751      #NONTERMINATING CONTINUES; #_; @;
752      napply (show_divergence s');
753      ##[ #tr1 s1 e1 S; napply (NONTERMINATING tr1 s1 e1);
754        nchange in ⊢ (?%????) with (Eapp E0 tr1); napply isteps_one;
755        napply S;
756      ##| #tr2 s2 e2 S; nrewrite > TR in UNREACTIVE; #UNREACTIVE; napply (UNREACTIVE tr2 s2 e2);
757          nchange in ⊢ (?%????) with (Eapp E0 tr2);
758          napply isteps_one; napply S;
759      ##| #tr2 s2 o k i e2 S; napply (CONTINUES tr2 s2 o k i);
760          nchange in ⊢ (?%????) with (Eapp E0 tr2);
761          napply (isteps_one … S);
762      ##]
763  ##]
764##| #_; #_; #_; #ENO; nelim (eno_wrong … ENO);
765##| #o k i e' UNREACTIVE NONTERMINATING CONTINUES; #_;
766    nlapply (CONTINUES E0 s o k i e' (isteps_none …));
767    *; #tr'; *; #s'; *; #e'; *; #EXEC NOTSILENT;
768    napply False_ind; napply (absurd ?? NOTSILENT);
769    napply (UNREACTIVE … s' e');
770    nrewrite < (E0_right tr') in ⊢ (?%????);
771    nrewrite > EXEC;
772    napply isteps_interact; //;
773##] nqed.
774(*
775nlemma exec_over_isteps: ∀ge,tr,s,s',e,e'.
776  execution_isteps tr s e s' e' →
777  e = (exec_inf_aux ge (exec_step ge s)) →
778  exec_inf_aux ge (exec_step ge s') = e'.
779#ge tr0 s0 s0' e0 e0';
780#ISTEPS; nelim ISTEPS;
781##[ #s e E; nrewrite > E; napply refl;
782##| #e1 e2 tr1 tr2 s1 s2 s3 ISTEPS' IH E;
783    napply IH; napply sym_eq; napply exec_e_step;
784    ##[ ##3: napply sym_eq; napply E ##]
785##| #e1 e2 o k i s1 s2 s3 tr1 tr2 ISTEPS' EXECK IH E;
786    napply IH;
787    ncases (exec_step ge s3) in E;
788    ##[ #o' k'; nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
789        #E'; nwhd in E':(???%); ndestruct (E');
790        napply sym_eq; napply exec_e_step;
791        ##[ ##3: napply EXECK; ##]
792    ##| #z; ncases z; #tr' s';
793        nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
794        nwhd in ⊢ (???% → ?); ncases (is_final_state s');
795        #F E'; nwhd in E':(???%); ndestruct (E');
796    ##| nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
797        #E'; nwhd in E':(???%); ndestruct (E');
798    ##]
799##] nqed.
800
801nlemma exec_over_isteps': ∀ge,tr,s,s',e'.
802  execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s' e' →
803  exec_inf_aux ge (exec_step ge s') = e'.
804#ge tr s s' e'; nletin e ≝ (exec_inf_aux ge (exec_step ge s)); #H;
805napply (exec_over_isteps … H (refl ??));
806nqed.
807*)
808include "Plogic/jmeq.ma".
809
810nlemma se_inv: ∀e1,e2.
811  single_exec_of e1 e2 →
812  match e1 with
813  [ e_stop tr r m ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ m = m' | _ ⇒ False ]
814  | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
815  | e_wrong ⇒ match e2 with [ se_wrong ⇒ True | _ ⇒ False ]
816  | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ]
817  ].
818#e01 e02 H;
819ncases H;
820##[ #tr r m; nwhd; @; ##[ @ ##] //
821##| #tr s e1' e2' H'; nwhd; @; ##[ @ ##] //
822##| nwhd; //
823##| #o k i e H'; nwhd; @; ##[ @ ##] //
824##] nqed.
825
826nlemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
827  exec_from ge s (se_interact o k i (se_step tr s' e)) →
828  tr ≠ E0.
829#ge o k i tr s s' e; nwhd in ⊢ (% → ?); nrewrite > (exec_inf_aux_unfold …);
830nlapply (exec_step_interaction ge s);
831ncases (exec_step ge s);
832##[ #o' k' ; nwhd in ⊢ (% → ?%? → ?); #H K; ncases (se_inv … K);
833    *; #E1 E2 H1; ndestruct (E1);
834    nlapply (H i); *; #tr'; *; #s''; *; #K' TR;
835    nrewrite > E2 in H1; #H1; nwhd in H1:(?%?); nrewrite > K' in H1;
836    nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (?%? → ?);
837    ncases (is_final_state s'');
838    ##[ #F; nwhd in ⊢ (?%? → ?); #S;
839        napply False_ind; napply (absurd ? S); ncases (se_inv … S)
840    ##| #NF S; nwhd in S:(?%?); ncases (se_inv … S);
841        *; #E1 E2 S'; nrewrite < E1; napply TR
842    ##]
843##| #x; ncases x; #tr' s'' H; nwhd in ⊢ (?%? → ?);
844    ncases (is_final_state s''); #F E; nwhd in E:(?%?);
845    ninversion E;
846    ##[ ##1,5: #tr1 e1 m1 E1 E2; ndestruct
847    ##| ##2,6: #tr s1 e1 e2 H E1 E2; ndestruct
848    ##| ##3,7: #E; ndestruct
849    ##| ##4,8: #o1 k1 i1 e1 H1 E1 E2; ndestruct
850    ##]
851##| #_; #E; nwhd in E:(?%?);
852    ninversion E;
853    ##[ ##1,5: #tr1 e1 m1 E1 E2; ndestruct
854    ##| ##2,6: #tr s1 e1 e2 H E1 E2; ndestruct
855    ##| ##3,7: #E1 E2; ndestruct
856    ##| ##4,8: #o1 k1 i1 e1 H1 E1 E2; ndestruct
857    ##]
858##] nqed.
859
860nlet corec reactive_traceinf' ge s e
861  (EXEC:exec_from ge s e)
862  (REACTIVE: ∀tr,s1,e1.
863    execution_isteps tr s e s1 e1 →
864    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
865  : traceinf' ≝ ?.
866nlapply (REACTIVE E0 s e (isteps_none …));
867*; #x; ncases x; #tr; #y; ncases y; #s' e'; *; #STEPS H;
868@ tr ? H;
869napply (reactive_traceinf' ge s' e' ?);
870##[ ncases (several_steps … STEPS EXEC); #_; //
871##| #tr1 s1 e1 STEPS1;
872    napply REACTIVE;
873    ##[ ##2:
874        napply (isteps_trans … STEPS STEPS1);
875    ##| ##skip
876    ##]
877##]
878nqed.
879
880(* A slightly different version of the above, to work around a problem with the
881   next result. *)
882nlet corec reactive_traceinf'' ge s e
883  (EXEC:exec_from ge s e)
884  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
885  (REACTIVE: ∀tr,s1,e1.
886    execution_isteps tr s e s1 e1 →
887    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
888  : traceinf' ≝ ?.
889ncases REACTIVE0; #x; ncases x; #tr; #y; ncases y; #s' e'; *; #STEPS H;
890@ tr ? H;
891napply (reactive_traceinf'' ge s' e' ?);
892##[ ncases (several_steps … STEPS EXEC); #_; //
893##| napply (REACTIVE … STEPS);
894##| #tr1 s1 e1 STEPS1;
895    napply REACTIVE;
896    ##[ ##2:
897        napply (isteps_trans … STEPS STEPS1);
898    ##| ##skip
899    ##]
900##] nqed.
901
902(* We want to prove
903
904nlemma show_reactive : ∀ge,s.
905  ∀REACTIVE:∀tr,s1,e1.
906    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
907    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
908  execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)).
909 
910but the current matita won't unfold reactive_traceinf' so that we can do case
911analysis on (REACTIVE …).  Instead we take an "applied" version of REACTIVE that
912we can do case analysis on, then get it into the desired form afterwards.
913*)
914nlet corec show_reactive' ge s e
915  (EXEC:exec_from ge s e)
916  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
917  (REACTIVE: ∀tr1,s1,e1.
918    execution_isteps tr1 s e s1 e1 →
919    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
920  : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?.
921(*nrewrite > (unroll_traceinf' (reactive_traceinf'' …));*)
922napply (match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ]);
923ncases REACTIVE0;
924#x; ncases x; #tr1; #y; ncases y; #s1 e1; #z; ncases z; #STEPS NOTSILENT;
925nwhd in ⊢ (?(?%)??);
926(*nrewrite > (traceinf_traceinfp_app …);*)
927napply (match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ]);
928napply (reacting … STEPS NOTSILENT);
929napply show_reactive';
930nqed.
931
932nlemma show_reactive : ∀ge,s,e.
933  ∀EXEC:exec_from ge s e.
934  ∀REACTIVE:∀tr,s1,e1.
935    execution_isteps tr s e s1 e1 →
936    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
937  execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC ? REACTIVE)) s e.
938##[ #ge s e EXEC REACTIVE;
939    napply show_reactive';
940##| napply (REACTIVE … (isteps_none …));
941##] nqed.
942
943nlemma execution_characterisation_complete:
944  ∀classic:(∀P:Prop.P ∨ ¬P).
945  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
946   ∀ge,s,e.
947   exec_from ge s e →
948   execution_characterisation s (se_step E0 s e).
949#classic constructive_indefinite_description ge s e EXEC;
950ncases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
951                 execution_not_over e1));
952##[ #NONTERMINATING;
953    ncases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧
954                     ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0));
955  ##[ *; #tr; *; #s1; *; #e1; *; #INITIAL UNREACTIVE;
956      napply (ec_diverges … s ? tr);
957      napply (diverges_diverging … INITIAL);
958      napply (show_divergence s1 e1);
959      ##[ #tr2 s2 e2 S; napply (NONTERMINATING (Eapp tr tr2) s2 e2);
960          napply (isteps_trans … INITIAL S);
961      ##| #tr2 s2 e2 S; napply (UNREACTIVE … S);
962      ##| #tr2 s2 o k i e2 STEPS;
963          nlapply (NONTERMINATING (Eapp tr tr2) s2 (se_interact o k i e2) ?);
964          ##[ napply (isteps_trans … INITIAL STEPS) ##]
965          #NOTOVER; ninversion NOTOVER;
966          ##[ #tr' s' e' E; ndestruct (E);
967          ##| #o' k' tr' s' e' i' E; ndestruct (E);
968              @ tr'; @s'; @e'; @;//;
969              ncases (several_steps … INITIAL EXEC); #_; #EXEC1;
970              ncases (several_steps … STEPS EXEC1); #_; #EXEC2;
971              napply (interaction_is_not_silent … EXEC2);
972          ##]
973      ##]
974
975  ##| *; #NOTUNREACTIVE;
976      ncut (∀tr,s1,e1.execution_isteps tr s e s1 e1 →
977            ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0);
978      ##[ #tr s1 e1 STEPS;
979          napply (classical_doubleneg classic); @; #NOREACTION;
980          napply NOTUNREACTIVE;
981          @ tr; @s1; @e1; @; //;
982          #tr2 s2 e2 STEPS2;
983          nlapply (not_ex_all_not … NOREACTION); #NR1;
984          nlapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2;
985          napply (classical_doubleneg classic);
986          napply NR2; //;
987      ##| #REACTIVE;
988          napply ec_reacts;
989          ##[ ##2: napply reacts;
990                   napply (show_reactive ge s … EXEC);
991                   #tr s1 e1 STEPS;
992                   napply constructive_indefinite_description;
993                   napply (REACTIVE … tr s1 e1 STEPS);
994          ##| ##skip
995          ##]
996      ##]
997  ##]
998 
999##| #NOTNONTERMINATING; nlapply (classical_not_all_ex_not classic … NOTNONTERMINATING);
1000    *; #tr NNT2; nlapply (classical_not_all_ex_not classic … NNT2);
1001    *; #s' NNT3; nlapply (classical_not_all_ex_not classic … NNT3);
1002    *; #e NNT4; nelim (imply_to_and classic … NNT4);
1003    ncases e;
1004    ##[ #tr' r m; #STEPS NOSTEP;
1005        napply (ec_terminates s r m ? (Eapp tr tr')); @;
1006        ##[ napply s'
1007        ##| napply STEPS
1008        ##]
1009    ##| #tr' s'' e' STEPS; *; #NOSTEP; napply False_rect_Type0;
1010        napply NOSTEP; //
1011    ##| #STEPS NOSTEP;
1012        napply (ec_wrong ? s s' tr); @; //;
1013    (* The following is stupidly complicated when most of the cases are impossible.
1014       It ought to be simplified. *)
1015    ##| #o k i e' STEPS NOSTEP;
1016        ncases e' in STEPS NOSTEP;
1017        ##[ #tr' r m STEPS NOSTEP;
1018            napply (ec_terminates s ???);
1019           ##[ ##4: napply (annoying_corner_case_terminates … STEPS); ##]
1020        ##| #tr1 s1 e1 STEPS; *; #NOSTEP;
1021            napply False_ind; napply NOSTEP; //
1022        ##| #STEPS NOSTEP;
1023            nlapply (exec_step_interaction ge s');
1024            ncases (several_steps … STEPS EXEC); #_;
1025            nwhd in ⊢ (% → ?);
1026            nrewrite > (exec_inf_aux_unfold …);
1027            ncases (exec_step ge s');
1028            ##[ #o1 k1 EXEC' H; nwhd in EXEC':(?%?) H;
1029                ncases (se_inv … EXEC'); *; #E1 E2 H2; ndestruct (E1 E2);
1030                ncases (H i); #tr1; *; #s1; *; #K E; nrewrite > K in H2;
1031                nrewrite > (exec_inf_aux_unfold …);
1032                nwhd in ⊢ (?%? → ?); ncases (is_final_state s1);
1033                #F S; nwhd in S:(?%?); ncases (se_inv … S);
1034            ##| #x; ncases x; #tr' s'; nwhd in ⊢ (?%? → ?);
1035                ncases (is_final_state s'); #F S; nwhd in S:(?%?);
1036                ncases (se_inv … S);
1037            ##| #S; ncases (se_inv … S);
1038            ##]
1039        ##| #o1 k1 i1 e1 STEPS NOSTEP;
1040            nlapply (exec_step_interaction ge s');
1041            ncases (several_steps … STEPS EXEC); #_;
1042            nwhd in ⊢ (% → ?);
1043            nrewrite > (exec_inf_aux_unfold …);
1044            ncases (exec_step ge s');
1045            ##[ #o1 k1 EXEC' H; nwhd in EXEC':(?%?) H;
1046                ncases (se_inv … EXEC'); *; #E1 E2 H2; ndestruct (E1 E2);
1047                ncases (H i); #tr1; *; #s1; *; #K E; nrewrite > K in H2;
1048                nrewrite > (exec_inf_aux_unfold …);
1049                nwhd in ⊢ (?%? → ?); ncases (is_final_state s1);
1050                #F S; nwhd in S:(?%?); ncases (se_inv … S);
1051            ##| #x; ncases x; #tr' s'; nwhd in ⊢ (?%? → ?);
1052                ncases (is_final_state s'); #F S; nwhd in S:(?%?);
1053                ncases (se_inv … S);
1054            ##| #S; ncases (se_inv … S);
1055            ##]
1056        ##]
1057    ##]
1058##]
1059nqed.   
1060
1061ninductive execution_matches_behavior: s_execution → program_behavior → Prop ≝
1062| emb_terminates: ∀s,e,tr,r,m.
1063    execution_terminates tr s e r m →
1064    execution_matches_behavior e (Terminates tr r)
1065| emb_diverges: ∀s,e,tr.
1066    execution_diverges tr s e →
1067    execution_matches_behavior e (Diverges tr)
1068| emb_reacts: ∀s,e,tr.
1069    execution_reacts tr s e →
1070    execution_matches_behavior e (Reacts tr)
1071| emb_wrong: ∀e,s,s',tr.
1072    execution_goes_wrong tr s e s' →
1073    execution_matches_behavior e (Goes_wrong tr)
1074| emb_initially_wrong:
1075    execution_matches_behavior se_wrong (Goes_wrong E0).
1076
1077nlemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
1078  execution_terminates tr s (se_step tr' s' e) r m → s = s'.
1079#tr tr' s s' e r m H; ninversion H;
1080##[ #s1 s2 tr1 tr2 r' e' m' H' E1 E2 E3 E4 E5; ndestruct; napply refl
1081##| #s1 s2 tr1 tr2 r' e' m' o k i H' E1 E2 E3 E4 E5; ndestruct; napply refl
1082##] nqed.
1083
1084nlemma exec_state_diverges: ∀tr,tr',s,s',e.
1085  execution_diverges tr s (se_step tr' s' e) → s = s'.
1086#tr tr' s s' e H; ninversion H;
1087#tr1 s1 s2 e1 e2 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
1088
1089nlemma exec_state_reacts: ∀tr,tr',s,s',e.
1090  execution_reacts tr s (se_step tr' s' e) → s = s'.
1091#tr tr' s s' e H; ninversion H;
1092#tr1 s1 e1 H' E1 E2 E3; ndestruct; napply refl; nqed.
1093
1094nlemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
1095  execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'.
1096#tr tr' s s' s'' e H; ninversion H;
1097#tr1 s1 s2 e1 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
1098
1099nlemma behavior_of_execution: ∀s,e.
1100  execution_characterisation s e →
1101  ∃b:program_behavior. execution_matches_behavior e b.
1102#s0 e0 exec;
1103ncases exec;
1104##[ #s r m e tr TERM;
1105    @ (Terminates tr r);
1106    napply (emb_terminates … TERM);
1107##| #s e tr DIV;
1108    @ (Diverges tr);
1109    napply (emb_diverges … DIV);
1110##| #s e tr REACTS;
1111    @ (Reacts tr);
1112    napply (emb_reacts … REACTS);
1113##| #e s s' tr WRONG;
1114    @ (Goes_wrong tr);
1115    napply (emb_wrong … WRONG);
1116##] nqed.
1117
1118nlemma initial_state_not_final: ∀ge,s.
1119  initial_state ge s →
1120  ¬ ∃r.final_state s r.
1121#ge s H; ncases H;
1122#b f E1 E2; @; *; #r H2;
1123ninversion H2;
1124#r' m E3 E4; ndestruct (E3);
1125nqed.
1126
1127nlemma initial_step: ∀ge,s,e.
1128  exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
1129  ¬(∃r.final_state s r) →
1130  ∃e'.e = e_step E0 s e'.
1131#ge s e; nrewrite > (exec_inf_aux_unfold …);
1132nwhd in ⊢ (??%? → ?); ncases (is_final_state s);
1133##[ #FINAL EXEC NOTFINAL;
1134    napply False_ind; napply (absurd ?? NOTFINAL);
1135    ncases FINAL;
1136    #r F; @r; napply F;
1137##| #F1 EXEC F2; nwhd in EXEC:(??%?); @; ##[ ##2: nrewrite < EXEC; napply refl ##]
1138nqed.
1139
1140ntheorem exec_inf_equivalence:
1141  ∀classic:(∀P:Prop.P ∨ ¬P).
1142  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
1143  ∀p,e. single_exec_of (exec_inf p) e →
1144   ∃b.execution_matches_behavior e b ∧ exec_program p b.
1145#classic constructive_indefinite_description p e;
1146nwhd in ⊢ (?%? → ??(λ_.?(?%?)%)); nletin ge ≝ (globalenv Genv fundef type p);
1147nlapply (make_initial_state_sound p);
1148nlapply (the_initial_state p);
1149ncases (make_initial_state p);
1150##[ #s INITIAL' INITIAL; nwhd in INITIAL ⊢ (?(??%)? → ?);
1151    nrewrite > (exec_inf_aux_unfold …);
1152    nwhd in ⊢ (?%? → ?);
1153    ncases (is_final_state s);
1154    ##[ #F; napply False_ind;
1155        napply (absurd ?? (initial_state_not_final … INITIAL));
1156        ncases F; #r F'; @r; napply F';
1157    ##| #NOTFINAL; nwhd in ⊢ (?%? → ?); ncases e;
1158        ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##]
1159        ncases (se_inv … EXEC0); *; #E1 E2; nrewrite < E1; nrewrite < E2; #EXEC';
1160    nlapply (behavior_of_execution ??
1161              (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
1162        *; #b MATCHES; @b; @; //;
1163        ninversion MATCHES;
1164        ##[ #s0 e1 tr1 r m TERM EXEC BEHAVES; nrewrite < EXEC in TERM;
1165            #TERM;
1166            nlapply (exec_state_terminates … TERM); #E1;
1167            nrewrite > E1 in TERM; #TERM;
1168            napply (program_terminates (mk_transrel … step) ?? ge s);
1169            ##[ ##2: napply INITIAL
1170            ##| ##3: napply (terminates_sound … TERM EXEC');
1171            ##| ##skip
1172            ##| //;
1173            ##]
1174        ##| #s0 e tr DIVERGES EXEC E2; nrewrite < EXEC in DIVERGES; #DIVERGES;
1175            nlapply (exec_state_diverges … DIVERGES);
1176            #E1; nrewrite > E1 in DIVERGES; #DIVERGES;
1177            ninversion DIVERGES; #tr' s1 s2 e1 e2 INITSTEPS DIVERGING E4 E5 E6;
1178            nrewrite < E4 in INITSTEPS ⊢ %; nrewrite < E5 in E6 ⊢ %; #E6 INITSTEPS;
1179            ncut (e0 = e1); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
1180            #E7; nrewrite < E7 in INITSTEPS; #INITSTEPS;
1181            ncases (several_steps … INITSTEPS EXEC'); #INITSTAR EXECDIV;
1182            napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL INITSTAR);
1183            napply (silent_sound … DIVERGING EXECDIV);
1184        ##| #s0 e tr REACTS EXEC E2; nrewrite < EXEC in REACTS; #REACTS;
1185            nlapply (exec_state_reacts … REACTS);
1186            #E1; nrewrite > E1 in REACTS; #REACTS;
1187            ninversion REACTS; #tr' s' e'' REACTING E4 E5;
1188            nrewrite < E4 in REACTING ⊢ %; nrewrite < E5; #REACTING E6;
1189            ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
1190            #E7; nrewrite < E7 in REACTING; #REACTING;
1191            napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL);
1192            napply (reacts_sound … REACTING EXEC');
1193        ##| #e s1 s2 tr WRONG EXEC E2; nrewrite < EXEC in WRONG; #WRONG;
1194            nlapply (exec_state_wrong … WRONG);
1195            #E1; nrewrite > E1 in WRONG; #WRONG;
1196            ninversion WRONG; #tr' s1' s2' e'' GOESWRONG E4 E5 E6 E7;
1197            nrewrite < E4 in GOESWRONG ⊢ %; nrewrite < E5; nrewrite < E7; #GOESWRONG;
1198            ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
1199            #E8; nrewrite < E8 in GOESWRONG; #GOESWRONG;
1200            nelim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR STOP FINAL;
1201            napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL STAR STOP);
1202            #r; @; #F; napply (absurd ?? FINAL); @r; napply F;
1203        ##| #E; ndestruct (E);
1204        ##]
1205   ##]
1206##| nwhd in ⊢ ((∀_.? → %) → ?);
1207    #NOINIT; #_; #EXEC;
1208    @ (Goes_wrong E0); @;
1209    ##[ nwhd in EXEC:(?(??%)?);
1210        nrewrite > (exec_inf_aux_unfold …) in EXEC; nwhd in ⊢ (?%? → ?);
1211        ncases e;
1212        ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##]
1213        ncases (se_inv … EXEC0);
1214        napply emb_initially_wrong;
1215    ##| napply program_goes_initially_wrong;
1216        #s; @; napply NOINIT;
1217    ##]
1218##] nqed.
1219
Note: See TracBrowser for help on using the repository browser.