include "Clight/labelSpecification.ma".
include "Clight/CexecInd.ma".

(* Useful for breaking up the labeling functions, because we don't care about
   *which* cost labels are added here and so can throw away the resulting name
   generator. *)
lemma shift_fst : ∀A,B,C,D:Type[0].∀e:A×B.∀F:A → C.∀G:B → D.
  \fst (let 〈x,y〉 ≝ e in 〈F x, G y〉) =  F (\fst e).
#A #B #C #D * //
qed.


(* Similarly, lemma to break up label_expr, label_exprs and label_statement in
   the labelling functions *)
lemma label_gen_elim : ∀Syn:Type[0].∀syn,u.∀T:Type[0].∀L:Syn → universe CostTag → Syn × (universe CostTag). ∀F:Syn → universe CostTag → T. ∀P:T → Type[0].
  (∀u'. P (F (\fst (L syn u)) u')) →
  P (let 〈syn',u'〉 ≝ L syn u in F syn' u').
#Syn #syn #u #T #L #F #P
cases (L syn u)
#syn' #u' #H @H
qed.

lemma add_cost_expr_elim : ∀e,u.∀T:Type[0].∀F:expr → universe CostTag → T. ∀P:T → Type[0].
  (∀u',l. P (F (Expr (Ecost l e) (typeof e)) u')) →
  P (let 〈e',u'〉 ≝ add_cost_expr e u in F e' u').
#e #u #T #F #P #H whd in match (add_cost_expr ??);
cases (fresh ??) #l #u' @H
qed.


lemma label_expr_type : ∀e,u.
  typeof (\fst (label_expr e u)) = typeof e.
* #e #ty #u >shift_fst //
qed.

(* Lemmas about trace_with_extra_labels *)

lemma twel_refl : ∀tr. trace_with_extra_labels tr tr.
#tr elim tr /2/
qed.

lemma twel_app : ∀tr1,tr2,tr1',tr2'.
  trace_with_extra_labels tr1 tr1' →
  trace_with_extra_labels tr2 tr2' →
  trace_with_extra_labels (tr1⧺tr2) (tr1'⧺tr2').
#tr1 #tr2 #tr1' #tr2' #twel1 elim twel1 /3/
qed.  


