include "Clight/Csyntax.ma".
include "Clight/TypeComparison.ma".

(* IG: used to prove preservation of the semantics. *)
include "Clight/Cexec.ma".
include "Clight/casts.ma".
include "Clight/CexecSound.ma".


(* include "ASM/AssemblyProof.ma". *) (* I had to manually copy some of the lemmas in this file, including an axiom ... *)

(* Attempt to remove unnecessary integer casts in Clight programs.

   This differs from the OCaml prototype by attempting to recursively determine
   whether subexpressions can be changed rather than using a fixed size pattern.
   As a result more complex expressions such as (char)((int)x + (int)y + (int)z)
   where x,y and z are chars can be simplified.
   
   A possible improvement that doesn't quite fit into this scheme would be to
   spot that casts can be removed in expressions like (int)x == (int)y where
   x and y have some smaller integer type.
 *)

(* Attempt to squeeze integer constant into a given type.

   This might be too conservative --- if we're going to cast it anyway, can't
   I just ignore the fact that the integer doesn't fit?
*)

(* [reduce_bits n m exp v] takes avector of size n + m + 1 and returns (if all goes well) a vector of size
 *  m+1 (an empty vector of bits makes no sense). It proceeds by removing /all/ the [n] leading bits equal
 * to [exp]. If it fails, it returns None. *)
let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝
match n return λn. BitVector (n+S m) → option (BitVector (S m)) with
[ O ⇒ λv. Some ? v
| S n' ⇒ λv. if eq_b (head' ?? v) exp then reduce_bits ?? exp (tail ?? v) else None ?
] v.

