include "Clight/Csyntax.ma".
include "Clight/fresh.ma".
include "basics/lists/list.ma".
include "common/Identifiers.ma".
include "Clight/Cexec.ma".
include "Clight/CexecInd.ma".
include "Clight/frontend_misc.ma".
(*
include "Clight/maps_obsequiv.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.

(* Obsolete. This version generates a nested pseudo-sequence of if-then-elses. *)
(*
let rec produce_cond 
  (e : expr) 
  (switch_cases : stlist) 
  (def_case : ident × sf_statement) 
  (exit : label) on switch_cases : sf_statement × label ≝
match switch_cases with
[ nil ⇒
  match def_case with
  [ mk_Prod default_label default_statement ⇒
    〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉
  ]
| cons switch_case tail ⇒
  let 〈case_label, case_value, case_statement〉 ≝ switch_case in
    match case_value with
    [ mk_DPair sz val ⇒
       let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in
       (* let test ≝ Expr (Ebinop Oeq e e) (Tint I32 Unsigned) in *)
       (* let test ≝ Expr (Econst_int I32 (bvzero 32)) (Tint I32 Signed)  in *)
       let 〈sub_statement, sub_label〉 ≝ produce_cond e tail def_case exit in
       let result ≝
         Sifthenelse test
          (Slabel case_label
            (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)
                       (Sgoto sub_label)))
          (pi1 … sub_statement)
      in
      〈«result, ?», case_label〉
    ]
].
[ 1: normalize @convert_break_lift elim default_statement //
| 2: whd @conj normalize try @conj try //
  [ 1: @convert_break_lift elim case_statement //
  | 2: elim sub_statement // ]
] qed. *)

(* We assume that the expression e is consistely typed w.r.t. the switch branches *)
(*
let rec produce_cond2
  (e : expr)
  (switch_cases : stlist)
  (def_case : ident × sf_statement)
  (exit : label) on switch_cases : sf_statement × label ≝
match switch_cases with
[ nil ⇒
  let 〈default_label, default_statement〉 ≝ def_case in
  〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉
| cons switch_case tail ⇒
  let 〈case_label, case_value, case_statement〉 ≝ switch_case in
  match case_value with
  [ mk_DPair sz val ⇒
    let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in
    let 〈sub_statement, sub_label〉 ≝ produce_cond2 e tail def_case exit in
    let case_statement_res ≝
       Sifthenelse test
        (Slabel case_label
          (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)
                     (Sgoto sub_label)))
        Sskip
    in
    〈«Ssequence case_statement_res (pi1 … sub_statement), ?», case_label〉
  ]
].
[ 1: normalize @convert_break_lift elim default_statement //
| 2: whd @conj
     [ 1: whd @conj try // whd in match (switch_free ?); @conj
          [ 1: @convert_break_lift elim case_statement //
          | 2: // ]
     | 2: elim sub_statement // ]
] 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 ⇒
  do 〈body', acc, fvs', u'〉 ← switch_removal body fvs u;
  ret 〈Swhile e body', 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 ⇒
  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. P s → P (Swhile e s))
  (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 ⇒ Swh e s
    (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. P s → P (Swhile e s))
  (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 #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')) (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.

(*
lemma switch_removal_fresh : ∀i,s,u. 
    fresh_for_univ ? i u → 
    fresh_for_univ ? i (\snd (switch_removal s u)).
#i #s @(statement_ind2 ? (λls. ∀u. fresh_for_univ ? i u →
                                      fresh_for_univ ? i (\snd (switch_removal_branches ls u))) … s)
try //
[ 1: #s1' #s2' #Hind1 #Hind2 #u #Hyp
     whd in match (switch_removal (Ssequence s1' s2') u);
     lapply (Hind1 u Hyp) elim (switch_removal s1' u)
     * #irr1 #irr2 #uA #HuA normalize nodelta
     lapply (Hind2 uA HuA) elim (switch_removal s2' uA)
     * #irr3 #irr4 #uB #HuB normalize nodelta //
| 2: #e #s1' #s2' #Hind1 #Hind2 #u #Hyp
     whd in match (switch_removal (Sifthenelse e s1' s2') u);
     lapply (Hind1 u Hyp) elim (switch_removal s1' u)
     * #irr1 #irr2 #uA #HuA normalize nodelta
     lapply (Hind2 uA HuA) elim (switch_removal s2' uA)
     * #irr3 #irr4 #uB #HuB normalize nodelta //
| 3,4: #e #s' #Hind #u #Hyp
     whd in match (switch_removal ? u);
     lapply (Hind u Hyp) elim (switch_removal s' u)
     * #irr1 #irr2 #uA #HuA normalize nodelta //
| 5: #s1' #e #s2' #s3' #Hind1 #Hind2 #Hind3 #u #Hyp
     whd in match (switch_removal (Sfor s1' e s2' s3') u);
     lapply (Hind1 u Hyp) elim (switch_removal s1' u)
     * #irr1 #irr2 #uA #HuA normalize nodelta
     lapply (Hind2 uA HuA) elim (switch_removal s2' uA)
     * #irr3 #irr4 #uB #HuB normalize nodelta
     lapply (Hind3 uB HuB) elim (switch_removal s3' uB)
     * #irr5 #irr6 #uC #HuC normalize nodelta //
| 6: #e #ls #Hind #u #Hyp
     whd in match (switch_removal (Sswitch e ls) u);
     lapply (Hind u Hyp)
     cases (switch_removal_branches ls u)
     * #irr1 #irr2 #uA #HuA normalize nodelta
     lapply (fresh_for_univ_still_fresh … HuA)
     cases (fresh SymbolTag uA) #v #uA' #Haux lapply (Haux v uA' (refl ? 〈v,uA'〉))
     -Haux #HuA' normalize nodelta
     lapply (simplify_switch_fresh uA' i (Expr (Evar v) (typeof e)) irr1 HuA')
     cases (simplify_switch ???) #stm #uB
     #Haux normalize nodelta //
| 7,8: #label #body #Hind #u #Hyp
     whd in match (switch_removal ? u);
     lapply (Hind u Hyp) elim (switch_removal body u)
     * #irr1 #irr2 #uA #HuA normalize nodelta //
| 9: #defcase #Hind #u #Hyp whd in match (switch_removal_branches ??);
     lapply (Hind u Hyp) elim (switch_removal defcase u)
     * #irr1 #irr2 #uA #HuA normalize nodelta //
| 10: #sz #i0 #s0 #tl #Hind1 #Hind2 #u #Hyp normalize
     lapply (Hind2 u Hyp) elim (switch_removal_branches tl u)
     * #irr1 #irr2 #uA #HuA normalize nodelta
     lapply (Hind1 uA HuA) elim (switch_removal s0 uA)
     * #irr3 #irr4 #uB #HuB //
] qed.

lemma switch_removal_branches_fresh : ∀i,ls,u. 
    fresh_for_univ ? i u → 
    fresh_for_univ ? i (\snd (switch_removal_branches ls u)).
#i #ls @(labeled_statements_ind2 (λs. ∀u. fresh_for_univ ? i u →
                                           fresh_for_univ ? i (\snd (switch_removal s u))) ? … ls)
try /2 by switch_removal_fresh/
[ 1: #s #Hind #u #Hfresh normalize lapply (switch_removal_fresh ? s ? Hfresh)
     cases (switch_removal s u) * //
| 2: #sz #i #s #tl #Hs #Htl #u #Hfresh normalize
     lapply (Htl u Hfresh)
     cases (switch_removal_branches tl u) * normalize nodelta
     #ls' #fvs #u' #Hfresh'
     lapply (Hs u' Hfresh')
     cases (switch_removal s u') * //
] 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_one_neutral : ∀v. max v one = v.
* // qed.

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 transitive_le : transitive ? le. // qed.

lemma le_S_weaken : ∀a,b. le (succ a) b → le a b.
#a #b /2/ qed.

(* cycle of length 1 *)
lemma le_S_contradiction_1 : ∀a. le (succ a) a → False.
* /2 by absurd/ qed.

(* cycle of length 2 *)
lemma le_S_contradiction_2 : ∀a,b. le (succ a) b → le (succ b) a → False.
#a #b #H1 #H2 lapply (le_to_le_to_eq … (le_S_weaken ?? H1) (le_S_weaken ?? H2))
#Heq @(le_S_contradiction_1 a) destruct // qed.

(* cycle of length 3 *)
lemma le_S_contradiction_3 : ∀a,b,c. le (succ a) b → le (succ b) c → le (succ c) a → False.
#a #b #c #H1 #H2 #H3 lapply (transitive_le … H1 (le_S_weaken ?? H2)) #H4
@(le_S_contradiction_2 … H3 H4)
qed.

lemma reflexive_leb : ∀a. leb a a = true.
#a @(le_to_leb_true a a) // qed.

(* This should be somewhere else. *)
lemma associative_max : associative ? max.
#a #b #c
whd in ⊢ (??%%); whd in match (max a b); whd in match (max b c);
lapply (pos_compare_to_Prop a b)
cases (pos_compare a b) whd in ⊢ (% → ?); #Hab
[ 1: >(le_to_leb_true a b) normalize nodelta /2/
     lapply (pos_compare_to_Prop b c)
     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
     [ 1: >(le_to_leb_true b c) normalize nodelta
          lapply (pos_compare_to_Prop a c)
          cases (pos_compare a c) whd in ⊢ (% → ?); #Hac
          [ 1: >(le_to_leb_true a c) /2/
          | 2: destruct cases (leb c c) //
          | 3: (* There is an obvious contradiction in the hypotheses. omega, I miss you *)
               @(False_ind … (le_S_contradiction_3 ??? Hab Hbc Hac))            
          ]
          @le_S_weaken //
     | 2: destruct
          cases (leb c c) normalize nodelta
          >(le_to_leb_true a c) /2/
     | 3: >(not_le_to_leb_false b c) normalize nodelta /2/
          >(le_to_leb_true a b) /2/
     ]
| 2: destruct (Hab) >reflexive_leb normalize nodelta
     lapply (pos_compare_to_Prop b c)
     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
     [ 1: >(le_to_leb_true b c) normalize nodelta
          >(le_to_leb_true b c) normalize nodelta
          /2/
     | 2: destruct >reflexive_leb normalize nodelta
          >reflexive_leb //
     | 3: >(not_le_to_leb_false b c) normalize nodelta
          >reflexive_leb /2/ ]
| 3: >(not_le_to_leb_false a b) normalize nodelta /2/
     lapply (pos_compare_to_Prop b c)
     cases (pos_compare b c) whd in ⊢ (% → ?); #Hbc
     [ 1: >(le_to_leb_true b c) normalize nodelta /2/
     | 2: destruct >reflexive_leb normalize nodelta @refl
     | 3: >(not_le_to_leb_false b c) normalize nodelta
          >(not_le_to_leb_false a b) normalize nodelta
          >(not_le_to_leb_false a c) normalize nodelta
          lapply (transitive_le … Hbc (le_S_weaken … Hab))
          #Hca /2/
     ]
] 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 max_of_expr_rewrite : 
  ∀e,id. max_of_expr e id = max_id (max_of_expr e (an_identifier SymbolTag one)) id.
@(expr_ind2 … (λed,t. ∀id. max_of_expr (Expr ed t) id=max_id (max_of_expr (Expr ed t) (an_identifier SymbolTag one)) id))
[ 1: #ed #t // ]
[ 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
[ 3: * #id_p whd in match (max_of_expr ??); cases var_id #var_p normalize nodelta
     whd in match (max_id ??) in ⊢ (???%);
     >max_one_neutral // ]
[ 1,2,11: * * //
| 3,4,5,7,13: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%); @Hind
| 6,9,10: #Hind1 #Hind2 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%);
     >(Hind1 (max_of_expr e2 (an_identifier SymbolTag one)))
     >max_id_associative
     >Hind1
     cases (max_of_expr e1 ?)
     #v1 <Hind2 @refl
| 8: #Hind1 #Hind2 #Hind3 #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%);
     >Hind1 in ⊢ (??%?); >Hind2 in ⊢ (??%?); >Hind3 in ⊢ (??%?);
     >Hind1 in ⊢ (???%); >Hind2 in ⊢ (???%);
     >max_id_associative >max_id_associative @refl
| 12: #Hind #id whd in match (max_of_expr (Expr ??) ?) in ⊢ (??%%);
      cases field #p normalize nodelta 
      >Hind cases (max_of_expr e1 ?) #e'
      cases id #id'
      whd in match (max_id ??); normalize nodelta
      whd in match (max_id ??); >associative_max @refl
] 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.

(* -----------------------------------------------------------------------------
   Stuff on memory and environments extensions.
   Let us recap: the memory model of a function is in two layers. An environment
   (type [env]) maps identifiers to blocks, and a memory maps blocks
   switch_removal introduces new, fresh variables. What is to be noted is that
   switch_removal modifies both the contents of the "disjoint" part of memory, but
   also where the data is allocated. The first solution considered was to consider
   an extensional equivalence relation on values, saying that equivalent pointers
   point to equivalent values. This has to be a coinductive relation, in order to
   take into account cyclic data structures. Rather than using coinductive types,
   we use the compcert solution, using so-called memory embeddings. 
   ---------------------------------------------------------------------------- *)

(* ---------------- *)
(* auxillary lemmas *)
lemma zlt_succ : ∀a,b. Zltb a b = true → Zltb a (Zsucc b) = true.
#a #b #HA
lapply (Zltb_true_to_Zlt … HA) #HA_prop
@Zlt_to_Zltb_true /2/
qed.

lemma zlt_succ_refl : ∀a. Zltb a (Zsucc a) = true.
#a @Zlt_to_Zltb_true /2/ qed.


definition le_offset : offset → offset → bool ≝
  λx,y. Zleb (offv x) (offv y).
  
lemma not_refl_absurd : ∀A:Type[0].∀x:A. x ≠ x → False. /2/. qed.

lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed.

(* When equality on A is decidable, [mem A elt l] is too. *)
lemma mem_dec : ∀A:Type[0]. ∀eq:(∀a,b:A. a = b ∨ a ≠ b). ∀elt,l. mem A elt l ∨ ¬ (mem A elt l).
#A #dec #elt #l elim l
[ 1: normalize %2 /2/
| 2: #hd #tl #Hind
     elim (dec elt hd)
     [ 1: #Heq >Heq %1 /2/
     | 2: #Hneq cases Hind
        [ 1: #Hmem %1 /2/
        | 2: #Hnmem %2 normalize
              % #H cases H
              [ 1: lapply Hneq * #Hl #Eq @(Hl Eq)
              | 2: lapply Hnmem * #Hr #Hmem @(Hr Hmem) ]
] ] ]
qed.

lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b.
#a #b @(eq_block_elim … a b) /2/ qed.

lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2.
#l #elt1 #elt2 elim l
[ 1: normalize #Habsurd @(False_ind … Habsurd)
| 2: #hd #tl #Hind normalize #Hl #Hr
   cases Hl
   [ 1: #Heq >Heq
        @(eq_block_elim … hd elt2)
        [ 1: #Heq >Heq /2 by not_to_not/
        | 2: #x @x ]
   | 2: #Hmem1 cases (mem_dec … block_eq_dec elt2 tl)
        [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2
        | 2: #Hmem2 @Hind //
        ]
   ]
] qed.

lemma neq_block_eq_block_false : ∀b1,b2:block. b1 ≠ b2 → eq_block b1 b2 = false.
#b1 #b2 * #Hb
@(eq_block_elim … b1 b2)
[ 1: #Habsurd @(False_ind … (Hb Habsurd))
| 2: // ] qed.

(* Type of blocks in a particular region. *)
definition block_in : region → Type[0] ≝ λrg. Σb. (block_region b) = rg.

(* An embedding is a function from blocks to (blocks+offset). *)
definition embedding ≝ block → option (block × offset).

definition offset_plus : offset → offset → offset ≝
  λo1,o2. mk_offset (offv o1 + offv o2).
  
lemma offset_plus_O : ∀o. offset_plus o (mk_offset OZ) = o.
* #z normalize // qed.

(* Translates a pointer through an embedding. *)
definition pointer_translation : ∀p:pointer. ∀E:embedding. option pointer ≝
λp,E.
match p with
[ mk_pointer pblock poff ⇒
   match E pblock with
   [ None ⇒ None ?
   | Some loc ⇒
    let 〈dest_block,dest_off〉 ≝ loc in
    let ptr ≝ (mk_pointer dest_block (offset_plus poff dest_off)) in
    Some ? ptr
   ]
].

(* We parameterise the "equivalence" relation on values with an embedding. *)
(* Front-end values. *)
inductive value_eq (E : embedding) : val → val → Prop ≝
| undef_eq : ∀v.
  value_eq E Vundef v
| vint_eq : ∀sz,i. 
  value_eq E (Vint sz i) (Vint sz i)
| vfloat_eq : ∀f.
  value_eq E (Vfloat f) (Vfloat f)
| vnull_eq :
  value_eq E Vnull Vnull
| vptr_eq : ∀p1,p2.
  pointer_translation p1 E = Some ? p2 →
  value_eq E (Vptr p1) (Vptr p2).
  
(* [load_sim] states the fact that each successful load in [m1] is matched by such a load in [m2] s.t.
 * the values are equivalent. *)
definition load_sim ≝
λ(E : embedding).λ(m1 : mem).λ(m2 : mem).
 ∀b1,off1,b2,off2,ty,v1.
  valid_block m1 b1 →
  E b1 = Some ? 〈b2,off2〉 →
  load_value_of_type ty m1 b1 off1 = Some ? v1 →
  (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2).

(* Definition of a memory injection *)
record memory_inj (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
{ (* Load simulation *)
  mi_inj : load_sim E m1 m2;
  (* Invalid blocks are not mapped *)
  mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?;
  (* Blocks in the codomain are valid *)
  mi_incl : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b';
  (* Regions are preserved *)
  mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b';
  (* Disjoint blocks are mapped to disjoint blocks. Note that our condition is stronger than compcert's.
   * This may cause some problems if we reuse this def for the translation from Clight to Cminor, where
   * all variables are allocated in the same block. *)
  mi_disjoint : ∀b1,b2,b1',b2',o1',o2'. 
                b1 ≠ b2 →
                E b1 = Some ? 〈b1',o1'〉 →
                E b2 = Some ? 〈b2',o2'〉 →
                b1' ≠ b2'
}.

(* Definition of a memory extension. /!\ Not equivalent to the compcert concept. /!\ 
 * A memory extension is a [memory_inj] with some particular blocks designated *)

alias id "meml" = "cic:/matita/basics/lists/list/mem.fix(0,2,1)".

record memory_ext (E : embedding) (m1 : mem) (m2 : mem) : Type[0] ≝
{ me_inj : memory_inj E m1 m2;
  me_writeable : list block;
  me_writeable_valid : ∀b. meml ? b me_writeable → valid_block m2 b;
  me_writeable_ok : ∀b,b',o'. 
                    valid_block m1 b → 
                    E b = Some ? 〈b',o'〉 →
                    ¬ (meml ? b' me_writeable)
}.

(* ---------------------------------------------------------------------------- *)
(* End of the definitions on memory injections. Now, on to proving some lemmas. *)

(* A particular inversion. *)
lemma value_eq_ptr_inversion : 
  ∀E,p1,v. value_eq E (Vptr p1) v → ∃p2. v = Vptr p2 ∧ pointer_translation p1 E = Some ? p2.
#E #p1 #v #Heq inversion Heq
[ 1: #v #Habsurd destruct (Habsurd)
| 2: #sz #i #Habsurd destruct (Habsurd)
| 3: #f #Habsurd destruct (Habsurd)
| 4:  #Habsurd destruct (Habsurd)
| 5: #p1' #p2 #Heq #Heqv #Heqv2 #_ destruct 
     %{p2} @conj try @refl try assumption
] qed.
 
(* If we succeed to load something by value from a 〈b,off〉 location, 
   [b] is a valid block. *)
lemma load_by_value_success_valid_block_aux :
  ∀ty,m,b,off,v.
    access_mode ty = By_value (typ_of_type ty) →
    load_value_of_type ty m b off = Some ? v →
    Zltb (block_id b) (nextblock m) = true. (* → valid_block m b *)
#ty #m * #brg #bid #off #v whd in match (valid_block ??);
cases ty
[ 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 ]
whd in match (load_value_of_type ????);
[ 1,7,8: #_ #Habsurd destruct (Habsurd) ]
#Hmode
[ 1,2,3,6: [ 1: elim sz | 2: elim fsz ]
     normalize in match (typesize ?); 
     whd in match (loadn ???);
     whd in match (beloadv ??);
     cases (Zltb bid (nextblock m)) normalize nodelta
     try // #Habsurd destruct (Habsurd)
| *: normalize in Hmode; destruct (Hmode)
] qed.


lemma valid_block_from_bool : ∀b,m. Zltb (block_id b) (nextblock m) = true → valid_block m b.
* #rg #id #m normalize
elim id /2/ qed.

lemma valid_block_to_bool : ∀b,m. valid_block m b → Zltb (block_id b) (nextblock m) = true.
* #rg #id #m normalize
elim id /2/ qed.

lemma load_by_value_success_valid_block :
  ∀ty,m,b,off,v.
    access_mode ty = By_value (typ_of_type ty) → 
    load_value_of_type ty m b off = Some ? v → 
    valid_block m b.
#ty #m #b #off #v #Haccess_mode #Hload
@valid_block_from_bool
@(load_by_value_success_valid_block_aux ty m b off v Haccess_mode Hload)
qed.

(* Making explicit the contents of memory_inj for load_value_of_type *)
lemma load_value_of_type_inj : ∀E,m1,m2,b1,off1,v1,b2,off2,ty.
    memory_inj E m1 m2 →
    value_eq E (Vptr (mk_pointer b1 off1)) (Vptr (mk_pointer b2 off2)) →
    load_value_of_type ty m1 b1 off1 = Some ? v1 →
    ∃v2. load_value_of_type ty m2 b2 off2 = Some ? v2 ∧ value_eq E v1 v2.
#E #m1 #m2 #b1 #off1 #v1 #b2 #off2 #ty #Hinj #Hvalue_eq
lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq #Hembed destruct
     normalize in Hembed;
     lapply (mi_inj … Hinj b1 off1)
     cases (E b1) in Hembed;
     [ 1: normalize #Habsurd destruct (Habsurd)
     | 2: * #b2' #off2' #H normalize in H; destruct (H) #Hyp lapply (Hyp b2 off2' ty v1) -Hyp ]
     lapply (refl ? (access_mode ty))
     cases ty
     [ 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 in ⊢ ((???%) → ?); #Hmode #Hyp
     [ 1,7,8: #Habsurd normalize in Habsurd; destruct (Habsurd)
     | 5,6: #Heq normalize in Heq; destruct (Heq) /4 by ex_intro, conj/ ]
     #Hload_success
     lapply (load_by_value_success_valid_block … Hmode … Hload_success)
     #Hvalid_block @(Hyp Hvalid_block (refl ??) Hload_success)
qed.


(* -------------------------------------- *)
(* Lemmas pertaining to memory allocation *)

(* A valid block stays valid after an alloc. *)
lemma alloc_valid_block_conservation :
  ∀m,m',z1,z2,r,new_block.
  alloc m z1 z2 r = 〈m', new_block〉 →
  ∀b. valid_block m b → valid_block m' b.
#m #m' #z1 #z2 #r * #b' #Hregion_eq
elim m #contents #nextblock #Hcorrect whd in match (alloc ????);
#Halloc destruct (Halloc)
#b whd in match (valid_block ??) in ⊢ (% → %); /2/
qed.

(* Allocating a new zone produces a valid block. *)
lemma alloc_valid_new_block :
  ∀m,m',z1,z2,r,new_block.
  alloc m z1 z2 r = 〈m', new_block〉 →
  valid_block m' new_block.
* #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq
whd in match (alloc ????); whd in match (valid_block ??);
#Halloc destruct (Halloc) /2/
qed.

(* All data in a valid block is unchanged after an alloc. *)
lemma alloc_beloadv_conservation :
  ∀m,m',block,offset,z1,z2,r,new_block.
    valid_block m block →
    alloc m z1 z2 r = 〈m', new_block〉 →
    beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset).
* #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r #new_block #Hvalid #Halloc
whd in Halloc:(??%?); destruct (Halloc)
whd in match (beloadv ??) in ⊢ (??%%);
lapply (valid_block_to_bool … Hvalid) #Hlt
>Hlt >(zlt_succ … Hlt)
normalize nodelta whd in match (update_block ?????); whd in match (eq_block ??);
cut (eqZb (block_id block) next = false)
[ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2/ ] #Hneq
>Hneq cases (eq_region ??) normalize nodelta  @refl
qed.

(* Lift [alloc_beloadv_conservation] to loadn *)
lemma alloc_loadn_conservation :
  ∀m,m',z1,z2,r,new_block.
    alloc m z1 z2 r = 〈m', new_block〉 →
    ∀n. ∀block,offset.
    valid_block m block →
    loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n.
#m #m' #z1 #z2 #r #new_block #Halloc #n
elim n try //
#n' #Hind #block #offset #Hvalid_block
whd in ⊢ (??%%);
>(alloc_beloadv_conservation … Hvalid_block Halloc)
cases (beloadv m' (mk_pointer block offset)) //
#bev normalize nodelta
whd in match (shift_pointer ???); >Hind try //
qed.

(* Memory allocation preserves [memory_inj] *)
lemma alloc_memory_inj :
  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
  alloc m2 z1 z2 r = 〈m2', new_block〉 →
  memory_inj E m1 m2'.
#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion #Hmemory_inj #Halloc
%
[ 1:
  whd
  #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
  elim (mi_inj E m1 m2 Hmemory_inj b1 off1 b2 off2 … ty v1 Hvalid Hembed Hload)
  #v2 * #Hload_eq #Hvalue_eq %{v2} @conj try //
  lapply (refl ? (access_mode ty))
  cases ty in Hload_eq;
  [ 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 ]
  #Hload normalize in ⊢ ((???%) → ?); #Haccess
  [ 1,7,8: normalize in Hload; destruct (Hload)
  | 2,3,4,9: whd in match (load_value_of_type ????);
     whd in match (load_value_of_type ????);
     lapply (load_by_value_success_valid_block … Haccess Hload)
     #Hvalid_block
     whd in match (load_value_of_type ????) in Hload;
     <(alloc_loadn_conservation … Halloc … Hvalid_block) 
     @Hload
  | 5,6: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ]
| 2: @(mi_freeblock … Hmemory_inj)
| 3: #b #b' #o' #HE
     lapply (mi_incl … Hmemory_inj … HE)
     elim m2 in Halloc; #contents #nextblock #Hnextblock
     whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
     whd in match (valid_block ??) in ⊢ (% → %); /2/
| 4: @(mi_region … Hmemory_inj)
| 5: @(mi_disjoint … Hmemory_inj)
] qed.

(* Memory allocation induces a memory extension. *)
lemma alloc_memory_ext :
  ∀E:embedding.∀m1,m2,m2',z1,z2,r,new_block. ∀H:memory_inj E m1 m2.
  alloc m2 z1 z2 r = 〈m2', new_block〉 →
  memory_ext E m1 m2'.
#E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hblock_region_eq #Hmemory_inj #Halloc
lapply (alloc_memory_inj … Hmemory_inj Halloc)
#Hinj' %
[ 1: @Hinj'
| 2: @[new_block]
| 3: #b normalize in ⊢ (%→ ?); * [ 2: #H @(False_ind … H) ]
      #Heq destruct (Heq) whd elim m2 in Halloc;
      #Hcontents #nextblock #Hnextblock
      whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
      /2/
| 4: #b #b' #o' normalize in ⊢ (% → ?); #Hvalid_b #Hload %
     normalize in ⊢ (% → ?); * [ 2: #H @(False_ind … H) ]
     #Heq destruct (Heq) 
     lapply (mi_incl … Hmemory_inj … Hload)
     whd in ⊢ (% → ?); #Habsurd
     (* contradiction car ¬ (valid_block m2 new_block)  *)
     elim m2 in Halloc Habsurd;
     #contents_m2 #nextblock_m2 #Hnextblock_m2
     whd in ⊢ ((??%?) → ?);
     #Heq_alloc destruct (Heq_alloc)
     lapply (irreflexive_Zlt nextblock_m2) * #Hcontr #Habsurd @(Hcontr Habsurd)
] qed.

lemma bestorev_beloadv_conservation :
  ∀mA,mB,wb,wo,v. 
    bestorev mA (mk_pointer wb wo) v = Some ? mB →
    ∀rb,ro. eq_block wb rb = false →
    beloadv mA (mk_pointer rb ro) = beloadv mB (mk_pointer rb ro).
#mA #mB #wb #wo #v #Hstore #rb #ro #Hblock_neq
whd in ⊢ (??%%);
elim mB in Hstore; #contentsB #nextblockB #HnextblockB
normalize in ⊢ (% → ?);
cases (Zltb (block_id wb) (nextblock mA)) normalize nodelta
[ 2: #Habsurd destruct (Habsurd) ]
cases (if Zleb (low (blocks mA wb)) (offv wo) 
       then Zltb (offv wo) (high (blocks mA wb)) 
       else false) normalize nodelta
[ 2: #Habsurd destruct (Habsurd) ]
#Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid
cases rr cases wr normalize try //
@(eqZb_elim … rid wid)
[ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd) ]
try //
qed.

(* lift [bestorev_beloadv_conservation to [loadn] *)
lemma bestorev_loadn_conservation :
  ∀mA,mB,n,wb,wo,v. 
    bestorev mA (mk_pointer wb wo) v = Some ? mB →
    ∀rb,ro. eq_block wb rb = false →
    loadn mA (mk_pointer rb ro) n = loadn mB (mk_pointer rb ro) n.
#mA #mB #n
elim n
[ 1: #wb #wo #v #Hstore #rb #ro #Hblock_neq normalize @refl
| 2: #n' #Hind #wb #wo #v #Hstore #rb #ro #Hneq
     whd in ⊢ (??%%);
     >(bestorev_beloadv_conservation … Hstore … Hneq)
     >(Hind … Hstore … Hneq) @refl
] qed.

(* lift [bestorev_loadn_conservation] to [load_value_of_type] *)
lemma bestorev_load_value_of_type_conservation :
  ∀mA,mB,wb,wo,v. 
    bestorev mA (mk_pointer wb wo) v = Some ? mB →
    ∀rb,ro. eq_block wb rb = false →
    ∀ty.load_value_of_type ty mA rb ro = load_value_of_type ty mB rb ro.
#mA #mB #wb #wo #v #Hstore #rb #ro #Hneq #ty
cases ty
[ 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 ] try //
[ 1: elim sz | 2: elim fsz | 3: | 4: ]
whd in ⊢ (??%%);
>(bestorev_loadn_conservation … Hstore … Hneq) @refl
qed.

(* Writing in the "extended" part of a memory preserves the underlying injection *)
lemma bestorev_memory_ext_to_load_sim :
  ∀E,mA,mB,mC.
  ∀Hext:memory_ext E mA mB.
  ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 
  bestorev mB (mk_pointer wb wo) v = Some ? mC →
  load_sim E mA mC.
#E #mA #mB #mC #Hext #wb #wo #v #Hwb #Hstore whd
#b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hembed #Hload
(* Show that (wb ≠ b2) *)
lapply (me_writeable_ok … Hext … Hvalid Hembed) #Hb2
lapply (mem_not_mem_neq … Hwb Hb2) #Hwb_neq_b2
cut ((eq_block wb b2) = false) [ @neq_block_eq_block_false @Hwb_neq_b2 ] #Heq_block_false
<(bestorev_load_value_of_type_conservation … Hstore … Heq_block_false)
@(mi_inj … (me_inj … Hext) … Hvalid  … Hembed …  Hload)
qed.

(* Writing in the "extended" part of a memory preserves the whole memory injection *)
lemma bestorev_memory_ext_to_memory_inj :
  ∀E,mA,mB,mC.
  ∀Hext:memory_ext E mA mB.
  ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 
  bestorev mB (mk_pointer wb wo) v = Some ? mC →
  memory_inj E mA mC.
#E #mA * #contentsB #nextblockB #HnextblockB #mC
#Hext #wb #wo #v #Hwb #Hstore
%
[ 1: @(bestorev_memory_ext_to_load_sim … Hext … Hwb Hstore) ]
elim Hext in Hwb; * #Hinj #Hvalid #Hcodomain #Hregion #Hdisjoint #writeable #Hwriteable_valid #Hwriteable_ok
#Hmem
[ 1: @Hvalid | 3: @Hregion | 4: @Hdisjoint ] - Hvalid -Hregion -Hdisjoint -Hwriteable_ok -Hinj
whd in Hstore:(??%?); lapply (Hwriteable_valid … Hmem)
normalize in ⊢ (% → ?); #Hlt_wb
>(Zlt_to_Zltb_true … Hlt_wb) in Hstore; normalize nodelta
cases (Zleb (low (contentsB wb)) (offv wo)∧Zltb (offv wo) (high (contentsB wb)))
normalize nodelta
[ 2: #Habsurd destruct (Habsurd) ]
#Heq destruct (Heq)
#b #b' #o' #Hembed @(Hcodomain … Hembed)
qed.

(* It even preserves memory extensions, with the same writeable blocks.  *)
lemma bestorev_memory_ext_to_memory_ext :
  ∀E,mA,mB.
  ∀Hext:memory_ext E mA mB.
  ∀wb,wo,v. meml ? wb (me_writeable … Hext) → 
  ∀mC.bestorev mB (mk_pointer wb wo) v = Some ? mC →
  ΣExt:memory_ext E mA mC.(me_writeable … Hext = me_writeable … Ext).
#E #mA #mB #Hext #wb #wo #v #Hmem #mC #Hstore
%{(mk_memory_ext … 
      (bestorev_memory_ext_to_memory_inj … Hext … Hmem … Hstore)
      (me_writeable … Hext)
      ?
      (me_writeable_ok … Hext)
 )} try @refl
#b #Hmemb
lapply (me_writeable_valid … Hext b Hmemb)
lapply (me_writeable_valid … Hext wb Hmem)
elim mB in Hstore; #contentsB #nextblockB #HnextblockB #Hstore #Hwb_valid #Hb_valid
lapply Hstore normalize in Hwb_valid Hb_valid ⊢ (% → ?);
>(Zlt_to_Zltb_true … Hwb_valid) normalize nodelta
cases (if Zleb (low (contentsB wb)) (offv wo) 
       then Zltb (offv wo) (high (contentsB wb)) 
       else false)
normalize [ 2: #Habsurd destruct (Habsurd) ]
#Heq destruct (Heq) @Hb_valid
qed.

(* Lift [bestorev_memory_ext_to_memory_ext] to storen *)
lemma storen_memory_ext_to_memory_ext :
  ∀E,mA,l,mB,mC.
  ∀Hext:memory_ext E mA mB.
  ∀wb,wo. meml ? wb (me_writeable … Hext) → 
  storen mB (mk_pointer wb wo) l = Some ? mC →
  memory_ext E mA mC.
#E #mA #l elim l
[ 1: #mB #mC #Hext #wb #wo #Hmem normalize in ⊢ (% → ?); #Heq destruct (Heq)
     @Hext 
| 2: #hd #tl #Hind #mB #mC #Hext #wb #wo #Hmem
     whd in ⊢ ((??%?) → ?);
     lapply (bestorev_memory_ext_to_memory_ext … Hext … wb wo hd Hmem)
     cases (bestorev mB (mk_pointer wb wo) hd)
     normalize nodelta
     [ 1: #H #Habsurd destruct (Habsurd) ]
     #mD #H lapply (H mD (refl ??)) * #HextD #Heq #Hstore
     @(Hind … HextD … Hstore)
     <Heq @Hmem
] qed.     

(* Lift [storen_memory_ext_to_memory_ext] to store_value_of_type *)
lemma store_value_of_type_memory_ext_to_memory_ext :
  ∀E,mA,mB,mC.
  ∀Hext:memory_ext E mA mB.
  ∀wb,wo. meml ? wb (me_writeable … Hext) → 
  ∀ty,v.store_value_of_type ty mB wb wo v = Some ? mC →
  memory_ext E mA mC.
#E #mA #mB #mC #Hext #wb #wo #Hmem #ty #v
cases ty
[ 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 ]
whd in ⊢ ((??%?) → ?);
[ 1,5,6,7,8: #Habsurd destruct (Habsurd) ]
#Hstore
@(storen_memory_ext_to_memory_ext … Hext … Hmem … Hstore)
qed.

(* End of the memory injection-related stuff. *)
(* ------------------------------------------ *)

(* 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  
  ]
].

(* [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)). λ(E:embedding). λ(Hext: memory_ext E 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 ⇒
         match lookup ?? e1 id with
         [ None ⇒ lookup ?? e2 id = None ?
         | Some b1 ⇒
           match lookup ?? e2 id with
           [ None ⇒ False
           | Some b2 ⇒
             valid_block m1 b1 ∧
             value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset))
           ]
         ]
       ].

(* 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]).
  λ(eq : A → A → Prop).
  λ(r1, r2 : res A).
  ∀a1. r1 = OK ? a1 → ∃a2. r2 = OK ? a2 ∧ eq a1 a2.

(* Specialisation of [res_sim] to match [exec_expr] *)
definition exec_expr_sim ≝ λE.
  res_sim (val × trace) (λr1,r2. value_eq E (\fst r1) (\fst r2) ∧ (\snd r1 = \snd r2)).

(* Specialisation of [res_sim] to match [exec_lvalue] *)
definition exec_lvalue_sim ≝ λE.
  res_sim (block × offset × trace)
    (λr1,r2.
      let 〈b1,o1,tr1〉 ≝ r1 in
      let 〈b2,o2,tr2〉 ≝ r2 in
      value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) ∧ tr1 = tr2).

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.

(*
lemma switch_removal_alloc_extension : ∀f, f', vars, env, env', m, m'.
   env = \fst (exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f))) →
   〈f',vars〉 = function_switch_removal f →
   env' = \fst (exec_alloc_variables empty_env m' ((fn_params f) @ vars @ (fn_vars f))) →
   environment_extension env env' vars. 

#f #f'
cut (∀l:list (ident × type). [ ] @ l = l) [ // ] #nil_append
cases (fn_params f) cases (fn_vars f)
[ 1: #vars >append_nil >append_nil >nil_append elim vars   
   [ 1: #env #env' #m #m' normalize in ⊢ (% → ? → % → ?); #Henv1 #_ #Henv2 destruct //
   | 2: #hd #tl #Hind #env #env' #m #m' #Henv1 #Heq
        whd in ⊢ ((???(???%)) → ?);
 #Henv #Hswrem #Henv'
#id   
*)

(*
lemma substatement_fresh : ∀s,u. 
    fresh_for_statement s u →
    substatement_P s (λs'. fresh_for_statement s' u) (λe. fresh_for_expression e u).
#s #u @(statement_ind2 ? (λls.fresh_for_labeled_statements ls u → substatement_ls ls (λs':statement.fresh_for_statement s' u)) … s)
try /by I/
[ 1: #e1 #e2 #H lapply (fresh_max_split … H) * #H1 #H2 whd @conj assumption
| 2: *
    [ 1: #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *
         #Hfresh_e #Hfresh_args @conj try assumption
         normalize nodelta in Hfresh_args;
         >max_id_commutative in Hfresh_args; >max_id_one_neutral
         #Hfresh_args         
    | 2: #ret #e #args whd in ⊢ (% → %); #H lapply (fresh_max_split ??? H) *
         #Hfresh_e #H lapply (fresh_max_split ??? H) *
         #Hfresh_ret #Hfresh_args @conj try @conj try assumption ]
    elim args in Hfresh_args;
    [ 1,3: //
    | 2,4: #hd #tl #Hind whd in match (foldl ?????); whd in match (All ???);
            >foldl_max #H elim (fresh_max_split ??? H) #Hu #HAll @conj
            [ 1,3: @Hu 
            | 2,4: @Hind assumption ] ] 
| 3: #s1 #s2 #_ #_
     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) * 
     whd in match (substatement_P ??); /2/
| 4: #e #cond #iftrue #iffalse #_
     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) *
     #Hexpr #H2 lapply (fresh_max_split … H2) * /2/
| 5,6: #e #stm #_
     whd in ⊢ (% → ?); #H lapply (fresh_max_split … H) * /2/
| 7: #init #cond #step #body #_ #_ #_ #H lapply (fresh_max_split … H) *
      #H1 #H2 elim (fresh_max_split … H1) #Hinit #Hcond
      elim (fresh_max_split … H2) #Hstep #Hbody whd @conj try @conj try @conj /3/
| 8: #ret #H whd elim ret in H; try //      
| 9: #expr #ls #Hind #H whd @conj
     [ 1: elim (fresh_max_split … H) //
     | 2: @Hind elim (fresh_max_split … H) // ]
| 10: #l #body #Hind #H whd elim (fresh_max_split … H) //
| 11: #sz #i #hd #tl #Hhd #Htl #H whd
     elim (fresh_max_split … H) #Htl_fresh #Hhd_fresh @conj //
     @Htl //
] qed.
*)

(* Eliminating switches introduces fresh variables. [environment_extension] characterizes
 * a local environment extended by some local variables. *)
 

(* lookup on environment extension *)
(*
lemma extension_lookup :
  ∀map, map', ext, id, result.
  environment_extension map map' ext →
  lookup ?? map id = Some ? result →
  lookup ?? map' id = Some ? result.
#map #map' #ext #id #result #Hext lapply (Hext id)
cases (mem_assoc_env ??) normalize nodelta
[ 1: * * #ext_result #H1 >H1 #Habsurd destruct (Habsurd)
| 2: #H >H // ] qed.

*)

(* Extending a map by an empty list of variables yields an observationally equivalent
 * environment. *)
(* 
lemma environment_extension_nil : ∀en,en':env. (environment_extension en en' [ ]) → imap_eq ?? en en'.
* #map1 * #map2 whd in ⊢ (% → ?); #Hext whd % #id #v #H
[ 1: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta
     cases (lookup_opt block id map2) normalize
     [ 1: >H #H2 >H2 @refl
     | 2: #b >H cases v
          [ 1: normalize * #H @(False_ind … H)
          | 2: #block normalize // ] ]
| 2: lapply (Hext (an_identifier ? id)) whd in match (lookup ????); normalize nodelta
     >H cases v normalize try //
     #block cases (lookup_opt ? id map1) normalize try //
     * #H @(False_ind … H)
] qed. *)

(* If two identifier maps are observationally equal, then they contain the same bocks.
 * see maps_obsequiv.ma for the details of the proof. *)
(* 
lemma blocks_of_env_eq : ∀e,e'. imap_eq ?? e e' → blocks_of_env e = blocks_of_env e'.
* #map1 * #map2 normalize #Hpmap_eq lapply (pmap_eq_fold … Hpmap_eq) #Hfold
>Hfold @refl
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,k,k',u,result.
    fresh_for_statement (Swhile e s) u →
    switch_cont_sim fvs k k' →
    switch_removal s fvs u = Some ? result →
    switch_cont_sim fvs (Kwhile e s k) (Kwhile e (ret_st ? result) 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.
*)

inductive switch_state_sim : state → state → Prop ≝
| sws_state : ∀u,f,s,k,k',m,m',result.
    ∀env, env', f', vars.
    ∀E:embedding.    
    ∀Hext:memory_ext E m m'.
    fresh_for_statement s u →
    (*
    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))) →
    *)
    〈f',vars〉 = function_switch_removal f →
    disjoint_extension env m env' m' vars E Hext →
    switch_removal s (map ?? (fst ??) vars) u = Some ? result → 
    switch_cont_sim (map ?? (fst ??) vars) k k' →
    switch_state_sim
      (State f s k env m)
      (State f' (ret_st ? result) k' env' m')
| sws_callstate : ∀vars, fd,args,k,k',m.
    switch_cont_sim vars k k' →
    switch_state_sim (Callstate fd args k m) (Callstate (fundef_switch_removal fd) args k' m) 
| sws_returnstate : ∀vars,res,k,k',m.
    switch_cont_sim vars k k' →
    switch_state_sim (Returnstate res k m) (Returnstate res k' m)
| sws_finalstate : ∀r.
    switch_state_sim (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_now : ∀ge,P,s,t. (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → 
                                      ∃t'.eventually ge P s (t ⧺ t').
#ge #P #s #t * #s' * #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.

(* lift value_eq to option block *)
definition option_block_eq ≝ λE,ob1,ob2.
match ob1 with
[ None ⇒
  match ob2 with
  [ None ⇒ True
  | Some _ ⇒ False ]
| Some b1 ⇒
  match ob2 with
  [ None ⇒ False
  | Some b2 ⇒ value_eq E (Vptr (mk_pointer b1 zero_offset)) (Vptr (mk_pointer b2 zero_offset))  ]
].

definition value_eq_opt ≝ λE,ov1,ov2.
match ov1 with
[ None ⇒
  match ov2 with
  [ None ⇒ True
  | Some _ ⇒ False ]
| Some v1 ⇒
  match ov2 with
  [ None ⇒ False
  | Some v2 ⇒ 
    value_eq E v1 v2 ]
].

record switch_removal_globals (E : embedding) (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
  rg_find_symbol: ∀s.
    option_block_eq E (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)
}.

lemma exec_lvalue_expr_elim :
  ∀E,r1,r2,Pok,Qok.
  ∀H:exec_lvalue_sim E r1 r2.
  (∀bo1,bo2,tr.
    let 〈b1,o1〉 ≝ bo1 in
    let 〈b2,o2〉 ≝ bo2 in
    value_eq E (Vptr (mk_pointer b1 o1)) (Vptr (mk_pointer b2 o2)) →
    match Pok 〈bo1,tr〉 with
    [ Error err ⇒ True
    | OK vt1 ⇒
      let 〈val1,trace1〉 ≝ vt1 in
      match Qok 〈bo2,tr〉 with
      [ Error err ⇒ False
      | OK vt2 ⇒
        let 〈val2,trace2〉 ≝ vt2 in
        trace1 = trace2 ∧ value_eq E val1 val2      
      ]
    ]) →
  exec_expr_sim E
    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
#E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
elim r1
[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
| 1: normalize nodelta #a1 #H lapply (H a1 (refl ??))
     * #a2 * #Hr2 >Hr2 normalize nodelta
     elim a1 * #b1 #o1 #tr1
     elim a2 * #b2 #o2 #tr2 normalize nodelta
     * #Hvalue_eq #Htrace_eq #H2
     destruct (Htrace_eq)
     lapply (H2 〈b1, o1〉 〈b2, o2〉 tr2 Hvalue_eq)
     cases (Pok 〈b1, o1, tr2〉)
     [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd)
     | 1: * #v1 #tr1' normalize nodelta #H3 whd
          * #v1' #tr1'' #Heq destruct (Heq)
          cases (Qok 〈b2,o2,tr2〉) in H3;
          [ 2: #error #Hfalse @(False_ind … Hfalse)
          | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq)
               #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj //
] ] ] qed.

lemma exec_expr_expr_elim :
  ∀E,r1,r2,Pok,Qok.
  ∀H:exec_expr_sim E r1 r2.
  (∀v1,v2,trace.
    value_eq E v1 v2 →
    match Pok 〈v1,trace〉 with
    [ Error err ⇒ True
    | OK vt1 ⇒
      let 〈val1,trace1〉 ≝ vt1 in
      match Qok 〈v2,trace〉 with
      [ Error err ⇒ False
      | OK vt2 ⇒
        let 〈val2,trace2〉 ≝ vt2 in
        trace1 = trace2 ∧ value_eq E val1 val2      
      ]
    ]) →
  exec_expr_sim E
    (match r1 with [ OK x ⇒ Pok x | Error err ⇒ Error ? err ])
    (match r2 with [ OK x ⇒ Qok x | Error err ⇒ Error ? err ]).
#E #r1 #r2 #Pok #Qok whd in ⊢ (% → ?);
elim r1
[ 2: #error #_ #_ normalize #a1 #Habsurd destruct (Habsurd)
| 1: normalize nodelta #a1 #H lapply (H a1 (refl ??))
     * #a2 * #Hr2 >Hr2 normalize nodelta
     elim a1 #v1 #tr1
     elim a2 #v2 #tr2 normalize nodelta
     * #Hvalue_eq #Htrace_eq #H2
     destruct (Htrace_eq)
     lapply (H2 v1 v2 tr2 Hvalue_eq)
     cases (Pok 〈v1, tr2〉)
     [ 2: #error #_ normalize #a1' #Habsurd destruct (Habsurd)
     | 1: * #v1 #tr1' normalize nodelta #H3 whd
          * #v1' #tr1'' #Heq destruct (Heq)
          cases (Qok 〈v2,tr2〉) in H3;
          [ 2: #error #Hfalse @(False_ind … Hfalse)
          | 1: * #v2 #tr2 normalize nodelta * #Htrace_eq destruct (Htrace_eq)
               #Hvalue_eq' %{〈v2,tr2〉} @conj try @conj //
] ] ] qed.

(* Commutation results of standard binary operations with value_eq. *)
lemma unary_operation_value_eq :
  ∀E,op,v1,v2,ty.
   value_eq E v1 v2 →
   ∀r1.
   sem_unary_operation op v1 ty = Some ? r1 →
    ∃r2.sem_unary_operation op v2 ty = Some ? r2 ∧ value_eq E r1 r2.
#E #op #v1 #v2 #ty #Hvalue_eq #r1
inversion Hvalue_eq
[ 1: #v #Hv1 #Hv2 #_ destruct
     cases op normalize
     [ 1: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
          normalize #Habsurd destruct (Habsurd)
     | 3: cases ty [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
          normalize #Habsurd destruct (Habsurd)
     | 2: #Habsurd destruct (Habsurd) ]
| 2: #vsz #i #Hv1 #Hv2 #_
     cases op
     [ 1: 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 ⊢ ((??%?) → ?); whd in match (sem_unary_operation ???);
          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
               %{(of_bool (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))))}
               cases (eq_bv (bitsize_of_intsize vsz) i (zero (bitsize_of_intsize vsz))) @conj
               //
          | *: #Habsurd destruct (Habsurd) ]
     | 2: whd in match (sem_unary_operation ???);      
          #Heq1 destruct %{(Vint vsz (exclusive_disjunction_bv (bitsize_of_intsize vsz) i (mone vsz)))} @conj //
     | 3: whd in match (sem_unary_operation ???);
          cases ty
          [ 1: | 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
          normalize nodelta
          whd in ⊢ ((??%?) → ?);
          [ 2: cases (eq_intsize sz vsz) normalize nodelta #Heq1 destruct
               %{(Vint vsz (two_complement_negation (bitsize_of_intsize vsz) i))} @conj //
          | *: #Habsurd destruct (Habsurd) ] ]
| 3: #f #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
     cases op normalize nodelta
     [ 1: 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 (sem_notbool ??);
          #Heq1 destruct
          cases (Fcmp Ceq f Fzero) /3 by ex_intro, vint_eq, conj/
     | 2: normalize #Habsurd destruct (Habsurd)
     | 3: 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 (sem_neg ??);
          #Heq1 destruct /3 by ex_intro, vfloat_eq, conj/ ]
| 4: #Hv1 #Hv2 #_ destruct  whd in match (sem_unary_operation ???);
     cases op normalize nodelta
     [ 1: 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 (sem_notbool ??);
          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
     | 2: normalize #Habsurd destruct (Habsurd)
     | 3: 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 (sem_neg ??);
          #Heq1 destruct ]
| 5: #p1 #p2 #Hptr_translation #Hv1 #Hv2 #_  whd in match (sem_unary_operation ???);
     cases op normalize nodelta
     [ 1: 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 (sem_notbool ??);          
          #Heq1 destruct /3 by ex_intro, vint_eq, conj/
     | 2: normalize #Habsurd destruct (Habsurd)
     | 3: 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 (sem_neg ??);          
          #Heq1 destruct ]
]
qed.

(* A cleaner version of inversion for [value_eq] *)
lemma value_eq_inversion :
  ∀E,v1,v2. ∀P : val → val → Prop. value_eq E v1 v2 → 
  (∀v. P Vundef v) →
  (∀sz,i. P (Vint sz i) (Vint sz i)) →
  (∀f. P (Vfloat f) (Vfloat f)) →
  (P Vnull Vnull) →
  (∀p1,p2. pointer_translation p1 E = Some ? p2 → P (Vptr p1) (Vptr p2)) →
  P v1 v2.
#E #v1 #v2 #P #Heq #H1 #H2 #H3 #H4 #H5
inversion Heq
[ 1: #v #Hv1 #Hv2 #_ destruct @H1
| 2: #sz #i #Hv1 #Hv2 #_ destruct @H2
| 3: #f #Hv1 #Hv2 #_ destruct @H3
| 4: #Hv1 #Hv2 #_ destruct @H4
| 5: #p1 #p2 #Hembed #Hv1 #Hv2 #_ destruct @H5 // ] qed.

(* value_eq lifts to addition *)
lemma add_value_eq :
  ∀E,v1,v2,v1',v2',ty1,ty2,m1,m2.
   value_eq E v1 v2 →
   value_eq E v1' v2' →
   memory_inj E m1 m2 → (* This injection seems useless TODO *)
   ∀r1. (sem_add v1 ty1 v1' ty2=Some val r1→
           ∃r2:val.sem_add v2 ty1 v2' ty2=Some val r2∧value_eq E r1 r2).
#E #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
@(value_eq_inversion E … Hvalue_eq1)
[ 1: #v | 2: #sz #i | 3: #f | 4: | 5: #p1 #p2 #Hembed ]
[ 1: whd in match (sem_add ????); normalize nodelta
     cases (classify_add ty1 ty2) normalize nodelta
     [ 1: #sz #sg | 2: #fsz | 3: #n #ty #sz #sg | 4: #n #sz #sg #ty | 5: #ty1' #ty2' ]
     #Habsurd destruct (Habsurd)
| 2: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
     cases (classify_add ty1 ty2) normalize nodelta     
     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     [ 2,3,5: #Habsurd destruct (Habsurd) ]
     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     [ 1,6: #v' | 2,7: #sz' #i' | 3,8: #f' | 4,9: | 5,10: #p1' #p2' #Hembed' ]
     [ 1,2,4,5,6,7,9: #Habsurd destruct (Habsurd) ]
     [ 1: @intsize_eq_elim_elim
          [ 1: #_ #Habsurd destruct (Habsurd)
          | 2: #Heq destruct (Heq) normalize nodelta
               #Heq destruct (Heq)
               /3 by ex_intro, conj, vint_eq/ ]
     | 2: @eq_bv_elim normalize nodelta #Heq1 #Heq2 destruct
          /3 by ex_intro, conj, vint_eq/
     | 3: #Heq destruct (Heq)
          normalize in Hembed'; elim p1' in Hembed'; #b1' #o1' normalize nodelta #Hembed
          %{(Vptr (shift_pointer_n (bitsize_of_intsize sz) p2' (sizeof ty) i))} @conj try @refl
          @vptr_eq whd in match (pointer_translation ??);
          cases (E b1') in Hembed;
          [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
          | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
               whd in match (shift_pointer_n ????);
               cut (offset_plus (shift_offset_n (bitsize_of_intsize sz) o1' (sizeof ty) i) offset =
                    (shift_offset_n (bitsize_of_intsize sz) (mk_offset (offv o1'+offv offset)) (sizeof ty) i))
               [ 1: normalize >sym_Zplus <associative_Zplus >(sym_Zplus (offv offset) (offv o1')) @refl ]
               #Heq >Heq @refl ]
     ]
| 3: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
     cases (classify_add ty1 ty2) normalize nodelta     
     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
     #Heq destruct (Heq)
     /3 by ex_intro, conj, vfloat_eq/
| 4: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
     cases (classify_add ty1 ty2) normalize nodelta     
     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     @eq_bv_elim 
     [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/
     | 2: #_ normalize nodelta #Habsurd destruct (Habsurd) ]
| 5: whd in match (sem_add ????); whd in match (sem_add ????); normalize nodelta
     cases (classify_add ty1 ty2) normalize nodelta
     [ 1: #tsz #tsg | 2: #tfsz | 3: #tn #ty #tsz #tsg | 4: #tn #tsz #tsg #ty | 5: #ty1' #ty2' ]
     [ 1,2,4,5: #Habsurd destruct (Habsurd) ]
     @(value_eq_inversion E … Hvalue_eq2) normalize nodelta
     [ 1: #v' | 2: #sz' #i' | 3: #f' | 4: | 5: #p1' #p2' #Hembed' ]
     [ 1,3,4,5: #Habsurd destruct (Habsurd) ]
     #Heq destruct (Heq)
     %{(Vptr (shift_pointer_n (bitsize_of_intsize sz') p2 (sizeof ty) i'))} @conj try @refl
     @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %;
     elim p1 in Hembed; #b1 #o1 normalize nodelta
     cases (E b1)
     [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
     | 2: * #block #offset normalize nodelta #Heq destruct (Heq)
          normalize >(sym_Zplus ? (offv offset)) <associative_Zplus >(sym_Zplus ? (offv offset))
          @refl
     ]
] qed.
          
(* TODO all other 10 binary operations. Then wrap this in [binary_operation_value_eq] *)


(* Commutation result for binary operators. *)
lemma binary_operation_value_eq :
  ∀E,op,v1,v2,v1',v2',ty1,ty2,m1,m2.
   value_eq E v1 v2 →
   value_eq E v1' v2' →
   memory_inj E m1 m2 →
   ∀r1.
   sem_binary_operation op v1 ty1 v1' ty2 m1 = Some ? r1 →
   ∃r2.sem_binary_operation op v2 ty1 v2' ty2 m2 = Some ? r2 ∧ value_eq E r1 r2.
#E #op #v1 #v2 #v1' #v2' #ty1 #ty2 #m1 #m2 #Hvalue_eq1 #Hvalue_eq2 #Hinj #r1
cases op
whd in match (sem_binary_operation ??????);
whd in match (sem_binary_operation ??????);
@cthulhu
qed.

 
(* Simulation relation on expressions *)
lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,ext.
  ∀E:embedding.
  ∀Hext:memory_ext E m1 m2.
  switch_removal_globals E ? fundef_switch_removal ge ge' →
  disjoint_extension en1 m1 en2 m2 ext E Hext →
  ext_fresh_for_genv ext ge →
  (∀e. exec_expr_sim E (exec_expr ge en1 m1 e) (exec_expr ge' en2 m2 e)) ∧
  (∀ed, ty. exec_lvalue_sim E (exec_lvalue' ge en1 m1 ed ty) (exec_lvalue' ge' en2 m2 ed ty)).
#ge #ge' #en1 #m1 #en2 #m2 #ext #E #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: #b1 #H elim (H b1 (refl ??)) #b2 *
           elim b1 * #bl1 #o1 #tr1 elim b2 * #bl2 #o2 #tr2
           #Heq >Heq normalize nodelta * #Hvalue_eq #Htrace_eq
           whd in match (load_value_of_type' ???); 
           whd in match (load_value_of_type' ???);
           lapply (load_value_of_type_inj E … (\fst a1) … ty (me_inj … Hext) Hvalue_eq)
           cases (load_value_of_type ty m1 bl1 o1)
           [ 1,3,5: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
           | 2,4,6: #v #Hyp normalize in ⊢ (% → ?); #Heq destruct (Heq)
                    elim (Hyp (refl ??)) #v2 * #Hload #Hvalue_eq >Hload
                    normalize /4 by ex_intro, conj/
  ] ] ]
| 4: #v #ty whd * * #b1 #o1 #tr1
     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)
               cases (find_symbol ???) normalize
               [ 1: #_ #Habsurd destruct (Habsurd)
               | 2: #block cases (lookup ?? (symbols clight_fundef ge') v)
                    [ 1: normalize nodelta #Hfalse @(False_ind … Hfalse)
                    | 2: #block' normalize #Hvalue_eq #Heq destruct (Heq)
                         %{〈block',mk_offset OZ,[]〉} @conj try @refl
                         normalize /2/
                ] ]
         | 2: #block
              cases (lookup ?? en2 v) normalize nodelta
              [ 1: #Hfalse @(False_ind … Hfalse)
              | 2: #b * #Hvalid_block #Hvalue_eq #Heq destruct (Heq)
                   %{〈b, zero_offset, E0〉} @conj try @refl
                   normalize /2/
    ] ] ]
| 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' * #Heq >Heq normalize nodelta
          * elim v1 normalize nodelta
          [ 1: #_ #_ #a1 #Habsurd destruct (Habsurd)
          | 2: #sz #i #_ #_ #a1  #Habsurd destruct (Habsurd)
          | 3: #fl #_ #_ #a1 #Habsurd destruct (Habsurd)
          | 4: #_ #_ #a1 #Habsurd destruct (Habsurd)
          | 5: #ptr #Hvalue_eq lapply (value_eq_ptr_inversion … Hvalue_eq) * #p2 * #Hp2_eq
               >Hp2_eq in Hvalue_eq; elim ptr #b1 #o1 elim p2 #b2 #o2
               #Hvalue_eq normalize
               cases (E b1) [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) ]
               * #b2' #o2' normalize #Heq destruct (Heq) #Htrace destruct (Htrace)
               * * #b1' #o1' #tr1'' #Heq2 destruct (Heq2) normalize
               %{〈b2,mk_offset (offv o1'+offv o2'),tr1''〉} @conj try @refl
               normalize @conj // ]
     | 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 ]
     * #b1 #o1 * #b2 #o2 normalize nodelta try /2 by I/
     #tr #H @conj try @refl try assumption
| 7: #ty #op #e
     #Hsim @(exec_expr_expr_elim … Hsim) #v1 #v2 #trace #Hvalue_eq
     lapply (unary_operation_value_eq E op v1 v2 (typeof e) Hvalue_eq)
     cases (sem_unary_operation op v1 (typeof e)) normalize nodelta
     [ 1: #_ @I
     | 2: #r1 #H elim (H r1 (refl ??)) #r1' * #Heq >Heq
           normalize /2/ ]
| *: @cthulhu ] qed.

(* TODO: Old cases, to be ported to memory injection.
| 8: #ty #op #e1 #e2 #Hind1 #Hind2
     whd in match (exec_expr ge ???);    
     whd in match (exec_expr ge' ???);
     @(exec_expr_expr_elim … Hind1)
     cases (exec_expr ge en1 m1 e2) in Hind2;
     [ 2: #error normalize //
     | 1: * #v1 #tr1 normalize in ⊢ (% → ?); #Hind2 elim (Hind2 〈v1,tr1〉 (refl ??)) * #v2 #tr2 *
          #Hexec_eq * #Hvalue_eq #Htrace_eq #v1' #v2' #trace #Hvalue_eq'
          >Hexec_eq whd in match (m_bind ?????); whd in match (m_bind ?????);


| 9: #ty #castty #e #Hind
     whd in match (exec_expr ge ???);    
     whd in match (exec_expr ge' ???);
     cases Hind
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk // 
          ] 
     ]
| 10: #ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3
     whd in match (exec_expr ge ???);    
     whd in match (exec_expr ge' ???);
     cases Hind1
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e1)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
               normalize nodelta
               cases (exec_bool_of_val ??)
               [ 2: #error @SimFail /2 by ex_intro/
               | 1: * whd in match (m_bind ?????); normalize nodelta
                    [ 1: cases Hind2
                         [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
                         | 1: cases (exec_expr ge en m e2)
                              [ 2: #error #_  @SimFail /2 by ex_intro/
                              | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))                                   
                                   @SimOk normalize nodelta #a2
                                   whd in match (m_bind ?????); // ]
                         ]
                    | 2: cases Hind3
                         [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
                         | 1: cases (exec_expr ge en m e3)
                              [ 2: #error #_  @SimFail /2 by ex_intro/
                              | 1: #a3 #Hind3 >(Hind3 a3 (refl ? (OK ? a3)))
                                   @SimOk normalize nodelta #a3
                                   whd in match (m_bind ?????); // ]
                         ]
     ] ] ] ]                      
| 11: #ty #e1 #e2 #Hind1 #Hind2
     whd in match (exec_expr ge ???);    
     whd in match (exec_expr ge' ???);
     cases Hind1
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e1)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
               normalize nodelta
               cases (exec_bool_of_val ??)
               [ 2: #error @SimFail /2 by ex_intro/
               | 1: * whd in match (m_bind ?????);
                    [ 2: @SimOk // ]
                    cases Hind2
                    [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
                    | 1: cases (exec_expr ge en m e2)
                         [ 2: #error #_  @SimFail /2 by ex_intro/
                         | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
                              @SimOk #a2
                              whd in match (m_bind ?????); //
     ] ] ] ] ]
| 12: #ty #e1 #e2 #Hind1 #Hind2
     whd in match (exec_expr ge ???);    
     whd in match (exec_expr ge' ???);
     cases Hind1
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e1)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a1 #Hind1 >(Hind1 a1 (refl ? (OK ? a1)))
               normalize nodelta
               cases (exec_bool_of_val ??)
               [ 2: #error @SimFail /2 by ex_intro/
               | 1: * whd in match (m_bind ?????);
                    [ 1: @SimOk // ]
                    cases Hind2
                    [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
                    | 1: cases (exec_expr ge en m e2)
                         [ 2: #error #_  @SimFail /2 by ex_intro/
                         | 1: #a2 #Hind2 >(Hind2 a2 (refl ? (OK ? a2)))
                              @SimOk #a2
                              whd in match (m_bind ?????); //
     ] ] ] ] ]
| 13: #ty #sizeof_ty
     whd in match (exec_expr ge ???);    
     whd in match (exec_expr ge' ???);
     @SimOk //
| 14: #ty #e #ty' #fld #Hind
     whd in match (exec_lvalue' ge ????);
     whd in match (exec_lvalue' ge' ????);
     whd in match (typeof ?);
     cases ty' in Hind;
     [ 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 #Hind
     try (@SimFail /2 by ex_intro/)
     whd in match (exec_lvalue ????);
     whd in match (exec_lvalue ????);     
     cases Hind
     [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1,3: cases (exec_lvalue' ge en m e ?)
         [ 2,4: #error #_ @SimFail /2 by ex_intro/
         | 1,3: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
     ] ]
| 15: #ty #l #e #Hind
     whd in match (exec_expr ge ???);
     whd in match (exec_expr ge' ???);
     cases Hind
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e)
        [ 2: #error #_ @SimFail /2 by ex_intro/
        | 1: #a #Hind >(Hind a (refl ? (OK ? a))) @SimOk //
     ] ]
| 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 ⊢ (% → ?);
  [ 1,2: #_ @SimOk #a normalize //
  | 3,4,13: #H @(False_ind … H)
  | *: #_ @SimFail /2 by ex_intro/
  ]
] 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,u.
   fresh_for_expression e u → fresh_for_statement s u → fresh_for_statement (Swhile e s) u.
#e #s * #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 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. *)



(* Main theorem. To be ported and completed to memory injections. TODO *)
(*
theorem switch_removal_correction : ∀ge, ge'.
  related_globals ? fundef_switch_removal ge ge' →
  ∀s1, s1', tr, s2.
  switch_state_sim s1 s1' →
  exec_step ge s1 = Value … 〈tr,s2〉 →
  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
inversion Hsim_state
[ 1: (* regular state *)
  #u #f #s #k #k' #m #m' #result #en #en' #f' #vars
  #Hu_fresh #Hen_eq #Hf_eq #Hen_eq' #Hswitch_removal #Hsim_cont #Hs1_eq #Hs1_eq' #_

  lapply (sim_related_globals ge ge' e m Hrelated) *
  #Hexpr_related #Hlvalue_related
  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
  cases s in Hu_fresh Heq_env;
  

theorem switch_removal_correction : ∀ge, ge'.
  related_globals ? fundef_switch_removal ge ge' →
  ∀s1, s1', tr, s2.
  switch_state_sim s1 s1' →
  exec_step ge s1 = Value … 〈tr,s2〉 →
  eventually ge' (λs2'. switch_state_sim s2 s2') s1' tr.
#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hsim_state #Hexec_step
inversion Hsim_state
[ 1: (* regular state *)
  #u #f #s #k #k' #e #e' #m #m' #Hu_fresh #Heq_env #Hsim_cont #Hs1_eq #Hs1_eq' #_
  lapply (sim_related_globals ge ge' e m Hrelated) *
  #Hexpr_related #Hlvalue_related
  >Hs1_eq in Hexec_step; whd in ⊢ ((??%?) → ?);
  cases s in Hu_fresh Heq_env;
  (* 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 ]
  #Hu_fresh #Heq_env
  [ 1: (* Skip *)
    whd in match (sw_rem ??);
    inversion Hsim_cont normalize nodelta
    [ 1: #Hk #Hk' #_ #Hexec_step
         @(eventually_now ????) whd in match (exec_step ??); >fn_return_simplify
         cases (fn_return f) in Hexec_step;
         [ 1,10: | 2,11: #sz #sg | 3,12: #fsz | 4,13: #rg #ptr_ty | 5,14: #rg #array_ty #array_sz | 6,15: #domain #codomain
         | 7,16: #structname #fieldspec | 8,17: #unionname #fieldspec | 9,18: #rg #id ]
         normalize nodelta
         [ 1,2: #H whd in match (ret ??) in H ⊢ %; destruct (H)
                %{(Returnstate Vundef Kstop (free_list m' (blocks_of_env e')))} @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))
          
  *)