source: src/Clight/switchRemoval.ma @ 2353

include "Clight/Csyntax.ma".
include "Clight/fresh.ma".
include "basics/lists/list.ma".
include "basics/lists/listb.ma".
include "common/Identifiers.ma".
include "utilities/extralib.ma".
include "Clight/Cexec.ma".
include "Clight/CexecInd.ma".
include "Clight/frontend_misc.ma".
include "Clight/memoryInjections.ma".

(* -----------------------------------------------------------------------------
   ----------------------------------------------------------------------------*)

(* -----------------------------------------------------------------------------
   Documentation
   ----------------------------------------------------------------------------*)

(* This file implements transformation of switches to linear sequences of
 * if/then/else. The implementation roughly follows the lines of the prototype.
 * /!\ We assume that the program is well-typed (the type of the evaluated 
 * expression must match the constants on each branch of the switch). /!\ *)

(* Documentation. Let the follwing be our input switch construct:
   // ---------------------------------  
   switch(e) {
   case v1:
     stmt1
   case v2:
     stmt2
   .
   .
   .
   default:
     stmt_default
   }
   // ---------------------------------  
  
   Note that stmt1,stmt2, ... stmt_default may contain "break" statements, wich have the effect of exiting 
   the switch statement. In the absence of break, the execution falls through each case sequentially.
 
   Given such a statement, we produce an equivalent sequence of if-then-elses chained by gotos:

   // ---------------------------------  
   fresh = e;
   if(fresh == v1) {
     stmt1';
     goto lbl_case2;
   }
   if(fresh == v2) {
     lbl_case2:
     stmt2';
     goto lbl_case2;
   }   
   ...
   stmt_default';
   exit_label:
   // ---------------------------------    

   where stmt1', stmt2', ... stmt_default' are the statements where all top-level [break] statements
   were replaced by [goto exit_label]. Note that fresh, lbl_casei are fresh identifiers and labels.
*)


(* -----------------------------------------------------------------------------
   Definitions allowing to state that the program resulting of the transformation
   is switch-free.
   ---------------------------------------------------------------------------- *)

(* Property of a Clight statement of containing no switch. Could be generalized into a kind of
 * statement_P, if useful elsewhere. *)
let rec switch_free (st : statement) : Prop ≝
match st with
[ Sskip ⇒ True
| Sassign _ _ ⇒ True
| Scall _ _ _ ⇒ True
| Ssequence s1 s2 ⇒ switch_free s1 ∧ switch_free s2
| Sifthenelse e s1 s2 ⇒ switch_free s1 ∧ switch_free s2
| Swhile e body _ ⇒ switch_free body
| Sdowhile e body ⇒ switch_free body
| Sfor s1 _ s2 s3 ⇒ switch_free s1 ∧ switch_free s2 ∧ switch_free s3
| Sbreak ⇒ True
| Scontinue ⇒ True
| Sreturn _ ⇒ True
| Sswitch _ _ ⇒ False
| Slabel _ body ⇒ switch_free body
| Sgoto _ ⇒ True
| Scost _ body ⇒ switch_free body
].

(* Property of a list of labeled statements of being switch-free *)
let rec branches_switch_free (sts : labeled_statements) : Prop ≝ 
match sts with
[ LSdefault st =>
  switch_free st
| LScase _ _ st tl => 
  switch_free st ∧ branches_switch_free tl
].

let rec branches_ind
  (sts : labeled_statements)
  (H   : labeled_statements → Prop)  
  (defcase : ∀st. H (LSdefault st))
  (indcase : ∀sz.∀int.∀st.∀sub_cases. H sub_cases → H (LScase sz int st sub_cases)) ≝
match sts with
[ LSdefault st ⇒ 
  defcase st
| LScase sz int st tl ⇒
  indcase sz int st tl (branches_ind tl H defcase indcase)
].

(* -----------------------------------------------------------------------------
   Switch-removal code for statements, functions and fundefs.
   ----------------------------------------------------------------------------*)

(* Converts the directly accessible ("free") breaks to gotos toward the [lab] label.  *)
let rec convert_break_to_goto (st : statement) (lab : label) : statement ≝
match st with
[ Sbreak ⇒
  Sgoto lab
| Ssequence s1 s2 ⇒
  Ssequence (convert_break_to_goto s1 lab) (convert_break_to_goto s2 lab)
| Sifthenelse e iftrue iffalse ⇒
  Sifthenelse e (convert_break_to_goto iftrue lab) (convert_break_to_goto iffalse lab)
| Sfor init e update body ⇒
  Sfor (convert_break_to_goto init lab) e update body
| Slabel l body ⇒
  Slabel l (convert_break_to_goto body lab)
| Scost cost body ⇒
  Scost cost (convert_break_to_goto body lab)
| _ ⇒ st
].

(* Converting breaks preserves switch-freeness. *)
lemma convert_break_lift : ∀s,label . switch_free s → switch_free (convert_break_to_goto s label).
#s elim s //
[ 1: #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
| 2: #e #s1 #s2 #Hind1 #Hind2 #label * #Hsf1 #Hsf2 /3/
| 3: #s1 #e #s2 #s3 #Hind1 #Hind2 #Hind3 #label * * #Hsf1 #Hsf2 #Hsf3 normalize
     try @conj try @conj /3/
| 4: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /2/
| 5: #l #s0 #Hind #lab #Hsf whd in Hsf; normalize /3/
] qed.

(*  (def_case : ident × sf_statement) *)

let rec produce_cond
  (e : expr)
  (switch_cases : labeled_statements)
  (u : universe SymbolTag)
  (exit : label) on switch_cases : statement × label × (universe SymbolTag) ≝
