source: src/Clight/switchRemoval.ma @ 2408

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


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

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

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

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

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

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


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

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

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

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

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

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

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

(*  (def_case : ident × sf_statement) *)

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

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

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

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

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

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

notation > "vbox('ret' 〈e1, e2, e3, e4〉)" with precedence 49
for @{ Some ? (mk_swret ? ${e1} ${e2} ${e3} ${e4})  }.
      
(* Recursively convert a statement into a switch-free one. We /provide/ directly to the function a list
   of identifiers (supposedly fresh). The actual task of producing this identifier is decoupled in another
   'twin' function. It is then proved that feeding [switch_removal] with the correct amount of free variables
   allows it to proceed without failing. This is all in order to ease the proof of simulation. *)
let rec switch_removal
  (st : statement)           (* the statement in which we will remove switches *)
  (fvs : list ident)         (* a finite list of names usable to create variables. *)
  (u : universe SymbolTag)   (* a fresh /label/ generator *)
  : option (swret statement) ≝
match st with
[ Sskip       ⇒ ret 〈st, [ ], fvs, u〉
| Sassign _ _ ⇒ ret 〈st, [ ], fvs, u〉
| Scall _ _ _ ⇒ ret 〈st, [ ], fvs, u〉
| Ssequence s1 s2 ⇒
  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
  ret 〈Ssequence s1' s2', acc1 @ acc2, fvs'', u''〉
| Sifthenelse e s1 s2 ⇒
  do 〈s1', acc1, fvs', u'〉 ← switch_removal s1 fvs u;
  do 〈s2', acc2, fvs'', u''〉 ← switch_removal s2 fvs' u';
  ret 〈Sifthenelse e s1' s2', acc1 @ acc2, fvs'', u''〉
| Swhile e body ⇒
  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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(* --------------------------------------------------------------------------- *)
(* "Observational" memory equivalence. Memories use closures to represent contents,
   so we have to use that short of asserting functional extensionality to reason
   on reordering of operations on memories, among others. For our
   limited purposes, we do not need (at this time of writing, i.e. 22 sept. 2012)
   to push the observation in the content_map. *)
(* --------------------------------------------------------------------------- *)  
definition memory_eq ≝ λm1,m2.
  nextblock m1 = nextblock m2 ∧
  ∀b. blocks m1 b = blocks m2 b.
  
(* memory_eq is an equivalence relation. *)
lemma reflexive_memory_eq : reflexive ? memory_eq.
whd * #contents #nextblock #Hpos normalize @conj try //
qed.

lemma symmetric_memory_eq : symmetric ? memory_eq.
whd * #contents #nextblock #Hpos * #contents' #nextblock' #Hpos'
normalize * #H1 #H2 @conj >H1 try //
qed.

lemma transitive_memory_eq : transitive ? memory_eq.
whd 
* #contents #nextblock #Hpos 
* #contents1 #nextblock1 #Hpos1
* #contents2 #nextblock2 #Hpos2
normalize * #H1 #H2 * #H3 #H4 @conj //
qed.

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

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

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

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

(* A writeable_block is a block that is:
   . valid
   . non-empty (i.e. it has been allocated a non-empty size)
*)
record nonempty_block (m : mem) (b : block) : Prop ≝
{
  wb_valid      : valid_block m b;
  wb_nonempty   : low (blocks m b) < high (blocks m b)
}. 

(* Type stating that m2 is an extension of m1, parameterised by a list of blocks where we can write freely *)
record sr_memext (m1 : mem) (m2 : mem) (writeable : list block) : Prop ≝
{ (*  Non-empty blocks are preserved as they are. This entails [load_sim]. *)
  me_nonempty : ∀b. nonempty_block m1 b → nonempty_block m2 b ∧ blocks m1 b = blocks m2 b;
  (* These blocks are valid in [m2] *)
  me_writeable_valid : ∀b. meml ? b writeable → nonempty_block m2 b;
  (* blocks in [m1] than can be validly pointed to cannot be in [me_writeable]. *)
  me_not_writeable : ∀b. nonempty_block m1 b → ¬ (meml ? b writeable);
  (* This field does not entail [me_not_writeable] and is necessary to prove valid
     pointer conservation after a [free]. *)
  me_not_writeable_ptr : ∀p. valid_pointer m1 p = true → ¬ (meml ? (pblock p) writeable);
  
  (* Extension blocks contain nothing in [m1] *)
  (* me_not_mapped : ∀b. meml … b me_writeable → blocks m1 b = empty_block OZ OZ;  *)
  (* Valid pointers are still valid in m2. One could think that this is superfluous as
     being implied by me_inj, and it is but for a small detail: valid_pointer allows a pointer
     to be one off the end of a block bound. The internal check in beloadv does not.
     valid_pointer should be understood as "pointer making sense" rather than "pointer from
     which you can load stuff". [mi_valid_pointers] is used for instance when proving the
     semantics preservation for equality testing (where we check that the pointers we
     compare are valid before being equal).
  *)
  me_valid_pointers : ∀p. (* ¬ (freed_pointer m1 p) → *)
                       valid_pointer m1 p = true → 
                       valid_pointer m2 p = true
}.

(* If we have a memory extension, we can simulate loads *)
lemma sr_memext_load_sim : ∀m1,m2,writeable. sr_memext m1 m2 writeable → load_sim m1 m2.
#m1 #m2 #writeable #Hext #ptr #bev whd in match (beloadv ??) in ⊢ (% → %);
#H cut (nonempty_block m1 (pblock ptr) ∧ 
         Zle (low (blocks m1 (pblock ptr)))
               (Z_of_unsigned_bitvector 16 (offv (poff ptr))) ∧
         Zlt (Z_of_unsigned_bitvector 16 (offv (poff ptr)))
              (high (blocks m1 (pblock ptr))) ∧
        bev = (contents (blocks m1 (pblock ptr)) (Z_of_unsigned_bitvector 16 (offv (poff ptr)))))
