Changeset 253


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

Update completeness proof for executable semantics with separate soundness
proofs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIOcomplete.ma

    r250 r253  
    7474ndefinition yieldsbare ≝ λA.λa:res A.λv':A.
    7575match a with [ OK v ⇒ v' = v | _ ⇒ False ].
     76
     77nlemma yieldsbare_eq: ∀A,a,v'. yieldsbare A a v' → a = OK ? v'.
     78#A a v'; ncases a; //; nwhd in ⊢ (% → ?); *;
     79nqed.
    7680
    7781nlemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
     
    121125##] nqed.
    122126
    123 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.
     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.
    124128#v ty r H; nelim H; #v t H'; nelim H';
    125129  ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
     
    134138nqed.
    135139
    136 nlemma bool_of_true: ∀v,ty. is_true v ty → yields ?? (bool_of_val_3 v ty) true.
     140nlemma bool_of_true: ∀v,ty. is_true v ty → yieldsbare ? (exec_bool_of_val v ty) true.
    137141#v ty H; nelim H;
    138142  ##[ #i is s ne; nwhd; nrewrite > (eq_false … ne); //;
     
    144148nqed.
    145149
    146 nlemma bool_of_false: ∀v,ty. is_false v ty → yields ?? (bool_of_val_3 v ty) false.
     150nlemma bool_of_false: ∀v,ty. is_false v ty → yieldsbare ? (exec_bool_of_val v ty) false.
    147151#v ty H; nelim H;
    148152  ##[ #i s; //;
     
    166170
    167171nlemma expr_lvalue_complete: ∀ge,env,m.
    168 (∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉)) ∧
    169 (∀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〉)).
     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〉)).
    170174#ge env m;
    171175napply (combined_expr_lvalue_ind ge env m
    172   (λe,v,tr,H. yields ?? (exec_expr ge env m e) (〈v,tr〉))
    173   (λe,sp,l,off,tr,H. yields ?? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)));
     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〉)));
    174178##[ #i ty; napply refl;
    175179##| #f ty; napply refl;
    176180##| #e ty sp l off v tr H1 H2; napply (lvalue_expr … H1);
    177181    ##[ #id ##| #e' ##| #e' id ##] #H3;
    178     nelim (yields_eq ???? H3);
    179     #p3 e3; napply remove_res_sig; nwhd in ⊢ (??%?); nwhd in e3:(??%?); nrewrite > e3;
     182    nwhd in ⊢ (??%?);
     183    nrewrite > (yieldsbare_eq ??? H3);
    180184    nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
    181 ##| #e ty sp l off tr H1 H2;
    182     nelim (yields_eq ???? H2); ncases e; #e' ty';
    183     #p2 e2; napply remove_res_sig; nrewrite > e2;
     185##| #e ty sp l off tr H1 H2; nwhd in ⊢ (??%?);
     186    nrewrite > (yieldsbare_eq ??? H2);
    184187    napply refl;
    185188##| #ty' ty; napply refl;
    186 ##| #op e ty v1 v tr H1 H2 H3; napply remove_res_sig;
    187     nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3;
     189##| #op e ty v1 v tr H1 H2 H3; nwhd in ⊢ (??%?);
     190    nrewrite > (yieldsbare_eq ??? H3);
    188191    nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
    189 ##| #op e1 e2 ty v1 v2 v tr1 tr2 H1 H2 e3 H4 H5; napply remove_res_sig;
    190     nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4;
    191     nwhd in ⊢ (??%?);
    192     nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5;
    193     nwhd in ⊢ (??%?);
     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 ⊢ (??%?);
    194195    nrewrite > e3; napply refl;
    195 ##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; napply remove_res_sig;
    196     nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?);
    197     nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
    198     nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5;
    199     napply refl;
    200 ##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; napply remove_res_sig;
    201     nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?);
    202     nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
    203     nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5;
    204     napply refl;
    205 ##| #e1 e2 ty v1 tr H1 H2 H3; napply remove_res_sig;
    206     nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
    207     nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
     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));
    208209    napply refl;   
    209 ##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; napply remove_res_sig;
    210     nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; nwhd in ⊢ (??%?);
    211     nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
    212     nelim (yields_eq ???? H6); #p6 e6; nrewrite > e6; nwhd in ⊢ (??%?);
     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 ⊢ (??%?);
    213214    nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb;
    214     nelim (yields_eq ???? Hb); #pb eb; nrewrite > eb; nwhd in ⊢ (??%?); nrewrite < evb;
     215    nrewrite > (yieldsbare_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb;
    215216    napply refl;   
    216 ##| #e1 e2 ty v1 tr H1 H2 H3; napply remove_res_sig;
    217     nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
    218     nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
     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));
    219220    napply refl;   
    220 ##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; napply remove_res_sig;
    221     nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; nwhd in ⊢ (??%?);
    222     nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
    223     nelim (yields_eq ???? H6); #p6 e6; nrewrite > e6; nwhd in ⊢ (??%?);
     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 ⊢ (??%?);
    224225    nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb;
    225     nelim (yields_eq ???? Hb); #pb eb; nrewrite > eb; nwhd in ⊢ (??%?); nrewrite < evb;
    226     napply refl;
    227 ##| #e ty ty' v1 v tr H1 H2 H3; napply remove_res_sig;
    228     nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
    229     nelim (yields_eq ???? (cast_complete … H2)); #p2 e2; nrewrite > e2;
    230     napply refl;
    231 ##| #e ty v l tr H1 H2; napply remove_res_sig;
    232     nelim (yields_eq ???? H2); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
    233     napply refl;
     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   
    234236  (* lvalues *)
    235  
    236  
    237  (* FIXME: next two cases produce type checking failures at nqed. *)
    238 ##| napply daemon (*#id l ty e1; nwhd in ⊢ (???%?); nrewrite > e1; napply refl;*)
    239 ##|napply daemon; (*#id sp l ty e1 e2; nwhd in ⊢ (???%?); napply (dep_option_rewrite ??????? e1);
    240     nrewrite > e2; napply refl;*)
    241 ##| #e ty sp l ofs tr H1 H2; napply remove_res_sig;
    242     nelim (yields_eq ???? H2); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
    243     napply refl;
    244 ##| (* careful!  Make sure we do the H2 rewrite before unfolding, or we end up
    245        in trouble because there's an equality proof floating around. *)
    246     #e i ty sp l ofs id fList delta tr H1 H2 H3 H4; ncases e in H2 H4 ⊢ %;
    247     #e' ty' H2; nwhd in H2:(??%?); nrewrite > H2; #H4; napply remove_res_sig;
    248     nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?);
     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 ⊢ (??%?);
    249246    nrewrite > H3; napply refl;
    250247##| #e i ty sp l ofs id fList tr; ncases e; #e' ty' H1 H2;
    251     nwhd in H2:(??%?); nrewrite > H2; #H3; napply remove_res_sig;
    252     nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; napply refl;
     248    nwhd in H2:(??%?); nrewrite > H2; #H3; nwhd in ⊢ (??%?);
     249    nrewrite > (yieldsbare_eq ??? H3); napply refl;
    253250##] nqed.
    254251
    255252ntheorem expr_complete:  ∀ge,env,m.
    256  ∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉).
     253 ∀e,v,tr. eval_expr ge env m e v tr → yieldsbare ? (exec_expr ge env m e) (〈v,tr〉).
    257254#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
    258255
    259256ntheorem exprlist_complete: ∀ge,env,m,es,vs,tr.
    260   eval_exprlist ge env m es vs tr → yields ?? (exec_exprlist ge env m es) (〈vs,tr〉).
     257  eval_exprlist ge env m es vs tr → yieldsbare ? (exec_exprlist ge env m es) (〈vs,tr〉).
    261258#ge env m es vs tr H; nelim H;
    262259##[ napply refl;
    263 ##| #e et v vt tr trt H1 H2 H3; napply remove_res_sig;
    264     nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    265     nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
     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);
    266263    napply refl;
    267264##] nqed.
    268265
    269266ntheorem lvalue_complete: ∀ge,env,m.
    270  ∀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〉).
     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〉).
    271268#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
    272269
     
    390387
    391388ntheorem step_complete: ∀ge,s,tr,s'.
    392   step ge s tr s' → yieldsIO ?? (exec_step ge s) 〈tr,s'〉.
     389  step ge s tr s' → yieldsIObare ? (exec_step ge s) 〈tr,s'〉.
    393390#ge s tr s' H; nelim H;
    394 ##[ #f e e1 k e2 m sp loc ofs v m' tr1 tr2 H1 H2 H3; napply remove_io_sig;
    395     nelim (yields_eq ???? (lvalue_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    396     nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
     391##[ #f e e1 k e2 m sp loc ofs v m' tr1 tr2 H1 H2 H3; nwhd in ⊢ (??%?);
     392    nrewrite > (yieldsbare_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
     393    nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
    397394    nrewrite > H3; napply refl;
    398 ##| #f e eargs k ef m vf vargs f' tr1 tr2 H1 H2 H3 H4; napply remove_io_sig;
    399     nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    400     nelim (yields_eq ???? (exprlist_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
     395##| #f e eargs k ef m vf vargs f' tr1 tr2 H1 H2 H3 H4; nwhd in ⊢ (??%?);
     396    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     397    nrewrite > (yieldsbare_eq ??? (exprlist_complete … H2)); nwhd in ⊢ (??%?);
    401398    nrewrite > H3; nwhd in ⊢ (??%?);
    402399    nrewrite > H4; nelim (assert_type_eq_true (typeof e)); #pty ety; nrewrite > ety;
    403400    napply refl;
    404 ##| #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;
    405     nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
    406     nelim (yields_eq ???? (exprlist_complete … H3)); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
     401##| #f el ef eargs k env m sp loc ofs vf vargs f' tr1 tr2 tr3 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?);
     402    nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
     403    nrewrite > (yieldsbare_eq ??? (exprlist_complete … H3)); nwhd in ⊢ (??%?);
    407404    nrewrite > H4; nwhd in ⊢ (??%?);
    408405    nrewrite > H5; nelim (assert_type_eq_true (typeof ef)); #pty ety; nrewrite > ety;
    409406    nwhd in ⊢ (??%?);
    410     nelim (yields_eq ???? (lvalue_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     407    nrewrite > (yieldsbare_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
    411408    napply refl;
    412409##| #f s1 s2 k env m; napply refl
    413410##| ##5,6,7: #f s k env m; napply refl
    414 ##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
    415     nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    416     nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
    417     napply refl
    418 ##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
    419     nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    420     nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
    421     napply refl
    422 ##| #f e s k env m v tr H1 H2; napply remove_io_sig;
    423     nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    424     nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
    425     napply refl
    426 ##| #f e s k env m v tr H1 H2; napply remove_io_sig;
    427     nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    428     nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
     411##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
     412    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     413    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
     414    napply refl
     415##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
     416    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     417    nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
     418    napply refl
     419##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?);
     420    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     421    nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
     422    napply refl
     423##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?);
     424    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     425    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
    429426    napply refl
    430427##| #f s1 e s2 k env m H; ncases H; #es1; nrewrite > es1; napply refl;
    431428##| ##13,14: #f e s k env m; napply refl
    432 ##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; napply remove_io_sig;
    433     nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    434     nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
    435     napply refl
    436 ##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; napply remove_io_sig;
    437     nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    438     nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
     429##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?);
     430    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     431    nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
     432    napply refl
     433##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?);
     434    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     435    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
    439436    napply refl
    440437##| #f e s k env m; napply refl;
    441 ##| #f s1 e s2 s3 k env m nskip; nwhd in ⊢ (???%?); ncases (is_Sskip s1);
     438##| #f s1 e s2 s3 k env m nskip; nwhd in ⊢ (??%?); ncases (is_Sskip s1);
    442439    ##[ #H; napply False_ind; /2/;
    443     ##| #H; napply remove_io_sig; napply refl ##]
    444 ##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
    445     nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    446     nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
    447     napply refl;
    448 ##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
    449     nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    450     nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
     440    ##| #H; nwhd in ⊢ (??%?); napply refl ##]
     441##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
     442    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     443    nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
     444    napply refl;
     445##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
     446    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     447    nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
    451448    napply refl;
    452449##| #f s1 e s2 s3 k env m; *; #es1; nrewrite > es1; napply refl;
    453450##| ##22,23: #f e s1 s2 k env m; napply refl;
    454 ##| napply daemon (* FIXME: rewrite causes failure at nqed  #f k env m H; nwhd in ⊢ (???%?); nrewrite > H; napply refl;*)
    455 ##| #f e k env m v tr H1 H2; napply remove_io_sig;
     451##| #f k env m H; nwhd in ⊢ (??%?); nrewrite > H; napply refl;
     452##| #f e k env m v tr H1 H2; nwhd in ⊢ (??%?);
    456453    nelim (is_not_void_true f H1); #pf ef; nrewrite > ef; nwhd in ⊢ (??%?);
    457     nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
     454    nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
    458455    napply refl;
    459456##| #f k env m; ncases k;
    460     ##[ #H1 H2; napply daemon (* FIXME nwhd in ⊢ (???%?); nrewrite > H2; napply refl; *)
     457    ##[ #H1 H2; nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
    461458    ##| #s' k'; nwhd in ⊢ (% → ?); *;
    462459    ##| ##3,4: #e' s' k'; nwhd in ⊢ (% → ?); *;
    463460    ##| ##5,6: #e' s1' s2' k'; nwhd in ⊢ (% → ?); *;
    464461    ##| #k'; nwhd in ⊢ (% → ?); *;
    465     ##| #r f' env' k' H1 H2; napply daemon (* FIXME typing error at nqed nwhd in ⊢ (???%?); nrewrite > H2; napply refl *)
     462    ##| #r f' env' k' H1 H2; nwhd in ⊢ (??%?); nrewrite > H2; napply refl
    466463    ##]
    467 ##| #f e s k env m i tr H1; napply remove_io_sig;
    468     nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    469     napply refl
    470 ##| #f s k env m; napply daemon (* FIXME *; #es; nrewrite > es; napply refl;*)
     464##| #f e s k env m i tr H1; nwhd in ⊢ (??%?);
     465    nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     466    napply refl
     467##| #f s k env m; *; #es; nrewrite > es; napply refl;
    471468##| #f k env m; napply refl
    472469##| #f l s k env m; napply refl
    473 ##| #f l k env m s k' H1; napply daemon(* FIXME nwhd in ⊢ (???%?); nrewrite > H1; napply refl; *)
    474 ##| #f args k m1 env m2 m3 H1 H2; napply remove_io_sig;
     470##| #f l k env m s k' H1; nwhd in ⊢ (??%?); nrewrite > H1; napply refl;
     471##| #f args k m1 env m2 m3 H1 H2; nwhd in ⊢ (??%?);
    475472    nelim (alloc_vars_complete … H1); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    476473    nelim (yields_eq ???? (bind_params_complete … H2)); #p2 e2; nrewrite > e2;
    477474    napply refl;
    478 ##| #id tys rty args k m rv tr H; napply remove_io_sig;
     475##| #id tys rty args k m rv tr H; nwhd in ⊢ (??%?);
    479476    ninversion H; #f' args' rv' eargs erv H1 H2 e1 e2 e3 e4; nrewrite < e1 in H1 H2;
    480477    #H1 H2;
     
    482479    nwhd; @ erv; nwhd in ⊢ (??%?);
    483480    nelim (yields_eq ???? (eventval_match_complete … H2)); #p2 e2; nrewrite > e2; napply refl
    484 ##| #v f env k m; nwhd in ⊢ (???%?); napply daemon (* FIXME: inductive semantics allows any value ?! *)
    485 ##| #v f env k m1 m2 sp loc ofs ty H; napply remove_io_sig;
     481##| #v f env k m; nwhd in ⊢ (??%?); napply daemon (* FIXME: inductive semantics allows any value ?! *)
     482##| #v f env k m1 m2 sp loc ofs ty H; nwhd in ⊢ (??%?);
    486483    nrewrite > H; napply refl
    487484##| #f l s k env m; napply refl
Note: See TracChangeset for help on using the changeset viewer.