Changeset 399


Ignore:
Timestamp:
Dec 10, 2010, 5:05:16 PM (9 years ago)
Author:
campbell
Message:

Rearrange executable semantics a little.

Location:
C-semantics
Files:
1 added
3 moved

Legend:

Unmodified
Added
Removed
  • C-semantics/Cexec.ma

    r398 r399  
    6060  ].
    6161
    62 nlemma exec_bool_of_val_sound: ∀v,ty,r.
    63  exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r).
    64 #v ty r;
    65 ncases v; ##[ ##2: #i ##| ##3: #f ##| ##4: #sp b of ##]
    66 nwhd; ##[ ##4: #H; nwhd in H:(??%?); ndestruct ##]
    67 ncases ty; ##[ ##2,11,20: #sz sg ##| ##3,12,21: #sz ##| ##4,13,22: #sp ty ##| ##5,14,23: #sp ty n ##| ##6,15,24: #args rty ##| ##7,8,16,17,25,26: #id fs ##| ##9,18,27: #id ##]
    68 #H; nwhd in H:(??%?); ndestruct;
    69 ##[ ##1,4: nlapply (eq_spec i zero); nelim (eq i zero);
    70   ##[ ##1,3: #e; nrewrite > e; napply bool_of_val_false; //;
    71   ##| ##2,4: #ne; napply bool_of_val_true; /2/;
    72   ##]
    73 ##| ##3: nelim (eq_dec f Fzero);
    74   ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //;
    75   ##| #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/;
    76   ##]
    77 ##| ##2,5: napply bool_of_val_true; //
    78 ##] nqed.
    79 
    8062nlemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b.
    8163#v ty r H; nelim H; #v t H'; nelim H';
     
    9375(* Prove a few minor results to make proof obligations easy. *)
    9476
    95 nlemma bind_assoc_r: ∀A,B,C,e,f,g.
    96   bind B C (bind A B e f) g = bind A C e (λx.bind B C (f x) g).
    97 #A B C e f g; ncases e; nnormalize; //; nqed.
    98 
    9977nlemma bind_OK: ∀A,B,P,e,f.
    10078  (∀v. e = OK A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
     
    12098#A B C P P' e f; nelim e; //;
    12199#v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed.
    122 
    123 nlemma bool_val_distinct: Vtrue ≠ Vfalse.
    124 @; #H; nwhd in H:(??%%); ndestruct; napply (absurd ? e0 one_not_zero);
    125 nqed.
    126 
    127 nlemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) →
    128   if b then is_true v ty else is_false v ty.
    129 #v ty b; ncases b; #H; ninversion H; #v' ty' H' ev et ev; //;
    130 napply False_ind; napply (absurd ? ev ?);
    131 ##[ ##2: napply sym_neq ##] napply bool_val_distinct;
    132 nqed.
    133100
    134101ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
     
    194161| false ⇒ Error ?
    195162].
    196 
    197 nlemma try_cast_null_sound: ∀m,i,ty,ty',v'. try_cast_null m i ty ty' = OK ? v' → cast m (Vint i) ty ty' v'.
    198 #m i ty ty' v';
    199 nwhd in ⊢ (??%? → ?);
    200 nlapply (eq_spec i zero); ncases (eq i zero);
    201 ##[ #e; nrewrite > e;
    202     ncases ty; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #id ##]
    203     nwhd in ⊢ (??%? → ?); ##[ ##1,3,7,8,9: #H; ndestruct ##]
    204     ncases ty'; ##[ ##2,11,20,29: #sz' sg' ##| ##3,12,21,30: #sz' ##| ##4,13,22,31: #sp' ty' ##| ##5,14,23,32: #sp' ty' n' ##| ##6,15,24,33: #args' res' ##| ##7,8,16,17,25,26,34,35: #id' fs' ##| ##9,18,27,36: #id' ##]
    205     nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
    206     ##[ ##1,5,9: napply cast_ip_z ##| ##*: napply cast_pp_z ##] //;
    207 ##| #_; nwhd in ⊢ (??%? → ?); #H; ndestruct
    208 ##]
    209 nqed.
    210163
    211164ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2).
     
    252205| _ ⇒ Error ?
    253206].
    254 
    255 ndefinition exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'.
    256 #m v ty ty' v';
    257 ncases v;
    258 ##[ #H; nwhd in H:(??%?); ndestruct;
    259 ##| #i; ncases ty;
    260   ##[ #H; nwhd in H:(??%?); ndestruct;
    261   ##| ##3,9: #a; #H; nwhd in H:(??%?); ndestruct;
    262   ##| ##7,8: #a b; #H; nwhd in H:(??%?); ndestruct;
    263   ##| #sz1 si1; ncases ty';
    264     ##[ #H; nwhd in H:(??%?); ndestruct;
    265     ##| ##3,9: #a; #H; nwhd in H:(??%?); ndestruct; //
    266     ##| ##2,7,8: #a b; #H; nwhd in H:(??%?); ndestruct; //
    267     ##| ##4,5,6: ##[ #sp ty''; nletin t ≝ (Tpointer sp ty'')
    268                  ##| #sp ty'' n; nletin t ≝ (Tarray sp ty'' n)
    269                  ##| #args rty; nletin t ≝ (Tfunction args rty) ##]
    270         nwhd in ⊢ (??%? → ?);
    271         nlapply (try_cast_null_sound m i (Tint sz1 si1) t v');
    272         ncases (try_cast_null m i (Tint sz1 si1) t);
    273         ##[ ##1,3,5: #v''; #H' e; napply H'; napply e;
    274         ##| ##*: #_; nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
    275         ##]
    276     ##]
    277   ##| ##*: ##[ #sp ty''; nletin t ≝ (Tpointer sp ty'')
    278            ##| #sp ty'' n; nletin t ≝ (Tarray sp ty'' n)
    279            ##| #args rty; nletin t ≝ (Tfunction args rty) ##]
    280         nwhd in ⊢ (??%? → ?);
    281         nlapply (try_cast_null_sound m i t ty' v');
    282         ncases (try_cast_null m i t ty');
    283         ##[ ##1,3,5: #v''; #H' e; napply H'; napply e;
    284         ##| ##*: #_; nwhd in ⊢ (??%? → ?); #H; ndestruct (H);
    285         ##]
    286   ##]
    287 ##| #f; ncases ty;  ##[ ##3,9: #x; ##| ##2,4,6,7,8: #x y; ##| ##5: #x y z; ##]
    288                     ##[ ncases ty'; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
    289                         nwhd in e:(??%?); ndestruct; //;
    290                     ##| ##*: #e; nwhd in e:(??%?); ndestruct
    291                     ##]
    292 ##| #sp b of; nwhd in ⊢ (??%? → ?); #e;
    293     nelim (bind_inversion ????? e); #s; *; #es e';
    294     nelim (bind_inversion ????? e'); #u; *; #eu e'';
    295     nelim (bind_inversion ????? e''); #s'; *; #es' e''';
    296     ncut (type_space ty s);
    297     ##[ ncases ty in es:(??%?) ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
    298         nwhd in e:(??%?); ndestruct; //;
    299     ##| #Hty;
    300         ncut (type_space ty' s');
    301         ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##]
    302             nwhd in e:(??%?); ndestruct; //;
    303         ##| #Hty';
    304             ncut (s = sp). nelim (ms_eq_dec sp s) in eu; //; nnormalize; #_; #e; ndestruct.
    305             #e; nrewrite < e;
    306             nwhd in match (is_pointer_compat ??) in e''';
    307             ncases (pointer_compat_dec (block_space m b) s') in e'''; #Hcompat e''';
    308             nwhd in e''':(??%?); ndestruct (e'''); /2/
    309         ##]
    310     ##]
    311 ##] nqed.
    312207
    313208ndefinition load_value_of_type' ≝
     
    423318match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
    424319
    425 nlet rec expr_lvalue_ind
    426   (P:expr → Prop)
    427   (Q:expr_descr → type → Prop)
    428   (ci:∀ty,i.P (Expr (Econst_int i) ty))
    429   (cf:∀ty,f.P (Expr (Econst_float f) ty))
    430   (lv:∀e,ty. Q e ty → Plvalue P e ty)
    431   (vr:∀v,ty.Q (Evar v) ty)
    432   (dr:∀e,ty.P e → Q (Ederef e) ty)
    433   (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty))
    434   (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty))
    435   (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty))
    436   (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty))
    437   (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty))
    438   (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty))
    439   (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty))
    440   (sz:∀ty,ty'. P (Expr (Esizeof ty') ty))
    441   (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty)
    442   (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty))
    443   (xx:∀e,ty. is_not_lvalue e → Q e ty)
    444   (e:expr) on e : P e ≝
    445 match e with
    446 [ Expr e' ty ⇒
    447   match e' with
    448   [ Econst_int i ⇒ ci ty i
    449   | Econst_float f ⇒ cf ty f
    450   | Evar v ⇒ lv (Evar v) ty (vr v ty)
    451   | Ederef e'' ⇒ lv (Ederef e'') ty (dr e'' ty (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e''))
    452   | Eaddrof e'' ⇒ match e'' with [ Expr e0 ty0 ⇒ ao ty e0 ty0 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e0 ty0) ]
    453   | Eunop op e'' ⇒ uo ty op e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
    454   | Ebinop op e1 e2 ⇒ bo ty op e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
    455   | Ecast ty' e'' ⇒ ca ty ty' e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
    456   | Econdition e1 e2 e3 ⇒ cd ty e1 e2 e3 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e3)
    457   | Eandbool e1 e2 ⇒ ab ty e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
    458   | Eorbool e1 e2 ⇒ ob ty e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2)
    459   | Esizeof ty' ⇒ sz ty ty'
    460   | Efield e'' i ⇒ match e'' with [ Expr ef tyf ⇒ lv (Efield (Expr ef tyf) i) ty (fl ty ef tyf i (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx ef tyf)) ]
    461   | Ecost l e'' ⇒ co ty l e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
    462   ]
    463 ]
    464 and lvalue_expr_ind
    465   (P:expr → Prop)
    466   (Q:expr_descr → type → Prop)
    467   (ci:∀ty,i.P (Expr (Econst_int i) ty))
    468   (cf:∀ty,f.P (Expr (Econst_float f) ty))
    469   (lv:∀e,ty. Q e ty → Plvalue P e ty)
    470   (vr:∀v,ty.Q (Evar v) ty)
    471   (dr:∀e,ty.P e → Q (Ederef e) ty)
    472   (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty))
    473   (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty))
    474   (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty))
    475   (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty))
    476   (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty))
    477   (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty))
    478   (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty))
    479   (sz:∀ty,ty'. P (Expr (Esizeof ty') ty))
    480   (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty)
    481   (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty))
    482   (xx:∀e,ty. is_not_lvalue e → Q e ty)
    483   (e:expr_descr) (ty:type) on e : Q e ty ≝
    484   match e return λe0. Q e0 ty with
    485   [ Evar v ⇒ vr v ty
    486   | Ederef e'' ⇒ dr e'' ty (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')
    487   | Efield e' i ⇒ match e' return λe1.Q (Efield e1 i) ty with [ Expr e'' ty'' ⇒ fl ty e'' ty'' i (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'' ty'') ]
    488   | _ ⇒ xx ? ty ?
    489   ]. nwhd; napply I; nqed.
    490 
    491 
    492 ntheorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr.
    493 (P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)).
    494 #ge en m e; napply (expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e);
    495 ##[ ##1,2: #ty c; nwhd; //;
    496 (* expressions that are lvalues *)
    497 ##| #e' ty; ncases e'; //; ##[ #i He' ##| #e He' ##| #e i He' ##] nwhd in He' ⊢ %;
    498     napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
    499     napply opt_bind_OK;  #vl evl; nwhd in evl:(??%?); napply (eval_Elvalue … evl);
    500     nrewrite > H in He'; #He'; napply He';
    501 ##| #v ty;
    502     nwhd in ⊢ (???%);
    503     nlapply (refl ? (get ident PTree block v en));
    504     ncases (get ident PTree block v en) in ⊢ (???% → %);
    505     ##[ #eget; napply opt_bind_OK; #sploc; ncases sploc; #sp loc efind;
    506         nwhd; napply (eval_Evar_global … eget efind);
    507     ##| #loc eget; napply (eval_Evar_local … eget);
    508     ##]
    509 ##| #ty e He; nwhd in ⊢ (???%);
    510     napply bind2_OK; #v; ncases v; //; #sp l ofs tr Hv; nwhd;
    511     napply eval_Ederef; nrewrite > Hv in He; #He; napply He;
    512 ##| #ty e'' ty'' He''; napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
    513     nwhd; napply eval_Eaddrof; nrewrite > H in He''; #He''; napply He'';
    514 ##| #ty op e1 He1; napply bind2_OK; #v1 tr Hv1;
    515     napply opt_bind_OK; #v ev;
    516     napply (eval_Eunop … ev);
    517     nrewrite > Hv1 in He1; #He1; napply He1;
    518 ##| #ty op e1 e2 He1 He2;
    519     napply bind2_OK; #v1 tr1 ev1; nrewrite > ev1 in He1; #He1;
    520     napply bind2_OK; #v2 tr2 ev2; nrewrite > ev2 in He2; #He2;
    521     napply opt_bind_OK; #v ev; nwhd in He1 He2; nwhd;
    522     napply (eval_Ebinop … He1 He2 ev);
    523 ##| #ty ty' e' He';
    524     napply bind2_OK; #v tr Hv; nrewrite > Hv in He'; #He';
    525     napply bind_OK; #v' ev';
    526     napply (eval_Ecast … He' ?);
    527     /2/;
    528 ##| #ty e1 e2 e3 He1 He2 He3;
    529     napply bind2_OK; #vb tr1 Hvb; nrewrite > Hvb in He1; #He1;
    530     napply bind_OK; #b;
    531     ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    532     napply bind2_OK; #v tr Hv;
    533     ##[ nrewrite > Hv in He2; #He2; nwhd in He2 Hv:(??%?) ⊢%;
    534         napply (eval_Econdition_true … He1 ? He2);  napply (bool_of ??? Hb);
    535     ##| nrewrite > Hv in He3; #He3; nwhd in He3 Hv:(??%?) ⊢%;
    536         napply (eval_Econdition_false … He1 ? He3);  napply (bool_of ??? Hb);
    537     ##]
    538 ##| #ty e1 e2 He1 He2;
    539     napply bind2_OK; #v1 tr1 Hv1; nrewrite > Hv1 in He1; #He1;
    540     napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1;
    541     ##[ napply bind2_OK; #v2 tr2 Hv2; nrewrite > Hv2 in He2; #He2;
    542         napply bind_OK; #b2 eb2;
    543         napply (eval_Eandbool_2 … He1 … He2);
    544         ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##]
    545     ##| napply (eval_Eandbool_1 … He1); napply (bool_of … Hb1);
    546     ##]
    547 ##| #ty e1 e2 He1 He2;
    548     napply bind2_OK; #v1 tr1 Hv1; nrewrite > Hv1 in He1; #He1;
    549     napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1;
    550     ##[ napply (eval_Eorbool_1 … He1); napply (bool_of … Hb1);
    551     ##| napply bind2_OK; #v2 tr2 Hv2; nrewrite > Hv2 in He2; #He2;
    552         napply bind_OK; #b2 eb2;
    553         napply (eval_Eorbool_2 … He1 … He2);
    554         ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##]
    555     ##]
    556 ##| #ty ty'; nwhd; //
    557 ##| #ty e' ty' i; ncases ty'; //;
    558     ##[ #id fs He'; napply bind2_OK;  #x; ncases x; #sp l ofs H;
    559         napply bind_OK; #delta Hdelta; nrewrite > H in He'; #He';
    560         napply (eval_Efield_struct …  He' (refl ??) Hdelta);
    561     ##| #id fs He'; napply bind2_OK;  #x; ncases x; #sp l ofs H;
    562         nrewrite > H in He'; #He';
    563         napply (eval_Efield_union … He' (refl ??));
    564     ##]
    565 ##| #ty l e' He'; napply bind2_OK; #v tr1 H; nrewrite > H in He'; #He';
    566     napply (eval_Ecost … He');
    567 (* exec_lvalue fails on non-lvalues. *)
    568 ##| #e' ty; ncases e';
    569     ##[ ##1,2,5,12: #a H ##| ##3,4: #a; * ##| ##13,14: #a b; * ##| ##6,8,10,11: #a b H ##| ##7,9: #a b c H ##]
    570     napply I;
    571 ##] nqed.
    572 
    573 nlemma addrof_eval_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
    574 eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr sp loc off) tr →
    575 eval_lvalue ge en m e sp loc off tr.
    576 #ge en m e sp loc off tr ty H; ninversion H;
    577 ##[ ##1,2,5: #a b H; napply False_ind; ndestruct (H);
    578 ##| #a b c d e f g H1 i H2; nrewrite < H2 in H1; #H1; napply False_ind;
    579     napply (eval_lvalue_inv_ind … H1);
    580     ##[ #a b c d bad; ndestruct (bad);
    581     ##| #a b c d e f bad; ndestruct (bad);
    582     ##| #a b c d e f g bad; ndestruct (bad);
    583     ##| #a b c d e f g  h i j k l m n bad; napply False_ind; ndestruct (bad);
    584     ##| #a b c d e f g h i j k l bad; ndestruct (bad);
    585     ##]
    586 ##| #e' ty' sp' loc' ofs' tr' H e1 e2 e3; ndestruct (e1 e2 e3); napply H;
    587 ##| #a b c d e f g h i bad; ndestruct (bad);
    588 ##| #a b c d e f g h i j k l k l bad; ndestruct (bad);
    589 ##| #a b c d e f g h i j k l m bad; ndestruct (bad);
    590 ##| #a b c d e f g h i j k l m bad; ndestruct (bad);
    591 ##| #a b c d e f g h bad; ndestruct (bad);
    592 ##| #a b c d e f g h i j k l m n bad; ndestruct (bad);
    593 ##| #a b c d e f g h bad; ndestruct (bad);
    594 ##| #a b c d e f g h i j k l m n bad;  ndestruct (bad);
    595 ##| #a b c d e f g h i bad; ndestruct (bad);
    596 ##| #a b c d e f g bad; ndestruct (bad);
    597 ##] nqed.
    598 
    599 nlemma addrof_exec_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty.
    600 exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉 →
    601 exec_expr ge en m (Expr (Eaddrof e) ty) = OK ? 〈Vptr sp loc off, tr〉.
    602 #ge en m e sp loc off tr ty H; nwhd in ⊢ (??%?);
    603 nrewrite > H; //;
    604 nqed.
    605 
    606 ntheorem exec_lvalue_sound: ∀ge,en,m,e.
    607 P_res ? (λr.eval_lvalue ge en m e (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue ge en m e).
    608 #ge en m e; nlapply (refl ? (exec_lvalue ge en m e));
    609 ncases (exec_lvalue ge en m e) in ⊢ (???% → %);
    610 ##[ #x; ncases x; #y; ncases y; #z; ncases z; #sp loc off tr H; nwhd;
    611     napply (addrof_eval_lvalue … Tvoid);
    612     nlapply (addrof_exec_lvalue … Tvoid H); #H';
    613     nlapply (exec_expr_sound ge en m (Expr (Eaddrof e) Tvoid));
    614     nrewrite > H'; #H''; napply H'';
    615 ##| #_; nwhd; napply I;
    616 ##] nqed.
    617 
    618 (* Plain equality versions of the above *)
    619 
    620 ndefinition exec_expr_sound' ≝ λge,en,m,e,v.
    621   λH:exec_expr ge en m e = OK ? v.
    622   P_res_to_P ???? (exec_expr_sound ge en m e) H.
    623 
    624 ndefinition exec_lvalue_sound' ≝ λge,en,m,e,sp,loc,off,tr.
    625   λH:exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉.
    626   P_res_to_P ???? (exec_lvalue_sound ge en m e) H.
    627 
    628320(* TODO: Can we do this sensibly with a map combinator? *)
    629321nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
     
    635327  OK ? 〈cons val v vs, tr1⧺tr2〉
    636328].
    637 
    638 nlemma exec_exprlist_sound: ∀ge,e,m,l. P_res ? (λvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) (exec_exprlist ge e m l).
    639 #ge e m l; nelim l;
    640  nwhd; //;
    641  #e1 es; #IH;
    642 napply bind2_OK; #v tr1 Hv;
    643 napply bind2_OK; #vs tr2 Hvs;
    644 nwhd; napply eval_Econs;
    645 ##[ napply (P_res_to_P … (exec_expr_sound ge e m e1) Hv);
    646 ##| napply (P_res_to_P … IH Hvs);
    647 ##] nqed.
    648329
    649330(* Don't really want to use subset rather than sigma here, but can't be bothered
     
    1013694].
    1014695
    1015 ntheorem exec_step_sound: ∀ge,st.
    1016   P_io ??? (λr. step ge st (\fst r) (\snd r)) (exec_step ge st).
    1017 #ge st; ncases st;
    1018 ##[ #f s k e m; ncases s;
    1019   ##[ ncases k;
    1020     ##[ nwhd in ⊢ (?????%);
    1021         nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %);
    1022         //; #H; nwhd;
    1023         napply step_skip_call; //;
    1024     ##| #s' k'; nwhd; //;
    1025     ##| #ex s' k'; napply step_skip_or_continue_while; @; //;
    1026     ##| #ex s' k';
    1027         napply res_bindIO2_OK; #v tr Hv;
    1028         nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
    1029         nlapply (refl ? bexpr);
    1030         ncases bexpr in ⊢ (???% → %);
    1031         ##[ #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    1032             nwhd in ⊢ (?????%);
    1033             ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv));
    1034               ##[ @; // ##| napply (bool_of … Hb); ##]
    1035             ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv));
    1036               ##[ @; // ##| napply (bool_of … Hb); ##]
    1037             ##]
    1038         ##| #_; //;
    1039         ##]
    1040     ##| #ex s1 s2 k'; napply step_skip_or_continue_for2; @; //;
    1041     ##| #ex s1 s2 k'; napply step_skip_for3;
    1042     ##| #k'; napply step_skip_break_switch; @; //;
    1043     ##| #r f' e' k'; nwhd in ⊢ (?????%);
    1044         nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %);
    1045         //; #H; nwhd;
    1046         napply step_skip_call; //;
    1047     ##]
    1048   ##| #ex1 ex2;
    1049     napply res_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval;
    1050     napply res_bindIO2_OK; #v2 tr2 Hv2;
    1051     napply opt_bindIO_OK; #m' em';
    1052     nwhd; napply (step_assign … (exec_lvalue_sound' … Hlval) (exec_expr_sound' … Hv2) em');
    1053   ##| #lex fex args;
    1054     napply res_bindIO2_OK; #vf tr1 Hvf0; nlapply (exec_expr_sound' … Hvf0); #Hvf;
    1055     napply res_bindIO2_OK; #vargs tr2 Hvargs0; nlapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs;
    1056     napply opt_bindIO_OK; #fd efd;
    1057     napply bindIO_OK; #ety;
    1058     ncases lex; nwhd;
    1059     ##[ napply (step_call_none … Hvf Hvargs efd ety);
    1060     ##| #lhs';
    1061         napply res_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr3 Hlocofs;
    1062         nwhd; napply (step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety);
    1063     ##]
    1064   ##| #s1 s2; nwhd; //;
    1065   ##| #ex s1 s2;
    1066     napply res_bindIO2_OK; #v tr Hv;
    1067     nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
    1068     nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    1069     #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    1070     ##[ napply (step_ifthenelse_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    1071     ##| napply (step_ifthenelse_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb)
    1072     ##]
    1073   ##| #ex s';
    1074     napply res_bindIO2_OK; #v tr Hv;
    1075     nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
    1076     nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    1077     #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    1078     ##[ napply (step_while_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    1079     ##| napply (step_while_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    1080     ##]
    1081   ##| #ex s'; nwhd; //;
    1082   ##| #s1 ex s2 s3; nwhd in ⊢ (?????%); nelim (is_Sskip s1); #Hs1; nwhd in ⊢ (?????%);
    1083     ##[ nrewrite > Hs1;
    1084       napply res_bindIO2_OK; #v tr Hv;
    1085       nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
    1086       nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    1087       #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    1088       ##[ napply (step_for_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    1089       ##| napply (step_for_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb);
    1090       ##]
    1091     ##| napply step_for_start; //;
    1092     ##]
    1093   ##| nwhd in ⊢ (?????%); ncases k; //;
    1094     ##[ #s' k'; nwhd; //;
    1095     ##| #ex s' k'; nwhd; //;
    1096     ##| #ex s' k'; nwhd; //;
    1097     ##| #ex s1 s2 k'; nwhd; //;
    1098     ##| #k'; napply step_skip_break_switch; @2; //;
    1099     ##]
    1100   ##| nwhd in ⊢ (?????%); ncases k; //;
    1101     ##[ #s' k'; nwhd; //;
    1102     ##| #ex s' k'; nwhd; napply step_skip_or_continue_while; @2; //;
    1103     ##| #ex s' k'; nwhd;
    1104       napply res_bindIO2_OK; #v tr Hv;
    1105       nletin bexpr ≝ (exec_bool_of_val v (typeof ex));
    1106       nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
    1107       #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
    1108       ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv));
    1109         ##[ @2; // ##| napply (bool_of … Hb); ##]
    1110       ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv));
    1111         ##[ @2; // ##| napply (bool_of … Hb); ##]
    1112       ##]
    1113     ##| #ex s1 s2 k'; nwhd; napply step_skip_or_continue_for2; @2; //
    1114     ##| #k'; nwhd; //;
    1115     ##]
    1116   ##| #r; nwhd in ⊢ (?????%); ncases r;
    1117     ##[ nwhd; nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %); //; #H;
    1118         napply step_return_0; napply H;
    1119     ##| #ex; ncases (type_eq_dec (fn_return f) Tvoid); //; nwhd in ⊢ (% → ?????%); #Hnotvoid;
    1120         napply res_bindIO2_OK; #v tr Hv;
    1121         nwhd; napply (step_return_1 … Hnotvoid (exec_expr_sound' … Hv));
    1122     ##]
    1123   ##| #ex ls; napply res_bindIO2_OK; #v; ncases v; //; #n tr Hv;
    1124     napply step_switch; napply (exec_expr_sound' … Hv);
    1125   ##| #l s'; nwhd; //;
    1126   ##| #l; nwhd in ⊢ (?????%); nlapply (refl ? (find_label l (fn_body f) (call_cont k)));
    1127       ncases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //;
    1128       #sk; ncases sk; #s' k' H;
    1129       napply (step_goto … H);
    1130   ##| #l s'; nwhd; //;
    1131   ##]
    1132 ##| #f0 vargs k m; nwhd in ⊢ (?????%); ncases f0;
    1133   ##[ #fn;
    1134     napply extract_subset_pair_io; #e m1 ealloc Halloc;
    1135     napply sig_bindIO_OK; #m2 Hbind;
    1136     nwhd; napply (step_internal_function … Halloc Hbind);
    1137   ##| #id argtys rty; napply sig_bindIO_OK; #evs Hevs;
    1138     napply bindIO_OK; #eres; nwhd;
    1139     napply step_external_function; @; ##[ napply Hevs; ##| napply mk_val_correct; ##]
    1140   ##] 
    1141 ##| #v k' m'; nwhd in ⊢ (?????%); ncases k'; //;
    1142     #r f e k; nwhd in ⊢ (?????%); ncases r;
    1143   ##[ nwhd; //;
    1144   ##| #x; ncases x; #y; ncases y; #z; ncases z; #pcl b ofs ty;
    1145     napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //;
    1146   ##]
    1147 ##]
    1148 nqed.
    1149 
    1150696nlet rec make_initial_state (p:program) : res state ≝
    1151697  let ge ≝ globalenv Genv ?? p in
     
    1155701    do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
    1156702    OK ? (Callstate f (nil ?) Kstop m0).
    1157 
    1158 nlemma make_initial_state_sound : ∀p. P_res ? (λs.initial_state p s) (make_initial_state p).
    1159 #p; ncases p; #fns main vars;
    1160 nwhd in ⊢ (???%);
    1161 napply opt_bind_OK; #x; ncases x; #sp b esb;
    1162 napply opt_bind_OK; #u ecode;
    1163 napply opt_bind_OK; #f ef;
    1164 ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##]
    1165 nwhd; napply (initial_state_intro … esb ef);
    1166 nqed.
    1167703
    1168704ndefinition is_final_state : ∀st:state. (Σr. final_state st r) + (¬∃r. final_state st r).
     
    1208744].
    1209745
    1210 ntheorem exec_steps_sound: ∀ge,n,st.
    1211  P_io ??? (λts:trace×state. star (mk_transrel ?? step) ge st (\fst ts) (\snd ts))
    1212  (exec_steps n ge st).
    1213 #ge n; nelim n;
    1214 ##[ #st; nwhd in ⊢ (?????%); nelim (is_final_state st); #H; nwhd; //;
    1215 ##| #n' IH st; nwhd in ⊢ (?????%); nelim (is_final_state st); #H;
    1216   ##[ nwhd; //;
    1217   ##| napply (P_bindIO2_OK ????????? (exec_step_sound …)); #t s'; ncases s';
    1218       ##[ #f s k e m; ##| #fd args k m; ##| #r k m; ##]
    1219       nwhd in ⊢ (? → ?????(??????%?));
    1220       ncases m; #mc mn mp; #Hstep;
    1221       nwhd in ⊢ (?????(??????%?));
    1222       napply (P_bindIO2_OK ????????? (IH …)); #t' s'' Hsteps;
    1223       nwhd; napply (star_step ????????? Hsteps); ##[ ##2,5,8: napply Hstep; ##| ##3,6,9: // ##]
    1224   ##]
    1225 nqed.
    1226 (*
    1227 nlet rec exec_steps_without_proof (n:nat) (ge:genv) (s:state) :
    1228  res (trace×state) ≝
    1229 match is_final_state s with
    1230 [ inl _ ⇒ OK ? 〈E0, s〉
    1231 | inr _ ⇒
    1232   match n with
    1233   [ O ⇒ OK ? 〈E0, s〉
    1234   | S n' ⇒
    1235       〈t,s'〉 ← exec_step ge s;
    1236       〈t',s''〉 ← exec_steps_without_proof n' ge s';
    1237       OK ? 〈t ⧺ t',s''〉
    1238   ]
    1239 ].
    1240 *)
    1241 
    1242 
    1243 
    1244746(* A (possibly non-terminating) execution.   *)
    1245747ncoinductive execution : Type ≝
     
    1297799nqed.
    1298800
    1299 (* Finite number of steps without interaction. *)
    1300 ninductive execution_steps : trace → execution → execution → Prop ≝
    1301 | steps_none : ∀e. execution_steps E0 e e
    1302 | steps_one : ∀e,e',tr,tr',s. execution_steps tr' e e' → execution_steps (tr⧺tr') (e_step tr s e) e'.
    1303 
    1304 nlemma one_step: ∀ge,tr,s,tr',s',e.
    1305   exec_inf_aux ge (Value ??? 〈tr,s〉) = e_step tr s (e_step tr' s' e) →
    1306   step ge s tr' s'.
    1307 #ge tr s tr' s' e;
    1308 nrewrite > (exec_inf_aux_unfold ge ?);
    1309 nwhd in ⊢ (??%? → ?); ncases (is_final_state s);
    1310 ##[ #H E; nwhd in E:(??%?); ndestruct (E);
    1311 ##| #H E; nwhd in E:(??%?); ndestruct;
    1312     nrewrite > (exec_inf_aux_unfold ge ?) in e0;
    1313     nlapply (refl ? (exec_step ge s));
    1314     ncases (exec_step ge s) in ⊢ (???% → %);
    1315     ##[ #i o E1 E2; nwhd in E2:(??%?); ndestruct (E2);
    1316     ##| #x; ncases x; #tr'' s'' E1 E2; nwhd in E2:(??%?);
    1317         ncases (is_final_state s'') in E2;
    1318         #H' E2; nwhd in E2:(??%?); ndestruct (E2);
    1319         nlapply (exec_step_sound ge s);
    1320         nrewrite > E1; nwhd in ⊢ (% → ?);
    1321         #H1; napply H1
    1322     ##| #E1 E2; nwhd in E2:(??%?); ndestruct;
    1323     ##]
    1324 ##] nqed.
    1325 
  • C-semantics/CexecComplete.ma

    r398 r399  
    1 include "CexecIOequiv.ma".
     1include "Cexec.ma".
    22include "Plogic/connectives.ma".
    33
    4 ndefinition yields : ∀A,P. res (Σx:A. P x) → A → Prop ≝
    5 λA,P,e,v. match e with [ OK v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | _ ⇒ False].
    6 
    7 (* This tells us that some execution of e results in v.
     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'.
    88   (There may be many possible executions due to I/O, but we're trying to prove
    99   that one particular one exists corresponding to a derivation in the inductive
    1010   semantics.) *)
    11 nlet rec yieldsIO (A:Type) (P:A → Prop) (e:IO io_out io_in (Σx:A. P x)) (v:A) on e : Prop ≝
     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 ≝
    1218match e with
    1319[ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ]
    14 | Interact _ k ⇒ ∃r.yieldsIO A P (k r) v
     20| Interact _ k ⇒ ∃r.yieldsIO_sig A P (k r) v
    1521| _ ⇒ 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.
    1641
    1742nlemma is_pointer_compat_true: ∀m,b,sp.
     
    2853##| ##skip
    2954##] nqed.
    30 
    31 notation < "vbox( e break ↓ break e')" with precedence 99 for @{'yields ${e} ${e'}}.
    32 interpretation "yields" 'yields e e' = (yields ?? e e').
    33 interpretation "yields IO" 'yields e e' = (yieldsIO ?? e e').
    3455
    3556ntheorem is_det: ∀p,s,s'.
     
    4768##] nqed.
    4869
    49 nlet rec yieldsIObare (A:Type) (a:IO io_out io_in A) (v':A) on a : Prop ≝
    50 match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIObare A (k r) v' | _ ⇒ False ].
    51 
    52 nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
    53 yieldsIObare A a v' →
    54 yieldsIO A P (io_inject io_out io_in A (λx.P x) (Some ? a) p) v'.
    55 #A P a; nelim a;
    56 ##[ #a k IH v' p H; nwhd in H ⊢ %; nelim H; #r H'; @ r; napply IH; napply H';
    57 ##| #v v' p H; napply H;
    58 ##| #a b; *;
    59 ##] nqed.
    60 
    61 ndefinition yieldsbare ≝ λA.λa:res A.λv':A.
    62 match a with [ OK v ⇒ v' = v | _ ⇒ False ].
    63 
    64 nlemma yieldsbare_eq: ∀A,a,v'. yieldsbare A a v' → a = OK ? v'.
    65 #A a v'; ncases a; //; nwhd in ⊢ (% → ?); *;
    66 nqed.
    67 
    6870nlemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
    69 yieldsbare A a v' →
    70 yields A P (err_inject A (λx.P x) (Some ? a) p) v'.
     71yields A a v' →
     72yields_sig A P (err_inject A (λx.P x) (Some ? a) p) v'.
    7173#A P a; ncases a;
    7274##[ #v v' p H; napply H;
     
    7678
    7779ntheorem the_initial_state:
    78   ∀p,s. initial_state p s → yieldsbare ? (make_initial_state p) s.
     80  ∀p,s. initial_state p s → yields ? (make_initial_state p) s.
    7981#p s; ncases p; #fns main globs H;
    8082ninversion H;
     
    8890
    8991nlemma cast_complete: ∀m,v,ty,ty',v'.
    90   cast m v ty ty' v' → yieldsbare ? (exec_cast m v ty ty') v'.
     92  cast m v ty ty' v' → yields ? (exec_cast m v ty ty') v'.
    9193#m v ty ty' v' H;
    9294nelim H;
     
    106108##] nqed.
    107109
    108 nlemma yields_eq: ∀A,P,e,v. yields A P e v → ∃p. e = OK ? (sig_intro … v p).
    109 #A P e v; ncases e;
    110 ##[ #vp; ncases vp; #v' p H; nwhd in H; nrewrite > H; @ p; napply refl;
    111 ##| *;
    112 ##] nqed.
    113 
    114110(* Use to narrow down the choice of expression to just the lvalues. *)
    115111nlemma lvalue_expr: ∀ge,env,m,e,ty,sp,l,ofs,tr. ∀P:expr_descr → Prop.
     
    125121##] nqed.
    126122
    127 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.
     123nlemma 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.
    128124#v ty r H; nelim H; #v t H'; nelim H';
    129125  ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
     
    138134nqed.
    139135
    140 nlemma bool_of_true: ∀v,ty. is_true v ty → yieldsbare ? (exec_bool_of_val v ty) true.
     136nlemma bool_of_true: ∀v,ty. is_true v ty → yields ? (exec_bool_of_val v ty) true.
    141137#v ty H; nelim H;
    142138  ##[ #i is s ne; nwhd; nrewrite > (eq_false … ne); //;
     
    148144nqed.
    149145
    150 nlemma bool_of_false: ∀v,ty. is_false v ty → yieldsbare ? (exec_bool_of_val v ty) false.
     146nlemma bool_of_false: ∀v,ty. is_false v ty → yields ? (exec_bool_of_val v ty) false.
    151147#v ty H; nelim H;
    152148  ##[ #i s; //;
     
    156152nqed.
    157153
    158 nremark eq_to_jmeq: ∀A. ∀a,b:A. a = b → a ≃ b.
    159 #A a b H; nrewrite > H; //; nqed.
    160 
    161 nlemma dep_option_rewrite: ∀A,B:Type. ∀e:option A. ∀r:B. ∀P:B → Prop. ∀Q:e ≃ None A → res (Σx:B. P x). ∀R:∀v. e ≃ Some A v → res (Σx:B. P x). ∀h: e = None A.
    162  yields ?? (Q (eq_to_jmeq ??? h)) r →
    163  yields ?? ((match e return λe'.e ≃ e' → ? with [ None ⇒ λp.Q p | Some v ⇒ λp.R v p ]) (refl_jmeq (option A) e)) r.
    164 #A B e; ncases e;
    165 ##[ #r P Q R h; nwhd in ⊢ (? → ???%?);
    166 napply (streicherKjmeq ?? (λe. yields ?? (Q e) r → yields ?? (Q (refl_jmeq (option A) (None A))) r));
    167 //;
    168 ##| #v r P Q R h; ndestruct (h);
    169 ##] nqed.
    170 
    171154nlemma expr_lvalue_complete: ∀ge,env,m.
    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〉)).
     155(∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉)) ∧
     156(∀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〉)).
    174157#ge env m;
    175158napply (combined_expr_lvalue_ind ge env m
    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〉)));
     159  (λe,v,tr,H. yields ? (exec_expr ge env m e) (〈v,tr〉))
     160  (λe,sp,l,off,tr,H. yields ? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)));
    178161##[ #i ty; napply refl;
    179162##| #f ty; napply refl;
     
    181164    ##[ #id ##| #e' ##| #e' id ##] #H3;
    182165    nwhd in ⊢ (??%?);
    183     nrewrite > (yieldsbare_eq ??? H3);
     166    nrewrite > (yields_eq ??? H3);
    184167    nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
    185168##| #e ty sp l off tr H1 H2; nwhd in ⊢ (??%?);
    186     nrewrite > (yieldsbare_eq ??? H2);
     169    nrewrite > (yields_eq ??? H2);
    187170    napply refl;
    188171##| #ty' ty; napply refl;
    189172##| #op e ty v1 v tr H1 H2 H3; nwhd in ⊢ (??%?);
    190     nrewrite > (yieldsbare_eq ??? H3);
     173    nrewrite > (yields_eq ??? H3);
    191174    nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
    192175##| #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 ⊢ (??%?);
     176    nrewrite > (yields_eq ??? H4); nwhd in ⊢ (??%?);
     177    nrewrite > (yields_eq ??? H5); nwhd in ⊢ (??%?);
    195178    nrewrite > e3; napply refl;
    196179##| #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);
     180    nrewrite > (yields_eq ??? H4); nwhd in ⊢ (??%?);
     181    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
     182    nrewrite > (yields_eq ??? H5);
    200183    napply refl;
    201184##| #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);
     185    nrewrite > (yields_eq ??? H4); nwhd in ⊢ (??%?);
     186    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
     187    nrewrite > (yields_eq ??? H5);
    205188    napply refl;
    206189##| #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));
     190    nrewrite > (yields_eq ??? H3); nwhd in ⊢ (??%?);
     191    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
    209192    napply refl;   
    210193##| #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 ⊢ (??%?);
     194    nrewrite > (yields_eq ??? H5); nwhd in ⊢ (??%?);
     195    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
     196    nrewrite > (yields_eq ??? H6); nwhd in ⊢ (??%?);
    214197    nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb;
    215     nrewrite > (yieldsbare_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb;
     198    nrewrite > (yields_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb;
    216199    napply refl;   
    217200##| #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));
     201    nrewrite > (yields_eq ??? H3); nwhd in ⊢ (??%?);
     202    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
    220203    napply refl;   
    221204##| #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 ⊢ (??%?);
     205    nrewrite > (yields_eq ??? H5); nwhd in ⊢ (??%?);
     206    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
     207    nrewrite > (yields_eq ??? H6); nwhd in ⊢ (??%?);
    225208    nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb;
    226     nrewrite > (yieldsbare_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb;
     209    nrewrite > (yields_eq ??? Hb); nwhd in ⊢ (??%?); nrewrite < evb;
    227210    napply refl;
    228211##| #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));
     212    nrewrite > (yields_eq ??? H3); nwhd in ⊢ (??%?);
     213    nrewrite > (yields_eq ??? (cast_complete … H2));
    231214    napply refl;
    232215##| #e ty v l tr H1 H2; nwhd in ⊢ (??%?);
    233     nrewrite > (yieldsbare_eq ??? H2); nwhd in ⊢ (??%?);
     216    nrewrite > (yields_eq ??? H2); nwhd in ⊢ (??%?);
    234217    napply refl;
    235218   
     
    239222    nrewrite > e2; napply refl;
    240223##| #e ty sp l ofs tr H1 H2; nwhd in ⊢ (??%?);
    241     nrewrite > (yieldsbare_eq ??? H2);
     224    nrewrite > (yields_eq ??? H2);
    242225    napply refl;
    243226##| #e i ty sp l ofs id fList delta tr H1 H2 H3 H4; ncases e in H2 H4 ⊢ %;
    244227    #e' ty' H2; nwhd in H2:(??%?); nrewrite > H2; #H4; nwhd in ⊢ (??%?);
    245     nrewrite > (yieldsbare_eq ??? H4); nwhd in ⊢ (??%?);
     228    nrewrite > (yields_eq ??? H4); nwhd in ⊢ (??%?);
    246229    nrewrite > H3; napply refl;
    247230##| #e i ty sp l ofs id fList tr; ncases e; #e' ty' H1 H2;
    248231    nwhd in H2:(??%?); nrewrite > H2; #H3; nwhd in ⊢ (??%?);
    249     nrewrite > (yieldsbare_eq ??? H3); napply refl;
     232    nrewrite > (yields_eq ??? H3); napply refl;
    250233##] nqed.
    251234
    252235ntheorem expr_complete:  ∀ge,env,m.
    253  ∀e,v,tr. eval_expr ge env m e v tr → yieldsbare ? (exec_expr ge env m e) (〈v,tr〉).
     236 ∀e,v,tr. eval_expr ge env m e v tr → yields ? (exec_expr ge env m e) (〈v,tr〉).
    254237#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
    255238
    256239ntheorem exprlist_complete: ∀ge,env,m,es,vs,tr.
    257   eval_exprlist ge env m es vs tr → yieldsbare ? (exec_exprlist ge env m es) (〈vs,tr〉).
     240  eval_exprlist ge env m es vs tr → yields ? (exec_exprlist ge env m es) (〈vs,tr〉).
    258241#ge env m es vs tr H; nelim H;
    259242##[ napply refl;
    260243##| #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);
     244    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     245    nrewrite > (yields_eq ??? H3);
    263246    napply refl;
    264247##] nqed.
    265248
    266249ntheorem lvalue_complete: ∀ge,env,m.
    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〉).
     250 ∀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〉).
    268251#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
    269252
     
    338321nlemma bind_params_complete: ∀e,m,params,vs,m2.
    339322  bind_parameters e m params vs m2 →
    340   yields ?? (exec_bind_parameters e m params vs) m2.
     323  yields_sig ?? (exec_bind_parameters e m params vs) m2.
    341324#e m params vs m2 H; nelim H;
    342325##[ //;
     
    345328    nrewrite > H1; nwhd in ⊢ (??%?);
    346329    nrewrite > H2; nwhd in ⊢ (??%?);
    347     nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4;
     330    nelim (yields_sig_eq ???? H4); #p4 e4; nrewrite > e4;
    348331    napply refl;
    349332##] nqed.
    350333
    351334nlemma eventval_match_complete': ∀ev,ty,v.
    352   eventval_match ev ty v → yields ?? (check_eventval' v ty) ev.
     335  eventval_match ev ty v → yields_sig ?? (check_eventval' v ty) ev.
    353336#ev ty v H; nelim H; //; nqed.
    354337
    355338nlemma eventval_list_match_complete: ∀vs,tys,evs.
    356   eventval_list_match evs tys vs → yields ?? (check_eventval_list vs tys) evs.
     339  eventval_list_match evs tys vs → yields_sig ?? (check_eventval_list vs tys) evs.
    357340#vs tys evs H; nelim H;
    358341##[ //
    359342##| #e etl ty tytl v vtl H1 H2 H3; napply remove_res_sig;
    360     nelim (yields_eq ???? (eventval_match_complete' … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    361     nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
     343    nelim (yields_sig_eq ???? (eventval_match_complete' … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     344    nelim (yields_sig_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
    362345    napply refl;
    363346##] nqed.
     
    376359
    377360ntheorem step_complete: ∀ge,s,tr,s'.
    378   step ge s tr s' → yieldsIObare ? (exec_step ge s) 〈tr,s'〉.
     361  step ge s tr s' → yieldsIO ? (exec_step ge s) 〈tr,s'〉.
    379362#ge s tr s' H; nelim H;
    380363##[ #f e e1 k e2 m sp loc ofs v m' tr1 tr2 H1 H2 H3; nwhd in ⊢ (??%?);
    381     nrewrite > (yieldsbare_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
    382     nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
     364    nrewrite > (yields_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
     365    nrewrite > (yields_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
    383366    nrewrite > H3; napply refl;
    384367##| #f e eargs k ef m vf vargs f' tr1 tr2 H1 H2 H3 H4; nwhd in ⊢ (??%?);
    385     nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
    386     nrewrite > (yieldsbare_eq ??? (exprlist_complete … H2)); nwhd in ⊢ (??%?);
     368    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     369    nrewrite > (yields_eq ??? (exprlist_complete … H2)); nwhd in ⊢ (??%?);
    387370    nrewrite > H3; nwhd in ⊢ (??%?);
    388371    nrewrite > H4; nelim (assert_type_eq_true (typeof e)); #pty ety; nrewrite > ety;
    389372    napply refl;
    390373##| #f el ef eargs k env m sp loc ofs vf vargs f' tr1 tr2 tr3 H1 H2 H3 H4 H5; nwhd in ⊢ (??%?);
    391     nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
    392     nrewrite > (yieldsbare_eq ??? (exprlist_complete … H3)); nwhd in ⊢ (??%?);
     374    nrewrite > (yields_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
     375    nrewrite > (yields_eq ??? (exprlist_complete … H3)); nwhd in ⊢ (??%?);
    393376    nrewrite > H4; nwhd in ⊢ (??%?);
    394377    nrewrite > H5; nelim (assert_type_eq_true (typeof ef)); #pty ety; nrewrite > ety;
    395378    nwhd in ⊢ (??%?);
    396     nrewrite > (yieldsbare_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
     379    nrewrite > (yields_eq ??? (lvalue_complete … H1)); nwhd in ⊢ (??%?);
    397380    napply refl;
    398381##| #f s1 s2 k env m; napply refl
    399382##| ##5,6,7: #f s k env m; napply refl
    400383##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
    401     nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
    402     nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
     384    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     385    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
    403386    napply refl
    404387##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
    405     nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
    406     nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
     388    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     389    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
    407390    napply refl
    408391##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?);
    409     nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
    410     nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
     392    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     393    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
    411394    napply refl
    412395##| #f e s k env m v tr H1 H2; nwhd in ⊢ (??%?);
    413     nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
    414     nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
     396    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     397    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
    415398    napply refl
    416399##| #f s1 e s2 k env m H; ncases H; #es1; nrewrite > es1; napply refl;
    417400##| ##13,14: #f e s k env m; napply refl
    418401##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?);
    419     nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
    420     nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
     402    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     403    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
    421404    napply refl
    422405##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; nwhd in ⊢ (??%?);
    423     nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
    424     nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
     406    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     407    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
    425408    napply refl
    426409##| #f e s k env m; napply refl;
     
    429412    ##| #H; nwhd in ⊢ (??%?); napply refl ##]
    430413##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
    431     nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
    432     nrewrite > (yieldsbare_eq ??? (bool_of_false ?? H2));
     414    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     415    nrewrite > (yields_eq ??? (bool_of_false ?? H2));
    433416    napply refl;
    434417##| #f e s1 s2 k env m v tr H1 H2; nwhd in ⊢ (??%?);
    435     nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
    436     nrewrite > (yieldsbare_eq ??? (bool_of_true ?? H2));
     418    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     419    nrewrite > (yields_eq ??? (bool_of_true ?? H2));
    437420    napply refl;
    438421##| #f s1 e s2 s3 k env m; *; #es1; nrewrite > es1; napply refl;
     
    442425    napply (dec_false ? (type_eq_dec (fn_return f) Tvoid) H1); #pf';
    443426    nwhd in ⊢ (??%?);
    444     nrewrite > (yieldsbare_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
     427    nrewrite > (yields_eq ??? (expr_complete … H2)); nwhd in ⊢ (??%?);
    445428    napply refl;
    446429##| #f k env m; ncases k;
     
    453436    ##]
    454437##| #f e s k env m i tr H1; nwhd in ⊢ (??%?);
    455     nrewrite > (yieldsbare_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
     438    nrewrite > (yields_eq ??? (expr_complete … H1)); nwhd in ⊢ (??%?);
    456439    napply refl
    457440##| #f s k env m; *; #es; nrewrite > es; napply refl;
     
    461444##| #f args k m1 env m2 m3 H1 H2; nwhd in ⊢ (??%?);
    462445    nelim (alloc_vars_complete … H1); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    463     nelim (yields_eq ???? (bind_params_complete … H2)); #p2 e2; nrewrite > e2;
     446    nelim (yields_sig_eq ???? (bind_params_complete … H2)); #p2 e2; nrewrite > e2;
    464447    napply refl;
    465448##| #id tys rty args k m rv tr H; nwhd in ⊢ (??%?);
    466449    ninversion H; #f' args' rv' eargs erv H1 H2 e1 e2 e3 e4; nrewrite < e1 in H1 H2;
    467450    #H1 H2;
    468     nelim (yields_eq ???? (eventval_list_match_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
     451    nelim (yields_sig_eq ???? (eventval_list_match_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
    469452    nwhd; ninversion H2; #x e5 e6 e7; @ x; nwhd in ⊢ (??%?);
    470453    napply refl
     
    474457##| #f l s k env m; napply refl
    475458##] nqed.
    476 
    477 nlemma exec_from_wrong: ∀ge,s.
    478   exec_from ge s se_wrong →
    479   exec_step ge s = Wrong ???.
    480 #ge s H; nwhd in H;
    481 ninversion H;
    482 ##[ #tr r m EXEC E; ndestruct (E)
    483 ##| #tr s' e e' H EXEC E; ndestruct (E)
    484 ##| nrewrite > (exec_inf_aux_unfold …);
    485     ncases (exec_step ge s);
    486   ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
    487   ##| #x; ncases x; #tr s'; nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
    488       #F EXEC; nwhd in EXEC:(??%?); ndestruct
    489   ##| //
    490   ##]
    491 ##| #o k i e H EXEC E; ndestruct
    492 ##] nqed.
    493 
    494 nlemma exec_from_step_notfinal: ∀ge,s,tr,s',e.
    495   exec_from ge s (se_step tr s' e) →
    496   ¬(∃r. final_state s' r).
    497 #ge s tr s' e H; nwhd in H; ninversion H;
    498 ##[ #tr' r m EXEC E; ndestruct
    499 ##| #tr' s'' e' e'' H EXEC E; ndestruct (E);
    500     nrewrite > (exec_inf_aux_unfold …) in EXEC;
    501     ncases (exec_step ge s);
    502     ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
    503     ##| #x; ncases x; #tr1 s1; nwhd in ⊢ (??%? → ?); ncases (is_final_state s1);
    504         #F E; nwhd in E:(??%?); ndestruct; napply F;
    505     ##| #E; nwhd in E:(??%?); ndestruct
    506     ##]
    507 ##| #EXEC E; ndestruct
    508 ##| #o k i e' H EXEC E; ndestruct
    509 ##] nqed.
    510 
    511 nlemma exec_from_interact_step_notfinal: ∀ge,s,o,k,i,tr,s',e.
    512   exec_from ge s (se_interact o k i (se_step tr s' e)) →
    513   ¬(∃r. final_state s' r).
    514 #ge s o k i tr s' e H;
    515 @; *; #r F; ncases F in H; #r' m H;
    516 ninversion H;
    517 ##[ #tr' r m EXEC E; ndestruct
    518 ##| #tr' s'' e' e'' H EXEC E; ndestruct (E);
    519 ##| #EXEC E; ndestruct
    520 ##| #o' k' i' e' H EXEC E; ndestruct;
    521     nrewrite > (exec_inf_aux_unfold …) in EXEC;
    522     ncases (exec_step ge s);
    523     ##[ #o1 k1 EXEC1; nwhd in EXEC1:(??%?); ndestruct (EXEC1);
    524         ninversion H;
    525         ##[ #tr1 r1 m1 EXECK E; ndestruct (E);
    526         ##| #tr1 s1 e1 e2 H1 EXECK E; ndestruct (E);
    527             nrewrite > (exec_inf_aux_unfold …) in EXECK;
    528             ncases (k1 i');
    529             ##[ #o2 k2 EXECK; nwhd in EXECK:(??%?); ndestruct
    530             ##| #x; ncases x; #tr2 s2; nwhd in ⊢ (??%? → ?);
    531                 ncases (is_final_state s2); #F EXECK;
    532                 nwhd in EXECK:(??%?); ndestruct;
    533                 napply (absurd ?? F);
    534                 @ r'; //;
    535             ##| #E; nwhd in E:(??%?); ndestruct
    536             ##]
    537         ##| #EXECK E;  nwhd in E:(??%?); ndestruct
    538         ##| #o2 k2 i2 e2 H2 EXECK E; ndestruct
    539         ##]
    540     ##| #x; ncases x; #tr1 s1; nwhd in ⊢ (??%? → ?);
    541         ncases (is_final_state s1); #F E; nwhd in E:(??%?); ndestruct;
    542     ##| #E; nwhd in E:(??%?); ndestruct
    543     ##]
    544 ##] nqed.
    545 
    546 nlemma wrong_sound: ∀ge,tr,s,s',e.
    547   execution_goes_wrong tr s (se_step E0 s e) s' →
    548   exec_from ge s e →
    549   (¬∃r. final_state s r) →
    550   star (mk_transrel … step) ge s tr s' ∧
    551   nostep (mk_transrel … step) ge s' ∧
    552   (¬∃r. final_state s' r).
    553 #ge tr0 s0 s0' e0 WRONG; ninversion WRONG;
    554 #tr s s' e ESTEPS E1 E2 E3 E4 EXEC NOTFINAL; ndestruct (E1 E2 E3 E4);
    555 ncases (several_steps … ESTEPS EXEC);
    556 #STAR EXEC'; @;
    557 ##[ @; ##[ napply STAR;
    558        ##| #badtr bads; @; #badSTEP;
    559            nlapply (step_complete … badSTEP);
    560            nrewrite > (exec_from_wrong … EXEC');
    561            //;
    562        ##]
    563 ##| @;
    564     nelim ESTEPS in NOTFINAL EXEC ⊢ %;
    565     ##[ #s1 e1 NF EX F; napply (absurd ? F NF);
    566     ##| #e1 e2 tr1 tr2 s1 s2 s3 ESTEPS1 IH NF EXEC;
    567         ncases (exec_from_step … EXEC); #EXEC3 EXEC1;
    568         napply (IH … EXEC1);
    569         napply (exec_from_step_notfinal … EXEC);
    570     ##| #e1 e2 o k i s1 s2 s3 tr1 tr2 ESTEPS1 IH NF EXEC;
    571         napply IH;
    572         ##[ napply (exec_from_interact_step_notfinal … EXEC);
    573         ##| ncases (exec_from_interact … EXEC); //;
    574         ##]
    575     ##]
    576 ##] nqed.
    577 
    578 ninductive execution_characterisation : state → s_execution → Prop ≝
    579 | ec_terminates: ∀s,r,m,e,tr.
    580     execution_terminates tr s e r m →
    581     execution_characterisation s e
    582 | ec_diverges: ∀s,e,tr.
    583     execution_diverges tr s e →
    584     execution_characterisation s e
    585 | ec_reacts: ∀s,e,tr.
    586     execution_reacts tr s e →
    587     execution_characterisation s e
    588 | ec_wrong: ∀e,s,s',tr.
    589     execution_goes_wrong tr s e s' →
    590     execution_characterisation s e.
    591 
    592 (* bit of a hack to avoid inability to reduce term in match *)
    593 ndefinition interact_prop : ∀A:Type.(∀o:io_out. (io_in o → IO io_out io_in A) → Prop) → IO io_out io_in A → Prop ≝
    594 λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ].
    595 
    596 nlemma err_does_not_interact: ∀A,B,P,e1,e2.
    597   (∀x:B.interact_prop A P (e2 x)) →
    598   interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2).
    599 #A B P e1 e2 H;
    600 ncases e1; //; nqed.
    601 
    602 nlemma err2_does_not_interact: ∀A,B,C,P,e1,e2.
    603   (∀x,y.interact_prop A P (e2 x y)) →
    604   interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2).
    605 #A B C P e1 e2 H;
    606 ncases e1; ##[ #z; ncases z; ##] //; nqed.
    607 
    608 nlemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2.
    609   (∀x.interact_prop A P (e2 x)) →
    610   interact_prop A P (bindIO ?? (sigma B Q) A (err_to_io_sig ??? Q e1) e2).
    611 #A B P Q e1 e2 H;
    612 ncases e1; //; nqed.
    613 
    614 nlemma opt_does_not_interact: ∀A,B,P,e1,e2.
    615   (∀x:B.interact_prop A P (e2 x)) →
    616   interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2).
    617 #A B P e1 e2 H;
    618 ncases e1; //; nqed.
    619 
    620 nlemma exec_step_interaction:
    621   ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s).
    622 #ge s; ncases s;
    623 ##[ #f st kk e m; ncases st;
    624   ##[ ##11,14: #a ##| ##2,4,6,7,12,13,15: #a b ##| ##3,5: #a b c ##| ##8: #a b c d ##]
    625   ##[ ##4,6,8,9: napply I ##]
    626   nwhd in ⊢ (???%);
    627   ##[ ncases a; ##[ ncases (fn_return f); //; ##| #e; nwhd nodelta in ⊢ (???%);
    628                     ncases (type_eq_dec (fn_return f) Tvoid); #x; //; napply err2_does_not_interact; // ##]
    629   ##| ncases (find_label a (fn_body f) (call_cont kk)); ##[ napply I ##| #z; ncases z; #x y; napply I ##]
    630   ##| napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5; napply I
    631   ##| ##4,7: napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I
    632   ##| napply err2_does_not_interact; #x1 x2; ncases x1; //;
    633   ##| napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5;  napply err_does_not_interact; #x6; ncases a;
    634       ##[ napply I; ##| #x7; napply err2_does_not_interact; #x8 x9; napply I ##]
    635   ##| ncases (is_Sskip a); #H; ##[ napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I
    636       ##| napply I ##]
    637   ##| ncases kk; ##[ ##1,8: ncases (fn_return f); //; ##| ##2,3,5,6,7: //;
    638       ##| #z1 z2 z3; napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I ##]
    639   ##| ncases kk; //;
    640   ##| ncases kk; ##[ ##4: #z1 z2 z3;  napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I
    641       ##| ##*: // ##]
    642   ##]
    643 ##| #f args kk m; ncases f;
    644   ##[ #f'; nwhd in ⊢ (???%); ncases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'));
    645       #x; ncases x; ##[ *; ##| #z; ncases z; #x1 x2 H;
    646                         napply err_sig_does_not_interact; //; ##]
    647   (* This is the only case that actually matters! *)
    648   ##| #fn argtys rty; nwhd in ⊢ (???%);
    649       napply  err_sig_does_not_interact; #x1;
    650       nwhd; #i; @; ##[ ##2: @; ##[ ##2: @; ##[ @; nwhd in ⊢ (??%?); napply refl;
    651         ##| @; #E; nwhd in E:(??%%); ndestruct (E); ##] ##] ##]
    652   ##]
    653 ##| #v kk m; nwhd in ⊢ (???%); ncases kk;
    654     ##[ ##8: #x1 x2 x3 x4; ncases x1;
    655       ##[ nwhd in ⊢ (???%); ncases v; // ##| #x5; nwhd in ⊢ (???%); ncases x5;
    656           #x6 x7; napply opt_does_not_interact; // ##]
    657     ##| ##*: // ##]
    658 ##] nqed.
    659 
    660 
    661 (* Some classical logic (roughly like a fragment of Coq's library) *)
    662 nlemma classical_doubleneg:
    663   ∀classic:(∀P:Prop.P ∨ ¬P).
    664   ∀P:Prop. ¬ (¬ P) → P.
    665 #classic P; *; #H;
    666 ncases (classic P);
    667 ##[ // ##| #H'; napply False_ind; /2/; ##]
    668 nqed.
    669 
    670 nlemma classical_not_all_not_ex:
    671   ∀classic:(∀P:Prop.P ∨ ¬P).
    672   ∀A:Type.∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x.
    673 #classic A P; *; #H;
    674 napply (classical_doubleneg classic); @; *; #H';
    675 napply H; #x; @; #H''; napply H'; @x; napply H'';
    676 nqed.
    677 
    678 nlemma classical_not_all_ex_not:
    679   ∀classic:(∀P:Prop.P ∨ ¬P).
    680   ∀A:Type.∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x.
    681 #classic A P; *; #H;
    682 napply (classical_not_all_not_ex classic A (λx.¬ P x));
    683 @; #H'; napply H; #x; napply (classical_doubleneg classic);
    684 napply H';
    685 nqed.
    686 
    687 nlemma not_ex_all_not:
    688   ∀A:Type.∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x.
    689 #A P; *; #H x; @; #H';
    690 napply H; @ x; napply H';
    691 nqed.
    692 
    693 nlemma not_imply_elim:
    694   ∀classic:(∀P:Prop.P ∨ ¬P).
    695   ∀P,Q:Prop. ¬ (P → Q) → P.
    696 #classic P Q; *; #H;
    697 napply (classical_doubleneg classic); @; *; #H';
    698 napply H; #H''; napply False_ind; napply H'; napply H'';
    699 nqed.
    700 
    701 nlemma not_imply_elim2:
    702   ∀P,Q:Prop. ¬ (P → Q) → ¬ Q.
    703 #P Q; *; #H; @; #H';
    704 napply H; #_; napply H';
    705 nqed.
    706 
    707 nlemma imply_to_and:
    708   ∀classic:(∀P:Prop.P ∨ ¬P).
    709   ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q.
    710 #classic P Q H; @;
    711 ##[ napply (not_imply_elim classic P Q H);
    712 ##| napply (not_imply_elim2 P Q H);
    713 ##] nqed.
    714 
    715 nlemma not_and_to_imply:
    716   ∀classic:(∀P:Prop.P ∨ ¬P).
    717   ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q.
    718 #classic P Q; *; #H H';
    719 @; #H''; napply H; @; //;
    720 nqed.
    721 
    722 ninductive execution_not_over : s_execution → Prop ≝
    723 | eno_step: ∀tr,s,e. execution_not_over (se_step tr s e)
    724 | eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)).
    725 
    726 nlemma eno_stop: ∀tr,r,m. execution_not_over (se_stop tr r m) → False.
    727 #tr0 r0 m0 H; ninversion H;
    728 ##[ #tr s e E; ndestruct
    729 ##| #o k tr s e i E; ndestruct
    730 ##] nqed.
    731 
    732 nlemma eno_wrong: execution_not_over se_wrong → False.
    733 #H; ninversion H;
    734 ##[ #tr s e E; ndestruct
    735 ##| #o k tr s e i E; ndestruct
    736 ##] nqed.
    737 
    738 nlet corec show_divergence s e
    739  (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
    740                  execution_not_over e1)
    741  (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0)
    742  (CONTINUES:∀tr2,s2,o,k,i,e'. execution_isteps tr2 s e s2 (se_interact o k i e') → ∃tr3.∃s3.∃e3. e' = se_step tr3 s3 e3 ∧ tr3 ≠ E0)
    743  : execution_diverging e ≝ ?.
    744 nlapply (NONTERMINATING E0 s e ?); //;
    745 ncases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %;
    746 ##[ #tr i m; #_; #_; #_; #ENO; nelim (eno_stop … ENO);
    747 ##| #tr s' e' UNREACTIVE; nlapply (UNREACTIVE tr s' e' ?);
    748   ##[ nrewrite < (E0_right tr) in ⊢ (?%????);
    749       napply isteps_one; napply isteps_none;
    750   ##| #TR; napply (match sym_eq ??? TR with [ refl ⇒ ? ]); (* nrewrite > TR in UNREACTIVE ⊢ %;*)
    751       #NONTERMINATING CONTINUES; #_; @;
    752       napply (show_divergence s');
    753       ##[ #tr1 s1 e1 S; napply (NONTERMINATING tr1 s1 e1);
    754         nchange in ⊢ (?%????) with (Eapp E0 tr1); napply isteps_one;
    755         napply S;
    756       ##| #tr2 s2 e2 S; nrewrite > TR in UNREACTIVE; #UNREACTIVE; napply (UNREACTIVE tr2 s2 e2);
    757           nchange in ⊢ (?%????) with (Eapp E0 tr2);
    758           napply isteps_one; napply S;
    759       ##| #tr2 s2 o k i e2 S; napply (CONTINUES tr2 s2 o k i);
    760           nchange in ⊢ (?%????) with (Eapp E0 tr2);
    761           napply (isteps_one … S);
    762       ##]
    763   ##]
    764 ##| #_; #_; #_; #ENO; nelim (eno_wrong … ENO);
    765 ##| #o k i e' UNREACTIVE NONTERMINATING CONTINUES; #_;
    766     nlapply (CONTINUES E0 s o k i e' (isteps_none …));
    767     *; #tr'; *; #s'; *; #e'; *; #EXEC NOTSILENT;
    768     napply False_ind; napply (absurd ?? NOTSILENT);
    769     napply (UNREACTIVE … s' e');
    770     nrewrite < (E0_right tr') in ⊢ (?%????);
    771     nrewrite > EXEC;
    772     napply isteps_interact; //;
    773 ##] nqed.
    774 (*
    775 nlemma exec_over_isteps: ∀ge,tr,s,s',e,e'.
    776   execution_isteps tr s e s' e' →
    777   e = (exec_inf_aux ge (exec_step ge s)) →
    778   exec_inf_aux ge (exec_step ge s') = e'.
    779 #ge tr0 s0 s0' e0 e0';
    780 #ISTEPS; nelim ISTEPS;
    781 ##[ #s e E; nrewrite > E; napply refl;
    782 ##| #e1 e2 tr1 tr2 s1 s2 s3 ISTEPS' IH E;
    783     napply IH; napply sym_eq; napply exec_e_step;
    784     ##[ ##3: napply sym_eq; napply E ##]
    785 ##| #e1 e2 o k i s1 s2 s3 tr1 tr2 ISTEPS' EXECK IH E;
    786     napply IH;
    787     ncases (exec_step ge s3) in E;
    788     ##[ #o' k'; nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
    789         #E'; nwhd in E':(???%); ndestruct (E');
    790         napply sym_eq; napply exec_e_step;
    791         ##[ ##3: napply EXECK; ##]
    792     ##| #z; ncases z; #tr' s';
    793         nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
    794         nwhd in ⊢ (???% → ?); ncases (is_final_state s');
    795         #F E'; nwhd in E':(???%); ndestruct (E');
    796     ##| nrewrite > (exec_inf_aux_unfold …) in ⊢ (% → ?);
    797         #E'; nwhd in E':(???%); ndestruct (E');
    798     ##]
    799 ##] nqed.
    800 
    801 nlemma exec_over_isteps': ∀ge,tr,s,s',e'.
    802   execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s' e' →
    803   exec_inf_aux ge (exec_step ge s') = e'.
    804 #ge tr s s' e'; nletin e ≝ (exec_inf_aux ge (exec_step ge s)); #H;
    805 napply (exec_over_isteps … H (refl ??));
    806 nqed.
    807 *)
    808 include "Plogic/jmeq.ma".
    809 
    810 nlemma se_inv: ∀e1,e2.
    811   single_exec_of e1 e2 →
    812   match e1 with
    813   [ e_stop tr r m ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ m = m' | _ ⇒ False ]
    814   | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
    815   | e_wrong ⇒ match e2 with [ se_wrong ⇒ True | _ ⇒ False ]
    816   | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ]
    817   ].
    818 #e01 e02 H;
    819 ncases H;
    820 ##[ #tr r m; nwhd; @; ##[ @ ##] //
    821 ##| #tr s e1' e2' H'; nwhd; @; ##[ @ ##] //
    822 ##| nwhd; //
    823 ##| #o k i e H'; nwhd; @; ##[ @ ##] //
    824 ##] nqed.
    825 
    826 nlemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
    827   exec_from ge s (se_interact o k i (se_step tr s' e)) →
    828   tr ≠ E0.
    829 #ge o k i tr s s' e; nwhd in ⊢ (% → ?); nrewrite > (exec_inf_aux_unfold …);
    830 nlapply (exec_step_interaction ge s);
    831 ncases (exec_step ge s);
    832 ##[ #o' k' ; nwhd in ⊢ (% → ?%? → ?); #H K; ncases (se_inv … K);
    833     *; #E1 E2 H1; ndestruct (E1);
    834     nlapply (H i); *; #tr'; *; #s''; *; #K' TR;
    835     nrewrite > E2 in H1; #H1; nwhd in H1:(?%?); nrewrite > K' in H1;
    836     nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (?%? → ?);
    837     ncases (is_final_state s'');
    838     ##[ #F; nwhd in ⊢ (?%? → ?); #S;
    839         napply False_ind; napply (absurd ? S); ncases (se_inv … S)
    840     ##| #NF S; nwhd in S:(?%?); ncases (se_inv … S);
    841         *; #E1 E2 S'; nrewrite < E1; napply TR
    842     ##]
    843 ##| #x; ncases x; #tr' s'' H; nwhd in ⊢ (?%? → ?);
    844     ncases (is_final_state s''); #F E; nwhd in E:(?%?);
    845     ninversion E;
    846     ##[ ##1,5: #tr1 e1 m1 E1 E2; ndestruct
    847     ##| ##2,6: #tr s1 e1 e2 H E1 E2; ndestruct
    848     ##| ##3,7: #E; ndestruct
    849     ##| ##4,8: #o1 k1 i1 e1 H1 E1 E2; ndestruct
    850     ##]
    851 ##| #_; #E; nwhd in E:(?%?);
    852     ninversion E;
    853     ##[ ##1,5: #tr1 e1 m1 E1 E2; ndestruct
    854     ##| ##2,6: #tr s1 e1 e2 H E1 E2; ndestruct
    855     ##| ##3,7: #E1 E2; ndestruct
    856     ##| ##4,8: #o1 k1 i1 e1 H1 E1 E2; ndestruct
    857     ##]
    858 ##] nqed.
    859 
    860 nlet corec reactive_traceinf' ge s e
    861   (EXEC:exec_from ge s e)
    862   (REACTIVE: ∀tr,s1,e1.
    863     execution_isteps tr s e s1 e1 →
    864     Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    865   : traceinf' ≝ ?.
    866 nlapply (REACTIVE E0 s e (isteps_none …));
    867 *; #x; ncases x; #tr; #y; ncases y; #s' e'; *; #STEPS H;
    868 @ tr ? H;
    869 napply (reactive_traceinf' ge s' e' ?);
    870 ##[ ncases (several_steps … STEPS EXEC); #_; //
    871 ##| #tr1 s1 e1 STEPS1;
    872     napply REACTIVE;
    873     ##[ ##2:
    874         napply (isteps_trans … STEPS STEPS1);
    875     ##| ##skip
    876     ##]
    877 ##]
    878 nqed.
    879 
    880 (* A slightly different version of the above, to work around a problem with the
    881    next result. *)
    882 nlet corec reactive_traceinf'' ge s e
    883   (EXEC:exec_from ge s e)
    884   (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    885   (REACTIVE: ∀tr,s1,e1.
    886     execution_isteps tr s e s1 e1 →
    887     Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    888   : traceinf' ≝ ?.
    889 ncases REACTIVE0; #x; ncases x; #tr; #y; ncases y; #s' e'; *; #STEPS H;
    890 @ tr ? H;
    891 napply (reactive_traceinf'' ge s' e' ?);
    892 ##[ ncases (several_steps … STEPS EXEC); #_; //
    893 ##| napply (REACTIVE … STEPS);
    894 ##| #tr1 s1 e1 STEPS1;
    895     napply REACTIVE;
    896     ##[ ##2:
    897         napply (isteps_trans … STEPS STEPS1);
    898     ##| ##skip
    899     ##]
    900 ##] nqed.
    901 
    902 (* We want to prove
    903 
    904 nlemma show_reactive : ∀ge,s.
    905   ∀REACTIVE:∀tr,s1,e1.
    906     execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
    907     Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
    908   execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)).
    909  
    910 but the current matita won't unfold reactive_traceinf' so that we can do case
    911 analysis on (REACTIVE …).  Instead we take an "applied" version of REACTIVE that
    912 we can do case analysis on, then get it into the desired form afterwards.
    913 *)
    914 nlet corec show_reactive' ge s e
    915   (EXEC:exec_from ge s e)
    916   (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    917   (REACTIVE: ∀tr1,s1,e1.
    918     execution_isteps tr1 s e s1 e1 →
    919     Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
    920   : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?.
    921 (*nrewrite > (unroll_traceinf' (reactive_traceinf'' …));*)
    922 napply (match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ]);
    923 ncases REACTIVE0;
    924 #x; ncases x; #tr1; #y; ncases y; #s1 e1; #z; ncases z; #STEPS NOTSILENT;
    925 nwhd in ⊢ (?(?%)??);
    926 (*nrewrite > (traceinf_traceinfp_app …);*)
    927 napply (match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ]);
    928 napply (reacting … STEPS NOTSILENT);
    929 napply show_reactive';
    930 nqed.
    931 
    932 nlemma show_reactive : ∀ge,s,e.
    933   ∀EXEC:exec_from ge s e.
    934   ∀REACTIVE:∀tr,s1,e1.
    935     execution_isteps tr s e s1 e1 →
    936     Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
    937   execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC ? REACTIVE)) s e.
    938 ##[ #ge s e EXEC REACTIVE;
    939     napply show_reactive';
    940 ##| napply (REACTIVE … (isteps_none …));
    941 ##] nqed.
    942 
    943 nlemma execution_characterisation_complete:
    944   ∀classic:(∀P:Prop.P ∨ ¬P).
    945   ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
    946    ∀ge,s,e.
    947    exec_from ge s e →
    948    execution_characterisation s (se_step E0 s e).
    949 #classic constructive_indefinite_description ge s e EXEC;
    950 ncases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
    951                  execution_not_over e1));
    952 ##[ #NONTERMINATING;
    953     ncases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧
    954                      ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0));
    955   ##[ *; #tr; *; #s1; *; #e1; *; #INITIAL UNREACTIVE;
    956       napply (ec_diverges … s ? tr);
    957       napply (diverges_diverging … INITIAL);
    958       napply (show_divergence s1 e1);
    959       ##[ #tr2 s2 e2 S; napply (NONTERMINATING (Eapp tr tr2) s2 e2);
    960           napply (isteps_trans … INITIAL S);
    961       ##| #tr2 s2 e2 S; napply (UNREACTIVE … S);
    962       ##| #tr2 s2 o k i e2 STEPS;
    963           nlapply (NONTERMINATING (Eapp tr tr2) s2 (se_interact o k i e2) ?);
    964           ##[ napply (isteps_trans … INITIAL STEPS) ##]
    965           #NOTOVER; ninversion NOTOVER;
    966           ##[ #tr' s' e' E; ndestruct (E);
    967           ##| #o' k' tr' s' e' i' E; ndestruct (E);
    968               @ tr'; @s'; @e'; @;//;
    969               ncases (several_steps … INITIAL EXEC); #_; #EXEC1;
    970               ncases (several_steps … STEPS EXEC1); #_; #EXEC2;
    971               napply (interaction_is_not_silent … EXEC2);
    972           ##]
    973       ##]
    974 
    975   ##| *; #NOTUNREACTIVE;
    976       ncut (∀tr,s1,e1.execution_isteps tr s e s1 e1 →
    977             ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0);
    978       ##[ #tr s1 e1 STEPS;
    979           napply (classical_doubleneg classic); @; #NOREACTION;
    980           napply NOTUNREACTIVE;
    981           @ tr; @s1; @e1; @; //;
    982           #tr2 s2 e2 STEPS2;
    983           nlapply (not_ex_all_not … NOREACTION); #NR1;
    984           nlapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2;
    985           napply (classical_doubleneg classic);
    986           napply NR2; //;
    987       ##| #REACTIVE;
    988           napply ec_reacts;
    989           ##[ ##2: napply reacts;
    990                    napply (show_reactive ge s … EXEC);
    991                    #tr s1 e1 STEPS;
    992                    napply constructive_indefinite_description;
    993                    napply (REACTIVE … tr s1 e1 STEPS);
    994           ##| ##skip
    995           ##]
    996       ##]
    997   ##]
    998  
    999 ##| #NOTNONTERMINATING; nlapply (classical_not_all_ex_not classic … NOTNONTERMINATING);
    1000     *; #tr NNT2; nlapply (classical_not_all_ex_not classic … NNT2);
    1001     *; #s' NNT3; nlapply (classical_not_all_ex_not classic … NNT3);
    1002     *; #e NNT4; nelim (imply_to_and classic … NNT4);
    1003     ncases e;
    1004     ##[ #tr' r m; #STEPS NOSTEP;
    1005         napply (ec_terminates s r m ? (Eapp tr tr')); @;
    1006         ##[ napply s'
    1007         ##| napply STEPS
    1008         ##]
    1009     ##| #tr' s'' e' STEPS; *; #NOSTEP; napply False_rect_Type0;
    1010         napply NOSTEP; //
    1011     ##| #STEPS NOSTEP;
    1012         napply (ec_wrong ? s s' tr); @; //;
    1013     (* The following is stupidly complicated when most of the cases are impossible.
    1014        It ought to be simplified. *)
    1015     ##| #o k i e' STEPS NOSTEP;
    1016         ncases e' in STEPS NOSTEP;
    1017         ##[ #tr' r m STEPS NOSTEP;
    1018             napply (ec_terminates s ???);
    1019            ##[ ##4: napply (annoying_corner_case_terminates … STEPS); ##]
    1020         ##| #tr1 s1 e1 STEPS; *; #NOSTEP;
    1021             napply False_ind; napply NOSTEP; //
    1022         ##| #STEPS NOSTEP;
    1023             nlapply (exec_step_interaction ge s');
    1024             ncases (several_steps … STEPS EXEC); #_;
    1025             nwhd in ⊢ (% → ?);
    1026             nrewrite > (exec_inf_aux_unfold …);
    1027             ncases (exec_step ge s');
    1028             ##[ #o1 k1 EXEC' H; nwhd in EXEC':(?%?) H;
    1029                 ncases (se_inv … EXEC'); *; #E1 E2 H2; ndestruct (E1 E2);
    1030                 ncases (H i); #tr1; *; #s1; *; #K E; nrewrite > K in H2;
    1031                 nrewrite > (exec_inf_aux_unfold …);
    1032                 nwhd in ⊢ (?%? → ?); ncases (is_final_state s1);
    1033                 #F S; nwhd in S:(?%?); ncases (se_inv … S);
    1034             ##| #x; ncases x; #tr' s'; nwhd in ⊢ (?%? → ?);
    1035                 ncases (is_final_state s'); #F S; nwhd in S:(?%?);
    1036                 ncases (se_inv … S);
    1037             ##| #S; ncases (se_inv … S);
    1038             ##]
    1039         ##| #o1 k1 i1 e1 STEPS NOSTEP;
    1040             nlapply (exec_step_interaction ge s');
    1041             ncases (several_steps … STEPS EXEC); #_;
    1042             nwhd in ⊢ (% → ?);
    1043             nrewrite > (exec_inf_aux_unfold …);
    1044             ncases (exec_step ge s');
    1045             ##[ #o1 k1 EXEC' H; nwhd in EXEC':(?%?) H;
    1046                 ncases (se_inv … EXEC'); *; #E1 E2 H2; ndestruct (E1 E2);
    1047                 ncases (H i); #tr1; *; #s1; *; #K E; nrewrite > K in H2;
    1048                 nrewrite > (exec_inf_aux_unfold …);
    1049                 nwhd in ⊢ (?%? → ?); ncases (is_final_state s1);
    1050                 #F S; nwhd in S:(?%?); ncases (se_inv … S);
    1051             ##| #x; ncases x; #tr' s'; nwhd in ⊢ (?%? → ?);
    1052                 ncases (is_final_state s'); #F S; nwhd in S:(?%?);
    1053                 ncases (se_inv … S);
    1054             ##| #S; ncases (se_inv … S);
    1055             ##]
    1056         ##]
    1057     ##]
    1058 ##]
    1059 nqed.   
    1060 
    1061 ninductive execution_matches_behavior: s_execution → program_behavior → Prop ≝
    1062 | emb_terminates: ∀s,e,tr,r,m.
    1063     execution_terminates tr s e r m →
    1064     execution_matches_behavior e (Terminates tr r)
    1065 | emb_diverges: ∀s,e,tr.
    1066     execution_diverges tr s e →
    1067     execution_matches_behavior e (Diverges tr)
    1068 | emb_reacts: ∀s,e,tr.
    1069     execution_reacts tr s e →
    1070     execution_matches_behavior e (Reacts tr)
    1071 | emb_wrong: ∀e,s,s',tr.
    1072     execution_goes_wrong tr s e s' →
    1073     execution_matches_behavior e (Goes_wrong tr)
    1074 | emb_initially_wrong:
    1075     execution_matches_behavior se_wrong (Goes_wrong E0).
    1076 
    1077 nlemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
    1078   execution_terminates tr s (se_step tr' s' e) r m → s = s'.
    1079 #tr tr' s s' e r m H; ninversion H;
    1080 ##[ #s1 s2 tr1 tr2 r' e' m' H' E1 E2 E3 E4 E5; ndestruct; napply refl
    1081 ##| #s1 s2 tr1 tr2 r' e' m' o k i H' E1 E2 E3 E4 E5; ndestruct; napply refl
    1082 ##] nqed.
    1083 
    1084 nlemma exec_state_diverges: ∀tr,tr',s,s',e.
    1085   execution_diverges tr s (se_step tr' s' e) → s = s'.
    1086 #tr tr' s s' e H; ninversion H;
    1087 #tr1 s1 s2 e1 e2 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
    1088 
    1089 nlemma exec_state_reacts: ∀tr,tr',s,s',e.
    1090   execution_reacts tr s (se_step tr' s' e) → s = s'.
    1091 #tr tr' s s' e H; ninversion H;
    1092 #tr1 s1 e1 H' E1 E2 E3; ndestruct; napply refl; nqed.
    1093 
    1094 nlemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
    1095   execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'.
    1096 #tr tr' s s' s'' e H; ninversion H;
    1097 #tr1 s1 s2 e1 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
    1098 
    1099 nlemma behavior_of_execution: ∀s,e.
    1100   execution_characterisation s e →
    1101   ∃b:program_behavior. execution_matches_behavior e b.
    1102 #s0 e0 exec;
    1103 ncases exec;
    1104 ##[ #s r m e tr TERM;
    1105     @ (Terminates tr r);
    1106     napply (emb_terminates … TERM);
    1107 ##| #s e tr DIV;
    1108     @ (Diverges tr);
    1109     napply (emb_diverges … DIV);
    1110 ##| #s e tr REACTS;
    1111     @ (Reacts tr);
    1112     napply (emb_reacts … REACTS);
    1113 ##| #e s s' tr WRONG;
    1114     @ (Goes_wrong tr);
    1115     napply (emb_wrong … WRONG);
    1116 ##] nqed.
    1117 
    1118 nlemma initial_state_not_final: ∀ge,s.
    1119   initial_state ge s →
    1120   ¬ ∃r.final_state s r.
    1121 #ge s H; ncases H;
    1122 #b f E1 E2; @; *; #r H2;
    1123 ninversion H2;
    1124 #r' m E3 E4; ndestruct (E3);
    1125 nqed.
    1126 
    1127 nlemma initial_step: ∀ge,s,e.
    1128   exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
    1129   ¬(∃r.final_state s r) →
    1130   ∃e'.e = e_step E0 s e'.
    1131 #ge s e; nrewrite > (exec_inf_aux_unfold …);
    1132 nwhd in ⊢ (??%? → ?); ncases (is_final_state s);
    1133 ##[ #FINAL EXEC NOTFINAL;
    1134     napply False_ind; napply (absurd ?? NOTFINAL);
    1135     ncases FINAL;
    1136     #r F; @r; napply F;
    1137 ##| #F1 EXEC F2; nwhd in EXEC:(??%?); @; ##[ ##2: nrewrite < EXEC; napply refl ##]
    1138 nqed.
    1139 
    1140 ntheorem exec_inf_equivalence:
    1141   ∀classic:(∀P:Prop.P ∨ ¬P).
    1142   ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
    1143   ∀p,e. single_exec_of (exec_inf p) e →
    1144    ∃b.execution_matches_behavior e b ∧ exec_program p b.
    1145 #classic constructive_indefinite_description p e;
    1146 nwhd in ⊢ (?%? → ??(λ_.?(?%?)%)); nletin ge ≝ (globalenv Genv fundef type p);
    1147 nlapply (make_initial_state_sound p);
    1148 nlapply (the_initial_state p);
    1149 ncases (make_initial_state p);
    1150 ##[ #s INITIAL' INITIAL; nwhd in INITIAL ⊢ (?(??%)? → ?);
    1151     nrewrite > (exec_inf_aux_unfold …);
    1152     nwhd in ⊢ (?%? → ?);
    1153     ncases (is_final_state s);
    1154     ##[ #F; napply False_ind;
    1155         napply (absurd ?? (initial_state_not_final … INITIAL));
    1156         ncases F; #r F'; @r; napply F';
    1157     ##| #NOTFINAL; nwhd in ⊢ (?%? → ?); ncases e;
    1158         ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##]
    1159         ncases (se_inv … EXEC0); *; #E1 E2; nrewrite < E1; nrewrite < E2; #EXEC';
    1160     nlapply (behavior_of_execution ??
    1161               (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
    1162         *; #b MATCHES; @b; @; //;
    1163         ninversion MATCHES;
    1164         ##[ #s0 e1 tr1 r m TERM EXEC BEHAVES; nrewrite < EXEC in TERM;
    1165             #TERM;
    1166             nlapply (exec_state_terminates … TERM); #E1;
    1167             nrewrite > E1 in TERM; #TERM;
    1168             napply (program_terminates (mk_transrel … step) ?? ge s);
    1169             ##[ ##2: napply INITIAL
    1170             ##| ##3: napply (terminates_sound … TERM EXEC');
    1171             ##| ##skip
    1172             ##| //;
    1173             ##]
    1174         ##| #s0 e tr DIVERGES EXEC E2; nrewrite < EXEC in DIVERGES; #DIVERGES;
    1175             nlapply (exec_state_diverges … DIVERGES);
    1176             #E1; nrewrite > E1 in DIVERGES; #DIVERGES;
    1177             ninversion DIVERGES; #tr' s1 s2 e1 e2 INITSTEPS DIVERGING E4 E5 E6;
    1178             nrewrite < E4 in INITSTEPS ⊢ %; nrewrite < E5 in E6 ⊢ %; #E6 INITSTEPS;
    1179             ncut (e0 = e1); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
    1180             #E7; nrewrite < E7 in INITSTEPS; #INITSTEPS;
    1181             ncases (several_steps … INITSTEPS EXEC'); #INITSTAR EXECDIV;
    1182             napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL INITSTAR);
    1183             napply (silent_sound … DIVERGING EXECDIV);
    1184         ##| #s0 e tr REACTS EXEC E2; nrewrite < EXEC in REACTS; #REACTS;
    1185             nlapply (exec_state_reacts … REACTS);
    1186             #E1; nrewrite > E1 in REACTS; #REACTS;
    1187             ninversion REACTS; #tr' s' e'' REACTING E4 E5;
    1188             nrewrite < E4 in REACTING ⊢ %; nrewrite < E5; #REACTING E6;
    1189             ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
    1190             #E7; nrewrite < E7 in REACTING; #REACTING;
    1191             napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL);
    1192             napply (reacts_sound … REACTING EXEC');
    1193         ##| #e s1 s2 tr WRONG EXEC E2; nrewrite < EXEC in WRONG; #WRONG;
    1194             nlapply (exec_state_wrong … WRONG);
    1195             #E1; nrewrite > E1 in WRONG; #WRONG;
    1196             ninversion WRONG; #tr' s1' s2' e'' GOESWRONG E4 E5 E6 E7;
    1197             nrewrite < E4 in GOESWRONG ⊢ %; nrewrite < E5; nrewrite < E7; #GOESWRONG;
    1198             ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
    1199             #E8; nrewrite < E8 in GOESWRONG; #GOESWRONG;
    1200             nelim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR STOP FINAL;
    1201             napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL STAR STOP);
    1202             #r; @; #F; napply (absurd ?? FINAL); @r; napply F;
    1203         ##| #E; ndestruct (E);
    1204         ##]
    1205    ##]
    1206 ##| nwhd in ⊢ ((∀_.? → %) → ?);
    1207     #NOINIT; #_; #EXEC;
    1208     @ (Goes_wrong E0); @;
    1209     ##[ nwhd in EXEC:(?(??%)?);
    1210         nrewrite > (exec_inf_aux_unfold …) in EXEC; nwhd in ⊢ (?%? → ?);
    1211         ncases e;
    1212         ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##]
    1213         ncases (se_inv … EXEC0);
    1214         napply emb_initially_wrong;
    1215     ##| napply program_goes_initially_wrong;
    1216         #s; @; napply NOINIT;
    1217     ##]
    1218 ##] nqed.
    1219 
  • C-semantics/CexecEquiv.ma

    r398 r399  
    1 include "CexecIO.ma".
     1include "CexecComplete.ma".
     2include "CexecSound.ma".
    23include "extralib.ma".
     4
     5include "Plogic/jmeq.ma".
     6include "Plogic/connectives.ma".
    37
    48(* A "single execution" - where all of the input values are made explicit. *)
     
    333337    ##]
    334338nqed.
     339
     340nlemma exec_from_wrong: ∀ge,s.
     341  exec_from ge s se_wrong →
     342  exec_step ge s = Wrong ???.
     343#ge s H; nwhd in H;
     344ninversion H;
     345##[ #tr r m EXEC E; ndestruct (E)
     346##| #tr s' e e' H EXEC E; ndestruct (E)
     347##| nrewrite > (exec_inf_aux_unfold …);
     348    ncases (exec_step ge s);
     349  ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
     350  ##| #x; ncases x; #tr s'; nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
     351      #F EXEC; nwhd in EXEC:(??%?); ndestruct
     352  ##| //
     353  ##]
     354##| #o k i e H EXEC E; ndestruct
     355##] nqed.
     356
     357nlemma exec_from_step_notfinal: ∀ge,s,tr,s',e.
     358  exec_from ge s (se_step tr s' e) →
     359  ¬(∃r. final_state s' r).
     360#ge s tr s' e H; nwhd in H; ninversion H;
     361##[ #tr' r m EXEC E; ndestruct
     362##| #tr' s'' e' e'' H EXEC E; ndestruct (E);
     363    nrewrite > (exec_inf_aux_unfold …) in EXEC;
     364    ncases (exec_step ge s);
     365    ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
     366    ##| #x; ncases x; #tr1 s1; nwhd in ⊢ (??%? → ?); ncases (is_final_state s1);
     367        #F E; nwhd in E:(??%?); ndestruct; napply F;
     368    ##| #E; nwhd in E:(??%?); ndestruct
     369    ##]
     370##| #EXEC E; ndestruct
     371##| #o k i e' H EXEC E; ndestruct
     372##] nqed.
     373
     374nlemma exec_from_interact_step_notfinal: ∀ge,s,o,k,i,tr,s',e.
     375  exec_from ge s (se_interact o k i (se_step tr s' e)) →
     376  ¬(∃r. final_state s' r).
     377#ge s o k i tr s' e H;
     378@; *; #r F; ncases F in H; #r' m H;
     379ninversion H;
     380##[ #tr' r m EXEC E; ndestruct
     381##| #tr' s'' e' e'' H EXEC E; ndestruct (E);
     382##| #EXEC E; ndestruct
     383##| #o' k' i' e' H EXEC E; ndestruct;
     384    nrewrite > (exec_inf_aux_unfold …) in EXEC;
     385    ncases (exec_step ge s);
     386    ##[ #o1 k1 EXEC1; nwhd in EXEC1:(??%?); ndestruct (EXEC1);
     387        ninversion H;
     388        ##[ #tr1 r1 m1 EXECK E; ndestruct (E);
     389        ##| #tr1 s1 e1 e2 H1 EXECK E; ndestruct (E);
     390            nrewrite > (exec_inf_aux_unfold …) in EXECK;
     391            ncases (k1 i');
     392            ##[ #o2 k2 EXECK; nwhd in EXECK:(??%?); ndestruct
     393            ##| #x; ncases x; #tr2 s2; nwhd in ⊢ (??%? → ?);
     394                ncases (is_final_state s2); #F EXECK;
     395                nwhd in EXECK:(??%?); ndestruct;
     396                napply (absurd ?? F);
     397                @ r'; //;
     398            ##| #E; nwhd in E:(??%?); ndestruct
     399            ##]
     400        ##| #EXECK E;  nwhd in E:(??%?); ndestruct
     401        ##| #o2 k2 i2 e2 H2 EXECK E; ndestruct
     402        ##]
     403    ##| #x; ncases x; #tr1 s1; nwhd in ⊢ (??%? → ?);
     404        ncases (is_final_state s1); #F E; nwhd in E:(??%?); ndestruct;
     405    ##| #E; nwhd in E:(??%?); ndestruct
     406    ##]
     407##] nqed.
     408
     409nlemma wrong_sound: ∀ge,tr,s,s',e.
     410  execution_goes_wrong tr s (se_step E0 s e) s' →
     411  exec_from ge s e →
     412  (¬∃r. final_state s r) →
     413  star (mk_transrel … step) ge s tr s' ∧
     414  nostep (mk_transrel … step) ge s' ∧
     415  (¬∃r. final_state s' r).
     416#ge tr0 s0 s0' e0 WRONG; ninversion WRONG;
     417#tr s s' e ESTEPS E1 E2 E3 E4 EXEC NOTFINAL; ndestruct (E1 E2 E3 E4);
     418ncases (several_steps … ESTEPS EXEC);
     419#STAR EXEC'; @;
     420##[ @; ##[ napply STAR;
     421       ##| #badtr bads; @; #badSTEP;
     422           nlapply (step_complete … badSTEP);
     423           nrewrite > (exec_from_wrong … EXEC');
     424           //;
     425       ##]
     426##| @;
     427    nelim ESTEPS in NOTFINAL EXEC ⊢ %;
     428    ##[ #s1 e1 NF EX F; napply (absurd ? F NF);
     429    ##| #e1 e2 tr1 tr2 s1 s2 s3 ESTEPS1 IH NF EXEC;
     430        ncases (exec_from_step … EXEC); #EXEC3 EXEC1;
     431        napply (IH … EXEC1);
     432        napply (exec_from_step_notfinal … EXEC);
     433    ##| #e1 e2 o k i s1 s2 s3 tr1 tr2 ESTEPS1 IH NF EXEC;
     434        napply IH;
     435        ##[ napply (exec_from_interact_step_notfinal … EXEC);
     436        ##| ncases (exec_from_interact … EXEC); //;
     437        ##]
     438    ##]
     439##] nqed.
     440
     441ninductive execution_characterisation : state → s_execution → Prop ≝
     442| ec_terminates: ∀s,r,m,e,tr.
     443    execution_terminates tr s e r m →
     444    execution_characterisation s e
     445| ec_diverges: ∀s,e,tr.
     446    execution_diverges tr s e →
     447    execution_characterisation s e
     448| ec_reacts: ∀s,e,tr.
     449    execution_reacts tr s e →
     450    execution_characterisation s e
     451| ec_wrong: ∀e,s,s',tr.
     452    execution_goes_wrong tr s e s' →
     453    execution_characterisation s e.
     454
     455(* bit of a hack to avoid inability to reduce term in match *)
     456ndefinition interact_prop : ∀A:Type.(∀o:io_out. (io_in o → IO io_out io_in A) → Prop) → IO io_out io_in A → Prop ≝
     457λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ].
     458
     459nlemma err_does_not_interact: ∀A,B,P,e1,e2.
     460  (∀x:B.interact_prop A P (e2 x)) →
     461  interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2).
     462#A B P e1 e2 H;
     463ncases e1; //; nqed.
     464
     465nlemma err2_does_not_interact: ∀A,B,C,P,e1,e2.
     466  (∀x,y.interact_prop A P (e2 x y)) →
     467  interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2).
     468#A B C P e1 e2 H;
     469ncases e1; ##[ #z; ncases z; ##] //; nqed.
     470
     471nlemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2.
     472  (∀x.interact_prop A P (e2 x)) →
     473  interact_prop A P (bindIO ?? (sigma B Q) A (err_to_io_sig ??? Q e1) e2).
     474#A B P Q e1 e2 H;
     475ncases e1; //; nqed.
     476
     477nlemma opt_does_not_interact: ∀A,B,P,e1,e2.
     478  (∀x:B.interact_prop A P (e2 x)) →
     479  interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2).
     480#A B P e1 e2 H;
     481ncases e1; //; nqed.
     482
     483nlemma exec_step_interaction:
     484  ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s).
     485#ge s; ncases s;
     486##[ #f st kk e m; ncases st;
     487  ##[ ##11,14: #a ##| ##2,4,6,7,12,13,15: #a b ##| ##3,5: #a b c ##| ##8: #a b c d ##]
     488  ##[ ##4,6,8,9: napply I ##]
     489  nwhd in ⊢ (???%);
     490  ##[ ncases a; ##[ ncases (fn_return f); //; ##| #e; nwhd nodelta in ⊢ (???%);
     491                    ncases (type_eq_dec (fn_return f) Tvoid); #x; //; napply err2_does_not_interact; // ##]
     492  ##| ncases (find_label a (fn_body f) (call_cont kk)); ##[ napply I ##| #z; ncases z; #x y; napply I ##]
     493  ##| napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5; napply I
     494  ##| ##4,7: napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I
     495  ##| napply err2_does_not_interact; #x1 x2; ncases x1; //;
     496  ##| napply err2_does_not_interact; #x1 x2; napply err2_does_not_interact; #x3 x4; napply opt_does_not_interact; #x5;  napply err_does_not_interact; #x6; ncases a;
     497      ##[ napply I; ##| #x7; napply err2_does_not_interact; #x8 x9; napply I ##]
     498  ##| ncases (is_Sskip a); #H; ##[ napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; napply I
     499      ##| napply I ##]
     500  ##| ncases kk; ##[ ##1,8: ncases (fn_return f); //; ##| ##2,3,5,6,7: //;
     501      ##| #z1 z2 z3; napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I ##]
     502  ##| ncases kk; //;
     503  ##| ncases kk; ##[ ##4: #z1 z2 z3;  napply err2_does_not_interact; #x1 x2; napply err_does_not_interact; #x3; ncases x3; napply I
     504      ##| ##*: // ##]
     505  ##]
     506##| #f args kk m; ncases f;
     507  ##[ #f'; nwhd in ⊢ (???%); ncases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'));
     508      #x; ncases x; ##[ *; ##| #z; ncases z; #x1 x2 H;
     509                        napply err_sig_does_not_interact; //; ##]
     510  (* This is the only case that actually matters! *)
     511  ##| #fn argtys rty; nwhd in ⊢ (???%);
     512      napply  err_sig_does_not_interact; #x1;
     513      nwhd; #i; @; ##[ ##2: @; ##[ ##2: @; ##[ @; nwhd in ⊢ (??%?); napply refl;
     514        ##| @; #E; nwhd in E:(??%%); ndestruct (E); ##] ##] ##]
     515  ##]
     516##| #v kk m; nwhd in ⊢ (???%); ncases kk;
     517    ##[ ##8: #x1 x2 x3 x4; ncases x1;
     518      ##[ nwhd in ⊢ (???%); ncases v; // ##| #x5; nwhd in ⊢ (???%); ncases x5;
     519          #x6 x7; napply opt_does_not_interact; // ##]
     520    ##| ##*: // ##]
     521##] nqed.
     522
     523
     524(* Some classical logic (roughly like a fragment of Coq's library) *)
     525nlemma classical_doubleneg:
     526  ∀classic:(∀P:Prop.P ∨ ¬P).
     527  ∀P:Prop. ¬ (¬ P) → P.
     528#classic P; *; #H;
     529ncases (classic P);
     530##[ // ##| #H'; napply False_ind; /2/; ##]
     531nqed.
     532
     533nlemma classical_not_all_not_ex:
     534  ∀classic:(∀P:Prop.P ∨ ¬P).
     535  ∀A:Type.∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x.
     536#classic A P; *; #H;
     537napply (classical_doubleneg classic); @; *; #H';
     538napply H; #x; @; #H''; napply H'; @x; napply H'';
     539nqed.
     540
     541nlemma classical_not_all_ex_not:
     542  ∀classic:(∀P:Prop.P ∨ ¬P).
     543  ∀A:Type.∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x.
     544#classic A P; *; #H;
     545napply (classical_not_all_not_ex classic A (λx.¬ P x));
     546@; #H'; napply H; #x; napply (classical_doubleneg classic);
     547napply H';
     548nqed.
     549
     550nlemma not_ex_all_not:
     551  ∀A:Type.∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x.
     552#A P; *; #H x; @; #H';
     553napply H; @ x; napply H';
     554nqed.
     555
     556nlemma not_imply_elim:
     557  ∀classic:(∀P:Prop.P ∨ ¬P).
     558  ∀P,Q:Prop. ¬ (P → Q) → P.
     559#classic P Q; *; #H;
     560napply (classical_doubleneg classic); @; *; #H';
     561napply H; #H''; napply False_ind; napply H'; napply H'';
     562nqed.
     563
     564nlemma not_imply_elim2:
     565  ∀P,Q:Prop. ¬ (P → Q) → ¬ Q.
     566#P Q; *; #H; @; #H';
     567napply H; #_; napply H';
     568nqed.
     569
     570nlemma imply_to_and:
     571  ∀classic:(∀P:Prop.P ∨ ¬P).
     572  ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q.
     573#classic P Q H; @;
     574##[ napply (not_imply_elim classic P Q H);
     575##| napply (not_imply_elim2 P Q H);
     576##] nqed.
     577
     578nlemma not_and_to_imply:
     579  ∀classic:(∀P:Prop.P ∨ ¬P).
     580  ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q.
     581#classic P Q; *; #H H';
     582@; #H''; napply H; @; //;
     583nqed.
     584
     585ninductive execution_not_over : s_execution → Prop ≝
     586| eno_step: ∀tr,s,e. execution_not_over (se_step tr s e)
     587| eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)).
     588
     589nlemma eno_stop: ∀tr,r,m. execution_not_over (se_stop tr r m) → False.
     590#tr0 r0 m0 H; ninversion H;
     591##[ #tr s e E; ndestruct
     592##| #o k tr s e i E; ndestruct
     593##] nqed.
     594
     595nlemma eno_wrong: execution_not_over se_wrong → False.
     596#H; ninversion H;
     597##[ #tr s e E; ndestruct
     598##| #o k tr s e i E; ndestruct
     599##] nqed.
     600
     601nlet corec show_divergence s e
     602 (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
     603                 execution_not_over e1)
     604 (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0)
     605 (CONTINUES:∀tr2,s2,o,k,i,e'. execution_isteps tr2 s e s2 (se_interact o k i e') → ∃tr3.∃s3.∃e3. e' = se_step tr3 s3 e3 ∧ tr3 ≠ E0)
     606 : execution_diverging e ≝ ?.
     607nlapply (NONTERMINATING E0 s e ?); //;
     608ncases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %;
     609##[ #tr i m; #_; #_; #_; #ENO; nelim (eno_stop … ENO);
     610##| #tr s' e' UNREACTIVE; nlapply (UNREACTIVE tr s' e' ?);
     611  ##[ nrewrite < (E0_right tr) in ⊢ (?%????);
     612      napply isteps_one; napply isteps_none;
     613  ##| #TR; napply (match sym_eq ??? TR with [ refl ⇒ ? ]); (* nrewrite > TR in UNREACTIVE ⊢ %;*)
     614      #NONTERMINATING CONTINUES; #_; @;
     615      napply (show_divergence s');
     616      ##[ #tr1 s1 e1 S; napply (NONTERMINATING tr1 s1 e1);
     617        nchange in ⊢ (?%????) with (Eapp E0 tr1); napply isteps_one;
     618        napply S;
     619      ##| #tr2 s2 e2 S; nrewrite > TR in UNREACTIVE; #UNREACTIVE; napply (UNREACTIVE tr2 s2 e2);
     620          nchange in ⊢ (?%????) with (Eapp E0 tr2);
     621          napply isteps_one; napply S;
     622      ##| #tr2 s2 o k i e2 S; napply (CONTINUES tr2 s2 o k i);
     623          nchange in ⊢ (?%????) with (Eapp E0 tr2);
     624          napply (isteps_one … S);
     625      ##]
     626  ##]
     627##| #_; #_; #_; #ENO; nelim (eno_wrong … ENO);
     628##| #o k i e' UNREACTIVE NONTERMINATING CONTINUES; #_;
     629    nlapply (CONTINUES E0 s o k i e' (isteps_none …));
     630    *; #tr'; *; #s'; *; #e'; *; #EXEC NOTSILENT;
     631    napply False_ind; napply (absurd ?? NOTSILENT);
     632    napply (UNREACTIVE … s' e');
     633    nrewrite < (E0_right tr') in ⊢ (?%????);
     634    nrewrite > EXEC;
     635    napply isteps_interact; //;
     636##] nqed.
     637
     638nlemma se_inv: ∀e1,e2.
     639  single_exec_of e1 e2 →
     640  match e1 with
     641  [ e_stop tr r m ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ m = m' | _ ⇒ False ]
     642  | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
     643  | e_wrong ⇒ match e2 with [ se_wrong ⇒ True | _ ⇒ False ]
     644  | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ]
     645  ].
     646#e01 e02 H;
     647ncases H;
     648##[ #tr r m; nwhd; @; ##[ @ ##] //
     649##| #tr s e1' e2' H'; nwhd; @; ##[ @ ##] //
     650##| nwhd; //
     651##| #o k i e H'; nwhd; @; ##[ @ ##] //
     652##] nqed.
     653
     654nlemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
     655  exec_from ge s (se_interact o k i (se_step tr s' e)) →
     656  tr ≠ E0.
     657#ge o k i tr s s' e; nwhd in ⊢ (% → ?); nrewrite > (exec_inf_aux_unfold …);
     658nlapply (exec_step_interaction ge s);
     659ncases (exec_step ge s);
     660##[ #o' k' ; nwhd in ⊢ (% → ?%? → ?); #H K; ncases (se_inv … K);
     661    *; #E1 E2 H1; ndestruct (E1);
     662    nlapply (H i); *; #tr'; *; #s''; *; #K' TR;
     663    nrewrite > E2 in H1; #H1; nwhd in H1:(?%?); nrewrite > K' in H1;
     664    nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (?%? → ?);
     665    ncases (is_final_state s'');
     666    ##[ #F; nwhd in ⊢ (?%? → ?); #S;
     667        napply False_ind; napply (absurd ? S); ncases (se_inv … S)
     668    ##| #NF S; nwhd in S:(?%?); ncases (se_inv … S);
     669        *; #E1 E2 S'; nrewrite < E1; napply TR
     670    ##]
     671##| #x; ncases x; #tr' s'' H; nwhd in ⊢ (?%? → ?);
     672    ncases (is_final_state s''); #F E; nwhd in E:(?%?);
     673    ninversion E;
     674    ##[ ##1,5: #tr1 e1 m1 E1 E2; ndestruct
     675    ##| ##2,6: #tr s1 e1 e2 H E1 E2; ndestruct
     676    ##| ##3,7: #E; ndestruct
     677    ##| ##4,8: #o1 k1 i1 e1 H1 E1 E2; ndestruct
     678    ##]
     679##| #_; #E; nwhd in E:(?%?);
     680    ninversion E;
     681    ##[ ##1,5: #tr1 e1 m1 E1 E2; ndestruct
     682    ##| ##2,6: #tr s1 e1 e2 H E1 E2; ndestruct
     683    ##| ##3,7: #E1 E2; ndestruct
     684    ##| ##4,8: #o1 k1 i1 e1 H1 E1 E2; ndestruct
     685    ##]
     686##] nqed.
     687
     688nlet corec reactive_traceinf' ge s e
     689  (EXEC:exec_from ge s e)
     690  (REACTIVE: ∀tr,s1,e1.
     691    execution_isteps tr s e s1 e1 →
     692    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     693  : traceinf' ≝ ?.
     694nlapply (REACTIVE E0 s e (isteps_none …));
     695*; #x; ncases x; #tr; #y; ncases y; #s' e'; *; #STEPS H;
     696@ tr ? H;
     697napply (reactive_traceinf' ge s' e' ?);
     698##[ ncases (several_steps … STEPS EXEC); #_; //
     699##| #tr1 s1 e1 STEPS1;
     700    napply REACTIVE;
     701    ##[ ##2:
     702        napply (isteps_trans … STEPS STEPS1);
     703    ##| ##skip
     704    ##]
     705##]
     706nqed.
     707
     708(* A slightly different version of the above, to work around a problem with the
     709   next result. *)
     710nlet corec reactive_traceinf'' ge s e
     711  (EXEC:exec_from ge s e)
     712  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     713  (REACTIVE: ∀tr,s1,e1.
     714    execution_isteps tr s e s1 e1 →
     715    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     716  : traceinf' ≝ ?.
     717ncases REACTIVE0; #x; ncases x; #tr; #y; ncases y; #s' e'; *; #STEPS H;
     718@ tr ? H;
     719napply (reactive_traceinf'' ge s' e' ?);
     720##[ ncases (several_steps … STEPS EXEC); #_; //
     721##| napply (REACTIVE … STEPS);
     722##| #tr1 s1 e1 STEPS1;
     723    napply REACTIVE;
     724    ##[ ##2:
     725        napply (isteps_trans … STEPS STEPS1);
     726    ##| ##skip
     727    ##]
     728##] nqed.
     729
     730(* We want to prove
     731
     732nlemma show_reactive : ∀ge,s.
     733  ∀REACTIVE:∀tr,s1,e1.
     734    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     735    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
     736  execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)).
     737 
     738but the current matita won't unfold reactive_traceinf' so that we can do case
     739analysis on (REACTIVE …).  Instead we take an "applied" version of REACTIVE that
     740we can do case analysis on, then get it into the desired form afterwards.
     741*)
     742nlet corec show_reactive' ge s e
     743  (EXEC:exec_from ge s e)
     744  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     745  (REACTIVE: ∀tr1,s1,e1.
     746    execution_isteps tr1 s e s1 e1 →
     747    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     748  : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?.
     749(*nrewrite > (unroll_traceinf' (reactive_traceinf'' …));*)
     750napply (match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ]);
     751ncases REACTIVE0;
     752#x; ncases x; #tr1; #y; ncases y; #s1 e1; #z; ncases z; #STEPS NOTSILENT;
     753nwhd in ⊢ (?(?%)??);
     754(*nrewrite > (traceinf_traceinfp_app …);*)
     755napply (match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ]);
     756napply (reacting … STEPS NOTSILENT);
     757napply show_reactive';
     758nqed.
     759
     760nlemma show_reactive : ∀ge,s,e.
     761  ∀EXEC:exec_from ge s e.
     762  ∀REACTIVE:∀tr,s1,e1.
     763    execution_isteps tr s e s1 e1 →
     764    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
     765  execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC ? REACTIVE)) s e.
     766##[ #ge s e EXEC REACTIVE;
     767    napply show_reactive';
     768##| napply (REACTIVE … (isteps_none …));
     769##] nqed.
     770
     771nlemma execution_characterisation_complete:
     772  ∀classic:(∀P:Prop.P ∨ ¬P).
     773  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
     774   ∀ge,s,e.
     775   exec_from ge s e →
     776   execution_characterisation s (se_step E0 s e).
     777#classic constructive_indefinite_description ge s e EXEC;
     778ncases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
     779                 execution_not_over e1));
     780##[ #NONTERMINATING;
     781    ncases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧
     782                     ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0));
     783  ##[ *; #tr; *; #s1; *; #e1; *; #INITIAL UNREACTIVE;
     784      napply (ec_diverges … s ? tr);
     785      napply (diverges_diverging … INITIAL);
     786      napply (show_divergence s1 e1);
     787      ##[ #tr2 s2 e2 S; napply (NONTERMINATING (Eapp tr tr2) s2 e2);
     788          napply (isteps_trans … INITIAL S);
     789      ##| #tr2 s2 e2 S; napply (UNREACTIVE … S);
     790      ##| #tr2 s2 o k i e2 STEPS;
     791          nlapply (NONTERMINATING (Eapp tr tr2) s2 (se_interact o k i e2) ?);
     792          ##[ napply (isteps_trans … INITIAL STEPS) ##]
     793          #NOTOVER; ninversion NOTOVER;
     794          ##[ #tr' s' e' E; ndestruct (E);
     795          ##| #o' k' tr' s' e' i' E; ndestruct (E);
     796              @ tr'; @s'; @e'; @;//;
     797              ncases (several_steps … INITIAL EXEC); #_; #EXEC1;
     798              ncases (several_steps … STEPS EXEC1); #_; #EXEC2;
     799              napply (interaction_is_not_silent … EXEC2);
     800          ##]
     801      ##]
     802
     803  ##| *; #NOTUNREACTIVE;
     804      ncut (∀tr,s1,e1.execution_isteps tr s e s1 e1 →
     805            ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0);
     806      ##[ #tr s1 e1 STEPS;
     807          napply (classical_doubleneg classic); @; #NOREACTION;
     808          napply NOTUNREACTIVE;
     809          @ tr; @s1; @e1; @; //;
     810          #tr2 s2 e2 STEPS2;
     811          nlapply (not_ex_all_not … NOREACTION); #NR1;
     812          nlapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2;
     813          napply (classical_doubleneg classic);
     814          napply NR2; //;
     815      ##| #REACTIVE;
     816          napply ec_reacts;
     817          ##[ ##2: napply reacts;
     818                   napply (show_reactive ge s … EXEC);
     819                   #tr s1 e1 STEPS;
     820                   napply constructive_indefinite_description;
     821                   napply (REACTIVE … tr s1 e1 STEPS);
     822          ##| ##skip
     823          ##]
     824      ##]
     825  ##]
     826 
     827##| #NOTNONTERMINATING; nlapply (classical_not_all_ex_not classic … NOTNONTERMINATING);
     828    *; #tr NNT2; nlapply (classical_not_all_ex_not classic … NNT2);
     829    *; #s' NNT3; nlapply (classical_not_all_ex_not classic … NNT3);
     830    *; #e NNT4; nelim (imply_to_and classic … NNT4);
     831    ncases e;
     832    ##[ #tr' r m; #STEPS NOSTEP;
     833        napply (ec_terminates s r m ? (Eapp tr tr')); @;
     834        ##[ napply s'
     835        ##| napply STEPS
     836        ##]
     837    ##| #tr' s'' e' STEPS; *; #NOSTEP; napply False_rect_Type0;
     838        napply NOSTEP; //
     839    ##| #STEPS NOSTEP;
     840        napply (ec_wrong ? s s' tr); @; //;
     841    (* The following is stupidly complicated when most of the cases are impossible.
     842       It ought to be simplified. *)
     843    ##| #o k i e' STEPS NOSTEP;
     844        ncases e' in STEPS NOSTEP;
     845        ##[ #tr' r m STEPS NOSTEP;
     846            napply (ec_terminates s ???);
     847           ##[ ##4: napply (annoying_corner_case_terminates … STEPS); ##]
     848        ##| #tr1 s1 e1 STEPS; *; #NOSTEP;
     849            napply False_ind; napply NOSTEP; //
     850        ##| #STEPS NOSTEP;
     851            nlapply (exec_step_interaction ge s');
     852            ncases (several_steps … STEPS EXEC); #_;
     853            nwhd in ⊢ (% → ?);
     854            nrewrite > (exec_inf_aux_unfold …);
     855            ncases (exec_step ge s');
     856            ##[ #o1 k1 EXEC' H; nwhd in EXEC':(?%?) H;
     857                ncases (se_inv … EXEC'); *; #E1 E2 H2; ndestruct (E1 E2);
     858                ncases (H i); #tr1; *; #s1; *; #K E; nrewrite > K in H2;
     859                nrewrite > (exec_inf_aux_unfold …);
     860                nwhd in ⊢ (?%? → ?); ncases (is_final_state s1);
     861                #F S; nwhd in S:(?%?); ncases (se_inv … S);
     862            ##| #x; ncases x; #tr' s'; nwhd in ⊢ (?%? → ?);
     863                ncases (is_final_state s'); #F S; nwhd in S:(?%?);
     864                ncases (se_inv … S);
     865            ##| #S; ncases (se_inv … S);
     866            ##]
     867        ##| #o1 k1 i1 e1 STEPS NOSTEP;
     868            nlapply (exec_step_interaction ge s');
     869            ncases (several_steps … STEPS EXEC); #_;
     870            nwhd in ⊢ (% → ?);
     871            nrewrite > (exec_inf_aux_unfold …);
     872            ncases (exec_step ge s');
     873            ##[ #o1 k1 EXEC' H; nwhd in EXEC':(?%?) H;
     874                ncases (se_inv … EXEC'); *; #E1 E2 H2; ndestruct (E1 E2);
     875                ncases (H i); #tr1; *; #s1; *; #K E; nrewrite > K in H2;
     876                nrewrite > (exec_inf_aux_unfold …);
     877                nwhd in ⊢ (?%? → ?); ncases (is_final_state s1);
     878                #F S; nwhd in S:(?%?); ncases (se_inv … S);
     879            ##| #x; ncases x; #tr' s'; nwhd in ⊢ (?%? → ?);
     880                ncases (is_final_state s'); #F S; nwhd in S:(?%?);
     881                ncases (se_inv … S);
     882            ##| #S; ncases (se_inv … S);
     883            ##]
     884        ##]
     885    ##]
     886##]
     887nqed.   
     888
     889ninductive execution_matches_behavior: s_execution → program_behavior → Prop ≝
     890| emb_terminates: ∀s,e,tr,r,m.
     891    execution_terminates tr s e r m →
     892    execution_matches_behavior e (Terminates tr r)
     893| emb_diverges: ∀s,e,tr.
     894    execution_diverges tr s e →
     895    execution_matches_behavior e (Diverges tr)
     896| emb_reacts: ∀s,e,tr.
     897    execution_reacts tr s e →
     898    execution_matches_behavior e (Reacts tr)
     899| emb_wrong: ∀e,s,s',tr.
     900    execution_goes_wrong tr s e s' →
     901    execution_matches_behavior e (Goes_wrong tr)
     902| emb_initially_wrong:
     903    execution_matches_behavior se_wrong (Goes_wrong E0).
     904
     905nlemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
     906  execution_terminates tr s (se_step tr' s' e) r m → s = s'.
     907#tr tr' s s' e r m H; ninversion H;
     908##[ #s1 s2 tr1 tr2 r' e' m' H' E1 E2 E3 E4 E5; ndestruct; napply refl
     909##| #s1 s2 tr1 tr2 r' e' m' o k i H' E1 E2 E3 E4 E5; ndestruct; napply refl
     910##] nqed.
     911
     912nlemma exec_state_diverges: ∀tr,tr',s,s',e.
     913  execution_diverges tr s (se_step tr' s' e) → s = s'.
     914#tr tr' s s' e H; ninversion H;
     915#tr1 s1 s2 e1 e2 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
     916
     917nlemma exec_state_reacts: ∀tr,tr',s,s',e.
     918  execution_reacts tr s (se_step tr' s' e) → s = s'.
     919#tr tr' s s' e H; ninversion H;
     920#tr1 s1 e1 H' E1 E2 E3; ndestruct; napply refl; nqed.
     921
     922nlemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
     923  execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'.
     924#tr tr' s s' s'' e H; ninversion H;
     925#tr1 s1 s2 e1 H' E1 E2 E3 E4; ndestruct; napply refl; nqed.
     926
     927nlemma behavior_of_execution: ∀s,e.
     928  execution_characterisation s e →
     929  ∃b:program_behavior. execution_matches_behavior e b.
     930#s0 e0 exec;
     931ncases exec;
     932##[ #s r m e tr TERM;
     933    @ (Terminates tr r);
     934    napply (emb_terminates … TERM);
     935##| #s e tr DIV;
     936    @ (Diverges tr);
     937    napply (emb_diverges … DIV);
     938##| #s e tr REACTS;
     939    @ (Reacts tr);
     940    napply (emb_reacts … REACTS);
     941##| #e s s' tr WRONG;
     942    @ (Goes_wrong tr);
     943    napply (emb_wrong … WRONG);
     944##] nqed.
     945
     946nlemma initial_state_not_final: ∀ge,s.
     947  initial_state ge s →
     948  ¬ ∃r.final_state s r.
     949#ge s H; ncases H;
     950#b f E1 E2; @; *; #r H2;
     951ninversion H2;
     952#r' m E3 E4; ndestruct (E3);
     953nqed.
     954
     955nlemma initial_step: ∀ge,s,e.
     956  exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
     957  ¬(∃r.final_state s r) →
     958  ∃e'.e = e_step E0 s e'.
     959#ge s e; nrewrite > (exec_inf_aux_unfold …);
     960nwhd in ⊢ (??%? → ?); ncases (is_final_state s);
     961##[ #FINAL EXEC NOTFINAL;
     962    napply False_ind; napply (absurd ?? NOTFINAL);
     963    ncases FINAL;
     964    #r F; @r; napply F;
     965##| #F1 EXEC F2; nwhd in EXEC:(??%?); @; ##[ ##2: nrewrite < EXEC; napply refl ##]
     966nqed.
     967
     968ntheorem exec_inf_equivalence:
     969  ∀classic:(∀P:Prop.P ∨ ¬P).
     970  ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
     971  ∀p,e. single_exec_of (exec_inf p) e →
     972   ∃b.execution_matches_behavior e b ∧ exec_program p b.
     973#classic constructive_indefinite_description p e;
     974nwhd in ⊢ (?%? → ??(λ_.?(?%?)%)); nletin ge ≝ (globalenv Genv fundef type p);
     975nlapply (make_initial_state_sound p);
     976nlapply (the_initial_state p);
     977ncases (make_initial_state p);
     978##[ #s INITIAL' INITIAL; nwhd in INITIAL ⊢ (?(??%)? → ?);
     979    nrewrite > (exec_inf_aux_unfold …);
     980    nwhd in ⊢ (?%? → ?);
     981    ncases (is_final_state s);
     982    ##[ #F; napply False_ind;
     983        napply (absurd ?? (initial_state_not_final … INITIAL));
     984        ncases F; #r F'; @r; napply F';
     985    ##| #NOTFINAL; nwhd in ⊢ (?%? → ?); ncases e;
     986        ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##]
     987        ncases (se_inv … EXEC0); *; #E1 E2; nrewrite < E1; nrewrite < E2; #EXEC';
     988    nlapply (behavior_of_execution ??
     989              (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
     990        *; #b MATCHES; @b; @; //;
     991        ninversion MATCHES;
     992        ##[ #s0 e1 tr1 r m TERM EXEC BEHAVES; nrewrite < EXEC in TERM;
     993            #TERM;
     994            nlapply (exec_state_terminates … TERM); #E1;
     995            nrewrite > E1 in TERM; #TERM;
     996            napply (program_terminates (mk_transrel … step) ?? ge s);
     997            ##[ ##2: napply INITIAL
     998            ##| ##3: napply (terminates_sound … TERM EXEC');
     999            ##| ##skip
     1000            ##| //;
     1001            ##]
     1002        ##| #s0 e tr DIVERGES EXEC E2; nrewrite < EXEC in DIVERGES; #DIVERGES;
     1003            nlapply (exec_state_diverges … DIVERGES);
     1004            #E1; nrewrite > E1 in DIVERGES; #DIVERGES;
     1005            ninversion DIVERGES; #tr' s1 s2 e1 e2 INITSTEPS DIVERGING E4 E5 E6;
     1006            nrewrite < E4 in INITSTEPS ⊢ %; nrewrite < E5 in E6 ⊢ %; #E6 INITSTEPS;
     1007            ncut (e0 = e1); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
     1008            #E7; nrewrite < E7 in INITSTEPS; #INITSTEPS;
     1009            ncases (several_steps … INITSTEPS EXEC'); #INITSTAR EXECDIV;
     1010            napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL INITSTAR);
     1011            napply (silent_sound … DIVERGING EXECDIV);
     1012        ##| #s0 e tr REACTS EXEC E2; nrewrite < EXEC in REACTS; #REACTS;
     1013            nlapply (exec_state_reacts … REACTS);
     1014            #E1; nrewrite > E1 in REACTS; #REACTS;
     1015            ninversion REACTS; #tr' s' e'' REACTING E4 E5;
     1016            nrewrite < E4 in REACTING ⊢ %; nrewrite < E5; #REACTING E6;
     1017            ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
     1018            #E7; nrewrite < E7 in REACTING; #REACTING;
     1019            napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL);
     1020            napply (reacts_sound … REACTING EXEC');
     1021        ##| #e s1 s2 tr WRONG EXEC E2; nrewrite < EXEC in WRONG; #WRONG;
     1022            nlapply (exec_state_wrong … WRONG);
     1023            #E1; nrewrite > E1 in WRONG; #WRONG;
     1024            ninversion WRONG; #tr' s1' s2' e'' GOESWRONG E4 E5 E6 E7;
     1025            nrewrite < E4 in GOESWRONG ⊢ %; nrewrite < E5; nrewrite < E7; #GOESWRONG;
     1026            ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
     1027            #E8; nrewrite < E8 in GOESWRONG; #GOESWRONG;
     1028            nelim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR STOP FINAL;
     1029            napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL STAR STOP);
     1030            #r; @; #F; napply (absurd ?? FINAL); @r; napply F;
     1031        ##| #E; ndestruct (E);
     1032        ##]
     1033   ##]
     1034##| nwhd in ⊢ ((∀_.? → %) → ?);
     1035    #NOINIT; #_; #EXEC;
     1036    @ (Goes_wrong E0); @;
     1037    ##[ nwhd in EXEC:(?(??%)?);
     1038        nrewrite > (exec_inf_aux_unfold …) in EXEC; nwhd in ⊢ (?%? → ?);
     1039        ncases e;
     1040        ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##]
     1041        ncases (se_inv … EXEC0);
     1042        napply emb_initially_wrong;
     1043    ##| napply program_goes_initially_wrong;
     1044        #s; @; napply NOINIT;
     1045    ##]
     1046##] nqed.
     1047
Note: See TracChangeset for help on using the changeset viewer.