[ @conj try @conj try @conj try %
  [ 1: @Zltb_true_to_Zlt ]
  cases (Zltb (block_id (pblock ptr)) (nextblock m1)) in H; normalize nodelta
  [ 1: //
  | 2,4,6,8,10: #Habsurd destruct ]
  generalize in match (Z_of_unsigned_bitvector offset_size (offv (poff ptr))); #z
  lapply (Zleb_true_to_Zle (low (blocks m1 (pblock ptr))) z)
  lapply (Zltb_true_to_Zlt z (high (blocks m1 (pblock ptr))))
  cases (Zleb (low (blocks m1 (pblock ptr))) z)
  cases (Zltb z (high (blocks m1 (pblock ptr)))) #H1 #H2
  [ 2,3,4,6,7,8,10,11,12,14,15,16: normalize #Habsurd destruct ] normalize #Heq
  lapply (H1 (refl ??)) lapply (H2 (refl ??))
  #Hle #Hlt destruct try assumption try @refl
  @(Zle_to_Zlt_to_Zlt … Hle Hlt) ]
* * * #Hnonempty #Hlow #Hhigh #Hres lapply (me_nonempty … Hext … Hnonempty) *
* #Hvalid #Hlt #Hblocks_eq
>(Zlt_to_Zltb_true … Hvalid) normalize <Hblocks_eq
>(Zle_to_Zleb_true … Hlow) >(Zlt_to_Zltb_true … Hhigh) normalize
>Hres @refl
qed.

(* --------------------------------------------------------------------------- *)
(* Some lemmas on environments and their contents *)


(* Definition of environment inclusion and equivalence *)
(* Environment "inclusion". *)
definition environment_sim ≝ λenv1,env2.
  ∀id, res. lookup SymbolTag block env1 id = Some ? res →
            lookup SymbolTag block env2 id = Some ? res.
            
lemma environment_sim_invert_aux : ∀en1,en2.
  (∀id,res. lookup_opt block id en1 = Some ? res → lookup_opt ? id en2 = Some ? res) →
  ∀id. lookup_opt ? id en2 = None ? → lookup_opt ? id en1 = None ?.
#en1 elim en1 try //
#opt1 #left1 #right1 #Hindl1 #Hindr1 #en2 #Hsim
normalize #id elim id normalize nodelta
[ 1: #Hlookup cases opt1 in Hsim; try // #res #Hsim lapply (Hsim one res (refl ??))
     #Hlookup2 >Hlookup2 in Hlookup; #H @H
| 2: #id' cases en2 in Hsim;
     [ 1: normalize  #Hsim #_ #_ lapply (Hsim (p1 id')) normalize nodelta
          cases (lookup_opt block id' right1) try //
          #res #Hsim' lapply (Hsim' ? (refl ??)) #Habsurd destruct
     | 2: #opt2 #left2 #right2 #Hsim #Hlookup whd in ⊢ ((??%?) → ?); #Hlookup'
          @(Hindr1 right2) try // #id0 #res0
          lapply (Hsim (p1 id0) res0) normalize #Hsol #H @Hsol @H ]
| 3: #id' cases en2 in Hsim;
     [ 1: normalize  #Hsim #_ #_ lapply (Hsim (p0 id')) normalize nodelta
          cases (lookup_opt block id' left1) try //
          #res #Hsim' lapply (Hsim' ? (refl ??)) #Habsurd destruct
     | 2: #opt2 #left2 #right2 #Hsim #Hlookup whd in ⊢ ((??%?) → ?); #Hlookup'
          @(Hindl1 left2) try // #id0 #res0
          lapply (Hsim (p0 id0) res0) normalize #Hsol #H @Hsol @H ]
] qed.          
            
lemma environment_sim_invert : 
  ∀en1,en2. environment_sim en1 en2 →
  ∀id. lookup SymbolTag block en2 id = None ? →
       lookup SymbolTag block en1 id = None ?.
* #en1 * #en2 #Hsim * #id @environment_sim_invert_aux
#id' #res #Hlookup normalize in Hsim;
lapply (Hsim (an_identifier … id') res) normalize #Hsol @Hsol @Hlookup
qed.

(* Environment equivalence. *)
definition environment_eq ≝ λenv1,env2. environment_sim env1 env2 ∧ environment_sim env2 env1.

lemma symmetric_environment_eq : ∀env1,env2. environment_eq env1 env2 → environment_eq env2 env1.
#env1 #env2 * #Hsim1 #Hsim2 % // qed.

lemma reflexive_environment_eq : ∀env. environment_eq env env.
#env % // qed.

(* An environment [e2] is a disjoint extension of [e1] iff (the new bindings are
   fresh and [e2] is equivalent to adding extension blocks to [e1]).  *)
definition disjoint_extension ≝
  λ(e1, e2 : env). 
  λ(new_vars : list (ident × type)).
 (∀id. mem_assoc_env id new_vars = true → lookup ?? e1 id = None ?) ∧          (* extension not in e1 *)
 (∀id. mem_assoc_env id new_vars = true → ∃res.lookup ?? e2 id = Some ? res) ∧ (* all of the extension is in e2 *)
 (∀id. mem_assoc_env id new_vars = false → lookup ?? e1 id = lookup ?? e2 id). (* only [new_vars] extends e2 *)
 
lemma disjoint_extension_to_inclusion :
  ∀e1,e2,vars. disjoint_extension e1 e2 vars →
  environment_sim e1 e2.
#e1 #e2 #vars * * #HA #HB #HC whd #id #res
@(match (mem_assoc_env id vars) return λx.(mem_assoc_env id vars = x) → ?
with
[ true ⇒ λH. ?
| false ⇒ λH. ?
] (refl ? (mem_assoc_env id vars)))
[ 1: #Hlookup lapply (HA ? H) #Habsurd >Habsurd in Hlookup; #H destruct
| 2: #Hlookup <(HC ? H) assumption ]
qed.

(* Small aux lemma to decompose folds on maps with list accumulators *)
lemma fold_to_concat : ∀A:Type[0].∀m:positive_map A.∀l.∀f.
 (fold ?? (λx,a,el. 〈an_identifier SymbolTag (f x), a〉::el) m l)
 = (fold ?? (λx,a,el. 〈an_identifier SymbolTag (f x), a〉::el) m []) @ l.
#A #m elim m
[ 1: #l #f normalize @refl
| 2: #optblock #left #right
     #Hind1 #Hind2 #l #f
     whd in match (fold ?????) in ⊢ (??%%);
     cases optblock
     [ 1: normalize nodelta >Hind1 >Hind2 >Hind2 in ⊢ (???%);
          >associative_append @refl
     | 2: #block normalize nodelta >Hind1 >Hind2 >Hind2 in ⊢ (???%);
          >Hind1 in ⊢ (???%); >append_cons <associative_append @refl
     ]
] qed.

lemma map_proj_fold : ∀A:Type[0].∀m:positive_map A. ∀f. ∀l.
  map ?? (λx.\snd  x) (fold ?? (λx,a,el.〈an_identifier SymbolTag x,a〉::el) m l) =
  map ?? (λx.\snd  x) (fold ?? (λx,a,el.〈an_identifier SymbolTag (f x),a〉::el) m l).
#A #m elim m
[ 1: #f #l normalize @refl
| 2: #opt #left #right #Hind1 #Hind2 #f #l
      normalize cases opt
      [ 1: normalize nodelta >fold_to_concat >fold_to_concat in ⊢ (???%);
           <map_append <map_append <Hind2 <Hind2 in ⊢ (???%); 
           <Hind1 <Hind1 in ⊢ (???%); @refl
      | 2: #elt normalize nodelta >fold_to_concat >fold_to_concat in ⊢ (???%);
           <map_append <map_append <Hind2 <Hind2 in ⊢ (???%); 
           <(Hind1 p0) <Hind1 in ⊢ (???%);
           >(fold_to_concat ?? (〈an_identifier SymbolTag one,elt〉::l))
           >(fold_to_concat ?? (〈an_identifier SymbolTag (f one),elt〉::l))
           <map_append <map_append normalize in match (map ??? (cons ???)); @refl
      ]
] qed.

lemma lookup_entails_block : ∀en:env.∀id,res. 
  lookup SymbolTag block en id = Some ? res →
  meml ? res (blocks_of_env en).
 * #map * #id #res
whd in match (blocks_of_env ?);
whd in match (elements ???);
whd in match (lookup ????);
normalize nodelta
lapply res lapply id -id -res
elim map
[ 1: #id #res normalize #Habsurd destruct (Habsurd)
| 2: #optblock #left #right #Hind1 #Hind2 #id #res #Hind3
     whd in match (fold ?????);
     cases optblock in Hind3;
     [ 1: normalize nodelta
          whd in match (lookup_opt ???);
          cases id normalize nodelta
          [ 1: #Habsurd destruct (Habsurd)
          | 2: #p #Hright lapply (Hind2 … Hright)
                normalize >fold_to_concat in ⊢ (? → %);
                <map_append #Haux @mem_append_backwards %1
                <map_proj_fold @Haux
          | 3: #p #Hleft lapply (Hind1 … Hleft)
                normalize >fold_to_concat in ⊢ (? → %);
                <map_append #Haux @mem_append_backwards %2
                <map_proj_fold @Haux ]
     | 2: #blo whd in match (lookup_opt ???);
          normalize >fold_to_concat <map_append
          cases id normalize nodelta
          [ 1: #Heq destruct (Heq)
               @mem_append_backwards %2 >fold_to_concat
               <map_append @mem_append_backwards %2 normalize %1 @refl
          | 2: #p #Hlookup lapply (Hind2 … Hlookup) #H
               @mem_append_backwards %1
               <map_proj_fold @H
          | 3: #p #Hlookup lapply (Hind1 … Hlookup) #H
               @mem_append_backwards %2 >fold_to_concat
               <map_append @mem_append_backwards %1
               <map_proj_fold @H
          ]
     ]
] qed.


lemma blocks_of_env_cons : 
  ∀en,id,hd. mem ? hd (blocks_of_env (add SymbolTag block en id hd)).
#en #id #hd @(lookup_entails_block … id)
cases id #p elim p try /2/ qed.

lemma in_blocks_exists_id : ∀env.∀bl. meml … bl (blocks_of_env env) → ∃id. lookup SymbolTag block env id = Some ? bl.
#env elim env #m elim m
[ 1: #bl normalize @False_ind
| 2: #opt #left #right #Hind1 #Hind2 #bl normalize
     >fold_to_concat <map_append #H
     elim (mem_append_forward ???? H)
     [ 1: <map_proj_fold -H #H lapply (Hind2 … H)
          * * #id #Hlookup normalize in Hlookup;
          %{(an_identifier SymbolTag (p1 id))} normalize nodelta @Hlookup
     | 2: <map_proj_fold cases opt
          [ 1: normalize -H #H lapply (Hind1 … H)
               * * #id #Hlookup normalize in Hlookup;
               %{(an_identifier SymbolTag (p0 id))} normalize nodelta @Hlookup
          | 2: #bl' normalize >fold_to_concat <map_append normalize
               #H' elim (mem_append_forward ???? H')
               [ 1: -H #H lapply (Hind1 … H) * * #id normalize #Hlookup
                    %{(an_identifier ? (p0 id))} normalize nodelta @Hlookup
               | 2: normalize * [ 2: @False_ind ]
                    #Heq destruct (Heq)
                    %{(an_identifier SymbolTag one)} @refl
               ]
          ]
     ]
] qed.

let rec inclusion_elim 
  (A : Type[0]) 
  (m1, m2 : positive_map A) 
  (P : positive_map A → positive_map A → Prop)
  (H1 : ∀m2. P (pm_leaf A) m2)
  (H2 : ∀opt1,left1,right1. P left1 (pm_leaf A) → P right1 (pm_leaf A) → P (pm_node A opt1 left1 right1) (pm_leaf A))
  (H3 : ∀opt1,left1,right1,opt2,left2,right2. P left1 left2 → P right1 right2 → P (pm_node A opt1 left1 right1) (pm_node A opt2 left2 right2))
  on m1 : P m1 m2 ≝
match m1 with
[ pm_leaf ⇒ 
  H1 m2
| pm_node opt1 left1 right1 ⇒
  match m2 with
  [ pm_leaf ⇒ 
    H2 opt1 left1 right1 (inclusion_elim A left1 (pm_leaf A) P H1 H2 H3) (inclusion_elim A right1 (pm_leaf A) P H1 H2 H3)
  | pm_node opt2 left2 right2 ⇒
    H3 opt1 left1 right1 opt2 left2 right2 (inclusion_elim A left1 left2 P H1 H2 H3) (inclusion_elim A right1 right2 P H1 H2 H3)
  ]
].

(* Environment inclusion entails block inclusion. *)
lemma environment_sim_blocks_inclusion :
  ∀env1, env2. environment_sim env1 env2 → lset_inclusion ? (blocks_of_env env1) (blocks_of_env env2).  
* #m1 * #m2 @(inclusion_elim … m1 m2) -m1 -m2
[ 1: #m2 normalize #_ @I
| 2: #opt1 #left1 #right1 #Hind1 #Hind2 #Hsim
      normalize >fold_to_concat in ⊢ (???%); <map_append @All_append
      [ 1: <map_proj_fold @Hind2 #id #res elim id #id' #Hlookup @(Hsim (an_identifier ? (p1 id')) res Hlookup)
      | 2: cases opt1 in Hsim;
           [ 1: normalize nodelta #Hsim
                <map_proj_fold @Hind1 #id #res elim id #id' #Hlookup @(Hsim (an_identifier ? (p0 id')) res Hlookup)
           | 2: #bl #Hsim lapply (Hsim (an_identifier ? one) bl ?) normalize try @refl
                #Habsurd destruct (Habsurd)
           ]
      ]
| 3: #opt1 #left1 #right1 #opt2 #left2 #right2 #Hind1 #Hind2 #Hsim
     normalize >fold_to_concat >fold_to_concat in ⊢ (???%);
     <map_append <map_append in ⊢ (???%); @All_append
     [ 1: cases opt2; normalize nodelta
          [ 1: <map_proj_fold <map_proj_fold in ⊢ (???%); <(map_proj_fold ?? p0)
               cut (environment_sim (an_id_map SymbolTag block right1) (an_id_map SymbolTag block right2))
               [ 1: * #id' #res #Hlookup
                    lapply (Hsim (an_identifier ? (p1 id')) res) normalize #H @H @Hlookup ]
               #Hsim' lapply (Hind2 Hsim') @All_mp
               #a #Hmem @mem_append_backwards %1 @Hmem
          | 2: #bl <map_proj_fold <map_proj_fold in ⊢ (???%); <(map_proj_fold ?? p0)
               cut (environment_sim (an_id_map SymbolTag block right1) (an_id_map SymbolTag block right2))
               [ 1: * #id' #res #Hlookup
                    lapply (Hsim (an_identifier ? (p1 id')) res) normalize #H @H @Hlookup ]
               #Hsim' lapply (Hind2 Hsim') @All_mp
               #a #Hmem @mem_append_backwards %1 @Hmem ]
     | 2: cut (environment_sim (an_id_map SymbolTag block left1) (an_id_map SymbolTag block left2))
          [ 1: * #id' #res #Hlookup
               lapply (Hsim (an_identifier ? (p0 id')) res) normalize #H @H @Hlookup ] #Hsim'
          lapply (Hind1 … Hsim') 
          <map_proj_fold <map_proj_fold in ⊢ (? → (???%)); <(map_proj_fold ?? p0)
          cases opt1 in Hsim; normalize nodelta
          [ 1: #Hsim @All_mp #a #Hmem @mem_append_backwards %2
               cases opt2 normalize nodelta
               [ 1: @Hmem
               | 2: #bl >fold_to_concat <map_append @mem_append_backwards %1 @Hmem ]
          | 2: #bl #Hsim #Hmem >fold_to_concat in ⊢ (???%); <map_append @All_append
               [ 2: normalize @conj try @I
                    cases opt2 in Hsim;
                     [ 1: #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??))
                          normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
                     | 2: #bl2 #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??))
                          normalize in ⊢ (% → ?); #Heq >Heq normalize nodelta
                          @mem_append_backwards %2 >fold_to_concat <map_append
                          @mem_append_backwards %2 normalize %1 @refl ]
               | 1: cases opt2 in Hsim;
                     [ 1: #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??))
                          normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
                     | 2: #bl2 #Hsim lapply (Hsim (an_identifier ? one) bl (refl ??))
                          normalize in ⊢ (% → ?); #Heq lapply (Hind1 Hsim')
                          @All_mp #a #Hmem >Heq normalize nodelta
                          @mem_append_backwards %2 >fold_to_concat <map_append
                          @mem_append_backwards %1 @Hmem ] ]
          ]
     ]
] qed.


(* equivalent environments yield "equal" sets of block (cf. frontend_misc.ma)  *)
lemma environment_eq_blocks_eq : ∀env1,env2.
  environment_eq env1 env2 →
  lset_eq ? (blocks_of_env env1) (blocks_of_env env2).
#env1 #env2 * #Hsim1 #Hsim2 @conj
@environment_sim_blocks_inclusion assumption
qed.

(* [env_codomain env vars] is the image of vars through env seen as a function. *)
definition env_codomain : env → list (ident×type) → lset block ≝ λe,l.
  foldi … (λid,block,acc.
    if mem_assoc_env … id l then
      block :: acc
    else
      acc
  ) e [ ].

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

(* Two equivalent memories yield a trivial memory extension. *)
lemma memory_eq_to_mem_ext : ∀m1,m2. memory_eq m1 m2 → sr_memext m1 m2 [ ].
* #contents1 #nextblock1 #Hpos * #contents2 #nextblock2 #Hpos' normalize *
#Hnextblock #Hcontents_eq destruct %
[ 1: #b #H @conj try % elim H try //
| 2: #b *
| 3: #b #_ normalize % //
| 4: #p #Hvalid % *
(* | 4: #b * *)
| 5: #p normalize >Hcontents_eq #H @H
] qed.

(* memory extensions form a preorder relation *)

lemma memory_ext_transitive : 
  ∀m1,m2,m3,writeable1,writeable2.
  sr_memext m1 m2 writeable1 → 
  sr_memext m2 m3 writeable2 → 
  sr_memext m1 m3 (writeable1 @ writeable2).
#m1 #m2 #m3 #writeable1 #writeable2 #H12 #H23 %
[ 1: #b #Hnonempty1
     lapply (me_nonempty … H12 b Hnonempty1) * #Hnonempty2 #Hblocks_eq
     lapply (me_nonempty … H23 b Hnonempty2) * #Hnonempty3 #Hblocks_eq' @conj
     try assumption >Hblocks_eq >Hblocks_eq' @refl
| 2: #b #Hmem lapply (mem_append_forward ???? Hmem) *
     [ 1: #Hmem12 lapply (me_writeable_valid … H12 b Hmem12) #Hnonempty2
          elim (me_nonempty … H23 … Hnonempty2) //
     | 2: #Hmem23 @(me_writeable_valid … H23 b Hmem23) ]
| 3: #b #Hvalid % #Hmem lapply (mem_append_forward ???? Hmem) *
     [ 1: #Hmem12
          lapply (me_not_writeable … H12 … Hvalid) * #H @H assumption
     | 2: #Hmem23 lapply (me_nonempty … H12 … Hvalid) * #Hvalid2
          lapply (me_not_writeable … H23 … Hvalid2) * #H #_ @H assumption
     ]
| 4: #p #Hvalid % #Hmem lapply (mem_append_forward ???? Hmem) *
     [ 1: #Hmem12
          lapply (me_not_writeable_ptr … H12 … Hvalid) * #H @H assumption
     | 2: #Hmem23
          lapply (me_valid_pointers … H12 … Hvalid) #Hvalid2
          lapply (me_not_writeable_ptr … H23 … Hvalid2) * #H @H assumption
     ]          
| 5: #p #Hvalid @(me_valid_pointers … H23) @(me_valid_pointers … H12) @Hvalid
] qed.

lemma memory_ext_reflexive : 
  ∀m. sr_memext m m [ ].
#m % /2/ #b * qed.

(* --------------------------------------------------------------------------- *)
(* Lift beloadv simulation to the front-end. *)       

(* Lift load_sim to loadn. *)
lemma load_sim_loadn :
 ∀m1,m2. load_sim m1 m2 →
 ∀sz,p,res. loadn m1 p sz = Some ? res → loadn m2 p sz = Some ? res.
#m1 #m2 #Hload_sim #sz
elim sz
[ 1: #p #res #H @H
| 2: #n' #Hind #p #res
     whd in match (loadn ???);
     whd in match (loadn m2 ??);
     lapply (Hload_sim p)
     cases (beloadv m1 p) normalize nodelta
     [ 1: #_ #Habsurd destruct (Habsurd) ]
     #bval #H >(H ? (refl ??)) normalize nodelta
     lapply (Hind (shift_pointer 2 p (bitvector_of_nat 2 1)))
     cases (loadn m1 (shift_pointer 2 p (bitvector_of_nat 2 1)) n')
     normalize nodelta
     [ 1: #_ #Habsurd destruct (Habsurd) ]
     #res' #H >(H ? (refl ??)) normalize
     #H @H
] qed.
 
(* Lift load_sim to front-end values. *)
lemma load_sim_fe :
  ∀m1,m2. load_sim m1 m2 →
  ∀ptr,ty,v.load_value_of_type ty m1 (pblock ptr) (poff ptr) = Some ? v →
            load_value_of_type ty m2 (pblock ptr) (poff ptr) = Some ? v.
#m1 #m2 #Hloadsim #ptr #ty #v
cases ty
[ 1: | 2: #sz #sg | 3: #fsz | 4: #ptrty | 5: #arrayty #arraysz | 6: #argsty #retty
| 7: #sid #fields | 8: #uid #fields | 9: #cptr_id ]
whd in match (load_value_of_type ????) in ⊢ ((??%?) → (??%?));
[ 1,7,8: #Habsurd destruct (Habsurd)
| 5,6: #H @H
| 2,3,4,9: 
  generalize in match (mk_pointer (pblock ptr) (poff ptr));
  elim (typesize ?)
  [ 1,3,5,7: #p #H @H
  | 2,4,6,8: #n' #Hind #p
      lapply (load_sim_loadn … Hloadsim (S n') p)
      cases (loadn m1 p (S n')) normalize nodelta
      [ 1,3,5,7: #_ #Habsurd destruct (Habsurd) ]      
      #bv #H >(H ? (refl ??)) #H @H
  ]
] qed.

(* --------------------------------------------------------------------------- *)
(* Lemmas relating reading and writing operation to memory properties. *)

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma nonempty_block_mismatch : ∀m,b,bl.
  nonempty_block (free m bl) b →
  nonempty_block m b ∧ b ≠ bl.
#m #b #bl #Hnonempty
@(eq_block_elim … b bl)
[ 1: #Heq >Heq in Hnonempty; * #_ normalize
     cases (block_region bl) normalize >eqZb_reflexive normalize *
| 2: #Hneq @conj try assumption elim Hnonempty #Hvalid #Hlh %
     [ 1: lapply Hvalid normalize //
     | 2: lapply Hlh normalize 
          cases (block_region b) normalize nodelta
          cases (block_region bl) normalize nodelta try //
          @(eqZb_elim … (block_id b) (block_id bl))
          [ 1,3: * normalize *
          | 2,4: #_ // ] ] ]
qed.

lemma eqb_to_eq_block : ∀a,b : block. a == b = eq_block a b.
#a #b lapply (eqb_true ? a b) @(eq_block_elim … a b)
/2 by neq_block_eq_block_false, true_to_andb_true/
qed.

(* We can free in both sides of a memory extension if we take care of removing
   the freed block from the set of writeable blocks. *)
lemma free_memory_ext :
  ∀m1,m2,writeable,bl.
   sr_memext m1 m2 writeable →
   sr_memext (free m1 bl) (free m2 bl) (lset_remove ? writeable bl).
#m1 #m2 #writeable #bl #Hext %
[ 1: #b #Hnonempty lapply (nonempty_block_mismatch … Hnonempty)
     * #Hnonempty' #Hblocks_neq lapply (me_nonempty … Hext … Hnonempty') *     
     #Hnonempty2 #Hcontents_eq @conj
     [ 1: % try @(wb_valid … Hnonempty2)
          whd in match (free ??);
          whd in match (update_block ?????);
          >(neq_block_eq_block_false … Hblocks_neq) normalize
          try @(wb_nonempty … Hnonempty2)
     | 2: whd in match (free ??) in ⊢ (??%%);
          whd in match (update_block ?????) in ⊢ (??%%);
          >(neq_block_eq_block_false … Hblocks_neq)
          normalize nodelta assumption ]          
| 2: #b #Hmem
     cut (mem block b writeable ∧ b ≠ bl)
     [ elim writeable in Hmem;
       [ 1: normalize *
       | 2: #hd #tl #Hind whd in match (filter ???);
            >eqb_to_eq_block
            @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta
            [ 1: #Heq #H whd in match (meml ???); elim (Hind H) #H0 #H1 @conj
                 [ 1: %2 ] assumption 
            | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); *
                 [ 1: #H destruct /3 by conj, or_introl, refl/
                 | 2: #H elim (Hind H) #H1 #H2 /3 by conj, or_intror, refl/ ] ] ]
     ] * #Hmem2 #Hblocks_neq
    lapply (me_writeable_valid … Hext … Hmem2) * #Hvalid #Hnonempty %
    try assumption whd in match (free ??); whd in match (update_block ?????);
    >(neq_block_eq_block_false … Hblocks_neq) @Hnonempty
| 3: #p #Hvalid lapply (nonempty_block_mismatch … Hvalid) * #Hnonempty #Hblocks_neq
     % #Hmem lapply (me_not_writeable … Hext … Hnonempty) * #H @H
     elim writeable in Hmem;
     [ 1: *
     | 2: #hd #tl #Hind whd in match (filter ???) in ⊢ (% → ?); >eqb_to_eq_block
          @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta
          [ 1: #Heq #H normalize %2 @(Hind H)
          | 2: #Hblocks_neq whd in match (meml ???); *
               [ 1: #Hneq normalize %1 assumption
               | 2: #Hmem normalize %2 @(Hind Hmem) ]
          ]
     ]
| 4: #p #Hvalid 
     lapply (valid_free_to_valid … Hvalid) #Hvalid'
     lapply (me_not_writeable_ptr … Hext … Hvalid') * #HA % #HB @HA     
     elim writeable in HB;
     [ 1: *
     | 2: #hd #tl #Hind whd in match (filter ???) in ⊢ (% → ?); >eqb_to_eq_block
          @(eq_block_elim … hd bl) normalize in match (notb ?); normalize nodelta
          [ 1: #Heq #H normalize %2 @(Hind H)
          | 2: #Hblocks_neq whd in match (meml ???); *
               [ 1: #Hneq normalize %1 assumption
               | 2: #Hmem normalize %2 @(Hind Hmem) ]
          ]
     ]
| 5: #p @(valid_pointer_free … writeable) @Hext
] qed.

(* Freeing from an extension block is ok. *) 
lemma memext_free_extended_conservation :
  ∀m1,m2 : mem.
  ∀writeable.
  ∀mem_hyp : sr_memext m1 m2 writeable.
  ∀b. meml ? b writeable → 
  sr_memext m1 (free m2 b) (lset_remove … writeable b).
#m1 #m2 #writeable #Hext #b #Hb_writeable %
[ 1: #bl #Hnonempty lapply (me_not_writeable … Hext … Hnonempty) #Hnot_mem
     lapply (mem_not_mem_neq … Hb_writeable Hnot_mem) #Hblocks_neq
     @conj
     [ 2: whd in match (free ??); whd in match (update_block ?????);
          >(neq_block_eq_block_false … (sym_neq … Hblocks_neq)) normalize
          elim (me_nonempty … Hext … Hnonempty) //
     | 1: % elim (me_nonempty … Hext … Hnonempty) * try //
          #Hvalid2 #Hlh #Hcontents_eq whd in match (free ??);
          whd in match (update_block ?????);
          >(neq_block_eq_block_false … (sym_neq … Hblocks_neq)) normalize assumption
    ]
| 2: #b' #Hmem (* contradiction in first premise *)
     cut (mem block b' writeable ∧ b' ≠ b)
     [ elim writeable in Hmem;
       [ 1: normalize @False_ind
       | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block
            @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta
            [ 1: #Heq #H whd in match (meml ???); destruct
                 elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption
            | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); *
                 [ 1: #H @conj [ 1: %1 @H | 2: destruct @Hneq ] 
                 | 2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ]
     ] ] ]
     * #Hb' #Hneq lapply (me_writeable_valid … Hext … Hb') #Hvalid %
     [ 1: @(wb_valid … Hvalid)
     | 2: whd in match (free ??);
          whd in match (update_block ?????);
          >(neq_block_eq_block_false … Hneq)
          @(wb_nonempty … Hvalid) ]
| 3: #b' #Hnonempty % #Hmem
     cut (mem block b' writeable ∧ b' ≠ b)
     [ elim writeable in Hmem;
       [ 1: normalize @False_ind
       | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block
            @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta
            [ 1: #Heq #H whd in match (meml ???); destruct
                 elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption
            | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); *
                 [ 1: #H @conj [ 1: %1 @H | 2: destruct @Hneq ] 
                 | 2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ]
     ] ] ] * #Hmem' #Hblocks_neq
     lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption
| 4: #p #Hnonempty % #Hmem
     cut (mem block (pblock p) writeable ∧ (pblock p) ≠ b)
     [ elim writeable in Hmem;
       [ 1: normalize @False_ind
       | 2: #hd #tl #Hind whd in match (filter ???); >eqb_to_eq_block
            @(eq_block_elim … hd b) normalize in match (notb ?); normalize nodelta
            [ 1: #Heq #H whd in match (meml ???); destruct
                 elim (Hind H) #Hmem #Hneq @conj try assumption %2 assumption
            | 2: #Hneq whd in match (meml ???) in ⊢ (% → %); *
                 [ 1: #H @conj [ 1: %1 @H | 2: destruct @Hneq ] 
                 | 2: #H elim (Hind H) #Hmem #Hneq' @conj try assumption %2 assumption ]
     ] ] ] * #Hmem' #Hblocks_neq
     lapply (me_not_writeable_ptr … Hext … Hnonempty) * #H @H assumption 
| 5: #p #Hvalid lapply (me_not_writeable_ptr … Hext … Hvalid) #Hnot_mem
     lapply (mem_not_mem_neq … Hb_writeable … Hnot_mem) #Hneq
     lapply (me_valid_pointers … Hext … Hvalid) #Hvalid'
     whd in match (free ??);
     whd in match (valid_pointer ??) in ⊢ (??%%);
     whd in match (low_bound ??); whd in match (high_bound ??);
     whd in match (update_block ?????);
     >(not_eq_block_rev … Hneq) normalize
     @Hvalid'
] qed.


  
  
lemma disjoint_extension_nil_eq_set :
  ∀env1,env2.
   disjoint_extension env1 env2 [ ] →
   lset_eq ? (blocks_of_env env1) (blocks_of_env env2).
#env1 #env whd in ⊢ (% → ?); * * #_ #_ #H normalize in H;
@environment_eq_blocks_eq whd @conj
#id #res >(H id) //
qed.

lemma free_list_equivalent_sets :
  ∀m,set1,set2.
  lset_eq ? set1 set2 →
  memory_eq (free_list m set1) (free_list m set2).
#m #set1 #set2 #Heq whd in match (free_list ??) in ⊢ (?%%);
@(lset_eq_fold block_DeqSet mem memory_eq  … Heq)
[ 1: @reflexive_memory_eq
| 2: @transitive_memory_eq
| 3: @symmetric_memory_eq
| 4: #x #acc1 #acc2
     whd in match (free ??) in ⊢ (? → (?%%));
     whd in match (memory_eq ??) in ⊢ (% → %); *
     #Hnextblock_eq #Hcontents_eq @conj try assumption
     #b normalize >Hcontents_eq @refl
| 5: #x1 #x2 #acc normalize @conj try @refl
     * * #id normalize nodelta cases (block_region x1)
     cases (block_region x2) normalize nodelta
     @(eqZb_elim id (block_id x1)) #Hx1 normalize nodelta
     @(eqZb_elim id (block_id x2)) #Hx2 normalize nodelta try @refl
| 6: * #r #i * #contents #nextblock #Hpos @conj
     [ 1: @refl
     | 2: #b normalize cases (block_region b) normalize
          cases r normalize cases (eqZb (block_id b) i)
          normalize @refl
     ]
] qed.

lemma foldr_identity : ∀A:Type[0]. ∀l:list A. foldr A ? (λx:A.λl0.x::l0) [] l = l.
#A #l elim l //
#hd #tl #Hind whd in match (foldr ?????); >Hind @refl
qed.

(* freeing equivalent sets of blocks on memory extensions yields memory extensions *)
lemma free_equivalent_sets :
  ∀m1,m2,writeable,set1,set2.
  lset_eq ? set1 set2 →
  sr_memext m1 m2 writeable →
  sr_memext (free_list m1 set1) (free_list m2 set2) (lset_difference ? writeable set1).
#m1 #m2 #writeable #set1 #set2 #Heq #Hext
lapply (free_list_equivalent_sets m2 … (symmetric_lset_eq … Heq))
#Heq
lapply (memory_eq_to_mem_ext … (symmetric_memory_eq … Heq)) #Hext'
lapply (memory_ext_transitive (free_list m1 set1) (free_list m2 set1) (free_list m2 set2) (filter block_eq (λwb:block_eq.¬wb∈set1) writeable) [ ] ? Hext')
[ 2: >append_nil #H @H ]
elim set1
[ 1: whd in match (free_list ??); whd in match (free_list ??);
     normalize >foldr_identity @Hext
| 2: #hd #tl #Hind >free_list_cons >free_list_cons
     lapply (free_memory_ext … hd … Hind)
     cut ((lset_remove block_eq (filter block_eq (λwb:block_eq.¬wb∈tl) writeable) hd) =
          (filter block_eq (λwb:block_eq.¬wb∈hd::tl) writeable))
     [ whd in match (lset_remove ???); elim writeable //
        #hd' #tl' #Hind_cut >filter_cons_unfold >filter_cons_unfold
        whd in match (memb ???) in ⊢ (???%); >eqb_to_eq_block
        (* elim (eqb_true block_DeqSet hd' hd)*)
        @(eq_block_elim … hd' hd) normalize nodelta
        [ 1: #Heq
             cases (¬hd'∈tl) normalize nodelta
             [ 1: whd in match (foldr ?????); >Heq >eqb_to_eq_block >eq_block_b_b normalize in match (notb ?);
                  normalize nodelta
                  lapply Hind_cut destruct #H @H
             | 2: lapply Hind_cut destruct #H @H ]
        | 2: #Hneq cases (¬hd'∈tl) normalize nodelta try assumption
             whd in match (foldr ?????); >eqb_to_eq_block
             >(neq_block_eq_block_false … Hneq)
             normalize in match (notb ?); normalize nodelta >Hind_cut @refl
        ]
    ]
    #Heq >Heq #H @H
] qed.

(* Remove a writeable block. *)
lemma memory_ext_weaken :
  ∀m1,m2,hd,writeable.
    sr_memext m1 m2 (hd :: writeable) →
    sr_memext m1 m2 writeable.
#m1 #m2 #hd #writeable * 
#Hnonempty #Hwriteable_valid #Hnot_writeable #Hnot_writeable_ptr #Hvalid_pointers %
try assumption
[ 1: #b #Hmem @Hwriteable_valid whd %2 assumption
| 2: #b #Hnonempty % #Hmem elim (Hnot_writeable … Hnonempty) #H @H whd %2 @Hmem
| 3: #p #Hvalid % #Hmem elim (Hnot_writeable_ptr … Hvalid) #H @H whd %2 @Hmem
] qed.

(* Perform a "rewrite" using lset_eq on the writeable blocks *)
lemma memory_ext_writeable_eq :
  ∀m1,m2,wr1,wr2.
    sr_memext m1 m2 wr1 →
    lset_eq ? wr1 wr2 →
    sr_memext m1 m2 wr2.
#m1 #m2 #wr1 #wr2 #Hext #Hset_eq %
[ 1: @(me_nonempty … Hext)
| 2:  #b #Hmem lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem)
      @(me_writeable_valid … Hext)
| 3: #b #Hnonempty % #Hmem 
     lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem'
     lapply (me_not_writeable … Hext … Hnonempty) * #H @H assumption
| 4: #p #Hvalid % #Hmem
     lapply (lset_eq_mem … (symmetric_lset_eq … Hset_eq) … Hmem) #Hmem'
     lapply (me_not_writeable_ptr … Hext … Hvalid) * #H @H assumption
| 5: @(me_valid_pointers … Hext) ]
qed.

axiom lset_inclusion_difference :
  ∀A : DeqSet.
  ∀s1,s2 : lset (carr A).
    lset_inclusion ? s1 s2 →
    ∃s2'. lset_eq ? s2 (s1 @ s2') ∧
          lset_disjoint ? s1 s2' ∧
          lset_eq ? s2' (lset_difference ? s2 s1).
          
lemma memory_eq_to_memory_ext_pre :
  ∀m1,m1',m2,writeable.
  memory_eq m1 m1' →
  sr_memext m1' m2 writeable →
  sr_memext m1 m2 writeable.
#m1 #m1' #m2 #writeable #Heq #Hext
lapply (memory_eq_to_mem_ext … Heq) #Hext'
@(memory_ext_transitive … Hext' Hext)
qed.

lemma memory_eq_to_memory_ext_post :
  ∀m1,m2,m2',writeable.
  memory_eq m2' m2 →
  sr_memext m1 m2' writeable →
  sr_memext m1 m2 writeable.
#m1 #m2 #m2' #writeable #Heq #Hext
lapply (memory_eq_to_mem_ext … Heq) #Hext'
lapply (memory_ext_transitive … Hext Hext') >append_nil #H @H
qed.

lemma lset_not_mem_difference :
  ∀A : DeqSet. ∀s1,s2,s3. lset_inclusion (carr A) s1 (lset_difference ? s2 s3) → ∀x. mem ? x s1 → ¬(mem ? x s3).
#A #s1 #s2 #s3 #Hincl #x #Hmem
lapply (lset_difference_disjoint ? s3 s2) whd in ⊢ (% → ?); #Hdisjoint % #Hmem_s3
elim s1 in Hincl Hmem;
[ 1: #_ *
| 2: #hd #tl #Hind whd in ⊢ (% → %); * #Hmem_hd #Hall *
     [ 2: #Hmem_x_tl @Hind assumption
     | 1: #Heq lapply (Hdisjoint … Hmem_s3 Hmem_hd) * #H @H @Heq ]
] qed.

lemma lset_difference_nil : ∀A,s. lset_difference A s [ ] = s. #A #s elim s //
#hd #tl #Hind >lset_difference_unfold normalize in match (memb ???); normalize nodelta >Hind @refl
qed.

lemma lset_mem_inclusion_mem :
  ∀A,s1,s2,elt.
  mem A elt s1 → lset_inclusion ? s1 s2 → mem ? elt s2.
#A #s1 elim s1
[ 1: #s2 #elt *
| 2: #hd #tl #Hind #s2 #elt *
     [ 1: #Heq destruct * //
     | 2: #Hmem_tl * #Hmem #Hall elim tl in Hall Hmem_tl;
          [ 1: #_ *
          | 2: #hd' #tl' #Hind * #Hmem' #Hall *
               [ 1: #Heq destruct @Hmem'
               | 2: #Hmem'' @Hind assumption ] ] ] ]
qed.

lemma lset_remove_inclusion :
  ∀A : DeqSet. ∀s,elt.
    lset_inclusion A (lset_remove ? s elt) s.
#A #s elim s try // qed.

lemma lset_difference_remove_inclusion :
  ∀A : DeqSet. ∀s1,s2,elt.
    lset_inclusion A 
      (lset_difference ? (lset_remove ? s1 elt) s2)  
      (lset_difference ? s1 s2).
#A #s elim s try // qed.

lemma lset_difference_permute :
  ∀A : DeqSet. ∀s1,s2,s3.
    lset_difference A s1 (s2 @ s3) =
    lset_difference A s1 (s3 @ s2).
#A #s1 #s2 elim s2 try //
#hd #tl #Hind #s3 >lset_difference_unfold2 >lset_difference_lset_remove_commute
>Hind elim s3 try //
#hd' #tl' #Hind' >cons_to_append >associative_append
>associative_append >(cons_to_append … hd tl)
>lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append
>lset_difference_unfold2 >lset_difference_lset_remove_commute >nil_append
<Hind' generalize in match (lset_difference ???); #foo
whd in match (lset_remove ???); whd in match (lset_remove ???) in ⊢ (??(?????%)?);
whd in match (lset_remove ???) in ⊢ (???%); whd in match (lset_remove ???) in ⊢ (???(?????%));
elim foo
[ 1: normalize @refl
| 2: #hd'' #tl'' #Hind normalize
      @(match (hd''==hd') return λx. ((hd''==hd') = x) → ? with
        [ true ⇒ λH. ?
        | false ⇒ λH. ?
        ] (refl ? (hd''==hd')))
      @(match (hd''==hd) return λx. ((hd''==hd) = x) → ? with
        [ true ⇒ λH'. ?
        | false ⇒ λH'. ?
        ] (refl ? (hd''==hd)))
      normalize nodelta
      try @Hind
[ 1: normalize >H normalize nodelta @Hind
| 2: normalize >H' normalize nodelta @Hind
| 3: normalize >H >H' normalize nodelta >Hind @refl
] qed.

lemma mem_not_mem_diff_aux :
  ∀s1,s2,s3,hd.
     mem ? hd s1 →
     ¬(mem ? hd s2) →
     mem block hd (lset_difference ? s1 (s2@(filter block_DeqSet (λx:block_DeqSet.¬x==hd) s3))).
#s1 #s2 #s3 #hd #Hmem #Hnotmem lapply Hmem lapply s1 -s1
elim s3
[ 1: #s1 >append_nil elim s1 try //
     #hd' #tl' #Hind *
     [ 1: #Heq >lset_difference_unfold
          @(match hd'∈s2 return λx. (hd'∈s2 = x) → ? with
            [ true ⇒ λH. ?
            | false ⇒ λH. ?
            ] (refl ? (hd'∈s2))) normalize nodelta
          [ 1: lapply (memb_to_mem … H) #Hmem elim Hnotmem #H' destruct
               @(False_ind … (H' Hmem))
          | 2: whd %1 assumption ]
     | 2: #Hmem >lset_difference_unfold
          @(match hd'∈s2 return λx. (hd'∈s2 = x) → ? with
            [ true ⇒ λH. ?
            | false ⇒ λH. ?
            ] (refl ? (hd'∈s2))) normalize nodelta
          [ 1:  @Hind @Hmem
          | 2: %2 @Hind @Hmem ] ]
| 2: #hd' #tl' #H #s1 #Hmem >filter_cons_unfold >eqb_to_eq_block
    @(eq_block_elim … hd' hd)
    [ 1:  >notb_true normalize nodelta #Heq @H @Hmem
    | 2: #Hneq >notb_false normalize nodelta
          >lset_difference_permute >(cons_to_append … hd')
          >associative_append >lset_difference_unfold2 >nil_append
          >lset_difference_permute @H
          elim s1 in Hmem; try //
          #hd'' #tl'' #Hind *
          [ 1: #Heq destruct whd in match (lset_remove ???);
               >eqb_to_eq_block >(neq_block_eq_block_false … (sym_neq … Hneq))
               >notb_false normalize nodelta %1 @refl
          | 2: #Hmem whd in match (lset_remove ???);
                cases (¬(hd''==hd')) normalize nodelta
                [ 1: %2 @Hind @Hmem
                | 2: @Hind @Hmem ] ] ]
] qed.                

lemma memext_free_extended_environment :
  ∀m1,m2,writeable.
   sr_memext m1 m2 writeable →
   ∀env,env_ext,vars. 
    disjoint_extension env env_ext vars →
    lset_inclusion ? (lset_difference ? (blocks_of_env env_ext) (blocks_of_env env)) writeable →
    sr_memext
      (free_list m1 (blocks_of_env env))
      (free_list m2 (blocks_of_env env_ext))
      (lset_difference ? writeable (blocks_of_env env_ext)).
#m1 #m2 #writeable #Hext #env #env_ext #vars #Hdisjoint #Hext_in_writeable
(* Disjoint extension induces environment "inclusion", i.e. simulation *)
lapply (disjoint_extension_to_inclusion … Hdisjoint) #Hincl
(* Environment inclusion entails set inclusion on the mapped blocks *)
lapply (environment_sim_blocks_inclusion … Hincl) #Hblocks_incl
(* This set inclusion can be decomposed on a common part and an extended part. *)
lapply (lset_inclusion_difference ??? Hblocks_incl)
* #extended_part * * #Hset_eq #Henv_disjoint_ext #Hextended_eq
lapply (lset_difference_lset_eq … writeable … Hset_eq) #HeqA
cut (lset_inclusion ? extended_part writeable)
[ 1: cases Hextended_eq #HinclA #_ @(transitive_lset_inclusion … HinclA … Hext_in_writeable) ]
-Hext_in_writeable #Hext_in_writeable
@(memory_ext_writeable_eq ????? (symmetric_lset_eq … HeqA))
lapply (free_list_equivalent_sets m2 ?? Hset_eq) #Hmem_eq
@(memory_eq_to_memory_ext_post … (symmetric_memory_eq … Hmem_eq))
(* Add extended ⊆ (lset_difference block_eq writeable (blocks_of_env env @ tl)) in Hind *)
cut (∀x. mem ? x extended_part → ¬ (mem ? x (blocks_of_env env)))
[ 1: cases Hextended_eq #Hincl_ext #_ @(lset_not_mem_difference … Hincl_ext) ]
lapply (proj2 … Hset_eq) lapply Hext_in_writeable
@(WF_rect ????? (filtered_list_wf block_DeqSet extended_part))
*
[ 1: #_ #_ #_ #_ #_ >append_nil
     @(free_equivalent_sets ???? (blocks_of_env env) (reflexive_lset_eq ??) Hext)
| 2: #hd #tl #Hwf_step #Hind_wf #Hext_in_writeable #Hset_incl #Hin_ext_not_in_env
     cut (lset_eq ? (blocks_of_env env@hd::tl) (hd::(blocks_of_env env@tl)))
     [ 1: >cons_to_append >cons_to_append in ⊢ (???%);
          @lset_eq_concrete_to_lset_eq // ]
     #Hpermute
     lapply (free_list_equivalent_sets m2 ?? Hpermute) #Hmem_eq2
     @(memory_eq_to_memory_ext_post … (symmetric_memory_eq … Hmem_eq2))
     >free_list_cons
     lapply (lset_difference_lset_eq … writeable … Hpermute) #HeqB
     @(memory_ext_writeable_eq ????? (symmetric_lset_eq … HeqB))
     >lset_difference_unfold2
     lapply (lset_difference_lset_remove_commute ? hd writeable (blocks_of_env env@tl))
     #Heq_commute >Heq_commute
     (* lapply (memory_ext_writeable_eq ????? (symmetric_lset_eq … Heq_commute)) *)
     lapply (Hind_wf (filter … (λx.¬(x==hd)) tl) ????)
     [ 2: @(transitive_lset_inclusion … Hset_incl)
          @lset_inclusion_concat_monotonic
          @cons_preserves_inclusion
          @lset_inclusion_filter_self
     | 3: @(transitive_lset_inclusion … Hext_in_writeable)
          @cons_preserves_inclusion
          @lset_inclusion_filter_self
     | 4: whd whd in ⊢ (???%);
          lapply (eqb_true ? hd hd) * #_ #H >(H (refl ??)) normalize in match (notb ?);
          normalize nodelta @refl
     | 1: #x #H @Hin_ext_not_in_env %2 elim tl in H; //
          #hd' #tl' #Hind >filter_cons_unfold >eqb_to_eq_block @(eq_block_elim … hd' hd)
          >notb_true >notb_false normalize nodelta
          [ 1: #Heq >Heq #H %2 @Hind @H
          | 2: #Hneq *
               [ 1: #Heq destruct %1 @refl
               | 2: #H %2 @Hind @H ] ]
     ]
     #Hext_ind
     lapply (Hin_ext_not_in_env … hd (or_introl … (refl ??)))
     #Hnot_in_env     
     lapply (memext_free_extended_conservation … Hext_ind hd ?)
     [ 1: @mem_not_mem_diff_aux try assumption elim Hext_in_writeable #H #_ @H ]
     -Hext_ind #Hext_ind
     cut (memory_eq (free (free_list m2 (blocks_of_env env@filter block_DeqSet (λx:block_DeqSet.¬x==hd) tl)) hd)
                    (free (free_list m2 (blocks_of_env env@tl)) hd))
     [ 1: <free_list_cons <free_list_cons
          @free_list_equivalent_sets @lset_eq_concrete_to_lset_eq
          >cons_to_append >cons_to_append in ⊢ (???%);
          @(transitive_lset_eq_concrete … (switch_lset_eq_concrete ????))
          @symmetric_lset_eq_concrete
          @(transitive_lset_eq_concrete ????? (switch_lset_eq_concrete ????))
          @lset_eq_to_lset_eq_concrete 
          elim (blocks_of_env env)
          [ 1: @symmetric_lset_eq @lset_eq_filter
          | 2: #hd0 #tl0 #Hind >cons_to_append 
               >associative_append in ⊢ (??%%);
               >associative_append in ⊢ (??%%);
               @cons_monotonic_eq @Hind ] ]
      #Hmem_eq3 @(memory_eq_to_memory_ext_post … Hmem_eq3)
      @(memory_ext_writeable_eq … Hext_ind)
      <lset_difference_lset_remove_commute <lset_difference_lset_remove_commute      
      <lset_difference_unfold2 <lset_difference_unfold2
      @lset_difference_lset_eq
      (* Note: exactly identical to the proof in the cut. *)
      @lset_eq_concrete_to_lset_eq
      >cons_to_append >cons_to_append in ⊢ (???%);
      @(transitive_lset_eq_concrete … (switch_lset_eq_concrete ????))
      @symmetric_lset_eq_concrete
      @(transitive_lset_eq_concrete ????? (switch_lset_eq_concrete ????))
      @lset_eq_to_lset_eq_concrete 
      elim (blocks_of_env env)
      [ 1: @symmetric_lset_eq @lset_eq_filter
      | 2: #hd0 #tl0 #Hind >cons_to_append 
           >associative_append in ⊢ (??%%);
           >associative_append in ⊢ (??%%);
           @cons_monotonic_eq @Hind ]
] qed.


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

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

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

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

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

(* Simulation relations. *)
inductive switch_cont_sim : (list ident) → cont → cont → Prop ≝
| swc_stop : ∀fvs.
    switch_cont_sim fvs Kstop Kstop
| swc_seq : ∀fvs,s,k,k',u,result.
    fresh_for_statement s u →
    switch_cont_sim fvs k k' →
    switch_removal s fvs u = Some ? result →
    switch_cont_sim fvs (Kseq s k) (Kseq (ret_st ? result) k')
| swc_while : ∀fvs,e,s,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.
*)

record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
  rg_find_symbol: ∀s.
    find_symbol ? ge s = find_symbol ? ge' s;
  rg_find_funct: ∀v,f.
    find_funct ? ge v = Some ? f →
    find_funct ? ge' v = Some ? (t f);
  rg_find_funct_ptr: ∀b,f.
    find_funct_ptr ? ge b = Some ? f →
    find_funct_ptr ? ge' b = Some ? (t f)
}.

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

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

(* [eventually ge P s tr] states that after a finite number of [exec_step], the 
   property P on states will be verified. *)
inductive eventually (ge : genv) (P : state → Prop) : state → trace → Prop ≝
| eventually_base : ∀s,t,s'.
    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
    P s' →
    eventually ge P s t
| eventually_step : ∀s,t,s',t',trace.
    exec_step ge s = Value io_out io_in ? 〈t, s'〉 →
    eventually ge P s' t' →
    trace = (t ⧺ t') →
    eventually ge P s trace.
    
(* [eventually] is not so nice to use directly, we would like to make the mandatory
 * [exec_step ge s = Value ??? 〈t, s'] visible - and in the end we would like not
   to give [s'] ourselves, but matita to compute it. Hence this little intro-wrapper. *)     
lemma eventually_now : ∀ge,P,s,t. 
  (∃s'.exec_step ge s = Value io_out io_in ? 〈t,s'〉 ∧ P s') → 
   eventually ge P s t.
#ge #P #s #t * #s' * #Hexec #HP %1{… Hexec HP}  (* %{E0} normalize >(append_nil ? t) %1{????? Hexec HP} *)
qed.

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

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


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

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


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

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

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

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

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

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

lemma while_fresh_lift : ∀e,s,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 some_inj : ∀A : Type[0]. ∀a,b : A. Some ? a = Some ? b → a = b. #A #a #b #H destruct (H) @refl qed.

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

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

(* Main theorem. To be ported and completed to memory injections. TODO *)
theorem switch_removal_correction :
  ∀ge,ge',s1, s1', tr, s2.
  switch_removal_globals ? fundef_switch_removal ge ge' →
  switch_state_sim ge s1 s1' →
  exec_step ge s1 = Value … 〈tr,s2〉 →
  eventually ge' (λs2'. switch_state_sim ge s2 s2') s1' tr.
#ge #ge' #st1 #st1' #tr #st2 #Hrelated #Hsim_state
@cthulhu
qed.

(*
inversion Hsim_state
[ 1: (* regular state *)
  #sss_statement #sss_result #sss_lu #sss_lu_fresh #sss_func #sss_func_tr #sss_new_vars
  #sss_func_hyp #sss_m #sss_m_ext #sss_env #sss_env_ext #sss_k #sss_k_ext #sss_writeable #sss_mem_hyp
  #sss_env_hyp #sss_result_hyp #sss_k_hyp #Hext_fresh_for_ge
  elim (sim_related_globals … ge ge'
             sss_env sss_m sss_env_ext sss_m_ext sss_writeable sss_new_vars
             sss_mem_hyp Hrelated sss_env_hyp Hext_fresh_for_ge)
  #Hsim_expr #Hsim_lvalue #Hst1_eq #Hst1_eq' #_
  cases sss_statement in sss_lu_fresh sss_result_hyp;
  (* Perform the intros for the statements *)
  [ 1: | 2: #lhs #rhs | 3: #retv #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
  | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
  | 14: #lab | 15: #cost #body ]
  #sss_lu_fresh #sss_result_hyp
  [ 1: (* Skip *)
    whd in match (switch_removal ???) in sss_result_hyp;
    <(some_inj ??? sss_result_hyp)
    inversion sss_k_hyp normalize nodelta
    [ 1: #fvs #Hfvs_eq #Hk #Hk' #_ #Hexec_step
         @(eventually_now ????) whd in match (exec_step ??);
         >(prod_eq_lproj ????? sss_func_hyp)
         >fn_return_simplify
         whd in match (exec_step ??) in Hexec_step;
         cases (fn_return sss_func) in Hexec_step;
         [ 1: | 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
         | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
         normalize nodelta
         whd in ⊢ ((??%?) → ?);
         [ 1: #H destruct (H) %{(Returnstate Vundef Kstop (free_list sss_m_ext (blocks_of_env sss_env_ext)))}
              @conj try @refl %3{(map (ident×type) ident \fst sss_new_vars)}
              [ 1: @(lset_difference ? sss_writeable (blocks_of_env sss_env_ext))
              | 3: @swc_stop
              | 2:
*)