lemma reduce_bits_ok : ∀n,m.∀exp.∀v,v'. reduce_bits (S n) m exp v = Some ? v'→ reduce_bits n m exp (tail ?? v) = Some ? v'.
#n #m #exp #v #v' #H whd in H:(??%?); lapply H -H
cases (eq_b ? exp)
[ 1: #H whd in H:(??%?); //
| 2: #H normalize in H; destruct ] qed.

lemma reduce_bits_trunc : ∀n,m.∀exp.∀v:(BitVector (plus n (S m))).∀v'. 
  reduce_bits n m exp v = Some ? v' → v' = truncate n (S m) v.
#n #m elim n
[ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >vsplit_O_n //
| 2: #n' #Hind #exp #v #v' #H >truncate_tail
 > (Hind ??? (reduce_bits_ok ?? exp v v' H)) // ] qed.
 
lemma reduce_bits_dec : ∀n,m.∀exp.∀v. (∃v'.reduce_bits n m exp v = Some ? v') ∨ reduce_bits n m exp v = None ?.
#n #m #exp #v elim (reduce_bits n m exp v)
[ 1: %2 //
| 2: #v' %1 @(ex_intro … v') // ] qed.

(* pred_bitsize_of_intsize I32 = 31, … *)
definition pred_bitsize_of_intsize : intsize → nat ≝
λsz. pred (bitsize_of_intsize sz).

definition signed : signedness → bool ≝
λsg. match sg with [ Unsigned ⇒ false | Signed ⇒ true ].

(* [simplify_int sz sz' sg sg' i] tries to convert an integer [i] of width [sz] and signedness [sg] 
 * into an integer of size [sz'] of signedness [sg'].
 * - It first proceeds by comparing the source and target width: if the target width is strictly superior
 *   to the source width, the conversion fails. 
 * - If the size is equal, the argument is returned as-is.
 * - If the target type is strictly smaller than the source, it tries to squeeze the integer to
 *   the desired size. 
*)
let rec simplify_int (sz,sz':intsize) (sg,sg':signedness) (i:bvint sz) : option (bvint sz') ≝
  let bit ≝ signed sg ∧ head' … i in
  (* [nat_compare] does more than an innocent post-doc might think. It also computes the difference between the two args.
   * if x < y, nat_compare x y = lt(x, y-(x+1))  
   * if x = y, nat_compare x y = eq x
   * if x > y, nat_compare x y = gt(x-(y+1), y) *)
  match nat_compare (pred_bitsize_of_intsize sz) (pred_bitsize_of_intsize sz')
      return λn,m,x.BitVector (S n) → option (BitVector (S m)) with
  [ nat_lt _ _ ⇒ λi. None ?   (* refuse to make constants larger *)
  | nat_eq _ ⇒ λi. Some ? i
  | nat_gt x y ⇒ λi. 
      (* Here, we have [x]=31-([y]+1) and [y] ∈ {15; 7} OR [x] = 15-(7+1) and [y] = 7. I.e.: x=15,y=15 or x=23,y=7 or x=7,y=7.
       * In [reduce_bits n m bit i], [i] is supposed to have type BitVector n + (S m). Since its type is here (S x) + (S y),
       * we deduce that the actual arguments of [reduce_bits] are (S x) and (S y), which is consistent.
       * If [i] is of signed type and if it is negative, then it tries to remove the (S x) first "1" bits.
       * Otherwise, it tries to remove the (S x) first "0" bits.
       *)
      match reduce_bits ?? bit (i⌈BitVector (S (y+S x))↦BitVector ((S x) + (S y))⌉) with
      [ Some i' ⇒ 
        if signed sg' then 
          if eq_b bit (head' … i') then 
            Some ? i' 
          else None ? 
        else Some ? i'
      | None ⇒ None ?
      ]
  ] i.
>(commutative_plus_faster (S x)) @refl
qed.


lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
* normalize //
qed.

lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s).
* normalize // 
qed.

lemma type_eq_identity : ∀t. type_eq t t = true.
#t normalize elim (type_eq_dec t t)
[ 1: #Heq normalize //
| 2: #H destruct elim H #Hcontr elim (Hcontr (refl ? t)) ] qed.

lemma type_neq_not_identity : ∀t1, t2. t1 ≠ t2 → type_eq t1 t2 = false.
#t1 #t2 #Hneq normalize elim (type_eq_dec t1 t2)
[ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2))
| 2: #Hneq' normalize // ] qed.

definition size_le ≝ λsz1,sz2.
match sz1 with
[ I8 ⇒ True
| I16 ⇒ 
  match sz2 with
  [ I16 ⇒ True | I32 ⇒ True | _ ⇒ False ]
| I32 ⇒
  match sz2 with
  [ I32 ⇒ True | _ ⇒ False ]
].

definition size_lt ≝ λsz1,sz2.
match sz1 with
[ I8 ⇒
  match sz2 with
  [ I16 ⇒ True | I32 ⇒ True | _ ⇒ False ]
| I16 ⇒ 
  match sz2 with
  [ I32 ⇒ True | _ ⇒ False ]
| I32 ⇒ False
].

lemma size_lt_to_le : ∀sz1,sz2. size_lt sz1 sz2 → size_le sz1 sz2.
#sz1 #sz2 elim sz1 elim sz2 normalize // qed.

lemma size_lt_dec : ∀sz1,sz2. size_lt sz1 sz2 + (¬ (size_lt sz1 sz2)).
* * normalize /2/ /3/
qed.

lemma size_not_lt_to_ge : ∀sz1,sz2. ¬(size_lt sz1 sz2) → (sz1 = sz2) + (size_lt sz2 sz1).
* * normalize /2/ /3/
qed.

(* This function already exists in prop, we want it in type. *)
definition sign_eq_dect : ∀sg1,sg2:signedness. (sg1 = sg2) + (sg1 ≠ sg2).
* * normalize // qed.

lemma size_absurd : ∀a,b. size_le a b → size_lt b a → False.
* * normalize
#H1 #H2 try (@(False_ind … H1)) try (@(False_ind … H2)) qed. 
  
(* This defines necessary conditions for [src_expr] to be coerced to "target_ty".
 * Again, these are /not/ sufficient conditions. See [simplify_inv] for the rest. *)
definition necessary_conditions ≝ λsrc_sz.λsrc_sg.λtarget_sz.λtarget_sg.
match size_lt_dec target_sz src_sz with
[ inl Hlt ⇒ true
| inr Hnlt ⇒
  match sz_eq_dec target_sz src_sz with
  [ inl Hsz_eq ⇒
    match sign_eq_dect src_sg target_sg with
    [ inl Hsg_eq ⇒ false
    | inr Hsg_neq ⇒ true
    ]            
  | inr Hsz_neq ⇒ false
  ]
].

(* Inversion on necessary_conditions *)
lemma necessary_conditions_spec : 
  ∀src_sz,src_sg,target_sz, target_sg. (necessary_conditions src_sz src_sg target_sz target_sg = true) → 
      ((size_lt target_sz src_sz) ∨ (src_sz = target_sz ∧ src_sg ≠ target_sg)).
#src_sz #src_sg #target_sz #target_sg 
whd in match (necessary_conditions ????);
cases (size_lt_dec target_sz src_sz) normalize nodelta
[ 1: #Hlt #_ %1 //
| 2: #Hnlt 
     cases (sz_eq_dec target_sz src_sz) normalize nodelta
     [ 2: #_ #Hcontr destruct
     | 1: #Heq cases (sign_eq_dect src_sg target_sg) normalize nodelta
       [ 1: #_ #Hcontr destruct
       | 2: #Hsg_neq #_ %2 destruct /2/ ]
     ]
] qed.

(* Compare the results [r1,r2] of the evaluation of two expressions. If [r1] is an
 * integer value smaller but containing the same stuff than [r2] then all is well.
 * If the first evaluation is erroneous, we don't care about anything else. *)
definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res(val×trace).
match r1 with
[ OK res1 ⇒
  let 〈val1, tr1〉 ≝ res1 in
  ∀v1. val1 = Vint src_sz v1 →  
  match r2 with
  [ OK res2 ⇒ 
    let 〈val2, tr2〉 ≝ res2 in
    ∃v2. (val2 = Vint dst_sz v2 ∧
          v2 = cast_int_int src_sz sg dst_sz v1 ∧ tr1 = tr2 ∧ size_le dst_sz src_sz)    
  | _ ⇒ False ]
| Error errmsg1 ⇒ True
].

(* Simulation relation used for expression evaluation. *)
inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝
| SimOk   :  (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2
| SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2.

(* Trick to reduce checking time by eliminating a load of costly automation.
   It would be nice to do this by refactoring the type and code instead, but we
   don't want to spend lots of time on something that already works. *)

lemma SimFailNicely : ∀A,err,r2. res_sim A (Error ? err) r2.
#A #err #r2 @SimFail %{err} %
qed.

(* Invariant of simplify_expr *)
inductive simplify_inv (ge : genv) (en : env) (m : mem) (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝
(* Inv_eq states a standard simulation result. We enforce some needed equations on types to prove the cast cases. *)
| Inv_eq : ∀result_flag.
     result_flag = false →
     typeof e1 = typeof e2 →
     res_sim ? (exec_expr ge en m e1) (exec_expr ge en m e2) →
     res_sim ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) →     
     simplify_inv ge en m e1 e2 target_sz target_sg result_flag
(* Inv_coerce_ok states that we successfuly squeezed the source expression to [target_sz]. The details are hidden in [smaller_integer_val]. *)
| Inv_coerce_ok : ∀src_sz,src_sg.
     (typeof e1) = (Tint src_sz src_sg) →
     (typeof e2) = (Tint target_sz target_sg) →     
     (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) →
     simplify_inv ge en m e1 e2 target_sz target_sg true.
     
(* Invariant of simplify_inside *)     
definition conservation ≝ λe,result:expr.
∀ge,en,m. res_sim ? (exec_expr ge en m e) (exec_expr ge en m result)
                                                    ∧ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
                                                    ∧ typeof e = typeof result.

(* This lemma proves that simplify_int actually implements an integer cast. *)
(* The case 4 can be merged with cases 7 and 8. *)

lemma simplify_int_implements_cast : ∀sz,sz'.∀sg,sg'.∀i,i'. simplify_int sz sz' sg sg' i = Some ? i' → i' = cast_int_int sz sg sz' i.
* * 
[ 1: #sg #sg' #i #i' #Hsimp normalize in Hsimp ⊢ %; elim sg normalize destruct //
| 2,3,6: #sg #sg' #i #i' #Hsimp normalize in Hsimp; destruct (* ⊢ %; destruct destruct  whd in Hsimp:(??%?); destruct *)
| 4: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %;
    normalize in match (signed ?) in Hsimp;
    normalize in match (S (plus ??)) in Hsimp;
    normalize in match (plus 7 8) in Hsimp;
    lapply Hsimp -Hsimp
    cases (head' bool 15 i)
    normalize in match (andb ??);
    [ 1,3: elim (reduce_bits_dec 8 7 true i) 
      [ 1,3: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta
        [ 1: cases (eq_b true ?) normalize #H destruct normalize @refl
        | 2: #H destruct normalize @refl ]
      | 2,4: #Heq >Heq normalize nodelta #H destruct ]
    | 2,4,5,6,7,8:
      elim (reduce_bits_dec 8 7 false i) 
      [ 1,3,5,7,9,11: * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq)
        [ 1,3,4: cases (eq_b false ?) normalize nodelta
         #H destruct normalize @refl
        | 2,5,6: #H destruct normalize @refl ]
      | 2,4,6,8,10,12: #Heq >Heq normalize nodelta #H destruct
      ]
    ]
| 5,9: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); destruct @refl
| 7, 8: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %;
    normalize in match (signed ?) in Hsimp;
    normalize in match (S (plus ??)) in Hsimp;    
    normalize in match (plus 7 24) in Hsimp;
    lapply Hsimp -Hsimp
    cases (head' bool ? i)   
    normalize in match (andb ??);
    [ 1,3,9,11:
      [ 1,2: (elim (reduce_bits_dec 24 7 true i)) | 3,4: (elim (reduce_bits_dec 16 15 true i)) ]
      [ 1,3,5,7: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta
        [ 1,3: cases (eq_b true ?) normalize #H destruct normalize @refl
        | 2,4: #H destruct normalize @refl ]
      | 2,4,6,8: #Heq >Heq normalize nodelta #H destruct ]
    | 2,4,5,6,7,8,10,12,13,14,15,16: 
      [ 1,2,3,4,5,6: elim (reduce_bits_dec 24 7 false i)
      | 6,7,8,9,10,11,12: elim (reduce_bits_dec 16 15 false i) ]
      [ 1,3,5,7,9,11,13,15,17,19,21,23: 
        * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq)
        [ 1,3,4,7,9,10: 
          cases (eq_b false ?) normalize nodelta #H destruct normalize @refl
        | 2,5,6,8,11,12: #H destruct normalize @refl ]
      | 2,4,6,8,10,12,14,16,18,20,22,24: #Heq >Heq normalize nodelta #H destruct
      ]
    ]
] qed.

(* Facts about cast_int_int *)

(* copied from AssemblyProof *)
lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
 #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
 #n #hd #tl #abs @⊥ destruct (abs)
qed.

lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
 ∃hd.∃tl.v ≃ VCons A n hd tl.
 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
 [ #abs @⊥ destruct (abs)
 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
qed.

lemma vector_append_zero:
  ∀A,m.
  ∀v: Vector A m.
  ∀q: Vector A 0.
    v = q@@v.
  #A #m #v #q
  >(Vector_O A q) %
qed.

corollary prod_vector_zero_eq_left:
  ∀A, n.
  ∀q: Vector A O.
  ∀r: Vector A n.
    〈q, r〉 = 〈[[ ]], r〉.
  #A #n #q #r
  generalize in match (Vector_O A q …);
  #hyp
  >hyp in ⊢ (??%?);
  %
qed.
 
lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
# A #m #n elim m
[ 1: normalize #v
  elim (Vector_Sn ?? v) #hd * #tl #Eq
  @(ex_intro … (hd ::: [[]])) @(ex_intro … tl)
  >Eq normalize //
| 2: #n' #Hind #v
  elim (Vector_Sn ?? v) #hd * #tl #Eq
  elim (Hind tl)
  #tl1 * #tl2 #Eq_tl
  @(ex_intro … (hd ::: tl1))
  @(ex_intro … tl2)  
  destruct normalize //
] qed.

lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
# A #m #n elim m
[ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize //
| 2: #n' #Hind #v
  elim (Vector_Sn ?? v) #hd * #tl #Eq
  elim (Hind tl)
  #tl1 * #tl2 #Eq_tl
  @(ex_intro … (hd ::: tl1))
  @(ex_intro … tl2)  
  destruct normalize //
] qed.

lemma vsplit_zero:
  ∀A,m.
  ∀v: Vector A m.
    〈[[]], v〉 = vsplit A 0 m v.
  #A #m #v
  elim v
  [ %
  | #n #hd #tl #ih
    normalize in ⊢ (???%); %
  ]
qed.


lemma vsplit_zero2:
  ∀A,m.
  ∀v: Vector A m.
    〈[[]], v〉 = vsplit' A 0 m v.
  #A #m #v
  elim v
  [ %
  | #n #hd #tl #ih
    normalize in ⊢ (???%); %
  ]
qed.

(* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
axiom vsplit_succ:
  ∀A, m, n.
  ∀l: Vector A m.
  ∀r: Vector A n.
  ∀v: Vector A (m + n).
  ∀hd.
    v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)).

axiom vsplit_succ2:
  ∀A, m, n.
  ∀l: Vector A m.
  ∀r: Vector A n.
  ∀v: Vector A (m + n).
  ∀hd.
    v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)).
     
lemma vsplit_prod2:
  ∀A,m,n.
  ∀p: Vector A (m + n).
  ∀v: Vector A m.
  ∀q: Vector A n.
    p = v@@q → 〈v, q〉 = vsplit' A m n p.
  #A #m
  elim m
  [ #n #p #v #q #hyp
    >hyp <(vector_append_zero A n q v)
    >(prod_vector_zero_eq_left A …)
    @vsplit_zero2
  | #r #ih #n #p #v #q #hyp
    >hyp
    cases (Vector_Sn A r v)
    #hd #exists
    cases exists
    #tl #jmeq >jmeq
    @vsplit_succ2 [1: % |2: @ih % ] 
  ]
qed.

lemma vsplit_prod:
  ∀A,m,n.
  ∀p: Vector A (m + n).
  ∀v: Vector A m.
  ∀q: Vector A n.
    p = v@@q → 〈v, q〉 = vsplit A m n p.
  #A #m
  elim m
  [ #n #p #v #q #hyp
    >hyp <(vector_append_zero A n q v)
    >(prod_vector_zero_eq_left A …)
    @vsplit_zero
  | #r #ih #n #p #v #q #hyp
    >hyp
    cases (Vector_Sn A r v)
    #hd #exists
    cases exists
    #tl #jmeq >jmeq
    @vsplit_succ [1: % |2: @ih % ] 
  ]
qed.

lemma cast_decompose : ∀s1, v. cast_int_int I32 s1 I8 v = (cast_int_int I16 s1 I8 (cast_int_int I32 s1 I16 v)).
#s1 #v normalize elim s1 normalize nodelta 
normalize in v;
elim (vsplit_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
[ 2,4: //
| 1,3: #l * #r normalize nodelta #Eq1
       <(vsplit_prod bool 16 16 … Eq1)
       elim (vsplit_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
       [ 2,4: //
       | 1,3: #lr * #rr normalize nodelta #Eq2
              <(vsplit_prod bool 8 8 … Eq2)
              cut (v = (l @@ lr) @@ rr)
              [ 1,3 : destruct >(vector_associative_append ? 16 8) //
              | 2,4: #Hrewrite destruct
                     <(vsplit_prod bool 24 8 … Hrewrite) @refl
              ]
       ]
] qed.

lemma cast_idempotent : ∀s1,s2,sz1,sz2,v. size_lt sz1 sz2 → cast_int_int sz2 s1 sz1 (cast_int_int sz1 s2 sz2 v) = v.
#s1 #s2 * * #v elim s1 elim s2
normalize #H try @refl
@(False_ind … H)
qed.

lemma cast_identity : ∀sz,sg,v. cast_int_int sz sg sz v = v.
* * #v normalize // qed.

lemma cast_collapse : ∀s1,s2,v. cast_int_int I32 s1 I8 (cast_int_int I16 s2 I32 v) = (cast_int_int I16 s1 I8 v).
#s1 #s2 #v >cast_decompose >cast_idempotent 
[ 1: @refl | 2: // ]
qed.

lemma cast_composition_lt : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val.
   size_lt c_sz a_sz → size_lt c_sz b_sz →
   (cast_int_int a_sz a_sg c_sz val = 
        cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)).       
* #a_sg * #b_sg * #val whd in match (size_lt ??); whd in match (size_lt ??);
#Hlt1 #Hlt2
[ 1,2,3,4,5,6,7,8,9,10,11,12,14,15,17,18,19,20,21,23,24,27:
  @(False_ind … Hlt1) @(False_ind … Hlt2)
| 13,25,26: >cast_identity elim a_sg elim b_sg normalize //
| 22: normalize elim b_sg elim a_sg normalize
      normalize in val;
      elim (vsplit_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
      [ 2,4,6,8: normalize //
      | 1,3,5,7: #left * #right normalize #Eq1
                 <(vsplit_prod bool 16 16 … Eq1)
                 elim (vsplit_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
                 [ 2,4,6,8: //
                 | 1,3,5,7: #rightleft * #rightright normalize #Eq2
                            <(vsplit_prod bool 8 8 … Eq2)
                            cut (val = (left @@ rightleft) @@ rightright)
                            [ 1,3,5,7: destruct >(vector_associative_append ? 16 8) //
                            | 2,4,6,8: #Hrewrite destruct
                                       <(vsplit_prod bool 24 8 … Hrewrite) @refl
                            ]
                 ]
     ]
| 16: elim b_sg elim a_sg >cast_collapse @refl
] qed.

lemma cast_composition : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val.
   size_le c_sz a_sz → size_le c_sz b_sz →
   (cast_int_int a_sz a_sg c_sz val = 
        cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)).
#a_sz #a_sg #b_sz #b_sg #c_sz #val #Hle_c_a #Hle_c_b
cases (size_lt_dec c_sz a_sz)
cases (size_lt_dec c_sz b_sz)
[ 1: #Hltb #Hlta @(cast_composition_lt … Hlta Hltb)
| 2: #Hnltb #Hlta 
  cases (size_not_lt_to_ge  … Hnltb)
  [ 1: #Heq destruct >cast_identity //
  | 2: #Hltb @(False_ind … (size_absurd ?? Hle_c_b Hltb))
  ]
| 3: #Hltb #Hnlta  
  cases (size_not_lt_to_ge  … Hnlta)
  [ 1: #Heq destruct >cast_idempotent //
  | 2: #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
  ]
| 4: #Hnltb #Hnlta
  cases (size_not_lt_to_ge  … Hnlta)  
  cases (size_not_lt_to_ge  … Hnltb)
  [ 1: #Heq_b #Heq_a destruct >cast_identity >cast_identity //
  | 2: #Hltb #Heq @(False_ind … (size_absurd ?? Hle_c_b Hltb))
  | 3: #Eq #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
  | 4: #Hltb #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
  ]
] qed. 

let rec assert_int_value (v : option val) (expected_size : intsize) : option (BitVector (bitsize_of_intsize expected_size)) ≝
match v with
[ None ⇒ None ?
| Some v ⇒
  match v with
  [ Vint sz i ⇒
    match sz_eq_dec sz expected_size with
    [ inl Heq ⇒ Some ??
    | inr _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ]
].
>Heq in i; #i @i qed.

(* cast_int_int behaves as truncate (≃ vsplit) when downsizing *)
(* ∀src_sz,target_sz,sg. ∀i. size_le target_sz src_sz → cast_int_int src_sz sg target_sz i = truncate *)

lemma vsplit_to_truncate : ∀m,n,i. (\snd  (vsplit bool m n i)) = truncate  m n i.
#m #n #i normalize // qed.

(* Somme lemmas on how "simplifiable" operations behave under cast_int_int. *)

lemma integer_add_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz →
                               (addition_n (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz sg target_sz lhs_int)
                                    (cast_int_int src_sz sg target_sz rhs_int)
                             = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
#src_sz #target_sz #sg #lhs_int #rhs_int #Hlt                             
elim src_sz in Hlt lhs_int rhs_int; elim target_sz
[ 1,2,3,5,6,9: normalize #H @(False_ind … H)
| *: elim sg #_
  normalize in match (bitsize_of_intsize ?);
  normalize in match (bitsize_of_intsize ?);
  #lint #rint
  normalize in match (cast_int_int ????);
  normalize in match (cast_int_int ????);
  whd in match (addition_n ???);
  whd in match (addition_n ???) in ⊢ (???%);
  >vsplit_to_truncate >vsplit_to_truncate
  <truncate_add_with_carries
  [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint rint false);
  | 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint rint false);
  | 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint rint false);
  ]
  * #result #carry
  normalize nodelta //
qed.

lemma integer_add_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz →
                               (addition_n (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz sg target_sz lhs_int)
                                    (cast_int_int src_sz sg target_sz rhs_int)
                             = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
#src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct
>cast_identity >cast_identity >cast_identity // qed.

lemma integer_add_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz →
                               (addition_n (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz sg target_sz lhs_int)
                                    (cast_int_int src_sz sg target_sz rhs_int)
                             = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
#src_sz #target_sz #sg #lhs_int #rhs_int #Hle
cases (sz_eq_dec target_sz src_sz)
[ 1: #Heq @(integer_add_cast_eq … Heq)
| 2: #Hneq cut (size_lt target_sz src_sz)
     [ 1: elim target_sz in Hle Hneq; elim src_sz normalize //
           #_ * #H @(H … (refl ??))
     | 2: #Hlt @(integer_add_cast_lt … Hlt)
     ]
] qed.

lemma truncate_eat : ∀l,n,m,v. l = n → ∃tl. truncate (S n) m v = truncate l m tl.
#l #n #m #v #len elim (Vector_Sn … v) #hd * #tl #Heq >len
@(ex_intro … tl)
>Heq >Heq 
elim (vsplit_eq2 … tl) #l * #r #Eq
normalize
 <(vsplit_prod bool n m tl l r Eq)
 <(vsplit_prod2 bool n m tl l r Eq)
 normalize //
qed.


lemma integer_neg_trunc : ∀m,n. ∀i: BitVector (m+n). two_complement_negation n (truncate m n i) = truncate m n (two_complement_negation (m+n) i).
#m elim m
[ 1: #n #i normalize in i; 
     whd in match (truncate ???);
     whd in match (truncate ???) in ⊢ (???%);
     <vsplit_zero <vsplit_zero //
| 2: #m' #Hind #n #i normalize in i;
     elim (Vector_Sn … i) #hd * #tl #Heq     
     whd in match (two_complement_negation (S ?) ?);      
     >Heq in ⊢ (??%?); >truncate_tail whd in match (tail ???) in ⊢ (??%?);
     whd in match (two_complement_negation ??) in ⊢ (??%?);
     lapply (Hind ? tl) #H
     whd in match (two_complement_negation ??) in H;
     (* trying to reduce add_with_carries *)     
     normalize in match (S m'+n);
     whd in match (zero ?) in ⊢ (???%);
     >Heq in match (negation_bv ??) in ⊢ (???%); 
     whd in match (negation_bv ??) in ⊢ (???%);
     >add_with_carries_unfold in ⊢ (???%);
     normalize in ⊢ (???%); 
     cases hd normalize nodelta
     [ 1,2: <add_with_carries_unfold  in ⊢ (???%); (* Good. Some progress. *)
          (* try to transform the rhs of H into what we need. *)     
          whd in match (two_complement_negation ??) in H:(???%);
          lapply H -H
          generalize in match (add_with_carries (m'+n) (negation_bv (m'+n) tl) (zero (m'+n)) true);
          * #Left #Right normalize nodelta
          #H generalize in ⊢ (???(???(????(???(match % with [ _ ⇒ ? | _ ⇒  ?])))));
          #b >(vsplit_to_truncate (S m')) >truncate_tail 
          cases b
          normalize nodelta 
          normalize in match (tail ???); @H
     ]
] qed. (* This was painful. *)
     
lemma integer_sub_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz →
                               (subtraction (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz sg target_sz lhs_int)
                                    (cast_int_int src_sz sg target_sz rhs_int)
                             = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
#src_sz #target_sz #sg #lhs_int #rhs_int #Hlt                             
elim src_sz in Hlt lhs_int rhs_int; elim target_sz
[ 1,2,3,5,6,9: normalize #H @(False_ind … H)
| *: elim sg #_
  normalize in match (bitsize_of_intsize ?);
  normalize in match (bitsize_of_intsize ?);
  #lint #rint
  normalize in match (cast_int_int ????);
  normalize in match (cast_int_int ????);
  whd in match (subtraction ???);
  whd in match (subtraction ???) in ⊢ (???%);
  >vsplit_to_truncate >vsplit_to_truncate
  >integer_neg_trunc <truncate_add_with_carries
  [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint ? false);
  | 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint ? false);
  | 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint ? false);
  ]
  * #result #carry
  normalize nodelta //
qed.

lemma integer_sub_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz →
                               (subtraction (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz sg target_sz lhs_int)
                                    (cast_int_int src_sz sg target_sz rhs_int)
                             = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
#src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct
>cast_identity >cast_identity >cast_identity //
qed.

lemma integer_sub_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz →
                               (subtraction (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz sg target_sz lhs_int)
                                    (cast_int_int src_sz sg target_sz rhs_int)
                             = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
#src_sz #target_sz #sg #lhs_int #rhs_int #Hle
cases (sz_eq_dec target_sz src_sz)
[ 1: #Heq @(integer_sub_cast_eq … Heq)
| 2: #Hneq cut (size_lt target_sz src_sz)
     [ 1: elim target_sz in Hle Hneq; elim src_sz normalize //
           #_ * #H @(H … (refl ??))
     | 2: #Hlt @(integer_sub_cast_lt … Hlt)
     ]
] qed.

lemma simplify_int_success_lt : ∀sz,sg,sz',sg',i,i'. (simplify_int sz sz' sg sg' i=Some (bvint sz') i') → size_le  sz' sz.
* #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed.

lemma smaller_integer_val_identity : ∀sz,sg,x.
     smaller_integer_val sz sz sg x x.
#sz #sg *
[ 2: #error //
| 1: * #val #trace whd in match (smaller_integer_val ?????);
     #v1 #Hval %{v1} @conj try @conj try @conj //
     elim sz //
] qed.     

(* Inversion on exec_cast *)
lemma exec_cast_inv : ∀castee_val,src_sz,src_sg,cast_sz,cast_sg,m,result.
                         exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg) = OK ? result →
                         ∃i. castee_val = Vint src_sz i ∧ result = Vint cast_sz (cast_int_int src_sz src_sg cast_sz i).
#castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result
elim castee_val 
[ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
[ 2: | *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ]
whd in ⊢ ((??%?) → ?);
cases (sz_eq_dec sz' src_sz)
[ 1: #Heq destruct >intsize_eq_elim_true normalize nodelta #Heq destruct
     %{i}  /2/
| 2: #Hneq >intsize_eq_elim_false; try assumption #H destruct ]
qed.


(* Lemmas related to the Ebinop case *) 

lemma classify_add_int : ∀sz,sg. classify_add (Tint sz sg) (Tint sz sg) = add_case_ii sz sg.
* * // qed.

lemma classify_sub_int : ∀sz,sg. classify_sub (Tint sz sg) (Tint sz sg) = sub_case_ii sz sg.
* * // qed. 

lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true.
* * normalize #H @conj // qed.

(* Operations where it is safe to use a smaller integer type on the assumption
   that we would cast it down afterwards anyway. *)
definition binop_simplifiable ≝
λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ].

(* Inversion principle for integer addition *)
lemma iadd_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r →
                                    ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (addition_n (bitsize_of_intsize dsz) i1 i2)).
#sz #sg #v1 #v2 #m #r
elim v1
[ 1: | 2: #sz' #i | 3: #f | 4: | 5: #ptr ]
whd in ⊢ ((??%?) → ?); normalize nodelta
>classify_add_int normalize nodelta #H destruct 
elim v2 in H;
[ 1: | 2: #sz'' #i' | 3: #f' | 4:  | 5: #ptr' ]
whd in ⊢ ((??%?) → ?); #H destruct
elim (sz_eq_dec sz' sz'')
[ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
| 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
] qed. 

(* Inversion principle for integer subtraction. *)
lemma isub_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r →
                                    ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)).
#sz #sg #v1 #v2 #m #r
elim v1
[ 1: | 2: #sz' #i | 3: #f | 4:  | 5: #ptr ]
whd in ⊢ ((??%?) → ?); normalize nodelta
>classify_sub_int normalize nodelta #H destruct 
elim v2 in H;
[ 1: | 2: #sz'' #i' | 3: #f' | 4:  | 5: #ptr' ]
whd in ⊢ ((??%?) → ?); #H destruct
elim (sz_eq_dec sz' sz'')
[ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
| 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
] qed.

definition is_int : val → Prop ≝
λv.
match v with
[ Vint _ _ ⇒ True
| _ ⇒ False ].

(* "negative" (in the sense of ¬ Some) inversion principle for integer addition *)
lemma neg_iadd_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = None ? →
                                        ¬ (is_int v1) ∨ ¬ (is_int v2) ∨
                                        ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2.
#sz #sg #v1 #v2 #m
elim v1
[ 1: | 2: #sz' #i | 3: #f | 4:  | 5: #ptr ]
[ 2: | *: #_ %1 %1 % #H @H ]
elim v2
[ 1: | 2: #sz'' #i' | 3: #f' | 4:  | 5: #ptr' ]
[ 2: | *: #_ %1 %2 % #H @H ]
whd in ⊢ ((??%?) → ?); normalize nodelta
>classify_add_int normalize nodelta
elim (sz_eq_dec sz' sz'')
[ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd)
| 2: #Hneq >intsize_eq_elim_false try assumption #_ 
     %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj //
] qed. 

(* "negative" inversion principle for integer subtraction *)
lemma neg_isub_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = None ? →
                                        ¬ (is_int v1) ∨ ¬ (is_int v2) ∨
                                        ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2.
#sz #sg #v1 #v2 #m
elim v1
[ 1: | 2: #sz' #i | 3: #f | 4:  | 5: #ptr ]
[ 2: | *: #_ %1 %1 % #H @H ]
elim v2
[ 1: | 2: #sz'' #i' | 3: #f' | 4:  | 5: #ptr' ]
[ 2: | *: #_ %1 %2 % #H @H ]
whd in ⊢ ((??%?) → ?); normalize nodelta
>classify_sub_int normalize nodelta
elim (sz_eq_dec sz' sz'')
[ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd)
| 2: #Hneq >intsize_eq_elim_false try assumption #_ 
     %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj //
] qed.


lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m. 
   ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?.
#op #sz #sg #v1 #v2 #m #H
elim op normalize in match (binop_simplifiable ?); #H destruct
elim v1 in H;
[ 1,6: | 2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,8: #f | 4,9: | 5,10: #ptr ]
#_
whd in match (sem_binary_operation ??????); normalize nodelta
>classify_add_int normalize nodelta //
>classify_sub_int normalize nodelta //
qed.

notation > "hvbox('let' «ident x,ident y» 'as' ident E ≝ t 'in' s)"
 with precedence 10
for @{ match $t return λx.x = $t → ? with [ mk_Sig ${ident x} ${ident y} ⇒ λ${ident E}.$s ] (refl ? $t) }.

notation > "hvbox('let' « 〈ident x1,ident x2〉, ident y» 'as' ident E, ident F ≝ t 'in' s)"
 with precedence 10
for @{ match $t return λx.x = $t → ? with 
       [ mk_Sig ${fresh a} ${ident y} ⇒ λ${ident E}.
         match ${fresh a} return λx.x = ${fresh a} → ? with
         [ mk_Prod ${ident x1} ${ident x2} ⇒ λ${ident F}. $s ] (refl ? ${fresh a})
       ] (refl ? $t)
      }.

(* This function will make your eyes bleed. You've been warned.
 * Implements a correct-by-construction version of Brian's original cast-removal code. Does so by
 * threading an invariant defined in [simplify_inv], which says roughly "simplification yields either
   what you hoped for, i.e. an integer value of the right size, OR something equivalent to the original
   expression". [simplify_expr] is not to be called directly: simplify inside is the proper wrapper.
 * TODO: proper doc. Some cases are simplifiable. Some type equality tests are maybe dispensable.
 * This function is slightly more conservative than the original one, but this should be incrementally
 * modifiable (replacing calls to simplify_inside by calls to simplify_expr, + proving correction).
 * Also, I think that the proofs are factorizable to a great deal, but I'd rather have something
 * more or less "modular", case-by-case wise.
 *)
let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness) 
  : Σresult:bool×expr. ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝ 
match e return λx. x = e → ? with
[ Expr ed ty ⇒ λHexpr_eq.
  match ed return λx. ed = x → ? with
  [ Econst_int cst_sz i ⇒ λHdesc_eq.
    match ty return λx. x=ty → ? with
    [ Tint ty_sz sg ⇒ λHexprtype_eq.
      (* Ensure that the displayed type size [cst_sz] and actual size [sz] are equal ... *)
      match sz_eq_dec cst_sz ty_sz with
      [ inl Hsz_eq ⇒       
        match type_eq_dec ty (Tint target_sz target_sg) with
        [ inl Hdonothing   ⇒ «〈true, e〉, ?»
        | inr Hdosomething ⇒
          (* Do the actual useful work *)
          match simplify_int cst_sz target_sz sg target_sg i return λx. (simplify_int cst_sz target_sz sg target_sg i) = x → ? with
          [ Some i' ⇒ λHsimpl_eq. 
            «〈true, Expr (Econst_int target_sz i') (Tint target_sz target_sg)〉, ?»
          | None    ⇒ λ_. 
            «〈false, e〉, ?»
          ] (refl ? (simplify_int cst_sz target_sz sg target_sg i))
        ]
      | inr _ ⇒ (* The expression is ill-typed. *)
        «〈false, e〉, ?»
      ]
    | _ ⇒ λ_. 
      «〈false, e〉, ?» 
    ] (refl ? ty)    
  | Ederef e1 ⇒ λHdesc_eq.
      let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in  
      «〈false, Expr (Ederef e2) ty〉, ?»            
  | Eaddrof e1 ⇒ λHdesc_eq.
      let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in
      «〈false, Expr (Eaddrof e2) ty〉, ?»
  | Eunop op e1 ⇒ λHdesc_eq.
     let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in
      «〈false, Expr (Eunop op e2) ty〉, ?»
  | Ebinop op lhs rhs ⇒ λHdesc_eq.
      (* Type equality is enforced to prove the equalities needed in return by the invariant. *)
      match binop_simplifiable op 
      return λx. (binop_simplifiable op) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)))
      with
      [ true ⇒ λHop_simplifiable_eq.
        match assert_type_eq ty (typeof lhs) with
        [ OK Hty_eq_lhs ⇒
            match assert_type_eq (typeof lhs) (typeof rhs) with
            [ OK Htylhs_eq_tyrhs ⇒
                let «〈desired_type_lhs, lhs1〉, Hinv_lhs» as Hsimplify_lhs, Hpair_lhs ≝ simplify_expr lhs target_sz target_sg in
                let «〈desired_type_rhs, rhs1〉, Hinv_rhs» as Hsimplify_rhs, Hpair_rhs ≝ simplify_expr rhs target_sz target_sg in
                match desired_type_lhs ∧ desired_type_rhs
                return  λx. (desired_type_lhs ∧ desired_type_rhs) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)))
                with
                [ true ⇒ λHdesired_eq.
                  «〈true, Expr (Ebinop op lhs1 rhs1) (Tint target_sz target_sg)〉, ?»
                | false ⇒ λHdesired_eq.
                  let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
                  let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
                  «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»
                ] (refl ? (desired_type_lhs ∧ desired_type_rhs))
            | Error _ ⇒
                let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
                let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
                «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»  
            ]                   
        | Error _ ⇒
            let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
            let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
             «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»          
        ]
      | false ⇒ λHop_simplifiable_eq.
        let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
        let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
          «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»
      ] (refl ? (binop_simplifiable op))
  | Ecast cast_ty castee ⇒ λHdesc_eq.
      match cast_ty return λx. x = cast_ty → ? with
      [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq.
        match type_eq_dec ty cast_ty with
        [ inl Hcast_eq ⇒
          match necessary_conditions cast_sz cast_sg target_sz target_sg
          return λx. x = (necessary_conditions cast_sz cast_sg target_sz target_sg) → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)))
          with
          [ true ⇒ λHconditions.
              let «〈desired_type, castee1〉, Hcastee_inv» as Hsimplify1, Hpair1 ≝ simplify_expr castee target_sz target_sg in
              match desired_type return λx. desired_type = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)) 
              with
              [ true ⇒ λHdesired_eq.
                «〈true, castee1〉, ?»
              | false ⇒ λHdesired_eq.
                let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in
                match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))
                with
                [ true ⇒ λHdesired2_eq.
                  «〈false, castee2〉, ?»
                | false ⇒ λHdesired2_eq.
                  «〈false, Expr (Ecast ty castee2) cast_ty〉, ?»
                ] (refl ? desired_type2)
              ] (refl ? desired_type)
          | false ⇒ λHconditions.
              let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in
              match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))
              with
              [ true ⇒ λHdesired2_eq.
                «〈false, castee2〉, ?»
              | false ⇒ λHdesired2_eq.
                «〈false, Expr (Ecast ty castee2) cast_ty〉, ?»
              ] (refl ? desired_type2)
          ] (refl ? (necessary_conditions cast_sz cast_sg target_sz target_sg))
        | inr Hcast_neq ⇒
          (* inconsistent types ... *)
          let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in
          «〈false, Expr (Ecast cast_ty castee1) ty〉, ?»
        ] 
      | _ ⇒ λHcast_ty_eq.
        let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in
        «〈false, Expr (Ecast cast_ty castee1) ty〉, ?»
      ] (refl ? cast_ty)      
  | Econdition cond iftrue iffalse ⇒ λHdesc_eq.
      let «cond1, Hcond_equiv» as Hsimplify ≝ simplify_inside cond in
      match assert_type_eq ty (typeof iftrue) with
      [ OK Hty_eq_iftrue ⇒
          match assert_type_eq (typeof iftrue) (typeof iffalse) with
          [ OK Hiftrue_eq_iffalse ⇒
              let «〈desired_true, iftrue1〉, Htrue_inv» as Hsimplify_iftrue, Hpair_iftrue      ≝ simplify_expr iftrue target_sz target_sg in
              let «〈desired_false, iffalse1〉, Hfalse_inv» as Hsimplify_iffalse, Hpair_iffalse ≝ simplify_expr iffalse target_sz target_sg in         
              match desired_true ∧ desired_false
              return  λx. (desired_true ∧ desired_false) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)))
              with
              [ true ⇒ λHdesired_eq.
                «〈true, Expr (Econdition cond1 iftrue1 iffalse1) (Tint target_sz target_sg)〉, ?»
              | false ⇒ λHdesired_eq.
                let «iftrue1, Htrue_equiv» as Hsimplify_iftrue    ≝ simplify_inside iftrue in
                let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in
                «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?»      
              ] (refl ? (desired_true ∧ desired_false))
          | _ ⇒
            let «iftrue1, Htrue_equiv» as Hsimplify_iftrue    ≝ simplify_inside iftrue in
            let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in
            «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?»           
          ]
      | _ ⇒
        let «iftrue1, Htrue_equiv» as Hsimplify_iftrue    ≝ simplify_inside iftrue in
        let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in
        «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?»      
      ]
    (* Could probably do better with these, too. *)
  | Eandbool lhs rhs ⇒ λHdesc_eq.
      let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in
      let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in
      «〈false, Expr (Eandbool lhs1 rhs1) ty〉, ?»
  | Eorbool lhs rhs ⇒ λHdesc_eq.
      let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in
      let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in
      «〈false, Expr (Eorbool lhs1 rhs1) ty〉,?»
  (* Could also improve Esizeof *)
  | Efield rec_expr f ⇒ λHdesc_eq.
      let «rec_expr1, Hrec_expr_equiv» as Hsimplify ≝ simplify_inside rec_expr in
      «〈false,Expr (Efield rec_expr1 f) ty〉, ?»
  | Ecost l e1 ⇒ λHdesc_eq.
      (* The invariant requires that the toplevel [ty] type matches the type of [e1]. *)
      (* /!\ XXX /!\ We assume that the type of a cost-labelled expr is the type of the underlying expr. *)
      match type_eq_dec ty (typeof e1) with
      [ inl Heq ⇒
        let «〈desired_type, e2〉, Hinv» as Hsimplify, Hpair ≝ simplify_expr e1 target_sz target_sg in
        «〈desired_type, Expr (Ecost l e2) (typeof e2)〉, ?»
      | inr Hneq ⇒
        let «e2, Hexpr_equiv» as Eq ≝ simplify_inside e1 in
        «〈false, Expr (Ecost l e2) ty〉, ?»
      ]                
  | Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?»
(* | Evar id ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *)
  (* In order for the simplification function to be less dymp, we would have to use this line, which would in fact
     require to alter the semantics of [load_value_of_type].  *)
  | Evar id        ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» 
  | Esizeof t      ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» 
  ] (refl ? ed)
] (refl ? e)

and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝
match e return λx. x = e → ? with
[ Expr ed ty ⇒ λHexpr_eq.
  match ed return λx. x = ed → ? with
  [ Ederef e1 ⇒ λHdesc_eq.
    let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in
    «Expr (Ederef e2) ty, ?»
  | Eaddrof e1 ⇒ λHdesc_eq.
    let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in
    «Expr (Eaddrof e2) ty, ?»
  | Eunop op e1 ⇒ λHdesc_eq.
    let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in
    «Expr (Eunop op e2) ty, ?»
  | Ebinop op lhs rhs ⇒ λHdesc_eq.
    let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in
    let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in
    «Expr (Ebinop op lhs1 rhs1) ty, ?»
  | Ecast cast_ty castee ⇒ λHdesc_eq.
    match type_eq_dec ty cast_ty with
    [ inl Hcast_eq ⇒
       match cast_ty return λx. x = cast_ty → Σresult:expr. conservation e result
       with
       [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq.
          let «〈success, castee1〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr castee cast_sz cast_sg in
          match success return λx. x = success → Σresult:expr. conservation e result
         with
         [ true ⇒ λHsuccess_eq.
           «castee1, ?»
         | false ⇒ λHsuccess_eq.
           «Expr (Ecast cast_ty castee1) ty, ?»
          ] (refl ? success)
       | _ ⇒ λHcast_ty_eq.
          «e, ?»
       ] (refl ? cast_ty)
    | inr Hcast_neq ⇒
       «e, ?»    
    ]    
  | Econdition cond iftrue iffalse ⇒ λHdesc_eq.
    let «cond1, Hequiv_cond» as Eq_cond ≝ simplify_inside cond in
    let «iftrue1, Hequiv_iftrue» as Eq_iftrue ≝ simplify_inside iftrue in
    let «iffalse1, Hequiv_iffalse» as Eq_iffalse ≝ simplify_inside iffalse in
    «Expr (Econdition cond1 iftrue1 iffalse1) ty, ?»    
  | Eandbool lhs rhs ⇒ λHdesc_eq.
    let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in
    let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in
    «Expr (Eandbool lhs1 rhs1) ty, ?»      
  | Eorbool lhs rhs ⇒ λHdesc_eq.
    let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in
    let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in
    «Expr (Eorbool lhs1 rhs1) ty, ?»
  | Efield rec_expr f ⇒ λHdesc_eq.
    let «rec_expr1, Hequiv_rec» as Eq_rec ≝ simplify_inside rec_expr in
    «Expr (Efield rec_expr1 f) ty, ?»    
  | Ecost l e1 ⇒ λHdesc_eq.
    let «e2, Hequiv» as Eq ≝ simplify_inside e1 in
    «Expr (Ecost l e2) ty, ?»       
  | _ ⇒ λHdesc_eq.
    «e, ?»
  ] (refl ? ed)
] (refl ? e).
#ge #en #m
[ 1,3,5,6,7,8,9,10,11,12: %1 try @refl
     cases (exec_expr ge en m e) #res
     try (@(SimOk ???) //)
| 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct /by refl/
(*
     whd in match (exec_expr ????); >eq_intsize_identity whd
     >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ]
*)     
| 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) / by refl/
     whd in match (exec_expr ????);
     whd in match (exec_expr ????);
     >eq_intsize_identity >eq_intsize_identity whd
     #v1 #Heq destruct (Heq) %{i'} try @conj try @conj try @conj //
     [ 1: @(simplify_int_implements_cast … Hsimpl_eq)
     | 2: @(simplify_int_success_lt … Hsimpl_eq) ]
| 13: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res
      try (@(SimOk ???) //)
| 14: elim (type_eq_dec ty (Tint target_sz target_sg))
      [ 1: #Heq >Heq >type_eq_identity @(Inv_coerce_ok ??????? target_sz target_sg)
           destruct
           [ 1,2: //
           | 3: @smaller_integer_val_identity ]
      | 2: #Hneq >(type_neq_not_identity … Hneq) %1 // destruct
           @(SimOk ???) //
      ]
| 15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
    [ 1: (* Proving preservation of the semantics for expressions. *)
      cases Hexpr_sim
      [ 2: (* Case where the evaluation of e1 as an expression fails *)      
        normalize * #err #Hfail >Hfail normalize nodelta @SimFailNicely
      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
        #Hsim %1 * #val #trace normalize #Hstep
        cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧
                   (load_value_of_type ty m (pblock ptr) (poff ptr) = Some ? val))
        [ 1: lapply Hstep -Hstep
             cases (exec_expr ge en m e1)
             [ 1: * #val' #trace' normalize nodelta
                  cases val' normalize nodelta
                  [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct
                  | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
                       cases (load_value_of_type ty m (pblock pointer) (poff pointer)) in Heq;
                       normalize nodelta
                       [ 1: #Heq destruct | 2: #val2 #Heq destruct @conj // ]
                  ]
             | 2: normalize nodelta #errmesg #Hcontr destruct
             ]
        | 2: * #e1_ptr * #He1_eq_ptr #Hloadptr
             cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉) 
                       ∧ (load_value_of_type ty m (pblock ptr1) (poff ptr1) = Some ? val))
             [ 1: @(ex_intro … e1_ptr) @conj
                  [ 1: @Hsim // | 2: // ]
             | 2: * #e2_ptr * #He2_exec #Hload_e2_ptr
                normalize >He2_exec normalize nodelta >Hload_e2_ptr normalize nodelta @refl
             ]
        ]
     ]
   | 2: (* Proving the preservation of the semantics for lvalues. *)
      cases Hexpr_sim
      [ 2: (* Case where the evaluation of e1 as an lvalue fails *)
        normalize * #err #Hfail >Hfail normalize nodelta @SimFailNicely
      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
        #Hsim %1 * * #block #offset #trace normalize #Hstep        
        cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ pblock ptr = block ∧ poff ptr = offset)
        [ 1: lapply Hstep -Hstep
             cases (exec_expr ge en m e1)
             [ 1: * #val' #trace' normalize nodelta
                  cases val' normalize nodelta
                  [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct
                  | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
                       destruct try @conj try @conj //
                  ]
             | 2: normalize nodelta #errmesg #Hcontr destruct
             ] 
        | 2: * #e1_ptr * * #He1_eq_ptr #Hblock #Hoffset
             cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉)  ∧ pblock ptr1 = block ∧ poff ptr1 = offset) 
             [ 1: @(ex_intro … e1_ptr) @conj try @conj // @Hsim //
             | 2: * #e2_ptr * * #He2_exec #Hblock #Hoffset
                normalize >He2_exec normalize nodelta //
             ]
        ]
     ]
   ]
| 16: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
    [ 1: (* Proving preservation of the semantics for expressions. *)
      cases Hlvalue_sim
      [ 2: (* Case where the evaluation of e1 as an expression fails *)      
        * #err #Hfail whd in match (exec_expr ????); >Hfail @SimFailNicely
      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
        #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep
        cut (∃block,offset,ptype. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧
                                 (ty = Tpointer ptype) ∧
                                  val = Vptr (mk_pointer block offset))
        [ 1: lapply Hstep -Hstep
             cases (exec_lvalue ge en m e1)
             [ 1: * * #block #offset #trace' normalize nodelta
                  cases ty
                  [ 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 try (#Heq destruct)
                  @(ex_intro … block) @(ex_intro … offset) @(ex_intro … ptr_ty)
                  try @conj try @conj destruct //
             | 2: normalize nodelta #errmesg #Hcontr destruct
             ]
        | 2: * #block * #offset * #ptype * * #Hexec_lvalue #Hty_eq #Hval_eq 
             whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta
             //
        ]
     ]
    | 2: (* Proving preservation of the semantics of lvalues. *)
         @SimFailNicely
    ]
| 17: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
      [ 1: whd in match (exec_expr ge en m (Expr ??));
           whd in match (exec_expr ge en m (Expr ??));
           cases Hexpr_sim           
           [ 2: * #error #Hexec >Hexec normalize nodelta @SimFailNicely
           | 1: cases (exec_expr ge en m e1)
                [ 2: #error #Hexec normalize nodelta @SimFailNicely
                | 1: * #val #trace #Hexec
                     >(Hexec ? (refl ? (OK ? 〈val,trace〉)))
                     normalize nodelta @SimOk #a >Htype_eq #H @H
                ]
           ]
      | 2: @SimFailNicely
      ]
| 18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq
      inversion (Hinv_lhs ge en m)
      [ 1: #result_flag_lhs #Hresult_lhs #Htype_lhs #Hsim_expr_lhs #Hsim_lvalue_lhs #Hresult_flag_lhs_eq_true
           #Hinv <Hresult_flag_lhs_eq_true in Hresult_lhs; >Hdesired_lhs #Habsurd destruct
      | 2: #lhs_src_sz #lhs_src_sg #Htype_lhs #Htype_lhs1 #Hsmaller_lhs #Hdesired_type_lhs #_
           inversion (Hinv_rhs ge en m)
           [ 1: #result_flag_rhs #Hresult_rhs #Htype_rhs #Hsim_expr_rhs #Hsim_lvalue_rhs #Hdesired_type_rhs_eq #_
                <Hdesired_type_rhs_eq in Hresult_rhs; >Hdesired_rhs #Habsurd destruct
           | 2: #rhs_src_sz #rhs_src_sg #Htype_rhs #Htype_rhs1 #Hsmaller_rhs #Hdesired_type_rhs #_
                @(Inv_coerce_ok  ge en m … target_sz target_sg lhs_src_sz lhs_src_sg)
                [ 1: >Htype_lhs //
                | 2: //
                | 3: whd in match (exec_expr ??? (Expr ??));
                     whd in match (exec_expr ??? (Expr ??));
                     (* Tidy up the type equations *)
                     >Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Heq destruct
                     lapply Hsmaller_rhs lapply Hsmaller_lhs
                     generalize in match rhs_src_sz; #src_sz 
                     generalize in match rhs_src_sg; #src_sg
                     -Hsmaller_lhs -Hsmaller_rhs -Htype_lhs -Htype_rhs -Hinv_lhs -Hinv_rhs
                     >Htype_lhs1 >Htype_rhs1 -Htype_lhs1 -Htype_rhs1
                     (* Enumerate all the cases for the evaluation of the source expressions ... *)
                     cases (exec_expr ge en m lhs);
                     try // * #val_lhs #trace_lhs normalize nodelta
                     cases (exec_expr ge en m rhs);
                     try // * #val_rhs #trace_rhs normalize nodelta
                     whd in match (m_bind ?????);
                     (* specialize to the actual simplifiable operations. *)
                     cases op in Hop_simplifiable_eq;                     
                     [ 1,2: | *: normalize in ⊢ (% → ?); #H destruct (H) ] #_                     
                     [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m)
                     | 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m) ]
                     cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m)
                     [ 1,3: #_ #_ #_ normalize @I ]
                     #src_result #Hinversion_src elim (Hinversion_src src_result (refl ? (Some ? src_result)))
                     #src_result_sz * #i1 * #i2 * * #Hval_lhs_eq #Hval_rhs_eq #Hsrc_result_eq
                     whd in match (opt_to_res ???); whd in match (m_bind ?????); normalize nodelta
                     >Hval_lhs_eq >Hval_rhs_eq #Hsmaller_rhs #Hsmaller_lhs
                     whd
                     #result_int #Hsrc_result >Hsrc_result in Hsrc_result_eq; #Hsrc_result_eq             
                     lapply (sym_eq ??? Hsrc_result_eq) -Hsrc_result_eq #Hsrc_result_eq                     
                     cut (src_result_sz = src_sz) [ 1,3: destruct // ] #Hsz_eq
                     lapply Hsmaller_lhs lapply Hsmaller_rhs
                     cases (exec_expr ge en m lhs1) normalize nodelta
                     [ 2,4: destruct #error normalize in ⊢ (% → ?); #H @(False_ind … (H i1 (refl ? (Vint src_sz i1)))) ]
                     * #val_lhs1 #trace_lhs1
                     cases (exec_expr ge en m rhs1)
                     [ 2,4: destruct #error #_ normalize in ⊢ (% → ?); #H @(False_ind … (H i2 (refl ? (Vint src_sz i2)))) ]
                     * #val_rhs1 #trace_rhs1
                     whd in match (m_bind ?????); normalize nodelta
                     [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m)
                          lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m)
                     | 2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m)
                          lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m) ]
                     cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg) val_rhs1 (Tint target_sz target_sg) m)
                     [ 1,3: destruct #_ #Hneg_inversion elim (Hneg_inversion (refl ? (None ?)))
                            (* Proceed by case analysis on Hneg_inversion to prove the absurdity of this branch *)
                            *
                            [ 1,4: whd in ⊢ (? → % → ?); normalize nodelta
                                   #Habsurd #Hcounterexample elim (Hcounterexample i1 (refl ? (Vint src_sz i1)))
                                   #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd
                                   @(False_ind … (Habsurd I))
                            | 2,5: whd in ⊢ (? → ? → % → ?); normalize nodelta
                                   #Habsurd #_ #Hcounterexample elim (Hcounterexample i2 (refl ? (Vint src_sz i2)))
                                   #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd
                                   @(False_ind … (Habsurd I))
                            | 3,6: #dsz1 * #dsz2 * #j1 * #j2 * * #Hval_lhs1 #Hval_rhs1 #Hsz_neq
                                   whd in ⊢ (% → % → ?); normalize nodelta
                                   #Hsmaller_lhs #Hsmaller_rhs 
                                   elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1))) 
                                   #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le
                                   elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2)))
                                   #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_
                                   destruct elim Hsz_neq #Habsurd @(Habsurd (refl ? target_sz))
                           ]
                     | 2,4: destruct #result #Hinversion #_ #Hsmaller_lhs #Hsmaller_rhs normalize nodelta
                            elim (Hinversion result (refl ? (Some ? result)))
                            #result_sz * #lhs_int * #rhs_int * * #Hlhs1_eq #Hrhs1_eq #Hop_eq
                            elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1))) 
                            #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le
                            elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2)))
                            #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_
                            destruct
                            [ 1: %{(addition_n (bitsize_of_intsize target_sz)
                                     (cast_int_int src_sz src_sg target_sz i1)
                                     (cast_int_int src_sz src_sg target_sz i2))}
                                 try @conj try @conj try @conj //
                                 >integer_add_cast_le try //
                            | 2: %{(subtraction (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz src_sg target_sz i1)
                                    (cast_int_int src_sz src_sg target_sz i2))}
                                 try @conj try @conj try @conj //
                                 >integer_sub_cast_le try //
                            ]
                     ] ] ] ]
