include "Cexec.ma". include "Plogic/connectives.ma". ndefinition yields ≝ λA.λa:res A.λv':A. match a with [ OK v ⇒ v' = v | _ ⇒ False ]. (* This tells us that some execution of a results in v'. (There may be many possible executions due to I/O, but we're trying to prove that one particular one exists corresponding to a derivation in the inductive semantics.) *) nlet rec yieldsIO (A:Type) (a:IO io_out io_in A) (v':A) on a : Prop ≝ match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIO A (k r) v' | _ ⇒ False ]. ndefinition yields_sig : ∀A,P. res (Σx:A. P x) → A → Prop ≝ λA,P,e,v. match e with [ OK v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | _ ⇒ False]. nlet rec yieldsIO_sig (A:Type) (P:A → Prop) (e:IO io_out io_in (Σx:A. P x)) (v:A) on e : Prop ≝ match e with [ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | Interact _ k ⇒ ∃r.yieldsIO_sig A P (k r) v | _ ⇒ False]. nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p. yieldsIO A a v' → yieldsIO_sig A P (io_inject io_out io_in A (λx.P x) (Some ? a) p) v'. #A P a; nelim a; ##[ #a k IH v' p H; nwhd in H ⊢ %; nelim H; #r H'; @ r; napply IH; napply H'; ##| #v v' p H; napply H; ##| #a b; *; ##] nqed. nlemma yields_eq: ∀A,a,v'. yields A a v' → a = OK ? v'. #A a v'; ncases a; //; nwhd in ⊢ (% → ?); *; nqed. nlemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? (sig_intro … v p). #A P e v; ncases e; ##[ #vp; ncases vp; #v' p H; nwhd in H; nrewrite > H; @ p; napply refl; ##| *; ##] nqed. nlemma is_pointer_compat_true: ∀m,b,sp. pointer_compat (block_space m b) sp → is_pointer_compat (block_space m b) sp = true. #m b sp H; nwhd in ⊢ (??%?); nelim (pointer_compat_dec (block_space m b) sp); ##[ // ##| #H'; napply False_ind; napply (absurd … H H'); ##] nqed. nlemma ms_eq_dec_true: ∀s. ms_eq_dec s s = inl ???. ##[ #s; ncases s; napply refl; ##| ##skip ##] nqed. ntheorem is_det: ∀p,s,s'. initial_state p s → initial_state p s' → s = s'. #p s s' H1 H2; ninversion H1; #b1 f1 e11 e12 e13; ninversion H2; #b2 f2 e21 e22 e23; nrewrite > e11 in e21; #e1; nrewrite > (?:b1 = b2) in e12; ##[ nrewrite > e22; #e2; nrewrite > (?:f2 = f1); ##[ //; ##| ndestruct (e2) skip (e22 e23); //; ##] ##| ndestruct (e1) skip (e11); // ##] nqed. nlemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p. yields A a v' → yields_sig A P (err_inject A (λx.P x) (Some ? a) p) v'. #A P a; ncases a; ##[ #v v' p H; napply H; ##| #a b; *; ##] nqed. ntheorem the_initial_state: ∀p,s. initial_state p s → yields ? (make_initial_state p) s. #p s; ncases p; #fns main globs H; ninversion H; #b f e1 e2 e3; nwhd in ⊢ (??%?); nrewrite > e1; nwhd in ⊢ (??%?); nrewrite > e2; nwhd; napply refl; nqed. nlemma cast_complete: ∀m,v,ty,ty',v'. cast m v ty ty' v' → yields ? (exec_cast m v ty ty') v'. #m v ty ty' v' H; nelim H; ##[ #m i sz1 sz2 sg1 sg2; napply refl; ##| #m f sz szi sg; napply refl; ##| #m i sz sz' sg; napply refl; ##| #m f sz sz'; napply refl; ##| #m sp sp' ty ty' b ofs H1 H2 H3; nelim H1; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #tys1 ty1; nletin sp1 ≝ Code ##] nwhd in ⊢ (??%?); ##[ ##1,2: nrewrite > (ms_eq_dec_true …); nwhd in ⊢ (??%?); ##] nelim H2 in H3 ⊢ %; ##[ ##1,4,7: #sp2 ty2 ##| ##2,5,8: #sp2 ty2 n2 ##| ##3,6,9: #tys2 ty2; nletin sp2 ≝ Code ##] #H3; nwhd in ⊢ (??%?); nrewrite > (is_pointer_compat_true …); //; ##| #m sz si ty'' H; ncases H; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #args rty ##] napply refl; ##| #m t t' H H'; ncases H; ncases H'; //; ##] nqed. (* Use to narrow down the choice of expression to just the lvalues. *) nlemma lvalue_expr: ∀ge,env,m,e,ty,sp,l,ofs,tr. ∀P:expr_descr → Prop. eval_lvalue ge env m (Expr e ty) sp l ofs tr → (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) → P e. #ge env m e ty sp l ofs tr P H; napply (eval_lvalue_inv_ind … H); ##[ #id l ty e1 e2 e3 e4 e5 e6; ndestruct; // ##| #id sp l ty e1 e2 e3 e4 e5 e6 e7; ndestruct; // ##| #e ty sp l ofs tr H e1 e2 e3 e4 e5; ndestruct; // ##| #e id ty sp l ofs id' fs d tr H e1 e2;(* bogus? *) #_; #e3 e4 e5 e6 e7; ndestruct; // ##| #e id ty sp l ofs id' fs tr H e1;(* bogus? *) #_; #e2 e3 e4 e5 e6; ndestruct; // ##] nqed. nlemma 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. #v ty r H; nelim H; #v t H'; nelim H'; ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //; ##| #p b i i0 s; @ true; @; // ##| #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //; ##| #p b i p0 t0; @ true; @; // ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //; ##| #i s; @ false; @; //; ##| #p t; @ false; @; //; ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //; ##] nqed. nlemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true. #v ty H; nelim H; ##[ #i is s ne; nwhd; nrewrite > (eq_false … ne); //; ##| #p b i i0 s; // ##| #i p t ne; nwhd; nrewrite > (eq_false … ne); //; ##| #p b i p0 t0; // ##| #f s ne; nwhd; nrewrite > (Feq_zero_false … ne); //; ##] nqed. nlemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false. #v ty H; nelim H; ##[ #i s; //; ##| #p t; //; ##| #s; nwhd; nrewrite > (Feq_zero_true …); //; ##] nqed. nlemma expr_lvalue_complete: ∀ge,env,m. (∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉)) ∧ (∀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〉)). #ge env m; napply (combined_expr_lvalue_ind ge env m (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉)) (λe,sp,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉))); ##[ #i ty; napply refl; ##| #f ty; napply refl; ##| #e ty sp l off v tr H1 H2; napply (lvalue_expr … H1); ##[ #id ##| #e' ##| #e' id ##] #H3; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H3); nwhd in ⊢ (??%?); nrewrite > H2; napply refl; ##| #e ty sp l off tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H2); napply refl; ##| #ty' ty; napply refl; ##| #op e ty v1 v tr H1 H2 H3; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H3); nwhd in ⊢ (??%?); nrewrite > H2; napply refl; ##| #op e1 e2 ty v1 v2 v tr1 tr2 H1 H2 e3 H4 H5; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H4); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H5); nwhd in ⊢ (??%?); nrewrite > e3; napply refl; ##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H4); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_true ?? H2)); nrewrite > (yields_eq ??? H5); napply refl; ##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H4); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_false ?? H2)); nrewrite > (yields_eq ??? H5); napply refl; ##| #e1 e2 ty v1 tr H1 H2 H3; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H3); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_true ?? H2)); napply refl; ##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H5); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_false ?? H2)); nrewrite > (yields_eq ??? H6); nwhd in ⊢ (??%?); nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb; nrewrite > (yields_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb; napply refl; ##| #e1 e2 ty v1 tr H1 H2 H3; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H3); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_false ?? H2)); napply refl; ##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H5); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_true ?? H2)); nrewrite > (yields_eq ??? H6); nwhd in ⊢ (??%?); nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb; nrewrite > (yields_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb; napply refl; ##| #e ty ty' v1 v tr H1 H2 H3; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H3); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (cast_complete … H2)); napply refl; ##| #e ty v l tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H2); nwhd in ⊢ (??%?); napply refl; (* lvalues *) ##| #id l ty e1; nwhd in ⊢ (??%?); nrewrite > e1; napply refl; ##| #id sp l ty e1 e2; nwhd in ⊢ (??%?); nrewrite > e1; nrewrite > e2; napply refl; ##| #e ty sp l ofs tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H2); napply refl; ##| #e i ty sp l ofs id fList delta tr H1 H2 H3 H4; ncases e in H2 H4 ⊢ %; #e' ty' H2; nwhd in H2:(??%?); nrewrite > H2; #H4; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H4); nwhd in ⊢ (??%?); nrewrite > H3; napply refl; ##| #e i ty sp l ofs id fList tr; ncases e; #e' ty' H1 H2; nwhd in H2:(??%?); nrewrite > H2; #H3; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H3); napply refl; ##] nqed. ntheorem expr_complete: ∀ge,env,m. ∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉). #ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed. ntheorem exprlist_complete: ∀ge,env,m,es,vs,tr. eval_exprlist ge env m es vs tr → yields ? (exec_exprlist ge env m es) (〈vs,tr〉). #ge env m es vs tr H; nelim H; ##[ napply refl; ##| #e et v vt tr trt H1 H2 H3; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? H3); napply refl; ##] nqed. ntheorem lvalue_complete: ∀ge,env,m. ∀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〉). #ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed. nlet rec P_typelist (P:type → Prop) (l:typelist) on l : Prop ≝ match l with [ Tnil ⇒ True | Tcons h t ⇒ P h ∧ P_typelist P t ]. nlet rec type_ind2l (P:type → Prop) (Q:typelist → Prop) (vo:P Tvoid) (it:∀i,s. P (Tint i s)) (fl:∀f. P (Tfloat f)) (pt:∀s,t. P t → P (Tpointer s t)) (ar:∀s,t,n. P t → P (Tarray s t n)) (fn:∀tl,t. Q tl → P t → P (Tfunction tl t)) (st:∀i,fl. P (Tstruct i fl)) (un:∀i,fl. P (Tunion i fl)) (cp:∀i. P (Tcomp_ptr i)) (nl:Q Tnil) (cs:∀t,tl. P t → Q tl → Q (Tcons t tl)) (t:type) on t : P t ≝ match t return λt'.P t' with [ Tvoid ⇒ vo | Tint i s ⇒ it i s | Tfloat s ⇒ fl s | Tpointer s t' ⇒ pt s t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t') | Tarray s t' n ⇒ ar s t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t') | 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') | Tstruct i fs ⇒ st i fs | Tunion i fs ⇒ un i fs | Tcomp_ptr i ⇒ cp i ] and typelist_ind2l (P:type → Prop) (Q:typelist → Prop) (vo:P Tvoid) (it:∀i,s. P (Tint i s)) (fl:∀f. P (Tfloat f)) (pt:∀s,t. P t → P (Tpointer s t)) (ar:∀s,t,n. P t → P (Tarray s t n)) (fn:∀tl,t. Q tl → P t → P (Tfunction tl t)) (st:∀i,fl. P (Tstruct i fl)) (un:∀i,fl. P (Tunion i fl)) (cp:∀i. P (Tcomp_ptr i)) (nl:Q Tnil) (cs:∀t,tl. P t → Q tl → Q (Tcons t tl)) (ts:typelist) on ts : Q ts ≝ match ts return λts'.Q ts' with [ Tnil ⇒ nl | Tcons t tl ⇒ cs t tl (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t) (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl) ]. nlemma assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p. #t; nwhd in ⊢ (??(λ_.??%?)); ncases (type_eq_dec t t); #E; ##[ @ E; // ##| napply False_ind; napply (absurd ?? E); // ##] nqed. nlemma alloc_vars_complete: ∀env,m,l,env',m'. alloc_variables env m l env' m' → ∃p.exec_alloc_variables env m l = sig_intro ?? (Some ? 〈env', m'〉) p. #env m l env' m' H; nelim H; ##[ #env'' m''; @ ?; nwhd; //; ##| #env1 m1 id ty l1 m2 loc m3 env2 H1 H2 H3; nwhd in H1:(??%?) ⊢ (??(λ_.??%?)); ndestruct (H1); nelim H3; #p3 e3; nrewrite > e3; nwhd in ⊢ (??(λ_.??%?)); @ ?; //; ##] nqed. nlemma bind_params_complete: ∀e,m,params,vs,m2. bind_parameters e m params vs m2 → yields_sig ?? (exec_bind_parameters e m params vs) m2. #e m params vs m2 H; nelim H; ##[ //; ##| #env1 m1 id ty l v tl loc m2 m3 H1 H2 H3 H4; napply remove_res_sig; nrewrite > H1; nwhd in ⊢ (??%?); nrewrite > H2; nwhd in ⊢ (??%?); nelim (yields_sig_eq ???? H4); #p4 e4; nrewrite > e4; napply refl; ##] nqed. nlemma eventval_match_complete': ∀ev,ty,v. eventval_match ev ty v → yields_sig ?? (check_eventval' v ty) ev. #ev ty v H; nelim H; //; nqed. nlemma eventval_list_match_complete: ∀vs,tys,evs. eventval_list_match evs tys vs → yields_sig ?? (check_eventval_list vs tys) evs. #vs tys evs H; nelim H; ##[ // ##| #e etl ty tytl v vtl H1 H2 H3; napply remove_res_sig; nelim (yields_sig_eq ???? (eventval_match_complete' … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_sig_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?); napply refl; ##] nqed. nlemma dec_true: ∀P:Prop.∀f:P + ¬P.∀p:P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inl ?? p')) → Q f. #P f p Q H; ncases f; ##[ napply H ##| #np; napply False_ind; napply (absurd ? p np); ##] nqed. nlemma dec_false: ∀P:Prop.∀f:P + ¬P.∀p:¬P.∀Q:(P + ¬P) → Prop. (∀p'.Q (inr ?? p')) → Q f. #P f p Q H; ncases f; ##[ #np; napply False_ind; napply (absurd ? np p); ##| napply H ##] nqed. ntheorem step_complete: ∀ge,s,tr,s'. step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉. #ge s tr s' H; nelim H; ##[ #f e e1 k e2 m sp loc ofs v m' tr1 tr2 H1 H2 H3; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?); nrewrite > H3; napply refl; ##| #f e eargs k ef m vf vargs f' tr1 tr2 H1 H2 H3 H4; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (exprlist_complete … H2)); nwhd in ⊢ (??%?); nrewrite > H3; nwhd in ⊢ (??%?); nrewrite > H4; nelim (assert_type_eq_true (typeof e)); #pty ety; nrewrite > ety; napply refl; ##| #f el ef eargs k env m sp loc ofs vf vargs f' tr1 tr2 tr3 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (exprlist_complete … H3)); nwhd in ⊢ (??%?); nrewrite > H4; nwhd in ⊢ (??%?); nrewrite > H5; nelim (assert_type_eq_true (typeof ef)); #pty ety; nrewrite > ety; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?); napply refl; ##| #f s1 s2 k env m; napply refl ##| ##5,6,7: #f s k env m; napply refl ##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_true ?? H2)); napply refl ##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_false ?? H2)); napply refl ##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_false ?? H2)); napply refl ##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_true ?? H2)); napply refl ##| #f s1 e s2 k env m H; ncases H; #es1; nrewrite > es1; napply refl; ##| ##13,14: #f e s k env m; napply refl ##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_false ?? H2)); napply refl ##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_true ?? H2)); napply refl ##| #f e s k env m; napply refl; ##| #f s1 e s2 s3 k env m nskip; nwhd in ⊢ (??%?); ncases (is_Sskip s1); ##[ #H; napply False_ind; /2/; ##| #H; nwhd in ⊢ (??%?); napply refl ##] ##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_false ?? H2)); napply refl; ##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (bool_of_true ?? H2)); napply refl; ##| #f s1 e s2 s3 k env m; *; #es1; nrewrite > es1; napply refl; ##| ##22,23: #f e s1 s2 k env m; napply refl; ##| #f k env m H; nwhd in ⊢ (??%?); nrewrite > H; napply refl; ##| #f e k env m v tr H1 H2; nwhd in ⊢ (??%?); napply (dec_false ? (type_eq_dec (fn_return f) Tvoid) H1); #pf'; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?); napply refl; ##| #f k env m; ncases k; ##[ #H1 H2; nwhd in ⊢ (??%?); nrewrite > H2; napply refl; ##| #s' k'; nwhd in ⊢ (% → ?); *; ##| ##3,4: #e' s' k'; nwhd in ⊢ (% → ?); *; ##| ##5,6: #e' s1' s2' k'; nwhd in ⊢ (% → ?); *; ##| #k'; nwhd in ⊢ (% → ?); *; ##| #r f' env' k' H1 H2; nwhd in ⊢ (??%?); nrewrite > H2; napply refl ##] ##| #f e s k env m i tr H1; nwhd in ⊢ (??%?); nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); napply refl ##| #f s k env m; *; #es; nrewrite > es; napply refl; ##| #f k env m; napply refl ##| #f l s k env m; napply refl ##| #f l k env m s k' H1; nwhd in ⊢ (??%?); nrewrite > H1; napply refl; ##| #f args k m1 env m2 m3 H1 H2; nwhd in ⊢ (??%?); nelim (alloc_vars_complete … H1); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_sig_eq ???? (bind_params_complete … H2)); #p2 e2; nrewrite > e2; napply refl; ##| #id tys rty args k m rv tr H; nwhd in ⊢ (??%?); ninversion H; #f' args' rv' eargs erv H1 H2 e1 e2 e3 e4; nrewrite < e1 in H1 H2; #H1 H2; nelim (yields_sig_eq ???? (eventval_list_match_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nwhd; ninversion H2; #x e5 e6 e7; @ x; nwhd in ⊢ (??%?); napply refl ##| #v f env k m; napply refl ##| #v f env k m1 m2 sp loc ofs ty H; nwhd in ⊢ (??%?); nrewrite > H; napply refl ##| #f l s k env m; napply refl ##] nqed.