source: Deliverables/D3.1/C-semantics/CexecComplete.ma @ 484

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

Separate out null values from integer zeros.

File size: 18.4 KB
Line 
1include "Cexec.ma".
2include "Plogic/connectives.ma".
3
4ndefinition yields ≝ λA.λa:res A.λv':A.
5match a with [ OK v ⇒ v' = v | _ ⇒ False ].
6
7(* This tells us that some execution of a 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) (a:IO io_out io_in A) (v':A) on a : Prop ≝
12match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIO A (k r) v' | _ ⇒ False ].
13
14ndefinition yields_sig : ∀A,P. res (Σx:A. P x) → A → Prop ≝
15λA,P,e,v. match e with [ OK v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | _ ⇒ False].
16
17nlet rec yieldsIO_sig (A:Type) (P:A → Prop) (e:IO io_out io_in (Σx:A. P x)) (v:A) on e : Prop ≝
18match e with
19[ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ]
20| Interact _ k ⇒ ∃r.yieldsIO_sig A P (k r) v
21| _ ⇒ False].
22
23nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
24yieldsIO A a v' →
25yieldsIO_sig A P (io_inject io_out io_in A (λx.P x) (Some ? a) p) v'.
26#A P a; nelim a;
27##[ #a k IH v' p H; nwhd in H ⊢ %; nelim H; #r H'; @ r; napply IH; napply H';
28##| #v v' p H; napply H;
29##| #a b; *;
30##] nqed.
31
32nlemma yields_eq: ∀A,a,v'. yields A a v' → a = OK ? v'.
33#A a v'; ncases a; //; nwhd in ⊢ (% → ?); *;
34nqed.
35
36nlemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? (sig_intro … v p).
37#A P e v; ncases e;
38##[ #vp; ncases vp; #v' p H; nwhd in H; nrewrite > H; @ p; napply refl;
39##| *;
40##] nqed.
41
42nlemma is_pointer_compat_true: ∀m,b,sp.
43  pointer_compat (block_space m b) sp →
44  is_pointer_compat (block_space m b) sp = true.
45#m b sp H; nwhd in ⊢ (??%?);
46nelim (pointer_compat_dec (block_space m b) sp);
47##[ //
48##| #H'; napply False_ind; napply (absurd … H H');
49##] nqed.
50
51nlemma eq_region_dec_true: ∀s. eq_region_dec s s = inl ???.
52##[ #s; ncases s; napply refl;
53##| ##skip
54##] nqed.
55
56ntheorem is_det: ∀p,s,s'.
57initial_state p s → initial_state p s' → s = s'.
58#p s s' H1 H2;
59ninversion H1; #b1 f1 e11 e12 e13;
60ninversion H2; #b2 f2 e21 e22 e23;
61nrewrite > e11 in e21;
62#e1; nrewrite > (?:b1 = b2) in e12;
63##[ nrewrite > e22; #e2; nrewrite > (?:f2 = f1);
64  ##[ //;
65  ##| ndestruct (e2) skip (e22 e23); //;
66  ##]
67##| ndestruct (e1) skip (e11); //
68##] nqed.
69
70nlemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
71yields A a v' →
72yields_sig A P (err_inject A (λx.P x) (Some ? a) p) v'.
73#A P a; ncases a;
74##[ #v v' p H; napply H;
75##| #a b; *;
76##] nqed.
77
78
79ntheorem the_initial_state:
80  ∀p,s. initial_state p s → yields ? (make_initial_state p) s.
81#p s; ncases p; #fns main globs H;
82ninversion H;
83#b f e1 e2 e3;
84nwhd in ⊢ (??%?);
85nrewrite > e1;
86nwhd in ⊢ (??%?);
87nrewrite > e2;
88nwhd; napply refl;
89nqed.
90
91nlemma cast_complete: ∀m,v,ty,ty',v'.
92  cast m v ty ty' v' → yields ? (exec_cast m v ty ty') v'.
93#m v ty ty' v' H;
94nelim H;
95##[ #m i sz1 sz2 sg1 sg2; napply refl;
96##| #m f sz szi sg; napply refl;
97##| #m i sz sz' sg; napply refl;
98##| #m f sz sz'; napply refl;
99##| #m sp sp' ty ty' b ofs H1 H2 H3;
100    nelim H1; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #tys1 ty1; nletin sp1 ≝ Code ##]
101    nwhd in ⊢ (??%?);
102    ##[ ##1,2: nrewrite > (eq_region_dec_true …); nwhd in ⊢ (??%?); ##]
103    nelim H2 in H3 ⊢ %; ##[ ##1,4,7: #sp2 ty2 ##| ##2,5,8: #sp2 ty2 n2 ##| ##3,6,9: #tys2 ty2; nletin sp2 ≝ Code ##]
104    #H3; nwhd in ⊢ (??%?);
105    nrewrite > (is_pointer_compat_true …); //;
106##| #m sz si ty'' r H; ncases H; //;
107##| #m t t' r r' H H'; ncases H; ntry #a; ntry #b; ntry #c; ncases H'; ntry #d; ntry #e; ntry #f;
108    nwhd in ⊢ (??%?); ntry napply refl; nrewrite > eq_region_dec_true; napply refl;
109##] nqed.
110
111(* Use to narrow down the choice of expression to just the lvalues. *)
112nlemma lvalue_expr: ∀ge,env,m,e,ty,sp,l,ofs,tr. ∀P:expr_descr → Prop.
113  eval_lvalue ge env m (Expr e ty) sp l ofs tr →
114  (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) →
115  P e.
116#ge env m e ty sp l ofs tr P H; napply (eval_lvalue_inv_ind … H);
117##[ #id l ty e1 e2 e3 e4 e5 e6; ndestruct; //
118##| #id sp l ty e1 e2 e3 e4 e5 e6 e7; ndestruct; //
119##| #e ty sp l ofs tr H e1 e2 e3 e4 e5; ndestruct; //
120##| #e id ty sp l ofs id' fs d tr H e1 e2;(* bogus? *) #_; #e3 e4 e5 e6 e7; ndestruct; //
121##| #e id ty sp l ofs id' fs tr H e1;(* bogus? *) #_; #e2 e3 e4 e5 e6; ndestruct; //
122##] nqed.
123
124nlemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yields ? (exec_bool_of_val v ty) b.
125#v ty r H; nelim H; #v t H'; nelim H';
126  ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
127  ##| #p b i i0 s; @ true; @; //
128  ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
129  ##| #i s; @ false; @; //;
130  ##| #r r' t; @ false; @; //;
131  ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
132  ##]
133nqed.
134
135nlemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true.
136#v ty H; nelim H;
137  ##[ #i is s ne; nwhd; nrewrite > (eq_false … ne); //;
138  ##| #p b i i0 s; //
139  ##| #f s ne; nwhd; nrewrite > (Feq_zero_false … ne); //;
140  ##]
141nqed.
142
143nlemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false.
144#v ty H; nelim H;
145  ##[ #i s; //;
146  ##| #r r' t; //;
147  ##| #s; nwhd; nrewrite > (Feq_zero_true …); //;
148  ##]
149nqed.
150
151nlemma expr_lvalue_complete: ∀ge,env,m.
152(∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉)) ∧
153(∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)).
154#ge env m;
155napply (combined_expr_lvalue_ind ge env m
156  (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
157  (λe,sp,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)));
158##[ #i ty; napply refl;
159##| #f ty; napply refl;
160##| #e ty sp l off v tr H1 H2; napply (lvalue_expr … H1);
161    ##[ #id ##| #e' ##| #e' id ##] #H3;
162    nwhd in ⊢ (??%?);
163    nrewrite > (yields_eq ??? H3);
164    nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
165##| #e ty sp l off tr H1 H2; nwhd in ⊢ (??%?);
166    nrewrite > (yields_eq ??? H2);
167    napply refl;
168##| #ty' ty; napply refl;
169##| #op e ty v1 v tr H1 H2 H3; nwhd in ⊢ (??%?);
170    nrewrite > (yields_eq ??? H3);
171    nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
172##| #op e1 e2 ty v1 v2 v tr1 tr2 H1 H2 e3 H4 H5; nwhd in ⊢ (??%?);
173    nrewrite > (yields_eq ??? H4); nwhd in ⊢ (??%?);
174    nrewrite > (yields_eq ??? H5); nwhd in ⊢ (??%?);
175    nrewrite > e3; napply refl;
176##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?);
177    nrewrite > (yields_eq ??? H4); nwhd in ⊢ (??%?);
178    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
179    nrewrite > (yields_eq ??? H5);
180    napply refl;
181##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?);
182    nrewrite > (yields_eq ??? H4); nwhd in ⊢ (??%?);
183    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
184    nrewrite > (yields_eq ??? H5);
185    napply refl;
186##| #e1 e2 ty v1 tr H1 H2 H3; nwhd in ⊢ (??%?);
187    nrewrite > (yields_eq ??? H3); nwhd in ⊢ (??%?);
188    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
189    napply refl;   
190##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; nwhd in ⊢ (??%?);
191    nrewrite > (yields_eq ??? H5); nwhd in ⊢ (??%?);
192    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
193    nrewrite > (yields_eq ??? H6); nwhd in ⊢ (??%?);
194    nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb;
195    nrewrite > (yields_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb;
196    napply refl;   
197##| #e1 e2 ty v1 tr H1 H2 H3; nwhd in ⊢ (??%?);
198    nrewrite > (yields_eq ??? H3); nwhd in ⊢ (??%?);
199    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
200    napply refl;   
201##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; nwhd in ⊢ (??%?);
202    nrewrite > (yields_eq ??? H5); nwhd in ⊢ (??%?);
203    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
204    nrewrite > (yields_eq ??? H6); nwhd in ⊢ (??%?);
205    nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb;
206    nrewrite > (yields_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb;
207    napply refl;
208##| #e ty ty' v1 v tr H1 H2 H3; nwhd in ⊢ (??%?);
209    nrewrite > (yields_eq ??? H3); nwhd in ⊢ (??%?);
210    nrewrite > (yields_eq ??? (cast_complete … H2));
211    napply refl;
212##| #e ty v l tr H1 H2; nwhd in ⊢ (??%?);
213    nrewrite > (yields_eq ??? H2); nwhd in ⊢ (??%?);
214    napply refl;
215   
216  (* lvalues *)
217##| #id l ty e1; nwhd in ⊢ (??%?); nrewrite > e1; napply refl;
218##| #id sp l ty e1 e2; nwhd in ⊢ (??%?); nrewrite > e1;
219    nrewrite > e2; napply refl;
220##| #e ty sp l ofs tr H1 H2; nwhd in ⊢ (??%?);
221    nrewrite > (yields_eq ??? H2);
222    napply refl;
223##| #e i ty sp l ofs id fList delta tr H1 H2 H3 H4; ncases e in H2 H4 ⊢ %;
224    #e' ty' H2; nwhd in H2:(??%?); nrewrite > H2; #H4; nwhd in ⊢ (??%?);
225    nrewrite > (yields_eq ??? H4); nwhd in ⊢ (??%?);
226    nrewrite > H3; napply refl;
227##| #e i ty sp l ofs id fList tr; ncases e; #e' ty' H1 H2;
228    nwhd in H2:(??%?); nrewrite > H2; #H3; nwhd in ⊢ (??%?);
229    nrewrite > (yields_eq ??? H3); napply refl;
230##] nqed.
231
232ntheorem expr_complete:  ∀ge,env,m.
233 ∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉).
234#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
235
236ntheorem exprlist_complete: ∀ge,env,m,es,vs,tr.
237  eval_exprlist ge env m es vs tr → yields ? (exec_exprlist ge env m es) (〈vs,tr〉).
238#ge env m es vs tr H; nelim H;
239##[ napply refl;
240##| #e et v vt tr trt H1 H2 H3; nwhd in ⊢ (??%?);
241    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
242    nrewrite > (yields_eq ??? H3);
243    napply refl;
244##] nqed.
245
246ntheorem lvalue_complete: ∀ge,env,m.
247 ∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉).
248#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
249
250nlet rec P_typelist (P:type → Prop) (l:typelist) on l : Prop ≝
251match l with
252[ Tnil ⇒ True
253| Tcons h t ⇒ P h ∧ P_typelist P t
254].
255
256nlet rec type_ind2l
257  (P:type → Prop) (Q:typelist → Prop)
258  (vo:P Tvoid)
259  (it:∀i,s. P (Tint i s))
260  (fl:∀f. P (Tfloat f))
261  (pt:∀s,t. P t → P (Tpointer s t))
262  (ar:∀s,t,n. P t → P (Tarray s t n))
263  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
264  (st:∀i,fl. P (Tstruct i fl))
265  (un:∀i,fl. P (Tunion i fl))
266  (cp:∀r,i. P (Tcomp_ptr r i))
267  (nl:Q Tnil)
268  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
269 (t:type) on t : P t ≝
270  match t return λt'.P t' with
271  [ Tvoid ⇒ vo
272  | Tint i s ⇒ it i s
273  | Tfloat s ⇒ fl s
274  | Tpointer s t' ⇒ pt s t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
275  | Tarray s t' n ⇒ ar s t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
276  | 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')
277  | Tstruct i fs ⇒ st i fs
278  | Tunion i fs ⇒ un i fs
279  | Tcomp_ptr r i ⇒ cp r i
280  ]
281and typelist_ind2l
282  (P:type → Prop) (Q:typelist → Prop)
283  (vo:P Tvoid)
284  (it:∀i,s. P (Tint i s))
285  (fl:∀f. P (Tfloat f))
286  (pt:∀s,t. P t → P (Tpointer s t))
287  (ar:∀s,t,n. P t → P (Tarray s t n))
288  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
289  (st:∀i,fl. P (Tstruct i fl))
290  (un:∀i,fl. P (Tunion i fl))
291  (cp:∀r,i. P (Tcomp_ptr r i))
292  (nl:Q Tnil)
293  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
294  (ts:typelist) on ts : Q ts ≝
295  match ts return λts'.Q ts' with
296  [ Tnil ⇒ nl
297  | Tcons t tl ⇒ cs t tl (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t)
298                     (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl)
299  ].
300
301nlemma assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
302#t; nwhd in ⊢ (??(λ_.??%?)); ncases (type_eq_dec t t); #E;
303##[ @ E; //
304##| napply False_ind; napply (absurd ?? E); //
305##] nqed.
306
307nlemma alloc_vars_complete: ∀env,m,l,env',m'.
308  alloc_variables env m l env' m' →
309  ∃p.exec_alloc_variables env m l = sig_intro ?? (Some ? 〈env', m'〉) p.
310#env m l env' m' H; nelim H;
311##[ #env'' m''; @ ?; nwhd; //;
312##| #env1 m1 id ty l1 m2 loc m3 env2 H1 H2 H3;
313    nwhd in H1:(??%?) ⊢ (??(λ_.??%?));
314    ndestruct (H1);
315    nelim H3; #p3 e3; nrewrite > e3; nwhd in ⊢ (??(λ_.??%?)); @ ?; //;
316##] nqed.
317
318nlemma bind_params_complete: ∀e,m,params,vs,m2.
319  bind_parameters e m params vs m2 →
320  yields_sig ?? (exec_bind_parameters e m params vs) m2.
321#e m params vs m2 H; nelim H;
322##[ //;
323##| #env1 m1 id ty l v tl loc m2 m3 H1 H2 H3 H4;
324    napply remove_res_sig;
325    nrewrite > H1; nwhd in ⊢ (??%?);
326    nrewrite > H2; nwhd in ⊢ (??%?);
327    nelim (yields_sig_eq ???? H4); #p4 e4; nrewrite > e4;
328    napply refl;
329##] nqed.
330
331nlemma eventval_match_complete': ∀ev,ty,v.
332  eventval_match ev ty v → yields_sig ?? (check_eventval' v ty) ev.
333#ev ty v H; nelim H; //; nqed.
334
335nlemma eventval_list_match_complete: ∀vs,tys,evs.
336  eventval_list_match evs tys vs → yields_sig ?? (check_eventval_list vs tys) evs.
337#vs tys evs H; nelim H;
338##[ //
339##| #e etl ty tytl v vtl H1 H2 H3; napply remove_res_sig;
340    nelim (yields_sig_eq ???? (eventval_match_complete' … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
341    nelim (yields_sig_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
342    napply refl;
343##] nqed.
344
345nlemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inl ?? p')) → Q f.
346#P f p Q H; ncases f;
347##[ napply H
348##| #np; napply False_ind; napply (absurd ? p np);
349##] nqed.
350
351nlemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inr ?? p')) → Q f.
352#P f p Q H; ncases f;
353##[ #np; napply False_ind; napply (absurd ? np p);
354##| napply H
355##] nqed.
356
357ntheorem step_complete: ∀ge,s,tr,s'.
358  step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉.
359#ge s tr s' H; nelim H;
360##[ #f e e1 k e2 m sp loc ofs v m' tr1 tr2 H1 H2 H3; nwhd in ⊢ (??%?);
361    nrewrite > (yields_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
362    nrewrite > (yields_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
363    nrewrite > H3; napply refl;
364##| #f e eargs k ef m vf vargs f' tr1 tr2 H1 H2 H3 H4; nwhd in ⊢ (??%?);
365    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
366    nrewrite > (yields_eq ??? (exprlist_complete … H2)); nwhd in ⊢ (??%?);
367    nrewrite > H3; nwhd in ⊢ (??%?);
368    nrewrite > H4; nelim (assert_type_eq_true (fun_typeof e)); #pty ety; nrewrite > ety;
369    napply refl;
370##| #f el ef eargs k env m sp loc ofs vf vargs f' tr1 tr2 tr3 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?);
371    nrewrite > (yields_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
372    nrewrite > (yields_eq ??? (exprlist_complete … H3)); nwhd in ⊢ (??%?);
373    nrewrite > H4; nwhd in ⊢ (??%?);
374    nrewrite > H5; nelim (assert_type_eq_true (fun_typeof ef)); #pty ety; nrewrite > ety;
375    nwhd in ⊢ (??%?);
376    nrewrite > (yields_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
377    napply refl;
378##| #f s1 s2 k env m; napply refl
379##| ##5,6,7: #f s k env m; napply refl
380##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
381    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
382    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
383    napply refl
384##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
385    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
386    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
387    napply refl
388##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?);
389    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
390    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
391    napply refl
392##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?);
393    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
394    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
395    napply refl
396##| #f s1 e s2 k env m H; ncases H; #es1; nrewrite > es1; napply refl;
397##| ##13,14: #f e s k env m; napply refl
398##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?);
399    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
400    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
401    napply refl
402##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?);
403    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
404    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
405    napply refl
406##| #f e s k env m; napply refl;
407##| #f s1 e s2 s3 k env m nskip; nwhd in ⊢ (??%?); ncases (is_Sskip s1);
408    ##[ #H; napply False_ind; napply (absurd ? H nskip)
409    ##| #H; nwhd in ⊢ (??%?); napply refl ##]
410##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
411    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
412    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
413    napply refl;
414##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
415    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
416    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
417    napply refl;
418##| #f s1 e s2 s3 k env m; *; #es1; nrewrite > es1; napply refl;
419##| ##22,23: #f e s1 s2 k env m; napply refl;
420##| #f k env m H; nwhd in ⊢ (??%?); nrewrite > H; napply refl;
421##| #f e k env m v tr H1 H2; nwhd in ⊢ (??%?);
422    napply (dec_false ? (type_eq_dec (fn_return f) Tvoid) H1); #pf';
423    nwhd in ⊢ (??%?);
424    nrewrite > (yields_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
425    napply refl;
426##| #f k env m; ncases k;
427    ##[ #H1 H2; nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
428    ##| #s' k'; nwhd in ⊢ (% → ?); *;
429    ##| ##3,4: #e' s' k'; nwhd in ⊢ (% → ?); *;
430    ##| ##5,6: #e' s1' s2' k'; nwhd in ⊢ (% → ?); *;
431    ##| #k'; nwhd in ⊢ (% → ?); *;
432    ##| #r f' env' k' H1 H2; nwhd in ⊢ (??%?); nrewrite > H2; napply refl
433    ##]
434##| #f e s k env m i tr H1; nwhd in ⊢ (??%?);
435    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
436    napply refl
437##| #f s k env m; *; #es; nrewrite > es; napply refl;
438##| #f k env m; napply refl
439##| #f l s k env m; napply refl
440##| #f l k env m s k' H1; nwhd in ⊢ (??%?); nrewrite > H1; napply refl;
441##| #f args k m1 env m2 m3 H1 H2; nwhd in ⊢ (??%?);
442    nelim (alloc_vars_complete … H1); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
443    nelim (yields_sig_eq ???? (bind_params_complete … H2)); #p2 e2; nrewrite > e2;
444    napply refl;
445##| #id tys rty args k m rv tr H; nwhd in ⊢ (??%?);
446    ninversion H; #f' args' rv' eargs erv H1 H2 e1 e2 e3 e4; nrewrite < e1 in H1 H2;
447    #H1 H2;
448    nelim (yields_sig_eq ???? (eventval_list_match_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
449    nwhd; ninversion H2; #x e5 e6 e7; @ x; nwhd in ⊢ (??%?);
450    napply refl
451##| #v f env k m; napply refl
452##| #v f env k m1 m2 sp loc ofs ty H; nwhd in ⊢ (??%?);
453    nrewrite > H; napply refl
454##| #f l s k env m; napply refl
455##] nqed.
Note: See TracBrowser for help on using the repository browser.