| 19,20,21,22: destruct %1 try @refl
   elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs
   elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs
   [ 1,3,5,7: 
      whd in match (exec_expr ????); whd in match (exec_expr ????);
      cases Hexpr_sim_lhs
      [ 2,4,6,8: * #error #Herror >Herror @SimFailNicely
      | *: cases (exec_expr ge en m lhs)
           [ 2,4,6,8: #error #_ @SimFailNicely
           | *: * #lval #ltrace #Hsim_lhs normalize nodelta         
                cases Hexpr_sim_rhs
                [ 2,4,6,8: * #error #Herror >Herror @SimFailNicely
                | *: cases (exec_expr ge en m rhs)
                     [ 2,4,6,8: #error #_  @SimFailNicely
                     | *: * #rval #rtrace #Hsim_rhs
                          whd in match (exec_expr ??? (Expr (Ebinop ???) ?));
                          >(Hsim_lhs 〈lval,ltrace〉 (refl ? (OK ? 〈lval,ltrace〉)))
                          >(Hsim_rhs 〈rval,rtrace〉 (refl ? (OK ? 〈rval,rtrace〉)))
                          normalize nodelta
                          >Htype_eq_lhs >Htype_eq_rhs
                          @SimOk * #val #trace #H @H
                     ]
                ]
           ]
      ]
   | *: @SimFailNicely
   ]
