# Changeset 253

Ignore:
Timestamp:
Nov 22, 2010, 2:40:31 PM (9 years ago)
Message:

Update completeness proof for executable semantics with separate soundness
proofs.

File:
1 edited

Unmodified
Removed
• ## C-semantics/CexecIOcomplete.ma

 r250 ndefinition yieldsbare ≝ λA.λa:res A.λv':A. match a with [ OK v ⇒ v' = v | _ ⇒ False ]. nlemma yieldsbare_eq: ∀A,a,v'. yieldsbare A a v' → a = OK ? v'. #A a v'; ncases a; //; nwhd in ⊢ (% → ?); *; nqed. nlemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p. ##] nqed. nlemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yields ?? (bool_of_val_3 v ty) b. nlemma 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. #v ty r H; nelim H; #v t H'; nelim H'; ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //; nqed. nlemma bool_of_true: ∀v,ty. is_true v ty → yields ?? (bool_of_val_3 v ty) true. nlemma bool_of_true: ∀v,ty. is_true v ty → yieldsbare ? (exec_bool_of_val v ty) true. #v ty H; nelim H; ##[ #i is s ne; nwhd; nrewrite > (eq_false … ne); //; nqed. nlemma bool_of_false: ∀v,ty. is_false v ty → yields ?? (bool_of_val_3 v ty) false. nlemma bool_of_false: ∀v,ty. is_false v ty → yieldsbare ? (exec_bool_of_val v ty) false. #v ty H; nelim H; ##[ #i s; //; 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〉)). (∀e,v,tr. eval_expr ge env m e v tr → yieldsbare ? (exec_expr ge env m e) (〈v,tr〉)) ∧ (∀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〉)). #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〉))); (λe,v,tr,H. yieldsbare ? (exec_expr ge env m e) (〈v,tr〉)) (λe,sp,l,off,tr,H. yieldsbare ? (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; nelim (yields_eq ???? H3); #p3 e3; napply remove_res_sig; nwhd in ⊢ (??%?); nwhd in e3:(??%?); nrewrite > e3; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H3); nwhd in ⊢ (??%?); nrewrite > H2; napply refl; ##| #e ty sp l off tr H1 H2; nelim (yields_eq ???? H2); ncases e; #e' ty'; #p2 e2; napply remove_res_sig; nrewrite > e2; ##| #e ty sp l off tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H2); napply refl; ##| #ty' ty; napply refl; ##| #op e ty v1 v tr H1 H2 H3; napply remove_res_sig; nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; ##| #op e ty v1 v tr H1 H2 H3; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H3); nwhd in ⊢ (??%?); nrewrite > H2; napply refl; ##| #op e1 e2 ty v1 v2 v tr1 tr2 H1 H2 e3 H4 H5; napply remove_res_sig; nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?); nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; nwhd in ⊢ (??%?); ##| #op e1 e2 ty v1 v2 v tr1 tr2 H1 H2 e3 H4 H5; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H4); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H5); nwhd in ⊢ (??%?); nrewrite > e3; napply refl; ##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; napply remove_res_sig; nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2; nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; napply refl; ##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; napply remove_res_sig; nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2; nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; napply refl; ##| #e1 e2 ty v1 tr H1 H2 H3; napply remove_res_sig; nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2; ##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H4); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2)); nrewrite > (yieldsbare_eq ??? H5); napply refl; ##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H4); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2)); nrewrite > (yieldsbare_eq ??? H5); napply refl; ##| #e1 e2 ty v1 tr H1 H2 H3; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H3); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2)); napply refl; ##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; napply remove_res_sig; nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2; nelim (yields_eq ???? H6); #p6 e6; nrewrite > e6; nwhd in ⊢ (??%?); ##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H5); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2)); nrewrite > (yieldsbare_eq ??? H6); nwhd in ⊢ (??%?); nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb; nelim (yields_eq ???? Hb); #pb eb; nrewrite > eb; nwhd in ⊢ (??%?); nrewrite < evb; nrewrite > (yieldsbare_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb; napply refl; ##| #e1 e2 ty v1 tr H1 H2 H3; napply remove_res_sig; nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2; ##| #e1 e2 ty v1 tr H1 H2 H3; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H3); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2)); napply refl; ##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; napply remove_res_sig; nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2; nelim (yields_eq ???? H6); #p6 e6; nrewrite > e6; nwhd in ⊢ (??%?); ##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H5); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2)); nrewrite > (yieldsbare_eq ??? H6); nwhd in ⊢ (??%?); nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb; nelim (yields_eq ???? Hb); #pb eb; nrewrite > eb; nwhd in ⊢ (??%?); nrewrite < evb; napply refl; ##| #e ty ty' v1 v tr H1 H2 H3; napply remove_res_sig; nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?); nelim (yields_eq ???? (cast_complete … H2)); #p2 e2; nrewrite > e2; napply refl; ##| #e ty v l tr H1 H2; napply remove_res_sig; nelim (yields_eq ???? H2); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?); napply refl; nrewrite > (yieldsbare_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb; napply refl; ##| #e ty ty' v1 v tr H1 H2 H3; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H3); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (cast_complete … H2)); napply refl; ##| #e ty v l tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? H2); nwhd in ⊢ (??%?); napply refl; (* lvalues *) (* FIXME: next two cases produce type checking failures at nqed. *) ##| napply daemon (*#id l ty e1; nwhd in ⊢ (???%?); nrewrite > e1; napply refl;*) ##|napply daemon; (*#id sp l ty e1 e2; nwhd in ⊢ (???%?); napply (dep_option_rewrite ??????? e1); nrewrite > e2; napply refl;*) ##| #e ty sp l ofs tr H1 H2; napply remove_res_sig; nelim (yields_eq ???? H2); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?); napply refl; ##| (* careful!  Make sure we do the H2 rewrite before unfolding, or we end up in trouble because there's an equality proof floating around. *) #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; napply remove_res_sig; nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?); ##| #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 > (yieldsbare_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 > (yieldsbare_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; napply remove_res_sig; nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; napply refl; nwhd in H2:(??%?); nrewrite > H2; #H3; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_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〉). ∀e,v,tr. eval_expr ge env m e v tr → yieldsbare ? (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〉). eval_exprlist ge env m es vs tr → yieldsbare ? (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; napply remove_res_sig; nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?); ##| #e et v vt tr trt H1 H2 H3; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_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〉). ∀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〉). #ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed. ntheorem step_complete: ∀ge,s,tr,s'. step ge s tr s' → yieldsIO ?? (exec_step ge s) 〈tr,s'〉. step ge s tr s' → yieldsIObare ? (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; napply remove_io_sig; nelim (yields_eq ???? (lvalue_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?); ##[ #f e e1 k e2 m sp loc ofs v m' tr1 tr2 H1 H2 H3; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_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; napply remove_io_sig; nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_eq ???? (exprlist_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?); ##| #f e eargs k ef m vf vargs f' tr1 tr2 H1 H2 H3 H4; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_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; napply remove_io_sig; nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?); nelim (yields_eq ???? (exprlist_complete … H3)); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?); ##| #f el ef eargs k env m sp loc ofs vf vargs f' tr1 tr2 tr3 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_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 ⊢ (??%?); nelim (yields_eq ???? (lvalue_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_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; napply remove_io_sig; nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2; napply refl ##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig; nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2; napply refl ##| #f e s k env m v tr H1 H2; napply remove_io_sig; nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2; napply refl ##| #f e s k env m v tr H1 H2; napply remove_io_sig; nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2; ##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2)); napply refl ##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2)); napply refl ##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2)); napply refl ##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_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; napply remove_io_sig; nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2; napply refl ##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; napply remove_io_sig; nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2; ##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2)); napply refl ##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_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); ##| #f s1 e s2 s3 k env m nskip; nwhd in ⊢ (??%?); ncases (is_Sskip s1); ##[ #H; napply False_ind; /2/; ##| #H; napply remove_io_sig; napply refl ##] ##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig; nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2; napply refl; ##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig; nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2; ##| #H; nwhd in ⊢ (??%?); napply refl ##] ##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2)); napply refl; ##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?); nrewrite > (yieldsbare_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; ##| napply daemon (* FIXME: rewrite causes failure at nqed  #f k env m H; nwhd in ⊢ (???%?); nrewrite > H; napply refl;*) ##| #f e k env m v tr H1 H2; napply remove_io_sig; ##| #f k env m H; nwhd in ⊢ (??%?); nrewrite > H; napply refl; ##| #f e k env m v tr H1 H2; nwhd in ⊢ (??%?); nelim (is_not_void_true f H1); #pf ef; nrewrite > ef; nwhd in ⊢ (??%?); nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?); napply refl; ##| #f k env m; ncases k; ##[ #H1 H2; napply daemon (* FIXME nwhd in ⊢ (???%?); nrewrite > H2; napply refl; *) ##[ #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; napply daemon (* FIXME typing error at nqed nwhd in ⊢ (???%?); nrewrite > H2; napply refl *) ##| #r f' env' k' H1 H2; nwhd in ⊢ (??%?); nrewrite > H2; napply refl ##] ##| #f e s k env m i tr H1; napply remove_io_sig; nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?); napply refl ##| #f s k env m; napply daemon (* FIXME *; #es; nrewrite > es; napply refl;*) ##| #f e s k env m i tr H1; nwhd in ⊢ (??%?); nrewrite > (yieldsbare_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; napply daemon(* FIXME nwhd in ⊢ (???%?); nrewrite > H1; napply refl; *) ##| #f args k m1 env m2 m3 H1 H2; napply remove_io_sig; ##| #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_eq ???? (bind_params_complete … H2)); #p2 e2; nrewrite > e2; napply refl; ##| #id tys rty args k m rv tr H; napply remove_io_sig; ##| #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; nwhd; @ erv; nwhd in ⊢ (??%?); nelim (yields_eq ???? (eventval_match_complete … H2)); #p2 e2; nrewrite > e2; napply refl ##| #v f env k m; nwhd in ⊢ (???%?); napply daemon (* FIXME: inductive semantics allows any value ?! *) ##| #v f env k m1 m2 sp loc ofs ty H; napply remove_io_sig; ##| #v f env k m; nwhd in ⊢ (??%?); napply daemon (* FIXME: inductive semantics allows any value ?! *) ##| #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
Note: See TracChangeset for help on using the changeset viewer.