include "Clight/CexecComplete.ma".
include "Clight/CexecSound.ma".
include "utilities/extralib.ma".

include "basics/jmeq.ma".
include alias "basics/logic.ma".

(* A "single execution" - where all of the input values are made explicit. *)
coinductive s_execution : Type[0] ≝
| se_stop : trace → int → mem → s_execution
| se_step : trace → state → s_execution → s_execution
| se_wrong : errmsg → s_execution
| se_interact : ∀o:io_out. (io_in o → execution state io_out io_in) → io_in o → s_execution → s_execution.

coinductive single_exec_of : execution state io_out io_in → s_execution → Prop ≝
| seo_stop : ∀tr,r,s. single_exec_of (e_stop ??? tr r s) (se_stop tr r (mem_of_state s))
| seo_step : ∀tr,s,e,se.
    single_exec_of e se →
    single_exec_of (e_step ??? tr s e) (se_step tr s se)
| seo_wrong : ∀msg:errmsg. single_exec_of (e_wrong ??? msg) (se_wrong msg)
| seo_interact : ∀o,k,i,se.
    single_exec_of (k i) se →
    single_exec_of (e_interact ??? o k) (se_interact o k i se).

(* starting after state s, zero or more steps of execution e reach state s'
   after which comes e'. *)
inductive execution_isteps : trace → state → s_execution → state → s_execution → Prop ≝
| isteps_none : ∀s,e. execution_isteps E0 s e s e
| isteps_one : ∀e,e',tr,tr',s,s',s0.
    execution_isteps tr' s e s' e' →
    execution_isteps (tr⧺tr') s0 (se_step tr s e) s' e'
| isteps_interact : ∀e,e',o,k,i,s,s',s0,tr,tr'.
    execution_isteps tr' s e s' e' →
    execution_isteps (tr⧺tr') s0 (se_interact o k i (se_step tr s e)) s' e'.

lemma isteps_trans: ∀tr1,tr2,s1,s2,s3,e1,e2,e3.
  execution_isteps tr1 s1 e1 s2 e2 →
  execution_isteps tr2 s2 e2 s3 e3 →
  execution_isteps (tr1⧺tr2) s1 e1 s3 e3.
#tr1 #tr2 #s1 #s2 #s3 #e1 #e2 #e3 #H1 elim H1;
[ #s #e //;
| #e #e' #tr #tr' #s1' #s2' #s3' #H1 #H2 #H3
    >(Eapp_assoc …)
    @isteps_one
    @H2 @H3
| #e #e' #o #k #i #s1' #s2' #s3' #tr #tr' #H1 #H2 #H3
    >(Eapp_assoc …)
    @isteps_interact
    /2/
] qed.

lemma is_final_elim: ∀s.∀P:option int → Type[0].
 (∀r. final_state s r → P (Some ? r)) →
 ((¬∃r.final_state s r) → P (None ?)) →
P (is_final s).
#s #P #F #NF lapply (refl ? (is_final s))
cases (is_final s) in ⊢ (???% → %);
[ #E @NF % * #r #H whd in E:(??%?); > (is_final_complete … H) in E; #H destruct
| #r #E @F @is_final_sound @E
] qed.

lemma is_final_elim': ∀ge,s.∀P:option int → Type[0].
 (∀r. final_state s r → P (Some ? r)) →
 ((¬∃r.final_state s r) → P (None ?)) →
P (is_final io_out io_in clight_fullexec ge s).
#ge @is_final_elim qed.

lemma exec_e_step: ∀ge,x,tr,s,e.
  exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e →
  exec_inf_aux ?? clight_exec ge (exec_step ge s) = e.
#ge #x #tr #s #e
>(exec_inf_aux_unfold …) cases x;
[ #o #k #EXEC whd in EXEC:(??%?); destruct
| #y cases y #tr' #s' whd in ⊢ (??%? → ?);
  @is_final_elim'
  [ #r #FINAL | #FINAL ]
  #EXEC whd in EXEC:(??%?); destruct @refl
| #msg #EXEC whd in EXEC:(??%?); destruct
] qed.

lemma exec_e_step_inv: ∀ge,x,tr,s,e.
  exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e →
  x = Value ??? 〈tr,s〉.
#ge #x #tr #s #e
>(exec_inf_aux_unfold …) cases x;
[ #o #k #EXEC whd in EXEC:(??%?); destruct
| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
  @is_final_elim'
  [ #r ] #FINAL #EXEC whd in EXEC:(??%?);
  destruct @refl
| #msg #EXEC whd in EXEC:(??%?); destruct
] qed.

lemma exec_e_step_inv2: ∀ge,x,tr,s,e.
  exec_inf_aux ?? clight_exec ge x = e_step ??? tr s e →
  ¬∃r.final_state s r.
#ge #x #tr #s #e
>(exec_inf_aux_unfold …) cases x;
[ #o #k #EXEC whd in EXEC:(??%?); destruct
| #y cases y; #tr' #s' whd in ⊢ (??%? → ?);
  @is_final_elim' [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F
| #msg #EXEC whd in EXEC:(??%?); destruct
] qed.

definition exec_from : genv → state → s_execution → Prop ≝
λge,s,se. single_exec_of (exec_inf_aux ?? clight_exec ge (exec_step ge s)) se.

lemma se_step_eq : ∀tr,s,e,tr',s',e'.
 se_step tr s e = se_step tr' s' e' →
 tr = tr' ∧ s = s' ∧ e = e'.
#tr #s #e #tr' #s' #e' #E destruct 
% try % @refl qed.

lemma exec_from_step : ∀ge,s,tr,s',e.
exec_from ge s (se_step tr s' e) →
exec_step ge s = Value ??? 〈tr,s'〉 ∧ exec_from ge s' e.
#ge #s0 #tr0 #s0' #e0 #H inversion H;
[ #tr #r #m #E1 #E2 destruct
| #tr #s #e #se #H1 #H2 #E (* destruct (E) ;*)
  cases (se_step_eq … E) * #E1 #E2 #E3 #E4 >E1 >E2 >E3
    >(exec_e_step_inv … H2)
    <(exec_e_step … H2) in H1; #H1 % //
| #msg #_ #E destruct
| #o #k #i #se #H1 #H2 #E destruct
] qed.

lemma exec_from_interact : ∀ge,s,o,k,i,tr,s',e.
exec_from ge s (se_interact o k i (se_step tr s' e)) →
step ge s tr s' ∧
(*exec_step ge s = Value ??? 〈tr,s'〉 ∧*) exec_from ge s' e.
#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
[ #tr #r #m #E1 #E2 destruct
| #tr #s #e #se #H1 #H2 #E destruct (E)
| #msg #_ #E destruct
| #o #k #i #se #H1 #H2 #E #X destruct (E);
    lapply (exec_step_sound ge s0);
    cases (exec_step ge s0) in H2 ⊢ %;
    [ #o' #k' >(exec_inf_aux_unfold …)
        #E' whd in E':(??%??); destruct (E');
        #STEP
        inversion H1;
        [ #tr #r #m #E1 #E2 destruct
        | #tr' #s' #e' #se' #H2 #H3 #E2 #_ destruct (E2);
            <(exec_e_step … H3) in H2; #H2 % [ 2: @H2 ]
            lapply (STEP i);
            >(exec_e_step_inv … H3)
            #S @S
        | #msg #_ #E destruct
        | #o #k #i #se #H1 #H2 #E destruct
        ]
    | #x cases x; #tr' #s' >(exec_inf_aux_unfold …)
        whd in ⊢ (??%?? → ?); @is_final_elim'
        [ #r ] #F #E whd in E:(??%??); destruct
    | #msg >(exec_inf_aux_unfold …)
        #E' whd in E':(??%??); destruct (E');
    ]
] qed.

lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.
exec_from ge s (se_interact o k i (se_stop tr r m)) →
step ge s tr (Returnstate (Vint I32 r) Kstop m).
#ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H;
[ #tr #r #m #E1 #E2 destruct
| #tr #s #e #se #H1 #H2 #E destruct (E)
| #msg #_ #E destruct
| #o #k #i #se #H1 #H2 #E #_ destruct (E);
    lapply (exec_step_sound ge s0);
    >(exec_inf_aux_unfold …) in H2;
    cases (exec_step ge s0);
    [ #o' #k'
        #E' whd in E':(??%??); destruct (E');
        #STEP
        inversion H1;
        [ #tr #r #m #E1 #E2 #_ lapply (STEP i); destruct;
            >(exec_inf_aux_unfold …) in E1;
            cases (k' i);
            [ #o2 #k2 #E whd in E:(??%??); destruct (E)
            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
                change with (is_final s2) in match (is_final ?????);
                @IFE
                [ #r' #FINAL #E whd in E:(??%??);
                    destruct (E);
                    inversion FINAL;
                    #r'' #m'' #E1 #E2 destruct (E1 E2); //;
                | #NF #E whd in E:(??%??); destruct (E)
                ]
            | #msg #E whd in E:(??%??); destruct (E)
            ]
       | #tr #s #e #e' #H #EXEC #E destruct (E)
       | #msg #EXEC #E destruct (E)
       | #o2 #k2 #i2 #e2 #H #EXEC #E destruct (E)
       ]
   | #x cases x; #tr #s whd in ⊢ (??%?? → ?);
       @is_final_elim' [ #r ] #F #E whd in E:(??%??); destruct (E)
   | #msg #E whd in E:(??%??); destruct (E)
   ]
] qed.

(* NB: the E0 in the execs are irrelevant. *)
lemma several_steps: ∀ge,tr,e,e',s,s'.
  execution_isteps tr s e s' e' →
  exec_from ge s e →
  star (mk_transrel … step) ge s tr s' ∧
  exec_from ge s' e'.
#ge #tr0 #e0 #e0' #s0 #s0' #H
elim H;
[ #s #e #EXEC % //;
| #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #STEPS #IH #EXEC
    elim (exec_from_step … EXEC); #EXEC3 #EXEC1
    elim (IH EXEC1);
    #STAR12 #EXEC2 % //;
    lapply (exec_step_sound ge s3);
    >EXEC3 #STEP3
    @(star_step (mk_transrel ?? step) … STEP3 STAR12)
    @refl
| #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #STEPS #IH #EXEC
    elim (exec_from_interact … EXEC);
    #STEP3 #EXEC1
    elim (IH EXEC1); #STAR #EXEC2
    %
    [ @(star_step (mk_transrel ?? step) … STEP3 STAR)
        @refl
    | //
    ]
] qed.

inductive execution_terminates : trace → state → s_execution → int → mem → Prop ≝
| terminates : ∀s,s',tr,tr',r,e,m.
    execution_isteps tr s e s' (se_stop tr' r m) →
    execution_terminates (tr⧺tr') s (se_step E0 s e) r m
(* We should only be able to get to here if main is an external function, which is silly. *)
| annoying_corner_case_terminates: ∀s,s',tr,tr',r,e,m,o,k,i.
    execution_isteps tr s e s' (se_interact o k i (se_stop tr' r m)) →
    execution_terminates (tr⧺tr') s (se_step E0 s e) r m.

coinductive execution_diverging : s_execution → Prop ≝
| diverging_step : ∀s,e. execution_diverging e → execution_diverging (se_step E0 s e).

(* Makes a finite number of interactions (including cost labels) before diverging. *)
inductive execution_diverges : trace → state → s_execution → Prop ≝
| diverges_diverging: ∀tr,s,s',e,e'.
    execution_isteps tr s e s' e' →
    execution_diverging e' →
    execution_diverges tr s (se_step E0 s e).

(* NB: "reacting" includes hitting a cost label. *)
coinductive execution_reacting : traceinf → state → s_execution → Prop ≝
| reacting: ∀tr,tr',s,s',e,e'.
    execution_reacting tr' s' e' →
    execution_isteps tr s e s' e' →
    tr ≠ E0 →
    execution_reacting (tr⧻tr') s e.

inductive execution_reacts : traceinf → state → s_execution → Prop ≝
| reacts: ∀tr,s,e.
    execution_reacting tr s e →
    execution_reacts tr s (se_step E0 s e).

inductive execution_goes_wrong: trace → state → s_execution → state → Prop ≝
| go_wrong: ∀tr,s,s',e,msg.
    execution_isteps tr s e s' (se_wrong msg) →
    execution_goes_wrong tr s (se_step E0 s e) s'.

let corec silent_sound ge s e
  (H0:execution_diverging e)
  (EXEC:exec_from ge s e) 
  : forever_silent (mk_transrel ?? step) … ge s ≝ ?.
cut (∃s2.∃e2.And (And (execution_diverging e2) (step ge s E0 s2)) (exec_from ge s2 e2));
[ cases H0 in EXEC ⊢ %; #s1 #e1 #H1 #EXEC
    elim (exec_from_step … EXEC);
    #EXEC0 #EXEC1
    %{ s1} %{ e1} % //; % //;
    lapply (exec_step_sound ge s); >EXEC0 whd in ⊢ (% → ?); #H @H
| *; #s2 *; #e2 *; *; #H2 #STEP2 #EXEC2
    @(forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 e2 ??))
    //;
] qed.

lemma final_step: ∀ge,tr,r,m,s.
  exec_from ge s (se_stop tr r m) →
  step ge s tr (Returnstate (Vint I32 r) Kstop m).
#ge #tr #r #m #s #EXEC
whd in EXEC;
inversion EXEC;
[ #tr' #r' #m' #EXEC' #E #_ destruct (E);
    lapply (exec_step_sound ge s);
    >(exec_inf_aux_unfold …) in EXEC';
    cases (exec_step ge s);
    [ #o #k #EXEC' whd in EXEC':(??%??); destruct (EXEC');
    | #x cases x; #tr'' #s' whd in ⊢ (??%?? → ?);
        @is_final_elim' [ #r'' #FINAL | #F ]
        #EXEC' whd in EXEC':(??%??); destruct (EXEC');
    | #msg #EXEC' whd in EXEC':(??%??); destruct (EXEC');
    ]
    inversion FINAL; #r''' #m'' #E1 #E2 #_ #H destruct (E1 E2);
    @H
| #tr' #s' #e' #se' #H #EXEC' #E destruct
| #msg #EXEC' #E destruct
| #o #k #i #e #H #EXEC #E destruct
] qed.


lemma e_stop_inv: ∀ge,x,tr,r,s.
  exec_inf_aux ?? clight_exec ge x = e_stop ??? tr r s →
  x = Value ??? 〈tr,Returnstate (Vint I32 r) Kstop (mem_of_state s)〉.
#ge #x #tr #r #s
>(exec_inf_aux_unfold …) cases x;
[ #o #k #EXEC whd in EXEC:(??%?); destruct;
| #z cases z; #tr' #s' whd in ⊢ (??%? → ?); @is_final_elim'
  [ #r' #FINAL cases FINAL; #r'' #m' #EXEC whd in EXEC:(??%?);
      destruct (EXEC); @refl
  | #F #EXEC whd in EXEC:(??%?); destruct (EXEC);
  ]
| #msg #EXEC whd in EXEC:(??%?); destruct (EXEC);
] qed.

lemma terminates_sound: ∀ge,tr,s,r,m,e.
  execution_terminates tr s (se_step E0 s e) r m →
  exec_from ge s e →
  star (mk_transrel … step) ge s tr (Returnstate (Vint I32 r) Kstop m).
#ge #tr0 #s0 #r #m #e0 #H inversion H;
[ #s #s' #tr #tr' #r' #e #m' #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC
    destruct (E1 E2 E3 E4 E5);
    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
    @(star_right … STARs')
    [ 2: @(final_step ge tr' r' m' s' … EXECs')
    | skip
    | @refl
    ]
| #s #s' #tr #tr' #r' #e #m' #o #k #i #ESTEPS #E1 #E2 #E3 #E4 #E5 #_ #EXEC
    destruct;
    cases (several_steps … ESTEPS EXEC); #STARs' #EXECs'
    @(star_right … STARs')
    [ @tr'
    | @(exec_from_interact_stop … EXECs')
    | @refl
    ]
] qed. 

let corec reacts_sound ge tr s e
  (REACTS:execution_reacting tr s e)
  (EXEC:exec_from ge s e) :
  forever_reactive (mk_transrel … step) ge s tr ≝ ?.
cut (∃s'.∃e'.∃tr'.∃tr''.(And (And (And (execution_reacting tr'' s' e') (execution_isteps tr' s e s' e')) (tr' ≠ E0)) (tr = tr'⧻tr'')));
[ inversion REACTS;
    #tr0 #tr' #s0 #s' #e0 #e' #EREACTS #ESTEPS #REACTED #E1 #E2 #E3 #_ destruct (E2 E3);
    %{ s'} %{ e'} %{ tr0} %{ tr'} % [ % [ % //; | @REACTED ] | @refl ]
| *; #s' *; #e' *; #tr' *; #tr''
    *; *; *; #REACTS' #ESTEPS #REACTED #APPTR
(*    >APPTR *)
    @(match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ])
    %
    cases (several_steps … ESTEPS EXEC); #STEPS #EXEC'
    [ 2: @STEPS
    | skip
    | @REACTED
    | @reacts_sound
      [ 2: @REACTS'
      | skip
      | @EXEC'
      ]
    ]
qed.

lemma exec_from_wrong: ∀ge,s,msg.
  exec_from ge s (se_wrong msg) →
  exec_step ge s = Wrong ??? msg.
#ge #s #msg #H whd in H;
inversion H;
[ #tr #r #m #EXEC #E destruct (E)
| #tr #s' #e #e' #H #EXEC #E destruct (E)
| #msg #EXEC #H #_ generalize in match H; -H; generalize in match EXEC; -EXEC;
  generalize in match msg; -msg; >(exec_inf_aux_unfold …)
    cases (exec_step ge s);
  [ #o #k #msg' #EXEC whd in EXEC:(??%??); destruct
  | #x cases x; #tr #s' #msg' whd in ⊢ (??%?? → ?); @is_final_elim'
      [ #r ] #F #EXEC whd in EXEC:(??%??); destruct
  | #msg1 #msg2 #EXEC #E whd in EXEC:(??%??); destruct @refl
  ]
| #o #k #i #e #H #EXEC #E destruct
] qed.

lemma exec_from_step_notfinal: ∀ge,s,tr,s',e.
  exec_from ge s (se_step tr s' e) →
  ¬(∃r. final_state s' r).
#ge #s #tr #s' #e #H whd in H; inversion H;
[ #tr' #r #m #EXEC #E destruct
| #tr' #s'' #e' #e'' #H #EXEC #E #_ destruct (E);
    >(exec_inf_aux_unfold …) in EXEC;
    cases (exec_step ge s);
    [ #o #k #EXEC whd in EXEC:(??%??); destruct
    | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?); @is_final_elim'
        [ #r ] #F #E whd in E:(??%??); destruct @F
    | #msg #E whd in E:(??%??); destruct
    ]
| #msg #EXEC #E destruct
| #o #k #i #e' #H #EXEC #E destruct
] qed.

lemma exec_from_interact_step_notfinal: ∀ge,s,o,k,i,tr,s',e.
  exec_from ge s (se_interact o k i (se_step tr s' e)) →
  ¬(∃r. final_state s' r).
#ge #s #o #k #i #tr #s' #e #H
% *; #r #F cases F in H; #r' #m #H
inversion H;
[ #tr' #r #m #EXEC #E destruct
| #tr' #s'' #e' #e'' #H #EXEC #E destruct (E);
| #msg #EXEC #E destruct
| #o' #k' #i' #e' #H #EXEC #E #_ destruct;
    >(exec_inf_aux_unfold …) in EXEC;
    cases (exec_step ge s);
    [ #o1 #k1 #EXEC1 whd in EXEC1:(??%??); destruct (EXEC1);
        inversion H;
        [ #tr1 #r1 #m1 #EXECK #E destruct (E);
        | #tr1 #s1 #e1 #e2 #H1 #EXECK #E #_ destruct (E);
            >(exec_inf_aux_unfold …) in EXECK;
            cases (k1 i');
            [ #o2 #k2 #EXECK whd in EXECK:(??%??); destruct
            | #x cases x; #tr2 #s2 whd in ⊢ (??%?? → ?);
                lapply (is_final_elim s2) #IFE whd in IFE:(∀_. ? → ? → ?%);
                change with (is_final s2) in match (is_final ?????);
                @IFE [ #r ] #F #EXECK
                whd in EXECK:(??%??); destruct;
                @(absurd ?? F)
                %{ r'} //;
            | #msg #E whd in E:(??%??); destruct
            ]
        | #msg #EXECK #E  whd in E:(??%??); destruct
        | #o2 #k2 #i2 #e2 #H2 #EXECK #E destruct
        ]
    | #x cases x; #tr1 #s1 whd in ⊢ (??%?? → ?);
        @is_final_elim' [ #r ] #F #E whd in E:(??%??); destruct;
    | #msg #E whd in E:(??%??); destruct
    ]
] qed.

lemma wrong_sound: ∀ge,tr,s,s',e.
  execution_goes_wrong tr s (se_step E0 s e) s' →
  exec_from ge s e →
  (¬∃r. final_state s r) →
  star (mk_transrel … step) ge s tr s' ∧
  nostep (mk_transrel … step) ge s' ∧
  (¬∃r. final_state s' r).
#ge #tr0 #s0 #s0' #e0 #WRONG inversion WRONG;
#tr #s #s' #e #msg #ESTEPS #E1 #E2 #E3 #E4 #_ #EXEC #NOTFINAL destruct (E1 E2 E3 E4);
cases (several_steps … ESTEPS EXEC);
#STAR #EXEC' %
[ % [ @STAR
       | #badtr #bads % #badSTEP
           lapply (step_complete … badSTEP);
           >(exec_from_wrong … EXEC')
           //;
       ]
| %
    elim ESTEPS in NOTFINAL EXEC ⊢ %;
    [ #s1 #e1 #NF #EX #F @(absurd ? F NF)
    | #e1 #e2 #tr1 #tr2 #s1 #s2 #s3 #ESTEPS1 #IH #NF #EXEC
        cases (exec_from_step … EXEC); #EXEC3 #EXEC1
        @(IH … EXEC1)
        @(exec_from_step_notfinal … EXEC)
    | #e1 #e2 #o #k #i #s1 #s2 #s3 #tr1 #tr2 #ESTEPS1 #IH #NF #EXEC
        @IH
        [ @(exec_from_interact_step_notfinal … EXEC)
        | cases (exec_from_interact … EXEC) #STEP #EF1 @EF1
        ]
    ]
] qed.

inductive execution_characterisation : state → s_execution → Prop ≝
| ec_terminates: ∀s,r,m,e,tr.
    execution_terminates tr s e r m →
    execution_characterisation s e
| ec_diverges: ∀s,e,tr.
    execution_diverges tr s e → 
    execution_characterisation s e
| ec_reacts: ∀s,e,tr.
    execution_reacts tr s e →
    execution_characterisation s e
| ec_wrong: ∀e,s,s',tr.
    execution_goes_wrong tr s e s' →
    execution_characterisation s e.

(* bit of a hack to avoid inability to reduce term in match *)
definition 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 ≝
λA,P,e. match e return λ_.Prop with [ Interact o k ⇒ P o k | _ ⇒ True ].

lemma err_does_not_interact: ∀A,B,P,e1,e2.
  (∀x:B.interact_prop A P (e2 x)) →
  interact_prop A P (bindIO ?? B A (err_to_io ??? e1) e2).
#A #B #P #e1 #e2 #H
cases e1; //; qed.

lemma err2_does_not_interact: ∀A,B,C,P,e1,e2.
  (∀x,y.interact_prop A P (e2 x y)) →
  interact_prop A P (bindIO2 ?? B C A (err_to_io ??? e1) e2).
#A #B #C #P #e1 #e2 #H
cases e1; [ #z cases z; ] //; qed.

lemma err_sig_does_not_interact: ∀A,B,P.∀Q:B→Prop.∀e1,e2.
  (∀x.interact_prop A P (e2 x)) →
  interact_prop A P (bindIO ?? (Sig B Q) A (err_to_io_sig ??? Q e1) e2).
#A #B #P #Q #e1 #e2 #H
cases e1; //; qed.

lemma opt_does_not_interact: ∀A,B,P,e1,e2,msg.
  (∀x:B.interact_prop A P (e2 x)) →
  interact_prop A P (bindIO ?? B A (opt_to_io ??? msg e1) e2).
#A #B #P #e1 #e2 #msg #H
cases e1; //; qed.

lemma exec_step_interaction:
  ∀ge,s. interact_prop ? (λo,k. ∀i.∃tr.∃s'. k i = Value ??? 〈tr,s'〉 ∧ tr ≠ E0) (exec_step ge s).
#ge #s cases s;
[ #f #st #kk #e #m cases st;
  [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
  [ 4,6,8,9: @I ]
  whd in ⊢ (???%);
  [ cases a; [ cases (fn_return f); //; | #e whd nodelta in ⊢ (???%);
                    cases (type_eq_dec (fn_return f) Tvoid); #x //; @err2_does_not_interact // ]
  | cases (find_label a (fn_body f) (call_cont kk)); [ @I | #z cases z #x #y @I ]
  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5 @I
  | 4,7: @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
  | @err2_does_not_interact #x1 #x2 cases x1; //;
  | @err2_does_not_interact #x1 #x2 @err2_does_not_interact #x3 #x4 @opt_does_not_interact #x5  @err_does_not_interact #x6 cases a;
      [ @I | #x7 @err2_does_not_interact #x8 #x9 @I ]
  | cases (is_Sskip a); #H [ @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 @I
      | @I ]
  | cases kk; [ 1,8: cases (fn_return f); //; | 2,3,5,6,7: //;
      | #z1 #z2 #z3 @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I ]
  | cases kk; //;
  | cases kk; [ 4: #z1 #z2 #z3  @err2_does_not_interact #x1 #x2 @err_does_not_interact #x3 cases x3; @I
      | *: // ]
  ]
| #f #args #kk #m cases f; 
  [ #f' whd in ⊢ (???%); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
    #x1 #x2 whd in ⊢ (???%); @err_does_not_interact //
  (* This is the only case that actually matters! *)
  | #fn #argtys #rty whd in ⊢ (???%);
      @err_does_not_interact #x1
      whd; #i % [ 2: % [ 2: % [ % whd in ⊢ (??%?); @refl
        | % #E whd in E:(??%%); destruct (E); ] ] ]
  ]
| #v #kk #m whd in ⊢ (???%); cases kk;
    [ 8: #x1 #x2 #x3 #x4 cases x1;
      [ whd in ⊢ (???%); cases v; // | #x5 whd in ⊢ (???%); cases x5;
          #x6 #x7 @opt_does_not_interact // ]
    | *: // ]
] qed.


(* Some classical logic (roughly like a fragment of Coq's library) *)
lemma classical_doubleneg:
  ∀classic:(∀P:Prop.P ∨ ¬P).
  ∀P:Prop. ¬ (¬ P) → P.
#classic #P *; #H
cases (classic P);
[ // | #H' @False_ind /2/; ]
qed.

lemma classical_not_all_not_ex:
  ∀classic:(∀P:Prop.P ∨ ¬P).
  ∀A:Type[0].∀P:A → Prop. ¬ (∀x. ¬ P x) → ∃x. P x.
#classic #A #P *; #H
@(classical_doubleneg classic) % *; #H'
@H #x % #H'' @H' %{x} @H''
qed.

lemma classical_not_all_ex_not:
  ∀classic:(∀P:Prop.P ∨ ¬P).
  ∀A:Type[0].∀P:A → Prop. ¬ (∀x. P x) → ∃x. ¬ P x.
#classic #A #P *; #H
@(classical_not_all_not_ex classic A (λx.¬ P x))
% #H' @H #x @(classical_doubleneg classic)
@H'
qed.

lemma not_ex_all_not:
  ∀A:Type[0].∀P:A → Prop. ¬ (∃x. P x) → ∀x. ¬ P x.
#A #P *; #H #x % #H'
@H %{ x} @H'
qed.

lemma not_imply_elim:
  ∀classic:(∀P:Prop.P ∨ ¬P).
  ∀P,Q:Prop. ¬ (P → Q) → P.
#classic #P #Q *; #H
@(classical_doubleneg classic) % *; #H'
@H #H'' @False_ind @H' @H''
qed.

lemma not_imply_elim2:
  ∀P,Q:Prop. ¬ (P → Q) → ¬ Q.
#P #Q *; #H % #H'
@H #_ @H'
qed.

lemma imply_to_and:
  ∀classic:(∀P:Prop.P ∨ ¬P).
  ∀P,Q:Prop. ¬ (P → Q) → P ∧ ¬Q.
#classic #P #Q #H %
[ @(not_imply_elim classic P Q H)
| @(not_imply_elim2 P Q H)
] qed.

lemma not_and_to_imply:
  ∀classic:(∀P:Prop.P ∨ ¬P).
  ∀P,Q:Prop. ¬ (P ∧ Q) → P → ¬Q.
#classic #P #Q *; #H #H'
% #H'' @H % //;
qed.

inductive execution_not_over : s_execution → Prop ≝
| eno_step: ∀tr,s,e. execution_not_over (se_step tr s e)
| eno_interact: ∀o,k,tr,s,e,i. execution_not_over (se_interact o k i (se_step tr s e)).

lemma eno_stop: ∀tr,r,m. execution_not_over (se_stop tr r m) → False.
#tr0 #r0 #m0 #H inversion H;
[ #tr #s #e #E destruct
| #o #k #tr #s #e #i #E destruct
] qed.

lemma eno_wrong: ∀msg. execution_not_over (se_wrong msg) → False.
#msg #H inversion H;
[ #tr #s #e #E destruct
| #o #k #tr #s #e #i #E destruct
] qed.

let corec show_divergence s e
 (NONTERMINATING:∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
                 execution_not_over e1)
 (UNREACTIVE:∀tr2,s2,e2. execution_isteps tr2 s e s2 e2 → tr2 = E0)
 (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))
 : execution_diverging e ≝ ?.
lapply (NONTERMINATING E0 s e ?); //;
cases e in UNREACTIVE NONTERMINATING CONTINUES ⊢ %;
[ #tr #i #m #_ #_ #_ #ENO elim (eno_stop … ENO);
| #tr #s' #e' #UNREACTIVE lapply (UNREACTIVE tr s' e' ?);
  [ <(E0_right tr) in ⊢ (?%????);
      @isteps_one @isteps_none
  | #TR @(match sym_eq ??? TR with [ refl ⇒ ? ]) (* >TR in UNREACTIVE ⊢ % *)
      #NONTERMINATING #CONTINUES #_ %
      @(show_divergence s')
      [ #tr1 #s1 #e1 #S @(NONTERMINATING tr1 s1 e1)
        change with (Eapp E0 tr1) in ⊢ (?%????); @isteps_one
        @S
      | #tr2 #s2 #e2 #S >TR in UNREACTIVE; #UNREACTIVE @(UNREACTIVE tr2 s2 e2)
          change with (Eapp E0 tr2) in ⊢ (?%????);
          @isteps_one @S
      | #tr2 #s2 #o #k #i #e2 #S @(CONTINUES tr2 s2 o k i)
          change with (Eapp E0 tr2) in ⊢ (?%????);
          @(isteps_one … S)
      ]
  ]
| #msg #_ #_ #_ #ENO elim (eno_wrong … ENO);
| #o #k #i #e' #UNREACTIVE #NONTERMINATING #CONTINUES #_
    lapply (CONTINUES E0 s o k i e' (isteps_none …));
    *; #tr' *; #s' *; #e' *; #EXEC #NOTSILENT
    @False_ind @(absurd ?? NOTSILENT)
    @(UNREACTIVE … s' e')
    <(E0_right tr') in ⊢ (?%????);
    >EXEC
    @isteps_interact //;
] qed.

lemma se_inv: ∀e1,e2.
  single_exec_of e1 e2 →
  match e1 with
  [ e_stop tr r s ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ mem_of_state s = m' | _ ⇒ False ]
  | e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2' | _ ⇒ False ]
  | e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True | _ ⇒ False ]
  | e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e | _ ⇒ False ]
  ].
#e01 #e02 #H
cases H;
[ #tr #r #s whd; % [ % ] //
| #tr #s #e1' #e2' #H' whd; % [ % ] //
| #msg whd; //
| #o #k #i #e #H' whd; % [ % ] //
] qed.

lemma interaction_is_not_silent: ∀ge,o,k,i,tr,s,s',e.
  exec_from ge s (se_interact o k i (se_step tr s' e)) →
  tr ≠ E0.
#ge #o #k #i #tr #s #s' #e whd in ⊢ (% → ?); >(exec_inf_aux_unfold …)
lapply (exec_step_interaction ge s);
cases (exec_step ge s);
[ #o' #k' ; whd in ⊢ (% → ?%? → ?); #H #K cases (se_inv … K);
    *; #E1 #E2 #H1 destruct (E1);
    lapply (H i); *; #tr' *; #s'' *; #K' #TR
    >E2 in H1; #H1 whd in H1:(?%?); >K' in H1;
    >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?);
    change with (is_final s'') in match (is_final ?????);
    @is_final_elim
    [ #r #F whd in ⊢ (?%? → ?); #S
        @False_ind @(absurd ? S) cases (se_inv … S)
    | #NF #S whd in S:(?%?); cases (se_inv … S);
        *; #E1 #E2 #S' <E1 @TR
    ]
| #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?);
    @is_final_elim' [ #r ] #F #E whd in E:(?%?);
    inversion E;
    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
    | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct
    | 3,7: #msg #E destruct
    | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct
    ]
| #msg #_ #E whd in E:(?%?); 
    inversion E;
    [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct
    | 2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct
    | 3,7: #msg #E1 #E2 destruct
    | 4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct
    ]
] qed.

let corec reactive_traceinf' ge s e
  (EXEC:exec_from ge s e)
  (REACTIVE: ∀tr,s1,e1.
    execution_isteps tr s e s1 e1 →
    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
  : traceinf' ≝ ?.
lapply (REACTIVE E0 s e (isteps_none …));
*; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H
%{ tr ? H}
@(reactive_traceinf' ge s' e' ?)
[ cases (several_steps … STEPS EXEC); #_ #H' @H'
| #tr1 #s1 #e1 #STEPS1
    @REACTIVE
    [ 2:
        @(isteps_trans … STEPS STEPS1)
    | skip
    ]
]
qed.

(* A slightly different version of the above, to work around a problem with the
   next result. *)
let corec reactive_traceinf'' ge s e
  (EXEC:exec_from ge s e)
  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
  (REACTIVE: ∀tr,s1,e1.
    execution_isteps tr s e s1 e1 →
    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
  : traceinf' ≝ ?.
cases REACTIVE0; #x cases x; #tr #y cases y; #s' #e' *; #STEPS #H
%{ tr ? H}
@(reactive_traceinf'' ge s' e' ?)
[ cases (several_steps … STEPS EXEC); #_ #H' @H'
| @(REACTIVE … STEPS)
| #tr1 #s1 #e1 #STEPS1
    @REACTIVE
    [ 2:
        @(isteps_trans … STEPS STEPS1)
    | skip
    ]
] qed.

(* We want to prove

lemma show_reactive : ∀ge,s.
  ∀REACTIVE:∀tr,s1,e1.
    execution_isteps tr s (exec_inf_aux ge (exec_step ge s)) s1 e1 →
    Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0.
  execution_reacting (traceinf_of_traceinf' (reactive_traceinf' ge s REACTIVE)) s (exec_inf_aux ge (exec_step ge s)).
  
but the current matita won't unfold reactive_traceinf' so that we can do case
analysis on (REACTIVE …).  Instead we take an "applied" version of REACTIVE that
we can do case analysis on, then get it into the desired form afterwards.
*)
let corec show_reactive' ge s e
  (EXEC:exec_from ge s e)
  (REACTIVE0: Σx.execution_isteps (\fst x) s e (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0)
  (REACTIVE: ∀tr1,s1,e1.
    execution_isteps tr1 s e s1 e1 →
    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0))
  : execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC REACTIVE0 REACTIVE)) s e ≝ ?.
(*>(unroll_traceinf' (reactive_traceinf'' …)) *)
@(match sym_eq ??? (unroll_traceinf' (reactive_traceinf'' …)) with [ refl ⇒ ? ])
cases REACTIVE0;
#x cases x; #tr1 #y cases y; #s1 #e1 #z cases z; #STEPS #NOTSILENT
whd in ⊢ (?(?%)??);
(*>(traceinf_traceinfp_app …) *)
@(match sym_eq ??? (traceinf_traceinfp_app …) with [ refl ⇒ ? ])
@(reacting … STEPS NOTSILENT)
@show_reactive'
qed.

lemma show_reactive : ∀ge,s,e.
  ∀EXEC:exec_from ge s e.
  ∀REACTIVE:∀tr,s1,e1.
    execution_isteps tr s e s1 e1 →
    (Σx.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0).
  execution_reacting (traceinf_of_traceinf' (reactive_traceinf'' ge s e EXEC ? REACTIVE)) s e.
[ #ge #s #e #EXEC #REACTIVE
    @show_reactive'
| @(REACTIVE … (isteps_none …))
] qed.

lemma execution_characterisation_complete:
  ∀classic:(∀P:Prop.P ∨ ¬P).
  ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P).
   ∀ge,s,e.
   exec_from ge s e →
   execution_characterisation s (se_step E0 s e).
#classic #constructive_indefinite_description #ge #s #e #EXEC
cases (classic (∀tr1,s1,e1. execution_isteps tr1 s e s1 e1 →
                 execution_not_over e1));
[ #NONTERMINATING
    cases (classic (∃tr,s1,e1. execution_isteps tr s e s1 e1 ∧
                     ∀tr2,s2,e2. execution_isteps tr2 s1 e1 s2 e2 → tr2 = E0));
  [ *; #tr *; #s1 *; #e1 *; #INITIAL #UNREACTIVE
      @(ec_diverges … s ? tr)
      @(diverges_diverging … INITIAL)
      @(show_divergence s1 e1)
      [ #tr2 #s2 #e2 #S @(NONTERMINATING (Eapp tr tr2) s2 e2)
          @(isteps_trans … INITIAL S)
      | #tr2 #s2 #e2 #S @(UNREACTIVE … S)
      | #tr2 #s2 #o #k #i #e2 #STEPS
          lapply (NONTERMINATING (Eapp tr tr2) s2 (se_interact o k i e2) ?);
          [ @(isteps_trans … INITIAL STEPS) ]
          #NOTOVER inversion NOTOVER;
          [ #tr' #s' #e' #E destruct (E);
          | #o' #k' #tr' #s' #e' #i' #E #_ destruct (E);
              %{ tr'} %{s'} %{e'} % //;
              cases (several_steps … INITIAL EXEC); #_ #EXEC1
              cases (several_steps … STEPS EXEC1); #_ #EXEC2
              @(interaction_is_not_silent … EXEC2)
          ]
      ]

  | *; #NOTUNREACTIVE
      cut (∀tr,s1,e1.execution_isteps tr s e s1 e1 →
            ∃x.execution_isteps (\fst x) s1 e1 (\fst (\snd x)) (\snd (\snd x)) ∧ (\fst x) ≠ E0);
      [ #tr #s1 #e1 #STEPS
          @(classical_doubleneg classic) % #NOREACTION
          @NOTUNREACTIVE
          %{ tr} %{s1} %{e1} % //;
          #tr2 #s2 #e2 #STEPS2
          lapply (not_ex_all_not … NOREACTION); #NR1
          lapply (not_and_to_imply classic … (NR1 〈tr2,〈s2,e2〉〉)); #NR2
          @(classical_doubleneg classic)
          @NR2 normalize //
      | #REACTIVE
          @ec_reacts
          [ 2: @reacts
                   @(show_reactive ge s … EXEC)
                   #tr #s1 #e1 #STEPS
                   @constructive_indefinite_description
                   @(REACTIVE … tr s1 e1 STEPS)
          | skip
          ]
      ]
  ]
 
| #NOTNONTERMINATING lapply (classical_not_all_ex_not classic … NOTNONTERMINATING);
    *; #tr #NNT2 lapply (classical_not_all_ex_not classic … NNT2);
    *; #s' #NNT3 lapply (classical_not_all_ex_not classic … NNT3);
    *; #e #NNT4 elim (imply_to_and classic … NNT4);
    cases e;
    [ #tr' #r #m #STEPS #NOSTEP
        @(ec_terminates s r m ? (Eapp tr tr')) %
        [ @s'
        | @STEPS
        ]
    | #tr' #s'' #e' #STEPS *; #NOSTEP @False_rect_Type0
        @NOSTEP //
    | #msg #STEPS #NOSTEP
        @(ec_wrong ? s s' tr) % //;
    (* The following is stupidly complicated when most of the cases are impossible.
       It ought to be simplified. *)
    | #o #k #i #e' #STEPS #NOSTEP
        cases e' in STEPS NOSTEP;
        [ #tr' #r #m #STEPS #NOSTEP
            @(ec_terminates s ???)
           [ 4: @(annoying_corner_case_terminates … STEPS) ]
        | #tr1 #s1 #e1 #STEPS *; #NOSTEP
            @False_ind @NOSTEP //
        | #msg #STEPS #NOSTEP
            lapply (exec_step_interaction ge s');
            cases (several_steps … STEPS EXEC); #_
            whd in ⊢ (% → ?);
            >(exec_inf_aux_unfold …)
            cases (exec_step ge s');
            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
                cases (H i); #tr1 *; #s1 *; #K #E >K in H2;
                >(exec_inf_aux_unfold …)
                whd in ⊢ (?%? → ?); @is_final_elim [ #r ]
                #F #S whd in S:(?%?); cases (se_inv … S);
            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
                cases (se_inv … S);
            | #msg #S cases (se_inv … S);
            ]
        | #o1 #k1 #i1 #e1 #STEPS #NOSTEP
            lapply (exec_step_interaction ge s');
            cases (several_steps … STEPS EXEC); #_
            whd in ⊢ (% → ?);
            >(exec_inf_aux_unfold …)
            cases (exec_step ge s');
            [ #o1 #k1 #EXEC' #H whd in EXEC':(?%?) H;
                cases (se_inv … EXEC'); *; #E1 #E2 #H2 destruct (E1 E2); normalize in H2;
                cases (H i); #tr1 *; #s1 *; #K #E >K in H2;
                >(exec_inf_aux_unfold …)
                whd in ⊢ (?%? → ?); @is_final_elim [ #r ]
                #F #S whd in S:(?%?); cases (se_inv … S);
            | #x cases x; #tr' #s' whd in ⊢ (?%? → ?);
                @is_final_elim' [ #r ] #F #S whd in S:(?%?);
                cases (se_inv … S);
            | #msg #S cases (se_inv … S);
            ]
        ]
    ]
]
qed.    

inductive execution_matches_behavior: s_execution → program_behavior → Prop ≝
| emb_terminates: ∀s,e,tr,r,m.
    execution_terminates tr s e r m →
    execution_matches_behavior e (Terminates tr r)
| emb_diverges: ∀s,e,tr.
    execution_diverges tr s e → 
    execution_matches_behavior e (Diverges tr)
| emb_reacts: ∀s,e,tr.
    execution_reacts tr s e →
    execution_matches_behavior e (Reacts tr)
| emb_wrong: ∀e,s,s',tr.
    execution_goes_wrong tr s e s' →
    execution_matches_behavior e (Goes_wrong tr)
| emb_initially_wrong: ∀msg.
    execution_matches_behavior (se_wrong msg) (Goes_wrong E0).

lemma exec_state_terminates: ∀tr,tr',s,s',e,r,m.
  execution_terminates tr s (se_step tr' s' e) r m → s = s'.
#tr #tr' #s #s' #e #r #m #H inversion H;
[ #s1 #s2 #tr1 #tr2 #r' #e' #m' #H' #E1 #E2 #E3 #E4 #E5 #_ destruct; @refl
| #s1 #s2 #tr1 #tr2 #r' #e' #m' #o #k #i #H' #E1 #E2 #E3 #E4 #E5 #_ destruct; @refl
] qed.

lemma exec_state_diverges: ∀tr,tr',s,s',e.
  execution_diverges tr s (se_step tr' s' e) → s = s'.
#tr #tr' #s #s' #e #H inversion H;
#tr1 #s1 #s2 #e1 #e2 #H' #E1 #E2 #E3 #E4 #_ destruct; @refl qed.

lemma exec_state_reacts: ∀tr,tr',s,s',e.
  execution_reacts tr s (se_step tr' s' e) → s = s'.
#tr #tr' #s #s' #e #H inversion H;
#tr1 #s1 #e1 #H' #E1 #E2 #E3 #_ destruct; @refl qed.

lemma exec_state_wrong: ∀tr,tr',s,s',s'',e.
  execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'.
#tr #tr' #s #s' #s'' #e #H inversion H;
#tr1 #s1 #s2 #e1 #msg #H' #E1 #E2 #E3 #E4 #_ destruct; @refl qed.

lemma behavior_of_execution: ∀s,e.
  execution_characterisation s e →
  ∃b:program_behavior. execution_matches_behavior e b.
#s0 #e0 #exec
cases exec;
[ #s #r #m #e #tr #TERM
    %{ (Terminates tr r)}
    @(emb_terminates … TERM)
| #s #e #tr #DIV
    %{ (Diverges tr)}
    @(emb_diverges … DIV)
| #s #e #tr #REACTS
    %{ (Reacts tr)}
    @(emb_reacts … REACTS)
| #e #s #s' #tr #WRONG
    %{ (Goes_wrong tr)}
    @(emb_wrong … WRONG)
] qed.

lemma initial_state_not_final: ∀ge,s.
  initial_state ge s →
  ¬ ∃r.final_state s r.
#ge #s #H cases H;
#b #f #ge #m #E1 #E2 #E3 #E4 % *; #r #H2
inversion H2;
#r' #m' #E5 #E6 destruct (E5);
qed.

lemma initial_step: ∀ge,s,e.
  exec_inf_aux ?? clight_exec ge (Value ??? 〈E0,s〉) = e →
  ¬(∃r.final_state s r) →
  ∃e'.e = e_step ??? E0 s e'.
#ge #s #e >(exec_inf_aux_unfold …)
whd in ⊢ (??%? → ?); @is_final_elim'
[ #r #FINAL #EXEC #NOTFINAL
    @False_ind @(absurd ?? NOTFINAL)
    %{r} @FINAL
| #F1 #EXEC #F2 whd in EXEC:(??%?); % [ 2: <EXEC @refl ]
qed.

theorem exec_inf_equivalence:
  ∀classic:(∀P:Prop.P ∨ ¬P).
  ∀constructive_indefinite_description:(∀A:Type[0]. ∀P:A→Prop. (∃x. P x) → Sig A P).
  ∀p,e. single_exec_of (exec_inf ?? clight_fullexec p) e →
   ∃b.execution_matches_behavior e b ∧ exec_program p b.
#classic #constructive_indefinite_description #p #e
whd in ⊢ (?%? → ??(λ_.?(?%?)%));
lapply (make_initial_state_sound p)
lapply (the_initial_state p)
whd in ⊢ (? → ? → ?(match % with [_ ⇒ ? | _ ⇒ ?])? → ?);
cases (make_initial_state p)
[ #s #INITIAL' #INITIAL whd in INITIAL ⊢ (?%? → ?);
    >exec_inf_aux_unfold
    whd in ⊢ (?%? → ?);
    @is_final_elim'
    [ #r #F @False_ind
        @(absurd ?? (initial_state_not_final … INITIAL))
        %{r} @F
    | #NOTFINAL whd in ⊢ (?%? → ?); cases e;
        [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
        cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC'
    lapply (behavior_of_execution ??
              (execution_characterisation_complete classic constructive_indefinite_description ? s ? EXEC'));
        *; #b #MATCHES %{b} % [ @MATCHES ]
        #ge #Ege
        inversion MATCHES;
        [ #s0 #e1 #tr1 #r #m #TERM #EXEC #BEHAVES <EXEC in TERM;
            #TERM
            lapply (exec_state_terminates … TERM); #E1
            >E1 in TERM; #TERM #_
            @(program_terminates (mk_transrel … step) ?? ge s)
            [ 2: @INITIAL
            | 3: <Ege @(terminates_sound … TERM EXEC')
            | skip
            | //;
            ]
        | #s0 #e #tr #DIVERGES #EXEC #E2 <EXEC in DIVERGES; #DIVERGES
            lapply (exec_state_diverges … DIVERGES);
            #E1 >E1 in DIVERGES; #DIVERGES #_
            inversion DIVERGES; #tr' #s1 #s2 #e1 #e2 #INITSTEPS #DIVERGING #E4 #E5 #E6
            <E4 in INITSTEPS ⊢ %; <E5 in E6 ⊢ %; #E6 #INITSTEPS
            cut (e0 = e1); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
            #E7 <E7 in INITSTEPS; #INITSTEPS
            cases (several_steps … INITSTEPS EXEC'); #INITSTAR #EXECDIV #_
            @(program_diverges (mk_transrel … step) ?? ge s … INITIAL)
            [ 2: <Ege @INITSTAR
            | 3: <Ege @(silent_sound … DIVERGING EXECDIV)
            ]
        | #s0 #e #tr #REACTS #EXEC #E2 <EXEC in REACTS; #REACTS
            lapply (exec_state_reacts … REACTS);
            #E1 >E1 in REACTS; #REACTS #_
            inversion REACTS; #tr' #s' #e'' #REACTING #E4 #E5
            <E4 in REACTING ⊢ %; <E5 #REACTING #E6
            cut (e0 = e''); [ destruct (E6) skip (MATCHES EXEC0 EXEC'); // ]
            #E7 <E7 in REACTING; #REACTING #_
            @(program_reacts (mk_transrel … step) ?? ge s … INITIAL)
            <Ege @(reacts_sound … REACTING EXEC')
        | #e #s1 #s2 #tr #WRONG #EXEC #E2 <EXEC in WRONG; #WRONG
            lapply (exec_state_wrong … WRONG);
            #E1 >E1 in WRONG; #WRONG #_
            inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7
            <E4 in GOESWRONG ⊢ %; <E5 <E7 #GOESWRONG
            cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ]
            #E8 <E8 in GOESWRONG; #GOESWRONG
            elim (wrong_sound … WRONG EXEC' NOTFINAL); *; #STAR #STOP #FINAL
            <Ege #_
            @(program_goes_wrong (mk_transrel … step) ?? ? s … INITIAL STAR STOP)
            #r % #F @(absurd ?? FINAL) %{r} @F
        | #msg #E destruct (E);
        ]
   ]
| #msg whd in ⊢ ((∀_.? → %) → ?);
    #NOINIT #_ #EXEC
    %{ (Goes_wrong E0)} %
    [ whd in EXEC:(?%?);
        cases e in EXEC;
        [ #tr #r #m #EXEC0 | #tr #s' #e0 #EXEC0 | #msg #EXEC0 | #o #k #i #e #EXEC0 ]
        cases (se_inv … EXEC0);
        @emb_initially_wrong
    | #ge #Ege
        @program_goes_initially_wrong
        #s % #INIT cases (NOINIT s INIT); #ge' #H @H
    ]
] qed.