include "utilities/extralib.ma".
include "common/IOMonad.ma".
include "common/Integers.ma".
include "common/Events.ma".

record trans_system (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
{ global : Type[1]
; state  : global → Type[0]
; is_final : ∀g. state g → option int
; step : ∀g. state g → IO outty inty (trace×(state g))
}.

let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:trans_system outty inty)
               (g:global ?? exec) (s:state ?? exec g)
 : IO outty inty (trace × (state ?? exec g)) ≝
match n with
[ O ⇒ Value ??? 〈E0, s〉
| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
         ! 〈tn,sn〉 ← repeat n' ?? exec g s1;
         Value ??? 〈t1⧺tn,sn〉
].

(* We take care here to check that we're not at the final state.  It is not
   necessarily the case that a success step guarantees this (e.g., because
   there may be no way to stop a processor, so an infinite loop is used
   instead). *)
inductive plus (O) (I) (TS:trans_system O I) (ge:global … TS) : state … TS ge → trace → state … TS ge → Prop ≝
| plus_one : ∀s1,tr,s2.
    is_final … TS ge s1 = None ? →
    step … TS ge s1 = OK … 〈tr,s2〉 →
    plus … ge s1 tr s2
| plus_succ : ∀s1,tr,s2,tr',s3.
    is_final … TS ge s1 = None ? →
    step … TS ge s1 = OK … 〈tr,s2〉 →
    plus … ge s2 tr' s3 →
    plus … ge s1 (tr⧺tr') s3.

lemma plus_not_final : ∀O,I,FE. ∀gl,s,tr,s'.
  plus O I FE gl s tr s' →
  is_final … FE gl s = None ?.
#O #I #FE #gl #s0 #tr0 #s0' * //
qed.

let rec trace_map (A,B:Type[0]) (f:A → res (trace × B))
                  (l:list A) on l : res (trace × (list B)) ≝
match l with
[ nil ⇒ OK ? 〈E0, [ ]〉
| cons h t ⇒
    do 〈tr,h'〉 ← f h;
    do 〈tr',t'〉 ← trace_map … f t;
    OK ? 〈tr ⧺ tr',h'::t'〉
].

(* A third version of making several steps (!)

   The idea here is to have a computational definition of reducing serveral
   steps then showing some property about the resulting trace and state.  By
   careful use of let rec we can ensure that reduction stops in a sensible
   way whenever the number of steps or the step currently being executed is
   not (reducible to) a value.
   
   An invariant is also asserted on every intermediate state (i.e., everything
   other than the first and last states).

   For example, we state a property to prove by something like

     ∃n. after_n_steps n … clight_exec ge s inv (λtr,s'. <some property>)

   then start reducing by giving the number of steps and reducing the
   definition

     %{3} whd

   and then whenever the reduction gets stuck, the currently reducing step is
   the third subterm, which we can reduce and unblock with (for example)
   rewriting

     whd in ⊢ (??%?); >EXe'

   and at the end reduce with whd to get the property as the goal.

   There are a few inversion-like results to get back the information contained in
   the proof below, and other that provides all the steps in an inductive form
   in Executions.ma.

  *)

record await_value_stuff : Type[2] ≝ {
 avs_O : Type[0];
 avs_I : avs_O → Type[0];
 avs_exec : trans_system avs_O avs_I;
 avs_g : global ?? avs_exec;
 avs_inv : state ?? avs_exec avs_g → bool
}.

let rec await_value (avs:await_value_stuff)
 (v:IO (avs_O avs) (avs_I avs) (trace × (state ?? (avs_exec avs) (avs_g avs))))
 (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop) on v : Prop ≝
match v with
[ Value ts ⇒ P (\fst ts) (\snd ts)
| _ ⇒ False
].

let rec assert (b:bool) (P:Prop) on b ≝
if b then P else False.

let rec assert_nz (n:nat) (b:bool) (P:Prop) on n ≝
match n with
[ O ⇒ P
| _ ⇒ assert b P
].

let rec after_aux (avs:await_value_stuff)
  (n:nat) (s:state ?? (avs_exec avs) (avs_g avs)) (tr:trace)
  (P:trace → state ?? (avs_exec avs) (avs_g avs) → Prop)
on n : Prop ≝
match n with
[ O ⇒ P tr s
| S n' ⇒
  match is_final … s with
  [ None ⇒ 
    await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s.
      assert_nz n' (avs_inv avs s) (after_aux avs n' s (tr ⧺ tr') P))
  | _ ⇒ False
  ]
].

lemma assert_nz_lift : ∀n,b,P,Q.
  (P → Q) →
  assert_nz n b P →
  assert_nz n b Q.
* [ /2/ | #n * [ normalize /2/ | #P #Q #_ * ] ]
qed.

definition after_n_steps : nat →
 ∀O,I. ∀exec:trans_system O I. ∀g:global ?? exec.
 state ?? exec g →
 (state ?? exec g → bool) →
 (trace → state ?? exec g → Prop) → Prop ≝
λn,O,I,exec,g,s,inv,P. after_aux (mk_await_value_stuff O I exec g inv) n s E0 P.

lemma after_aux_covariant : ∀avs,P,Q,tr'.
  (∀tr,s. P (tr'⧺tr) s → Q tr s) →
  ∀n,s,tr.
  after_aux avs n s (tr'⧺tr) P →
  after_aux avs n s tr Q.
#avs #P #Q #tr' #H #n elim n
[ normalize /2/
| #n' #IH #s #tr
  whd in ⊢ (% → %); cases (is_final … s) [ 2: #x * ]
  whd in ⊢ (% → %);
  cases (step … s) [1,3: normalize /2/ ]
  * #tr'' #s''
  whd in ⊢ (% → %);
  @assert_nz_lift
  >Eapp_assoc @IH
] qed.

lemma after_n_covariant : ∀n,O,I,exec,g,P,inv,Q.
  (∀tr,s. P tr s → Q tr s) →
  ∀s.
  after_n_steps n O I exec g s inv P →
  after_n_steps n O I exec g s inv Q.
normalize /3/
qed.

(* for joining a couple of these together *)

lemma after_n_m : ∀n,m,O,I,exec,g,inv,P,Q,s,s'.
  after_n_steps m O I exec g s' inv Q →
  (notb (eqb m 0) → inv s') →
  after_n_steps n O I exec g s inv (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) →
  after_n_steps (n+m) O I exec g s inv P.
#n #m #O #I #exec #g #inv #P #Q whd in ⊢ (? → ? → ? → ? → % → %); generalize in match E0; elim n
[ #tr #s #s' #H #INVs' whd in ⊢ (% → %); * #E destruct #H2
  whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %;
  generalize in match s; -s
  elim m
  [ #s #tr' whd in ⊢ (% → %); @H2
  | #m' #IH #s #tr' whd in ⊢ (% → %);
    cases (is_final … s) [2: #r * ]
    whd in ⊢ (% → %);
    cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %);
    @assert_nz_lift
    >Eapp_assoc @IH ]
| #n' #IH #tr #s #s' #H #INVs' whd in ⊢ (% → %);
  cases (is_final … s) [2: #r * ]
  whd in ⊢ (% → %);
  cases (step O I exec g s) [1,3: normalize // ]
  * #tr1 #s1 whd in ⊢ (% → %);
  cases n' in IH H ⊢ %; [ cases m in INVs' ⊢ %;
    [ #Is' #IH #H @IH [ // | * #H cases (H (refl ??)) ]
    | #m' #Is' #IH #H * #E destruct >Is' [ #X @(IH … H) [ @Is' | % // @X ] | % #E destruct ] ] ]
  #n'' #IH #H
  cases (inv s1) [2:*]
  @IH assumption
] qed.

(* Inversion lemmas. *)

lemma assert_nz_inv : ∀n,b,P.
  assert_nz n b P →
  (n = 0 ∨ bool_to_Prop b) ∧ P.
* [ /3/ | #n * [ #P #p % /2/ @p | #P * ] ]
qed.

lemma after_1_of_n_steps : ∀n,O,I,exec,g,inv,P,s.
  after_n_steps (S n) O I exec g s inv P →
  ∃tr,s'.
  is_final … exec g s = None ? ∧
  step … exec g s = Value … 〈tr,s'〉 ∧
  (notb (eqb n 0) → bool_to_Prop (inv s')) ∧
  after_n_steps n O I exec g s' inv (λtr'',s''. P (tr⧺tr'') s'').
#n #O #I #exec #g #inv #P #s
whd in ⊢ (% → ?);
cases (is_final … s)
[ whd in ⊢ (% → ?);
  cases (step … s)
  [ #o #k *
  | * #tr #s' whd in ⊢ (% → ?); #ASSERT cases (assert_nz_inv … ASSERT) * #H #AFTER
    %{tr} %{s'} % [1,3: % [1,3: /2/ | *: >H /4 by notb_Prop, absurd, nmk, I/ ] |*: /2/ ] 
  | #m *
  ]
| #r *
] qed.

lemma after_1_step : ∀O,I,exec,g,inv,P,s.
  after_n_steps 1 O I exec g s inv P →
  ∃tr,s'. is_final … exec g s = None ? ∧ 
    step ?? exec g s = Value … 〈tr,s'〉 ∧
    P tr s'.
#O #I #exec #g #inv #P #s #AFTER
cases (after_1_of_n_steps … AFTER)
#tr * #s' * * * #NF #STEP #INV #FIN %{tr} %{s'} % [%] // whd in FIN; >E0_right in FIN; //
qed.

(* A typical way to use the following:

   With a hypothesis
     EX : after_n_steps n ... (State ...) ...
   reduce it [whd in EX;] to
     EX : await_value ... 
   then perform inversion
   [cases (await_value_bind_inv … EX) -EX * #x * #E1 #EX]
      x : T
     E1 : f = return x
     EX : await_value ...
 *)

lemma await_value_bind_inv : ∀avs,T,f,g,P.
  await_value avs (m_bind … f g) P →
  ∃x:T. (f = return x) ∧ await_value avs (g x) P.
#avs #T *
[ #o #k #g #P *
| #x #g #P #AWAIT %{x} % //
| #m #g #P *
] qed.

(* A (possibly non-terminating) execution.   *)
coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
| e_stop : trace → int → state → execution state output input
| e_step : trace → state → execution state output input → execution state output input
| e_wrong : errmsg → execution state output input
| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.

(* This definition is slightly awkward because of the need to provide resumptions.
   It records the last trace/state passed in, then recursively processes the next
   state. *)

let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
                       (exec:trans_system output input) (g:global ?? exec)
                       (s:IO output input (trace×(state ?? exec g)))
                       : execution ??? ≝
match s with
[ Wrong m ⇒ e_wrong ??? m
| Value v ⇒ let 〈t,s'〉 ≝ v in 
    match is_final ?? exec g s' with
    [ Some r ⇒ e_stop ??? t r s'
    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
].

lemma execution_cases: ∀o,i,s.∀e:execution s o i.
 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
 | e_step tr s e ⇒ e_step ??? tr s e
 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
#o #i #s #e cases e; [1: #T #I #M % | 2: #T #S #E % | 3: #E %
 | 4: #O #I % ] qed. (* XXX: assertion failed: superposition.ml when using auto
  here, used reflexivity instead *)

axiom exec_inf_aux_unfold: ∀o,i,exec,g,s. exec_inf_aux o i exec g s =
match s with
[ Wrong m ⇒ e_wrong ??? m
| Value v ⇒ let 〈t,s'〉 ≝ v in
    match is_final ?? exec g s' with
    [ Some r ⇒ e_stop ??? t r s'
    | None ⇒ e_step ??? t s' (exec_inf_aux ??? g (step ?? exec g s')) ]
| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? g (k' v))
].
(*
#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
[ #o #k
| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
| ] 
whd in ⊢ (??%%); //;
qed.
*)

lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r.
  exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' →
  step … ge s = Value … 〈tr, s'〉 ∧
  is_final … s' = Some ? r.
#O #I #TS #ge #s #s' #tr #r
>exec_inf_aux_unfold
cases (step … ge s)
[ 1,3: normalize #H1 #H2 try #H3 destruct
| * #tr' #s''
  whd in ⊢ (??%? → ?);
  lapply (refl ? (is_final … s''))
  cases (is_final … s'') in ⊢ (???% → %);
  [ #_ whd in ⊢ (??%? → ?); #E destruct
  | #r' #E1 #E2 whd in E2:(??%?);  destruct % //
  ]
] qed.

lemma extract_step : ∀O,I,TS,ge,s,s',tr,e.
  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
  step … ge s = Value …  〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s').
#O #I #TS #ge #s #s' #tr #e
>exec_inf_aux_unfold
cases (step … s)
[ 1,3: normalize #H1 #H2 try #H3 destruct
| * #tr' #s''
  whd in ⊢ (??%? → ?);
  cases (is_final … s'')
  [ #E normalize in E; destruct /2/
  | #r #E normalize in E; destruct
  ]
] qed.

lemma extract_interact : ∀O,I,TS,ge,s,o,k.
  exec_inf_aux O I TS ge (step … ge s) = e_interact … o k →
  ∃k'. step … ge s = Interact … o k' ∧ k = (λv. exec_inf_aux ??? ge (k' v)).
#O #I #TS #ge #s #o #k >exec_inf_aux_unfold
cases (step … s)
[ #o' #k' normalize #E destruct %{k'} /2/
| * #x #y normalize cases (is_final ?????) normalize
  #X try #Y destruct
| normalize #m #E destruct
] qed.

lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e.
  exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e →
  is_final … s' = None ?.
#O #I #TS #ge #s #s' #tr #e
>exec_inf_aux_unfold
cases (step … s)
[ 1,3: normalize #H1 #H2 try #H3 destruct
| * #tr' #s''
  whd in ⊢ (??%? → ?);
  lapply (refl ? (is_final … s''))
  cases (is_final … s'') in ⊢ (???% → %);
  [ #F whd in ⊢ (??%? → ?); #E destruct @F
  | #r' #_ #E whd in E:(??%?);  destruct
  ]
] qed.



record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝
{ program : Type[0]
; es1 :> trans_system outty inty
; make_global : program → global ?? es1
; make_initial_state : ∀p:program. res (state ?? es1 (make_global p))
}.

definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx (make_global … fx p)) o i ≝
λo,i,fx,p.
  match make_initial_state ?? fx p with 
  [ OK s ⇒ exec_inf_aux ?? fx (make_global … fx p) (Value … 〈E0,s〉)
  | Error m ⇒ e_wrong ??? m
  ].




definition execution_prefix : Type[0] → Type[0] ≝ λstate. list (trace × state).

let rec split_trace O I (state:Type[0]) (x:execution state O I) (n:nat) on n : option (execution_prefix state × (execution state O I)) ≝
match n with
[ O ⇒ Some ? 〈[ ], x〉
| S n' ⇒
  match x with
  [ e_step tr s x' ⇒
    ! 〈pre,x''〉 ← split_trace ?? state x' n';
    Some ? 〈〈tr,s〉::pre,x''〉
    (* Necessary for a measurable trace at the end of the program *)
  | e_stop tr r s ⇒
    match n' with
    [ O ⇒ Some ? 〈[〈tr,s〉], x〉
    | _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ]
].

(* For now I'm doing this without I/O, to keep things simple.  In the place I
   intend to use it (the definition of measurable subtraces, and proofs using
   that) I should allow I/O for the prefix.
   
   If the execution has the form
   
     s1 -tr1→ s2 -tr2→ … sn -trn→ s'
   
   then the function returns
   
     〈[〈s1,tr1〉; 〈s2,tr2〉; …; 〈sn,trn〉], s'〉
   *)

let rec exec_steps (n:nat) O I (fx:fullexec O I) (g:global … fx) (s:state … fx g) : res (list (state … fx g × trace) × (state … fx g)) ≝
match n with
[ O ⇒ return 〈[ ], s〉
| S m ⇒
  match is_final … fx g s with
  [ Some r ⇒ Error … (msg TerminatedEarly)
  | None ⇒
    match step … fx g s with
    [ Value trs ⇒
        ! 〈tl,s'〉 ← exec_steps m O I fx g (\snd trs);
        return 〈〈s, \fst trs〉::tl, s'〉
    | Interact _ _ ⇒ Error … (msg UnexpectedIO)
    | Wrong m ⇒ Error … m
    ]
  ]
].

(* Show that it's nice. *)

lemma exec_steps_S : ∀O,I,fx,g,n,s,trace,s''.
  exec_steps (S n) O I fx g s = OK … 〈trace,s''〉 →
  is_final … fx g s = None ? ∧
  ∃tr',s',tl.
    trace = 〈s,tr'〉::tl ∧
    step … fx g s = Value … 〈tr',s'〉 ∧
    exec_steps n O I fx g s' = OK … 〈tl,s''〉.
#O #I #fx #g #n #s #trace #s''
whd in ⊢ (??%? → ?);
cases (is_final … s)
[ whd in ⊢ (??%? → ?);
  cases (step … s)
  [ #o #i #EX whd in EX:(??%?); destruct
  | * #tr' #s' whd in ⊢ (??%? → ?); #EX %{(refl ??)}
    %{tr'} %{s'} cases (exec_steps … g s') in EX ⊢ %;
    [ * #tl #s'' #EX whd in EX:(??%?); destruct %{tl} /3/
    | #m #EX whd in EX:(??%?); destruct
    ]
  | #m #EX whd in EX:(??%?); destruct
  ]
| #r #EX whd in EX:(??%?); destruct
] qed.

lemma exec_steps_length : ∀O,I,fx,g,n,s,trace,s'.
  exec_steps n O I fx g s = OK … 〈trace,s'〉 →
  n = |trace|.
#O #I #fx #g #n elim n
[ #s #trace #s' #EX whd in EX:(??%?); destruct %
| #m #IH #s #trace #s' #EX
  cases (exec_steps_S … EX) #notfinal * #tr' * #s'' * #tl * * #Etl #Estep #steps
  >(IH … steps) >Etl %
] qed.

lemma exec_steps_nonterm : ∀O,I,fx,g,n,s,h,t,s'.
  exec_steps n O I fx g s = OK … 〈h::t,s'〉 →
  is_final … s = None ?.
#O #I #fx #g #n #s #h #t #s' #EX
lapply (exec_steps_length … EX)
#Elen destruct whd in EX:(??%?);
cases (is_final … s) in EX ⊢ %;
[ //
| #r #EX whd in EX:(??%?); destruct
] qed.

lemma exec_steps_nonterm' : ∀O,I,fx,g,n,s,h,t,s'.
  exec_steps n O I fx g s = OK … 〈h@[t], s'〉 →
  is_final … s = None ?.
#O #I #fx #g #n #s * [2: #h1 #h2] #t #s' @exec_steps_nonterm
qed.

let rec gather_trace S (l:list (S × trace)) on l : trace ≝
match l with
[ nil ⇒ E0
| cons h t ⇒ (\snd h)⧺(gather_trace S t)
].

lemma exec_steps_after_n_simple : ∀n,O,I,fx,g,s,trace,s'.
  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
  after_n_steps n O I fx g s (λ_. true) (λtr,s''. 〈tr,s''〉 = 〈gather_trace ? trace,s'〉).
#n elim n
[ #O #I #fx #g #s #trace #s' #EXEC whd in EXEC:(??%?); destruct
  whd %
| #m #IH #O #I #fx #g #s #trace #s' #EXEC
  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
  @(after_n_m 1 … (IH … STEPS)) //
  whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #E destruct %
] qed.

lemma exec_steps_after_n : ∀n,O,I,fx,g,s,trace,s',inv,P.
  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
  all ? (λstr. inv (\fst str)) (tail … trace) →
  P (gather_trace ? trace) s' →
  after_n_steps n O I fx g s inv P.
#n elim n
[ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct
  #ALL #p whd @p
| #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC
  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
  destruct 
  #ALL cut ((notb (eqb m 0) → bool_to_Prop (inv s1)) ∧ bool_to_Prop (all ? (λst. inv (\fst st)) (tail … tl)))
  [ cases m in STEPS;
    [ whd in ⊢ (??%? → ?); #E destruct % [ * #H cases (H (refl ??)) | /2/ ]
    | #m' #STEPS cases (exec_steps_S … STEPS) #_ * #tr'' * #s'' * #tl'' * * #E #_ #_ destruct
      whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; [ /2/ | * ]
    ]
  ] * #i1 #itl
  #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?))
  [ @p
  | @i1 
  | whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #p' @p'
  ]
] qed.

lemma exec_steps_after_n_noinv : ∀n,O,I,fx,g,s,trace,s',P.
  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
  P (gather_trace ? trace) s' →
  after_n_steps n O I fx g s (λ_.true) P.
#n #O #I #fx #g #s #trace #s' #P #EXEC #p
@(exec_steps_after_n … EXEC) //
cases trace // #x #trace'
elim trace' /2/
qed.

lemma exec_steps_first : ∀n,O,I,fx,g,s,s1,tr1,tl,s'.
  exec_steps n O I fx g s = OK ? 〈〈s1,tr1〉::tl,s'〉 →
  s = s1.
#n #O #I #fx #g #s #s1 #tr1 #tl #s' #EXEC
lapply (exec_steps_length … EXEC) #E normalize in E; destruct
cases (exec_steps_S … EXEC) #_ * #tr2 * #s2 * #tl2 * * #E #_ #_ destruct
%
qed. 

lemma after_n_exec_steps : ∀n,O,I. ∀fx:fullexec O I. ∀g,s,inv,P.
  after_n_steps n O I fx g s inv P →
  ∃trace,s'.
    exec_steps n O I fx g s = OK ? 〈trace,s'〉 ∧
    bool_to_Prop (all ? (λstr. inv (\fst str)) (tail … trace)) ∧
    P (gather_trace ? trace) s'.
#n elim n
[ #O #I #fx #g #s #inv #P #AFTER %{[ ]} %{s} % [ %{(refl ??)} % | @AFTER ]
| #m #IH #O #I #fx #g #s #inv #P #AFTER
  cases (after_1_of_n_steps … AFTER)
  #tr1 * #s1 * * * #NF #STEP #INV #AFTER'
  cases (IH … AFTER')
  #tl * #s' * * #STEPS #INV' #p
  %{(〈s,tr1〉::tl)} %{s'} %
  [ %
    [ whd in ⊢ (??%?); >NF whd in ⊢ (??%?); >STEP whd in ⊢ (??%?); >STEPS %
    | cases tl in STEPS INV INV' ⊢ %; [ // | * #sx #trx #t #STEPS #INV #INV'
      <(exec_steps_first … STEPS) whd in ⊢ (?%); >INV //
      >(exec_steps_length … STEPS) %
      ]
    ]
  | // ]
] qed.

lemma exec_steps_split : ∀n,m,O,I,fx,g,s,trace,s'.
  exec_steps (n+m) O I fx g s = OK ? 〈trace,s'〉 →
  ∃trace1,trace2,s1.
    exec_steps n O I fx g s = OK ? 〈trace1,s1〉 ∧
    exec_steps m O I fx g s1 = OK ? 〈trace2,s'〉 ∧    
    trace = trace1 @ trace2.
#n elim n
[ #m #O #I #fx #g #s #trace #s' #EXEC
  %{[ ]} %{trace} %{s} /3/
| #n' #IH #m #O #I #fx #g #s #trace #s' #EXEC
  cases (exec_steps_S … EXEC) #NF * #tr' * #s' * #tl * * #E1 #STEP #EXEC'
  cases (IH … EXEC') #trace1 * #trace2 * #s1 * * #EXEC1 #EXEC2 #E2
  %{(〈s,tr'〉::trace1)} %{trace2} %{s1}
  %
  [ %
    [ whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >EXEC1 % 
    | @EXEC2
    ]
  | destruct %
  ]
] qed.

lemma exec_steps_join : ∀n,m,O,I,fx,g,s1,trace1,s2,trace2,s3.
  exec_steps n O I fx g s1 = OK ? 〈trace1,s2〉 →
  exec_steps m O I fx g s2 = OK ? 〈trace2,s3〉 →
  exec_steps (n+m) O I fx g s1 = OK ? 〈trace1@trace2,s3〉.
#n elim n
[ #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2
  whd in EXEC1:(??%?); destruct @EXEC2
| #n' #IH #m #O #I #fx #g #s1 #trace1 #s2 #trace2 #s3 #EXEC1 #EXEC2
  cases (exec_steps_S … EXEC1) #NF * #tr' * #s' * #tl' * * #E1 #STEP #EXEC'
  whd in ⊢ (??%?); >NF >STEP whd in ⊢ (??%?); >(IH … EXEC' EXEC2)
  destruct %
] qed.

(* Show that it corresponds to split_trace … (exec_inf …).
   We need to adjust the form of trace. *)

let rec switch_trace_aux S tr (l:list (S × trace)) (s':S) on l : list (trace × S) ≝
match l with
[ nil ⇒ [〈tr,s'〉]
| cons h t ⇒ 〈tr,\fst h〉::(switch_trace_aux S (\snd h) t s')
].

definition switch_trace ≝
λS,l,s'. match l with
[ nil ⇒ nil ?
| cons h t ⇒ switch_trace_aux S (\snd h) t s'
].

lemma exec_steps_inf_aux : ∀O,I. ∀fx:fullexec O I. ∀g,n,s,trace,s'.
  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
  match is_final … s' with
  [ None ⇒ split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', exec_inf_aux … fx g (step … s')〉
  | Some r ⇒ n = 0 ∨ ∃tr'. split_trace … (exec_inf_aux … fx g (step … fx g s)) n = Some ? 〈switch_trace ? trace s', e_stop … tr' r s'〉
  ].
#O #I #fx #g #n elim n
[ #s #trace #s' #EX whd in EX:(??%%); destruct
  cases (is_final … s') [ % | #r %1 % ]
| #m #IH #s #trace #s' #EX
  cases (exec_steps_S … EX)
  #notfinal * #tr'' * #s'' * #tl * * #Etrace #Estep #Esteps
  cases tl in Etrace Esteps ⊢ %;
  [ #E destruct #Esteps
    lapply (exec_steps_length … Esteps) #Elen normalize in Elen; destruct
    whd in Esteps:(??%?); destruct
    >Estep
    >exec_inf_aux_unfold normalize nodelta
    cases (is_final … s')
    [ whd %
    | #r %2 %{tr''} %
    ]
  | * #s1 #tr1 #tl1 #E normalize in E; destruct #Esteps
    lapply (IH … Esteps) cases (is_final … s')
    [ normalize nodelta #IH' >Estep <(exec_steps_first … Esteps)
      >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
      >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' normalize nodelta %
    | normalize nodelta #r *
      [ #E @⊥ >(exec_steps_length … Esteps) in E; #E normalize in E; destruct
      | * #tr'' #IH' %2 %{tr''} >Estep <(exec_steps_first … Esteps)
        >exec_inf_aux_unfold whd in ⊢ (??(????%?)?);
        >(exec_steps_nonterm … Esteps) whd in ⊢ (??%?); >IH' %
      ]
    ]
  ]
] qed.