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

Rearrange executable semantics a little.

File:
1 moved

Legend:

Unmodified
Added
Removed
  • 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 
Note: See TracChangeset for help on using the changeset viewer.