match switch_cases with
[ LSdefault st ⇒  
  let 〈lab,u1〉 ≝ fresh ? u in
  let st' ≝ convert_break_to_goto st exit in
  〈Slabel lab st', lab, u1〉
| LScase sz tag st other_cases ⇒
  let 〈sub_statements, sub_label, u1〉 ≝ produce_cond e other_cases u exit in
  let st' ≝ convert_break_to_goto st exit in
  let 〈lab, u2〉 ≝ fresh ? u1 in
  let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz tag) (typeof e))) (Tint I32 Signed) in
  let case_statement ≝
       Sifthenelse test
        (Slabel lab (Ssequence st' (Sgoto sub_label)))
        Sskip
  in
  〈Ssequence case_statement sub_statements, lab, u2〉
].

definition simplify_switch ≝
   λ(e : expr).
   λ(switch_cases : labeled_statements).
   λ(uv : universe SymbolTag).
 let 〈exit_label, uv1〉            ≝ fresh ? uv in
 let 〈result, useless_label, uv2〉 ≝ produce_cond e switch_cases uv1 exit_label in
 〈Ssequence result (Slabel exit_label Sskip), uv2〉.

lemma produce_cond_switch_free : ∀l.∀H:branches_switch_free l.∀e,lab,u.switch_free (\fst (\fst (produce_cond e l u lab))).
#l @(labeled_statements_ind … l) 
[ 1: #s #Hsf #e #lab #u normalize cases (fresh ??) #lab0 #u1 
     normalize in Hsf ⊢ %; @(convert_break_lift … Hsf)
| 2: #sz #i #hd #tl #Hind whd in ⊢ (% → ?); * #Hsf_hd #Hsf_tl
     #e #lab #u normalize
     lapply (Hind Hsf_tl e lab u)
     cases (produce_cond e tl u lab) * #cond #lab' #u' #Hsf normalize nodelta
     cases (fresh ??) #lab0 #u2 normalize nodelta
     normalize try @conj try @conj try @conj try //
     @(convert_break_lift … Hsf_hd)
] qed.

lemma simplify_switch_switch_free : ∀e,l. ∀H:branches_switch_free l. ∀u. switch_free (\fst (simplify_switch e l u)).
#e #l cases l
[ 1: #def normalize #H #u cases (fresh ? u) #exit_label #uv normalize cases (fresh ? uv) #lab #uv' normalize nodelta
     whd @conj whd
     [ 1: @convert_break_lift assumption
     | 2: @I ]
| 2: #sz #i #case #tl normalize * #Hsf #Hsftl #u
     cases (fresh ? u) #exit_label #uv1 normalize nodelta
     lapply (produce_cond_switch_free tl Hsftl e exit_label uv1)
     cases (produce_cond e tl uv1 exit_label)
     * #cond #lab #u1 #Hsf_cond normalize nodelta
     cases (fresh ??) #lab0 #u2 normalize nodelta
     normalize @conj try @conj try @conj try @conj try //
     @(convert_break_lift ?? Hsf)
] qed.

(* Instead of using tuples, we use a special type to pack the results of [switch_removal]. We do that in
   order to circumvent the associativity problems in notations. *)
record swret (A : Type[0]) : Type[0] ≝ {
  ret_st  : A;
  ret_acc : list (ident × type);
  ret_fvs : list ident;
  ret_u   : universe SymbolTag
}.

notation > "vbox('do' 〈ident v1, ident v2, ident v3, ident v4〉 ← e; break e')" with precedence 48
for @{ match ${e} with
       [ None ⇒ None ?
       | Some ${fresh ret} ⇒
          (λ${ident v1}.λ${ident v2}.λ${ident v3}.λ${ident v4}. ${e'})
          (ret_st ? ${fresh ret})
          (ret_acc ? ${fresh ret})
          (ret_fvs ? ${fresh ret})
          (ret_u ? ${fresh ret}) ] }.

notation > "vbox('ret' 〈e1, e2, e3, e4〉)" with precedence 49
for @{ Some ? (mk_swret ? ${e1} ${e2} ${e3} ${e4})  }.
      
(* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list
   of identifiers (supposedly fresh). The actual task of producing this identifier is decoupled in another
   'twin' function. It is then proved that feeding [switch_removal] with the correct amount of free variables
   allows it to proceed without failing. This is all in order to ease the proof of simulation. *)
let rec switch_removal
  (st : statement)           (* the statement in which we will remove switches *)
  (fvs : list ident)         (* a finite list of names usable to create variables. *)
  (u : universe SymbolTag)   (* a fresh /label/ generator *)
  : option (swret statement) ≝
match st with
[ Sskip       ⇒ ret 〈st, [ ], fvs, u〉
| Sassign _ _ ⇒ ret 〈st, [ ], fvs, u〉
| Scall _ _ _ ⇒ ret 〈st, [ ], fvs, u〉
| Ssequence s1 s2 ⇒
  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
  ret 〈Ssequence s1' s2', acc1 @ acc2, fvs'', u''〉
| Sifthenelse e s1 s2 ⇒
  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
  ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
| Swhile e body cl ⇒
  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
  ret 〈Swhile e body' cl, acc, fvs', u'〉
| Sdowhile e body ⇒
  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
  ret 〈Sdowhile e body', acc, fvs', u'〉
| Sfor s1 e s2 s3 ⇒
  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
  do 〈s3', acc3, fvs''', u'''〉 ← switch_removal s3 fvs'' u'';
  ret 〈Sfor s1' e s2' s3', acc1 @ acc2 @ acc3, fvs''', u'''〉
| Sbreak ⇒
  ret 〈st, [ ], fvs, u〉
| Scontinue ⇒
  ret 〈st, [ ], fvs, u〉
| Sreturn _ ⇒
  ret 〈st, [ ], fvs, u〉
| Sswitch e branches ⇒   
   do 〈sf_branches, acc, fvs', u'〉 ← switch_removal_branches branches fvs u;
   match fvs' with
   [ nil ⇒ None ?
   | cons fresh tl ⇒
     (* let 〈switch_tmp, uv2〉 ≝ fresh ? uv1 in *)
     let ident         ≝ Expr (Evar fresh) (typeof e) in
     let assign        ≝ Sassign ident e in
     let 〈result, u''〉 ≝ simplify_switch ident sf_branches u' in
       ret 〈Ssequence assign result, (〈fresh, typeof e〉 :: acc), tl, u'〉
   ]
| Slabel label body ⇒
  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
  ret 〈Slabel label body', acc, fvs', u'〉
| Sgoto _ ⇒
  ret 〈st, [ ], fvs, u〉
| Scost cost body ⇒
  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
  ret 〈Scost cost body', acc, fvs', u'〉 
]

and switch_removal_branches 
  (l : labeled_statements) 
  (fvs : list ident) 
  (u : universe SymbolTag)
(*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
match l with
[ LSdefault st ⇒
  do 〈st', acc1, fvs', u'〉 ← switch_removal st fvs u;
  ret 〈LSdefault st', acc1, fvs', u'〉
| LScase sz int st tl =>
  do 〈tl_result, acc1, fvs', u'〉 ← switch_removal_branches tl fvs u;
  do 〈st', acc2, fvs'', u''〉 ← switch_removal st fvs' u';
  ret 〈LScase sz int st' tl_result, acc1 @ acc2, fvs'', u''〉
].

let rec mk_fresh_variables
  (st : statement)           (* the statement in which we will remove switches *)
  (u : universe SymbolTag)   (* a fresh /label/ generator *)
  : (list ident) × (universe SymbolTag) ≝
match st with
[ Sskip       ⇒ 〈[ ], u〉
| Sassign _ _ ⇒ 〈[ ], u〉
| Scall _ _ _ ⇒ 〈[ ], u〉
| Ssequence s1 s2 ⇒
  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
  〈fvs @ fvs', u''〉
| Sifthenelse e s1 s2 ⇒
  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
  〈fvs @ fvs', u''〉
| Swhile e body cl ⇒
  mk_fresh_variables body u
| Sdowhile e body ⇒
  mk_fresh_variables body u
| Sfor s1 e s2 s3 ⇒
  let 〈fvs, u'〉 ≝ mk_fresh_variables s1 u in
  let 〈fvs', u''〉 ≝ mk_fresh_variables s2 u' in
  let 〈fvs'', u'''〉 ≝ mk_fresh_variables s3 u'' in
  〈fvs @ fvs' @fvs'', u'''〉
| Sbreak ⇒
  〈[ ], u〉
| Scontinue ⇒
  〈[ ], u〉
| Sreturn _ ⇒
  〈[ ], u〉
| Sswitch e branches ⇒   
   let 〈ident, u'〉 ≝ fresh ? u in (* This is actually the only point where we need to create a fresh var. *)
   let 〈fvs, u''〉 ≝ mk_fresh_variables_branches branches u' in
   〈fvs @ [ident], u''〉  (* reversing the order to match a proof invariant *)
| Slabel label body ⇒
  mk_fresh_variables body u
| Sgoto _ ⇒
  〈[ ], u〉
| Scost cost body ⇒
  mk_fresh_variables body u
]

and mk_fresh_variables_branches 
  (l : labeled_statements) 
  (u : universe SymbolTag)
(*  : option (labeled_statements × (list (ident × type)) × (list ident) × (universe SymbolTag)) *) ≝
match l with
[ LSdefault st ⇒
  mk_fresh_variables st u
| LScase sz int st tl =>
  let 〈fvs, u'〉 ≝ mk_fresh_variables_branches tl u in
  let 〈fvs',u''〉 ≝ mk_fresh_variables st u' in
  〈fvs @ fvs', u''〉
].

(* Copied this from Csyntax.ma, lifted from Prop to Type 
   (I needed to eliminate something proved with this towards Type)  *)
let rec statement_indT
  (P:statement → Type[1]) (Q:labeled_statements → Type[1])
  (Ssk:P Sskip)
  (Sas:∀e1,e2. P (Sassign e1 e2))
  (Sca:∀eo,e,args. P (Scall eo e args))
  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
  (Swh:∀e,s,cl. P s → P (Swhile e s cl))
  (Sdo:∀e,s. P s → P (Sdowhile e s))
  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
  (Sbr:P Sbreak)
  (Sco:P Scontinue)
  (Sre:∀eo. P (Sreturn eo))
  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
  (Sla:∀l,s. P s → P (Slabel l s))
  (Sgo:∀l. P (Sgoto l))
  (Scs:∀l,s. P s → P (Scost l s))
  (LSd:∀s. P s → Q (LSdefault s))
  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
  (s:statement) on s : P s ≝
match s with
[ Sskip ⇒ Ssk
| Sassign e1 e2 ⇒ Sas e1 e2
| Scall eo e args ⇒ Sca eo e args
| Ssequence s1 s2 ⇒ Ssq s1 s2
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
| Swhile e s cl ⇒ Swh e s cl
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
| Sdowhile e s ⇒ Sdo e s
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
| Sbreak ⇒ Sbr
| Scontinue ⇒ Sco
| Sreturn eo ⇒ Sre eo
| Sswitch e ls ⇒ Ssw e ls
    (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls)
| Slabel l s ⇒ Sla l s
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
| Sgoto l ⇒ Sgo l
| Scost l s ⇒ Scs l s
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
]
and labeled_statements_indT
  (P:statement → Type[1]) (Q:labeled_statements → Type[1])
  (Ssk:P Sskip)
  (Sas:∀e1,e2. P (Sassign e1 e2))
  (Sca:∀eo,e,args. P (Scall eo e args))
  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
  (Swh:∀e,s,cl. P s → P (Swhile e s cl))
  (Sdo:∀e,s. P s → P (Sdowhile e s))
  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
  (Sbr:P Sbreak)
  (Sco:P Scontinue)
  (Sre:∀eo. P (Sreturn eo))
  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
  (Sla:∀l,s. P s → P (Slabel l s))
  (Sgo:∀l. P (Sgoto l))
  (Scs:∀l,s. P s → P (Scost l s))
  (LSd:∀s. P s → Q (LSdefault s))
  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
  (ls:labeled_statements) on ls : Q ls ≝
match ls with
[ LSdefault s ⇒ LSd s
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
| LScase sz i s t ⇒ LSc sz i s t
    (statement_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    (labeled_statements_indT P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
].

lemma switch_removal_ok :
  ∀st, u0, u1, post.
  Σresult. 
  (switch_removal st ((\fst (mk_fresh_variables st u0)) @ post) u1 = Some ? result) ∧ (ret_fvs ? result = post).
#st 
@(statement_indT ? (λls. ∀u0, u1, post. 
                          Σresult.
                          (switch_removal_branches ls ((\fst (mk_fresh_variables_branches ls u0)) @ post) u1 = Some ? result)
                          ∧ (ret_fvs ? result = post)
                   ) … st)
[ 1: #u0 #u1 #post normalize
     %{(mk_swret statement Sskip [] post u1)} % //
| 2: #e1 #e2 #u0 #u1 #post normalize
     %{((mk_swret statement (Sassign e1 e2) [] post u1))} % try //
| 3: #e0 #e #args #u0 #u1 #post normalize
     %{(mk_swret statement (Scall e0 e args) [] post u1)} % try //
| 4: #s1 #s2 #H1 #H2 #u0 #u1 #post normalize
     elim (H1 u0 u1 ((\fst  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' *      
     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
     elim (H2 u' (ret_u ? s1') post) #s2' *
     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
     #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize
     %{(mk_swret statement (Ssequence (ret_st statement s1') (ret_st statement s2'))
        (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
        (ret_u statement s2'))} % try //
| 5: #e #s1 #s2 #H1 #H2 #u0 #u1 #post normalize
     elim (H1 u0 u1 ((\fst  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))) @ post)) #s1' *      
     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
     elim (H2 u' (ret_u ? s1') post) #s2' *
     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
     #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs >associative_append >Heq1 normalize nodelta >Heq1_fvs >Heq2 normalize
     %{((mk_swret statement
         (Sifthenelse e (ret_st statement s1') (ret_st statement s2'))
         (ret_acc statement s1'@ret_acc statement s2') (ret_fvs statement s2')
         (ret_u statement s2')))} % try //
| 6: #e #s #cl #H #u0 #u1 #post normalize
     elim (H u0 u1 post) #s1' * normalize
     cases (mk_fresh_variables s u0) #fvs #u'
     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
     %{(mk_swret statement (Swhile e (ret_st statement s1') cl) (ret_acc statement s1')
        (ret_fvs statement s1') (ret_u statement s1'))} % try //
| 7: #e #s #H #u0 #u1 #post normalize
     elim (H u0 u1 post) #s1' * normalize
     cases (mk_fresh_variables s u0) #fvs #u'
     #Heq1 #Heq1_fvs >Heq1 normalize nodelta
     %{(mk_swret statement (Sdowhile e (ret_st statement s1')) (ret_acc statement s1')
        (ret_fvs statement s1') (ret_u statement s1'))} % try //
| 8: #s1 #e #s2 #s3 #H1 #H2 #H3 #u0 #u1 #post normalize
     elim (H1 u0 u1
                (\fst (mk_fresh_variables s2 (\snd  (mk_fresh_variables s1 u0))) @
                (\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 (\snd (mk_fresh_variables s1 u0)))))) @
                post)) #s1' *
     cases (mk_fresh_variables s1 u0) #fvs #u' normalize nodelta
     elim (H2 u' (ret_u ? s1') ((\fst (mk_fresh_variables s3 (\snd  (mk_fresh_variables s2 u')))) @
                                 post)) #s2' *
     cases (mk_fresh_variables s2 u') #fvs' #u'' normalize nodelta
     elim (H3 u'' (ret_u ? s2') post) #s3' *
     cases (mk_fresh_variables s3 u'') #fvs'' #u''' normalize nodelta
     #Heq3 #Heq3_fvs #Heq2 #Heq2_fvs #Heq1 #Heq1_fvs
     >associative_append >associative_append >Heq1 normalize >Heq1_fvs
     >Heq2 normalize >Heq2_fvs >Heq3 normalize
     %{(mk_swret statement
        (Sfor (ret_st statement s1') e (ret_st statement s2') (ret_st statement s3'))
        (ret_acc statement s1'@ret_acc statement s2'@ret_acc statement s3')
        (ret_fvs statement s3') (ret_u statement s3'))} % try //
| 9:  #u0 #u1 #post normalize %{(mk_swret statement Sbreak [] post u1)} % //
| 10: #u0 #u1 #post normalize %{(mk_swret statement Scontinue [] post u1)} % //
| 11: #e #u0 #u1 #post normalize %{(mk_swret statement (Sreturn e) [] post u1)} % //
| 12: #e #ls #H #u0 #u1 #post
      whd in match (mk_fresh_variables ??);
      whd in match (switch_removal ???);      
      elim (fresh ? u0) #fresh #u'
      elim (H u' u1 ([fresh] @ post)) #ls' * normalize nodelta
      cases (mk_fresh_variables_branches ls u') #fvs #u'' normalize nodelta      
      >associative_append #Heq #Heq_fvs >Heq normalize nodelta
      >Heq_fvs normalize nodelta
      cases (simplify_switch ???) #st' #u''' normalize nodelta
      %{((mk_swret statement
          (Ssequence (Sassign (Expr (Evar fresh) (typeof e)) e) st')
          (〈fresh,typeof e〉::ret_acc labeled_statements ls') ([]@post)
          (ret_u labeled_statements ls')))} % //
| 13: #l #s #H #u0 #u1 #post normalize
      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
      %{(mk_swret statement (Slabel l (ret_st statement s')) (ret_acc statement s')
           post (ret_u statement s'))} % //
| 14: #l #u0 #u1 #post normalize %{((mk_swret statement (Sgoto l) [] post u1))} % //
| 15: #l #s #H #u0 #u1 #post normalize
      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
      %{(mk_swret statement (Scost l (ret_st statement s')) (ret_acc statement s')
           post (ret_u statement s'))} % //
| 16: #s #H #u0 #u1 #post normalize
      elim (H u0 u1 post) #s' * #Heq >Heq normalize nodelta #Heq_fvs >Heq_fvs
      %{(mk_swret labeled_statements (LSdefault (ret_st statement s'))
         (ret_acc statement s') post (ret_u statement s'))} % //
| 17: #sz #i #hd #tl #H1 #H2 #u0 #u1 #post normalize
      elim (H2 u0 u1 (\fst (mk_fresh_variables hd (\snd (mk_fresh_variables_branches tl u0))) @ post)) #ls' *
      cases (mk_fresh_variables_branches tl u0) #fvs #u' normalize
      elim (H1 u' (ret_u labeled_statements ls') post) #s1' *
      cases (mk_fresh_variables hd u') #fvs' #u' normalize #Heq #Heq_fvs #Heql #Heql_fvs
      >associative_append >Heql normalize >Heql_fvs >Heq normalize
      %{(mk_swret labeled_statements
          (LScase sz i (ret_st statement s1') (ret_st labeled_statements ls'))
          (ret_acc labeled_statements ls'@ret_acc statement s1')
          (ret_fvs statement s1') (ret_u statement s1'))} % //
] qed.

axiom cthulhu : ∀A:Prop. A. (* Because of the nightmares. *)

(* Proof that switch_removal_switch_free does its job. *)
lemma switch_removal_switch_free : ∀st,fvs,u,result. switch_removal st fvs u = Some ? result → switch_free (ret_st ? result).
#st @(statement_ind2 ? (λls. ∀fvs,u,ls_result. switch_removal_branches ls fvs u = Some ? ls_result → 
                                                 branches_switch_free (ret_st ? ls_result)) … st)
[ 1: #fvs #u #result normalize #Heq destruct (Heq) //
| 2: #e1 #e2 #fvs #u #result normalize #Heq destruct (Heq) //
| 3: #e0 #e #args #fvs #u #result normalize #Heq destruct (Heq) //
| 4: #s1 #s2 #H1 #H2 #fvs #u #result normalize lapply (H1 fvs u)
     elim (switch_removal s1 fvs u) normalize
     [ 1: #_ #Habsurd destruct (Habsurd)
     | 2: #res1 #Heq1 lapply (H2 (ret_fvs statement res1) (ret_u statement res1))
          elim (switch_removal s2 (ret_fvs statement res1) (ret_u statement res1))
          [ 1: normalize #_ #Habsurd destruct (Habsurd)
          | 2: normalize #res2 #Heq2 #Heq destruct (Heq)
               normalize @conj
               [ 1: @Heq1 // | 2: @Heq2 // ]
     ] ]
| *: 
  (* TODO the first few cases show that the lemma is routinely proved. TBF later. *)
  @cthulhu ]
qed.

(* -----------------------------------------------------------------------------
   Switch-removal code for programs.
   ----------------------------------------------------------------------------*)  

(* The functions in fresh.ma do not consider labels. Using [universe_for_program p] may lead to 
 * name clashes for labels. We have no choice but to actually run through the function and to 
 * compute the maximum of labels+identifiers. This way we can generate both fresh variables and
 * fresh labels using the same univ. While we're at it we also consider record fields. 
 * Cost labels are not considered, though. They already live in a separate universe. 
 *
 * Important note: this is partially redundant with fresh.ma. We take care of avoiding name clashes,
 * but in the end it might be good to move the following functions into fresh.ma.
 *)

(* Least element in the total order of identifiers. *)
definition least_identifier ≝ an_identifier SymbolTag one. 

(* This is certainly overkill: variables adressed in an expression should be declared in the
 * enclosing function's prototype. *) 
let rec max_of_expr (e : expr) : ident ≝
match e with
[ Expr ed _ ⇒
  match ed with
  [ Econst_int _ _ ⇒ least_identifier
  | Econst_float _ ⇒ least_identifier
  | Evar id ⇒ id
  | Ederef e1 ⇒ max_of_expr e1
  | Eaddrof e1 ⇒ max_of_expr e1
  | Eunop _ e1 ⇒ max_of_expr e1
  | Ebinop _ e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2)
  | Ecast _ e1 ⇒ max_of_expr e1
  | Econdition e1 e2 e3 ⇒  
    max_id (max_of_expr e1) (max_id (max_of_expr e2) (max_of_expr e3))
  | Eandbool e1 e2 ⇒
    max_id (max_of_expr e1) (max_of_expr e2)
  | Eorbool e1 e2 ⇒
    max_id (max_of_expr e1) (max_of_expr e2)  
  | Esizeof _ ⇒ least_identifier
  | Efield r f ⇒ max_id f (max_of_expr r)
  | Ecost _ e1 ⇒ max_of_expr e1
  ]
].

(* Reasoning about this promises to be a serious pain. Especially the Scall case. *)
let rec max_of_statement (s : statement) : ident ≝
match s with
[ Sskip ⇒ least_identifier
| Sassign e1 e2 ⇒ max_id (max_of_expr e1) (max_of_expr e2)
| Scall r f args ⇒
  let retmax ≝ 
    match r with
    [ None ⇒ least_identifier
    | Some e ⇒ max_of_expr e ]
  in
  max_id (max_of_expr f) 
         (max_id retmax
                 (foldl ?? (λacc,elt. max_id (max_of_expr elt) acc) least_identifier args) )
| Ssequence s1 s2 ⇒
  max_id (max_of_statement s1) (max_of_statement s2)
| Sifthenelse e s1 s2 ⇒
  max_id (max_of_expr e) (max_id (max_of_statement s1) (max_of_statement s2))
| Swhile e body _ ⇒
  max_id (max_of_expr e) (max_of_statement body)
| Sdowhile e body ⇒
  max_id (max_of_expr e) (max_of_statement body)
| Sfor init test incr body ⇒
  max_id (max_id (max_of_statement init) (max_of_expr test)) (max_id (max_of_statement incr) (max_of_statement body))
| Sbreak ⇒ least_identifier
| Scontinue ⇒ least_identifier
| Sreturn opt ⇒
  match opt with
  [ None ⇒ least_identifier
  | Some e ⇒ max_of_expr e
  ]
| Sswitch e ls ⇒
  max_id (max_of_expr e) (max_of_ls ls)
| Slabel lab body ⇒
  max_id lab (max_of_statement body)
| Sgoto lab ⇒
  lab
| Scost _ body ⇒
  max_of_statement body
]
and max_of_ls (ls : labeled_statements) : ident ≝
match ls with
[ LSdefault s ⇒ max_of_statement s
| LScase _ _ s ls' ⇒ max_id (max_of_ls ls') (max_of_statement s)
].

definition max_id_of_function : function → ident ≝
λf. max_id (max_of_statement (fn_body f)) (max_id_of_fn f).

(* We compute fresh universes on a function-by function basis, since there can't
 * be cross-functions gotos or stuff like that. *)
definition function_switch_removal : function → function × (list (ident × type)) ≝ 
λf.
  (λres_record.
    let new_vars ≝ ret_acc ? res_record in
    let result ≝ mk_function (fn_return f) (fn_params f) (new_vars @ (fn_vars f)) (ret_st ? res_record) in
    〈result, new_vars〉)
  (let u ≝ universe_of_max (max_id_of_function f) in
   let 〈fvs,u'〉 as Hfv ≝ mk_fresh_variables (fn_body f) u in
   match switch_removal (fn_body f) fvs u' return λx. (switch_removal (fn_body f) fvs u' = x) → ? with
   [ None ⇒ λHsr. ?
   | Some res_record ⇒ λ_. res_record
   ] (refl ? (switch_removal (fn_body f) fvs u'))).    
lapply (switch_removal_ok (fn_body f) u u' [ ]) * #result' * #Heq #Hret_eq
<Hfv in Heq; >append_nil >Hsr #Habsurd destruct (Habsurd)
qed.

let rec fundef_switch_removal (f : clight_fundef) : clight_fundef ≝
match f with
[ CL_Internal f ⇒
  CL_Internal (\fst (function_switch_removal f))
| CL_External _ _ _ ⇒
  f
].

let rec program_switch_removal (p : clight_program) : clight_program ≝
 let prog_funcs ≝ prog_funct ?? p in
 let sf_funcs   ≝ map ?? (λcl_fundef. 
    let 〈fun_id, fun_def〉 ≝ cl_fundef in 
    〈fun_id, fundef_switch_removal fun_def〉
  ) prog_funcs in
 mk_program ??
  (prog_vars … p)
  sf_funcs
  (prog_main … p).


(* -----------------------------------------------------------------------------
   Applying two relations on all substatements and all subexprs (directly under). 
   ---------------------------------------------------------------------------- *)

let rec substatement_P (s1 : statement) (P : statement → Prop) (Q : expr → Prop) : Prop ≝
match s1 with
[ Sskip ⇒ True
| Sassign e1 e2 ⇒ Q e1 ∧ Q e2
| Scall r f args ⇒
  match r with
  [ None ⇒ Q f ∧ (All … Q args)
  | Some r ⇒ Q r ∧ Q f ∧ (All … Q args)
  ]
| Ssequence sub1 sub2 ⇒ P sub1 ∧ P sub2
| Sifthenelse e sub1 sub2 ⇒ P sub1 ∧ P sub2
| Swhile e sub _ ⇒ Q e ∧ P sub
| Sdowhile e sub ⇒ Q e ∧ P sub
| Sfor sub1 cond sub2 sub3 ⇒ P sub1 ∧ Q cond ∧ P sub2 ∧ P sub3
| Sbreak ⇒ True
| Scontinue ⇒ True
| Sreturn r ⇒
  match r with
  [ None ⇒ True
  | Some r ⇒ Q r ]
| Sswitch e ls ⇒ Q e ∧ (substatement_ls ls P)
| Slabel _ sub ⇒ P sub
| Sgoto _ ⇒ True
| Scost _ sub ⇒ P sub
]
and substatement_ls ls (P : statement → Prop) : Prop ≝
match ls with
[ LSdefault sub ⇒ P sub
| LScase _ _ sub tl ⇒ P sub ∧ (substatement_ls tl P)
].

(* -----------------------------------------------------------------------------
   Freshness conservation results on switch removal.
   ---------------------------------------------------------------------------- *)

(* Similar stuff in toCminor.ma. *)
lemma fresh_for_univ_still_fresh :
   ∀u,i. fresh_for_univ SymbolTag i u → ∀v,u'. 〈v, u'〉 = fresh ? u → fresh_for_univ ? i u'.
* #p * #i #H1 #v * #p' lapply H1 normalize
#H1 #H2 destruct (H2) /2/ qed.

lemma fresh_eq : ∀u,i. fresh_for_univ SymbolTag i u → ∃fv,u'. fresh ? u = 〈fv, u'〉 ∧ fresh_for_univ ? i u'.
#u #i #Hfresh lapply (fresh_for_univ_still_fresh … Hfresh) 
cases (fresh SymbolTag u)
#fv #u' #H %{fv} %{u'} @conj try // @H //
qed.

lemma produce_cond_fresh : ∀e,exit,ls,u,i. fresh_for_univ ? i u → fresh_for_univ ? i (\snd (produce_cond e ls u exit)).
#e #exit #ls @(branches_ind … ls)
[ 1: #st #u #i #Hfresh normalize
     lapply (fresh_for_univ_still_fresh … Hfresh)
     cases (fresh ? u) #lab #u1 #H lapply (H lab u1 (refl ??)) normalize //
| 2: #sz #i #hd #tl #Hind #u #i' #Hfresh normalize
     lapply (Hind u i' Hfresh) elim (produce_cond e tl u exit) *
     #subcond #sublabel #u1 #Hfresh1 normalize
     lapply (fresh_for_univ_still_fresh … Hfresh1)
     cases (fresh ? u1) #lab #u2 #H2 lapply (H2 lab u2 (refl ??)) normalize //
] qed.

lemma simplify_switch_fresh : ∀u,i,e,ls. 
 fresh_for_univ ? i u → 
 fresh_for_univ ? i (\snd (simplify_switch e ls u)).
#u #i #e #ls #Hfresh
normalize
lapply (fresh_for_univ_still_fresh … Hfresh)
cases (fresh ? u)
#exit_label #uv1 #Haux lapply (Haux exit_label uv1 (refl ??)) -Haux #Haux
normalize lapply (produce_cond_fresh e exit_label ls … Haux)
elim (produce_cond ????) * #stm #label #uv2 normalize nodelta //
qed.

(* -----------------------------------------------------------------------------
   Simulation proof and related voodoo.
   ----------------------------------------------------------------------------*)

definition expr_lvalue_ind_combined ≝
λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
conj ??
 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
 
let rec expr_ind2 
    (P : expr → Prop) (Q : expr_descr → type → Prop)
    (IE : ∀ed. ∀t. Q ed t → P (Expr ed t))
    (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t)
    (Iconst_float : ∀f, t. Q (Econst_float f) t)
    (Ivar : ∀id, t. Q (Evar id) t)
    (Ideref : ∀e, t. P e → Q (Ederef e) t)
    (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t)
    (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t)
    (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t)
    (Icast : ∀castt, e, t. P e →  Q (Ecast castt e) t)  
    (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t)
    (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t)
    (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t)
    (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t)
    (Ifield : ∀e,f,t. P e → Q (Efield e f) t)
    (Icost : ∀c,e,t. P e → Q (Ecost c e) t) 
    (e : expr) on e : P e ≝
match e with
[ Expr ed t ⇒ IE ed t (expr_desc_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost ed t) ]

and expr_desc_ind2
    (P : expr → Prop) (Q : expr_descr → type → Prop)
    (IE : ∀ed. ∀t. Q ed t → P (Expr ed t))
    (Iconst_int : ∀sz, i, t. Q (Econst_int sz i) t)
    (Iconst_float : ∀f, t. Q (Econst_float f) t)
    (Ivar : ∀id, t. Q (Evar id) t)
    (Ideref : ∀e, t. P e → Q (Ederef e) t)
    (Iaddrof : ∀e, t. P e → Q (Eaddrof e) t)
    (Iunop : ∀op,arg,t. P arg → Q (Eunop op arg) t)
    (Ibinop : ∀op,arg1,arg2,t. P arg1 → P arg2 → Q (Ebinop op arg1 arg2) t)
    (Icast : ∀castt, e, t. P e →  Q (Ecast castt e) t)  
    (Icond : ∀e1,e2,e3,t. P e1 → P e2 → P e3 → Q (Econdition e1 e2 e3) t)
    (Iandbool : ∀e1,e2,t. P e1 → P e2 → Q (Eandbool e1 e2) t)
    (Iorbool : ∀e1,e2,t. P e1 → P e2 → Q (Eorbool e1 e2) t)
    (Isizeof : ∀sizeoft,t. Q (Esizeof sizeoft) t)
    (Ifield : ∀e,f,t. P e → Q (Efield e f) t)
    (Icost : ∀c,e,t. P e → Q (Ecost c e) t) 
    (ed : expr_descr) (t : type) on ed : Q ed t ≝
match ed with
[ Econst_int sz i ⇒ Iconst_int sz i t
| Econst_float f ⇒ Iconst_float f t
| Evar id ⇒ Ivar id t
| Ederef e ⇒ Ideref e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
| Eaddrof e ⇒ Iaddrof e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
| Eunop op e ⇒ Iunop op e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
| Ebinop op e1 e2 ⇒ Ibinop op e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
| Ecast castt e ⇒ Icast castt e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
| Econdition e1 e2 e3 ⇒ Icond e1 e2 e3 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e3)
| Eandbool e1 e2 ⇒ Iandbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
| Eorbool e1 e2 ⇒ Iorbool e1 e2 t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e1) (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e2)
| Esizeof sizeoft ⇒ Isizeof sizeoft t
| Efield e field ⇒ Ifield e field t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost  e)
| Ecost c e ⇒ Icost c e t (expr_ind2 P Q IE Iconst_int Iconst_float Ivar Ideref Iaddrof Iunop Ibinop Icast Icond Iandbool Iorbool Isizeof Ifield Icost e)
].

(* Correctness: we can't use a lock-step simulation result. The exec_step for Sswitch will be matched
   by a non-constant number of evaluations in the converted program. More precisely, 
   [seq_of_labeled_statement (select_switch sz n sl)] will be matched by all the steps
   necessary to execute all the "if-then-elses" corresponding to cases /before/ [n]. *)
   
(* A version of simplify_switch hiding the ugly projs *)
definition fresh_for_expression ≝
  λe,u. fresh_for_univ SymbolTag (max_of_expr e) u.

definition fresh_for_statement ≝
  λs,u. fresh_for_univ SymbolTag (max_of_statement s) u.

(* needed during mutual induction ... *)
definition fresh_for_labeled_statements ≝ 
  λls,u. fresh_for_univ ? (max_of_ls ls) u.
   
definition fresh_for_function ≝
  λf,u. fresh_for_univ SymbolTag (max_id_of_function f) u.

(* misc properties of the max function on positives. *)

lemma max_id_one_neutral : ∀v. max_id v (an_identifier ? one) = v.
* #p whd in ⊢ (??%?); >max_one_neutral // qed.

lemma max_id_commutative : ∀v1, v2. max_id v1 v2 = max_id v2 v1.
* #p1 * #p2 whd in match (max_id ??) in ⊢ (??%%);
>commutative_max // qed.

lemma max_id_associative : ∀v1, v2, v3. max_id (max_id v1 v2) v3 = max_id v1 (max_id v2 v3).
* #a * #b * #c whd in match (max_id ??) in ⊢ (??%%); >associative_max //
qed.

lemma fresh_max_split : ∀a,b,u. fresh_for_univ SymbolTag (max_id a b) u → fresh_for_univ ? a u ∧ fresh_for_univ ? b u.
* #a * #b * #u normalize
lapply (pos_compare_to_Prop a b)
cases (pos_compare a b) whd in ⊢ (% → ?); #Hab
[ 1: >(le_to_leb_true a b) try /2/ #Hbu @conj /2/
| 2: destruct >reflexive_leb /2/
| 3: >(not_le_to_leb_false a b) try /2/ #Hau @conj /2/
] qed.

(* Auxilliary commutation lemma used in [substatement_fresh]. *)

lemma foldl_max : ∀l,a,b. 
  foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) (max_id a b) l = 
  max_id a (foldl ?? (λacc,elt.max_id (max_of_expr elt) acc) b l).
#l elim l
[ 1: * #a * #b whd in match (foldl ?????) in ⊢ (??%%); @refl
| 2: #hd #tl #Hind #a #b whd in match (foldl ?????) in ⊢ (??%%);
     <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl
] qed.

(* Lookup functions in list environments (used to type local variables in functions) *)      
let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
match l with
[ nil ⇒ false
| cons hd tl ⇒
  let 〈id, ty〉 ≝ hd in
  match identifier_eq SymbolTag i id with
  [ inl Hid_eq ⇒ true
  | inr Hid_neq ⇒ mem_assoc_env i tl  
  ]
].

let rec assoc_env (i : ident) (l : list (ident×type)) on l : option type ≝
match l with
[ nil ⇒ None ?
| cons hd tl ⇒
  let 〈id, ty〉 ≝ hd in
  match identifier_eq SymbolTag i id with
  [ inl Hid_eq ⇒ Some ? ty
  | inr Hid_neq ⇒ assoc_env i tl  
  ]
].

(* --------------------------------------------------------------------------- *)
(* Memory extensions (limited form on memoryInjection.ma). Note that we state the
   properties at the back-end level. *)
(* --------------------------------------------------------------------------- *)  

(*
definition block_DeqSet : DeqSet ≝ mk_DeqSet block eq_blockb ?.
* #r1 #id1 * #r2 #id2 @(eqZb_elim … id1 id2)
[ 1: #Heq >Heq cases r1 cases r2 normalize
     >eqZb_reflexive normalize @conj #H destruct (H)
     try @refl
| 2: #Hneq cases r1 cases r2 normalize
     >(eqZb_false … Hneq) normalize @conj
     #H destruct (H) elim Hneq #H @(False_ind … (H (refl ??)))
] qed. *)

(* [load_sim] states the fact that each successful load in [m1] is matched by a load in [m2] s.t. the back-end values are equal. *)
definition load_sim ≝
λ(m1 : mem).λ(m2 : mem).
 ∀ptr,bev.
  beloadv m1 ptr = Some ? bev → 
  beloadv m2 ptr = Some ? bev.

(* The [valid_pointer] property is too weak to be preserved by [free]. We use the following guard. *)
(* definition freed_pointer ≝ λ(m : mem).λ(p : pointer).
  low_bound m (pblock p) = OZ ∧
  high_bound m (pblock p) = OZ. *)
  
(* definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res. *)

definition in_bounds_pointer ≝ λm,p. ∀A,f.∃res. do_if_in_bounds A m p f = Some ? res.

definition outbound_pointer ≝ λm,p. 
   Zltb (block_id (pblock p)) (nextblock m) = true ∧
   Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))) = true ∧
   high_bound m (pblock p) = Z_of_unsigned_bitvector … (offv (poff p)).

lemma valid_pointer_def : ∀m,p. valid_pointer m p = true ↔ in_bounds_pointer m p ∨ outbound_pointer m p.
#m #p @conj
[ 1: whd in match (valid_pointer m p); whd in match (in_bounds_pointer ??);
     whd in match (outbound_pointer ??);
     whd in match (do_if_in_bounds); normalize nodelta
     cases (Zltb (block_id (pblock p)) (nextblock m))
     [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]     
     >andb_lsimpl_true normalize nodelta
     cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
     [ 2: normalize nodelta #Habsurd destruct (Habsurd) ]
     >andb_lsimpl_true normalize nodelta
     lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p)))
     elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high_bound m (pblock p)))
     [ 1: #H >H #_ normalize nodelta #_ %1 #A #f /2 by ex_intro/
     | 2: * #_ #H1 #_ #H2 >(Zleb_true_to_Zleb_true_to_eq … H1 H2) %2 @conj try @conj @refl ]
| 2: whd in match (valid_pointer ??); *
     [ 1: whd in match (in_bounds_pointer ??); #H
          lapply (H bool (λblock,contents,off. true))
          * #foo whd in match (do_if_in_bounds ????);
          cases (Zltb (block_id (pblock p)) (nextblock m)) normalize nodelta
          [ 2: #Habsurd destruct (Habsurd) ]
          >andb_lsimpl_true 
          cases (Zleb (low (blocks m (pblock p))) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
          normalize nodelta
          [ 2: #Habsurd destruct (Habsurd) ]
          >andb_lsimpl_true
          elim (Zltb_dec (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))
          [ 1: #H >(Zltb_to_Zleb_true … H) #_ @refl
          | 2: * #Hnlt #Hle >Hnlt normalize nodelta #Habsurd destruct (Habsurd) ]
     | 2: whd in match (outbound_pointer ??); * * #Hlt #Hleb >Hlt >Hleb 
          #Hhigh >Hhigh >andb_lsimpl_true 
          lapply (reflexive_Zle … (Z_of_unsigned_bitvector offset_size (offv (poff p))))
          #Hle >(Zle_to_Zleb_true … Hle) @refl
     ]
] qed.

(*
lemma freed_pointer_dec : ∀m,p. freed_pointer m p ∨ (¬freed_pointer m p).
#m #p
whd in match (freed_pointer ??);
cases (low_bound m (pblock p))
[ 2,3: #low %2 % * #H destruct (H) ]
cases (high_bound m (pblock p))
[ 1: %1 @conj @refl | 2,3: #low %2 % * #_ #H destruct (H) ]
qed. *)

(* In the limited setting of switch removal, a memory extension is a list of fresh blocks
 * to which we can write. *)
record sr_memext (m1 : mem) (m2 : mem) : Type[0] ≝
{ me_inj : load_sim m1 m2;
  (* A list of blocks where we can write freely *)
  me_writeable : list block;   
  (* These blocks are valid *)
  me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b;  
  (* And pointers to m1 are oblivious to these blocks *)
  me_writeable_ok : ∀p.valid_pointer m1 p = true →
                     ¬ (meml ? (pblock p) me_writeable);
  (* Valid pointers are still valid in m2. One could think that this is superfluous as
     being implied by me_inj, and it is but for a small detail: valid_pointer allows a pointer
     to be one off the end of a block bound. The internal check in beloadv does not.
     valid_pointer should be understood as "pointer making sense" rather than "pointer from
     which you can load stuff". [mi_valid_pointers] is used for instance when proving the
     semantics preservation for equality testing (where we check that the pointers we
     compare are valid before being equal).
  *)
  me_valid_pointers : ∀p. (* ¬ (freed_pointer m1 p) → *)
                       valid_pointer m1 p = true → 
                       valid_pointer m2 p = true
}.
 
(* [disjoint_extension e1 m1 e2 m2 types ext] states that [e2] is an extension
   of the environment [e1] s.t. the new binders are in [new], and such that those
   new binders are "writeable" in the memory extension [Hext] *)
definition disjoint_extension ≝
λ(e1 : env). λ(m1 : mem). λ(e2 : env). λ(m2 : mem).
λ(new : list (ident × type)). λ(Hext: sr_memext m1 m2).
  ∀id. match mem_assoc_env id new with
       [ true ⇒
           ∃b. lookup ?? e2 id = Some ? b
            ∧ meml ? b (me_writeable … Hext)
            ∧ lookup ?? e1 id = None ?
       | false ⇒ lookup ?? e1 id = lookup ?? e2 id
       ].
       
(* Lift load_sim to loadn. *)
lemma load_sim_loadn :
 ∀m1,m2. load_sim m1 m2 →
 ∀sz,p,res. loadn m1 p sz = Some ? res → loadn m2 p sz = Some ? res.
#m1 #m2 #Hload_sim #sz
elim sz
[ 1: #p #res #H @H
| 2: #n' #Hind #p #res
     whd in match (loadn ???);
     whd in match (loadn m2 ??);
     lapply (Hload_sim p)
     cases (beloadv m1 p) normalize nodelta
     [ 1: #_ #Habsurd destruct (Habsurd) ]
     #bval #H >(H ? (refl ??)) normalize nodelta
     lapply (Hind (shift_pointer 2 p (bitvector_of_nat 2 1)))
     cases (loadn m1 (shift_pointer 2 p (bitvector_of_nat 2 1)) n')
     normalize nodelta
     [ 1: #_ #Habsurd destruct (Habsurd) ]
     #res' #H >(H ? (refl ??)) normalize
     #H @H
] qed.
 
(* Lift load_sim to front-end values. *)
lemma load_sim_fe :
  ∀m1,m2. load_sim m1 m2 →
  ∀ptr,ty,v.load_value_of_type ty m1 (pblock ptr) (poff ptr) = Some ? v →
            load_value_of_type ty m2 (pblock ptr) (poff ptr) = Some ? v.
#m1 #m2 #Hloadsim #ptr #ty #v
cases ty
[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptrty | 5: #arrayty #arraysz | 6: #argsty #retty
| 7: #sid #fields | 8: #uid #fields | 9: #cptr_id ]
whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?));
[ 1,7,8: #Habsurd destruct (Habsurd)
| 5,6: #H @H
| 2,3,4,9: 
  generalize in match (mk_pointer (pblock ptr) (poff ptr));
  elim (typesize ?)
  [ 1,3,5,7: #p #H @H
  | 2,4,6,8: #n' #Hind #p
      lapply (load_sim_loadn … Hloadsim (S n') p)
      cases (loadn m1 p (S n')) normalize nodelta
      [ 1,3,5,7: #_ #Habsurd destruct (Habsurd) ]      
      #bv #H >(H ? (refl ??)) #H @H
  ]
] qed.

(* Lemmas relating memory extensions to [free] *)

(* Successful beloadv implies valid_pointer. The converse is *NOT* true. *)
lemma beloadv_to_valid_pointer : ∀m,ptr,res. beloadv m ptr = Some ? res → valid_pointer m ptr = true.
* #contents #next #nextpos #ptr #res
whd in match (beloadv ??);
whd in match (valid_pointer ??);
cases (Zltb (block_id (pblock ptr)) next)
normalize nodelta
[ 2: #Habsurd destruct (Habsurd) ]
>andb_lsimpl_true
whd in match (low_bound ??);
whd in match (high_bound ??); 
cases (Zleb (low (contents (pblock ptr)))
        (Z_of_unsigned_bitvector offset_size (offv (poff ptr))))
[ 2: >andb_lsimpl_false normalize #Habsurd destruct (Habsurd) ]
>andb_lsimpl_true
normalize nodelta #H
@Zltb_to_Zleb_true
cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high (contents (pblock ptr)))) in H;
try // normalize #Habsurd destruct (Habsurd) qed.

lemma low_free_eq : ∀m,b1,b2. b1 ≠ b2 → low (blocks m b1) = low (blocks (free m b2) b1).
* #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
@(eqZb_elim … bid1 bid2)
[ 1: #Heq >Heq cases br1 cases br2 normalize 
     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
     #_ @refl
| 2: cases br1 cases br2 normalize #_ #_ @refl ]
qed.

lemma high_free_eq : ∀m,b1,b2. b1 ≠ b2 → high (blocks m b1) = high (blocks (free m b2) b1).
* #contents #next #nextpos * #br1 #bid1 * #br2 #bid2 normalize
@(eqZb_elim … bid1 bid2)
[ 1: #Heq >Heq cases br1 cases br2 normalize 
     [ 1,4: * #H @(False_ind … (H (refl ??))) ]
     #_ @refl
| 2: cases br1 cases br2 normalize #_ #_ @refl ]
qed.

lemma beloadv_free_blocks_neq :
  ∀m,block,pblock,poff,res.
  beloadv (free m block) (mk_pointer pblock poff) = Some ? res → pblock ≠ block.
* #contents #next #nextpos * #br #bid * #pbr #pbid #poff #res
normalize
cases (Zltb pbid next) normalize nodelta
[ 2: #Habsurd destruct (Habsurd) ]
cases pbr cases br normalize nodelta
[ 2,3: #_ % #Habsurd destruct (Habsurd) ]
@(eqZb_elim pbid bid) normalize nodelta
#Heq destruct (Heq)
[ 1,3: >free_not_in_bounds normalize nodelta #Habsurd destruct (Habsurd) ]
#_ % #H destruct (H) elim Heq #H @H @refl
qed.

(*
lemma be_to_fe_value_inj : ∀bv1,bv2.
    be_to_fe_value (ASTint I8 Unsigned) [bv1]
  = be_to_fe_value (ASTint I8 Unsigned) [bv2] → bv1 = bv2.
#bv1 #bv2
whd in match (be_to_fe_value ??);
whd in match (be_to_fe_value ??);
cases bv1 normalize nodelta
[ 1: cases bv2 normalize nodelta
     [ 1: #H @refl | 2:
try //
[ cases bv2 *)

lemma beloadv_free_beloadv :
  ∀m,block,ptr,res.
    beloadv (free m block) ptr = Some ? res →
    beloadv m ptr = Some ? res.
* #contents #next #nextpos #block * #pblock #poff #res
#H lapply (beloadv_free_blocks_neq … H) #Hblocks_neq
lapply H
whd in match (beloadv ??);
whd in match (beloadv ??) in ⊢ (? → %);
whd in match (nextblock (free ??));
cases (Zltb (block_id pblock) next)
[ 2: normalize #Habsurd destruct (Habsurd) ]
normalize nodelta
<(low_free_eq … Hblocks_neq)
<(high_free_eq … Hblocks_neq)
whd in match (free ??);
whd in match (update_block ?????);
@(eq_block_elim … pblock block)
[ 1: #Habsurd >Habsurd in Hblocks_neq; * #H @(False_ind … (H (refl ??))) ]
#_ normalize nodelta
#H @H
qed.

lemma beloadv_free_beloadv2 :
  ∀m,block,ptr,res.
  pblock ptr ≠ block →
  beloadv m ptr = Some ? res →
  beloadv (free m block) ptr = Some ? res.
* #contents #next #nextpos #block * #pblock #poff #res #Hneq
whd in match (beloadv ??);
whd in match (beloadv ??) in ⊢ (? → %);
whd in match (nextblock (free ??));
cases (Zltb (block_id pblock) next)
[ 2: normalize #Habsurd destruct (Habsurd) ]
normalize nodelta
<(low_free_eq … Hneq)
<(high_free_eq … Hneq)
whd in match (free ??);
whd in match (update_block ?????);
@(eq_block_elim … pblock block)
[ 1: #Habsurd >Habsurd in Hneq; * #H @(False_ind … (H (refl ??))) ]
#_ normalize nodelta
#H @H
qed.

lemma beloadv_free_simulation :
  ∀m1,m2,block,ptr,res.
  ∀mem_hyp : sr_memext m1 m2.  
  beloadv (free m1 block) ptr = Some ? res → beloadv (free m2 block) ptr = Some ? res.
* #contents1 #nextblock1 #nextpos1 * #contents2 #nextblock2 #nextpos2
* #br #bid * * #pr #pid #poff #res *
#Hload_sim #Hme_writeable #Hme_writeable_valid #Hptr_not_mem #Hvalid_conserv
#Hload
lapply (beloadv_free_beloadv … Hload) #Hload_before_free
lapply (beloadv_free_blocks_neq … Hload) #Hblocks_neq
@beloadv_free_beloadv2
[ 1: @Hblocks_neq ]
@Hload_sim assumption
qed.

lemma in_bounds_free_to_in_bounds : ∀m,b,p. in_bounds_pointer (free m b) p → in_bounds_pointer m p.
#m #b #p whd in match (in_bounds_pointer ??) in ⊢ (% → %);
#H #A #f elim (H bool (λ_,_,_.true)) #foo whd in match (do_if_in_bounds ????) in ⊢ (% → %);
elim (Zltb_dec … (block_id (pblock p)) (nextblock (free m b)))
[ 1: #Hlt >Hlt normalize nodelta 
     @(eq_block_elim … b (pblock p))
     [ 1: #Heq >Heq whd in match (free ??);
          whd in match (update_block ?????); >eq_block_b_b
          normalize nodelta normalize in match (low ?);
          >Zltb_unsigned_OZ >andb_comm >andb_lsimpl_false normalize nodelta
          #Habsurd destruct (Habsurd)
     | 2: #Hblock_neq whd in match (free ? ?);
          whd in match (update_block ?????);
          >(not_eq_block_rev … Hblock_neq) normalize nodelta
          cases (Zleb (low_bound m (pblock p)) (Z_of_unsigned_bitvector offset_size (offv (poff p))))
          [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
          >andb_lsimpl_true
          lapply (Zltb_to_Zleb_true (Z_of_unsigned_bitvector offset_size (offv (poff p)))
                                     (high (blocks m (pblock p))))
          cases (Zltb (Z_of_unsigned_bitvector offset_size (offv (poff p))) (high (blocks m (pblock p))))
          [ 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
          normalize nodelta #H #_ /2 by ex_intro/
     ]
| 2: * #Hlt #Hle >Hlt normalize nodelta #Habsurd destruct (Habsurd) ]
qed.

lemma outbound_free_to_outbound : ∀m,b,p. outbound_pointer (free m b) p → outbound_pointer m p.
#m #b #p whd in match (free ??);
whd in match (outbound_pointer ??) in ⊢ (% → %);
whd in match (update_block ????);
whd in match (low_bound ??); whd in match (high_bound ??);
@(eq_block_elim … (pblock p) b) normalize nodelta
[ 1: #Heq >Heq cases (Zltb ? (nextblock m))
     [ 2: * * #Habsurd destruct (Habsurd) ]
     * * #_ whd in match (low ?); whd in match (high ?);
     #H1 #H2 <H2 in H1; normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
| 2: #Hneq #H @H ]
qed.

lemma valid_free_to_valid : ∀m,b,p. valid_pointer (free m b) p = true → valid_pointer m p = true.
#m #b #p #Hvalid
lapply (valid_pointer_def … m p) * #_ #Hdef @Hdef
elim (valid_pointer_def … (free m b) p) #H #_
elim (H Hvalid)
[ 1: #Hin %1 @in_bounds_free_to_in_bounds assumption
| 2: #Hout %2 @outbound_free_to_outbound assumption ]
qed.

lemma valid_after_free : ∀m,b,p. valid_pointer (free m b) p = true → b ≠ pblock p.
#m #b #p
whd in match (valid_pointer ??);
whd in match (free ??);
whd in match (update_block ????);
whd in match (low_bound ??);
whd in match (high_bound ??);
@(eq_block_elim … b (pblock p))
[ 1: #Heq >Heq >eq_block_b_b normalize nodelta
     whd in match (low ?); whd in match (high ?);
     cases (Zltb ? (nextblock m))
     [ 2: >andb_lsimpl_false normalize nodelta #Habsurd destruct (Habsurd) ]
     >andb_lsimpl_true >free_not_valid #Habsurd destruct (Habsurd)
| 2: #Hneq #_ @Hneq ]
qed.

lemma valid_pointer_free : ∀m1,m2. sr_memext m1 m2 → ∀p,b. valid_pointer (free m1 b) p = true → valid_pointer (free m2 b) p = true.
#m1 #m2 #Hext #p #b #Hvalid
lapply (valid_free_to_valid … Hvalid) #Hvalid_before_free
lapply (me_valid_pointers … Hext … Hvalid_before_free)
lapply (valid_after_free … Hvalid) #Hneq
whd in match (free ??);
whd in match (update_block ????);
whd in match (valid_pointer ??) in ⊢ (% → %);
whd in match (low_bound ??) in ⊢ (% → %);
whd in match (high_bound ??) in ⊢ (% → %);
>(not_eq_block_rev … Hneq) normalize nodelta #H @H
qed.

(* Performing a [free] preserves memory extensions. *)
lemma free_memory_ext : 
  ∀m1,m2,bl.
   sr_memext m1 m2 →
   sr_memext (free m1 bl) (free m2 bl).
#m1 #m2 #bl #Hext
%
[ 1: @(λptr,bev. beloadv_free_simulation m1 m2 bl ptr bev Hext)
| 2: @(filter ? (λwb. notb (eq_block wb bl)) (me_writeable … Hext))
| 3: #b #Hmem
     cut (mem block b (me_writeable m1 m2 Hext))
     [ elim (me_writeable m1 m2 Hext) in Hmem;
       [ 1: #H @H
       | 2: #h #tl #Hind whd in match (filter ???);
            @(eq_block_elim … h bl) normalize in match (notb ?); normalize nodelta
            [ 1: #Heq #H whd in match (meml ???); destruct %2 @Hind @H
            | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); *
                 [ 1: #H %1 @H 
                 | 2: #H %2 @Hind @H ] ] ] ]
    #Hmem2 lapply (me_writeable_valid … Hmem2)
    elim m2 #contents #nextblock #pos elim b #br #bid
    normalize #H @H
| 4: #p #Hvalid elim (valid_pointer_free_ok_alt … Hvalid)
     [ 1: #Heq >Heq elim (me_writeable m1 m2 Hext)
        [ 1: normalize % //
        | 2: #hd #tl #Hind
             whd in match (filter ???);
             @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta
             [ 1: #Heq @Hind
             | 2: #Hneq whd in match (meml ???); % *
                  [ 1: #Heq elim Hneq #H @H @(sym_eq … Heq)
                  | 2: #H elim Hind #Hind @Hind @H ] ] ]
    | 2: * #_ #Hvalid lapply (me_writeable_ok … Hext … Hvalid)
        * #Hyp % #Htarget @Hyp
        elim (me_writeable m1 m2 Hext) in Htarget;
        [ 1: normalize //
        | 2: #hd #tl #Hind
             whd in match (filter ???);
             @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta
             [ 1: #Heq whd in match (meml ???) in ⊢ (? → %);
                  #H %2 @Hind @H
             | 2: #Hneq whd in match (meml ???);
                  whd in match (meml ???) in ⊢ (? → %); *
                  [ 1: #H %1 @H 
                  | 2: #H %2@Hind @H ] ] ] ]
| 5: #p @valid_pointer_free @Hext 
] qed.


lemma free_list_memory_ext : 
  ∀l,m1,m2.
   sr_memext m1 m2 →
   sr_memext (free_list m1 l) (free_list m2 l).
#l elim l
[ 1: #m1 #m2 #H @H
| 2: #hd #tl #Hind #m1 #m2 #H >free_list_cons >free_list_cons
     @free_memory_ext @Hind @H
] qed.

(* Extend the previous lemma to [free_list] *)
lemma beloadv_free_list_memory_ext :
  ∀m1,m2,blocks,ptr,res.
  ∀mem_hyp : sr_memext m1 m2.  
  beloadv (free_list m1 blocks) ptr = Some ? res → beloadv (free_list m2 blocks) ptr = Some ? res.
#m1 #m2 #blocks #mtr #res #Hext #Hload
lapply (free_list_memory_ext blocks … Hext) #Hext_list
lapply (me_inj … Hext_list) #H @H @Hload
qed.


(* Prove that memory extensions are preserved by free.*)
(*
lemma memext_free_conservation : 
  ∀m1,m2 : mem.
  ∀mem_hyp : sr_memext m1 m2.
  ∀env,env_ext.
  ∀new_vars.
  ∀env_hyp : disjoint_extension env m1 env_ext m2 new_vars mem_hyp.
   (sr_memext (free_list m1 (blocks_of_env env))
     (free_list m2 (blocks_of_env env_ext))).
#m1 #m2 * #Hloadsim #Hwriteable #Hwritevalid #Holdnotwriteable #Hvalidok #env #env_ext #new_vars
whd in ⊢ (% → ?); #Hdisjoint *)


(* In proofs, [disjoint_extension] is not enough. When a variable lookup arises, if
 * the variable is not in a local environment, then we search into the global one.
 * A proper "extension" of a local environment should be such that the extension
 * does not collide with a given global env. 
 * To see the details of why we need that, see [exec_lvalue'], Evar id case.
 *)
definition ext_fresh_for_genv ≝
λ(ext : list (ident × type)). λ(ge : genv).
  ∀id. mem_assoc_env id ext = true → find_symbol … ge id = None ?.

(* Any environment is a "disjoint" extension of itself with nothing. *)
(*
lemma disjoint_extension_nil : ∀e,m,types. disjoint_extension e m e m types [].
#e #m #ty #id
normalize in match (mem_assoc_env id []); normalize nodelta
cases (lookup ?? e id) try //
#b normalize nodelta
% #ty cases (load_value_of_type ????)
[ 1: %2 /2/ | 2: #v %1 %{v} %{v} @conj //
cases (assoc_env id ty) //
qed. *)

(* "generic" simulation relation on [res ?] *)
definition res_sim ≝
  λ(A : Type[0]).
  λ(r1, r2 : res A).
  ∀a. r1 = OK ? a → r2 = OK ? a.

(* Specialisation of [res_sim] to match [exec_expr] *)
definition exec_expr_sim ≝ res_sim (val × trace).

(* Specialisation of [res_sim] to match [exec_lvalue] *)
definition exec_lvalue_sim ≝ res_sim (block × offset × trace).

lemma load_value_of_type_dec : ∀ty, m, b, o. load_value_of_type ty m b o = None ? ∨ ∃r. load_value_of_type ty m b o = Some ? r.
#ty #m #b #o cases (load_value_of_type ty m b o)
[ 1: %1 // | 2: #v %2 /2 by ex_intro/ ] qed.

(* Simulation relations. *)
inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝
| swc_stop : ∀fvs.
    switch_cont_sim fvs Kstop Kstop
| swc_seq : ∀fvs,s,k,k',u,result.
    fresh_for_statement s u →
    switch_cont_sim fvs k k' →
    switch_removal s fvs u = Some ? result →
    switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
| swc_while : ∀fvs,e,s,cl,k,k',u,result.
    fresh_for_statement (Swhile e s cl) u →
    switch_cont_sim fvs k k' →
    switch_removal s fvs u = Some ? result →
    switch_cont_sim fvs (Kwhile e s cl k) (Kwhile e (ret_st ? result) cl k')
| swc_dowhile : ∀fvs,e,s,k,k',u,result.
    fresh_for_statement (Sdowhile e s) u →
    switch_cont_sim fvs k k' →
    switch_removal s fvs u = Some ? result →
    switch_cont_sim fvs (Kdowhile e s k) (Kdowhile e (ret_st ? result) k')
| swc_for1 : ∀fvs,e,s1,s2,k,k',u,result.
    fresh_for_statement (Sfor Sskip e s1 s2) u →
    switch_cont_sim fvs k k' →
    switch_removal (Sfor Sskip e s1 s2) fvs u = Some ? result →
    switch_cont_sim fvs (Kseq (Sfor Sskip e s1 s2) k) (Kseq (ret_st ? result) k')
| swc_for2 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
    fresh_for_statement (Sfor Sskip e s1 s2) u →
    switch_cont_sim fvs k k' →
    switch_removal s1 fvs u = Some ? result1 →
    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 →
    switch_cont_sim fvs (Kfor2 e s1 s2 k) (Kfor2 e (ret_st ? result1) (ret_st ? result2) k')
| swc_for3 : ∀fvs,e,s1,s2,k,k',u,result1,result2.
    fresh_for_statement (Sfor Sskip e s1 s2) u →
    switch_cont_sim fvs k k' →
    switch_removal s1 fvs u = Some ? result1 →
    switch_removal s2 fvs (ret_u ? result1) = Some ? result2 ->
    switch_cont_sim fvs (Kfor3 e s1 s2 k) (Kfor3 e (ret_st ? result1) (ret_st ? result2) k')
| swc_switch : ∀fvs,k,k'.
    switch_cont_sim fvs k k' → 
    switch_cont_sim fvs (Kswitch k) (Kswitch k')
| swc_call : ∀fvs,en,en',r,f,k,k'. (* Warning: possible caveat with environments here. *)       
    switch_cont_sim fvs k k' →
    (* /!\ Update [en] with [fvs'] ... *)
    switch_cont_sim 
      (map … (fst ??) (\snd (function_switch_removal f)))
      (Kcall r f en k)
      (Kcall r (\fst (function_switch_removal f)) en' k').

(* 
 en' = exec_alloc_variables en m (\snd (function_switch_removal f))
 TODO : si variable héréditairement générée depuis [u], alors variable dans \snd (function_switch_removal f) et donc
        variable dans en'. 

        1) Pb: je voudrais que les noms générés dans (switch_removal s u) soient les mêmes que 
           dans (function_switch_removal f). Pas faisable. Ce dont on a réellement besoin, c'est
           de savoir que :
           si je lookup une variable générée à partir d'un univers frais dans l'environement en',
           alors j'aurais un hit. L'environnement en' doit être à la fois fixe de step en step,
           et contenir tout ce qui est généré par u. Donc, on contraint u à etre "fresh for s"
           et à etre "(function_switch_removal f)-contained".

        2) J'aurais surement besoin de l'hypothèse de freshness pour montrer que le lookup
           et l'update n'altèrent pas le comportement du reste du programme.

        relation : si un statement S0 est inclus dans un statement S1, alors les variables générées
                   depuis tout freshgen u sur S0 sont inclus dans celles générées pour S1.
                   en particulier, si u est frais pour S1 u est frais pour S0.

        Montrer que "environment_extension en en' (\snd (function_switch_removal f))" implique
                    "environment_extension en en' (\fst (\fst (switch_removal s u)))"
                    
 ---------------------------------------------------------------
 . constante de la transformation: exec_step laisse $en$ et $m$ invariants, sauf lors d'un appel de fonction
   et d'updates. Il est donc impossible d'allouer les variables sur [en] au fur et à mesure de leur génération.
   on doit donc utiliser l'env créé lors de l'allocation de la fonction. Conséquence directe : on doit donner
   en argument les freshgens qui correspondent à ce que la fonction switch_removal fait.
*)

(*  env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
    env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →  *)
record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
  rg_find_symbol: ∀s.
    find_symbol ? ge s = find_symbol ? ge' s;
  rg_find_funct: ∀v,f.
    find_funct ? ge v = Some ? f →
    find_funct ? ge' v = Some ? (t f);
  rg_find_funct_ptr: ∀b,f.
    find_funct_ptr ? ge b = Some ? f →
    find_funct_ptr ? ge' b = Some ? (t f)
}.

(* This record aims to shorten the definition of the simulation relation on states more readeable. *)
inductive switch_state_sim (ge : genv) : state → state → Prop ≝
| sws_state :
 (* current statement *)
 ∀sss_statement  : statement.
 (* statement after transformation *)
 ∀sss_result     : swret statement.
 (* label universe *)
 ∀sss_lu         : universe SymbolTag.
 (* [sss_lu] must be fresh *)
 ∀sss_lu_fresh   : fresh_for_statement sss_statement sss_lu.
 (* current function *)
 ∀sss_func       : function.
 (* current function after translation *)
 ∀sss_func_tr    : function.
 (* variables generated during conversion of the function *) 
 ∀sss_new_vars   : list (ident × type).
 (* statement of the transformation *)  
 ∀sss_func_hyp   : 〈sss_func_tr, sss_new_vars〉 = function_switch_removal sss_func.
 (* memory state before conversion *)
 ∀sss_m          : mem.
 (* memory state after conversion *)
 ∀sss_m_ext      : mem.
 (* environment before conversion *)
 ∀sss_env        : env.
 (* environment after conversion *)
 ∀sss_env_ext    : env.
 (* continuation before conversion *)
 ∀sss_k          : cont.
 (* continuation after conversion *)
 ∀sss_k_ext      : cont.
 (* memory "injection" *)
 ∀sss_mem_hyp    : sr_memext sss_m sss_m_ext.
 (* The extended environment does not interfer with the old one. *)
 ∀sss_env_hyp    : disjoint_extension sss_env sss_m sss_env_ext sss_m_ext sss_new_vars sss_mem_hyp.
 (* conversion of the current statement, using the variables produced during the conversion of the current function *)
 ∀sss_result_hyp : switch_removal sss_statement (map ?? (fst ??) sss_new_vars) sss_lu = Some ? sss_result.
 (* simulation between the continuations before and after conversion. *)
 ∀sss_k_hyp      : switch_cont_sim (map ?? (fst ??) sss_new_vars) sss_k sss_k_ext.  
 ext_fresh_for_genv sss_new_vars ge →
    switch_state_sim
      ge
      (State sss_func sss_statement sss_k sss_env sss_m)
      (State sss_func_tr (ret_st … sss_result) sss_k_ext sss_env_ext sss_m_ext)
| sws_callstate : ∀vars, fd,args,k,k',m.
    switch_cont_sim vars k k' →
    switch_state_sim ge (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m) 
| sws_returnstate : 
 ∀ssr_vars.
 ∀ssr_result.
 ∀ssr_k       : cont.
 ∀ssr_k_ext   : cont.
 ∀ssr_m       : mem.
 ∀ssr_m_ext   : mem.
 ∀ssr_mem_hyp : sr_memext ssr_m ssr_m_ext.
    switch_cont_sim ssr_vars ssr_k ssr_k_ext →
    switch_state_sim ge (Returnstate ssr_result ssr_k ssr_m) (Returnstate ssr_result ssr_k_ext ssr_m_ext)
| sws_finalstate : ∀r.
    switch_state_sim ge (Finalstate r) (Finalstate r).

lemma call_cont_swremoval : ∀fv,k,k'.
  switch_cont_sim fv k k' →
  switch_cont_sim fv (call_cont k) (call_cont k').
#fv #k0 #k0' #K elim K /2/
qed.

(* [eventually ge P s tr] states that after a finite number of [exec_step], the 
   property P on states will be verified. *)
inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝
| eventually_base : ∀s,t,s'.
    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
    P s' →
    eventually ge P s t
| eventually_step : ∀s,t,s',t',trace.
    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
    eventually ge P s' t' →
    trace = (t ⧺ t') →
    eventually ge P s trace.

(* [eventually] is not so nice to use directly, we would like to make the mandatory
 * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not
   to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *)     
lemma eventually_now : ∀ge,P,s,t. 
  (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → 
   eventually ge P s t.
#ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP}  (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *)
qed.

lemma eventually_later : ∀ge,P,s,t. 
   (∃s',tstep.exec_step ge s = Value io_out io_in ? 〈tstep,s'〉 ∧ ∃tnext. t = tstep ⧺ tnext ∧ eventually ge P s' tnext) → 
    eventually ge P s t.
#ge #P #s #t * #s' * #tstep * #Hexec_step * #tnext * #Heq #Heventually %2{s tstep s' tnext … Heq}
try assumption
qed.

lemma exec_lvalue_expr_elim :
  ∀r1,r2,Pok,Qok.
  exec_lvalue_sim r1 r2 →
  (∀val,trace.
    match Pok 〈val,trace〉 with
    [ Error err ⇒ True
    | OK pvt ⇒
      let 〈pval,ptrace〉 ≝ pvt in
      match Qok 〈val,trace〉 with
      [ Error err ⇒ False
      | OK qvt ⇒
        let 〈qval,qtrace〉 ≝ qvt in
        ptrace = qtrace ∧ pval = qval
      ]
    ]) →  
  exec_expr_sim
    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
#r1 #r2 #Pok #Qok whd in ⊢ (% → ?); 
elim r1
[ 2:  #error #_ #_ normalize #a #Habsurd destruct (Habsurd)
| 1: normalize nodelta #a #H lapply (H a (refl ??))
     #Hr2 >Hr2 normalize #H #a' elim a * #b #o #tr
     lapply (H 〈b, o〉 tr) #H1 #H2 >H2 in H1;
     normalize nodelta elim a' in H2; #pval #ptrace #Hpok
     normalize nodelta cases (Qok 〈b,o,tr〉)
     [ 2: #error normalize #Habsurd @(False_ind … Habsurd)
     | 1: * #qval #qtrace normalize nodelta * #Htrace #Hval
          destruct @refl
] ] qed.


lemma exec_expr_expr_elim :
  ∀r1,r2,Pok,Qok.
  exec_expr_sim r1 r2 →
  (∀val,trace.
    match Pok 〈val,trace〉 with
    [ Error err ⇒ True
    | OK pvt ⇒
      let 〈pval,ptrace〉 ≝ pvt in
      match Qok 〈val,trace〉 with
      [ Error err ⇒ False
      | OK qvt ⇒
        let 〈qval,qtrace〉 ≝ qvt in
        ptrace = qtrace ∧ pval = qval
      ]
    ]) → 
  exec_expr_sim 
    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
#r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
elim r1
[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
| 1: normalize nodelta #a #H lapply (H a (refl ??))
     #Hr2 >Hr2 normalize nodelta #H
     elim a in Hr2; #val #trace
     lapply (H … val trace)
     cases (Pok 〈val, trace〉)
     [ 2: #error normalize #_ #_ #a' #Habsurd destruct (Habsurd)
     | 1: * #pval #ptrace normalize nodelta
          cases (Qok 〈val,trace〉)
          [ 2: #error normalize #Hfalse @(False_ind … Hfalse)
          | 1: * #qval #qtrace normalize nodelta * #Htrace_eq #Hval_eq
               #Hr2_eq destruct #a #H @H
] ] ] qed.


lemma load_value_of_type_inj : ∀m1,m2,b,off,ty.
    sr_memext m1 m2 → ∀v.
    load_value_of_type ty m1 b off = Some ? v →
    load_value_of_type ty m2 b off = Some ? v.
#m1 #m2 #b #off #ty #Hinj #v
@(load_sim_fe … (me_inj … Hinj) (mk_pointer b off))
qed.

(* Conservation of the smenantics of binary operators *)
lemma sim_sem_binary_operation : ∀op,v1,v2,e1,e2,m1,m2.
  ∀Hext:sr_memext m1 m2. ∀res.
  sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m1 = Some ? res →
  sem_binary_operation op v1 (typeof e1) v2 (typeof e2) m2 = Some ? res.
#op #v1 #v2 #e1 #e2 #m1 #m2 #Hmemext #res cases op
whd in match (sem_binary_operation ??????);
try //
whd in match (sem_binary_operation ??????);
elim m1 in Hmemext; #contents1 #nextblocks1 #Hnextpos1
elim m2 #contents2 #nextblocks2 #Hnextpos2
* #Hptrsim #writeable #Hvalid #Hdisjoint #Hvalid_cons
whd in match (sem_cmp ??????);
whd in match (sem_cmp ??????);
[ 1: cases (classify_cmp (typeof e1) (typeof e2))
     normalize nodelta
     [ 1: #sz #sg try //
     | 2: #opt #ty
          cases v1 normalize nodelta
          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
          [ 1,2,3: #Habsurd destruct (Habsurd)
          | 4: #H @H ]
          cases v2 normalize nodelta
          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
          [ 1,2,3: #Habsurd destruct (Habsurd)
          | 4: #H @H ]
          lapply (Hvalid_cons ptr)
          elim (freed_pointer_dec … (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
          [ 2: #Hnot_freed #Hvalid lapply (Hvalid … Hnot_freed)
               cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
               [ 2: >andb_lsimpl_false normalize nodelta #_ #Habsurd destruct (Habsurd) ]
               #Hvalid >(Hvalid (refl ??))
               lapply (Hvalid_cons ptr')
               elim (freed_pointer_dec … (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
               [ 2: #Hnot_freed' #Hvalid' lapply (Hvalid' … Hnot_freed')
                    cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
                    [ 2: >andb_lsimpl_true #_ normalize nodelta #Habsurd destruct (Habsurd) ]
                    #H' >(H' (refl ??)) >andb_lsimpl_true #Hres @Hres
               | 1: normalize in ⊢ (% → ?); * #Hlow' #Hhigh' #_
                    >andb_lsimpl_true >andb_lsimpl_true
                    whd in match (valid_pointer ??);
                    whd in match (low_bound ??);
                    whd in match (high_bound ??);
                    >Hlow' >Hhigh' >Zleb_unsigned_OZ >andb_comm >andb_lsimpl_true
                    whd in match (valid_pointer ??);
               
               cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
               [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
               #H' >(H' (refl ??)) #Hok @Hok
          | 1:
          ]
     | 3: #fsz #H @H
     | 4: #ty1 #ty2 #H @H ]
| 2: cases (classify_cmp (typeof e1) (typeof e2))
     normalize nodelta
     [ 1: #sz #sg try //
     | 2: #opt #ty
          cases v1 normalize nodelta
          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
          [ 1,2,3: #Habsurd destruct (Habsurd)
          | 4: #H @H ]
          cases v2 normalize nodelta
          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
          [ 1,2,3: #Habsurd destruct (Habsurd)
          | 4: #H @H ]
          lapply (Hvalid_cons ptr)
          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
          #H >(H (refl ??))
          lapply (Hvalid_cons ptr')
          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
          #H' >(H' (refl ??)) #Hok @Hok
     | 3: #fsz #H @H
     | 4: #ty1 #ty2 #H @H ]
| 3: cases (classify_cmp (typeof e1) (typeof e2))
     normalize nodelta
     [ 1: #sz #sg try //
     | 2: #opt #ty
          cases v1 normalize nodelta
          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
          [ 1,2,3: #Habsurd destruct (Habsurd)
          | 4: #H @H ]
          cases v2 normalize nodelta
          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
          [ 1,2,3: #Habsurd destruct (Habsurd)
          | 4: #H @H ]
          lapply (Hvalid_cons ptr)
          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
          #H >(H (refl ??))
          lapply (Hvalid_cons ptr')
          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
          #H' >(H' (refl ??)) #Hok @Hok
     | 3: #fsz #H @H
     | 4: #ty1 #ty2 #H @H ]
| 4: cases (classify_cmp (typeof e1) (typeof e2))
     normalize nodelta
     [ 1: #sz #sg #H @H          
     | 2: #opt #ty
          cases v1 normalize nodelta
          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
          [ 1,2,3: #Habsurd destruct (Habsurd)
          | 4: #H @H ]
          cases v2 normalize nodelta
          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
          [ 1,2,3: #Habsurd destruct (Habsurd)
          | 4: #H @H ]
          lapply (Hvalid_cons ptr)
          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
          #H >(H (refl ??))
          lapply (Hvalid_cons ptr')
          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
          #H' >(H' (refl ??)) #Hok @Hok
     | 3: #fsz #H @H
     | 4: #ty1 #ty2 #H @H ]
| 5: cases (classify_cmp (typeof e1) (typeof e2))
     normalize nodelta
     [ 1: #sz #sg #H @H          
     | 2: #opt #ty
          cases v1 normalize nodelta
          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
          [ 1,2,3: #Habsurd destruct (Habsurd)
          | 4: #H @H ]
          cases v2 normalize nodelta
          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
          [ 1,2,3: #Habsurd destruct (Habsurd)
          | 4: #H @H ]
          lapply (Hvalid_cons ptr)
          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
          #H >(H (refl ??))
          lapply (Hvalid_cons ptr')
          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
          #H' >(H' (refl ??)) #Hok @Hok
     | 3: #fsz #H @H
     | 4: #ty1 #ty2 #H @H ]
| 6: cases (classify_cmp (typeof e1) (typeof e2))
     normalize nodelta
     [ 1: #sz #sg #H @H          
     | 2: #opt #ty
          cases v1 normalize nodelta
          [ 1: | 2: #sz #i | 3: #fl | 4: | 5: #ptr ]
          [ 1,2,3: #Habsurd destruct (Habsurd)
          | 4: #H @H ]
          cases v2 normalize nodelta
          [ 1: | 2: #sz' #i' | 3: #fl' | 4: | 5: #ptr' ]
          [ 1,2,3: #Habsurd destruct (Habsurd)
          | 4: #H @H ]
          lapply (Hvalid_cons ptr)
          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr)
          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
          #H >(H (refl ??))
          lapply (Hvalid_cons ptr')
          cases (valid_pointer (mk_mem contents1 nextblocks1 Hnextpos1) ptr')
          [ 2: #_ normalize #Habsurd destruct (Habsurd) ]
          #H' >(H' (refl ??)) #Hok @Hok
     | 3: #fsz #H @H
     | 4: #ty1 #ty2 #H @H ]
] qed.


(* Simulation relation on expressions *)
lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
  ∀Hext:sr_memext m1 m2.
  switch_removal_globals ? fundef_switch_removal ge ge' →
  disjoint_extension en1 m1 en2 m2 ext Hext →
  ext_fresh_for_genv ext ge →
  (∀e. exec_expr_sim (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
  (∀ed, ty. exec_lvalue_sim (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).
#ge #ge' #en1 #m1 #en2 #m2 #ext #Hext #Hrelated #Hdisjoint #Hext_fresh_for_genv
@expr_lvalue_ind_combined
[ 1: #csz #cty #i #a1
     whd in match (exec_expr ????); elim cty
     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     normalize nodelta
     [ 2: cases (eq_intsize csz sz) normalize nodelta
          [ 1: #H destruct (H) /4 by ex_intro, conj, vint_eq/
          | 2: #Habsurd destruct (Habsurd) ]
     | 4,5,6: #_ #H destruct (H)
     | *: #H destruct (H) ]
| 2: #ty #fl #a1
     whd in match (exec_expr ????); #H1 destruct (H1) /4 by ex_intro, conj, vint_eq/
| 3: *
  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
  #ty whd in ⊢ (% → ?); #Hind try @I
  whd in match (Plvalue ???);
  [ 1,2,3: whd in match (exec_expr ????); whd in match (exec_expr ????); #a1
       cases (exec_lvalue' ge en1 m1 ? ty) in Hind;
       [ 2,4,6: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
       | 1,3,5: normalize nodelta #b1 #H lapply (H b1 (refl ??)) #Heq >Heq       
           normalize nodelta
           elim b1 * #bl1 #o1 #tr1 (* elim b2 * #bl2 #o2 #tr2 *)
           whd in match (load_value_of_type' ???); 
           whd in match (load_value_of_type' ???);
           lapply (load_value_of_type_inj m1 m2 bl1 o1 ty Hext)
           cases (load_value_of_type ty m1 bl1 o1)
           [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
           | 2,4,6: #v #H normalize in ⊢ (% → ?); #Heq destruct (Heq)
                    >(H v (refl ??)) @refl
  ] ] ]
| 4: #v #ty whd * * #b #o #tr
     whd in match (exec_lvalue' ?????);
     whd in match (exec_lvalue' ?????);
     lapply (Hdisjoint v)
     lapply (Hext_fresh_for_genv v)
     cases (mem_assoc_env v ext) #Hglobal
     [ 1: * #vblock * * #Hlookup_en2 #Hwriteable #Hnot_in_en1
          >Hnot_in_en1 normalize in Hglobal ⊢ (% → ?);
          >(Hglobal (refl ??)) normalize
          #Habsurd destruct (Habsurd)
     | 2: normalize nodelta
          cases (lookup ?? en1 v) normalize nodelta
          [ 1: #Hlookup2 <Hlookup2 normalize nodelta
               lapply (rg_find_symbol … Hrelated v) #Heq_find_sym >Heq_find_sym
               #H @H
          | 2: #block
              cases (lookup ?? en2 v) normalize nodelta
              [ 1: #Habsurd destruct (Habsurd)
              | 2: #b #Heq destruct (Heq) #H @H ]
          ]
    ]
| 5: #e #ty whd in ⊢ (% → %);
     whd in match (exec_lvalue' ?????);
     whd in match (exec_lvalue' ?????);
     cases (exec_expr ge en1 m1 e)
     [ 1: * #v1 #tr1 #H elim (H 〈v1,tr1〉 (refl ??)) * #v1' #tr1' #H @H
     | 2: #error #_ normalize #a1 #Habsurd destruct (Habsurd) ]
| 6: #ty #e #ty'
     #Hsim @(exec_lvalue_expr_elim … Hsim)
     cases ty
     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     * #b #o normalize nodelta try /2 by I/
     #tr @conj try @refl
| 7: #ty #op #e
     #Hsim @(exec_expr_expr_elim … Hsim) #v #trace
     cases (sem_unary_operation op v (typeof e)) normalize nodelta
     try @I
     #v @conj @refl
| 8: #ty #op #e1 #e2 #Hsim1 #Hsim2
     @(exec_expr_expr_elim … Hsim1) #v #trace
     cases (exec_expr ge en1 m1 e2) in Hsim2;
     [ 2: #error // ]
     * #pval #ptrace normalize in ⊢ (% → ?); #Hsim2
     whd in match (m_bind ?????);
     >(Hsim2 ? (refl ??))
     whd in match (m_bind ?????);
     lapply (sim_sem_binary_operation op v pval e1 e2 m1 m2 Hext)
     cases (sem_binary_operation op v (typeof e1) pval (typeof e2) m1)
     [ 1: #_ // ] #val #H >(H val (refl ??))
     normalize destruct @conj @refl
| 9: #ty #cast_ty #e #Hsim @(exec_expr_expr_elim … Hsim)
     #v #tr
     cut (exec_cast m1 v (typeof e) cast_ty = exec_cast m2 v (typeof e) cast_ty)
     [ @refl ]
     #Heq >Heq     
     cases (exec_cast m2 v (typeof e) cast_ty)
     [ 2: //
     | 1: #v normalize @conj @refl ]
| 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3
     @(exec_expr_expr_elim … Hsim1) #v #tr
     cases (exec_bool_of_val ? (typeof e1)) #b
     [ 2: normalize @I ]
     cases b normalize nodelta
     whd in match (m_bind ?????);
     whd in match (m_bind ?????);
     normalize nodelta
     [ 1: (* true branch *)
          cases (exec_expr ge en1 m1 e2) in Hsim2;
          [ 2: #error normalize #_ @I
          | 1: * #e2v #e2tr normalize #H >(H ? (refl ??)) normalize nodelta
               @conj @refl ]
     | 2: (* false branch *)
          cases (exec_expr ge en1 m1 e3) in Hsim3;
          [ 2: #error normalize #_ @I
          | 1: * #e3v #e3tr normalize #H >(H ? (refl ??)) normalize nodelta
               @conj @refl ] ]
| 11,12: #ty #e1 #e2 #Hsim1 #Hsim2
     @(exec_expr_expr_elim … Hsim1) #v #tr
     cases (exec_bool_of_val v (typeof e1))
     [ 2,4: #error normalize @I ]
     *
     whd in match (m_bind ?????);
     whd in match (m_bind ?????);
     [ 2,3: normalize @conj try @refl ]
     cases (exec_expr ge en1 m1 e2) in Hsim2;
     [ 2,4: #error #_ normalize @I ]
     * #v2 #tr2 whd in ⊢ (% → %); #H2 normalize nodelta >(H2 ? (refl ??))
     normalize nodelta
     cases (exec_bool_of_val v2 (typeof e2))
     [ 2,4: #error normalize @I ]
     * normalize @conj @refl
| 13: #ty #ty' cases ty
     [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n 
     | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
     whd in match (exec_expr ????); whd #a #H @H
| 14: #ty #ed #aggregty #i #Hsim whd * * #b #o #tr
    whd in match (exec_lvalue' ?????);
    whd in match (exec_lvalue' ge' en2 m2 (Efield (Expr ed aggregty) i) ty);
    whd in match (typeof ?);
    cases aggregty in Hsim;
    [ 1: | 2: #sz' #sg' | 3: #fl' | 4: #ty' | 5: #ty' #n'
    | 6: #tl' #ty' | 7: #id' #fl' | 8: #id' #fl' | 9: #ty' ]
    normalize nodelta #Hsim
    [ 1,2,3,4,5,6,9: #Habsurd destruct (Habsurd) ]
    whd in match (m_bind ?????);
    whd in match (m_bind ?????);
    whd in match (exec_lvalue ge en1 m1 (Expr ed ?));
    cases (exec_lvalue' ge en1 m1 ed ?) in Hsim;
    [ 2,4: #error #_ normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
    * * #b1 #o1 #tr1 whd in ⊢ (% → ?); #H
    whd in match (exec_lvalue ge' en2 m2 (Expr ed ?));    
     >(H ? (refl ??)) normalize nodelta #H @H
| 15: #ty #l #e #Hsim
     @(exec_expr_expr_elim … Hsim) #v #tr normalize nodelta @conj //
| 16: *
  [ 1: #sz #i | 2: #fl | 3: #var_id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
  | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
  #ty normalize in ⊢ (% → ?);
  [ 3,4,13: @False_ind
  | *: #_ normalize #a1 #Habsurd @Habsurd ]
] qed.



(*
lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
related_globals ? fundef_switch_removal ge ge' →
∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m args).
#ge #ge' #en #m #Hrelated #args
elim args
[ 1: /3/
| 2: #hd #tl #Hind normalize
     elim (sim_related_globals ge ge' en m Hrelated)
     #Hexec_sim #Hlvalue_sim lapply (Hexec_sim hd)
     cases (exec_expr ge en m hd)
     [ 2: #error #_  @SimFail /2 by refl, ex_intro/
     | 1: * #val_hd #trace_hd normalize nodelta
          cases Hind
          [ 2: * #error #Heq >Heq #_ @SimFail /2 by ex_intro/
          | 1: cases (exec_exprlist ge en m tl)
               [ 2: #error #_ #Hexec_hd @SimFail /2 by ex_intro/
               | 1: * #values #trace #H >(H 〈values, trace〉 (refl ??))
                    normalize nodelta #Hexec_hd @SimOk * #values2 #trace2 #H2
                    cases Hexec_hd
                    [ 2: * #error #Habsurd destruct (Habsurd)
                    | 1: #H >(H 〈val_hd, trace_hd〉 (refl ??)) normalize destruct // ]
] ] ] ] qed.
*)

(* The return type of any function is invariant under switch removal *)
lemma fn_return_simplify : ∀f. fn_return (\fst (function_switch_removal f)) = fn_return f.
#f elim f #r #args #vars #body whd in match (function_switch_removal ?); @refl
qed.

(* Similar stuff for fundefs *)
lemma fundef_type_simplify : ∀clfd. type_of_fundef clfd = type_of_fundef (fundef_switch_removal clfd).
* // qed.

(*
lemma expr_fresh_lift : 
  ∀e,u,id. 
      fresh_for_expression e u →
      fresh_for_univ SymbolTag id u →
      fresh_for_univ SymbolTag (max_of_expr e id) u.
#e #u #id
normalize in match (fresh_for_expression e u);
#H1 #H2
>max_of_expr_rewrite
normalize in match (fresh_for_univ ???);
cases (max_of_expr e ?) in H1; #p #H1 
cases id in H2; #p' #H2
normalize nodelta
cases (leb p p') normalize nodelta
[ 1: @H2 | 2: @H1 ]
qed. *)

lemma while_fresh_lift : ∀e,s,cl,u.
   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s cl) u.
#e #s #cl * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Swhile ???));
cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
cases (leb e s) try /2/
qed.

(*
lemma while_commute : ∀e0, s0, us0. Swhile e0 (switch_removal s0 us0) = (sw_rem (Swhile e0 s0) us0).
#e0 #s0 #us0 normalize 
cases (switch_removal s0 us0) * #body #newvars #u' normalize //
qed.*)

lemma dowhile_fresh_lift : ∀e,s,u.
   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Sdowhile e s) u.
#e #s * #u whd in ⊢ (% → % → %); whd in match (max_of_statement (Sdowhile ??));
cases (max_of_expr e) #e cases (max_of_statement s) #s normalize
cases (leb e s) try /2/
qed.
(*
lemma dowhile_commute : ∀e0, s0, us0. Sdowhile e0 (sw_rem s0 us0) = (sw_rem (Sdowhile e0 s0) us0).
#e0 #s0 #us0 normalize
cases (switch_removal s0 us0) * #body #newvars #u' normalize //
qed.*)

lemma for_fresh_lift : ∀cond,step,body,u. 
  fresh_for_statement step u → 
  fresh_for_statement body u → 
  fresh_for_expression cond u → 
  fresh_for_statement (Sfor Sskip cond step body) u.
#cond #step #body #u
whd in ⊢ (% → % → % → %); whd in match (max_of_statement (Sfor ????));
cases (max_of_statement step) #s
cases (max_of_statement body) #b
cases (max_of_expr cond) #c
whd in match (max_of_statement Sskip); 
>(max_id_commutative least_identifier)
>max_id_one_neutral normalize nodelta
normalize elim u #u
cases (leb s b) cases (leb c b) cases (leb c s) try /2/
qed.

(*
lemma for_commute : ∀e,stm1,stm2,u,uA.
   (uA=\snd  (switch_removal stm1 u)) → 
   sw_rem (Sfor Sskip e stm1 stm2) u = (Sfor Sskip e (sw_rem stm1 u) (sw_rem stm2 uA)).
#e #stm1 #stm2 #u #uA #HuA
whd in match (sw_rem (Sfor ????) u);
whd in match (switch_removal ??);   
destruct
normalize in match (\snd (switch_removal Sskip u));
whd in match (sw_rem stm1 u);
cases (switch_removal stm1 u)
* #stm1' #fresh_vars #uA normalize nodelta
whd in match (sw_rem stm2 uA);
cases (switch_removal stm2 uA)
* #stm2' #fresh_vars2 #uB normalize nodelta
//
qed.*)

(*
lemma simplify_is_not_skip: ∀s,u.s ≠ Sskip → ∃pf. is_Sskip (sw_rem s u) = inr … pf.
*
[ 1: #u * #Habsurd elim (Habsurd (refl ? Sskip))
| 2: #e1 #e2 #u #_ 
     whd in match (sw_rem ??);
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/
| 3: #ret #f #args #u
     whd in match (sw_rem ??);
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/
| 4: #s1 #s2 #u
     whd in match (sw_rem ??);
     whd in match (switch_removal ??);     
     cases (switch_removal ? ?) * #a #b #c #d normalize nodelta
     cases (switch_removal ? ?) * #e #f #g normalize nodelta     
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/
| 5: #e #s1 #s2 #u #_
     whd in match (sw_rem ??);
     whd in match (switch_removal ??);     
     cases (switch_removal ? ?) * #a #b #c normalize nodelta
     cases (switch_removal ? ?) * #e #f #h normalize nodelta
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/
| 6,7: #e #s #u #_
     whd in match (sw_rem ??);
     whd in match (switch_removal ??);     
     cases (switch_removal ? ?) * #a #b #c normalize nodelta
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/
| 8: #s1 #e #s2 #s3 #u #_     
     whd in match (sw_rem ??);
     whd in match (switch_removal ??);     
     cases (switch_removal ? ?) * #a #b #c normalize nodelta
     cases (switch_removal ? ?) * #e #f #g normalize nodelta
     cases (switch_removal ? ?) * #i #j #k normalize nodelta
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/
| 9,10: #u #_     
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/
| 11: #e #u #_
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/
| 12: #e #ls #u #_
     whd in match (sw_rem ??);
     whd in match (switch_removal ??);
     cases (switch_removal_branches ? ?) * #a #b #c normalize nodelta
     cases (fresh ??) #e #f normalize nodelta
     normalize in match (simplify_switch ???);
     cases (fresh ? f) #g #h normalize nodelta
     cases (produce_cond ????) * #k #l #m normalize nodelta
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/
| 13,15: #lab #st #u #_
     whd in match (sw_rem ??);
     whd in match (switch_removal ??);
     cases (switch_removal ? ?) * #a #b #c normalize nodelta
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/
| 14: #lab #u     
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/ ]
qed.
*)

(*
lemma sw_rem_commute : ∀stm,u.
  (\fst (\fst (switch_removal stm u))) = sw_rem stm u.
#stm #u whd in match (sw_rem stm u); // qed.
*)

lemma fresh_for_statement_inv : 
  ∀u,s. fresh_for_statement s u →
        match u with
        [ mk_universe p ⇒ le (p0 one) p ]. 
* #p #s whd in match (fresh_for_statement ??);
cases (max_of_statement s) #s
normalize /2/ qed.

lemma fresh_for_Sskip :
  ∀u,s. fresh_for_statement s u → fresh_for_statement Sskip u.
#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.

lemma fresh_for_Sbreak :
  ∀u,s. fresh_for_statement s u → fresh_for_statement Sbreak u.
#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.

lemma fresh_for_Scontinue :
  ∀u,s. fresh_for_statement s u → fresh_for_statement Scontinue u.
#u #s #H lapply (fresh_for_statement_inv … H) elim u /2/ qed.

(*
lemma switch_removal_eq : ∀s,u. ∃res,fvs,u'. switch_removal s u = 〈res, fvs, u'〉.
#s #u elim (switch_removal s u) * #res #fvs #u'
%{res} %{fvs} %{u'} //
qed.

lemma switch_removal_branches_eq : ∀switchcases, u. ∃res,fvs,u'. switch_removal_branches switchcases u = 〈res, fvs, u'〉.
#switchcases #u elim (switch_removal_branches switchcases u) * #res #fvs #u'
%{res} %{fvs} %{u'} //
qed.
*)

lemma produce_cond_eq : ∀e,ls,u,exit_label. ∃s,lab,u'. produce_cond e ls u exit_label = 〈s,lab,u'〉.
#e #ls #u #exit_label cases (produce_cond e ls u exit_label) *
#s #lab #u' %{s} %{lab} %{u'} //
qed.

(* TODO: this lemma ought to be in a more central place, along with its kin of SimplifiCasts.ma ... *)
lemma neq_intsize : ∀s1,s2. s1 ≠ s2 → eq_intsize s1 s2 = false.
* * *
[ 1,5,9: #H @(False_ind … (H (refl ??)))
| *: #_ normalize @refl ]
qed.

lemma exec_expr_int : ∀ge,e,m,expr.
    (∃sz,n,tr. exec_expr ge e m expr = (OK ? 〈Vint sz n, tr〉)) ∨ (∀sz,n,tr. exec_expr ge e m expr ≠ (OK ? 〈Vint sz n, tr〉)).
#ge #e #m #expr cases (exec_expr ge e m expr)
[ 2: #error %2 #sz #n #tr % #H destruct (H)
| 1: * #val #trace cases val
     [ 2: #sz #n %1 %{sz} %{n} %{trace} @refl
     | 3: #fl | 4: | 5: #ptr ]
     %2 #sz #n #tr % #H destruct (H)
] qed.

lemma some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed.

lemma prod_eq_lproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → a = \fst c.
#A #B #a #b * #a' #b' #H destruct @refl
qed.

lemma prod_eq_rproj : ∀A,B : Type[0]. ∀a : A. ∀b : B. ∀c : A × B. 〈a,b〉 = c → b = \snd c.
#A #B #a #b * #a' #b' #H destruct @refl
qed.

(* Main theorem. To be ported and completed to memory injections. TODO *) 
theorem switch_removal_correction :
  ∀ge,ge',s1, s1', tr, s2.
  switch_removal_globals ? fundef_switch_removal ge ge' →
  switch_state_sim ge s1 s1' →
  exec_step ge s1 = Value … 〈tr,s2〉 →
  eventually ge' (λs2'. switch_state_sim ge s2 s2') s1' tr.
#ge #ge' #st1 #st1' #tr #st2 #Hrelated #Hsim_state
inversion Hsim_state
[ 1: (* regular state *)
  #sss_statement #sss_result #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars 
  #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_mem_hyp
  #sss_env_hyp #sss_result_hyp #sss_k_hyp #Hext_fresh_for_ge
  elim (sim_related_globals … ge ge' 
             sss_env sss_m sss_env_ext sss_m_ext sss_new_vars
             sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge)
  #Hsim_expr #Hsim_lvalue #Hst1_eq #Hst1_eq' #_
  cases sss_statement in sss_lu_fresh sss_result_hyp;
  (* Perform the intros for the statements *)
  [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
  | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
  | 14: #lab | 15: #cost #body ]
  #sss_lu_fresh #sss_result_hyp
  [ 1: (* Skip *)
    whd in match (switch_removal ???) in sss_result_hyp;
    <(some_inj ??? sss_result_hyp)
    inversion sss_k_hyp normalize nodelta
    [ 1: #fvs #Hfvs_eq #Hk #Hk' #_ #Hexec_step
         @(eventually_now ????) whd in match (exec_step ??);
         >(prod_eq_lproj ????? sss_func_hyp)
         >fn_return_simplify
         whd in match (exec_step ??) in Hexec_step;
         cases (fn_return sss_func) in Hexec_step;
         [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
         normalize nodelta
         whd in ⊢ ((??%?) → ?);
         [ 1: #H destruct (H) %{(Returnstate Vundef Kstop (free_list sss_m_ext (blocks_of_env sss_env_ext)))}
              @conj try @refl %3{(map (ident×type) ident \fst sss_new_vars)} try //
                %{(Returnstate Vundef Kstop (free1_list sss_m_ext (blocks_of_env sss_env_ext)))} @conj try //
                normalize in Heq_env; destruct (Heq_env)
                %3 //
(*                cut (blocks_of_env e = blocks_of_env e')
                [ normalize in match (\snd (\fst (switch_removal ??))) in Henv_incl;
                  lapply (environment_extension_nil … Henv_incl) #Himap_eq @(blocks_of_env_eq … Himap_eq) ]
                #Heq >Heq %3 // *)
         | *: #H destruct (H) ]
    | 2: #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
         whd in match (ret ??) in Heq; destruct (Heq)
         @(eventually_now ????) whd in match (exec_step ??);
         %{(State (\fst (function_switch_removal f)) (sw_rem s0 us) k0' e' m')} @conj try //
         %1 try //   
    | 3: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
         @(eventually_now ????) whd in match (exec_step ??);
         whd in match (ret ??) in Heq; destruct (Heq)
         %{(State (function_switch_removal f) (Swhile e0 (sw_rem s0 us)) k0' e m)} @conj try //
         >while_commute %1 try //
    | 4: #e0 #s0 #k0 #k0' #us #Hus_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
         @(eventually_now ????) whd in match (exec_step ??);
         lapply (Hexpr_related e0)
         cases (exec_expr ge e m e0) in Heq;
         [ 2: #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
         | 1: * #b #tr whd in match (m_bind ?????); #Heq
              *
              [ 2: * #error #Habsurd destruct (Habsurd)
              | 1: #Hrelated >(Hrelated 〈b,tr〉 (refl ? (OK ? 〈b,tr〉)))
                   whd in match (bindIO ??????);
                   cases (exec_bool_of_val b (typeof e0)) in Heq;
                   [ 2: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
                   | 1: * whd in match (bindIO ??????); #Heq destruct (Heq)
                        whd in match (bindIO ??????);
                        [ 1: %{(State (function_switch_removal f) (Sdowhile e0 (sw_rem s0 us)) k0' e m)}
                             @conj // >dowhile_commute %1 try //
                        | 2: %{(State (function_switch_removal f) Sskip k0' e m)}
                             @conj // %1{us} try //
                             @(fresh_for_Sskip … Hus_fresh)
                        ] ] ] ]
    | 5: #e0 #stm1 #stm2 #k0 #k0' #u #Hu_fresh #Hsim_cont #_ #Hk #Hk' #_ #Heq
         @(eventually_now ????) whd in match (exec_step ??);
         whd in match (ret ??) in Heq; destruct
         %{(State (function_switch_removal f) (sw_rem (Sfor Sskip e0 stm1 stm2) u) k0' e m)}
         @conj try // %1{u} try //
    | 6: #e0 #stm1 #stm2 #k0 #k0' #us #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
         destruct (Heq)
         %{(State (function_switch_removal f) (sw_rem stm1 us) (Kfor3 e0 (sw_rem stm1 us) (sw_rem stm2 uA) k0') e m)}
         @conj try // %1
         [ 2: @swc_for3 //
         | 1: elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) us Hfresh) * // ]
    | 7: #e0 #stm1 #stm2 #k0 #k0' #u #uA #Hfresh #HeqA #Hsim_cont #_ #Hk #Hk' #_ #Heq
         @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in Heq;
         destruct (Heq)
         %{(State (function_switch_removal f) (Sfor Sskip e0 (sw_rem stm1 u) (sw_rem stm2 uA)) k0' e m)}
         @conj try // <(for_commute ??? u uA) try // %1
         [ 2: assumption
         | 1: >HeqA elim (substatement_fresh (Sfor Sskip e0 stm1 stm2) u Hfresh) * // ]
    | 8: #k0 #k0' #Hsim_cont #_ #Hk #Hk' #_ whd in match (ret ??) in ⊢ (% → ?);
         #Heq @(eventually_now ????) whd in match (exec_step ??);
         destruct (Heq)
         %{(State (function_switch_removal f) Sskip k0' e m)} @conj //
         %1{u} //
    | 9: #r #f' #en #k0 #k0' #sim_cont #_ #Hk #Hk' #_ #Heq
         @(eventually_now ????) whd in match (exec_step ??);
         >fn_return_simplify cases (fn_return f) in Heq;
         [ 1: | 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
         normalize nodelta
         [ 1: #H whd in match (ret ??) in H ⊢ %; destruct (H)
              %1{(Returnstate Vundef (Kcall r (function_switch_removal f') en k0') (free_list m (blocks_of_env e)))}
              @conj try // %3 destruct //
         | *: #H destruct (H) ]     
     ]
  | 2: (* Sassign *) normalize nodelta #Heq @(eventually_now ????)
       whd in match (exec_step ??);
       cases lhs in Hu_fresh Heq; #lhs #lhs_type
       cases (Hlvalue_related lhs lhs_type)
       whd in match (exec_lvalue ge e m (Expr ??));
       whd in match (exec_lvalue ge' e m (Expr ??));
       [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd) ]
       cases (exec_lvalue' ge e m lhs lhs_type)
       [ 2: #error #_ whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
       | 1: * * #lblock #loffset #ltrace #H >(H 〈lblock, loffset, ltrace〉 (refl ??))
            whd in match (m_bind ?????);
            cases (Hexpr_related rhs)
            [ 2: * #error #Hfail >Hfail #_
                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
            | 1: cases (exec_expr ge e m rhs)
                 [ 2: #error #_ whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
                 | 1: * #rval #rtrace #H >(H 〈rval, rtrace〉 (refl ??))
                      whd in match (bindIO ??????) in ⊢ (% → % → %);
                      cases (opt_to_io io_out io_in ???) 
                      [ 1: #o #resumption whd in match (bindIO ??????); #_ #Habsurd destruct (Habsurd)
                      | 3: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
                      | 2: #mem #Hfresh whd in match (bindIO ??????); #Heq destruct (Heq)
                           %{(State (function_switch_removal f) Sskip k' e mem)}
                           whd in match (bindIO ??????); @conj //
                           %1{u} try // @(fresh_for_Sskip … Hfresh)
       ] ] ] ]
   | 3: (* Scall *) normalize nodelta #Heq @(eventually_now ????)
        whd in match (exec_step ??);
        cases (Hexpr_related func) in Heq;
        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
        | 1: cases (exec_expr ge e m func)
             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
             | 1: * #fval #ftrace #H >(H 〈fval,ftrace〉 (refl ??))
                  whd in match (m_bind ?????); normalize nodelta
                  lapply (related_globals_exprlist_simulation ge ge' e m Hrelated)
                  #Hexprlist_sim cases (Hexprlist_sim args)
                  [ 2: * #error #Hfail >Hfail
                       whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
                  | 1: cases (exec_exprlist ge e m args)
                       [ 2: #error #_ whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
                       | 1: * #values #values_trace #Hexprlist >(Hexprlist 〈values,values_trace〉 (refl ??))
                            whd in match (bindIO ??????) in ⊢ (% → %);
                            elim Hrelated #_ #Hfind_funct #_ lapply (Hfind_funct fval)
                            cases (find_funct clight_fundef ge fval)
                            [ 2: #clfd #Hclfd >(Hclfd clfd (refl ??))
                                 whd in match (bindIO ??????) in ⊢ (% → %);
                                 >fundef_type_simplify
                                 cases (assert_type_eq (type_of_fundef (fundef_switch_removal clfd)) (fun_typeof func))
                                 [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                                 | 1: #Heq whd in match (bindIO ??????) in ⊢ (% → %);
                                      cases retv normalize nodelta
                                      [ 1: #Heq2 whd in match (ret ??) in Heq2 ⊢ %; destruct
                                           %{(Callstate (fundef_switch_removal clfd) values
                                                (Kcall (None (block×offset×type)) (function_switch_removal f) e k') m)}
                                           @conj try // %2 try // @swc_call //
                                      | 2: * #retval_ed #retval_type
                                           whd in match (exec_lvalue ge ???);
                                           whd in match (exec_lvalue ge' ???);                                      
                                           elim (Hlvalue_related retval_ed retval_type)
                                           [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
                                           | 1: cases (exec_lvalue' ge e m retval_ed retval_type)
                                                [ 2: #error #_ whd in match (m_bind ?????); #Habsurd
                                                     destruct (Habsurd)
                                                | 1: * * #block #offset #trace #Hlvalue >(Hlvalue 〈block,offset,trace〉 (refl ??))
                                                     whd in match (m_bind ?????) in ⊢ (% → %);
                                                     #Heq destruct (Heq)
                                                     %{(Callstate (fundef_switch_removal clfd) values
                                                        (Kcall (Some ? 〈block,offset,typeof (Expr retval_ed retval_type)〉)
                                                               (function_switch_removal f) e k') m)}
                                                     @conj try //
                                                     %2 @swc_call //
                                ] ] ] ]
                            | 1: #_ whd in match (opt_to_io ?????) in ⊢ (% → %);
                                 whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
       ] ] ] ] ]
   | 4: (* Ssequence *) normalize nodelta
        whd in match (ret ??) in ⊢ (% → ?); #Heq
        @(eventually_now ????) 
        %{(State (function_switch_removal f)
                 (\fst (\fst (switch_removal stm1 u)))
                 (Kseq (\fst  (\fst  (switch_removal stm2 (\snd (switch_removal stm1 u))))) k') e m)}
        @conj
        [ 2: destruct (Heq) %1
             [ 1: elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) //
             | 2: @swc_seq try // @switch_removal_fresh 
                  elim (substatement_fresh (Ssequence stm1 stm2) u Hu_fresh) // ]
        | 1: whd in match (sw_rem ??); whd in match (switch_removal ??);
             cases (switch_removal stm1 u)
             * #stm1' #fresh_vars #u' normalize nodelta
             cases (switch_removal stm2 u')
             * #stm2' #fresh_vars2 #u'' normalize nodelta
             whd in match (exec_step ??);
             destruct (Heq) @refl
        ]
   | 5: (* If-then-else *) normalize nodelta
        whd in match (ret ??) in ⊢ (% → ?); #Heq
        @(eventually_now ????) whd in match (sw_rem ??);
        whd in match (switch_removal ??);
        elim (switch_removal_eq iftrue u) #iftrue' * #fvs_iftrue * #uA #Hiftrue_eq >Hiftrue_eq normalize nodelta
        elim (switch_removal_eq iffalse uA) #iffalse' * #fvs_iffalse * #uB #Hiffalse_eq >Hiffalse_eq normalize nodelta
        whd in match (exec_step ??);
        cases (Hexpr_related cond) in Heq;
        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
        | 1: cases (exec_expr ge e m cond)
             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
                  cases (exec_bool_of_val condval (typeof cond))
                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
                       destruct (Heq_condval) whd in match (bindIO ??????);
                       normalize nodelta
                      [ 1: %{(State (function_switch_removal f) iftrue' k' e m)} @conj try //
                           cut (iftrue' = (\fst (\fst (switch_removal iftrue u))))
                           [ 1: >Hiftrue_eq normalize // ]
                           #Hrewrite >Hrewrite %1
                           elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh) //
                      | 2: %{(State (function_switch_removal f) iffalse' k' e m)} @conj try //
                           cut (iffalse' = (\fst (\fst (switch_removal iffalse uA))))
                           [ 1: >Hiffalse_eq // ]
                           #Hrewrite >Hrewrite %1 try //
                           cut (uA = (\snd (switch_removal iftrue u)))
                           [ 1: >Hiftrue_eq //
                           | 2: #Heq_uA >Heq_uA
                                elim (substatement_fresh (Sifthenelse cond iftrue iffalse) u Hu_fresh)
                                #Hiftrue_fresh #Hiffalse_fresh whd @switch_removal_fresh //
       ] ] ] ] ]
   | 6: (* While loop *) normalize nodelta
        whd in match (ret ??) in ⊢ (% → ?); #Heq
        @(eventually_now ????) whd in match (sw_rem ??);
        whd in match (switch_removal ??);
        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
        whd in match (exec_step ??);
        cases (Hexpr_related cond) in Heq;
        [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
        | 1: cases (exec_expr ge e m cond)
             [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
             | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
                  whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
                  cases (exec_bool_of_val condval (typeof cond))
                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                  | 1: * whd in match (bindIO ??????); normalize nodelta #Heq_condval
                       destruct (Heq_condval) whd in match (bindIO ??????);
                       normalize nodelta
                       [ 1: %{(State (function_switch_removal f) body' (Kwhile cond body' k') e m)} @conj try //
                            cut (body' = (\fst (\fst (switch_removal body u))))
                            [ 1: >Hbody_eq // ]
                            #Hrewrite >Hrewrite %1
                            [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
                            | 2: @swc_while lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
                       | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj //
                            %1{u} try // @(fresh_for_Sskip … Hu_fresh)
        ] ] ] ]
   | 7: (* Dowhile loop *) normalize nodelta
        whd in match (ret ??) in ⊢ (% → ?); #Heq
        @(eventually_now ????) whd in match (sw_rem ??);
        whd in match (switch_removal ??);
        elim (switch_removal_eq body u) #body' * #fvs * #uA #Hbody_eq >Hbody_eq normalize nodelta
        whd in match (exec_step ??);
        destruct (Heq) %{(State (function_switch_removal f) body' (Kdowhile cond body' k') e m)} @conj
        try //
        cut (body' = (\fst (\fst (switch_removal body u))))
        [ 1: >Hbody_eq // ]
        #Hrewrite >Hrewrite %1
        [ 1: elim (substatement_fresh (Swhile cond body) u Hu_fresh) //
        | 2: @swc_dowhile lapply (substatement_fresh (Swhile cond body) u Hu_fresh) // ]
   | 8: (* For loop *) normalize nodelta
        whd in match (ret ??) in ⊢ (% → ?); #Heq
        @(eventually_now ????) whd in match (sw_rem ??);
        whd in match (switch_removal ??);
        cases (is_Sskip init) in Heq; normalize nodelta #Hinit_Sskip
        [ 1: >Hinit_Sskip normalize in match (switch_removal Sskip u); normalize nodelta
              elim (switch_removal_eq step u) #step' *  #fvs_step * #uA #Hstep_eq >Hstep_eq normalize nodelta
              elim (switch_removal_eq body uA) #body' * #fvs_body * #uB #Hbody_eq >Hbody_eq normalize nodelta
              whd in match (exec_step ??);
              cases (Hexpr_related cond)
              [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
              | 1: cases (exec_expr ge e m cond)
                   [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                   | 1: * #condval #condtrace #Heq >(Heq 〈condval, condtrace〉 (refl ??))
                        whd in match (m_bind ?????); whd in match (bindIO ??????) in ⊢ (? → %);
                        cases (exec_bool_of_val condval (typeof cond))
                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                        | 1: * whd in match (bindIO ??????) in ⊢ (% → %); normalize nodelta #Heq_condval
                             destruct (Heq_condval)
                             [ 1: %{(State (function_switch_removal f) body' (Kfor2 cond step' body' k') e m)} @conj
                                  try //
                                  cut (body' = (\fst (\fst (switch_removal body uA))))
                                  [ 1: >Hbody_eq // ]
                                  #Hrewrite >Hrewrite
                                  cut (uA = (\snd (switch_removal step u)))
                                  [ 1: >Hstep_eq // ] #HuA
                                  elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
                                  #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1
                                  [ 1: >HuA @switch_removal_fresh assumption
                                  | 2: cut (step' = (\fst (\fst (switch_removal step u))))
                                       [ >Hstep_eq // ]
                                       #Hstep >Hstep @swc_for2 try assumption
                                       @for_fresh_lift try assumption ]
                             | 2: %{(State (function_switch_removal f) Sskip k' e m)} @conj
                                   try // %1{u} try @(fresh_for_Sskip … Hu_fresh) assumption
               ] ] ] ]
        | 2: #Heq
             elim (switch_removal_eq init u) #init' * #fvs_init * #uA #Hinit_eq >Hinit_eq normalize nodelta
             elim (switch_removal_eq step uA) #step' * #fvs_step * #uB #Hstep_eq >Hstep_eq normalize nodelta
             elim (switch_removal_eq body uB) #body' * #fvs_body * #uC #Hbody_eq >Hbody_eq normalize nodelta
             whd in match (exec_step ??);
             cut (init' = (\fst (\fst (switch_removal init u)))) [ 1: >Hinit_eq // ]
             #Hinit >Hinit elim (simplify_is_not_skip ? u Hinit_Sskip)
             whd in match (sw_rem ??) in ⊢ (? → % → ?); #pf #Hskip >Hskip normalize nodelta
             whd in match (ret ??); destruct (Heq)
             %{(State (function_switch_removal f) (\fst  (\fst  (switch_removal init u))) (Kseq (Sfor Sskip cond step' body') k') e m)}
             @conj try //
             cut (step' = (\fst (\fst (switch_removal step uA)))) [ >Hstep_eq // ] #Hstep' >Hstep'
             cut (body' = (\fst (\fst (switch_removal body uB)))) [ >Hbody_eq // ] #Hbody' >Hbody'
             <for_commute [ 2: >Hstep_eq // ]
             elim (substatement_fresh (Sfor init cond step body) u Hu_fresh) * *
             #Hinit_fresh_u #Hcond_fresh_u #Hstep_fresh_u #Hbody_fresh_u %1{u} try assumption
             @swc_seq try // @for_fresh_lift
             cut (uA = (\snd (switch_removal init u))) [ 1,3,5: >Hinit_eq // ] #HuA_eq
             >HuA_eq @switch_removal_fresh assumption       
       ]
   | 9: (* break *) normalize nodelta
        inversion Hsim_cont
        [ 1: #Hk #Hk' #_        
        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
        normalize nodelta #H try (destruct (H))
        whd in match (ret ??) in H; destruct (H)
        @(eventually_now ????)
        [ 1,4: %{(State (function_switch_removal f) Sbreak k0' e m)} @conj [ 1,3: // | 2,4: %1{u} // ]
        | 2,3,5,6: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try // %1{u} // ]
    | 10: (* Continue *) normalize nodelta
        inversion Hsim_cont
        [ 1: #Hk #Hk' #_        
        | 2: #stm' #k0 #k0' #u0 #Hstm_fresh' #Hconst_cast0 #_ #Hk #Hk' #_
        | 3: #cond #body #k0 #k0' #u0 #Hwhile_fresh #Hconst_cast0 #_ #Hk #Hk' #_
        | 4: #cond #body #k0 #k0' #u0 #Hdowhile_fresh #Hcont_cast0 #_ #Hk #Hk' #_
        | 5: #cond #step #body #k0 #k0' #u0 #Hfor_fresh #Hcont_cast0 #_ #Hk #Hk' #_
        | 6,7: #cond #step #body #k0 #k0' #u0 #uA0 #Hfor_fresh #HuA0 #Hcont_cast0 #_ #Hk #Hk' #_
        | 8: #k0 #k0' #Hcont_cast0 #_ #Hk #Hk' #_
        | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #_ #Hk #Hk' #_ ]
        normalize nodelta #H try (destruct (H))
        @(eventually_now ????) whd in match (exec_step ??); whd in match (ret ??) in H;
        destruct (H)
        [ 1: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u} try assumption
        | 2: %{(State (function_switch_removal f) (Swhile cond (sw_rem body u0)) k0' e m)} @conj try //
             >while_commute %1{u0} try assumption
        | 3: lapply (Hexpr_related cond) cases (exec_expr ge e m cond) in H;
             [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
             | 1: * #condval #trace whd in match (m_bind ?????);
                  #Heq * 
                  [ 2: * #error #Habsurd destruct (Habsurd)
                  | 1: #Hexec lapply (Hexec 〈condval,trace〉 (refl ??)) -Hexec #Hexec >Hexec
                       whd in match (bindIO ??????);
                       cases (exec_bool_of_val condval (typeof cond)) in Heq;
                       [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                       | 1: * #Heq normalize in Heq; destruct (Heq) whd in match (bindIO ??????);
                            [ 1: %{(State (function_switch_removal f) (Sdowhile cond (sw_rem body u0)) k0' e m)} 
                                 @conj try // >dowhile_commute %1{u0} assumption
                            | 2: %{(State (function_switch_removal f) Sskip k0' e m)} @conj try //
                                 %1{u0} try // @(fresh_for_Sskip … Hdowhile_fresh) ]
             ] ] ]
        | 4: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try // %1{u0}
             try // @(fresh_for_Scontinue … Hfor_fresh)
        | 5: %{(State (function_switch_removal f) (sw_rem step u0) (Kfor3 cond (sw_rem step u0) (sw_rem body uA0) k0') e m)}
             @conj try // %1{u0}
             elim (substatement_fresh … Hfor_fresh) * * try //
             #HSskip #Hcond #Hstep #Hbody
             @swc_for3 assumption
        | 6: %{(State (function_switch_removal f) Scontinue k0' e m)} @conj try //
             %1{u} try //
        ]
    | 11: (* Sreturn *) normalize nodelta #Heq
          @(eventually_now ????)
          whd in match (exec_step ??) in Heq ⊢ %;
          cases retval in Heq; normalize nodelta
          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
               whd in match (ret ??) in ⊢ (% → %);
               [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
               | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
               #H destruct (H)
               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env e)))}
               @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
          | 2: #expr >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta
               [ 1: #_ #Habsurd destruct (Habsurd)
               | 2: #_ elim (Hexpr_related expr)
                    [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
                    | 1: cases (exec_expr ??? expr)
                         [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                         | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a)))
                              #Hrewrite >Hrewrite
                              whd in match (m_bind ?????); whd in match (m_bind ?????);
                              #Heq destruct (Heq)
                              %{(Returnstate (\fst  a) (call_cont k') (free_list m (blocks_of_env e)))}
                              @conj [ 1: // | 2: %3 @call_cont_swremoval // ]
         ] ] ] ]
    | 12: (* Sswitch. Main proof case. *) normalize nodelta
          (* Case analysis on the outcome of the tested expression *)
          cases (exec_expr_int ge e m cond)
          [ 2: cases (exec_expr ge e m cond)
               [ 2: #error whd in match (m_bind ?????); #_ #Habsurd destruct (Habsurd)
               | 1: * #val #trace cases val
                    [ 1: | 2: #condsz #condv | 3: #condf | 4: #condrg | 5: #condptr ]
                    whd in match (m_bind ?????);
                    [ 1,3,4,5: #_ #Habsurd destruct (Habsurd)
                    | 2: #Habsurd lapply (Habsurd condsz condv trace) * #Hfalse @(False_ind … (Hfalse (refl ??))) ]  ]
          ]
          * #condsz * #condval * #condtr #Hexec_cond >Hexec_cond
          whd in match (m_bind ?????); #Heq
          destruct (Heq)
          @eventually_later
          whd in match (sw_rem (Sswitch cond switchcases) u);
          whd in match (switch_removal (Sswitch cond switchcases) u);
          elim (switch_removal_branches_eq switchcases u)
          #switchcases' * #new_vars * #uv1 #Hsrb_eq >Hsrb_eq normalize nodelta
          cut (uv1 = (\snd (switch_removal_branches switchcases u)))
          [ 1: >Hsrb_eq // ] #Huv1_eq
          cut (fresh_for_statement (Sswitch cond switchcases) uv1)
          [ 1: >Huv1_eq @switch_removal_branches_fresh assumption ] -Huv1_eq #Huv1_eq
          elim (fresh_eq … Huv1_eq) #switch_tmp * #uv2 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv2_eq normalize nodelta
          whd in match (simplify_switch ???);
          elim (fresh_eq … Huv2_eq) #exit_label * #uv3 * #Hfresh_eq >Hfresh_eq -Hfresh_eq #Huv3_eq normalize nodelta
          lapply (produce_cond_fresh (Expr (Evar switch_tmp) (typeof cond)) exit_label switchcases' uv3 (max_of_statement (Sswitch cond switchcases)) Huv3_eq)
          elim (produce_cond_eq (Expr (Evar switch_tmp) (typeof cond)) switchcases' uv3 exit_label)          
          #result * #top_label * #uv4 #Hproduce_cond_eq >Hproduce_cond_eq normalize nodelta
          #Huv4_eq
          whd in match (exec_step ??);
          %{(State (function_switch_removal f)
                   (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
                   (Kseq (Ssequence result (Slabel exit_label Sskip)) k') e m)}
          %{E0} @conj try @refl
          %{tr} normalize in match (eq ???); @conj try //
          (* execute the conditional *)
          @eventually_later
          (* lift the result of the previous case analysis from [ge] to [ge'] *)
          whd in match (exec_step ??);
          whd in match (exec_lvalue ????);
          
          >(exec_expr_related … Hexec_cond (Hexpr_related cond))
          
  *)

(*
lemma exec_expr_related : ∀ge,ge',e,m,cond,v,tr.
  exec_expr ge e m cond = OK ? 〈v,tr〉 → 
  (res_sim ? (exec_expr ge e m cond) (exec_expr ge' e m cond)) →
  exec_expr ge' e m cond = OK ? 〈v,tr〉.
#ge #ge' #e #m #cond #v #tr #H *
[ 1: #Hsim >(Hsim ? H) //
| 2: * #error >H #Habsurd destruct (Habsurd) ]
qed. *)

(*
lemma switch_simulation :
∀ge,ge',e,m,cond,f,condsz,condval,switchcases,k,k',condtr,u.
 switch_cont_sim k k' →
 (exec_expr ge e m cond=OK (val×trace) 〈Vint condsz condval,condtr〉) →
 fresh_for_statement (Sswitch cond switchcases) u →
 ∃tr'.
 (eventually ge'
  (λs2':state
   .switch_state_sim
    (State f
     (seq_of_labeled_statement (select_switch condsz condval switchcases))
     (Kswitch k) e m) s2')
  (State (function_switch_removal f) (sw_rem (Sswitch cond switchcases) u) k' e m)
  tr').
#ge #ge' #e #m #cond #f #condsz #condval #switchcases #k #k' #tr #u #Hsim_cont #Hexec_cond #Hfresh
whd in match (sw_rem (Sswitch cond switchcases) u);
whd in match (switch_removal (Sswitch cond switchcases) u);
cases switchcases in Hfresh;
[ 1: #default_statement #Hfresh_for_default
     whd in match (switch_removal_branches ??);
     whd in match (select_switch ???); whd in match (seq_of_labeled_statement ?);
     elim (switch_removal_eq default_statement u)
     #default_statement' * #Hdefault_statement_sf * #Hnew_vars * #u' #Hdefault_statement_eq >Hdefault_statement_eq
     normalize nodelta
     cut (u' = (\snd (switch_removal default_statement u)))
     [ 1: >Hdefault_statement_eq // ] #Heq_u'
     cut (fresh_for_statement (Sswitch cond (LSdefault default_statement)) u')
     [ 1: >Heq_u' @switch_removal_fresh @Hfresh_for_default ] -Heq_u' #Heq_u'
     lapply (fresh_for_univ_still_fresh u' ? Heq_u') cases (fresh ? u')
     #switch_tmp #uv2 #Hfreshness lapply (Hfreshness ?? (refl ? 〈switch_tmp, uv2〉))
     -Hfreshness #Heq_uv2 (* We might need to produce some lookup hypotheses here *)
     normalize nodelta
     whd in match (simplify_switch (Expr ??) ?? uv2);
     lapply (fresh_for_univ_still_fresh uv2 ? Heq_uv2) cases (fresh ? uv2)
     #exit_label #uv3 #Hfreshness lapply (Hfreshness ?? (refl ? 〈exit_label, uv3〉))
     -Hfreshness #Heq_uv3
     normalize nodelta whd in match (add_starting_lbl_list ????);
     lapply (fresh_for_univ_still_fresh uv3 ? Heq_uv3) cases (fresh ? uv3)
     #default_lab #uv4 #Hfreshness lapply (Hfreshness ?? (refl ? 〈default_lab, uv4〉))
     -Hfreshness #Heq_uv4
     normalize nodelta
     @(eventually_later ge' ?? E0)
     whd in match (exec_step ??);
     %{(State (function_switch_removal f)
          (Sassign (Expr (Evar switch_tmp) (typeof cond)) cond)
          (Kseq
          (Ssequence
            (Slabel default_lab (convert_break_to_goto default_statement' exit_label))
            (Slabel exit_label Sskip))
          k') e m)} @conj try //
     @(eventually_later ge' ?? E0)
     whd in match (exec_step ??);
     
@chthulhu | @chthulhu
qed. *)