(* Jump to the cast cases *)   
| 23,30,31,32,33,34,35,36: %1 try @refl
  [ 1,4,7,10,13,16,19,22: destruct // ]
  elim (Hcastee_equiv ge en m) * #Hexec_sim #Hlvalue_sim #Htype_eq
  (* exec_expr simulation *)
  [ 1,3,5,7,9,11,13,15: cases Hexec_sim
       [ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail whd in match (exec_expr ge en m ?);
            >Hexec_fail @SimFailNicely
       | 1,3,5,7,9,11,13,15: #Hsim @SimOk * #val #trace <Hexpr_eq >Hdesc_eq
            whd in match (exec_expr ge en m ?); #Hstep
            cut (∃v1. exec_expr ge en m castee = OK ? 〈v1,trace〉
                    ∧ exec_cast m v1 (typeof castee) cast_ty = OK ? val)
            [ 1,3,5,7,9,11,13,15: 
                 lapply Hstep -Hstep cases (exec_expr ge en m castee)
                 [ 2,4,6,8,10,12,14,16: #error1 normalize nodelta #Hcontr destruct
                 | 1,3,5,7,9,11,13,15: * #val1 #trace1 normalize nodelta
                      #Hstep @(ex_intro … val1)
                      cases (exec_cast m val1 (typeof castee) cast_ty) in Hstep;
                      [ 2,4,6,8,10,12,14,16: #error #Hstep normalize in Hstep; destruct
                      | 1,3,5,7,9,11,13,15: #result #Hstep normalize in Hstep; destruct
                           @conj @refl
                      ]
                 ]
            | 2,4,6,8,10,12,14,16: * #v1 * #Hexec_expr #Hexec_cast
                 whd in match (exec_expr ge en m ?);
                 >(Hsim … Hexec_expr ) normalize nodelta
                 <Htype_eq >Hexec_cast //
            ]   
      ]
  | 2,4,6,8,10,12,14,16: destruct  @SimFailNicely
  ]
| 24: destruct inversion (Hcastee_inv ge en m)
  [ 1: #result_flag #Hresult_flag #Htype_eq #Hexpr_sim #Hlvalue_sim #Hresult_flag_2 
       <Hresult_flag_2 in Hresult_flag; #Hcontr destruct
  | 2: #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller_eval #_ #Hinv_eq
       @(Inv_coerce_ok ??????? cast_sz cast_sg)
       [ 1: // | 2: <Htype_castee1 //
       | 3: whd in match (exec_expr ??? (Expr ??));
            >Htype_castee
            (* Simplify the goal by culling impossible cases, using Hsmaller_val *)
            cases (exec_expr ge en m castee) in Hsmaller_eval;
            [ 2: #error //
            | 1: * #castee_val #castee_trace #Hsmaller normalize nodelta
              lapply (exec_cast_inv castee_val src_sz src_sg cast_sz cast_sg m)
              cases (exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg))
              [ 2: #error #_ @I
              | 1: #result #Hinversion elim (Hinversion result (refl ? (OK ? result))) 
                   #castee_int * #Hcastee_val_eq #Hresult_eq
                   whd in match (m_bind ?????);
                   #result_int #Hresult_eq2
                   cases (exec_expr ge en m castee1) in Hsmaller;
                   [ 2: #error normalize in ⊢ (% → ?); #Habsurd 
                        @(False_ind … (Habsurd castee_int Hcastee_val_eq))
                   | 1: * #val1 #trace1 whd in ⊢ (% → ?); normalize nodelta
                        #Hsmaller elim (Hsmaller castee_int Hcastee_val_eq)
                        #val1_int * * * #Hval1_eq #Hval1_int_eq #Hcastee_trace_eq 
                        destruct #Hle %{(cast_int_int src_sz src_sg target_sz castee_int)}
                        try @conj try @conj try @conj try //                                                
                        [ 1: @cast_composition ] try assumption
                        elim (necessary_conditions_spec … (sym_eq … Hconditions))
                        [ 2,4: * #Heq >Heq #_ elim target_sz //
                        | 1,3: #Hlt @(size_lt_to_le ?? Hlt) ]
 ] ] ] ] ]
| 25,27: destruct
      inversion (Hcast2 ge en m)
      [ 1,3: (* Impossible case.  *)
           #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hresult_contr <Hresult_contr in Hresult;
           #Hcontr destruct
      | 2,4: (* We successfuly cast the expression to the desired type. We can thus get rid of the "cast" itself.
              We did not successfuly cast the subexpression to target_sz, though. *)
           #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq
           @(Inv_eq ???????) //
           [ 1,3: >Htype_castee2 //
           | 2,4: (* Prove simulation for exec_expr *)
               whd in match (exec_expr ??? (Expr ??));
               cases (exec_expr ge en m castee) in Hsmaller_eval;
               [ 2,4: (* erroneous evaluation of the original expression *)
                     #error #Hsmaller_eval @SimFailNicely
               | 1,3: * #val #trace normalize nodelta >Htype_castee
                      lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m)
                      cases (exec_cast m val (Tint src_sz src_sg) (Tint cast_sz cast_sg))
                      [ 2,4: #error #_ #_ @SimFailNicely
                      | 1,3: #result #Hinversion elim (Hinversion result (refl ??))
                             #val_int * #Hval_eq #Hresult_eq
                             cases (exec_expr ge en m castee2)
                             [ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … (Hsmaller_eval val_int Hval_eq))
                             | 1,3: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq)
                                    #val1_int * * * #Hval1_eq #Hcast_eq #Htrace_eq #Hle
                                    destruct @SimOk normalize #a #H @H ]
                ] ]
      ] ]
