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

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

Fix treatment of pointers in initialisation data, a little like later versions
of CompCert?. Remove obsolete Init_pointer.

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