Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (9 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/CexecEquiv.ma

    r485 r487  
    33include "extralib.ma".
    44
    5 include "Plogic/jmeq.ma".
    6 include "Plogic/connectives.ma".
     5include "basics/jmeq.ma".
    76
    87(* A "single execution" - where all of the input values are made explicit. *)
    9 ncoinductive s_execution : Type
     8coinductive s_execution : Type[0]
    109| se_stop : trace → int → mem → s_execution
    1110| se_step : trace → state → s_execution → s_execution
     
    1312| se_interact : ∀o:io_out. (io_in o → execution) → io_in o → s_execution → s_execution.
    1413
    15 ncoinductive single_exec_of : execution → s_execution → Prop ≝
     14coinductive single_exec_of : execution → s_execution → Prop ≝
    1615| seo_stop : ∀tr,r,m. single_exec_of (e_stop tr r m) (se_stop tr r m)
    1716| seo_step : ∀tr,s,e,se.
     
    2524(* starting after state s, zero or more steps of execution e reach state s'
    2625   after which comes e'. *)
    27 ninductive execution_isteps : trace → state → s_execution → state → s_execution → Prop ≝
     26inductive execution_isteps : trace → state → s_execution → state → s_execution → Prop ≝
    2827| isteps_none : ∀s,e. execution_isteps E0 s e s e
    2928| isteps_one : ∀e,e',tr,tr',s,s',s0.
     
    3433    execution_isteps (tr⧺tr') s0 (se_interact o k i (se_step tr s e)) s' e'.
    3534
    36 nlemma isteps_trans: ∀tr1,tr2,s1,s2,s3,e1,e2,e3.
     35lemma isteps_trans: ∀tr1,tr2,s1,s2,s3,e1,e2,e3.
    3736  execution_isteps tr1 s1 e1 s2 e2 →
    3837  execution_isteps tr2 s2 e2 s3 e3 →
    3938  execution_isteps (tr1⧺tr2) s1 e1 s3 e3.
    40 #tr1 tr2 s1 s2 s3 e1 e2 e3 H1; nelim H1;
    41 ##[ #s e; //;
    42 ##| #e e' tr tr' s1' s2' s3' H1 H2 H3;
    43     nrewrite > (Eapp_assoc …);
    44     napply isteps_one;
    45     napply H2; napply H3;
    46 ##| #e e' o k i s1' s2' s3' tr tr' H1 H2 H3;
    47     nrewrite > (Eapp_assoc …);
    48     napply isteps_interact;
     39#tr1 #tr2 #s1 #s2 #s3 #e1 #e2 #e3 #H1 elim H1;
     40[ #s #e //;
     41| #e #e' #tr #tr' #s1' #s2' #s3' #H1 #H2 #H3
     42    >(Eapp_assoc …)
     43    @isteps_one
     44    @H2 @H3
     45| #e #e' #o #k #i #s1' #s2' #s3' #tr #tr' #H1 #H2 #H3
     46    >(Eapp_assoc …)
     47    @isteps_interact
    4948    /2/
    50 ##] nqed.
    51 
    52 nlemma exec_e_step: ∀ge,x,tr,s,e.
     49] qed.
     50
     51lemma exec_e_step: ∀ge,x,tr,s,e.
    5352  exec_inf_aux ge x = e_step tr s e →
    5453  exec_inf_aux ge (exec_step ge s) = e.
    55 #ge x tr s e;
    56 nrewrite > (exec_inf_aux_unfold …); ncases x;
    57 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
    58 ##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
    59     ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    60     napply refl;
    61 ##| #EXEC; nwhd in EXEC:(??%?); ndestruct
    62 ##] nqed.
    63 
    64 nlemma exec_e_step_inv: ∀ge,x,tr,s,e.
     54#ge #x #tr #s #e
     55>(exec_inf_aux_unfold …) cases x;
     56[ #o #k #EXEC whd in EXEC:(??%?); destruct
     57| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
     58    cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct;
     59    @refl
     60| #EXEC whd in EXEC:(??%?); destruct
     61] qed.
     62
     63lemma exec_e_step_inv: ∀ge,x,tr,s,e.
    6564  exec_inf_aux ge x = e_step tr s e →
    6665  x = Value ??? 〈tr,s〉.
    67 #ge x tr s e;
    68 nrewrite > (exec_inf_aux_unfold …); ncases x;
    69 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
    70 ##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
    71     ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    72     napply refl;
    73 ##| #EXEC; nwhd in EXEC:(??%?); ndestruct
    74 ##] nqed.
    75 
    76 nlemma exec_e_step_inv2: ∀ge,x,tr,s,e.
     66#ge #x #tr #s #e
     67>(exec_inf_aux_unfold …) cases x;
     68[ #o #k #EXEC whd in EXEC:(??%?); destruct
     69| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
     70    cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct;
     71    @refl
     72| #EXEC whd in EXEC:(??%?); destruct
     73] qed.
     74
     75lemma exec_e_step_inv2: ∀ge,x,tr,s,e.
    7776  exec_inf_aux ge x = e_step tr s e →
    7877  ¬∃r.final_state s r.
    79 #ge x tr s e;
    80 nrewrite > (exec_inf_aux_unfold …); ncases x;
    81 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct
    82 ##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?);
    83     ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
    84     napply FINAL;
    85 ##| #EXEC; nwhd in EXEC:(??%?); ndestruct
    86 ##] nqed.
    87 
    88 ndefinition exec_from : genv → state → s_execution → Prop ≝
     78#ge #x #tr #s #e
     79>(exec_inf_aux_unfold …) cases x;
     80[ #o #k #EXEC whd in EXEC:(??%?); destruct
     81| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
     82    cases (is_final_state s'); #FINAL #EXEC whd in EXEC:(??%?); destruct;
     83    @FINAL
     84| #EXEC whd in EXEC:(??%?); destruct
     85] qed.
     86
     87definition exec_from : genv → state → s_execution → Prop ≝
    8988λge,s,se. single_exec_of (exec_inf_aux ge (exec_step ge s)) se.
    9089
    91 nlemma exec_from_step : ∀ge,s,tr,s',e.
     90lemma exec_from_step : ∀ge,s,tr,s',e.
    9291exec_from ge s (se_step tr s' e) →
    9392exec_step ge s = Value ??? 〈tr,s'〉 ∧ exec_from ge s' e.
    94 #ge s0 tr0 s0' e0 H; ninversion H;
    95 ##[ #tr r m E1 E2; ndestruct
    96 ##| #tr s e se H1 H2 E; ndestruct (E);
    97     nrewrite > (exec_e_step_inv … H2);
    98     nrewrite < (exec_e_step … H2) in H1; #H1; @; //
    99 ##| #_; #E; ndestruct
    100 ##| #o k i se H1 H2 E; ndestruct
    101 ##] nqed.
    102 
    103 nlemma exec_from_interact : ∀ge,s,o,k,i,tr,s',e.
     93#ge #s0 #tr0 #s0' #e0 #H inversion H;
     94[ #tr #r #m #E1 #E2 destruct
     95| #tr #s #e #se #H1 #H2 #E destruct (E);
     96    >(exec_e_step_inv … H2)
     97    <(exec_e_step … H2) in H1 #H1 % //
     98| #_ #E destruct
     99| #o #k #i #se #H1 #H2 #E destruct
     100] qed.
     101
     102lemma exec_from_interact : ∀ge,s,o,k,i,tr,s',e.
    104103exec_from ge s (se_interact o k i (se_step tr s' e)) →
    105104step ge s tr s' ∧
    106105(*exec_step ge s = Value ??? 〈tr,s'〉 ∧*) exec_from ge s' e.
    107 #ge s0 o0 k0 i0 tr0 s0' e0 H; ninversion H;
    108 ##[ #tr r m E1 E2; ndestruct
    109 ##| #tr s e se H1 H2 E; ndestruct (E)
    110 ##| #_; #E; ndestruct
    111 ##| #o k i se H1 H2 E; ndestruct (E);
    112     nlapply (exec_step_sound ge s0);
    113     ncases (exec_step ge s0) in H2 ⊢ %;
    114     ##[ #o' k'; nrewrite > (exec_inf_aux_unfold …);
    115         #E'; nwhd in E':(??%?); ndestruct (E');
    116         #STEP;
    117         ninversion H1;
    118         ##[ #tr r m E1 E2; ndestruct
    119         ##| #tr' s' e' se' H2 H3 E2; ndestruct (E2);
    120             nrewrite < (exec_e_step … H3) in H2; #H2; @; //;
    121             nlapply (STEP i);
    122             nrewrite > (exec_e_step_inv … H3);
    123             #S; napply S;
    124         ##| #_; #E; ndestruct
    125         ##| #o k i se H1 H2 E; ndestruct
    126         ##]
    127     ##| #x; ncases x; #tr' s'; nrewrite > (exec_inf_aux_unfold …);
    128         nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
    129         #F E; nwhd in E:(??%?); ndestruct
    130     ##| nrewrite > (exec_inf_aux_unfold …);
    131         #E'; nwhd in E':(??%?); ndestruct (E');
    132     ##]
    133 ##] nqed.
    134 
    135 nlemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
     106#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
     107[ #tr #r #m #E1 #E2 destruct
     108| #tr #s #e #se #H1 #H2 #E destruct (E)
     109| #_ #E destruct
     110| #o #k #i #se #H1 #H2 #E destruct (E);
     111    lapply (exec_step_sound ge s0);
     112    cases (exec_step ge s0) in H2 ⊢ %;
     113    [ #o' #k' >(exec_inf_aux_unfold …)
     114        #E' whd in E':(??%?); destruct (E');
     115        #STEP
     116        inversion H1;
     117        [ #tr #r #m #E1 #E2 destruct
     118        | #tr' #s' #e' #se' #H2 #H3 #E2 destruct (E2);
     119            <(exec_e_step … H3) in H2 #H2 % //;
     120            lapply (STEP i);
     121            >(exec_e_step_inv … H3)
     122            #S @S
     123        | #_ #E destruct
     124        | #o #k #i #se #H1 #H2 #E destruct
     125        ]
     126    | #x cases x; #tr' #s' >(exec_inf_aux_unfold …)
     127        whd in ⊢ (??%? → ?); cases (is_final_state s');
     128        #F #E whd in E:(??%?); destruct
     129    | >(exec_inf_aux_unfold …)
     130        #E' whd in E':(??%?); destruct (E');
     131    ]
     132] qed.
     133
     134lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
    136135exec_from ge s (se_interact o k i (se_stop tr r m)) →
    137136step ge s tr (Returnstate (Vint r) Kstop m).
    138 #ge s0 o0 k0 i0 tr0 s0' e0 H; ninversion H;
    139 ##[ #tr r m E1 E2; ndestruct
    140 ##| #tr s e se H1 H2 E; ndestruct (E)
    141 ##| #_; #E; ndestruct
    142 ##| #o k i se H1 H2 E; ndestruct (E);
    143     nlapply (exec_step_sound ge s0);
    144     nrewrite > (exec_inf_aux_unfold …) in H2;
    145     ncases (exec_step ge s0);
    146     ##[ #o' k';
    147         #E'; nwhd in E':(??%?); ndestruct (E');
    148         #STEP;
    149         ninversion H1;
    150         ##[ #tr r m E1 E2; nlapply (STEP i); ndestruct;
    151             nrewrite > (exec_inf_aux_unfold …) in E1;
    152             ncases (k' i);
    153             ##[ #o2 k2 E; nwhd in E:(??%?); ndestruct (E)
    154             ##| #x; ncases x; #tr2 s2; nwhd in ⊢ (??%? → ?);
    155                 ncases (is_final_state s2);
    156                 ##[ #F; ncases F; #r' FINAL E; nwhd in E:(??%?);
    157                     ndestruct (E);
    158                     ninversion FINAL;
    159                     #r'' m'' E1 E2; ndestruct (E1 E2); //;
    160                 ##| #NF E; nwhd in E:(??%?); ndestruct (E)
    161                 ##]
    162             ##| #E; nwhd in E:(??%?); ndestruct (E)
    163             ##]
    164        ##| #tr s e e' H EXEC E; ndestruct (E)
    165        ##| #EXEC E; ndestruct (E)
    166        ##| #o2 k2 i2 e2 H EXEC E; ndestruct (E)
    167        ##]
    168    ##| #x; ncases x; #tr s; nwhd in ⊢ (??%? → ?);
    169        ncases (is_final_state s); #F E; nwhd in E:(??%?); ndestruct (E)
    170    ##| #E; nwhd in E:(??%?); ndestruct (E)
    171    ##]
    172 ##] nqed.
     137#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
     138[ #tr #r #m #E1 #E2 destruct
     139| #tr #s #e #se #H1 #H2 #E destruct (E)
     140| #_ #E destruct
     141| #o #k #i #se #H1 #H2 #E destruct (E);
     142    lapply (exec_step_sound ge s0);
     143    >(exec_inf_aux_unfold …) in H2;
     144    cases (exec_step ge s0);
     145    [ #o' #k'
     146        #E' whd in E':(??%?); destruct (E');
     147        #STEP
     148        inversion H1;
     149        [ #tr #r #m #E1 #E2 lapply (STEP i); destruct;
     150            >(exec_inf_aux_unfold …) in E1;
     151            cases (k' i);
     152            [ #o2 #k2 #E whd in E:(??%?); destruct (E)
     153            | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
     154                cases (is_final_state s2);
     155                [ #F cases F; #r' #FINAL #E whd in E:(??%?);
     156                    destruct (E);
     157                    inversion FINAL;
     158                    #r'' #m'' #E1 #E2 destruct (E1 E2); //;
     159                | #NF #E whd in E:(??%?); destruct (E)
     160                ]
     161            | #E whd in E:(??%?); destruct (E)
     162            ]
     163       | #tr #s #e #e' #H #EXEC #E destruct (E)
     164       | #EXEC #E destruct (E)
     165       | #o2 #k2 #i2 #e2 #H #EXEC #E destruct (E)
     166       ]
     167   | #x cases x; #tr #s whd in ⊢ (??%? → ?);
     168       cases (is_final_state s); #F #E whd in E:(??%?); destruct (E)
     169   | #E whd in E:(??%?); destruct (E)
     170   ]
     171] qed.
    173172
    174173(* NB: the E0 in the execs are irrelevant. *)
    175 nlemma several_steps: ∀ge,tr,e,e',s,s'.
     174lemma several_steps: ∀ge,tr,e,e',s,s'.
    176175  execution_isteps tr s e s' e' →
    177176  exec_from ge s e →
    178177  star (mk_transrel … step) ge s tr s' ∧
    179178  exec_from ge s' e'.
    180 #ge tr0 e0 e0' s0 s0' H;
    181 nelim H;
    182 ##[ #s e EXEC; @; //;
    183 ##| #e1 e2 tr1 tr2 s1 s2 s3 STEPS IH EXEC;
    184     nelim (exec_from_step … EXEC); #EXEC3 EXEC1;
    185     nelim (IH EXEC1);
    186     #STAR12 EXEC2; @; //;
    187     nlapply (exec_step_sound ge s3);
    188     nrewrite > EXEC3; #STEP3;
    189     napply (star_step (mk_transrel ?? step) … STEP3 STAR12);
    190     napply refl
    191 ##| #e1 e2 o k i s1 s2 s3 tr1 tr2 STEPS IH EXEC;
    192     nelim (exec_from_interact … EXEC);
    193     #STEP3 EXEC1;
    194     nelim (IH EXEC1); #STAR EXEC2;
    195     @;
    196     ##[ napply (star_step (mk_transrel ?? step) … STEP3 STAR);
    197         napply refl
    198     ##| //
    199     ##]
    200 ##] nqed.
    201 
    202 ninductive execution_terminates : trace → state → s_execution → int → mem → Prop ≝
     179#ge #tr0 #e0 #e0' #s0 #s0' #H
     180elim H;
     181[ #s #e #EXEC % //;
     182| #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #STEPS #IH #EXEC
     183    elim (exec_from_step … EXEC); #EXEC3 #EXEC1
     184    elim (IH EXEC1);
     185    #STAR12 #EXEC2 % //;
     186    lapply (exec_step_sound ge s3);
     187    >EXEC3 #STEP3
     188    @(star_step (mk_transrel ?? step) … STEP3 STAR12)
     189    @refl
     190| #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #STEPS #IH #EXEC
     191    elim (exec_from_interact … EXEC);
     192    #STEP3 #EXEC1
     193    elim (IH EXEC1); #STAR #EXEC2
     194    %
     195    [ @(star_step (mk_transrel ?? step) … STEP3 STAR)
     196        @refl
     197    | //
     198    ]
     199] qed.
     200
     201inductive execution_terminates : trace → state → s_execution → int → mem → Prop ≝
    203202| terminates : ∀s,s',tr,tr',r,e,m.
    204203    execution_isteps tr s e s' (se_stop tr' r m) →
     
    209208    execution_terminates (tr⧺tr') s (se_step E0 s e) r m.
    210209
    211 ncoinductive execution_diverging : s_execution → Prop ≝
     210coinductive execution_diverging : s_execution → Prop ≝
    212211| diverging_step : ∀s,e. execution_diverging e → execution_diverging (se_step E0 s e).
    213212
    214213(* Makes a finite number of interactions (including cost labels) before diverging. *)
    215 ninductive execution_diverges : trace → state → s_execution → Prop ≝
     214inductive execution_diverges : trace → state → s_execution → Prop ≝
    216215| diverges_diverging: ∀tr,s,s',e,e'.
    217216    execution_isteps tr s e s' e' →
     
    220219
    221220(* NB: "reacting" includes hitting a cost label. *)
    222 ncoinductive execution_reacting : traceinf → state → s_execution → Prop ≝
     221coinductive execution_reacting : traceinf → state → s_execution → Prop ≝
    223222| reacting: ∀tr,tr',s,s',e,e'.
    224223    execution_reacting tr' s' e' →
     
    227226    execution_reacting (tr⧻tr') s e.
    228227
    229 ninductive execution_reacts : traceinf → state → s_execution → Prop ≝
     228inductive execution_reacts : traceinf → state → s_execution → Prop ≝
    230229| reacts: ∀tr,s,e.
    231230    execution_reacting tr s e →
    232231    execution_reacts tr s (se_step E0 s e).
    233232
    234 ninductive execution_goes_wrong: trace → state → s_execution → state → Prop ≝
     233inductive execution_goes_wrong: trace → state → s_execution → state → Prop ≝
    235234| go_wrong: ∀tr,s,s',e.
    236235    execution_isteps tr s e s' se_wrong →
    237236    execution_goes_wrong tr s (se_step E0 s e) s'.
    238237
    239 nlet corec silent_sound ge s e
     238let corec silent_sound ge s e
    240239  (H0:execution_diverging e)
    241240  (EXEC:exec_from ge s e)
    242241  : forever_silent (mk_transrel ?? step) … ge s ≝ ?.
    243 ncut (∃s2.∃e2.And (And (execution_diverging e2) (step ge s E0 s2)) (exec_from ge s2 e2));
    244 ##[ ncases H0 in EXEC ⊢ %; #s1 e1 H1 EXEC;
    245     nelim (exec_from_step … EXEC);
    246     #EXEC0 EXEC1;
    247     @ s1; @ e1; @; //; @; //;
    248     nlapply (exec_step_sound ge s); nrewrite > EXEC0; nwhd in ⊢ (% → ?); //;
    249 ##| *; #s2; *; #e2; *; *; #H2 STEP2 EXEC2;
    250     napply (forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 e2 ??));
     242cut (∃s2.∃e2.And (And (execution_diverging e2) (step ge s E0 s2)) (exec_from ge s2 e2));
     243[ cases H0 in EXEC ⊢ %; #s1 #e1 #H1 #EXEC
     244    elim (exec_from_step … EXEC);
     245    #EXEC0 #EXEC1
     246    %{ s1} %{ e1} % //; % //;
     247    lapply (exec_step_sound ge s); >EXEC0 whd in ⊢ (% → ?); #H @H
     248| *; #s2 *; #e2 *; *; #H2 #STEP2 #EXEC2
     249    @(forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 e2 ??))
    251250    //;
    252 ##] nqed.
    253 
    254 nlemma final_step: ∀ge,tr,r,m,s.
     251] qed.
     252
     253lemma final_step: ∀ge,tr,r,m,s.
    255254  exec_from ge s (se_stop tr r m) →
    256255  step ge s tr (Returnstate (Vint r) Kstop m).
    257 #ge tr r m s EXEC;
    258 nwhd in EXEC;
    259 ninversion EXEC;
    260 ##[ #tr' r' m' EXEC' E; ndestruct (E);
    261     nlapply (exec_step_sound ge s);
    262     nrewrite > (exec_inf_aux_unfold …) in EXEC';
    263     ncases (exec_step ge s);
    264     ##[ #o k EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
    265     ##| #x; ncases x; #tr'' s'; nwhd in ⊢ (??%? → ?);
    266         ncases (is_final_state s'); #F; ##[ ##1: ncases F; #r'' FINAL; ##]
    267         #EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
    268     ##| #EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
    269     ##]
    270     ninversion FINAL; #r''' m' E1 E2 H; ndestruct (E1 E2);
    271     napply H;
    272 ##| #tr' s' e' se' H EXEC' E; ndestruct
    273 ##| #EXEC' E; ndestruct
    274 ##| #o k i e H EXEC E; ndestruct
    275 ##] nqed.
    276 
    277 
    278 nlemma e_stop_inv: ∀ge,x,tr,r,m.
     256#ge #tr #r #m #s #EXEC
     257whd in EXEC;
     258inversion EXEC;
     259[ #tr' #r' #m' #EXEC' #E destruct (E);
     260    lapply (exec_step_sound ge s);
     261    >(exec_inf_aux_unfold …) in EXEC';
     262    cases (exec_step ge s);
     263    [ #o #k #EXEC' whd in EXEC':(??%?); destruct (EXEC');
     264    | #x cases x; #tr'' #s' whd in ⊢ (??%? → ?);
     265        cases (is_final_state s'); #F [ 1: cases F; #r'' #FINAL ]
     266        #EXEC' whd in EXEC':(??%?); destruct (EXEC');
     267    | #EXEC' whd in EXEC':(??%?); destruct (EXEC');
     268    ]
     269    inversion FINAL; #r''' #m' #E1 #E2 #H destruct (E1 E2);
     270    @H
     271| #tr' #s' #e' #se' #H #EXEC' #E destruct
     272| #EXEC' #E destruct
     273| #o #k #i #e #H #EXEC #E destruct
     274] qed.
     275
     276
     277lemma e_stop_inv: ∀ge,x,tr,r,m.
    279278  exec_inf_aux ge x = e_stop tr r m →
    280279  x = Value ??? 〈tr,Returnstate (Vint r) Kstop m〉.
    281 #ge x tr r m;
    282 nrewrite > (exec_inf_aux_unfold …); ncases x;
    283 ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct;
    284 ##| #z; ncases z; #tr' s'; nwhd in ⊢ (??%? → ?); ncases (is_final_state s');
    285   ##[ #F; ncases F; #r' FINAL; ncases FINAL; #r'' m' EXEC; nwhd in EXEC:(??%?);
    286       ndestruct (EXEC); napply refl;
    287   ##| #F EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
    288   ##]
    289 ##| #EXEC; nwhd in EXEC:(??%?); ndestruct (EXEC);
    290 ##] nqed.
    291 
    292 nlemma terminates_sound: ∀ge,tr,s,r,m,e.
     280#ge #x #tr #r #m
     281>(exec_inf_aux_unfold …) cases x;
     282[ #o #k #EXEC whd in EXEC:(??%?); destruct;
     283| #z cases z; #tr' #s' whd in ⊢ (??%? → ?); cases (is_final_state s');
     284  [ #F cases F; #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);
     285      destruct (EXEC); @refl
     286  | #F #EXEC whd in EXEC:(??%?); destruct (EXEC);
     287  ]
     288| #EXEC whd in EXEC:(??%?); destruct (EXEC);
     289] qed.
     290
     291lemma terminates_sound: ∀ge,tr,s,r,m,e.
    293292  execution_terminates tr s (se_step E0 s e) r m →
    294293  exec_from ge s e →
    295294  star (mk_transrel … step) ge s tr (Returnstate (Vint r) Kstop m).
    296 #ge tr0 s0 r m e0 H; ninversion H;
    297 ##[ #s s' tr tr' r e m ESTEPS E1 E2 E3 E4 E5 EXEC;
    298     ndestruct (E1 E2 E3 E4 E5);
    299     ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
    300     napply (star_right … STARs');
    301     ##[ ##2: napply (final_step ge tr' r m s' … EXECs');
    302     ##| ##skip
    303     ##| napply refl
    304     ##]
    305 ##| #s s' tr tr' r e m o k i ESTEPS E1 E2 E3 E4 E5 EXEC;
    306     ndestruct;
    307     ncases (several_steps … ESTEPS EXEC); #STARs' EXECs';
    308     napply (star_right … STARs');
    309     ##[ napply tr'
    310     ##| napply (exec_from_interact_stop … EXECs');
    311     ##| napply refl
    312     ##]
    313 ##] nqed.
    314 
    315 nlet corec reacts_sound ge tr s e
     295#ge #tr0 #s0 #r #m #e0 #H inversion H;
     296[ #s #s' #tr #tr' #r #e #m #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC
     297    destruct (E1 E2 E3 E4 E5);
     298    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
     299    @(star_right … STARs')
     300    [ 2: @(final_step ge tr' r m s' … EXECs')
     301    | skip
     302    | @refl
     303    ]
     304| #s #s' #tr #tr' #r #e #m #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #EXEC
     305    destruct;
     306    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
     307    @(star_right … STARs')
     308    [ @tr'
     309    | @(exec_from_interact_stop … EXECs')
     310    | @refl
     311    ]
     312] qed.
     313
     314let corec reacts_sound ge tr s e
    316315  (REACTS:execution_reacting tr s e)
    317316  (EXEC:exec_from ge s e) :
    318317  forever_reactive (mk_transrel … step) ge s tr ≝ ?.
    319 ncut (∃s'.∃e'.∃tr'.∃tr''.(And (And (And (execution_reacting tr'' s' e') (execution_isteps tr' s e s' e')) (tr' ≠ E0)) (tr = tr'⧻tr'')));
    320 ##[ ninversion REACTS;
    321     #tr0 tr' s0 s' e0 e' EREACTS ESTEPS REACTED E1 E2 E3; ndestruct (E2 E3);
    322     @ s'; @ e'; @ tr0; @ tr'; @; ##[ @; ##[ @; //; ##| napply REACTED ##] ##| napply refl ##]
    323 ##| *; #s'; *; #e'; *; #tr'; *; #tr'';
    324     *; *; *; #REACTS' ESTEPS REACTED APPTR;
    325 (*    nrewrite > APPTR;*)
    326     napply (match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ]);
    327     @;
    328     ncases (several_steps … ESTEPS EXEC); #STEPS EXEC';
    329     ##[ ##2: napply STEPS;
    330     ##| ##skip
    331     ##| napply REACTED
    332     ##| napply reacts_sound;
    333       ##[ ##2: napply REACTS';
    334       ##| ##skip
    335       ##| napply EXEC'
    336       ##]
    337     ##]
    338 nqed.
    339 
    340 nlemma exec_from_wrong: ∀ge,s.
     318cut (∃s'.∃e'.∃tr'.∃tr''.(And (And (And (execution_reacting tr'' s' e') (execution_isteps tr' s e s' e')) (tr' ≠ E0)) (tr = tr'⧻tr'')));
     319[ inversion REACTS;
     320    #tr0 #tr' #s0 #s' #e0 #e' #EREACTS #ESTEPS #REACTED #E1 #E2 #E3 destruct (E2 E3);
     321    %{ s'} %{ e'} %{ tr0} %{ tr'} % [ % [ % //; | @REACTED ] | @refl ]
     322| *; #s' *; #e' *; #tr' *; #tr''
     323    *; *; *; #REACTS' #ESTEPS #REACTED #APPTR
     324(*    >APPTR *)
     325    @(match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ])
     326    %
     327    cases (several_steps … ESTEPS EXEC); #STEPS #EXEC'
     328    [ 2: @STEPS
     329    | skip
     330    | @REACTED
     331    | @reacts_sound
     332      [ 2: @REACTS'
     333      | skip
     334      | @EXEC'
     335      ]
     336    ]
     337qed.
     338
     339lemma exec_from_wrong: ∀ge,s.
    341340  exec_from ge s se_wrong →
    342341  exec_step ge s = Wrong ???.
    343 #ge s H; nwhd in H;
    344 ninversion 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 
    357 nlemma exec_from_step_notfinal: ∀ge,s,tr,s',e.
     342#ge #s #H whd in H;
     343inversion H;
     344[ #tr #r #m #EXEC #E destruct (E)
     345| #tr #s' #e #e' #H #EXEC #E destruct (E)
     346| >(exec_inf_aux_unfold …)
     347    cases (exec_step ge s);
     348  [ #o #k #EXEC whd in EXEC:(??%?); destruct
     349  | #x cases x; #tr #s' whd in ⊢ (??%? → ?); cases (is_final_state s');
     350      #F #EXEC whd in EXEC:(??%?); destruct
     351  | //
     352  ]
     353| #o #k #i #e #H #EXEC #E destruct
     354] qed.
     355
     356lemma exec_from_step_notfinal: ∀ge,s,tr,s',e.
    358357  exec_from ge s (se_step tr s' e) →
    359358  ¬(∃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 
    374 nlemma exec_from_interact_step_notfinal: ∀ge,s,o,k,i,tr,s',e.
     359#ge #s #tr #s' #e #H whd in H; inversion H;
     360[ #tr' #r #m #EXEC #E destruct
     361| #tr' #s'' #e' #e'' #H #EXEC #E destruct (E);
     362    >(exec_inf_aux_unfold …) in EXEC;
     363    cases (exec_step ge s);
     364    [ #o #k #EXEC whd in EXEC:(??%?); destruct
     365    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?); cases (is_final_state s1);
     366        #F #E whd in E:(??%?); destruct; @F
     367    | #E whd in E:(??%?); destruct
     368    ]
     369| #EXEC #E destruct
     370| #o #k #i #e' #H #EXEC #E destruct
     371] qed.
     372
     373lemma exec_from_interact_step_notfinal: ∀ge,s,o,k,i,tr,s',e.
    375374  exec_from ge s (se_interact o k i (se_step tr s' e)) →
    376375  ¬(∃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;
    379 ninversion 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 
    409 nlemma wrong_sound: ∀ge,tr,s,s',e.
     376#ge #s #o #k #i #tr #s' #e #H
     377% *; #r #F cases F in H; #r' #m #H
     378inversion H;
     379[ #tr' #r #m #EXEC #E destruct
     380| #tr' #s'' #e' #e'' #H #EXEC #E destruct (E);
     381| #EXEC #E destruct
     382| #o' #k' #i' #e' #H #EXEC #E destruct;
     383    >(exec_inf_aux_unfold …) in EXEC;
     384    cases (exec_step ge s);
     385    [ #o1 #k1 #EXEC1 whd in EXEC1:(??%?); destruct (EXEC1);
     386        inversion H;
     387        [ #tr1 #r1 #m1 #EXECK #E destruct (E);
     388        | #tr1 #s1 #e1 #e2 #H1 #EXECK #E destruct (E);
     389            >(exec_inf_aux_unfold …) in EXECK;
     390            cases (k1 i');
     391            [ #o2 #k2 #EXECK whd in EXECK:(??%?); destruct
     392            | #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?);
     393                cases (is_final_state s2); #F #EXECK
     394                whd in EXECK:(??%?); destruct;
     395                @(absurd ?? F)
     396                %{ r'} //;
     397            | #E whd in E:(??%?); destruct
     398            ]
     399        | #EXECK #E  whd in E:(??%?); destruct
     400        | #o2 #k2 #i2 #e2 #H2 #EXECK #E destruct
     401        ]
     402    | #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?);
     403        cases (is_final_state s1); #F #E whd in E:(??%?); destruct;
     404    | #E whd in E:(??%?); destruct
     405    ]
     406] qed.
     407
     408lemma wrong_sound: ∀ge,tr,s,s',e.
    410409  execution_goes_wrong tr s (se_step E0 s e) s' →
    411410  exec_from ge s e →
     
    414413  nostep (mk_transrel … step) ge s' ∧
    415414  (¬∃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);
    418 ncases (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');
     415#ge #tr0 #s0 #s0' #e0 #WRONG inversion WRONG;
     416#tr #s #s' #e #ESTEPS #E1 #E2 #E3 #E4 #EXEC #NOTFINAL destruct (E1 E2 E3 E4);
     417cases (several_steps … ESTEPS EXEC);
     418#STAR #EXEC' %
     419[ % [ @STAR
     420       | #badtr #bads % #badSTEP
     421           lapply (step_complete … badSTEP);
     422           >(exec_from_wrong … EXEC')
    424423           //;
    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 
    441 ninductive execution_characterisation : state → s_execution → Prop ≝
     424       ]
     425| %
     426    elim ESTEPS in NOTFINAL EXEC ⊢ %;
     427    [ #s1 #e1 #NF #EX #F @(absurd ? F NF)
     428    | #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #ESTEPS1 #IH #NF #EXEC
     429        cases (exec_from_step … EXEC); #EXEC3 #EXEC1
     430        @(IH … EXEC1)
     431        @(exec_from_step_notfinal … EXEC)
     432    | #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #ESTEPS1 #IH #NF #EXEC
     433        @IH
     434        [ @(exec_from_interact_step_notfinal … EXEC)
     435        | cases (exec_from_interact … EXEC); //;
     436        ]
     437    ]
     438] qed.
     439
     440inductive execution_characterisation : state → s_execution → Prop ≝
    442441| ec_terminates: ∀s,r,m,e,tr.
    443442    execution_terminates tr s e r m →
     
    454453
    455454(* bit of a hack to avoid inability to reduce term in match *)
    456 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 ≝
     455definition interact_prop : ∀A:Type[0].(∀o:io_out. (io_in o → IO io_out io_in A) → Prop) → IO io_out io_in A → Prop ≝
    457456λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ].
    458457
    459 nlemma err_does_not_interact: ∀A,B,P,e1,e2.
     458lemma err_does_not_interact: ∀A,B,P,e1,e2.
    460459  (∀x:B.interact_prop A P (e2 x)) →
    461460  interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2).
    462 #A B P e1 e2 H;
    463 ncases e1; //; nqed.
    464 
    465 nlemma err2_does_not_interact: ∀A,B,C,P,e1,e2.
     461#A #B #P #e1 #e2 #H
     462cases e1; //; qed.
     463
     464lemma err2_does_not_interact: ∀A,B,C,P,e1,e2.
    466465  (∀x,y.interact_prop A P (e2 x y)) →
    467466  interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2).
    468 #A B C P e1 e2 H;
    469 ncases e1; ##[ #z; ncases z; ##] //; nqed.
    470 
    471 nlemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2.
     467#A #B #C #P #e1 #e2 #H
     468cases e1; [ #z cases z; ] //; qed.
     469
     470lemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2.
    472471  (∀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;
    475 ncases e1; //; nqed.
    476 
    477 nlemma opt_does_not_interact: ∀A,B,P,e1,e2.
     472  interact_prop A P (bindIO ?? (Sig B Q) A (err_to_io_sig ??? Q e1) e2).
     473#A #B #P #Q #e1 #e2 #H
     474cases e1; //; qed.
     475
     476lemma opt_does_not_interact: ∀A,B,P,e1,e2.
    478477  (∀x:B.interact_prop A P (e2 x)) →
    479478  interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2).
    480 #A B P e1 e2 H;
    481 ncases e1; //; nqed.
    482 
    483 nlemma exec_step_interaction:
     479#A #B #P #e1 #e2 #H
     480cases e1; //; qed.
     481
     482lemma exec_step_interaction:
    484483  ∀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; //; ##]
     484#ge #s cases s;
     485[ #f #st #kk #e #m cases st;
     486  [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
     487  [ 4,6,8,9: @I ]
     488  whd in ⊢ (???%);
     489  [ cases a; [ cases (fn_return f); //; | #e whd nodelta in ⊢ (???%);
     490                    cases (type_eq_dec (fn_return f) Tvoid); #x //; @err2_does_not_interact // ]
     491  | cases (find_label a (fn_body f) (call_cont kk)); [ @I | #z cases z #x #y @I ]
     492  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I
     493  | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
     494  | @err2_does_not_interact #x1 #x2 cases x1; //;
     495  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5  @err_does_not_interact #x6 cases a;
     496      [ @I | #x7 @err2_does_not_interact #x8 #x9 @I ]
     497  | cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
     498      | @I ]
     499  | cases kk; [ 1,8: cases (fn_return f); //; | 2,3,5,6,7: //;
     500      | #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I ]
     501  | cases kk; //;
     502  | cases kk; [ 4: #z1 #z2 #z3  @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I
     503      | *: // ]
     504  ]
     505| #f #args #kk #m cases f;
     506  [ #f' whd in ⊢ (???%); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
     507    #x1 #x2 whd in ⊢ (???%) @err_does_not_interact //
    510508  (* 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.
     509  | #fn #argtys #rty whd in ⊢ (???%);
     510      @err_does_not_interact #x1
     511      whd; #i % [ 2: % [ 2: % [ % whd in ⊢ (??%?); @refl
     512        | % #E whd in E:(??%%); destruct (E); ] ] ]
     513  ]
     514| #v #kk #m whd in ⊢ (???%); cases kk;
     515    [ 8: #x1 #x2 #x3 #x4 cases x1;
     516      [ whd in ⊢ (???%); cases v; // | #x5 whd in ⊢ (???%); cases x5;
     517          #x6 #x7 @opt_does_not_interact // ]
     518    | *: // ]
     519] qed.
    522520
    523521
    524522(* Some classical logic (roughly like a fragment of Coq's library) *)
    525 nlemma classical_doubleneg:
     523lemma classical_doubleneg:
    526524  ∀classic:(∀P:Prop.P ∨ ¬P).
    527525  ∀P:Prop. ¬ (¬ P) → P.
    528 #classic P; *; #H;
    529 ncases (classic P);
    530 ##[ // ##| #H'; napply False_ind; /2/; ##]
    531 nqed.
    532 
    533 nlemma classical_not_all_not_ex:
     526#classic #P *; #H
     527cases (classic P);
     528[ // | #H' @False_ind /2/; ]
     529qed.
     530
     531lemma classical_not_all_not_ex:
    534532  ∀classic:(∀P:Prop.P ∨ ¬P).
    535   ∀A:Type.∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x.
    536 #classic A P; *; #H;
    537 napply (classical_doubleneg classic); @; *; #H';
    538 napply H; #x; @; #H''; napply H'; @x; napply H'';
    539 nqed.
    540 
    541 nlemma classical_not_all_ex_not:
     533  ∀A:Type[0].∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x.
     534#classic #A #P *; #H
     535@(classical_doubleneg classic) % *; #H'
     536@H #x % #H'' @H' %{x} @H''
     537qed.
     538
     539lemma classical_not_all_ex_not:
    542540  ∀classic:(∀P:Prop.P ∨ ¬P).
    543   ∀A:Type.∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x.
    544 #classic A P; *; #H;
    545 napply (classical_not_all_not_ex classic A (λx.¬ P x));
    546 @; #H'; napply H; #x; napply (classical_doubleneg classic);
    547 napply H';
    548 nqed.
    549 
    550 nlemma not_ex_all_not:
    551   ∀A:Type.∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x.
    552 #A P; *; #H x; @; #H';
    553 napply H; @ x; napply H';
    554 nqed.
    555 
    556 nlemma not_imply_elim:
     541  ∀A:Type[0].∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x.
     542#classic #A #P *; #H
     543@(classical_not_all_not_ex classic A (λx.¬ P x))
     544% #H' @H #x @(classical_doubleneg classic)
     545@H'
     546qed.
     547
     548lemma not_ex_all_not:
     549  ∀A:Type[0].∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x.
     550#A #P *; #H #x % #H'
     551@H %{ x} @H'
     552qed.
     553
     554lemma not_imply_elim:
    557555  ∀classic:(∀P:Prop.P ∨ ¬P).
    558556  ∀P,Q:Prop. ¬ (P → Q) → P.
    559 #classic P Q; *; #H;
    560 napply (classical_doubleneg classic); @; *; #H';
    561 napply H; #H''; napply False_ind; napply H'; napply H'';
    562 nqed.
    563 
    564 nlemma not_imply_elim2:
     557#classic #P #Q *; #H
     558@(classical_doubleneg classic) % *; #H'
     559@H #H'' @False_ind @H' @H''
     560qed.
     561
     562lemma not_imply_elim2:
    565563  ∀P,Q:Prop. ¬ (P → Q) → ¬ Q.
    566 #P Q; *; #H; @; #H';
    567 napply H; #_; napply H';
    568 nqed.
    569 
    570 nlemma imply_to_and:
     564#P #Q *; #H % #H'
     565@H #_ @H'
     566qed.
     567
     568lemma imply_to_and:
    571569  ∀classic:(∀P:Prop.P ∨ ¬P).
    572570  ∀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 
    578 nlemma not_and_to_imply:
     571#classic #P #Q #H %
     572[ @(not_imply_elim classic P Q H)
     573| @(not_imply_elim2 P Q H)
     574] qed.
     575
     576lemma not_and_to_imply:
    579577  ∀classic:(∀P:Prop.P ∨ ¬P).
    580578  ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q.
    581 #classic P Q; *; #H H';
    582 @; #H''; napply H; @; //;
    583 nqed.
    584 
    585 ninductive execution_not_over : s_execution → Prop ≝
     579#classic #P #Q *; #H #H'
     580% #H'' @H % //;
     581qed.
     582
     583inductive execution_not_over : s_execution → Prop ≝
    586584| eno_step: ∀tr,s,e. execution_not_over (se_step tr s e)
    587585| eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)).
    588586
    589 nlemma 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 
    595 nlemma 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 
    601 nlet corec show_divergence s e
     587lemma eno_stop: ∀tr,r,m. execution_not_over (se_stop tr r m) → False.
     588#tr0 #r0 #m0 #H inversion H;
     589[ #tr #s #e #E destruct
     590| #o #k #tr #s #e #i #E destruct
     591] qed.
     592
     593lemma eno_wrong: execution_not_over se_wrong → False.
     594#H inversion H;
     595[ #tr #s #e #E destruct
     596| #o #k #tr #s #e #i #E destruct
     597] qed.
     598
     599let corec show_divergence s e
    602600 (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
    603601                 execution_not_over e1)
    604602 (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)
     603 (CONTINUES:∀tr2,s2,o,k,i,e'. execution_isteps tr2 s e s2 (se_interact o k i e') → ∃tr3.∃s3.∃e3. And (e' = se_step tr3 s3 e3) (tr3 ≠ E0))
    606604 : execution_diverging e ≝ ?.
    607 nlapply (NONTERMINATING E0 s e ?); //;
    608 ncases 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 
    638 nlemma se_inv: ∀e1,e2.
     605lapply (NONTERMINATING E0 s e ?); //;
     606cases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %;
     607[ #tr #i #m #_ #_ #_ #ENO elim (eno_stop … ENO);
     608| #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?);
     609  [ <(E0_right tr) in ⊢ (?%????)
     610      @isteps_one @isteps_none
     611  | #TR @(match sym_eq ??? TR with [ refl ⇒ ? ]) (* >TR in UNREACTIVE ⊢ % *)
     612      #NONTERMINATING #CONTINUES #_ %
     613      @(show_divergence s')
     614      [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1)
     615        change in ⊢ (?%????) with (Eapp E0 tr1); @isteps_one
     616        @S
     617      | #tr2 #s2 #e2 #S >TR in UNREACTIVE #UNREACTIVE @(UNREACTIVE tr2 s2 e2)
     618          change in ⊢ (?%????) with (Eapp E0 tr2);
     619          @isteps_one @S
     620      | #tr2 #s2 #o #k #i #e2 #S @(CONTINUES tr2 s2 o k i)
     621          change in ⊢ (?%????) with (Eapp E0 tr2);
     622          @(isteps_one … S)
     623      ]
     624  ]
     625| #_ #_ #_ #ENO elim (eno_wrong … ENO);
     626| #o #k #i #e' #UNREACTIVE #NONTERMINATING #CONTINUES #_
     627    lapply (CONTINUES E0 s o k i e' (isteps_none …));
     628    *; #tr' *; #s' *; #e' *; #EXEC #NOTSILENT
     629    @False_ind @(absurd ?? NOTSILENT)
     630    @(UNREACTIVE … s' e')
     631    <(E0_right tr') in ⊢ (?%????)
     632    >EXEC
     633    @isteps_interact //;
     634] qed.
     635
     636(* XXX == > jmeq notation and coercion *)
     637
     638lemma jmeq_to_eq : ∀A:Type[0].∀a,b:A.jmeq A a A b → a = b.
     639#A #a #b #E @gral @jm_to_eq_sigma @E
     640qed.
     641
     642coercion jmeq_to_eq : ∀A:Type[0].∀a,b:A.∀p:jmeq A a A b.a = b ≝
     643  jmeq_to_eq on _p: jmeq ???? to eq ???.
     644
     645notation > "hvbox(a break ≃ b)"
     646  non associative with precedence 45
     647for @{ 'jmeq ? $a ? $b }.
     648
     649notation < "hvbox(term 46 a break maction (≃) (≃\sub(t,u)) term 46 b)"
     650  non associative with precedence 45
     651for @{ 'jmeq $t $a $u $b }.
     652
     653interpretation "john major's equality" 'jmeq t x u y = (jmeq t x u y).
     654
     655(* XXX < == *)
     656
     657lemma se_inv: ∀e1,e2.
    639658  single_exec_of e1 e2 →
    640659  match e1 with
     
    644663  | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ]
    645664  ].
    646 #e01 e02 H;
    647 ncases 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 
    654 nlemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
     665#e01 #e02 #H
     666cases H;
     667[ #tr #r #m whd; % [ % ] //
     668| #tr #s #e1' #e2' #H' whd; % [ % ] //
     669| whd; //
     670| #o #k #i #e #H' whd; % [ % ] //
     671] qed.
     672
     673lemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
    655674  exec_from ge s (se_interact o k i (se_step tr s' e)) →
    656675  tr ≠ E0.
    657 #ge o k i tr s s' e; nwhd in ⊢ (% → ?); nrewrite > (exec_inf_aux_unfold …);
    658 nlapply (exec_step_interaction ge s);
    659 ncases (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 
    688 nlet corec reactive_traceinf' ge s e
     676#ge #o #k #i #tr #s #s' #e whd in ⊢ (% → ?); >(exec_inf_aux_unfold …)
     677lapply (exec_step_interaction ge s);
     678cases (exec_step ge s);
     679[ #o' #k' ; whd in ⊢ (% → ?%? → ?); #H #K cases (se_inv … K);
     680    *; #E1 #E2 #H1 destruct (E1);
     681    lapply (H i); *; #tr' *; #s'' *; #K' #TR
     682    >E2 in H1 #H1 whd in H1:(?%?); >K' in H1
     683    >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?);
     684    cases (is_final_state s'');
     685    [ #F whd in ⊢ (?%? → ?); #S
     686        @False_ind @(absurd ? S) cases (se_inv … S)
     687    | #NF #S whd in S:(?%?); cases (se_inv … S);
     688        *; #E1 #E2 #S' <E1 @TR
     689    ]
     690| #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?);
     691    cases (is_final_state s''); #F #E whd in E:(?%?);
     692    inversion E;
     693    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
     694    | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct
     695    | 3,7: #E destruct
     696    | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct
     697    ]
     698| #_ #E whd in E:(?%?);
     699    inversion E;
     700    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
     701    | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct
     702    | 3,7: #E1 #E2 destruct
     703    | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct
     704    ]
     705] qed.
     706
     707let corec reactive_traceinf' ge s e
    689708  (EXEC:exec_from ge s e)
    690709  (REACTIVE: ∀tr,s1,e1.
    691710    execution_isteps tr s e s1 e1 →
    692     Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     711    (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)))
    693712  : traceinf' ≝ ?.
    694 nlapply (REACTIVE E0 s e (isteps_none …));
    695 *; #x; ncases x; #tr; #y; ncases y; #s' e'; *; #STEPS H;
    696 @ tr ? H;
    697 napply (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 ##]
    706 nqed.
     713lapply (REACTIVE E0 s e (isteps_none …));
     714*; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H
     715%{ tr ? H}
     716@(reactive_traceinf' ge s' e' ?)
     717[ cases (several_steps … STEPS EXEC); #_ #H' @H'
     718| #tr1 #s1 #e1 #STEPS1
     719    @REACTIVE
     720    [ 2:
     721        @(isteps_trans … STEPS STEPS1)
     722    | skip
     723    ]
     724]
     725qed.
    707726
    708727(* A slightly different version of the above, to work around a problem with the
    709728   next result. *)
    710 nlet corec reactive_traceinf'' ge s e
     729let corec reactive_traceinf'' ge s e
    711730  (EXEC:exec_from ge s e)
    712   (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     731  (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
    713732  (REACTIVE: ∀tr,s1,e1.
    714733    execution_isteps tr s e s1 e1 →
    715     Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     734    (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)))
    716735  : traceinf' ≝ ?.
    717 ncases REACTIVE0; #x; ncases x; #tr; #y; ncases y; #s' e'; *; #STEPS H;
    718 @ tr ? H;
    719 napply (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.
     736cases REACTIVE0; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H
     737%{ tr ? H}
     738@(reactive_traceinf'' ge s' e' ?)
     739[ cases (several_steps … STEPS EXEC); #_ #H' @H'
     740| @(REACTIVE … STEPS)
     741| #tr1 #s1 #e1 #STEPS1
     742    @REACTIVE
     743    [ 2:
     744        @(isteps_trans … STEPS STEPS1)
     745    | skip
     746    ]
     747] qed.
    729748
    730749(* We want to prove
    731750
    732 nlemma show_reactive : ∀ge,s.
     751lemma show_reactive : ∀ge,s.
    733752  ∀REACTIVE:∀tr,s1,e1.
    734753    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
     
    740759we can do case analysis on, then get it into the desired form afterwards.
    741760*)
    742 nlet corec show_reactive' ge s e
     761let corec show_reactive' ge s e
    743762  (EXEC:exec_from ge s e)
    744   (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     763  (REACTIVE0: Sig ? (λx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
    745764  (REACTIVE: ∀tr1,s1,e1.
    746765    execution_isteps tr1 s e s1 e1 →
    747     Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
     766    (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)))
    748767  : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?.
    749 (*nrewrite > (unroll_traceinf' (reactive_traceinf'' …));*)
    750 napply (match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ]);
    751 ncases REACTIVE0;
    752 #x; ncases x; #tr1; #y; ncases y; #s1 e1; #z; ncases z; #STEPS NOTSILENT;
    753 nwhd in ⊢ (?(?%)??);
    754 (*nrewrite > (traceinf_traceinfp_app …);*)
    755 napply (match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ]);
    756 napply (reacting … STEPS NOTSILENT);
    757 napply show_reactive';
    758 nqed.
    759 
    760 nlemma show_reactive : ∀ge,s,e.
     768(*>(unroll_traceinf' (reactive_traceinf'' …)) *)
     769@(match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ])
     770cases REACTIVE0;
     771#x cases x; #tr1 #y cases y; #s1 #e1 #z cases z; #STEPS #NOTSILENT
     772whd in ⊢ (?(?%)??);
     773(*>(traceinf_traceinfp_app …) *)
     774@(match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ])
     775@(reacting … STEPS NOTSILENT)
     776@show_reactive'
     777qed.
     778
     779lemma show_reactive : ∀ge,s,e.
    761780  ∀EXEC:exec_from ge s e.
    762781  ∀REACTIVE:∀tr,s1,e1.
    763782    execution_isteps tr s e s1 e1 →
    764     Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
     783    (Sig ? (λx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)).
    765784  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 
    771 nlemma execution_characterisation_complete:
     785[ #ge #s #e #EXEC #REACTIVE
     786    @show_reactive'
     787| @(REACTIVE … (isteps_none …))
     788] qed.
     789
     790lemma execution_characterisation_complete:
    772791  ∀classic:(∀P:Prop.P ∨ ¬P).
    773   ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
     792  ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P).
    774793   ∀ge,s,e.
    775794   exec_from ge s e →
    776795   execution_characterisation s (se_step E0 s e).
    777 #classic constructive_indefinite_description ge s e EXEC;
    778 ncases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
     796#classic #constructive_indefinite_description #ge #s #e #EXEC
     797cases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
    779798                 execution_not_over e1));
    780 ##[ #NONTERMINATING;
    781     ncases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧
     799[ #NONTERMINATING
     800    cases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧
    782801                     ∀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 →
     802  [ *; #tr *; #s1 *; #e1 *; #INITIAL #UNREACTIVE
     803      @(ec_diverges … s ? tr)
     804      @(diverges_diverging … INITIAL)
     805      @(show_divergence s1 e1)
     806      [ #tr2 #s2 #e2 #S @(NONTERMINATING (Eapp tr tr2) s2 e2)
     807          @(isteps_trans … INITIAL S)
     808      | #tr2 #s2 #e2 #S @(UNREACTIVE … S)
     809      | #tr2 #s2 #o #k #i #e2 #STEPS
     810          lapply (NONTERMINATING (Eapp tr tr2) s2 (se_interact o k i e2) ?);
     811          [ @(isteps_trans … INITIAL STEPS) ]
     812          #NOTOVER inversion NOTOVER;
     813          [ #tr' #s' #e' #E destruct (E);
     814          | #o' #k' #tr' #s' #e' #i' #E destruct (E);
     815              %{ tr'} %{s'} %{e'} % //;
     816              cases (several_steps … INITIAL EXEC); #_ #EXEC1
     817              cases (several_steps … STEPS EXEC1); #_ #EXEC2
     818              @(interaction_is_not_silent … EXEC2)
     819          ]
     820      ]
     821
     822  | *; #NOTUNREACTIVE
     823      cut (∀tr,s1,e1.execution_isteps tr s e s1 e1 →
    805824            ∃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   ##]
     825      [ #tr #s1 #e1 #STEPS
     826          @(classical_doubleneg classic) % #NOREACTION
     827          @NOTUNREACTIVE
     828          %{ tr} %{s1} %{e1} % //;
     829          #tr2 #s2 #e2 #STEPS2
     830          lapply (not_ex_all_not … NOREACTION); #NR1
     831          lapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2
     832          @(classical_doubleneg classic)
     833          @NR2 normalize //
     834      | #REACTIVE
     835          @ec_reacts
     836          [ 2: @reacts
     837                   @(show_reactive ge s … EXEC)
     838                   #tr #s1 #e1 #STEPS
     839                   @constructive_indefinite_description
     840                   @(REACTIVE … tr s1 e1 STEPS)
     841          | skip
     842          ]
     843      ]
     844  ]
    826845 
    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); @; //;
     846| #NOTNONTERMINATING lapply (classical_not_all_ex_not classic … NOTNONTERMINATING);
     847    *; #tr #NNT2 lapply (classical_not_all_ex_not classic … NNT2);
     848    *; #s' #NNT3 lapply (classical_not_all_ex_not classic … NNT3);
     849    *; #e #NNT4 elim (imply_to_and classic … NNT4);
     850    cases e;
     851    [ #tr' #r #m #STEPS #NOSTEP
     852        @(ec_terminates s r m ? (Eapp tr tr')) %
     853        [ @s'
     854        | @STEPS
     855        ]
     856    | #tr' #s'' #e' #STEPS *; #NOSTEP @False_rect_Type0
     857        @NOSTEP //
     858    | #STEPS #NOSTEP
     859        @(ec_wrong ? s s' tr) % //;
    841860    (* The following is stupidly complicated when most of the cases are impossible.
    842861       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 ##]
    887 nqed.   
    888 
    889 ninductive execution_matches_behavior: s_execution → program_behavior → Prop ≝
     862    | #o #k #i #e' #STEPS #NOSTEP
     863        cases e' in STEPS NOSTEP;
     864        [ #tr' #r #m #STEPS #NOSTEP
     865            @(ec_terminates s ???)
     866           [ 4: @(annoying_corner_case_terminates … STEPS) ]
     867        | #tr1 #s1 #e1 #STEPS *; #NOSTEP
     868            @False_ind @NOSTEP //
     869        | #STEPS #NOSTEP
     870            lapply (exec_step_interaction ge s');
     871            cases (several_steps … STEPS EXEC); #_
     872            whd in ⊢ (% → ?);
     873            >(exec_inf_aux_unfold …)
     874            cases (exec_step ge s');
     875            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
     876                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2);
     877                cases (H i); #tr1 *; #s1 *; #K #E >K in H2
     878                >(exec_inf_aux_unfold …)
     879                whd in ⊢ (?%? → ?); cases (is_final_state s1);
     880                #F #S whd in S:(?%?); cases (se_inv … S);
     881            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
     882                cases (is_final_state s'); #F #S whd in S:(?%?);
     883                cases (se_inv … S);
     884            | #S cases (se_inv … S);
     885            ]
     886        | #o1 #k1 #i1 #e1 #STEPS #NOSTEP
     887            lapply (exec_step_interaction ge s');
     888            cases (several_steps … STEPS EXEC); #_
     889            whd in ⊢ (% → ?);
     890            >(exec_inf_aux_unfold …)
     891            cases (exec_step ge s');
     892            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
     893                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2);
     894                cases (H i); #tr1 *; #s1 *; #K #E >K in H2
     895                >(exec_inf_aux_unfold …)
     896                whd in ⊢ (?%? → ?); cases (is_final_state s1);
     897                #F #S whd in S:(?%?); cases (se_inv … S);
     898            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
     899                cases (is_final_state s'); #F #S whd in S:(?%?);
     900                cases (se_inv … S);
     901            | #S cases (se_inv … S);
     902            ]
     903        ]
     904    ]
     905]
     906qed.   
     907
     908inductive execution_matches_behavior: s_execution → program_behavior → Prop ≝
    890909| emb_terminates: ∀s,e,tr,r,m.
    891910    execution_terminates tr s e r m →
     
    903922    execution_matches_behavior se_wrong (Goes_wrong E0).
    904923
    905 nlemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
     924lemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
    906925  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 
    912 nlemma exec_state_diverges: ∀tr,tr',s,s',e.
     926#tr #tr' #s #s' #e #r #m #H inversion H;
     927[ #s1 #s2 #tr1 #tr2 #r' #e' #m' #H' #E1 #E2 #E3 #E4 #E5 destruct; @refl
     928| #s1 #s2 #tr1 #tr2 #r' #e' #m' #o #k #i #H' #E1 #E2 #E3 #E4 #E5 destruct; @refl
     929] qed.
     930
     931lemma exec_state_diverges: ∀tr,tr',s,s',e.
    913932  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 
    917 nlemma exec_state_reacts: ∀tr,tr',s,s',e.
     933#tr #tr' #s #s' #e #H inversion H;
     934#tr1 #s1 #s2 #e1 #e2 #H' #E1 #E2 #E3 #E4 destruct; @refl qed.
     935
     936lemma exec_state_reacts: ∀tr,tr',s,s',e.
    918937  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 
    922 nlemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
     938#tr #tr' #s #s' #e #H inversion H;
     939#tr1 #s1 #e1 #H' #E1 #E2 #E3 destruct; @refl qed.
     940
     941lemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
    923942  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 
    927 nlemma behavior_of_execution: ∀s,e.
     943#tr #tr' #s #s' #s'' #e #H inversion H;
     944#tr1 #s1 #s2 #e1 #H' #E1 #E2 #E3 #E4 destruct; @refl qed.
     945
     946lemma behavior_of_execution: ∀s,e.
    928947  execution_characterisation s e →
    929948  ∃b:program_behavior. execution_matches_behavior e b.
    930 #s0 e0 exec;
    931 ncases 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 
    946 nlemma initial_state_not_final: ∀ge,s.
     949#s0 #e0 #exec
     950cases exec;
     951[ #s #r #m #e #tr #TERM
     952    %{ (Terminates tr r)}
     953    @(emb_terminates … TERM)
     954| #s #e #tr #DIV
     955    %{ (Diverges tr)}
     956    @(emb_diverges … DIV)
     957| #s #e #tr #REACTS
     958    %{ (Reacts tr)}
     959    @(emb_reacts … REACTS)
     960| #e #s #s' #tr #WRONG
     961    %{ (Goes_wrong tr)}
     962    @(emb_wrong … WRONG)
     963] qed.
     964
     965lemma initial_state_not_final: ∀ge,s.
    947966  initial_state ge s →
    948967  ¬ ∃r.final_state s r.
    949 #ge s H; ncases H;
    950 #b f ge m E1 E2 E3 E4; @; *; #r H2;
    951 ninversion H2;
    952 #r' m' E5 E6; ndestruct (E5);
    953 nqed.
    954 
    955 nlemma initial_step: ∀ge,s,e.
     968#ge #s #H cases H;
     969#b #f #ge #m #E1 #E2 #E3 #E4 % *; #r #H2
     970inversion H2;
     971#r' #m' #E5 #E6 destruct (E5);
     972qed.
     973
     974lemma initial_step: ∀ge,s,e.
    956975  exec_inf_aux ge (Value ??? 〈E0,s〉) = e →
    957976  ¬(∃r.final_state s r) →
    958977  ∃e'.e = e_step E0 s e'.
    959 #ge s e; nrewrite > (exec_inf_aux_unfold …);
    960 nwhd 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 ##]
    966 nqed.
    967 
    968 ntheorem exec_inf_equivalence:
     978#ge #s #e >(exec_inf_aux_unfold …)
     979whd in ⊢ (??%? → ?); cases (is_final_state s);
     980[ #FINAL #EXEC #NOTFINAL
     981    @False_ind @(absurd ?? NOTFINAL)
     982    cases FINAL;
     983    #r #F %{r} @F
     984| #F1 #EXEC #F2 whd in EXEC:(??%?); % [ 2: <EXEC @refl ]
     985qed.
     986
     987theorem exec_inf_equivalence:
    969988  ∀classic:(∀P:Prop.P ∨ ¬P).
    970   ∀constructive_indefinite_description:(∀A:Type. ∀P:A→Prop. (∃x. P x) → Σx : A. P x).
     989  ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P).
    971990  ∀p,e. single_exec_of (exec_inf p) e →
    972991   ∃b.execution_matches_behavior e b ∧ exec_program p b.
    973 #classic constructive_indefinite_description p e;
    974 nwhd in ⊢ (?%? → ??(λ_.?(?%?)%));
    975 nlapply (make_initial_state_sound p);
    976 nlapply (the_initial_state p);
    977 ncases (make_initial_state p);
    978 ##[ #gs; ncases gs; #ge s INITIAL' INITIAL; nwhd in INITIAL ⊢ (?%? → ?);
    979     ncases INITIAL; #Ege INITIAL'';
    980     nrewrite > (exec_inf_aux_unfold …);
    981     nwhd in ⊢ (?%? → ?);
    982     ncases (is_final_state s);
    983     ##[ #F; napply False_ind;
    984         napply (absurd ?? (initial_state_not_final … INITIAL''));
    985         ncases F; #r F'; @r; napply F';
    986     ##| #NOTFINAL; nwhd in ⊢ (?%? → ?); ncases e;
    987         ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##]
    988         ncases (se_inv … EXEC0); *; #E1 E2; nrewrite < E1; nrewrite < E2; #EXEC';
    989     nlapply (behavior_of_execution ??
     992#classic #constructive_indefinite_description #p #e
     993whd in ⊢ (?%? → ??(λ_.?(?%?)%));
     994lapply (make_initial_state_sound p);
     995lapply (the_initial_state p);
     996cases (make_initial_state p);
     997[ #gs cases gs; #ge #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
     998    cases INITIAL; #Ege #INITIAL''
     999    >(exec_inf_aux_unfold …)
     1000    whd in ⊢ (?%? → ?);
     1001    cases (is_final_state s);
     1002    [ #F @False_ind
     1003        @(absurd ?? (initial_state_not_final … INITIAL''))
     1004        cases F; #r #F' %{r} @F'
     1005    | #NOTFINAL whd in ⊢ (?%? → ?); cases e;
     1006        [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #EXEC0 | #o #k #i #e #EXEC0 ]
     1007        cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC'
     1008    lapply (behavior_of_execution ??
    9901009              (execution_characterisation_complete classic constructive_indefinite_description ge s ? EXEC'));
    991         *; #b MATCHES; @b; @; //;
    992         #ge'; nrewrite > Ege; #Ege'; nrewrite > (?:ge' = ge); ##[ ##2: ndestruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ##]
    993         ninversion MATCHES;
    994         ##[ #s0 e1 tr1 r m TERM EXEC BEHAVES; nrewrite < EXEC in TERM;
    995             #TERM;
    996             nlapply (exec_state_terminates … TERM); #E1;
    997             nrewrite > E1 in TERM; #TERM;
    998             napply (program_terminates (mk_transrel … step) ?? ge s);
    999             ##[ ##2: napply INITIAL''
    1000             ##| ##3: napply (terminates_sound … TERM EXEC');
    1001             ##| ##skip
    1002             ##| //;
    1003             ##]
    1004         ##| #s0 e tr DIVERGES EXEC E2; nrewrite < EXEC in DIVERGES; #DIVERGES;
    1005             nlapply (exec_state_diverges … DIVERGES);
    1006             #E1; nrewrite > E1 in DIVERGES; #DIVERGES;
    1007             ninversion DIVERGES; #tr' s1 s2 e1 e2 INITSTEPS DIVERGING E4 E5 E6;
    1008             nrewrite < E4 in INITSTEPS ⊢ %; nrewrite < E5 in E6 ⊢ %; #E6 INITSTEPS;
    1009             ncut (e0 = e1); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
    1010             #E7; nrewrite < E7 in INITSTEPS; #INITSTEPS;
    1011             ncases (several_steps … INITSTEPS EXEC'); #INITSTAR EXECDIV;
    1012             napply (program_diverges (mk_transrel … step) ?? ge s … INITIAL'' INITSTAR);
    1013             napply (silent_sound … DIVERGING EXECDIV);
    1014         ##| #s0 e tr REACTS EXEC E2; nrewrite < EXEC in REACTS; #REACTS;
    1015             nlapply (exec_state_reacts … REACTS);
    1016             #E1; nrewrite > E1 in REACTS; #REACTS;
    1017             ninversion REACTS; #tr' s' e'' REACTING E4 E5;
    1018             nrewrite < E4 in REACTING ⊢ %; nrewrite < E5; #REACTING E6;
    1019             ncut (e0 = e''); ##[ ndestruct (E6) skip (MATCHES EXEC0 EXEC'); // ##]
    1020             #E7; nrewrite < E7 in REACTING; #REACTING;
    1021             napply (program_reacts (mk_transrel … step) ?? ge s … INITIAL'');
    1022             napply (reacts_sound … REACTING EXEC');
    1023         ##| #e s1 s2 tr WRONG EXEC E2; nrewrite < EXEC in WRONG; #WRONG;
    1024             nlapply (exec_state_wrong … WRONG);
    1025             #E1; nrewrite > E1 in WRONG; #WRONG;
    1026             ninversion WRONG; #tr' s1' s2' e'' GOESWRONG E4 E5 E6 E7;
    1027             nrewrite < E4 in GOESWRONG ⊢ %; nrewrite < E5; nrewrite < E7; #GOESWRONG;
    1028             ncut (e0 = e''); ##[ ndestruct (E6) skip (INITIAL MATCHES EXEC0 EXEC'); // ##]
    1029             #E8; nrewrite < E8 in GOESWRONG; #GOESWRONG;
    1030             nelim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR STOP FINAL;
    1031             napply (program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL'' STAR STOP);
    1032             #r; @; #F; napply (absurd ?? FINAL); @r; napply F;
    1033         ##| #E; ndestruct (E);
    1034         ##]
    1035    ##]
    1036 ##| nwhd in ⊢ ((∀_.? → %) → ?);
    1037     #NOINIT; #_; #EXEC;
    1038     @ (Goes_wrong E0); @;
    1039     ##[ nwhd in EXEC:(?%?);
    1040         ncases e in EXEC;
    1041         ##[ #tr r m EXEC0 ##| #tr s' e0 EXEC0 ##| #EXEC0 ##| #o k i e EXEC0 ##]
    1042         ncases (se_inv … EXEC0);
    1043         napply emb_initially_wrong;
    1044     ##| #ge Ege;
    1045         napply program_goes_initially_wrong;
    1046         #s; @; #INIT; ncases (NOINIT s INIT); #ge' H; napply H;
    1047     ##]
    1048 ##] nqed.
    1049 
     1010        *; #b #MATCHES %{b} % //;
     1011        #ge' >Ege #Ege' >(?:ge' = ge) [ 2: destruct (Ege') skip (INITIAL Ege EXEC0 EXEC'); // ]
     1012        inversion MATCHES;
     1013        [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM
     1014            #TERM
     1015            lapply (exec_state_terminates … TERM); #E1
     1016            >E1 in TERM #TERM
     1017            @(program_terminates (mk_transrel … step) ?? ge s)
     1018            [ 2: @INITIAL''
     1019            | 3: @(terminates_sound … TERM EXEC')
     1020            | skip
     1021            | //;
     1022            ]
     1023        | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES #DIVERGES
     1024            lapply (exec_state_diverges … DIVERGES);
     1025            #E1 >E1 in DIVERGES #DIVERGES
     1026            inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6
     1027            <E4 in INITSTEPS ⊢ % <E5 in E6 ⊢ % #E6 #INITSTEPS
     1028            cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
     1029            #E7 <E7 in INITSTEPS #INITSTEPS
     1030            cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV
     1031            @(program_diverges (mk_transrel … step) ?? ge s … INITIAL'' INITSTAR)
     1032            @(silent_sound … DIVERGING EXECDIV)
     1033        | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS #REACTS
     1034            lapply (exec_state_reacts … REACTS);
     1035            #E1 >E1 in REACTS #REACTS
     1036            inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5
     1037            <E4 in REACTING ⊢ % <E5 #REACTING #E6
     1038            cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
     1039            #E7 <E7 in REACTING #REACTING
     1040            @(program_reacts (mk_transrel … step) ?? ge s … INITIAL'')
     1041            @(reacts_sound … REACTING EXEC')
     1042        | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG #WRONG
     1043            lapply (exec_state_wrong … WRONG);
     1044            #E1 >E1 in WRONG #WRONG
     1045            inversion WRONG; #tr' #s1' #s2' #e'' #GOESWRONG #E4 #E5 #E6 #E7
     1046            <E4 in GOESWRONG ⊢ % <E5 <E7 #GOESWRONG
     1047            cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ]
     1048            #E8 <E8 in GOESWRONG #GOESWRONG
     1049            elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL
     1050            @(program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL'' STAR STOP)
     1051            #r % #F @(absurd ?? FINAL) %{r} @F
     1052        | #E destruct (E);
     1053        ]
     1054   ]
     1055| whd in ⊢ ((∀_.? → %) → ?);
     1056    #NOINIT #_ #EXEC
     1057    %{ (Goes_wrong E0)} %
     1058    [ whd in EXEC:(?%?);
     1059        cases e in EXEC;
     1060        [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #EXEC0 | #o #k #i #e #EXEC0 ]
     1061        cases (se_inv … EXEC0);
     1062        @emb_initially_wrong
     1063    | #ge #Ege
     1064        @program_goes_initially_wrong
     1065        #s % #INIT cases (NOINIT s INIT); #ge' #H @H
     1066    ]
     1067] qed.
     1068
Note: See TracChangeset for help on using the changeset viewer.