| 26,28: destruct
      inversion (Hcast2 ge en m)
      [ 2,4: (* Impossible case. *)
            #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #Habsurd #Hinv_eq
            (* Do some gymnastic to transform the Habsurd jmeq into a proper, 'destruct'able eq *)
            letin Habsurd_eq ≝ (jmeq_to_eq ??? Habsurd) lapply Habsurd_eq
            -Habsurd_eq -Habsurd #Habsurd destruct
      | 1,3: (* All our attempts at casting down the expression have failed. We still use the
               resulting expression, as we may have discovered and simplified unrelated casts. *)
            #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #_ #Hinv
            @(Inv_eq ???????) //
                 whd in match (exec_expr ??? (Expr ??));
                 whd in match (exec_expr ??? (Expr ??));
                 cases Hsim_expr
                 [ 2,4: * #error #Hexec_err >Hexec_err @SimFailNicely
                 | 1,3: #Hexec_ok
                      cases (exec_expr ge en m castee) in Hexec_ok;
                      [ 2,4: #error #Hsim @SimFailNicely
                      | 1,3: * #val #trace #Hsim normalize nodelta
                           >Htype_eq >(Hsim 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) normalize nodelta
                           @SimOk #a #H @H
                      ]
                 ]
      ]
| 29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
      @(Inv_eq ???????) //
      whd in match (exec_expr ??? (Expr ??));
      whd in match (exec_expr ??? (Expr ??));
      cases Hsim_expr
           [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
           | 1: #Hexec_ok @SimOk * #val #trace
                cases (exec_expr ge en m castee) in Hexec_ok;
                [ 2: #error #Habsurd normalize in Habsurd; normalize nodelta #H destruct
                | 1: * #val #trace #Hexec_ok normalize nodelta
                     >(Hexec_ok … 〈val, trace〉 (refl ? (OK ? 〈val, trace〉)))
                     >Htype_eq
                     normalize nodelta #H @H
                ]
           ]
| 37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq
      inversion (Htrue_inv ge en m)
      [ 1: #result_flag_true #Hresult_true #Htype_true #Hsim_expr_true #Hsim_lvalue_true #Hresult_flag_true_eq_false
           #Hinv <Hresult_flag_true_eq_false in Hresult_true; >Hdesired_true #Habsurd destruct
      | 2: #true_src_sz #true_src_sg #Htype_eq_true #Htype_eq_true1 #Hsmaller_true #_ #Hinv_true 
           inversion (Hfalse_inv ge en m)
           [ 1: #result_flag_false #Hresult_false #Htype_false #Hsim_expr_false #Hsim_lvalue_false #Hresult_flag_false_eq_false
                #Hinv <Hresult_flag_false_eq_false in Hresult_false; >Hdesired_false #Habsurd destruct
           | 2: #false_src_sz #false_src_sg #Htype_eq_false #Htype_eq_false1 #Hsmaller_false #_ #Hinv_false
                >Htype_eq_true @(Inv_coerce_ok ??????? true_src_sz true_src_sg)
                [ 1,2: //
                | 3: whd in match (exec_expr ????); whd in match (exec_expr ??? (Expr ??));
                     elim (Hcond_equiv ge en m) * #Hexec_cond_sim #_ #Htype_cond_eq
                     cases Hexec_cond_sim
                     [ 2: * #error #Herror >Herror normalize @I
                     | 1: cases (exec_expr ge en m cond)
                          [ 2: #error #_ normalize @I
                          | 1: * #cond_val #cond_trace #Hcond_sim 
                               >(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))                               
                               normalize nodelta
                               >Htype_cond_eq
                               cases (exec_bool_of_val cond_val (typeof cond1)) *
                               [ 3,4: normalize //
                               | 1,2: normalize in match (m_bind ?????);
                                      normalize in match (m_bind ?????);
                                      -Hexec_cond_sim -Hcond_sim -cond_val
                                      [ 1: (* true branch taken *)
                                           cases (exec_expr ge en m iftrue) in Hsmaller_true;
                                           [ 2: #error #_ @I
                                           | 1: * #val_true_branch #trace_true_branch #Hsmaller
                                                #val_true_branch #Hval_true_branch lapply Hsmaller -Hsmaller                                                
                                                cases (exec_expr ge en m iftrue1)
                                                [ 2: #error normalize in ⊢ (% → ?); #Hsmaller 
                                                     @(False_ind … (Hsmaller val_true_branch Hval_true_branch))
                                                | 1: * #val_true1_branch #trace_true1_branch #Hsmaller normalize nodelta
                                                     elim (Hsmaller val_true_branch Hval_true_branch)
                                                     #val_true1_int * * * #val_true1_branch #Hval_cast_eq #Htrace_eq #Hle
                                                     %{val_true1_int} try @conj try @conj try @conj //
                                           ] ]
                                     | 2: (* false branch taken. Same proof as above, different arguments ... *) 
                                           cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg)
                                           [ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq
                                                destruct (Htype_eq) @conj @refl ] * #Hsz_eq #Hsg_eq destruct
                                           cases (exec_expr ge en m iffalse) in Hsmaller_false;
                                           [ 2: #error #_ @I
                                           | 1: destruct * #val_false_branch #trace_false_branch #Hsmaller
                                                #val_false_branch #Hval_false_branch lapply Hsmaller -Hsmaller
                                                cases (exec_expr ge en m iffalse1)
                                                [ 2: #error normalize in ⊢ (% → ?); #Hsmaller 
                                                     @(False_ind … (Hsmaller val_false_branch Hval_false_branch))
                                                | 1: * #val_false1_branch #trace_false1_branch #Hsmaller normalize nodelta
                                                     elim (Hsmaller val_false_branch Hval_false_branch)
                                                     #val_false1_int * * * #val_false1_branch #Hval_cast_eq #Htrace_eq #Hle
                                                     %{val_false1_int} try @conj try @conj try @conj //
                                           ] ]
      ] ] ] ] ] ] ]
| 38,39,40: destruct
   elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq
   elim (Htrue_equiv ge en m) * #Hsim_expr_true #Hsim_vlalue_true #Htype_true_eq
   elim (Hfalse_equiv ge en m) * #Hsim_expr_false #Hsim_vlalue_false #Htype_false_eq
   %1 try @refl
   [ 1,3,5: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
            cases (exec_expr ge en m cond) in Hsim_expr_cond;
            [ 2,4,6: #error #_ @SimFailNicely
            | 1,3,5: * #cond_val #cond_trace normalize nodelta 
                cases (exec_expr ge en m cond1)
                [ 2,4,6: #error *
                         [ 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) 
                                  #Habsurd destruct
                         | *: * #error #Habsurd destruct ]
                | 1,3,5: * #cond_val1 #cond_trace1 *
                         [ 2,4,6: * #error #Habsurd destruct
                         | 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))
                             #Hcond_eq normalize nodelta destruct (Hcond_eq)
                             >Htype_cond_eq cases (exec_bool_of_val cond_val (typeof cond1))
                             [ 2,4,6: #error @SimFailNicely
                             | 1,3,5: * (* true branch *)
                                [ 1,3,5:
                                 normalize in match (m_bind ?????);
                                 normalize in match (m_bind ?????);
                                 cases Hsim_expr_true
                                 [ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFailNicely
                                 | 1,3,5: cases (exec_expr ge en m iftrue)
                                     [ 2,4,6: #error #_ normalize nodelta @SimFailNicely
                                     | 1,3,5: * #val_true #trace_true normalize nodelta #Hsim
                                              >(Hsim 〈val_true,trace_true〉 (refl ? (OK ? 〈val_true,trace_true〉)))
                                              normalize nodelta @SimOk #a #H @H
                                     ]
                                 ]
                             | 2,4,6:
                                 normalize in match (m_bind ?????);
                                 normalize in match (m_bind ?????);                             
                                 cases Hsim_expr_false
                                 [ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFailNicely
                                 | 1,3,5: cases (exec_expr ge en m iffalse)
                                     [ 2,4,6: #error #_ normalize nodelta @SimFailNicely
                                     | 1,3,5: * #val_false #trace_false normalize nodelta #Hsim
                                              >(Hsim 〈val_false,trace_false〉 (refl ? (OK ? 〈val_false,trace_false〉)))
                                              normalize nodelta @SimOk #a #H @H
                                     ]
                                 ]
                               ]
                             ]
                          ]
                ]
            ]
   | 2,4,6: @SimFailNicely
   ]
| 41,42: destruct
    elim (Hlhs_equiv ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
    elim (Hrhs_equiv ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
    %1 try @refl
    [ 1,3: whd in match (exec_expr ??? (Expr ??));
           whd in match (exec_expr ??? (Expr ??));
           cases Hsim_expr_lhs
           [ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFailNicely
           | 1,3: cases (exec_expr ge en m lhs) 
              [ 2,4: #error #_ @SimFailNicely
              | 1,3: * #lhs_val #lhs_trace #Hsim normalize nodelta
                     >(Hsim 〈lhs_val,lhs_trace〉 (refl ? (OK ? 〈lhs_val,lhs_trace〉)))
                     normalize nodelta >Htype_eq_lhs
                     cases (exec_bool_of_val lhs_val (typeof lhs1))
                       [ 2,4: #error normalize @SimFailNicely
                     | 1,3: * 
                         whd in match (m_bind ?????);
                         whd in match (m_bind ?????);                    
                         [ 2,3: (* lhs evaluates to true *)
                            @SimOk #a #H @H
                         | 1,4: cases Hsim_expr_rhs
                            [ 2,4: * #error #Hexec >Hexec @SimFailNicely
                            | 1,3: cases (exec_expr ge en m rhs) 
                                [ 2,4: #error #_ @SimFailNicely
                                | 1,3: * #rhs_val #rhs_trace -Hsim #Hsim
                                       >(Hsim 〈rhs_val,rhs_trace〉 (refl ? (OK ? 〈rhs_val,rhs_trace〉)))
                                       normalize nodelta >Htype_eq_rhs
                                       @SimOk #a #H @H
                                ]
                            ]
                         ]
                      ]
              ]
          ]
   | 2,4:  @SimFailNicely
   ]
| 43: destruct
      cases (type_eq_dec ty (Tint target_sz target_sg))
      [ 1: #Htype_eq >Htype_eq >type_eq_identity
           @(Inv_coerce_ok ??????? target_sz target_sg)
           [ 1,2: //
           | 3: @smaller_integer_val_identity ]
      | 2: #Hneq >(type_neq_not_identity … Hneq)
           %1 // @SimOk #a #H @H
      ]
| 44: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
      %1 try @refl
      [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
           whd in match (exec_lvalue ????) in Hsim_lvalue;
           whd in match (exec_lvalue' ?????);
           whd in match (exec_lvalue' ?????);
           >Htype_eq
           cases (typeof rec_expr1) normalize nodelta
           [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
           [ 1,2,3,4,5,8,9: @SimFailNicely
           | 6,7: cases Hsim_lvalue
              [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely
              | 1,3: cases (exec_lvalue ge en m rec_expr)
                 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFailNicely
                 | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a)))
                         whd in match (m_bind ?????);
                         @SimOk #a #H @H
                 ]
              ]
           ]
      | 2: whd in match (exec_lvalue ??? (Expr ??)); whd in match (exec_lvalue ??? (Expr ??));
           >Htype_eq
           cases (typeof rec_expr1) normalize nodelta
           [ 2: #sz #sg | 3: #fl | 4: #ty | 5: #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #ty ]
           [ 1,2,3,4,5,8,9: @SimFailNicely
           | 6,7: cases Hsim_lvalue
              [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely
              | 1,3: cases (exec_lvalue ge en m rec_expr)
                 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFailNicely
                 | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a)))
                         whd in match (m_bind ?????);
                         @SimOk #a #H @H
                 ]
              ]
           ]
     ]
| 45: destruct 
   inversion (Hinv ge en m)
   [ 2: #src_sz #src_sg #Htypeof_e1 #Htypeof_e2 #Hsmaller #Hdesired_eq #_
         @(Inv_coerce_ok ??????? src_sz src_sg)
         [ 1: >Htypeof_e1 //
         | 2: >Htypeof_e2 //
         | 3: whd in match (exec_expr ??? (Expr ??));
              whd in match (exec_expr ??? (Expr ??));
              cases (exec_expr ge en m e1) in Hsmaller;
              [ 2: #error normalize //
              | 1: * #val1 #trace1 #Hsmaller #val1_int #Hval1_eq                   
                   cases (exec_expr ge en m e2) in Hsmaller;
                   [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … (Habsurd val1_int Hval1_eq))
                   | 1: * #val2 #trace #Hsmaller elim (Hsmaller val1_int Hval1_eq)
                        #val2_int * * * #Hval2_eq #Hcast #Htrace #Hle normalize nodelta
                        %{val2_int} try @conj try @conj try @conj //
                   ]
               ]
         ]
   | 1: #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hdesired_typ #_
        >Hresult %1 try @refl
        [ 1: >Htype_eq //
        | 2: whd in match (exec_expr ??? (Expr ??));
             whd in match (exec_expr ??? (Expr ??));
             cases Hsim_expr
             [ 2: * #error #Hexec_error >Hexec_error @SimFailNicely
             | 1: cases (exec_expr ge en m e1)
                  [ 2: #error #_ @SimFailNicely
                  | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec
                        @SimOk #a #H @H
                  ]
             ]
        | 3: @SimFailNicely
        ]
   ]