theorem label_expr_ok : ∀ge,ge',en,m.
  related_globals … label_fundef ge ge' →
  (∀e,v,tr.
   exec_expr ge en m e = OK … 〈v,tr〉 →
   ∀u. ∃tr'. exec_expr ge' en m (\fst (label_expr e u)) = OK … 〈v,tr'〉 ∧ 
             trace_with_extra_labels tr tr') ∧
  (∀e,ty,b,o,tr. exec_lvalue' ge en m e ty = OK … 〈〈b,o〉,tr〉 →
          ∀u. ∃tr'. exec_lvalue' ge' en m (\fst (label_expr_descr e u ty)) ty = OK … 〈〈b,o〉,tr'〉 ∧
                    trace_with_extra_labels tr tr').
(* Proof goes by breaking up the execution in the hypothesis, breaking up the
   labelling function to get a new term and executing it by rewriting what we
   learned from the hypothesis. *)
#ge #ge' #en #m #RG @expr_lvalue_ind_combined
[ 1,2: normalize /3 by ex_intro, conj/
| * //
 [ #id #ty #IH #v #tr #EX #u
   cases (bind_inversion ????? EX) -EX * * #b #o #tr1 * #EX1 #EX
   cases (bind_inversion ????? EX) -EX #v2 * #EX2 #EX
   normalize in EX; destruct
   cases (IH … EX1 u) #tr1' * #EX1' #T1
   %{(tr1')} % [ whd in ⊢ (??%?); >EX1' whd in ⊢ (??%?); >EX2 @refl | // ]
 | #e1 #ty #IH #v #tr #EX #u
   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
   normalize in EXrem; destruct
   cases (IH … EX1 u) #tr1' * #EX1' #twel1
   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' whd in ⊢ (?(??%?)?); >EX1'
   whd in ⊢ (?(??%?)?); >EXl /2/
 | #e1 #id #ty #IH #v #tr #EX #u
   cases (bind_inversion ????? EX) * * #b #o #tr1 * #EX1 #EX1r
   cases (bind_inversion ????? EX1r) #v * #EXl #EXrem
   normalize in EXrem; destruct
   cases (IH … EX1 u) #tr1' * #EX1' #twel1
   %{tr1'} >shift_fst in EX1'; >shift_fst >shift_fst #EX1' % // whd in ⊢ (??%?); >EX1'
   whd in ⊢ (??%?); >EXl @refl
 ]
| #v #ty #b #o #tr #EX #u %{tr} % [
    whd in EX:(??%?) ⊢ (??%?); cases (lookup ??? v) in EX ⊢ %;
    [ whd in ⊢ (??%? → ??%?); >(rg_find_symbol … RG) //
    | #b // ]
  | // ]
| #e1 #ty #IH #b #o #tr #EX #u
  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
  cases (IH … EX1 u) #tr1' * #EX1' #twel1
  %{tr1'} >shift_fst whd in ⊢ (?(??%?)?); >EX1'
  whd in ⊢ (?(??%?)?);
  cases v1 in EX1rem ⊢ %; normalize #A try #B try #C destruct /2/
| #ty' #e1 #ty #IH #v #tr #EX #u
  cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
  cases (IH … EX1 u) #tr1' * #EX1' #twel1
  %{tr1'} >shift_fst >shift_fst >shift_fst whd in ⊢ (?(??%?)?); 
  whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EX1'
  whd in ⊢ (?(??%?)?); 
  cases ty' in EX1rem ⊢ %;
  [ 4: #r #ty' whd in ⊢ (??%? → ?(??%?)?); cases (pointer_compat_dec b1 r)
       #pc normalize #E destruct /2/
  | *: normalize #A try #B try #C try #D destruct
  ]
| #ty #op #e1 #IH #v #tr #EX #u
  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EXrem
  normalize in EXrem; destruct
  cases (IH … EX1 u) #tr1' * #EX1' #twel1
  %{tr1'} % // >shift_fst 
  whd in ⊢ (??(????(?(???%)?))?);
  @label_gen_elim #u2
  whd in ⊢ (??%?); >EX1'
  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
| #ty #op #e1 #e2 #IH1 #IH2 #v #tr #EX
  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
  cases (bind_inversion ????? EX1rem) * #v2 #tr2 * #EX2 #EX2rem
  cases (bind_inversion ????? EX2rem) #v' * #EXop #EXop'
  #u
  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
  >shift_fst
  whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
  @label_gen_elim #u2
  cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
  @label_gen_elim #u3 %{(tr1'⧺tr2')}
  whd in ⊢ (?(??%?)?); >EX1'
  whd in ⊢ (?(??%?)?); >EX2'
  whd in ⊢ (?(??%?)?); >label_expr_type >label_expr_type >EXop
  normalize in EXop'; destruct % /2/
| #ty #ty' #e1 #IH #v #tr #EX #u 
  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
  cases (bind_inversion ????? EX1rem) #v2 * #EX2 #EX2rem
  normalize in EX2rem; destruct
  cases (IH … EX1 u) #tr1' * #EX1' #twel1
  %{tr1'} % // >shift_fst >shift_fst
  whd in ⊢ (??%?); >EX1' 
  whd in ⊢ (??%?); >label_expr_type >EX2 @refl
| #ty #e1 #e2 #e3 #IH1 #IH2 #IH3 #v #tr #EX #u
  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
  cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
  normalize in EX2rem; destruct
  cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
  @label_gen_elim #u2
  @label_gen_elim #u3
  @add_cost_expr_elim #u4 #l4
  @label_gen_elim #u5
  @add_cost_expr_elim #u6 #l6
  [ cases (IH2 … EX2 u2) | cases (IH3 … EX2 u4) ] #trx' * #EXx' #twelx
  [ %{(tr1'⧺trx'⧺(Echarge l4))} | %{(tr1'⧺trx'⧺(Echarge l6))} ]
  whd in ⊢ (?(??%?)?); >EX1'
  whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
  whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?); >EXx' 
  normalize % // @twel_app // <(E0_right tr2) @twel_app /2/
| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
  @label_gen_elim #u2
  @label_gen_elim #u3
  @add_cost_expr_elim #u4 #l4
  @add_cost_expr_elim #u5 #l5
  [ cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
    -EX1rem -EXguardrem -EX2rem
    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l4)}
    whd in ⊢ (?(??%?)?); >EX1'
    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
    whd in EX3rem:(??%%) ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ]
  | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    %{(tr1'⧺E0⧺Echarge l5)}
    whd in ⊢ (?(??%?)?); >EX1'
    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
    whd in EXguardrem:(??%%); destruct % // <(E0_right tr) @twel_app /2/
  ]
| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
  cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
  @label_gen_elim #u2
  @add_cost_expr_elim #u4 #l4
  @label_gen_elim #u3
  @add_cost_expr_elim #u5 #l5
  [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    %{(tr1'⧺Echarge l4)}
    whd in ⊢ (?(??%?)?); >EX1'
    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
    whd in EXguardrem:(??%%) ⊢ %; destruct % // <(E0_right tr) /3/
  | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
    cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    cases (IH2 … EX2 u4) #tr2' * #EX2' #twel2
    %{(tr1'⧺(tr2'⧺E0)⧺Echarge l5)}
    whd in ⊢ (?(??%?)?); >EX1'
    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
    whd in EX3rem:(??%%) ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/
  ]
| #ty #ty' #v #tr normalize /3/
| #ty #e1 #ty' #id #IH #b #o #tr #EX #u cases ty' in IH EX ⊢ %;
  [ 7: #id #fl #IH #EX
    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
    cases (bind_inversion ????? EX1rem) #n * #EXoff #EXoffrem
    whd in EXoffrem:(???%); destruct >shift_fst >shift_fst
    cases (IH … EX1 u) #tr1' * #EX1' #twel1
    %{tr1'} % //
    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
    whd in ⊢ (??%?); >EXoff whd in ⊢ (??%?); @refl
  | 8: #id #fl #IH #EX
    cases (bind_inversion ????? EX) * * #b1 #o1 #tr1 * #EX1 #EX1rem
    whd in EX1rem:(???%); destruct >shift_fst >shift_fst
    cases (IH … EX1 u) #tr1' * #EX1' #twel1
    %{tr1'} % //
    whd in ⊢ (??%?); whd in ⊢ (??(match % with [_⇒?|_⇒?])?); >EX1'
    whd in ⊢ (??%?); @refl
  | *: normalize #A #B try #C try #D try #F destruct
  ]
| #ty #l #e1 #IH #v #tr #EX #u
  cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
  whd in EX1rem:(???%); destruct
  cases (IH … EX1 u) #tr1' * #EX1' #twel1 %{(tr1'@Echarge l)}
  >shift_fst >shift_fst whd in ⊢ (?(??%?)?); >EX1' 
  whd in ⊢ (?(??%?)?); /3/
| #e1 #ty #NLV #b #o #tr #EX @⊥
  cases e1 in NLV EX; normalize //
  #A #B #C try #D try #F destruct
] qed.

lemma label_exprs_ok : ∀ge,ge'.
   related_globals … label_fundef ge ge' →
   ∀en,m,es,vs,tr.
   exec_exprlist ge en m es = OK … 〈vs,tr〉 →
   ∀u. ∃tr'. exec_exprlist ge' en m (\fst (label_exprs es u)) = OK … 〈vs,tr'〉 ∧ 
             trace_with_extra_labels tr tr'.
#ge #ge' #RG #en #m #es elim es
[ #vs #tr #EX whd in EX:(??%?); destruct #u %{E0} /2/
| #e #tl #IH #vs #tr #EX
  cases (bind_inversion ????? EX) -EX * #v1 #tr1 * #EX1 #EX
  cases (bind_inversion ????? EX) -EX * #tl' #tr' * #EX2 #EX
  whd in EX:(??%%); destruct
  #u whd in match (label_exprs ??); @label_gen_elim #u' >shift_fst
  cases (proj1 ?? (label_expr_ok ge ge' en m RG) ??? EX1 u) #tr1' * #EX1' #T1
  cases (IH … EX2 u') #tr'' * #EX2' #T2
  % [2: % [ whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
    whd in ⊢ (??%?); >EX2' in ⊢ (??%?); @refl
  | /2/ ] | skip ]
] qed.


(* Now we move on to describe the simulation relation.  First, relate the
   continuations. *)
inductive cont_with_labels : cont → cont → Prop ≝
| cwl_stop : cont_with_labels Kstop Kstop
| cwl_seq : ∀u,s,k,k'. cont_with_labels k k' → cont_with_labels (Kseq s k) (Kseq (\fst (label_statement s u)) k')
| cwl_while : ∀ue,e,us,s,cs,cpost,k,k'.
    cont_with_labels k k' →
    cont_with_labels (Kwhile e s k) (Kwhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
| cwl_dowhile : ∀ue,e,us,s,cs,cpost,k,k'.
    cont_with_labels k k' →
    cont_with_labels (Kdowhile e s k) (Kdowhile (\fst (label_expr e ue)) (Scost cs (\fst (label_statement s us))) (Kseq (Scost cpost Sskip) k'))
| cwl_for1 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'.
    cont_with_labels k k' →
    cont_with_labels (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2)))) (Kseq (Scost cpost Sskip) k'))
| cwl_for2 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor2 e s1 s2 k) (Kfor2 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
| cwl_for3 : ∀ue,e,us1,s1,us2,s2,cs,cpost,k,k'. cont_with_labels k k' → cont_with_labels (Kfor3 e s1 s2 k) (Kfor3 (\fst (label_expr e ue)) (\fst (label_statement s1 us1)) (Scost cs (\fst (label_statement s2 us2))) (Kseq (Scost cpost Sskip) k'))
| cwl_switch : ∀k,k'. cont_with_labels k k' → cont_with_labels (Kswitch k) (Kswitch k')
| cwl_call : ∀r,f,en,k,k'. cont_with_labels k k' → cont_with_labels (Kcall r f en k) (Kcall r (label_function f) en k')
| cwl_seqls : ∀ls,u,k,k'. cont_with_labels k k' →
    cont_with_labels (Kseq (seq_of_labeled_statement ls) k) (Kseq (seq_of_labeled_statement (\fst (label_lstatements ls u))) k').

lemma call_cont_with_labels : ∀k,k'.
  cont_with_labels k k' →
  cont_with_labels (call_cont k) (call_cont k').
#k0 #k0' #K elim K /2/
qed.

(* Now define almost all of the simulation relation... *)
inductive state_with_labels_partial : state → state → Prop ≝
| swl_state : ∀f,us,s,k,k',e,m. cont_with_labels k k' → state_with_labels_partial (State f s k e m) (State (label_function f) (\fst (label_statement s us)) k' e m)
(* Extra matching states that we can reach that don't quite correspond to the
   labelling function *)
| swl_whilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    state_with_labels_partial (State f (Swhile a s) k e m) (State (label_function f) (Swhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
| swl_dowhilestate : ∀f,ua,a,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    state_with_labels_partial (State f (Sdowhile a s) k e m) (State (label_function f) (Sdowhile (\fst (label_expr a ua)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
| swl_forstate : ∀f,ua2,a2,us3,s3,us,s,cs,cpost,k,k',e,m. cont_with_labels k k' →
    state_with_labels_partial (State f (Sfor Sskip a2 s3 s) k e m) (State (label_function f) (Sfor Sskip (\fst (label_expr a2 ua2)) (\fst (label_statement s3 us3)) (Scost cs (\fst (label_statement s us)))) (Kseq (Scost cpost Sskip) k') e m)
(* and the rest *)
| swl_callstate : ∀fd,args,k,k',m. cont_with_labels k k' → state_with_labels_partial (Callstate fd args k m) (Callstate (label_fundef fd) args k' m)
| swl_returnstate : ∀res,k,k',m. cont_with_labels k k' → state_with_labels_partial (Returnstate res k m) (Returnstate res k' m)
| swl_finalstate : ∀r. state_with_labels_partial (Finalstate r) (Finalstate r)
.

(* ... and add the states where the cases from switch statements are expanded.
   We do these separately because in the LSdefault case we have to execute a
   cost label alongside an arbitrary statement, and we want to reuse the result
   on arbitrary statements we get for state_with_labels_partial. *)
inductive state_with_labels : state → state → Prop ≝
| swl_partial : ∀s,s'. state_with_labels_partial s s' → state_with_labels s s'
| swl_switchstate : ∀f,u,ls,k,k',e,m. cont_with_labels k k' →
    state_with_labels (State f (seq_of_labeled_statement ls) k e m)
                      (State (label_function f) (seq_of_labeled_statement (\fst  (label_lstatements ls u))) k' e m)
. 

(* TODO: this (or something like it) ought to be elsewhere. *)
inductive plus (ge:genv) : state → trace → state → Prop ≝
| plus_one : ∀s1,tr,s2. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s1 tr s2
| plus_succ : ∀s1,tr,s2,tr',s3. exec_step ge s1 = OK … 〈tr,s2〉 → plus ge s2 tr' s3 → plus ge s1 (tr⧺tr') s3.

(* Some details are invariant under labelling. *)
lemma label_function_return : ∀f.
  fn_return (label_function f) = fn_return f.
* #rty #params #vars #body
whd in ⊢ (??(?%)?);
cases (label_statement ??) #body' #u'
whd in ⊢ (??(?%)?);
cases (add_cost_before ??) #body'' #u''
//
qed.

lemma label_expr_fun_typeof : ∀a,u.
  fun_typeof (\fst (label_expr a u)) = fun_typeof a.
#a #u whd in ⊢ (??%?); >label_expr_type @refl
qed.

lemma label_fundef_typeof_fundef : ∀fd.
  type_of_fundef (label_fundef fd) = type_of_fundef fd.
* //
* #rty #args #vars #body
normalize cases (label_statement ??) #body' #u
normalize cases (fresh ??) //
qed.

lemma label_fn_params : ∀f.
  fn_params (label_function f) = fn_params f.
* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
qed.

lemma label_fn_vars : ∀f.
  fn_vars (label_function f) = fn_vars f.
* #rty #params #vars #s whd in ⊢ (??(?%)?); @breakup_pair @breakup_pair //
qed.

(* Some annoying rewrite rules *)
lemma exec_lvalue_labelled : ∀ge,e,m,a,ty,u.
  exec_lvalue ge e m (\fst (label_expr (Expr a ty) u)) =
  exec_lvalue' ge e m (\fst (label_expr_descr a u ty)) ty.
#ge #e #m #a #ty #u
whd in ⊢ (??(????(???%))?); >shift_fst @refl
qed.

lemma opt_find_funct : ∀ge,ge',m,vf,fd.
  related_globals … label_fundef ge ge' →
  opt_to_io io_out io_in … m (find_funct … ge vf) = Value … fd →
  opt_to_io io_out io_in … m (find_funct … ge' vf) = Value … (label_fundef fd).
#ge #ge' #m #vf #fd #RG
lapply (rg_find_funct … RG … vf fd)
cases (find_funct … vf)
[ #_ #E normalize in E; destruct
| #fd' #H #E normalize in E; destruct >(H (refl ??)) //
] qed.

lemma labelled_not_skip : ∀s,u.
  s ≠ Sskip →
  (\fst (label_statement s u)) ≠ Sskip.
* #u
[ * #H cases (H (refl ??))
| *: #a try #b try #c try #d try #e
     (* Use the state-monad-like structure of the labelling function to break
        it up *)
     whd in match (label_statement ??);
     repeat @(breakup_pair ???? (λx.\fst x ≠ Sskip))
     % #E destruct
] qed.

lemma labelled_is_not_skip : ∀s,u.
  s ≠ Sskip →
  ∃pf. is_Sskip (\fst (label_statement s u)) = inr … pf.
#s #u #NE
cases (is_Sskip ?)
[ #E @⊥ @(absurd ? E) @labelled_not_skip //
| /2/
] qed.

lemma label_select_ls : ∀sz,i,ls,u.
  ∃u'.
    select_switch sz i (\fst (label_lstatements ls u)) =
    \fst (label_lstatements (select_switch sz i ls) u').
#sz #i #ls @(labeled_statements_ind … ls)
[ #s #u % [2: whd in match (label_lstatements ??);
  @label_gen_elim #u1 >shift_fst @refl | skip ]
| #sz' #i' #s #tl #IH #u
  whd in match (label_lstatements ??);
  whd in match (select_switch ?? (LScase ????));
  @intsize_eq_elim_elim
  [ #NE
    @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
    cases (IH u2)
    #u4 #E %{u4} whd in ⊢ (??%?);
    >intsize_eq_elim_false //
  | #E <E in i' ⊢ %; #i' whd
    @eq_bv_elim
    [ #Ei >Ei
      %{u}
      whd in match (label_lstatements (if ? then ? else ?) ?);
      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
      whd in ⊢ (??%?);
      >intsize_eq_elim_true
      >eq_bv_true
      @refl
    | #NEi
      @label_gen_elim #u1 @label_gen_elim #u2 @label_gen_elim #u3
       whd in ⊢ (??(λ_.??%?));
       >intsize_eq_elim_true
       >eq_bv_false //
    ]
  ]
] qed.

(* Break up labelling function in one go for statements. *)
lemma blindly_label : ∀u,s. ∀P:statement → Prop.
match s with
[ Sskip ⇒ P Sskip
| Sassign e1 e2 ⇒ ∀u1,u2. P (Sassign (\fst (label_expr e1 u1)) (\fst (label_expr e2 u2)))
| Scall eo e args ⇒ ∀u1,u2,u3. P (Scall (\fst (label_opt_expr eo u1)) (\fst (label_expr e u2)) (\fst (label_exprs args u3))) 
| Ssequence s1 s2 ⇒ ∀u1,u2. P (Ssequence (\fst (label_statement s1 u1)) (\fst (label_statement s2 u2)))
| Sifthenelse e s1 s2 ⇒ ∀u1,u2,u3,c2,c3. P (Sifthenelse (\fst (label_expr e u1)) (Scost c2 (\fst (label_statement s1 u2))) (Scost c3 (\fst (label_statement s2 u3))))
| Swhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Swhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
| Sdowhile e s1 ⇒ ∀u1,u2,cs,cpost. P (Ssequence (Sdowhile (\fst (label_expr e u1)) (Scost cs (\fst (label_statement s1 u2)))) (Scost cpost Sskip))
| Sfor s1 e s2 s3 ⇒ ∀u1,u2,u3,u4,c3,c4. P (Ssequence (Sfor (\fst (label_statement s1 u1)) (\fst (label_expr e u2)) (\fst (label_statement s2 u3)) (Scost c3 (\fst (label_statement s3 u4)))) (Scost c4 Sskip))
| Sbreak ⇒ P Sbreak
| Scontinue ⇒ P Scontinue
| Sreturn eo ⇒ ∀u1. P (Sreturn (\fst (label_opt_expr eo u1)))
| Sswitch e ls ⇒ ∀u1,u2. P (Sswitch (\fst (label_expr e u1)) (\fst (label_lstatements ls u2)))
| Slabel l s1 ⇒ ∀u1,cs. P (Slabel l (Scost cs (\fst (label_statement s1 u1))))
| Sgoto l ⇒ P (Sgoto l)
| Scost c s1 ⇒ ∀u1. P (Scost c (\fst (label_statement s1 u1)))
] → P (\fst (label_statement s u)).  
#u * // #A #B #C try #D try #E try #F whd in match (label_statement ??);
@label_gen_elim #u1 //
@label_gen_elim #u2 //
[ 6: >shift_fst //
| *: @label_gen_elim #u3 //
     @label_gen_elim #u4
     [ @label_gen_elim #u5 >shift_fst >shift_fst //
     | 2,3: >shift_fst >shift_fst //
     | @label_gen_elim #u5 >shift_fst >shift_fst >shift_fst //
     ]
] qed.

(* Apply induction hypothesis in label_find_label proof below while getting
   Matita to infer the continuations k0 and k0', and the universe u0, rather
   than having to give them explicitly. *)
lemma lfl_IH : ∀s0,lbl.
  ∀C:option (statement×cont) → option (statement×cont) → Prop.
  ∀IH:cont → cont → universe CostTag → Prop.
  (∀k,k',u. cont_with_labels k k' → IH k k' u) →
  ∀k0,k0',u0. cont_with_labels k0 k0' →
   (IH k0 k0' u0 →
    C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0')) →
   C (find_label lbl s0 k0) (find_label lbl (\fst (label_statement s0 u0)) k0').
/3/
qed.

(* Finding a goto label in a cost-labelled program gives a labelled version of
   the statement and continuation found by the original function, if any. *)
lemma label_find_label : ∀lbl,s,k,k',u.
  cont_with_labels k k' →
  match find_label lbl s k with
  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
    ∃u',cs,k1'.
    find_label lbl (\fst (label_statement s u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
    cont_with_labels k1 k1'
  | None ⇒ find_label lbl (\fst (label_statement s u)) k' = None ?
  ].
#lbl #s @(statement_ind2 ? (λls.
  ∀k,k',u.
  cont_with_labels k k' →
  match find_label_ls lbl ls k with
  [ Some r' ⇒ let 〈s1,k1〉 ≝ r' in
    ∃u',cs,k1'.
    find_label_ls lbl (\fst (label_lstatements ls u)) k' = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
    cont_with_labels k1 k1'
  | None ⇒ find_label_ls lbl (\fst (label_lstatements ls u)) k' = None ?
  ])
 … s)
[ #k #k' #u #F @refl
| #e1 #e2 #k #k' #u #K @blindly_label #u1 #u2 whd @refl
| #e0 #e #args #k #k' #u #K @blindly_label #u1 #u2 #u3 whd @refl
| #sA #sB #IH1 #IH2 #k #k' #u #K @blindly_label #u1 #u2 whd in match (find_label ???);
  whd in match (find_label ?? k');
  @(lfl_IH sA … IH1) [ /2/ ]
  cases (find_label ???)
  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
    @(lfl_IH … IH2) [ // ]
    cases (find_label ???)
    [ whd in ⊢ (% → %); #FIND2' whd in ⊢ (??%?); >FIND1' >FIND2' @refl
    | * #s3 #k3 whd in ⊢ (% → %); * #u3 * #cs * #k1' * #FIND2' #K1'
      % [2: %{cs} %{k1'} % // whd in ⊢ (??%?); >FIND1' in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl | skip ]
    ]
  | * #sA' #kA' whd in ⊢ (% → %);
    * #u1' * #cs * #k1' * #FA' #K'
         % [2: %{cs} %{k1'} % [ whd in ⊢ (??%?); >FA' in ⊢ (??%?); @refl | // ] |skip]
  ]
| #e #s1 #s2 #IH1 #IH2 #k #k' #u @blindly_label #u1 #u2 #u3 #c2 #c3 #K
  whd in match (find_label ?? k); whd in match (find_label ?? k'); 
  whd in match (find_label ?? k');
  @(lfl_IH  … IH1) [ // ] cases (find_label ???)
  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1'
    lapply (IH2 k k' u3 K) cases (find_label ???)
    [ whd in ⊢ (% → %); #FIND2'
      whd in match (find_label ???); >FIND1'
      whd in match (find_label ???); >FIND2' @refl
    | * #s2' #k2' * #u4 * #cs * #k1' * #FIND2' #K2'
      % [2: % [2: % [2: % [ whd in ⊢ (??%?);
      whd in match (find_label ???); >FIND1' in ⊢ (??%?);
      whd in match (find_label ???); >FIND2' in ⊢ (??%?); @refl
      | // ]|skip]|skip]|skip]
    ]
  | * #s1' #k1 whd in ⊢ (% → %); * #u4 * #cs * #k1' * #FIND1' #K1'
    % [2: % [2: % [2: % [
      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
      @refl | // ] |skip ]| skip ]| skip ]
  ]
| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
  whd in match (find_label ?? k); normalize in match (find_label ?? k');
  @(lfl_IH s0 … IH) [ /2/ ]
  cases (find_label ???)
  [ whd in ⊢ (% → %); #FIND1'
    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
    % [2: % [2: % [2: % [
      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
      @refl | // ]| skip ]| skip ]| skip ]
  ]
| #e #s0 #IH #k #k' #u #K @blindly_label #u1 #u2 #cs #cpost
  whd in match (find_label ?? k); normalize in match (find_label ?? k');
  @(lfl_IH s0 … IH) [ /2/ ]
  cases (find_label ???)
  [ whd in ⊢ (% → %); #FIND1'
    whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' @refl
  | * #s1 #k1 * #u4 * #cs * #k1' * #FIND1' #K1'
    % [2: % [2: % [2: % [
      whd in ⊢ (??%?); whd in match (find_label ???); >FIND1' in ⊢ (??%?);
      @refl | // ]| skip ]| skip ]| skip ]
  ]
| #s1 #e #s2 #s3 #IH1 #IH2 #IH3 #k #k' #u #K @blindly_label #u1 #u2 #u3 #u4 #c3 #c4
  whd in match (find_label ???); normalize in match (find_label ?? k');
  @(lfl_IH s1 … IH1) [ /2/ ]
  cases (find_label ???)
  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND1' >FIND1'
    @(lfl_IH s3 … IH3) [ /2/ ]
    cases (find_label ???)
    [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND3' >FIND3'
      @(lfl_IH s2 … IH2) [ /2/ ]
      cases (find_label ???)
      [ whd in ⊢ (% → %); #FIND2' >FIND2' @refl
      | * #s2' #k2' * #u2' * #cs' * #k1' * #FIND2' #K2'
        % [2: % [2: % [2: % [
         whd in ⊢ (??%?); >FIND2' in ⊢ (??%?); @refl
        | // ]| skip ]| skip ]| skip ]
      ]
    | * #s3' #k3' * #u3' * #cs' * #k1' * #FIND3' #K3'
        % [2: % [2: % [2: % [
        >FIND3' in ⊢ (??%?); whd in ⊢ (??%?); @refl 
        | // ]| skip ]| skip ]| skip ]
    ]
  | * #s1' #k1' * #u1' * #cs' * #k1' * #FIND1' #K1'
        % [2: % [2: % [2: % [
        >FIND1' in ⊢ (??%?); whd in ⊢ (??%?); @refl 
        | // ]| skip ]| skip ]| skip ]
  ]
| //
| //
| #eo #k #k' #u @blindly_label #u1 //
| #e #ls #IH #k #k' #u #K @blindly_label #u1 #u2
  normalize in match (find_label ???); normalize in match (find_label ???);
  lapply (IH (Kswitch k) (Kswitch k') u2 ?) [/2/] cases (find_label_ls ???)
  [ whd in ⊢ (% → %); //
  | * #s1' #k1' * #u' * #cs * #k'' * #FIND' #K'
    % [2: % [2: % [2: % [ @FIND' | // ]|skip ]|skip]|skip]
  ]
| #l #s0 #IH #k #k' #u #K @blindly_label #u1 #cs
  whd in match (find_label ???); whd in match (find_label ?? k');
  cases (ident_eq lbl l)
  [ #E destruct whd
    % [2: % [2: % [2: % [ @refl | // ]|skip ]|skip ]| skip ]
  | #NE whd in ⊢ (match % with [_⇒?|_⇒?]);
    normalize in match (find_label ?? k');
    @(lfl_IH s0 … IH) [ // ]
    cases (find_label ???)
    [ //
    | * #s0' #k0' * #u' * #cs0 * #k1' * #FIND0 #K0
      % [2: % [2: % [2: % [ @FIND0 | // ]|skip ]|skip]|skip]
    ]
  ]
| //
| #l #s0 #IH #k #k' #u #K @blindly_label #u1 /2/
| #s0 #IH #k #k' #u whd in match (label_lstatements ??);
  @label_gen_elim #u1 >shift_fst >shift_fst
  whd in match (find_label_ls ???); whd in match (find_label_ls ???);
  @IH
| #sz #i #s0 #tl #IH1 #IH2 #k #k' #u #K
  whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
  @label_gen_elim #u3 >shift_fst 
  whd in match (find_label_ls ???); normalize in match (find_label_ls ?? k');
  @(lfl_IH s0 … IH1) [ /2/ ]
  cases (find_label ???)
  [ whd in ⊢ (% → match % with [_⇒?|_⇒?]); #FIND0 >FIND0
    lapply (IH2 k k' u2 K) cases (find_label_ls ???)
    [ whd in ⊢ (% → %); #FINDtl >FINDtl @refl
    | * #stl #ktl //
    ]
  | * #s0' #k0' whd in ⊢ (% → %);
    * #u' * #cs * #k1' * #FIND0 #K0 >FIND0
    % [2: % [2: % [2: % [ @refl | // ] | skip ] | skip ] | skip ]
  ]
] qed.

lemma label_find_label_fn : ∀lbl,f,k,k',s1,k1.
  cont_with_labels k k' →
  find_label lbl (fn_body f) (call_cont k) = Some ? 〈s1,k1〉 →
  ∃u',cs,k1'.
    find_label lbl (fn_body (label_function f)) (call_cont k') = Some ? 〈Scost cs (\fst (label_statement s1 u')), k1'〉 ∧
    cont_with_labels k1 k1'.
#lbl * #rty #args #vars #s #k #k' #s1 #k1 #K #FIND
whd in match (label_function ?);
@label_gen_elim #u1 @label_gen_elim #u2 >shift_fst
lapply (label_find_label lbl s (call_cont k) (call_cont k') (new_universe ?) ?)
[ /2/ ]
>FIND //
qed.


(* We show the main simulation in two stages.  First, we show it for all states
   in the relation *except* those for labeled_statements, then we'll show the
   whole thing.  This is so that we can appeal to the other cases in the proof
   for labeled_statements. *)
lemma step_with_labels_partial : ∀ge,ge'.
  related_globals … label_fundef ge ge' →
  ∀s1,s1',tr,s2.
  state_with_labels_partial s1 s1' →
  exec_step ge s1 = Value … 〈tr,s2〉 →
   ∃tr',s2'. plus ge' s1' tr' s2' ∧
             trace_with_extra_labels tr tr' ∧
             state_with_labels s2 s2'.

(* General plan is like the expressions result, except that we do case analysis
   on the simulation first, then:  break up the original execution, break up the
   cost labelling, use the earlier results to deal with expressions, then
   run the labelled version for enough steps.  We try to avoid having to write
   out the final trace and state and "skip" them afterwards. *)
#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
[ #f #us #s #k #k' #e #m #KL cases s
  [ #EX inversion KL
    [ #E1 #E2 #_ destruct %{tr}
      whd in EX:(??%?);
      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
      [ #E >E in EX; whd in ⊢ (??%% → ?); #EX' destruct %{(Returnstate Vundef Kstop (free_list m (blocks_of_env e)))}
        % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl
        | // ] | /3/ ]
      | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
      ]
    | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
      %{(State (label_function f) (\fst (label_statement s0 u)) k0' e m)}
      whd in EX:(??%%); destruct
      % [ % [ @plus_one @refl | // ] | /3/ ]
    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr}
      whd in EX:(??%%); destruct
      % [ 2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_whilestate // ] | skip ]
    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
      cases (bindIO_inversion ??????? EX) * #ve #tre * #EXe #EXrem
      cases (bindIO_inversion ??????? EXrem) * * #EXb #EXbrem -EXrem
      normalize in EXbrem; destruct
      cases ((proj1 ?? (label_expr_ok ge ge' e m RG)) ??? EXe ue) #tre' * #EXe' #Te
      [ % [ 2: % [ 2: % [ % [ @plus_one
        whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
        whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
        whd in ⊢ (??%?); @refl
        | // ]
        | @swl_partial @swl_dowhilestate // ] | skip ] | skip ]
      | % [ 2: % [ 2: % [ % [ @plus_succ [
        4: whd in ⊢ (??%?); >EXe' in ⊢ (??%?);
           whd in ⊢ (??%?); >label_expr_type >EXb in ⊢ (??%?);
           whd in ⊢ (??%?); @refl
        | skip | skip
        | 5: @plus_succ [ 4: @refl | skip | skip
        | 5: @plus_one @refl | skip ] | skip ]
        | <(E0_right tr) @twel_app /2/ ]
        | /3/ ] | skip ] | skip ]
      ]
    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
      whd in EX:(??%?); destruct
      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]
    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
      whd in EX:(??%?); destruct
      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
    | #ue #e0 #us1 #st1 #us2 #st2 #cs #cpost #k0 #k0' #K #_ #E1 #E2 #E3 destruct
      whd in EX:(??%?); destruct
      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
    | #k0 #k0' #K #_ #E1 #E2 #E3 destruct
      whd in EX:(??%?); destruct
      %{E0} % [2: % [ % [ @plus_one @refl | // ] | /4/ ] | skip ]
    | #r #f0 #en #k0 #k0' #K #_ #E1 #E2 #E3 destruct
      whd in EX:(??%?);
      lapply (refl ? (fn_return f)) cases (fn_return f) in ⊢ (???% → ?);
      [ #E >E in EX; whd in ⊢ (??%? → ?); #EX destruct
        %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?);
        @refl | // ] | /4/ ] | skip ]
      | *: #A [ 1,3,5,6,7,8: #B | 4: #B #C ] #E >E in EX; #EX whd in EX:(??%%); destruct
      ]
    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
      % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ]| skip ]| skip ]
    ]
  | * #a1 #ty1 #a2 #EX
    cases (bindIO_inversion ??????? EX) -EX * * #b1 #o1 #tr1 * #EX1 #EX
    cases (bindIO_inversion ??????? EX) -EX * #v2 #tr2 * #EX2 #EX
    cases (bindIO_inversion ??????? EX) -EX #m3 * #EX3 #EX
    whd in EX:(??%%); destruct
    cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX1 us) #tr1' * #EX1' #T1
    whd in match (label_statement ??);
    @label_gen_elim #ua1 @label_gen_elim #ua2
    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX2 ua1) #tr2' * #EX2' #T2
    % [2: % [2: % [ % [
      @plus_one whd in ⊢ (??%?);     
      >exec_lvalue_labelled >EX1' in ⊢ (??%?);
      whd in ⊢ (??%?); >EX2' in ⊢ (??%?);
      whd in ⊢ (??%?); >label_expr_type >EX3 in ⊢ (??%?);
      @refl
    | @twel_app // ] | /3/ ] | skip ] | skip ]
  | * [2: * #er #tyr ] #ef #args #EX
    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    cases (bindIO_inversion ??????? EX) -EX * #args' #tr2 * #EX2 #EX
    cases (bindIO_inversion ??????? EX) -EX #fd * #EX3 #EX
    cases (bindIO_inversion ??????? EX) -EX #E4 * #EX4 #EX
    whd in EX:(??%%);
    [ cases (bindIO_inversion ??????? EX) -EX * * #b5 #o5 #tr5 * #EX5 #EX whd in EX:(??%%); ]
    destruct
    whd in match (label_statement ??);
    whd in match (label_opt_expr ??);
    [ @(label_gen_elim … (Expr er tyr)) #u' @breakup_pair | letin u' ≝ us ]
    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 u') #tr1' * #EX1' #T1
    @label_gen_elim #u1
    @label_gen_elim #u2
    cases (label_exprs_ok ge ge' RG e m args args' ? EX2 u1) #tr2' * #EX2' #T2
    [ cases (proj2 ?? (label_expr_ok ge ge' e m RG) ????? EX5 us) #tr5' * #EX5' #T5 ]
    % [2,4: % [2,4: % [1,3: % [1,3:
      @plus_one whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX why do I need the repetition? *)
      whd in ⊢ (??%?); [ >EX2' in ⊢ (??%?); | >EX2' in ⊢ (??%?); ]
      whd in ⊢ (??%?); >(opt_find_funct … RG … EX3) in ⊢ (??%?);
      whd in ⊢ (??%?); >label_fundef_typeof_fundef >label_expr_fun_typeof [ >EX4 in ⊢ (??%?); | >EX4 in ⊢ (??%?); ]
      whd in ⊢ (??%?); [ >exec_lvalue_labelled >EX5' in ⊢ (??%?); ] 
      @refl | *: @twel_app /2/ ] | *: @swl_partial @swl_callstate /2/ ] | *: skip ] | *: skip ]
  | #st1 #st2 #EX
    whd in EX:(??%%); destruct
    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
    %{E0} % [2: % [ % [ @plus_one @refl | // ] | @swl_partial @swl_state /2/ ] | skip ]
  | #a #st1 #st2 #EX
    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
    normalize in EX; destruct
    whd in match (label_statement ??); @label_gen_elim #u1
    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
    @label_gen_elim #u5
    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
    whd in match (add_cost_before ??); cases (fresh ??) #c7 #u7
    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9:
      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] 
      whd in ⊢ (??%?); @refl
    | 1,2,6,7: skip
    | 5,10: @plus_one @refl
    | *: skip
    ]
    | 2,4: <(E0_right tr) @twel_app /2/
    ]| 2,4: /3/ ] | *: skip ] | *: skip ]
  | #a #st #EX
    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
    normalize in EX; destruct
    whd in match (label_statement ??); @label_gen_elim #u1
    @label_gen_elim #u2
    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6
    >shift_fst whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7
    >shift_fst
    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
      | 5,10: @plus_succ [ 4,9: 
      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] 
      whd in ⊢ (??%?); @refl
    | 1,2,6,7: skip
    | 5: @plus_one @refl
    | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
    | *: skip
    ]
    | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
    ]| 2,4: /4/ ] | *: skip ] | *: skip ]
  | #a #st #EX
    normalize in EX; destruct
    whd in match (label_statement ??); @label_gen_elim #u1
    @label_gen_elim #u2
    whd in match (add_cost_before ??); cases (fresh ??) #c6 #u6 >shift_fst
    whd in match (add_cost_after ??); cases (fresh ??) #c7 #u7 >shift_fst
    % [2: % [2: % [ % [ @plus_succ [ 4: @refl | 1,2: skip
      | 5: @plus_succ [ 4: @refl | 1,2: skip | 5: @plus_one // | skip ] | skip ]
      | /2/ ] | /4/ ] | skip ] | skip ]
  | #st1 #a #st2 #st #EX
    lapply (refl ? (is_Sskip st1)) cases (is_Sskip st1) in ⊢ (???% → ?); #Esk #Eskip
    whd in EX:(??%?); >Eskip in EX; #EX
    whd in match (label_statement ??); @label_gen_elim #u1
    @label_gen_elim #u2 @label_gen_elim #u3 @label_gen_elim #u4
    whd in match (add_cost_before ??); cases (fresh ??) #c5 #u5 >shift_fst
    whd in match (add_cost_after ??); cases (fresh ??) #c6 #u6 >shift_fst
    [ cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
      normalize in EX; destruct
      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
      % [2,4: % [2,4: % [1,3: % [1,3: @plus_succ [ 4,9: @refl | 1,2,6,7: skip
      | 5,10: @plus_succ [ 4,9: 
      whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] 
      whd in ⊢ (??%?); @refl
      | 1,2,6,7: skip
      | 5: @plus_one @refl
      | 10: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
      | *: skip
      ]
      | 2,4: <(E0_left tr) @twel_app // <(E0_right tr) @twel_app /2/
      ]| 2,4: /4/ ] | *: skip ] | *: skip ]
    | whd in EX:(??%%); destruct
      % [2: % [2: %[ %[ @plus_succ [ 4: @refl | 5: @plus_one
        whd in ⊢ (??%?); cases (labelled_is_not_skip ? u1 Esk) #Esk' #Eskip'
        >Eskip' whd in ⊢ (??%?); @refl | *: skip ]| // ] | @swl_partial @swl_state /2/ ]
      | skip ] | skip ]
    ]
  | #EX inversion KL
    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    ]
    whd in match (label_statement ??);
    % [2,4,6,8,10,12,14: % [2,4,6,8,10,12,14: % [1,3,5,7,9,11,13: %
    [1,11,13: @plus_one @refl | 2,12,14: //
    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
    | @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip] | /2/
    | @plus_succ [ 4: @refl | 5: @plus_succ [ 4: @refl | 5: @plus_one @refl |*:skip]|*:skip] | /2/
    ]| *: /3/ ]|*: skip]|*: skip ]
  | #EX inversion KL
    [ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    |#u #s0 #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #ue #e0 #us0 #s0 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #ue #e0 #us1 #s1 #us2 #st2 #cs #cpost #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #r #f0 #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
    ]
    whd in match (label_statement ??);
    [ 1,2,4,5,6,7: % [2,4,6,8,10,12: % [2,4,6,8,10,12: % [1,3,5,7,9,11: %
      [1,3,7,9,11: @plus_one @refl | 5: @plus_succ [4:@refl | 5:@plus_one @refl | *: skip ]
      | *: // ] | *: @swl_partial /3 by cwl_for3, swl_state, swl_whilestate/ ]| *:skip ]| *: skip ]
    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
      cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
      normalize in EX; destruct
      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ue) #tr1' * #EX1' #T1
      % [2,4: % [2,4: % [1,3: % [1,3: [ @plus_one | @plus_succ ] [ 1,5:
        whd in ⊢ (??%?); [ >EX1' in ⊢ (??%?); | >EX1' in ⊢ (??%?); ] (* XXX repeated? *)
      whd in ⊢ (??%?); >label_expr_type [ >EX2 in ⊢ (??%?); | >EX2 in ⊢ (??%?); ] 
      whd in ⊢ (??%?); @refl
      | 6: @plus_succ [ 4: @refl | 5: @plus_one @refl | *: skip ] |*: skip ]
      | // | <(E0_right tr) @twel_app /2/
      ]
      | /3/ | /3/ ] | *: skip ] | *: skip ]
    ]
  | * [2: #a ] #EX
    whd in EX:(??%?); cases (type_eq_dec (fn_return f) Tvoid) in EX;
    #Ety #EX whd in EX:(??%?);
    [ destruct
    | cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
      cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    | >Ety in EX; #EX
    | @⊥ cases (fn_return f) in Ety EX;
      [ * #H cases (H (refl ??))
      | *: normalize #a #b #c try #d try #e destruct
      ]
    ]
    whd in match (label_statement ??);
    [ @label_gen_elim #u' whd in match (label_opt_expr ??); @label_gen_elim #u'' ]
    whd in EX:(??%%); destruct
    % [2,4: % [2,4: % [1,3: %[1,3: @plus_one
      whd in ⊢ (??%?);
      [ >label_function_return @(dec_false ? (type_eq_dec ??) Ety) #Ety''
        whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
      | >label_function_return >Ety in ⊢ (??%?);
      ] whd in ⊢ (??%?); @refl
      | *: // ]| *: @swl_partial @swl_returnstate /2/ ]|*:skip]|*:skip]
  | #a #ls #EX
    cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
    cases v1 in EX1 EX;
    [ 2: #sz #i #EX1 #EX
    | *: normalize #A #B try #C destruct
    ]
    whd in EX:(??%%); destruct 
    cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 us) #tr1' * #EX1' #T1
    whd in match (label_statement ??); @label_gen_elim #u1 @label_gen_elim #u2
    % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1' in ⊢ (??%?); @refl
      | // ]| cases (label_select_ls … sz i ls u1) #u3 #Els >Els /3/
      ]|skip ]| skip ]
  | #l #st #EX
    whd in EX:(??%?); destruct
    whd in match (label_statement ??); @label_gen_elim #u1 >shift_fst
    whd in match (add_cost_before ??); cases (fresh ??) #cs #u2 >shift_fst
    %[2: %[2: %[ %[ @plus_succ
      [ 4: @refl | 5: @plus_one @refl | *: skip ]
      | /2/ ] | /3/ ] |skip ]| skip ]
  | #l #EX
    whd in EX:(??%?);
    @blindly_label whd
    lapply (refl ? (find_label l (fn_body f) (call_cont k)))
    cases (find_label ???) in ⊢ (???% → ?);
    [ #F @⊥  >F in EX; #EX whd in EX:(??%?); destruct
    | * #s1 #k1 #F >F in EX; #EX whd in EX:(??%?); destruct
      cases (label_find_label_fn … KL F)
      #u' * #cs * #k1' * #F' #K'
      % [2: %[2: %[ %[ @plus_succ
        [ 4: whd in ⊢ (??%?); >F' in ⊢ (??%?); @refl | 5: @plus_one @refl | *: skip ]
        | /2/ ] | /3/ ] | skip ] | skip ]
    ]
  | #c #st #EX whd in EX:(??%?); destruct @blindly_label #u1
    % [2: % [2: % [ % [ @plus_one @refl | // ] | /3/ ] | skip ]| skip ]
  ]
| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
  whd in EX:(??%%); destruct
  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua) #tr1' * #EX1' #T1
  [ % [2: % [2: % [ % [
    @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
               |5: @plus_one @refl | *: skip ]
    | <(E0_right tr) /3/ ]| /4/ ]| skip ]| skip ]
  | % [2: % [2: % [ % [
    @plus_succ [4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
                   whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    | 5: @plus_succ [4: @refl
    | 5: @plus_one @refl | *: skip ] | *: skip ]
    | <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip ]
  ]
| #f #ua #a #us #s #cs #cpost #k #k' #e #m #K #EX
  whd in EX:(??%%); destruct
  % [2: % [2: % [ % [
    @plus_succ [4: % | 5: @plus_one % | *: skip ]
    | /2/ ]| /4/ ]| skip ]| skip ]
| #f #ua2 #a2 #us3 #s3 #us #s #cs #cpost #k #k' #e #m #K #EX
  cases (bindIO_inversion ??????? EX) -EX * #v1 #tr1 * #EX1 #EX
  cases (bindIO_inversion ??????? EX) -EX * * #EX2 #EX
  whd in EX:(??%%); destruct
  cases (proj1 ?? (label_expr_ok ge ge' e m RG) ??? EX1 ua2) #tr1' * #EX1' #T1
  [ % [2: % [2: % [ % [
    @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    | 5: whd in ⊢ (??(??%%??)??); @plus_one @refl
    | *: skip ]| <(E0_right tr) /3/ ] | /4/ ]| skip ]| skip ]
  | % [2: % [2: % [ % [
    @plus_succ [ 4: whd in ⊢ (??%?); >EX1' in ⊢ (??%?);
                    whd in ⊢ (??%?); >label_expr_type >EX2 in ⊢ (??%?); @refl
    | 5: whd in ⊢ (??(??%%??)??); @plus_succ [4: @refl
    | 5: @plus_one @refl ]| *: skip ]| <(E0_right tr) /3/ ]| /3/ ]| skip ]| skip
    ]
  ]
| *
  [ #f #args #k #k' #m #K whd in ⊢ (??%? → ?); @pair_elim #e #m1 #EX1 #EX
    cases (bindIO_inversion ??????? EX) -EX #m2 * #EX2 #EX
    whd in EX:(??%%); destruct
    whd in match (label_fundef ?);
    whd in match (label_function ?);
    lapply (refl ? (label_function f)) whd in ⊢ (???% → ?);
    @label_gen_elim #u1 @label_gen_elim #u2 >shift_fst #Ef
    % [2: % [2: % [ % [ @plus_succ [4: whd in ⊢ (??%?); >EX1 in ⊢ (??%?);
      whd in ⊢ (??%?); >EX2 in ⊢ (??%?); @refl
    | 5: @plus_one @refl | *: skip ] | /2/ ]| <Ef @swl_partial @swl_state @K ]| skip ]| skip ]
  | #id #tys #ty #args #k #k' #m #K #EX
    cases (bindIO_inversion ??????? EX) -EX #vs * #EX1 #EX
    cases (bindIO_inversion ??????? EX) -EX #ety * #EX2 #EX
    whd in EX2:(??%%); destruct
  ]
| #res #k #k' #m #K #EX inversion K
  [ #E1 #E2 #E3 destruct cases res in EX ⊢ %;
    [ 2: * #i #EX whd in EX:(??%?); destruct
    | *: normalize #A try #B try #C destruct
    ]
    % [2: % [2: % [ % [ @plus_one @refl | // ]| /2/ ]| skip ]| skip ]
  | 9: #r #f #en #k0 #k0' #K' #_ #E1 #E2 #E3 destruct cases r in EX ⊢ %;
    [ #EX whd in EX:(??%?); destruct
      % [2: % [2: % [ % [ @plus_one @refl | // ]| /3/ ]| skip ]| skip ]
    | * * #b #o #ty #EX
      cases (bindIO_inversion ??????? EX) -EX #m2 * #EX1 #EX
      whd in EX:(??%%); destruct
      % [2: % [2: % [ % [ @plus_one whd in ⊢ (??%?); >EX1 in ⊢ (??%?); @refl | // ]| /3/ ]| skip ]| skip ]
    ]
  | *: #A #B #C #D #E #F #G try #H try #I try #J try #L try #M try #N try #O
       destruct whd in EX:(??%?); destruct
  ]
| #r #EX whd in EX:(??%%); destruct
] qed.


theorem step_with_labels : ∀ge,ge'.
  related_globals … label_fundef ge ge' →
  ∀s1,s1',tr,s2.
  state_with_labels s1 s1' →
  (exec_step ge s1 = Value … 〈tr,s2〉 →
   ∃tr',s2'. plus ge' s1' tr' s2' ∧
             trace_with_extra_labels tr tr' ∧
             state_with_labels s2 s2').
#ge #ge' #RG #Xs1 #Xs1' #tr #s2 *
[ #s1 #s1' @step_with_labels_partial //
| #f #u *
(* If we have LSdefault we need to smuggle the execution of the cost label in
   before the actual statement. *)
  [ #s #k #k' #e #m #K #EX
    whd in EX:(??(??(??%???))?);
    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
    >shift_fst whd in match (seq_of_labeled_statement ?);
    cases (step_with_labels_partial … RG (State f s k e m) (State (label_function f) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
    #tr' * #s2' * * #P #T #S
    % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @P | *: skip ] | /2/ ]| @S ]| skip ]| skip ]
(* but for LScase it's just like the cases in step_with_labels_partial *)
  | #sz #i #s #ls #k #k' #e #m #K #EX
    whd in EX:(??(??(??%???))?);
    whd in match (label_lstatements ??); @label_gen_elim #u1 @label_gen_elim #u2
    @label_gen_elim #u3 >shift_fst whd in match (seq_of_labeled_statement ?);
    whd in EX:(??%?); destruct
    % [2: % [2: % [ % [ @plus_succ [4: @refl | 5: @plus_one @refl | *: skip ] | /2/ ]| /4/ ]| skip ]| skip ]
  ]    
] qed.


lemma exec_step_interaction:
  ∀ge,s,o,k. exec_step ge s = Interact … o k  →
  ∃f,argtys,retty,vargs,k',m. s = Callstate (CL_External f argtys retty) vargs k' m.
#ge #s cases s
[ #f #st #kk #e #m #o #k #EX @⊥ cases st in EX ⊢ %;
  [ 11,14: #a | 2,4,6,7,12,13,15: #a #b | 3,5: #a #b #c | 8: #a #b #c #d ]
  whd in ⊢ (??%? → ?);
  [ 4,6,8,9: #EX destruct ]
  [ cases a 
    [ whd in ⊢ (??%? → ?); cases (fn_return f) normalize #A try #B try #C try #D destruct
    | #a' whd nodelta in ⊢ (??%? → ?); cases (type_eq_dec (fn_return f) Tvoid)
      #x whd in ⊢ (??%? → ?); [2: cases (exec_expr ????) #y ] #EX whd in EX:(??%?); destruct
    ]
  | cases (find_label a (fn_body f) (call_cont kk)) [ 2: * #x #y ] #EX whd in EX:(??%?); destruct
  | @bindIO_res_interact #l #El @bindIO_res_interact #vt #Evt @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct
  | 4,7: @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 #EX whd in EX:(??%?); destruct
  | @bindIO_res_interact * * normalize #A #B #C try #D try #E destruct
  | @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 @bindIO_opt_interact #x5 #x6 @bindIO_res_interact #x7 #x8 cases a
      [ 2: #x9 @bindIO_res_interact #x10 #x11 ] #EX whd in EX:(??%?); destruct
  | cases (is_Sskip a) #H [ @bindIO_res_interact #vt #Evt @bindIO_res_interact #v #Ev ] #EX whd in EX:(??%?); destruct
  | cases kk [ 1,8: cases (fn_return f) normalize #A try #B try #C try #D try #E try #F try #G try #H destruct
    | 2,3,5,6,7: normalize #A #B try #C try #D try #E destruct
    | #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct ]
  | cases kk normalize #A try #B try #C try #D try #E destruct
  | cases kk [ 4: #z1 #z2 #z3 @bindIO_res_interact #x1 #x2 @bindIO_res_interact #x3 #x4 cases x3 #EX whd in EX:(??%?); destruct
    | *: normalize #A try #B try #C try #D try #E destruct
    ]
  ]
| #f #args #kk #m #o #k cases f 
  [ #f' whd in ⊢ (??%? → ?); cases (exec_alloc_variables empty_env m (fn_params f'@fn_vars f'))
    #x1 #x2 @bindIO_res_interact #m #Em #EX whd in EX:(??%?); destruct
  (* This is the only case that actually matters! *)
  | #fn #argtys #rty whd in ⊢ (??%? → ?);
    @bindIO_res_interact #vs #Evs
    #EX whd in EX:(??%?); destruct
    %{fn} %{argtys} %{rty} %{args} %{kk} %{m} %
  ]
| #v #kk #m #o #k whd in ⊢ (??%? → ?); cases kk
    [ cases v [2: * ] normalize #A try #B destruct
    | 8: #x1 #x2 #x3 #x4 cases x1
      [ whd in ⊢ (??%? → ?); #EX destruct | #x5 whd in ⊢ (??%? → ?); cases x5
          #x6 #x7 @bindIO_opt_interact #m' #Em #EX whd in EX:(??%?); destruct ]
    | *: normalize #A try #B try #C try #D try #E destruct ]
| #r #o #k #EX whd in EX:(??%?); destruct
] qed.

lemma state_with_labels_call : ∀f,a,k,m,s1.
 state_with_labels (Callstate f a k m) s1 →
 ∃k'. cont_with_labels k k' ∧ s1 = Callstate (label_fundef f) a k' m.
#f #a #k #m #s1 #S inversion S
[ #s #s' #S' #E1 #E2 #E3 destruct inversion S'
  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct
  | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct
  | #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 destruct
  | #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 destruct
  | #f' #a' #k' #k'' #m' #K #E1 #E2 #E3 destruct %{k''} % //
  | #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct
  | #H72 #H73 #H74 #H75 destruct
  ]
| #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 #H86 #H87 destruct
] qed. 

lemma interactive_step_with_labels : ∀ge,ge'.
  related_globals … label_fundef ge ge' →
  ∀s1,s1',o,k.
  exec_step ge s1 = Interact … o k →
  state_with_labels s1 s1' →
  ∃k'.
      exec_step ge' s1' = Interact … o k' ∧
  ∀i. ∃tr,s2.
    k i = Value … 〈tr,s2〉 ∧
    ∃tr',s2'.
      k' i = Value … 〈tr',s2'〉 ∧
      trace_with_extra_labels tr tr' ∧
      state_with_labels s2 s2'.
#ge #ge' #RG #s1 #s1' #o #k #EX
cases (exec_step_interaction … EX)
#fn * #argtys * #retty * #vargs * #k' * #m #E
destruct
#S cases (state_with_labels_call … S)
#k'' * #K #E2 destruct
whd in EX:(??%?);
@(bindIO_res_interact ?????????? EX) -EX
#vs #CHECK #EX whd in EX:(??%?); destruct
% [2: %
[ whd in ⊢ (??%?);
  >CHECK in ⊢ (??%?);
  whd in ⊢ (??%?);
  @refl
| #i
  % [2: % [2: %
  [ @refl
  | % [2: % [ 2: % [ %
    [ @refl
    | // ]
    | /3/ ]
    | skip ]| skip ]
  ]| skip ]| skip ]
]| skip
] qed.


lemma initial_state_in_simulation : ∀p,s.
  make_initial_state p = OK ? s →
  ∃s'. make_initial_state (clight_label p) = OK ? s' ∧ state_with_labels s s'.
* #vars #fns #main #s
whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
cases (bind_inversion ????? EX) -EX #m * #Em #EX
cases (bind_inversion ????? EX) -EX #b * #Emain #EX
cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
whd in EX:(??%%); destruct
whd in match (make_initial_state ?);
letin ge' ≝ (make_global ?)
cut (related_globals … label_fundef ge ge')
[ // ] #RG
% [2: %
[ whd in ⊢ (??%?);
  change with (transform_program ??? (mk_program …) (λ_.label_fundef)) in match (mk_program ??? (transf_program ????) ?);
  >init_mem_transf >Em in ⊢ (??%?);
  whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
  whd in ⊢ (??%?); >(rg_find_funct_ptr … RG … Emain')
  whd in ⊢ (??%?); @refl
| /3/
] | skip ]
qed.
  


lemma not_wrong_init : ∀p.
  not_wrong (exec_inf … clight_fullexec p) →
  ∃s. make_initial_state … p = OK ? s.
#p whd in ⊢ (?% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
cases (make_initial_state p)
[ /2/
| normalize #m #NW @⊥
  inversion NW #H1 #H2 #H3 #H4 try #H5 destruct
] qed.

lemma final_related : ∀s1,s2.
  state_with_labels s1 s2 →
  is_final s1 = is_final s2.
#s1x #s2x *
[ #s1y #s2y * //
| //
] qed.

lemma plus_not_final : ∀ge,s,tr,s'.
  plus ge s tr s' →
  is_final s = None ?.
#ge #s0 #tr0 #s0' * 
[ #s1 #tr #s2 #EX | #s1 #tr #s2 #tr' #s3 #EX #PL ]
lapply (refl ? (is_final s1))
cases (is_final s1) in ⊢ (???% → %);
//
#r cases s1 in EX ⊢ %;
#H9 #H10 #H11 try #H12 try #H13 try #H14 try #H15
[ 1,5: whd in H15:(??%?); | 2,6: whd in H14:(??%?); | 3,7: whd in H13:(??%?); | 4,8: whd in H11:(??%?); ]
destruct
normalize in H10;
destruct
qed.

lemma plus_exec : ∀ge,s,tr,s'.
  plus ge s tr s' →
  is_final s' = None ? →
  steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
           (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
#ge #s0 #tr0 #s0' #P elim P
[ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold
  whd in ⊢ (??%?);
  whd in match (is_final ?????); >NF
  %2
| #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF
  >exec_inf_aux_unfold >EX1
  whd in ⊢ (??%?);
  whd in match (is_final ?????); >(plus_not_final … P2)
  %3 @IH //
] qed.

lemma plus_exec_final : ∀ge,s,tr,s',r.
  plus ge s tr s' →
  is_final s' = Some ? r →
  ∃tr'. steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
                 (e_stop … tr' r s').
#ge #s0 #tr0 #s0' #r #P elim P
[ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold
  %{tr} whd in ⊢ (??%?);
  whd in match (is_final ?????); >F
  %1
| #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #F
  cases (IH … F)
  #tr' #S' %{tr'}
  >exec_inf_aux_unfold >EX1
  whd in ⊢ (??%?);
  whd in match (is_final ?????); >(plus_not_final … P2)
  %3 @S'
] qed.

let corec build_exec
  (ge1,ge2:genv)
  (RG:related_globals … label_fundef ge1 ge2)
  (s1,s2:state)
  (S:state_with_labels s1 s2)
  (NW:not_wrong (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
: sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝ 
match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
[ nw_stop tr i s ⇒ ?
| nw_step tr1 s1' e1 NW1 ⇒ ?
| nw_interact o k NWk ⇒ ?
] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))).
[ #E1
  cases (exec_inf_stops_at_final ?? clight_fullexec … E1)
  #EX1 #F1
  cases (step_with_labels … RG … S EX1)
  #tr2 * #s2' * * #PL #TWL #S'
  lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2
  cases (plus_exec_final ????? PL F2)
  #tr2' #S2
  @(swl_stop … S2 TWL)
| #E1
  cases (extract_step ?? clight_fullexec … E1)
  #EX1 #E1'
  cases (step_with_labels … RG … S EX1)
  #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*)
  @(swl_steps … (plus_exec … EX2 ?))
  [ <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1)
  | //
  | (* Manual rewrite to prevent guardedness condition getting upset. *)
    @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?])
    @build_exec // >E1' in NW1; //
  ]
| #E1 
  cases (extract_interact ?? clight_fullexec … E1)
  #k' * #EX1 #Ek lapply NWk -NWk @(match sym_eq … Ek with [refl ⇒ ?]) #NWk
  cases (interactive_step_with_labels … RG … EX1 S)
  #k2' * #EX2 #H2 @(match sym_eq … EX2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) (* XXX why is this necessary? *) whd in ⊢ (??%);
  @swl_interact
  #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
  lapply (NWk i)
  @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (?% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])
  @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge2 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????);
  cases (is_final s2')
  [ whd in ⊢ (?% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
    inversion NW'
    [ #H1 #H2 #H3 #H4 #H5 destruct
    | #H7 #H8 #H9 #H10 #H11 #H12 destruct //
    | #H14 #H15 #H16 #H17 #H18 destruct
    ]
  | #r whd in ⊢ (?% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
  ]
] qed.

lemma initial_state_is_not_final : ∀p,s.
  make_initial_state p = OK ? s →
  is_final s = None ?.
* #vars #fns #main #s
whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
cases (bind_inversion ????? EX) -EX #m * #Em #EX
cases (bind_inversion ????? EX) -EX #b * #Emain #EX
cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
whd in EX:(??%%); destruct //
qed.


theorem labelling_sim : labelled_exec_is_equiv.
whd (* let's remind ourselves of the spec *)
#p
#NW
cases (not_wrong_init p NW)
#s1 #I1
cases (initial_state_in_simulation … I1)
#s2 * #I2

whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %;
letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %;
change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p);
>I1

whd in match (exec_inf ????);
letin ge2 ≝ (make_global ?? clight_fullexec (clight_label p))
change with (make_initial_state (clight_label p)) in match (make_initial_state ?? clight_fullexec (clight_label p));
>I2

whd in ⊢ (?% → ? → ?%%);
>exec_inf_aux_unfold
>exec_inf_aux_unfold
whd in ⊢ (?% → ? → ?%%);
whd in match (is_final ?????);
>(initial_state_is_not_final … I1)
whd in match (is_final ?????);
>(initial_state_is_not_final … I2)
whd in ⊢ (?% → ? → ?%%);

#NW #S
@(swl_steps E0 E0)
[ 2: @steps_step | skip | // | @build_exec
  [ @transform_program_related | // | inversion NW
    [ #tr #i #s #E1 #E2 destruct
    | #trX #sX #eX #NWX #E1X #E2X destruct //
    | #H1 #H2 #H3 #H4 #H5 destruct
    ]
  ]
] qed.