| 46: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
      %1 try @refl
      [ 1: whd in match (exec_expr ??? (Expr ??));
           whd in match (exec_expr ??? (Expr ??));
           cases Hsim_expr
           [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
           | 1: cases (exec_expr ge en m e1)
                [ 2: #error #_ @SimFailNicely
                | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hsim2 >Hsim2 @SimOk #a #H @H ]
           ]
      | 2: @SimFail /2 by ex_intro/ ]
(* simplify_inside cases. Amounts to propagate a simulation result, except for the /cast/ case which actually calls
 * simplify_expr *)      
| 47, 48, 49: (* trivial const_int, const_float and var cases *)
  try @conj try @conj try @refl
  @SimOk #a #H @H
| 50: (* Deref case *) destruct
  elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
  try @conj try @conj
  [ 1: 
    whd in match (exec_expr ??? (Expr ??));
    whd in match (exec_expr ??? (Expr ??));
    whd in match (exec_lvalue' ?????);
    whd in match (exec_lvalue' ?????);  
  | 2:
    whd in match (exec_lvalue ??? (Expr ??));
    whd in match (exec_lvalue ??? (Expr ??));
  ]
  [ 1,2:  
    cases Hsim_expr
    [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    | 1,3: cases (exec_expr ge en m e1)
         [ 2,4: #error #_ @SimFailNicely
         | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ]
  | 3: // ]
| 51: (* Addrof *) destruct
  elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
  try @conj try @conj   
  [ 1: 
    whd in match (exec_expr ??? (Expr ??));
    whd in match (exec_expr ??? (Expr ??));
    cases Hsim_lvalue
    [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely
    | 1: cases (exec_lvalue ge en m e1)
       [ 2: #error #_ @SimFailNicely
       | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ]
  | 2: @SimFailNicely
  | 3: // ]
| 52: (* Unop *) destruct
  elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
  try @conj try @conj
  [ 1: 
    whd in match (exec_expr ??? (Expr ??));
    whd in match (exec_expr ??? (Expr ??));
    cases Hsim_expr
    [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    | 1: cases (exec_expr ge en m e1)
         [ 2: #error #_ @SimFailNicely
         | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk
              >Htype_eq #a #H @H ] ]
  | 2: @SimFailNicely              
  | 3: // ]
| 53: (* Binop *) destruct
  elim (Hequiv_lhs ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
  elim (Hequiv_rhs ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
  try @conj try @conj
  [ 1: 
    whd in match (exec_expr ??? (Expr ??));
    whd in match (exec_expr ??? (Expr ??));
    cases Hsim_expr_lhs
    [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
    | 1: cases (exec_expr ge en m lhs)
         [ 2: #error #_ @SimFailNicely
         | 1: #lhs_value #Hsim_lhs cases Hsim_expr_rhs
              [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
              | 1: cases (exec_expr ge en m rhs)
                   [ 2: #error #_ @SimFailNicely
                   | 1: #rhs_value #Hsim_rhs 
                        lapply (Hsim_lhs lhs_value (refl ? (OK ? lhs_value)))
                        lapply (Hsim_rhs rhs_value (refl ? (OK ? rhs_value)))
                        #Hrhs >Hrhs #Hlhs >Hlhs >Htype_eq_rhs >Htype_eq_lhs
                        @SimOk #a #H @H
                   ]
              ]
         ]
    ]
  | 2: @SimFailNicely
  | 3: //
  ]
| 54: (* Cast, fallback case *)
  try @conj try @conj try @refl
  @SimOk #a #H @H
| 55: (* Cast, success case *) destruct
  inversion (Htrans_inv ge en m)
  [ 1: (* contradiction *)
       #result_flag #Hresult_flag #Htype_eq #Hsim_epr #Hsim_lvalue #Hresult_flag_true
       <Hresult_flag_true in Hresult_flag; #Habsurd destruct
  | 2: #src_sz #src_sg #Hsrc_type_eq #Htarget_type_eq #Hsmaller #_ #_
       try @conj try @conj try @conj
       [ 1: whd in match (exec_expr ??? (Expr ??));
            cases (exec_expr ge en m castee) in Hsmaller;
            [ 2: #error #_ @SimFailNicely
            | 1: * #val #trace normalize nodelta >Hsrc_type_eq
                 lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m)
                 cases (exec_cast m val ??)
                 [ 2: #error #_ #_ @SimFailNicely
                 | 1: #result #Hinversion elim (Hinversion result (refl ??)) 
                      #val_int * #Hval_eq #Hcast
                      cases (exec_expr ge en m castee1)
                      [ 2: #error #Habsurd normalize in Habsurd; @(False_ind … (Habsurd val_int Hval_eq))
                      | 1: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq)
                           #val1_int * * * #Hval1_int #Hval18int #Htrace #Hle
                           @SimOk destruct normalize // ]
                      ]
             ]
      | 2: @SimFailNicely
      | 3: >Htarget_type_eq //
      ]
  ]
| 56: (* Cast, "failure" case *) destruct
  inversion (Htrans_inv ge en m)
  [ 2: (* contradiction *)
       #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller #Habsurd
       lapply (jmeq_to_eq ??? Habsurd) -Habsurd #Herror destruct
  | 1: #result_flag #Hresult_flag #Htype_eq #Hsim_expr #Hsim_lvalue #_ #_
       try @conj try @conj try @conj
       [ 1: whd in match (exec_expr ????);
            whd in match (exec_expr ??? (Expr ??));
            cases Hsim_expr
            [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
            | 1: cases (exec_expr ??? castee)
                 [ 2: #error #_ @SimFailNicely
                 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec_ok >Hexec_ok
                       @SimOk >Htype_eq #a #H @H ]
            ]
       | 2: @SimFailNicely
       | 3: //
       ]
  ]
| 57,58,59,60,61,62,63,64,68:       
  try @conj try @conj try @refl
  @SimOk #a #H @H
| 65: destruct
  elim (Hequiv_cond ge en m) * #Hsim_exec_cond #Hsim_lvalue_cond #Htype_eq_cond
  elim (Hequiv_iftrue ge en m) * #Hsim_exec_true #Hsim_lvalue_true #Htype_eq_true
  elim (Hequiv_iffalse ge en m) * #Hsim_exec_false #Hsim_lvalue_false #Htype_eq_false
  try @conj try @conj
  [ 1: whd in match (exec_expr ??? (Expr ??));
       whd in match (exec_expr ??? (Expr ??));
       cases Hsim_exec_cond
       [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
       | 1: cases (exec_expr ??? cond)
            [ 2: #error #_ @SimFailNicely
            | 1: * #condb #condtrace #Hcond_sim lapply (Hcond_sim 〈condb, condtrace〉 (refl ? (OK ? 〈condb, condtrace〉)))
                 #Hcond_ok >Hcond_ok >Htype_eq_cond
                 normalize nodelta
                 cases (exec_bool_of_val condb (typeof cond1))
                 [ 2: #error @SimFailNicely
                 | 1: * whd in match (m_bind ?????); whd in match (m_bind ?????);
                      normalize nodelta
                      [ 1: (* true branch taken *)
                           cases Hsim_exec_true
                           [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
                           | 1: cases (exec_expr ??? iftrue)
                                [ 2: #error #_ @SimFailNicely
                                | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
                                     @SimOk #a #H @H
                                ]
                           ]
                      | 2: (* false branch taken *)
                           cases Hsim_exec_false
                           [ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
                           | 1: cases (exec_expr ??? iffalse)
                                [ 2: #error #_ @SimFailNicely
                                | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
                                     @SimOk #a #H @H
                                ]
                           ]
                      ]
                ]
           ]
      ]
  | 2: @SimFailNicely
  | 3: //
  ]
| 66,67: destruct
  elim (Hequiv_lhs ge en m) * #Hsim_exec_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
  elim (Hequiv_rhs ge en m) * #Hsim_exec_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
  try @conj try @conj
  whd in match (exec_expr ??? (Expr ??));
  whd in match (exec_expr ??? (Expr ??));
  [ 1,4: cases Hsim_exec_lhs 
       [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely
       | 1,3: cases (exec_expr ??? lhs)
            [ 2,4: #error #_ @SimFailNicely
            | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hlhs >Hlhs >Htype_eq_lhs
                   normalize nodelta elim a #lhs_val #lhs_trace
                   cases (exec_bool_of_val lhs_val (typeof lhs1))
                   [ 2,4: #error @SimFailNicely
                   | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????);
                        [ 2,3: @SimOk //
                        | 1,4: cases Hsim_exec_rhs
                            [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely
                            | 1,3: cases (exec_expr ??? rhs)
                               [ 2,4: #error #_ @SimFailNicely
                               | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrhs >Hrhs >Htype_eq_rhs
                                    @SimOk #a #H @H
                               ]
                            ]
                        ]
                   ]
             ]
        ]
  | 2,5: @SimFailNicely
  | 3,6: //
  ]
| 69: (* record field *) destruct
   elim (Hequiv_rec ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
   try @conj try @conj   
   whd in match (exec_expr ??? (Expr ??));
   whd in match (exec_expr ??? (Expr ??)); 
   whd in match (exec_lvalue' ??? (Efield rec_expr f) ty);
   whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty);  
   [ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta
       [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
       | 7: #id #fl | 8: #id #fl | 9: #id ]
       try (@SimFailNicely)
       cases Hsim_lvalue
       [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely
       | 1,3: cases (exec_lvalue ge en m rec_expr)
            [ 2,4: #error #_ @SimFailNicely
            | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec
                   @SimOk #a #H @H ]
       ]
   | 2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *)
       >Htype_eq cases (typeof rec_expr1) normalize nodelta
       [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
       | 7: #id #fl | 8: #id #fl | 9: #id ]
       try (@SimFailNicely)
       cases Hsim_lvalue
       [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely
       | 1,3: cases (exec_lvalue ge en m rec_expr)
            [ 2,4: #error #_ @SimFailNicely
            | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec
                   @SimOk #a #H @H ]
       ]
   | 3: // ]
| 70: (* cost label *) destruct
   elim (Hequiv ge en m) *  #Hsim_expr #Hsim_lvalue #Htype_eq
   try @conj try @conj
   whd in match (exec_expr ??? (Expr ??));
   whd in match (exec_expr ??? (Expr ??));
   [ 1:
     cases Hsim_expr
     [ 2: * #error #Hexec >Hexec @SimFailNicely
     | 1: cases (exec_expr ??? e1)
          [ 2: #error #_ @SimFailNicely
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
               @SimOk #a #H @H ]
     ]
   | 2: @SimFail /2 by ex_intro/
   | 3: //
   ]
] qed.

(* Propagate cast simplification through statements and programs. *)

definition simplify_e ≝ λe. pi1 … (simplify_inside e).

let rec simplify_statement (s:statement) : statement ≝
match s with
[ Sskip ⇒ Sskip
| Sassign e1 e2 ⇒ Sassign (simplify_e e1) (simplify_e e2)
| Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es)
| Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2)
| Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *)
| Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
| Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
| Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *)
| Sbreak ⇒ Sbreak
| Scontinue ⇒ Scontinue
| Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo)
| Sswitch e ls ⇒ Sswitch (simplify_e e) (simplify_ls ls)
| Slabel l s1 ⇒ Slabel l (simplify_statement s1)
| Sgoto l ⇒ Sgoto l
| Scost l s1 ⇒ Scost l (simplify_statement s1)
]
and simplify_ls ls ≝
match ls with
[ LSdefault s ⇒ LSdefault (simplify_statement s)
| LScase sz i s ls' ⇒ LScase sz i (simplify_statement s) (simplify_ls ls')
].

definition simplify_function : function → function ≝
λf. mk_function (fn_return f) (fn_params f) (fn_vars f) (simplify_statement (fn_body f)).

definition simplify_fundef : clight_fundef → clight_fundef ≝
λf. match f with
  [ CL_Internal f ⇒ CL_Internal (simplify_function f)
  | _ ⇒ f
  ].

definition simplify_program : clight_program → clight_program ≝
λp. transform_program … p (λ_.simplify_fundef).

(* Simulation on statement continuations. Stolen from labelSimulation and adapted to our setting. *)
inductive cont_cast : cont → cont → Prop ≝
| cc_stop : cont_cast Kstop Kstop
| cc_seq : ∀s,k,k'. cont_cast k k' → cont_cast (Kseq s k) (Kseq (simplify_statement s) k')
| cc_while : ∀e,s,k,k'.
    cont_cast k k' →
    cont_cast (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k')
| cc_dowhile : ∀e,s,k,k'.
    cont_cast k k' →
    cont_cast (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k')
| cc_for1 : ∀e,s1,s2,k,k'.
    cont_cast k k' →
    cont_cast (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (simplify_e e) (simplify_statement s1) (simplify_statement s2)) k')
| cc_for2 : ∀e,s1,s2,k,k'. 
    cont_cast k k' →
    cont_cast (Kfor2 e s1 s2 k) (Kfor2 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k')
| cc_for3 : ∀e,s1,s2,k,k'. 
    cont_cast k k' → 
    cont_cast (Kfor3 e s1 s2 k) (Kfor3 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k')
| cc_switch : ∀k,k'. 
    cont_cast k k' → cont_cast (Kswitch k) (Kswitch k')
| cc_call : ∀r,f,en,k,k'. 
    cont_cast k k' → 
    cont_cast (Kcall r f en k) (Kcall r (simplify_function f) en k').

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

inductive state_cast : state → state → Prop ≝
| swc_state : ∀f,s,k,k',e,m. 
  cont_cast k k' →
  state_cast (State f s k e m) (State (simplify_function f) (simplify_statement s ) k' e m)
| swc_callstate : ∀fd,args,k,k',m. 
  cont_cast k k' → state_cast (Callstate fd args k m) (Callstate (simplify_fundef fd) args k' m)
| swc_returnstate : ∀res,k,k',m. 
  cont_cast k k' → state_cast (Returnstate res k m) (Returnstate res k' m)
| swc_finalstate : ∀r. 
  state_cast (Finalstate r) (Finalstate r)
.

record related_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)
}.

(* The return type of any function is invariant under cast simplification *)
lemma fn_return_simplify : ∀f. fn_return (simplify_function f) = fn_return f.
// qed.


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).
 
lemma simulation_transitive : ∀A,r0,r1,r2. res_sim A r0 r1 → res_sim A r1 r2 → res_sim A r0 r2.
#A #r0 #r1 #r2 *
[ 2: * #error #H >H #_ @SimFail /2 by ex_intro/
| 1: cases r0
     [ 2: #error #_ #_ @SimFail /2 by ex_intro/
     | 1: #elt #Hsim lapply (Hsim elt (refl ? (OK ? elt))) #H >H // ]
] qed.

lemma sim_related_globals : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' → 
  (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧
  (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).
#ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined
[ 1: #sz #ty #i @SimOk #a normalize //
| 2: #ty #f @SimOk #a normalize //
| 3: * 
    [ 1: #sz #i | 2: #fl | 3: #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 #Hsim_lvalue try //
    whd in match (Plvalue ???);
    whd in match (exec_expr ????);
    whd in match (exec_expr ????);
    cases Hsim_lvalue
    [ 2,4,6: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
    | *: cases (exec_lvalue' ge en m ? ty)
         [ 2,4,6: #error #_ @SimFail /2 by ex_intro/
         | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite
              @SimOk // ]
    ]
| 4: #v #ty whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
     cases (lookup SymbolTag block en v) normalize nodelta
     [ 2: #block @SimOk //
     | 1: elim Hrelated #Hsymbol #_ #_ >(Hsymbol v) @SimOk //
     ]
| 5: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
     cases Hsim_expr
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
                @SimOk // ]
     ]
| 6: #ty #ed #ty' #Hsim_lvalue 
     whd in match (exec_expr ????); whd in match (exec_expr ????);
     whd in match (exec_lvalue ????); whd in match (exec_lvalue ????);
     cases Hsim_lvalue
     [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
     | 1: cases (exec_lvalue' ge en m ed ty')
         [ 2: #error #_ @SimFail /2 by ex_intro/
         | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite
              @SimOk // ]
    ]
| 7: #ty #op #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     cases Hsim
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
               @SimOk // ]
     ]
| 8: #ty #op #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     cases Hsim1
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e1)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
               cases Hsim2
               [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
               | 1: cases (exec_expr ge en m e2)
                    [ 2: #error #_ @SimFail /2 by ex_intro/
                    | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
                         @SimOk // ]
               ]
          ]
     ]
| 9: #ty #cast_ty #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     cases Hsim
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
               @SimOk // ]
     ] (* mergeable with 7 modulo intros *)
| 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     cases Hsim1
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e1)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta
               cases (exec_bool_of_val (\fst a) (typeof e1))
               [ 2: #error @SimFail /2 by ex_intro/
               | 1: *
                    [ 1: (* true branch *) cases Hsim2
                    | 2: (* false branch *) cases Hsim3 ]
                    [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
                    | 1: cases (exec_expr ge en m e2) | 3: cases (exec_expr ge en m e3) ]
                    [ 2,4: #error #_ @SimFail /2 by ex_intro/ 
                    | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ]
              ]
          ]
     ]
| 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     cases Hsim1
     [ 2,4: * #error #Hfail >Hfail @SimFailNicely
     | 1,3: cases (exec_expr ge en m e1)
          [ 2,4: #error #_ @SimFailNicely
          | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta
                 cases (exec_bool_of_val ??)
                 [ 2,4: #erro @SimFailNicely
                 | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); 
                        [ 2,3: @SimOk //
                        | 1,4: cases Hsim2
                               [ 2,4: * #error #Hfail >Hfail normalize nodelta @SimFail /2 by ex_intro/
                               | 1,3: cases (exec_expr ge en m e2)
                                      [ 2,4: #error #_ @SimFail /2 by ex_intro/
                                      | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
                                           @SimOk // ]
                               ]
                        ]
                ]
          ]
     ]
| 13: #ty #sizeof_ty @SimOk normalize //
| 14: #ty #e #ty' #field #Hsim_lvalue 
      whd in match (exec_lvalue' ? en m (Efield ??) ty); 
      whd in match (exec_lvalue' ge' en m (Efield ??) ty);
      normalize in match (typeof (Expr ??));
      cases ty' in Hsim_lvalue; normalize nodelta
      [ 2: #sz #sg | 3: #fsz | 4: #ptr_ty | 5: #array_ty #array_sz | 6: #domain #codomain
      | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #id ]
      #Hsim_lvalue
      try (@SimFail /2 by ex_intro/)
      normalize in match (exec_lvalue ge en m ?);
      normalize in match (exec_lvalue ge' en m ?);
      cases Hsim_lvalue
      [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
      | 1,3: cases (exec_lvalue' ge en m e ?)
             [ 2,4: #error #_ @SimFail /2 by ex_intro/
             | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
                    @SimOk /2 by ex_intro/ ]
      ]
| 15: #ty #lab #e #Hsim 
      whd in match (exec_expr ??? (Expr ??));
      whd in match (exec_expr ??? (Expr ??));
      cases Hsim
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
               @SimOk // ]
     ] (* cf case 7, again *)
| 16: *
      [ 1: #sz #i | 2: #fl | 3: #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 match (is_not_lvalue ?);
      [ 3,4,13: #Habsurd @(False_ind … Habsurd) ] #_
      @SimFailNicely
] qed.

lemma related_globals_expr_simulation : ∀ge,ge',en,m. 
  related_globals ? simplify_fundef ge ge' →
  ∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧
      typeof e = typeof (simplify_e e).
#ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
cases e #ed #ty cases ed
[ 1: #sz #i | 2: #fl | 3: #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 ]
elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m)
* * try //
cases (exec_expr ge en m (Expr ??))
try (#error #_ #_ #_ @SimFailNicely)
* #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq
try @(simulation_transitive ???? Hsim_expr (proj1 ?? (sim_related_globals ge ge' en m Hrelated) ?))
qed.

lemma related_globals_lvalue_simulation : ∀ge,ge',en,m. 
  related_globals ? simplify_fundef ge ge' →
  ∀e. res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧
      typeof e = typeof (simplify_e e).
#ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
cases e #ed #ty cases ed
[ 1: #sz #i | 2: #fl | 3: #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 ]
elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m)
* * try //
cases (exec_lvalue ge en m (Expr ??))
try (#error #_ #_ #_ @SimFailNicely)
* #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq
(* Having to distinguish between exec_lvalue' and exec_lvalue is /ugly/. *)
cases e' in Hsim_lvalue ⊢ %; #ed' #ty' whd in match (exec_lvalue ????); whd in match (exec_lvalue ????);
lapply (proj2 ?? (sim_related_globals ge ge' en m Hrelated) ed' ty') #Hsim_lvalue2 #Hsim_lvalue1
try @(simulation_transitive ???? Hsim_lvalue1 Hsim_lvalue2)
qed.

lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
related_globals ? simplify_fundef ge ge' →
∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)).
#ge #ge' #en #m #Hrelated #args
elim args
[ 1: /3/
| 2: #hd #tl #Hind normalize
     elim (related_globals_expr_simulation ge ge' en m Hrelated hd)
     *
     [ 2: * #error #Hfail >Hfail #_ @SimFail /2 by refl, ex_intro/
     | 1: cases (exec_expr ge en m hd)
          [ 2: #error #_ #_ @SimFail /2 by refl, ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq
               cases Hind normalize
               [ 2: * #error #Hfail >Hfail @SimFail /2 by refl, ex_intro/
               | 1: cases (exec_exprlist ??? tl)
                    [ 2: #error #_ @SimFail /2 by refl, ex_intro/
                    | 1: * #values #trace #Hsim lapply (Hsim 〈values, trace〉 (refl ? (OK ? 〈values, trace〉)))
                         #Heq >Heq @SimOk // ]
               ]
          ]
     ]
] qed.

lemma simplify_type_of_fundef_eq : ∀clfd. (type_of_fundef (simplify_fundef clfd)) = (type_of_fundef clfd).
* // qed.

lemma simplify_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. typeof (simplify_e func) = typeof func.
#ge #en #m #func whd in match (simplify_e func); elim (simplify_inside func)
#func' #H lapply (H ge en m) * * #_ #_ //
qed.

lemma simplify_fun_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. fun_typeof (simplify_e func) = fun_typeof func.
#ge #en #m #func whd in match (simplify_e func); whd in match (fun_typeof ?) in ⊢ (??%%);
>simplify_typeof_eq whd in match (simplify_e func); // qed.

lemma simplify_is_not_skip: ∀s.s ≠ Sskip → ∃pf. is_Sskip (simplify_statement s) = inr … pf.
*
[ 1: * #Habsurd elim (Habsurd (refl ? Sskip))
| *: #a try #b try #c try #d try #e
     whd in match (simplify_statement ?);
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/
] qed.

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

lemma simplify_ls_commute : ∀l. (simplify_statement (seq_of_labeled_statement l)) = (seq_of_labeled_statement (simplify_ls l)).
#l @(labeled_statements_ind … l)
[ 1: #default_statement //
| 2: #sz #i #s #tl #Hind
     whd in match (seq_of_labeled_statement ?) in ⊢ (??%?);
     whd in match (simplify_ls ?) in ⊢ (???%);
     whd in match (seq_of_labeled_statement ?) in ⊢ (???%);
     whd in match (simplify_statement ?) in ⊢ (??%?);
     >Hind //
] qed.

lemma select_switch_commute : ∀sz,i,l.
 select_switch sz i (simplify_ls l) = simplify_ls (select_switch sz i l).
#sz #i #l @(labeled_statements_ind … l)
[ 1: #default_statement //
| 2: #sz' #i' #s #tl #Hind
     whd in match (simplify_ls ?) in ⊢ (??%?);
     whd in match (select_switch ???) in ⊢ (??%%);
     cases (sz_eq_dec sz sz')
     [ 1: #Hsz_eq destruct >intsize_eq_elim_true >intsize_eq_elim_true
           cases (eq_bv (bitsize_of_intsize sz') i' i) normalize nodelta
           whd in match (simplify_ls ?) in ⊢ (???%);
           [ 1: // | 2: @Hind ]
     | 2: #Hneq >(intsize_eq_elim_false ? sz sz' ???? Hneq) >(intsize_eq_elim_false ? sz sz' ???? Hneq)
          @Hind
     ]
] qed.

lemma elim_IH_aux :
  ∀lab. ∀s:statement.∀k,k'. cont_cast k k' →
  ∀Hind:(∀k:cont.∀k':cont.
          cont_cast k k' → 
          match find_label lab s k with 
          [ None ⇒ find_label lab (simplify_statement s) k'=None (statement×cont)
          | Some (r:(statement×cont))⇒
            let 〈s',ks〉 ≝r in 
            ∃ks':cont. find_label lab (simplify_statement s) k' = Some (statement×cont) 〈simplify_statement s',ks'〉
                        ∧ cont_cast ks ks']).
  (find_label lab s k = None ? ∧ find_label lab (simplify_statement s) k' = None ?) ∨
  (∃st,kst,kst'. find_label lab s k = Some ? 〈st,kst〉 ∧ find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement st,kst'〉 ∧ cont_cast kst kst').
#lab #s #k #k' #Hcont_cast #Hind
lapply (Hind k k' Hcont_cast)
cases (find_label lab s k)
[ 1: normalize nodelta #Heq >Heq /3/
| 2: * #st #kst normalize nodelta * #kst' * #Heq #Hcont_cast' >Heq %2
     %{st} %{kst} %{kst'} @conj try @conj //
] qed.


lemma cast_find_label : ∀lab,s,k,k'.
  cont_cast k k' →
  match find_label lab s k with
  [ Some r ⇒
    let 〈s',ks〉 ≝ r in
    ∃ks'. find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement s', ks'〉
    ∧ cont_cast ks ks'
  | None ⇒
    find_label lab (simplify_statement s) k' = None ?
  ].
#lab #s @(statement_ind2 ? (λls.
    ∀k:cont
    .∀k':cont
     .cont_cast k k'
      →match find_label_ls lab ls k with 
       [None⇒ 
        find_label_ls lab (simplify_ls ls) k' = None ?
       |Some r ⇒
        let 〈s',ks〉 ≝r in 
        ∃ks':cont
        .find_label_ls lab (simplify_ls ls) k'
         =Some (statement×cont) 〈simplify_statement s',ks'〉
         ∧cont_cast ks ks']
) … s)
[ 1: #k #k' #Hcont_cast
     whd in match (find_label ? Sskip ?); normalize nodelta @refl
| 2: #e1 #e2 #k #k' #Hcont_cast
     whd in match (find_label ? (Sassign e1 e2) ?); normalize nodelta @refl
| 3: #e0 #e #args #k #k' #Hcont_cast
     whd in match (find_label ? (Scall e0 e args) ?); normalize nodelta @refl
| 4: #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast
     whd in match (find_label ? (Ssequence s1 s2) ?); 
     whd in match (find_label ? (simplify_statement (Ssequence s1 s2)) ?); 
     elim (elim_IH_aux lab s1 (Kseq s2 k) (Kseq (simplify_statement s2) k') ? Hind_s1)
     [ 3: try ( @cc_seq // )
     | 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/ 
     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
          elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2)
          [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast'
               normalize nodelta %{kst'} /2/
          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     ] ]  
| 5: #e #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     elim (elim_IH_aux lab s1 k k' Hcont_cast Hind_s1)
     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/
     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
          elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2)
          [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast'
               normalize nodelta %{kst'} /2/
          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     ] ]
| 6: #e #s #Hind_s #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     elim (elim_IH_aux lab s (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s)
     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/
     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     | 3: @cc_while // ]
| 7: #e #s #Hind_s #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     elim (elim_IH_aux lab s (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') ? Hind_s)
     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/
     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     | 3: @cc_dowhile // ]
| 8: #s1 #cond #s2 #s3 #Hind_s1 #Hind_s2 #Hind_s3 #k #k' #Hcont_cast     
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     elim (elim_IH_aux lab s1
               (Kseq (Sfor Sskip cond s2 s3) k)
               (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) (simplify_statement s3)) k')
               ? Hind_s1)
     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/
     | 3: @cc_for1 //
     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
          elim (elim_IH_aux lab s3
                    (Kfor2 cond s2 s3 k)
                    (Kfor2 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
                      ? Hind_s3)
          [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
                normalize nodelta %{kst'} /2/
          | 3: @cc_for2 //
          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
               elim (elim_IH_aux lab s2
                         (Kfor3 cond s2 s3 k)
                         (Kfor3 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
                           ? Hind_s2)
               [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
                    normalize nodelta %{kst'} /2/
               | 3: @cc_for3 //
               | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
    ] ] ]
| 9,10: #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta //
| 11: #e #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta //
| 12: #e #ls #Hind #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     (* We can't elim the Hind on a list of labeled statements. We must proceed more manually. *)
     lapply (Hind (Kswitch k) (Kswitch k') ?)
     [ 1: @cc_switch //
     | 2: cases (find_label_ls lab ls (Kswitch k)) normalize nodelta
          [ 1: //
          | 2: * #st #kst normalize nodelta // ] ]
| 13: #lab' #s0 #Hind #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     cases (ident_eq lab lab') normalize nodelta
     [ 1: #_ %{k'} /2/
     | 2: #_ elim (elim_IH_aux lab s0 k k' Hcont_cast Hind)
          [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
                normalize nodelta %{kst'} /2/
          | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] 
     ]
| 14: #l #k #k' #Hcont_cast //
| 15: #l #s0 #Hind #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     elim (elim_IH_aux lab s0 k k' Hcont_cast Hind)
     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/
     | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ]
| 16: #s0 #Hind #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     elim (elim_IH_aux lab s0 k k' Hcont_cast Hind)
     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/
     | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ]
| 17: #sz #i #s0 #t #Hind_s0 #Hind_ls #k #k' #Hcont_cast
     whd in match (simplify_ls ?);
     whd in match (find_label_ls ???);
     lapply Hind_ls
     @(labeled_statements_ind … t)
     [ 1: #default_case #Hind_ls whd in match (seq_of_labeled_statement ?);
          elim (elim_IH_aux lab s0 
                  (Kseq default_case k) 
                  (Kseq (simplify_statement default_case) k') ? Hind_s0)
         [ 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast'
              >Hrewrite >Hrewrite1         
              normalize nodelta whd in match (find_label_ls ???);
              >Hrewrite >Hrewrite1 normalize nodelta
              %{kst'} /2/
         | 3: @cc_seq //
         | 1: * #Hrewrite #Hrewrite1 >Hrewrite normalize nodelta
              lapply (Hind_ls k k' Hcont_cast)
              cases (find_label_ls lab (LSdefault default_case) k)
              [ 1: normalize nodelta #Heq1 
                   whd in match (simplify_ls ?);
                   whd in match (find_label_ls lab ??);
                   whd in match (seq_of_labeled_statement ?);
                   whd in match (find_label_ls lab ??);
                   >Hrewrite1 normalize nodelta @Heq1
              | 2: * #st #kst normalize nodelta #H
                   whd in match (find_label_ls lab ??);
                   whd in match (simplify_ls ?);
                   whd in match (seq_of_labeled_statement ?);
                   >Hrewrite1 normalize nodelta @H
              ]
         ]
     | 2: #sz' #i' #s' #tl' #Hind #A
     
          whd in match (seq_of_labeled_statement ?);
          elim (elim_IH_aux lab s0
                   (Kseq (Ssequence s' (seq_of_labeled_statement tl')) k)
                   (Kseq (simplify_statement (Ssequence s' (seq_of_labeled_statement tl'))) k')
                   ?
                   Hind_s0)
          [ 3: @cc_seq //
          | 1: * #Heq #Heq2 >Heq >Heq2 normalize nodelta
               lapply (A k k' Hcont_cast)
               cases (find_label_ls lab (LScase sz' i' s' tl') k) normalize nodelta
               [ 1: #H whd in match (find_label_ls ???);
                    <simplify_ls_commute
                    whd in match (seq_of_labeled_statement ?);
                    >Heq2 normalize nodelta
                    assumption
               | 2: * #st #kst normalize nodelta #H
                    whd in match (find_label_ls ???);
                    <simplify_ls_commute >Heq2 normalize nodelta @H
               ]
          | 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast'
               >Hrewrite normalize nodelta
               %{kst'} @conj try //
               whd in match (find_label_ls ???);
               <simplify_ls_commute >Hrewrite1 //
          ]
    ]
] qed.    
                   
lemma cast_find_label_fn : ∀lab,f,k,k',s,ks.
  cont_cast k k' →
  find_label lab (fn_body f) k = Some ? 〈s,ks〉 →
  ∃ks'. find_label lab (fn_body (simplify_function f)) k' = Some ? 〈simplify_statement s,ks'〉
        ∧ cont_cast ks ks'.
#lab * #rettype #args #vars #body #k #k' #s #ks #Hcont_cast #Hfind_lab
whd in match (simplify_function ?);
lapply (cast_find_label lab body ?? Hcont_cast)
>Hfind_lab normalize nodelta //
qed.

theorem cast_correction : ∀ge, ge'.
  related_globals ? simplify_fundef ge ge' →
  ∀s1, s1', tr, s2. 
  state_cast s1 s1' →
  exec_step ge s1 = Value … 〈tr,s2〉 →
  ∃s2'. exec_step ge' s1' = Value … 〈tr,s2'〉 ∧
        state_cast s2 s2'.
#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hs1_sim_s1' #Houtcome
inversion Hs1_sim_s1'
[ 1: (* regular state *) 
     #f #stm #k #k' #en #m #Hcont_cast
     lapply (related_globals_expr_simulation ge ge' en m Hrelated) #Hsim_related
     lapply (related_globals_lvalue_simulation ge ge' en m Hrelated) #Hsim_lvalue_related
     cases stm
     (* Perform the intros for the statements*)
     [ 1: | 2: #lhs #rhs | 3: #ret #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 ]
     [ 1: (* Skip *)
          #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1
          whd in match (exec_step ??); whd in match (exec_step ??);
          inversion Hcont_cast
          [ 1: (* Kstop *)
               #Hk #Hk' #_ >fn_return_simplify cases (fn_return f) normalize nodelta
               [ 1: >Heq_s1 in Hs1_sim_s1'; >Heq_s1' #Hsim inversion Hsim
                    [ 1: #f0 #s #k0 #k0' #e #m0 #Hcont_cast0 #Hstate_eq #Hstate_eq' #_
                         #Eq whd in match (ret ??) in Eq; destruct (Eq) 
                         %{(Returnstate Vundef Kstop (free_list m (blocks_of_env en)))} @conj
                         [ 1: // | 2: %3 %1 ]
                    | 2: #fd #args #k0 #k0' #m0 #Hcont_cast0 #Habsurd destruct (Habsurd)
                    | 3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd)
                    | 4: #r #Habsurd destruct (Habsurd) ]                    
               | 3,4,9: #irrelevant #Habsurd destruct
               | *: #irrelevant1 #irrelevant2 #Habsurd destruct ]
          | 2: (* Kseq stm' k' *)
               #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
               whd in match (ret ??) in Eq; destruct (Eq)
               %{(State (simplify_function f) (simplify_statement stm') k0' en m)} @conj
               [ 1: // | 2: %1 // ]               
          | 3: (* Kwhile *)
               #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
               whd in match (ret ??) in Eq; destruct (Eq)               
               %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} @conj
               [ 1: // | 2: %1 // ]
          | 4: (* Kdowhile *)
               #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
               elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq cases Hsim_cond
               [ 2: * #error #Hfail >Hfail in Eq; #Habsurd normalize in Habsurd; destruct
               | 1: cases (exec_expr ge en m cond) in Eq;
                    [ 2: #error whd in match (m_bind ?????) in ⊢ (% → ?); #Habsurd destruct
                    | 1: * #val #trace whd in match (m_bind ?????) in ⊢ (% → ?); <Htype_cond_eq
                         #Eq #Hsim_cond lapply (Hsim_cond 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) 
                         #Hrewrite_cond >Hrewrite_cond whd in match (m_bind ?????);
                         (* case analysis on the outcome of the conditional *)
                         cases (exec_bool_of_val val (typeof cond)) in Eq ⊢ %;
                         [ 2: (* evaluation of the conditional fails *)
                              #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
                         | 1: * whd in match (bindIO ??????); 
                                whd in match (bindIO ??????);
                                #Eq destruct (Eq)
                              [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)}
                                   @conj [ 1: // | 2: %1 // ]
                              | 2: %{(State (simplify_function f) Sskip k0' en m)}
                                   @conj [ 1: // | 2: %1 // ]
                              ]
                         ]
                    ]
               ]
           | 5,6,7:
                #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
                whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
                [ 1: %{(State (simplify_function f) 
                              (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) 
                               k0' en m)} @conj
                     [ 1: // | 2: %1 // ]
                | 2: %{(State (simplify_function f) 
                              (simplify_statement step) 
                              (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0')
                              en m)} @conj
                     [ 1: // | 2: %1 @cc_for3 // ]
                | 3: %{(State (simplify_function f)
                              (Sfor Sskip (simplify_e cond) (simplify_statement step)
                              (simplify_statement body)) 
                              k0' en m)} @conj
                     [ 1: // | 2: %1 // ]
                ]
           | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
                whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
                %{(State (simplify_function f) Sskip k0' en m)} @conj
                [ 1: // | 2: %1 // ]
           | 9: (* Call *)
                #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ #Eq
                >fn_return_simplify cases (fn_return f) in Eq; normalize nodelta
               [ 1: #Eq whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
                    %{(Returnstate Vundef (Kcall r (simplify_function f0) en0 k0')
                                  (free_list m (blocks_of_env en)))} @conj
                    [ 1: // | 2: %3 @cc_call // ]                                  
               | 3,4,9: #irrelevant #Habsurd destruct (Habsurd)
               | *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ]
           ]
     | 2: (* Assign *)
          #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1
          whd in match (simplify_statement ?); #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          (* Begin by making the simplify_e disappear using Hsim_related *)
          elim (Hsim_lvalue_related lhs) *
          [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd)
          | 1: cases (exec_lvalue ge en m lhs) in Heq;
               [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
               | 1: * * #block #offset #trace
                    whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_lhs
                    lapply (Hsim 〈block, offset, trace〉 (refl ? (OK ? 〈block, offset, trace〉)))
                    #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????);
                    (* After [lhs], treat [rhs] *)
                    elim (Hsim_related rhs) *
                    [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd)
                    | 1: cases (exec_expr ge en m rhs) in Heq;
                         [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                         | 1: * #val #trace
                              whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_rhs
                              lapply (Hsim 〈val, trace〉 (refl ? (OK ? 〈val, trace〉)))
                              #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????);
                              <Htype_eq_lhs <Htype_eq_rhs
                              cases (opt_to_io ?????) in Heq;
                              [ 1: #o #resumption whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
                              | 3: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
                              | 2: #mem whd in match (bindIO ??????); #Heq destruct (Heq)
                                   %{(State (simplify_function f) Sskip k' en mem)} @conj
                                   [ 1: // | 2: %1 // ]
                              ]
                         ]
                    ]
               ]
         ]
    | 3: (* Call *)
         #Heq_s1 #Heq_s1' #_  lapply Houtcome >Heq_s1
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         elim (Hsim_related func) in Heq; *
         [ 2: * #error #Hfail >Hfail #Htype_eq #Habsurd normalize in Habsurd; destruct (Habsurd)
         | 1: cases (exec_expr ??? func)
              [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
              | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq
                   whd in match (bindIO ??????) in ⊢ (% → %);
                   elim (related_globals_exprlist_simulation ge ge' en m Hrelated args)
                   [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
                   | 1: cases (exec_exprlist ge en m args)
                        [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                        | 1: #l -Hsim #Hsim lapply (Hsim l (refl ? (OK ? l))) #Heq >Heq
                             whd in match (bindIO ??????) in ⊢ (% → %);
                             elim Hrelated #_ #Hfunct #_ lapply (Hfunct (\fst a))
                             cases (find_funct clight_fundef ge (\fst a));
                             [ 1: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                             | 2: #clfd -Hsim #Hsim lapply (Hsim clfd (refl ? (Some ? clfd))) #Heq >Heq
                                  whd in match (bindIO ??????) in ⊢ (% → %);
                                  >simplify_type_of_fundef_eq >(simplify_fun_typeof_eq ge en m)
                                  cases (assert_type_eq (type_of_fundef clfd) (fun_typeof func))
                                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                                  | 1: #Htype_eq cases ret                                     
                                       [ 1: whd in match (bindIO ??????) in ⊢ (% → %);
                                            #Eq destruct (Eq)
                                            %{(Callstate (simplify_fundef clfd) (\fst  l) 
                                                         (Kcall (None (block×offset×type)) (simplify_function f) en k') m)}
                                            @conj
                                            [ 1: // | 2: %2 @cc_call // ]
                                       | 2: #fptr whd in match (bindIO ??????) in ⊢ (% → %); 
                                            elim (Hsim_lvalue_related fptr) *
                                            [ 2: * #error #Hfail >Hfail #_
                                                 #Habsurd normalize in Habsurd; destruct (Habsurd)
                                            | 1: cases (exec_lvalue ge en m fptr)
                                                 [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                                                 | 1: #a #Hsim #Htype_eq_fptr >(Hsim a (refl ? (OK ? a)))
                                                      whd in match (bindIO ??????) in ⊢ (% → %);
                                                      #Heq destruct (Heq)
                                                      %{(Callstate (simplify_fundef clfd) (\fst  l)
                                                                   (Kcall (Some (block×offset×type) 〈\fst  a,typeof (simplify_e fptr)〉)
                                                                   (simplify_function f) en k') m)}
                                                      @conj [ 1: // | 2: >(simplify_typeof_eq ge en m) %2 @cc_call // ]
        ] ] ] ] ] ] ] ] ]
    | 4: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         destruct (Heq)
         %{(State (simplify_function f) (simplify_statement stm1) (Kseq (simplify_statement stm2) k') en m)}
         @conj
         [ 1: // | 2: %1 @cc_seq // ]
    | 5: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         elim (Hsim_related cond) in Heq; *
         [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
         | 1: cases (exec_expr ge en m cond)
              [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
              | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq
                   #Htype_eq_cond
                   whd in match (bindIO ??????) in ⊢ (% → %);
                   >(simplify_typeof_eq ge en m)
                   cases (exec_bool_of_val condval (typeof cond))
                   [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                   | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %;
                        [ 1: destruct skip (condtrace)
                             %{(State (simplify_function f) (simplify_statement iftrue) k' en m)} @conj
                             [ 1: // | 2: <e0 %1 // ]
                        | 2: destruct skip (condtrace)
                             %{(State (simplify_function f) (simplify_statement iffalse) k' en m)} @conj
                             [ 1: // | 2: <e0 %1 // ]
                        ] ] ] ]
    | 6: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         elim (Hsim_related cond) in Heq; *
         [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
         | 1: cases (exec_expr ge en m cond)
              [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
              | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq
                   #Htype_eq_cond
                   whd in match (bindIO ??????) in ⊢ (% → %);
                   >(simplify_typeof_eq ge en m)
                   cases (exec_bool_of_val condval (typeof cond))
                   [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                   | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %;
                        [ 1: destruct skip (condtrace)
                             %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) k') en m)}
                             @conj
                             [ 1: // | 2: <e0 %1 @cc_while // ]
                        | 2: destruct skip (condtrace)
                             %{(State (simplify_function f) Sskip k' en m)} @conj
                             [ 1: // | 2: <e0 %1 // ]
                        ] ] ] ]
    | 7: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         destruct (Heq)
         %{(State (simplify_function f) (simplify_statement body)
                  (Kdowhile (simplify_e cond) (simplify_statement body) k') en m)} @conj
         [ 1: // | 2: %1 @cc_dowhile // ]
    | 8: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         cases (is_Sskip init) in Heq;
         [ 2: #Hinit_neq_Sskip elim (simplify_is_not_skip init Hinit_neq_Sskip) #pf #Hrewrite >Hrewrite
              normalize nodelta
              whd in match (ret ??) in ⊢ (% → %);
              #Eq destruct (Eq)
              %{(State (simplify_function f) (simplify_statement init)
                       (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) k') en m)} @conj
              [ 1: // | 2: %1 @cc_for1 // ]   
         | 1: #Hinit_eq_Sskip >Hinit_eq_Sskip 
              whd in match (simplify_statement ?);
              whd in match (is_Sskip ?);
              normalize nodelta
              elim (Hsim_related cond) *
              [ 2: * #error #Hfail #_ >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
              | 1: cases (exec_expr ge en m cond)
                   [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                   | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite #Htype_eq_cond >Hrewrite
                        whd in match (m_bind ?????); whd in match (m_bind ?????);
                        <Htype_eq_cond
                        cases (exec_bool_of_val ? (typeof cond))
                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                        | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????);
                             normalize nodelta #Heq destruct (Heq)
                             [ 1: %{(State (simplify_function f) (simplify_statement body)
                                           (Kfor2 (simplify_e cond) (simplify_statement step) (simplify_statement body) k') en m)}
                                   @conj [ 1: // | 2: %1 @cc_for2 // ]
                             | 2: %{(State (simplify_function f) Sskip k' en m)} @conj
                                  [ 1: // | 2: %1 // ]
         ] ] ] ] ]
    | 9: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         inversion Hcont_cast in Heq; normalize nodelta
         [ 1: #Hk #Hk' #_
         | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 
         | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
         | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
         | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 
         | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
         | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
         #H whd in match (ret ??) in H ⊢ %;
         destruct (H)
         [ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: // | 2,4: %1 // ]
         | 2,3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ]
    | 10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         inversion Hcont_cast in Heq; normalize nodelta
         [ 1: #Hk #Hk' #_
         | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 
         | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
         | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
         | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 
         | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
         | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
         #H whd in match (ret ??) in H ⊢ %;
         destruct (H)
         [ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 //
         | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} 
              @conj try // %1 //
         | 3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H;
              [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
              | 1: cases (exec_expr ??? cond)
                   [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                   | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
                        whd in match (m_bind ?????) in ⊢ (% → %);
                        <Htype_cond_eq
                        cases (exec_bool_of_val ? (typeof cond))
                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                        | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????);
                             normalize nodelta #Heq destruct (Heq)
                             [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)}
                                  @conj [ 1: // | 2: %1 // ]
                             | 2: %{(State (simplify_function f) Sskip k0' en m)}
                                  @conj [ 1: // | 2: %1 // ]
             ] ] ] ]
         | 5: %{(State (simplify_function f) (simplify_statement step)
                       (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') en m)} @conj
              [ 1: // | 2: %1 @cc_for3 // ]
         ]
    | 11: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          cases retval in Heq; normalize nodelta
          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
               whd in match (ret ??) in ⊢ (% → %);
               [ 2: #sz #sg | 3: #fl | 4: #ty' | 5: #ty #n | 6: #tl #ty'
               | 7: #id #fl | 8: #id #fl | 9: #id ]
               #H destruct (H)
               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))}
               @conj [ 1: // | 2: %3 @call_cont_simplify // ]
          | 2: #e >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta
               [ 1: #_ #Habsurd destruct (Habsurd)
               | 2: #_ elim (Hsim_related e) *
                    [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                    | 1: cases (exec_expr ??? e)
                         [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                         | 1: #a #Hsim #Htype_eq_e lapply (Hsim a (refl ? (OK ? a)))
                              #Hrewrite >Hrewrite
                              whd in match (m_bind ?????); whd in match (m_bind ?????); 
                              #Heq destruct (Heq)
                              %{(Returnstate (\fst  a) (call_cont k') (free_list m (blocks_of_env en)))}
                              @conj [ 1: // | 2: %3 @call_cont_simplify // ]
         ] ] ] ]
    | 12: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          elim (Hsim_related cond) in Heq; *
          [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
          | 1: cases (exec_expr ??? cond)
               [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
               | 1: #a #Hsim #Htype_eq_cond lapply (Hsim a (refl ? (OK ? a)))
                    #Hrewrite >Hrewrite
                    whd in match (bindIO ??????); whd in match (bindIO ??????);
                    cases (\fst a) normalize nodelta
                    [ 1,3,4,5: #a destruct (a) #b destruct (b)
                    | 2: #sz #i whd in match (ret ??) in ⊢ (% → %); #Heq destruct (Heq)
                         %{(State (simplify_function f)
                                  (seq_of_labeled_statement (select_switch sz i (simplify_ls switchcases)))
                                  (Kswitch k') en m)} @conj
                         [ 1: //
                         | 2: @(labeled_statements_ind … switchcases)
                              [ 1: #default_s
                                   whd in match (simplify_ls ?);
                                   whd in match (select_switch sz i ?) in ⊢ (?%%);
                                   whd in match (seq_of_labeled_statement ?) in ⊢ (?%%);
                                   %1 @cc_switch //
                              | 2: #sz' #i' #top_case #tail #Hind
                                   cut ((seq_of_labeled_statement (select_switch sz i (simplify_ls (LScase sz' i' top_case tail))))
                                         = (simplify_statement (seq_of_labeled_statement (select_switch sz i (LScase sz' i' top_case tail)))))
                                   [ 1: >select_switch_commute >simplify_ls_commute @refl
                                   | 2: #Hrewrite >Hrewrite
                                        %1 @cc_switch //
         ] ] ] ] ] ]
    | 13: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          destruct (Heq)
          %{(State (simplify_function f) (simplify_statement body) k' en m)}
          @conj %1 //
   | 14: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          lapply (cast_find_label_fn lab f (call_cont k) (call_cont k'))
          cases (find_label lab (fn_body f) (call_cont k)) in Heq;
          normalize nodelta
          [ 1: #Habsurd destruct (Habsurd)
          | 2: * #st #kst normalize nodelta
               #Heq whd in match (ret ??) in Heq;
               #H lapply (H st kst (call_cont_simplify ???) (refl ? (Some ? 〈st,kst〉))) try //
               * #kst' * #Heq2 #Hcont_cast' >Heq2 normalize nodelta
               destruct (Heq)
               %{(State (simplify_function f) (simplify_statement st) kst' en m)} @conj
               [ 1: // | 2: %1 // ]
          ]
   | 15: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          destruct (Heq)                    
          %{(State (simplify_function f) (simplify_statement body) k' en m)}
          @conj
          [ 1: // | 2: %1 // ]
   ]
| 2: (* Call state *)
     #fd #args #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     whd in match (exec_step ??) in ⊢ (% → %);
     elim fd in Heq_s1'; normalize nodelta
     [ 1: * #rettype #args #vars #body #Heq_s1'
          whd in match (simplify_function ?);
          cases (exec_alloc_variables empty_env ??)
          #local_env #new_mem normalize nodelta
          cases (exec_bind_parameters ????)
          [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
          | 1: #new_mem_init
               whd in match (m_bind ?????); whd in match (m_bind ?????);
                #Heq destruct (Heq)               
                %{(State (mk_function rettype args vars (simplify_statement body))
                         (simplify_statement body) k' local_env new_mem_init)} @conj
                [ 1: // | 2: %1 // ]
          ]
     | 2: #id #argtypes #rettype #Heq_s1'
          cases (check_eventval_list args ?)
          [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
          | 1: #l whd in match (m_bind ?????); whd in match (m_bind ?????);
          #Habsurd destruct (Habsurd) ]
     ]
| 3: (* Return state *)              
     #res #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     whd in match (exec_step ??) in ⊢ (% → %);
     inversion Hcont_cast 
     [ 1: #Hk #Hk' #_
     | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 
     | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 
     | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
     normalize nodelta
     [ 1: cases res normalize nodelta
          [ 2: * normalize nodelta #i 
               [ 3: #Heq whd in match (ret ??) in Heq; destruct (Heq)
                    %{(Finalstate i)} @conj [ 1: // | 2: // ]
               | * : #Habsurd destruct (Habsurd) ]
          | *: #a try #b destruct ]
     | 9: elim r normalize nodelta
          [ 2: * * #block #offset #typ normalize nodelta
               cases (opt_to_io io_out io_in mem ? (store_value_of_type' ????))
               [ 2: #mem whd in match (m_bind ?????); whd in match (m_bind ?????);
                    #Heq destruct (Heq)
                    %{(State (simplify_function f0) Sskip k0' en0 mem)} @conj
                    [ 1: // | 2: %1 // ]
               | 1: #output #resumption
                    whd in match (m_bind ?????); #Habsurd destruct (Habsurd)
               | 3: #eror #Habsurd normalize in Habsurd; destruct (Habsurd) ]
          | 1: #Heq whd in match (ret ??) in Heq; destruct (Heq)
               %{(State (simplify_function f0) Sskip k0' en0 m)} @conj
               [ 1: // | 2: %1 // ]
          ]
     | *: #Habsurd destruct (Habsurd) ]
| 4: (* Final state *)
     #r #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 
     whd in match (exec_step ??) in ⊢ (% → %);
     #Habsurd destruct (Habsurd)
] qed.